runNext

macros.tex

@@ -455,6 +455,10 @@
 \newcommand{\ufork}{\dec{ufork}}
 \newcommand{\Wait}{\dec{Wait}}
 \newcommand{\scheduler}{\dec{scheduler}}
+\newcommand{\Sstate}{\dec{Sstate}}
+\newcommand{\Ready}{\dec{Ready}}
+\newcommand{\Blocked}{\dec{Blocked}}
+\newcommand{\init}{\dec{init}}
 
 %%
 %% Some control operators

thesis.tex

@@ -7498,7 +7498,10 @@ being handled. Semantically, parameterised handlers are defined as
 folds with state threading over computation trees.
 
 We take the deep handler calculus $\HCalc$ as our starting point and
-extend it with parameterised handlers to yield the calculus $\HPCalc$.
+extend it with parameterised handlers to yield the calculus
+$\HPCalc$. The parameterised handler extension interacts nicely with
+shallow handlers, and as such it can be added to $\SCalc$ with low
+effort.
 
 \subsection{Syntax and static semantics}
 In addition to a computation, a parameterised handler also take a
@@ -7511,16 +7514,26 @@ cell embedded inside the handler.
 \slab{Parameterised\textrm{ }definitions}   & H^\param   &::=& q^A.~H
 \end{syntax}
 %
-Figure~\ref{fig:param-syntax} extends the syntax of
+The syntactic category of handler types $F$ is extended with a new
-$\HCalc$ with parameterised handlers. Syntactically a parameterised
+kind of handler arrow for parameterised handlers. The left hand side
-handler is new binding form $(q^A.~H)$, where $q$ is the name of the
+of the arrow is a pair, whose first component denotes the type of the
-parameter, whose type is $A$. The name is bound in the ordinary
+input computation and the second component denotes the type of the
-handler definition $H$. The elimination form
+handler parameter. The right hand side denotes the return type of the
-($\ParamHandle\; M\;\With\;H^\param(W)$) is similar to the form for
+handler.
-ordinary deep handlers, except that the parameterised handler
+%
-definition is applied to a value $W$, which is the initial value of
+The computations category is extended with a new application form for
-the parameter $q$.
+handlers, which runs a computation $M$ under a parameterised handler
+$H$ applied to the value $W$.
+%
+Finally, a new category is added for parameterised handler
+definitions. A parameterised handler definition is a new binding form
+$(q^A.~H)$, where $q$ is the name of the parameter, whose type is $A$,
+and $H$ is an ordinary handler definition $H$. The parameter $q$ is
+accessible in the $\Return$ and operation clauses of $H$.
 
+As with ordinary deep handlers and shallow handlers, there are two
+typing rules: one for handler application and another for handler
+definitions.
 %
 \begin{mathpar}
   % Handle
@@ -7532,7 +7545,18 @@ the parameter $q$.
     \typ{\Gamma}{H^\param : \Record{C; A} \Harrow^\param D}
    }
    {\Gamma \vdash \ParamHandle \; M \; \With\; H^\param(W) : D}
