From 2a50b7402cf44de41558ca2871873bd37580a265 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Fri, 2 Oct 2020 01:48:39 +0100
Subject: [PATCH] Code for session management

---
 macros.tex |  7 +++++--
 thesis.tex | 53 +++++++++++++++++++++++++++++++++++++++++++++++------
 2 files changed, 52 insertions(+), 8 deletions(-)

diff --git a/macros.tex b/macros.tex
index 68fbf5a..c7b9b24 100644
--- a/macros.tex
+++ b/macros.tex
@@ -348,6 +348,9 @@
 \newcommand{\Root}{\dec{Root}}
 \newcommand{\User}{\dec{User}}
 \newcommand{\environment}{\dec{env}}
-\newcommand{\EnvE}{\dec{Env}}
+\newcommand{\EnvE}{\dec{Session}}
 \newcommand{\Ask}{\dec{Ask}}
-\newcommand{\whoami}{\dec{whoami}}
\ No newline at end of file
+\newcommand{\whoami}{\dec{whoami}}
+\newcommand{\Su}{\dec{Su}}
+\newcommand{\su}{\dec{su}}
+\newcommand{\sessionmgr}{\dec{sessionmgr}}
\ No newline at end of file
diff --git a/thesis.tex b/thesis.tex
index 0a55334..95b09d3 100644
--- a/thesis.tex
+++ b/thesis.tex
@@ -2185,11 +2185,11 @@ For simplicity we will fix the users to be root, Alice, and Bob.
 
 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$.
+variable can be accessed via an operation $\Ask : \UnitType \opto \String$.
 %
-\[
-  \EnvE \defas \{\Ask : \UnitType \opto \String\}
-\]
+% \[
+%   \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},
@@ -2197,7 +2197,7 @@ which returns the name of the current user.
 %
 \[
   \bl
-    \whoami : \UnitType \to \String \eff \EnvE\\
+    \whoami : \UnitType \to \String \eff \{\Ask : \UnitType \opto \String\}\\
     \whoami~\Unit \defas \Do\;\Ask~\Unit
   \el
 \]
@@ -2206,7 +2206,7 @@ The following handler implements the environment.
 %
 \[
   \bl
-    \environment : \Record{\User;\UnitType \to \alpha \eff \EnvE} \to \alpha\\
+    \environment : \Record{\User;\UnitType \to \alpha \eff \{\Ask : \UnitType \opto \String\}} \to \alpha\\
     \environment~\Record{user;m} \defas
        \ba[t]{@{~}l}
          \Handle\;m\,\Unit\;\With\\
@@ -2245,7 +2245,48 @@ embrace UNIX's laissez-faire attitude and resume with the empty
 string.
 
 \paragraph{Session management}
+%
+\[
+  \EnvE \defas \{\Ask : \UnitType \opto \String;\Su : \User \opto \UnitType\}
+\]
+
+\[
+  \bl
+    \su : \User \to \UnitType \eff \{\Su : \User \opto \UnitType\}\\
+    \su~user \defas \Do\;\Su~user
+  \el
+\]
 
+\[
+  \bl
+    \sessionmgr : \Record{\User; \UnitType \to \alpha \eff \EnvE} \to \alpha\\
+    \sessionmgr~\Record{user;m} \defas
+      \environment\,\langle{}user;(\lambda\Unit.
+         \ba[t]{@{~}l}
+           \Handle\;m\,\Unit\;\With\\
+             ~\ba{@{~}l@{~}c@{~}l}
+                \Return\;res &\mapsto& res\\
+                \Su~user'~resume &\mapsto& \environment\,\Record{user';resume})\rangle
+              \ea
+         \ea
+  \el
+\]
+
+\[
+  \ba{@{~}l@{~}l}
+    &\bl
+      \basicIO\,(\lambda\Unit.\\
+         \qquad\sessionmgr\,\Record{\Root;\lambda\Unit.\\
+           \qquad\qquad\status\,(\lambda\Unit.
+            \ba[t]{@{}l@{~}l}
+              \su~\Alice;&\fwrite\,\Record{\stdout;\whoami\,\Unit};~\fwrite\,\Record{\stdout;\texttt{" "}};\\
+              \su~\Bob;&\fwrite\,\Record{\stdout;\whoami\,\Unit};~\fwrite\,\Record{\stdout;\texttt{" "}};\\
+              \su~\Root;&\fwrite\,\Record{\stdout;\whoami\,\Unit})})
+            \ea
+     \el \smallskip\\
+   \reducesto^+& \Record{0;\texttt{"alice bob root"}} : \Record{\Int;\UFile}
+ \ea
+\]
 \subsection{Nondeterminism: time sharing}
 \label{sec:tiny-unix-time}