diff --git a/thesis.tex b/thesis.tex index 36fa067..6bea51c 100644 --- a/thesis.tex +++ b/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\\