-
+\end{mathpar}
+%
+The $\tylab{Handle^\param}$ rule is similar to the $\tylab{Handle}$
+and $\tylab{Handle^\dagger}$ rules, except that it has to account for
+the parameter $W$, whose type has to be compatible with the second
+component of the domain type of the handler definition $H^\param$.
+%
+The typing rule for parameterised handler definitions adapts the
+corresponding typing rule $\tylab{Handler}$ for ordinary deep handlers
+with the addition of a parameter.
+%
+\begin{mathpar}
 % Parameterised handler
   \inferrule*[Lab=\tylab{Handler^\param}]
     {{\bl
@@ -7546,101 +7570,290 @@ the parameter $q$.
     {\typ{\Delta;\Gamma}{(q^{A'} . H) : \Record{C;A'} \Harrow^\param D}}
 \end{mathpar}
 %%
-We require two additional rules to type parameterised handlers. The
+The key differences between the \tylab{Handler} and
-rules are given in Figure~\ref{fig:param-static-semantics}. The main
+\tylab{Handler^\param} rules are that in the latter the return and
-differences between the \tylab{Handler} and \tylab{Handler^\param} are
+operation cases are typed with respect to the parameter $q$, and that
-that in the latter the return and operation cases are typed with
+resumptions $r_i$ have type $\Record{B_\ell;A'} \to D$, that is a
-respect to the parameter $q$, and that resumptions $r$ have type
+parameterised resumption is a binary function, where the first
-$\Record{B_\ell;A'} \to D$, that is they accept a pair as
+argument is the interpretation of an operation and the second argument
-input.
+is the (updated) handler state. The return type of $r_i$ is the same
+as the return type of the handler, meaning that an invocation of $r_i$
+is guarded in the same way as an invocation of an ordinary deep
+resumption.
 
 \subsection{Dynamic semantics}
-Operationally, a parameterised resumption uses the first component as
+The two reduction rules for parameterised handlers adapt the reduction
-the return value of the operation, and the second component as the
+rules for ordinary deep handlers with a parameter.
-updated value of the handler parameter $q$.
 %
-This operational behaviour is formalised by following reduction rule
+\begin{reductions}
-$\semlab{Op^\param}$.
+\semlab{Ret^\param} &
+  \ParamHandle \; (\Return \; V) \; \With \; (q.H)(W) &\reducesto& N[V/x,W/q],\\
+  \multicolumn{4}{@{}r@{}}{
+    \hfill\text{where } \hret = \{ \Return \; x \mapsto N \}} \\
+\semlab{Op^\param} &
+  \ParamHandle \; \EC[\Do \; \ell \, V] \; \With \; (q.H)(W)
+                                                      &\reducesto& N[V/p,W/q,R/r],\\
+\multicolumn{4}{@{}r@{}}{
+  \hfill\ba[t]{@{~}r@{~}l}
+                   \text{where}& R = \lambda\Record{y;q'}.\ParamHandle\;\EC[\Return \; y]\;\With\;(q.H)(q')\\
+                   \text{and}  &\hell = \{ \OpCase{\ell}{p}{r} \mapsto N \}\\
+                   \text{and}  &\ell \notin \BL(\EC)
+              \ea
+}
+\end{reductions}
+%
+The rule $\semlab{Ret^\param}$ handles the return value of a
+computation. Just like the rule $\semlab{Ret}$ the return value $V$ is
+substituted for the binder $x$ in the return case body
+$N$. Furthermore the value $W$ is substituted for the handler
+parameter $q$ in $N$, meaning the handler parameter is accessible in
+the return case.
+
+The $\semlab{Op^\param}$ handles an operation invocation. Both the
+operation payload $V$ and handler argument $W$ are accessible inside
+the case body $N$. As with ordinary deep handlers, the resumption
+rewraps its handler, but with the slight twist that the parameterised
+handler definition is applied to the updated parameter value $q'$
+rather than the original value $W$. This achieves the effect of state
+passing as the value of $q'$ becomes available upon the next
+activation of the handler.
+
+\subsection{Process synchronisation}
+%
+In Section~\ref{sec:tiny-unix-time} we implemented a time-sharing
+system on top of a simple process model. However, the model lacks a
+process synchronisation facility. It is somewhat difficult to cleanly
+add support for synchronisation to the implementation as it is in
+Section~\ref{sec:tiny-unix-time}. Firstly, because the interface of
+$\Fork : \UnitType \to \Bool$ only gives us two possible process
+identifiers: $\True$ and $\False$, meaning at any point we can only
+identify two processes. Secondly, and more importantly, some state is
+necessary to implement synchronisation, but the current implementation
+of process scheduling is split amongst two handlers and one auxiliary
+function, all of which need to coordinate their access and
+manipulation of the state cell. One option is to use some global state
+via the interface from Section~\ref{sec:tiny-unix-io}, which has the
+advantage of making the state manipulation within the scheduler
+modular, but it also has the disadvantage of exposing the state as an
+implementation detail --- and it comes with all the caveats of
+programming with global state. A parameterised handler provides an
+elegant solution, which lets us internalise the state within the
+scheduler.
+
+We will see how a parameterised handler enables us to implement a
+richer process model supporting synchronisation with ease. The effect
+signature of process concurrency is as follows.
 %
 \[
-\ba{@{~}l@{~}l}
+  \Co \defas \{\UFork : \UnitType \opto \Int; \Wait : \Int \opto \UnitType; \Interrupt : \UnitType \opto \UnitType\}
-  &\ParamHandle \; \EC[\Do \; \ell \; V] \; \With \; (q.~H)(W)\\
-  \reducesto&
-  N[V/p,W/q,\lambda \Record{y;q'}.\Handle \; \EC[\Return \; y] \; \With \; (q.~H)(q')/r]\\
-  & \text{ where } \ell \notin BL(\EC) \text{ and } \hell = \{ \OpCase{\ell}{p}{r} \mapsto N \}
-\ea
 \]
 %
-The parameter value $W$ is substituted for the parameter name $q$ into
+The operation $\UFork$ models \UNIX{}
-the operation case body $N$. As with ordinary deep handlers, the
+\emph{fork}~\cite{RitchieT74}. It is generalisation of the $\Fork$
-resumption rewraps its handler, but with the slight twist that the
+operation from Section~\ref{sec:tiny-unix-time}. The operation is
-parameterised handler definition is applied to the updated parameter
+intended to return twice: once to the parent process with a unique
-value $q'$ rather than the original value $W$. The reduction rule for
+process identifier for the child process, and a second time to the
-handling the return of a computation is as follows.
+child process with the zero identifier. The $\Wait$ operation takes a
+process identifier as argument and then blocks the invoking process
+until the process associated with the provided identifier has
+completed. The $\Interrupt$ operation is the same as in
+Section~\ref{sec:tiny-unix-time}; it temporarily suspends the invoking
+process in order to let another process run.
+
+The main idea is to use the state cell of a parameterised handler to
+manage the process queue and to keep track of the return values of
+completed processes. The scheduler will return the list of values when
+there are no more processes to be run. The process queue will consist
+of reified processes, which we will represent using parameterised
+resumptions. To make the type signatures understandable we will make
+use of three mutually recursive type aliases.
 %
 \[
-  \ParamHandle \, (\Return \; V) \; \With \; (q.~H)(W) \reducesto N[V/x,W/q], \text{where } \hret = \{ \Return \; x \mapsto N \}
+  \ba{@{~}l@{~}l@{~}c@{~}l}
+    \Proc   &\alpha~\varepsilon   &\defas& \Sstate~\alpha~\varepsilon \to \List~\alpha \eff \varepsilon\\
+    \Pstate &\alpha~\varepsilon &\defas& [\Ready:\Proc~\alpha~\varepsilon;\Blocked:\Record{\Int;\Proc~\alpha~\varepsilon}]\\
+    \Sstate &\alpha~\varepsilon &\defas& \Record{q:\List\,\Record{\Int;\Pstate~\alpha~\varepsilon};done:\List~\alpha;pid:\Int;pnext:\Int}\\
+  \ea
 \]
 %
-Both the return value $V$ and the parameter value $W$ are substituted
+The $\Proc$ alias is the type of reified processes. It is defined as a
-into the return case body $N$ for their respective binders.
+function that takes the current scheduler state and returns a list of
-
+$\alpha$s. This is almost the type of a parameterised resumption as
-\subsection{Process scheduling}
+the only thing missing is the a component for the interpretation of an
-
+operation.
-\[
+%
-  \Co \defas \{\UFork : \UnitType \opto \Int; \Interrupt : \UnitType \opto \UnitType; \Wait : \Int \opto \UnitType\}
+The second alias $\Pstate$ enumerates the possible process
-\]
+states. Either a process is \emph{ready} to be run or it is
+\emph{blocked} on some other process. The payload of the $\Ready$ tag
+is the process to run. The $\Blocked$ tag is parameterised by a pair,
+where the first component is the identifier of the process that is
+being waited on and the second component is the process to be
+continued when the other process has completed.
+%
+The third alias $\Sstate$ is the type of scheduler state. It is a
+quadruple, where the label $q$ is the process queue. It is implemented
+as an association list indexed by process identifiers. The label
+$done$ is used to store the return values of completed processes. The
+label $pid$ is used to remember the identifier of currently executing
+process, and finally $pnext$ is used to compute a unique identifier
+for new processes.
 
+We will abstract some of the scheduling logic into an auxiliary
+function $\runNext$, which is responsible for dequeuing and running
+the next process from the queue.
+%
 \[
   \bl
-    \dec{SchedState}~\alpha~\varepsilon \defas \Record{\List\,(\dec{Process}~\alpha~\varepsilon);\List~\alpha;\Int;\Int}\\
+    \runNext : \Sstate~\alpha~\varepsilon \to \List~\alpha \eff \varepsilon\\
-    \dec{Process}~\alpha~\varepsilon \defas \dec{SchedState} \to \alpha \eff \varepsilon
+    \runNext~st \defas
+      \bl
+        \Case\;st.q\;\{\\
+        ~\bl
+           \nil \mapsto st.done\\
+           \Record{pid;\Blocked\,\Record{pid';resume}} \cons q' \mapsto\\
+             \quad\bl
+               \Let\;st' \revto \Record{st \;\With\; q = q' \concat [\Record{pid;\Blocked\,\Record{pid';resume}}]}\;\In\\
+               \runNext~st'
+             \el\\
+           \Record{pid;\Ready~resume} \cons q' \mapsto\\
+             \quad\bl
+               \Let\;st' \revto \Record{st \;\With\; q = q'; pid = pid}\;\In\\
+               resume~st'\,\}
+             \el
+         \el
+      \el
   \el
 \]
-
+%
+The function operates on the scheduler state. It first performs a case
+split on the process queue. There are three cases to consider.
+\begin{enumerate}
+  \item The queue is empty. Then the function returns the list $done$,
+    which is the list of process return values.
+  \item The next process is blocked. Then the process is moved to the
+    end of the queue, and the function is applied recursively to the
+    scheduler state with the updated queue.
+  \item The next process is ready. Then the $q$ and $pid$ fields
+    within the scheduler state are updated accordingly. The updated
+    state is supplied as argument to the reified process.
+\end{enumerate}
+%
 \[
   \bl
-    \scheduler : \Record{\alpha \eff \Co;\dec{SchedState}~\alpha~\Co} \Harrow^\param \List~\alpha\\
+    \scheduler : \Record{\alpha \eff \{\Co;\varepsilon\};\Sstate~\alpha~\varepsilon} \Harrow^\param \List~\alpha \eff \varepsilon\\
     \scheduler \defas
     \bl
-    \Record{ps;qs;done;pid;nextpid}.\\
+    st.\\
       \bl
-      \Return\;x \mapsto \Case\;qs \concat ps\;\{\\
+      \Return\;x \mapsto \\
       \quad\bl
-          \nil       \mapsto x \cons done\\
+             \Let\;done' \revto x \cons st.done\;\In\\
-          \Record{pid';qs';resume} \cons ps' \mapsto resume\,\Record{ps';qs';done;pid;nextpid}\}
+             \runNext\,\Record{st\;\With\;done = done'}
            \el\\
       \OpCase{\UFork}{\Unit}{resume} \mapsto\\
       \quad\bl
-              \Let\;ps' \revto \Record{nextpid;\nil;\lambda s.resume~\Record{0;s}} \cons ps\;\In\\
+             \Let\;resume' \revto \lambda st.resume\,\Record{0;st}\;\In\\
-              resume\,\Record{nextpid;\Record{ps';qs;done;pid;nextpid+1}}
+             \Let\;pid \revto st.pnext \;\In\\
+             \Let\;q' \revto  st.q \concat [\Record{pid;\Ready~resume'}]\;\In\\
+             \Let\;st' \revto \Record{st\;\With\;q = q'; pnext = pid + 1}\;\In\\
+             resume\,\Record{pid;st'}
+           \el\\
+      \OpCase{\Wait}{pid}{resume} \mapsto\\
+      \quad\bl
+             \Let\;resume' \revto \lambda st.resume~\Record{\Unit;st}\;\In\\
+             \Let\;q' \revto
+             \bl
+             \If\;\dec{has}\,\Record{pid;st.q}\\
+             \Then\;st.q \concat [\Record{st.pid;\Blocked\,\Record{pid;resume'}}]\\
+             \Else\;st.q \concat [\Record{st.pid;\Ready~resume'}]
+             \el\\
+             \In\;\runNext\,\Record{st\;\With\;q = q'}
            \el\\
       \OpCase{\Interrupt}{\Unit}{resume} \mapsto\\
-           \quad\bl\Let\;\Record{pid';qs';resume'} \cons ps' \revto ps \concat [\Record{pid;qs;\lambda s.resume\,\Record{\Unit;s}}]\;\In\\
-             resume'\,\Record{ps';qs';done;pid';nextpid}
-             \el\\
-         \OpCase{\Wait}{pid'}{resume} \mapsto\\
       \quad\bl
-             \Let\; q \revto \Record{qs;\lambda s.resume\,\Record{\Unit;s}}\;\In\\
+             \Let\;resume' \revto \lambda st.resume\,\Record{\Unit;st}\;\In\\
-             \Let\;\Record{qs';resume'} \revto \lookup\,\Record{pid';ps}\;\In\\
+             \Let\;q' \revto st.q \concat [\Record{st.pid;\Ready~resume'}]\;\In\\
-             \Let\;p \revto \Record{\Record{pid;q} \cons qs;resume'}\;\In\\
+             \runNext~\Record{st \;\With\; q = q'}
-             \Let\;s \revto \modify\,\Record{pid';p;ps}\;\In\\
-             
            \el
       \el
      \el
   \el
 \]
-
+%
+%
 \[
   \bl
     \timesharee : (\UnitType \to \alpha \eff \Co) \to \List~\alpha\\
     \timesharee~m \defas
       \bl
-        \ParamHandle\;m\,\Unit\;\With\; \scheduler~\Record{\nil;1;2}
+        \Let\;st_0 \revto \Record{q=\nil;done=\nil;pid=1;pnext=2}\;\In\\
+        \ParamHandle\;m\,\Unit\;\With\; \scheduler~st_0
       \el
   \el
 \]
+%
+%
+\[
+  \bl
+    \init : (\Unit \to \alpha \eff \varepsilon) \to \alpha \eff \{\Co;\Exit : \Int \opto \ZeroType;\varepsilon\}\\
+    \init~main \defas
+      \bl
+        \Let\;pid \revto \Do\;\UFork~\Unit\;\In\\
+        \If\;pid = 0\\
+        \Then\;main\,\Unit\\
+        \Else\;\Do\;\Wait~pid; \exit~1
+      \el
+  \el
+\]
+%
+%
+\[
+  \ba{@{~}l@{~}l}
+    &\bl
+    \runState\,\Record{\dec{fs}_0;\fileIO\,(\lambda\Unit.\\
+         \quad\timesharee\,(\lambda\Unit.\\
+         \qquad\dec{interruptWrite}\,(\lambda\Unit.\\
+         \qquad\quad\sessionmgr\,\Record{\Root;\lambda\Unit.\\
+         \qquad\qquad\status\,(\lambda\Unit.
+                       \init\,(\lambda\Unit.
+                  \ba[t]{@{}l}
+                  \Let\;pid \revto \Do\;\UFork\,\Unit\;\In\\
+                  \If\;pid = 0\\
+                  \Then\;\bl
+                         \su~\Alice; \Do\;\Wait~pid;
+                         \quoteRitchie\,\Unit; \exit~2
+                       \el\\
+                  \Else\; \su~\Bob; \quoteHamlet\,\Unit;\exit~3))})))}
+                 \ea
+     \el \smallskip\\
+     \reducesto^+&
+     \bl
+      \Record{
+       \ba[t]{@{}l}
+       [1;2;3];\\
+       \Record{
+         \ba[t]{@{}l}
+           dir=[\Record{\strlit{stdout};0}];\\
+           ilist=[\Record{0;\Record{lno=1;loc=0}}];\\
+           dreg=[
+             \ba[t]{@{}l}
+               \Record{0;
+                 \ba[t]{@{}l@{}l}
+                   \texttt{"}&\texttt{To be, or not to be,\nl{}that is the question:\nl{}}\\
+                             &\texttt{Whether 'tis nobler in the mind to suffer\nl{}}\\
+                             &\texttt{UNIX is basically a simple operating system, but }\\
+                             &\texttt{you have to be a genius to understand the simplicity.\nl"}}];
+                 \ea\\
+                lnext=1; inext=1}}\\
+           \ea
+         \ea
+       \ea\\
+       : \Record{\List~\Int; \FileSystem}
+     \el
+  \ea
+\]
+%
+
 
 \section{Related work}
 \label{sec:unix-related-work}