From 972b556831e660c0c6c56ca00ac451c4f9c1ca4e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Fri, 2 Oct 2020 00:47:59 +0100 Subject: [PATCH] UNIX example: environment [WIP]. --- macros.tex | 10 +++++- thesis.bib | 16 ++++++++++ thesis.tex | 90 ++++++++++++++++++++++++++++++++++++++++++++++++++++-- 3 files changed, 113 insertions(+), 3 deletions(-) diff --git a/macros.tex b/macros.tex index e978e74..15661b2 100644 --- a/macros.tex +++ b/macros.tex @@ -339,4 +339,12 @@ \newcommand{\fwrite}{\dec{fwrite}} \newcommand{\iter}{\dec{iter}} \newcommand{\stdout}{\dec{stdout}} -\newcommand{\IO}{\dec{IO}} \ No newline at end of file +\newcommand{\IO}{\dec{IO}} +\newcommand{\Alice}{\dec{Alice}} +\newcommand{\Bob}{\dec{Bob}} +\newcommand{\Root}{\dec{Root}} +\newcommand{\User}{\dec{User}} +\newcommand{\environment}{\dec{env}} +\newcommand{\EnvE}{\dec{Env}} +\newcommand{\Ask}{\dec{Ask}} +\newcommand{\whoami}{\dec{whoami}} \ No newline at end of file diff --git a/thesis.bib b/thesis.bib index a5af29f..c594def 100644 --- a/thesis.bib +++ b/thesis.bib @@ -1025,3 +1025,19 @@ publisher = {Pearson Education} } +# GNU coreutils +@book{MacKenzieMPPBYS20, + author = {David MacKenzie + and Jim Meyering + and Ross Paterson + and François Pinard + and Karl Berry + and Brian Youmans + and Richard Stallman}, + title = {{GNU} {Coreutils}}, + note = {for version 8.32}, + month = feb, + year = 2020, + publisher = {Free Software Foundation}, + address = {Boston, MA, USA} +} diff --git a/thesis.tex b/thesis.tex index 1775e2f..2b91d30 100644 --- a/thesis.tex +++ b/thesis.tex @@ -2004,7 +2004,7 @@ operation invocations. This reading was suggested to me by James McKinna (personal communication). In this section I will take this reading literally, and demonstrate how we can use the power of (deep) effect handlers to -implement a small operating system that supports multiple users, +implement a tiny operating system that supports multiple users, time-sharing, and file i/o. % The operating system will be a variation of UNIX~\cite{RitchieT74}, @@ -2121,9 +2121,95 @@ We can now write some contents to the file and observe the effects. \subsection{Exceptions: non-local exits} \label{sec:tiny-unix-exit} -\subsection{Dynamic binding: the environment} +\subsection{Dynamic binding: user-specific environments} \label{sec:tiny-unix-env} +In UNIX an environment maps keys to string-values. A key-value pair is +referred to as an \emph{environment variable}. Each user gets their +own environment with their own set of environment variables. Some +environment variable names are common to all environments, but their +valuation may depend on the particular user session. For example, the +environment variable \texttt{USER} is bound to the (string) name of +the user; the result of querying the environment for the value of +\texttt{USER} depends on which user session it is executed under. +% +\dhil{The value of an environment variable may also change during execution.} + +An environment variable is an instance of dynamic binding. Dynamic +binding is a computational effect which dates back to the original +Lisp~\cite{McCarthy60}. +% +We will use dynamic binding to implement user-specific environments. + +For simplicity we will fix the users to be root, Alice, and Bob. +% +\[ + \User \defas [\Alice;\Bob;\Root] +\] + +Our environment will only support a single environment variable +intended to store the name of the current user. The value of this +variable can be accessed via an operation $\Ask$. +% +\[ + \EnvE \defas \{\Ask : \UnitType \opto \String\} +\] +% +Using this operation we can readily implement the \emph{whoami} +utility from the GNU coreutils~\cite[Section~20.3]{MacKenzieMPPBYS20}, +which returns the name of the current user. +% +\[ + \bl + \whoami : \UnitType \to \String \eff \EnvE\\ + \whoami~\Unit \defas \Do\;\Ask~\Unit + \el +\] +% +The following handler implements the environment. +% +\[ + \bl + \environment : \Record{\User;\UnitType \to \alpha \eff \EnvE} \to \alpha\\ + \environment~\Record{user;m} \defas + \ba[t]{@{~}l} + \Handle\;m\,\Unit\;\With\\ + ~\ba{@{~}l@{~}c@{~}l} + \Return\;res &\mapsto& res\\ + \Ask~\Unit~resume &\mapsto& + \bl + \Case\;user\,\{ + \ba[t]{@{}l@{~}c@{~}l} + \Alice &\mapsto& resume~\texttt{"alice"}\\ + \Bob &\mapsto& resume~\texttt{"bob"}\\ + \Root &\mapsto& resume~\texttt{"root"}\} + \ea + \el + \ea + \ea + \el +\] +% +The handler takes as input the current $user$ and a computation that +may perform the $\Ask$ operation. When an invocation of $\Ask$ occurs +the handler pattern matches on the $user$ parameter and resumes with a +string representation of the user. With this implementation we can +interpret an application of $\whoami$. +% +\[ + \environment~\Record{\Root;\whoami} \reducesto^+ \texttt{"root"} : \String +\] +% +It is not difficult to extend this basic environment model to support +a more faithful UNIX environment supporting an arbitrary number of +variables. This can be done by parameterising the $\Ask$ operation by +some name representation (e.g. a string), which the environment +handler can use to index into a list of string values. In case the +name is unbound the environment handler can adopt the lax attitude of +UNIX and resume with the empty string. + +\paragraph{Session management} + \subsection{Nondeterminism: time sharing} \label{sec:tiny-unix-time}