Something about fork

thesis.tex

@@ -186,7 +186,8 @@
 %% Finally, a dedication (this is optional -- uncomment the following line if
 %% you want one).
 % \dedication{To my mummy.}
-\dedication{\emph{To be or to do}}
+% \dedication{\emph{To be or to do}}
+\dedication{\emph{Nec temere, nec timide\\(Neither rashly nor timidly)}}
 
 % \begin{preface}
 % A preface will possibly appear here\dots
@@ -2415,13 +2416,62 @@ blocks to build a multi-user system.
 \subsection{Nondeterminism: time sharing}
 \label{sec:tiny-unix-time}
 
+Time sharing is a mechanism that enables multiple processes to run
+concurrently, and hence, multiple users to work concurrently.
+%
+Thus far in our system there is exactly one process.
+%
+In \UNIX{} there exists only a single process whilst the system is
+bootstrapping itself into operation. After bootstrapping is complete
+the system duplicates the initial process to start running user
+managed processes, which may duplicate themselves to create further
+processes.
+%
+The process duplication primitive in \UNIX{} is called
+\emph{fork}~\cite{RitchieT74}.
+%
+The fork-invoking process is typically referred to as the parent
+process, whilst its clone is referred to as the child process.
+%
+Following an invocation of fork, the parent process is provided with a
+nonzero identifier for the child process and the child process is
+provided with the zero identifier. This enables processes to determine
+their respective roles in the parent-child relationship, e.g.
+%
+\[
+  \bl
+    \Let\;i\revto fork~\Unit\;\In\\
+    \If\;i = 0\;\Then\;
+    ~\textit{child's code}\\
+    \Else\;~\textit{parent's code}
+  \el
+\]
+%
+In our system, we can model fork as an effectful operation, that
+returns a boolean to indicate the process role.
+%
 \[
   \bl
     \fork : \UnitType \to \Bool \eff \{\Fork : \UnitType \opto \Bool\}\\
     \fork~\Unit \defas \Do\;\Fork~\Unit
   \el
 \]
-
+%
+By convention we will interpret the return value $\True$ to mean that
+the process is a parent.
+%
+In \UNIX{} the parent process \emph{continues} execution after the
+fork point, and the child process \emph{begins} its execution after
+the fork point.
+%
+Thus, operationally, we may understand fork as returning twice. We can
+implement this behaviour by invoking the resumption arising from an
+invocation of $\Fork$ twice: first with $\True$ to continue the parent
+process, and subsequently with $\False$ to continue the child process
+(or the other way around if we feel inclined).
+%
+The following handler realises this behaviour.
+%
 \[
   \bl
     \nondet : (\UnitType \to \alpha \eff \{\Fork:\UnitType \opto \Bool\}) \to \List~\alpha\\
@@ -2435,16 +2485,17 @@ blocks to build a multi-user system.
          \ea
   \el
 \]
-
+%
 \dhil{This is an instance of non-blind backtracking}
-
+%
 \[
   \bl
     \interrupt : \UnitType \to \UnitType \eff \{\Interrupt : \UnitType \opto \UnitType\}\\
     \interrupt~\Unit \defas \Do\;\Interrupt~\Unit
   \el
 \]
-
+%
+%
 \[
   \Pstate~\alpha~\varepsilon \defas \forall \theta.
      \ba[t]{@{}l@{}l}
@@ -2452,7 +2503,8 @@ blocks to build a multi-user system.
         &\Suspended:\UnitType \to \Pstate~\alpha~\varepsilon \eff \{\Interrupt:\theta';\varepsilon\} ]
      \ea
 \]
-
+%
+%
 \[
   \bl
     \slice : (\UnitType \to \alpha \eff \{\Interrupt:\UnitType \opto \UnitType;\varepsilon\}) \to \Pstate~\alpha~\varepsilon\\
@@ -2466,7 +2518,8 @@ blocks to build a multi-user system.
          \ea
   \el
 \]
-
+%
+%
 \[
   \bl
     \runNext : \List~(\Pstate~\alpha~\{\Fork:\Bool;\varepsilon\}) \to \List~\alpha \eff \varepsilon\\
@@ -2481,7 +2534,8 @@ blocks to build a multi-user system.
                 \ea
   \el
 \]
-
+%
+%
 \[
   \bl
      \timeshare : (\UnitType \to \alpha \eff \{\Fork:\UnitType \opto \Bool;\Interrupt:\UnitType \opto \UnitType;\epsilon\}) \to (\List~\alpha) \eff \epsilon\\