note

thesis.bib

@@ -264,6 +264,20 @@
   year      = {2019}
 }
 
+@article{FowlerLMD19,
+  author    = {Simon Fowler and
+               Sam Lindley and
+               J. Garrett Morris and
+               S{\'{a}}ra Decova},
+  title     = {Exceptional asynchronous session types: session types without tiers},
+  journal   = {Proc. {ACM} Program. Lang.},
+  volume    = {3},
+  number    = {{POPL}},
+  pages     = {28:1--28:29},
+  year      = {2019}
+}
+
+
 @phdthesis{Kammar14,
   author    = {Ohad Kammar},
   title     = {Algebraic theory of type-and-effect systems},

thesis.tex

@@ -5396,22 +5396,19 @@ some return value $\alpha$ and a set of effects $\varepsilon$ that the
 process may perform.
 %
 \[
-  \Pstate~\alpha~\varepsilon \defas \forall \theta.
-     \ba[t]{@{}l@{}l}
+  \Pstate~\alpha~\varepsilon~\theta \defas
+    \ba[t]{@{}l@{}l}
        [&\Done:\alpha;\\
-        &\Suspended:\UnitType \to \Pstate~\alpha~\varepsilon \eff \{\Interrupt:\theta;\varepsilon\} ]
+        &\Suspended:\UnitType \to \Pstate~\alpha~\varepsilon~\theta \eff \{\Interrupt:\theta;\varepsilon\} ]
      \ea
 \]
 %
-\dhil{Cite resumption monad}
-%
-The $\Done$-tag simply carries the return value of type $\alpha$. The
-$\Suspended$-tag carries a suspended computation, which returns
-another instance of $\Pstate$, and may or may not perform any further
-invocations of $\Interrupt$. Note that, the presence variable $\theta$
-in the effect row is universally quantified in the type alias
-definition. The reason for this particular definition is that the type
-of a value carried by $\Suspended$ is precisely the type of a
+This data type definition is an instance of the \emph{resumption
+  monad}~\cite{Papaspyrou01}. The $\Done$-tag simply carries the
+return value of type $\alpha$. The $\Suspended$-tag carries a
+suspended computation, which returns another instance of $\Pstate$,
+and may or may not perform any further invocations of
+$\Interrupt$. Payload type of $\Suspended$ is precisely the type of a
 resumption originating from a handler that handles only the operation
 $\Interrupt$ such as the following handler.
 %
@@ -5431,7 +5428,13 @@ $\Interrupt$ such as the following handler.
 %
 This handler tags and returns values with $\Done$. It also tags and
 returns the resumption provided by the $\Interrupt$-case with
-$\Suspended$. If we compose this handler with the nondeterminism
+$\Suspended$.
+%
+This particular implementation is amounts to a handler-based variation
+of \citeauthor{Harrison06}'s non-reactive resumption
+monad~\cite{Harrison06}.
+%
+If we compose this handler with the nondeterminism
 handler, then we obtain a term with the following type.
 %
 \[
@@ -5655,7 +5658,7 @@ readily be implemented with an effect handler~\cite{KammarLO13}.
 %
 It is a deliberate choice to leave state for last, because once you
 have state it is tempting to use it excessively --- to the extent it
-becomes platitudinous.
+becomes a cliche.
 %
 As demonstrated in the previous sections, it is possible to achieve
 many things that have a stateful flavour without explicit state by
@@ -7730,14 +7733,19 @@ 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 blocked. Then the process is appended on
+    to the end of the queue, and $\runNext$ is applied recursively to
+    the scheduler state $st'$ 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.
+    within the scheduler state are updated accordingly. The reified
+    process $resume$ is applied to the updated scheduler state $st'$.
 \end{enumerate}
 %
+Evidently, this function may enter an infinite loop if every process
+is in blocked state. This may happen if we deadlock any two processes
+by having them wait on one another.  Using this function we can define
+a handler that implements a process scheduler.
+%
 \[
   \bl
     \scheduler : \Record{\alpha \eff \{\Co;\varepsilon\};\Sstate~\alpha~\varepsilon} \Harrow^\param \List~\alpha \eff \varepsilon\\
@@ -7780,6 +7788,48 @@ split on the process queue. There are three cases to consider.
   \el
 \]
 %
+The handler definition $\scheduler$ takes as input a computation that
+computes a value of type $\alpha$ whilst making use of the concurrency
+operations from the $\Co$ signature. In addition it takes the initial
+scheduler state as input. Ultimately, the handler returns a
+computation that computes a list of $\alpha$s, where all the
+$\Co$-operations have been handled.
+%
+In the definition the scheduler state is bound by the name $st$.
+
+The $\return$ case is invoked when a process completes. The return
+value $x$ is consed onto the list $done$. Subsequently, the function
+$\runNext$ is invoked in order to the next ready process.
+
+The $\UFork$ case implements the semantics for process forking. First
+the child process is constructed by abstracting the parameterised
+resumption $resume$ such that it becomes an unary state-accepting
+function, which can be ascribed type $\Proc~\alpha~\varepsilon$. The
+parameterised resumption applied to the process identifier $0$, which
+lets the receiver know that it assumes the role of child in the
+parent-child relationship amongst the processes. The next line
+retrieves the unique process identifier for the child. Afterwards, the
+child process is pushed on to the queue in ready state. The next line
+updates the scheduler state with the new queue and a new unique
+identifier for the next process. Finally, the parameterised resumption
+is applied to the child process identifier and the updated scheduler
+state.
+
+The $\Wait$ case implements the synchronisation operation. The
+parameter $pid$ is the identifier of the process that the invoking
+process wants to wait on. First we construct an unary state-accepting
+function. Then we check whether there exists a process with identifier
+$pid$ in the queue. If there is one, then we enqueue the current
+process in blocked state. If no such process exists (e.g. it may
+already have finished), then we enqueue the current process in ready
+state. Finally, we invoke $\runNext$ with the scheduler state updated
+with the new process queue in order to run the next ready process.
+
+The $\Interrupt$ case suspends the current process by enqueuing it in
+ready state, and dequeuing the next ready process.
+
+Using this handler we can implement version 2 of the time-sharing
+system.
 %
 \[
   \bl
@@ -7792,6 +7842,18 @@ split on the process queue. There are three cases to consider.
   \el
 \]
 %
+The computation $m$, which may perform any of the concurrency
+operations, is handled by the parameterised handler $\scheduler$. The
+parameterised handler definition is applied to the initial scheduler
+state, which has an empty process queue, an empty done list, and it
+assigns the first process the identifier $1$, and sets up the
+identifier for the next process to be $2$.
+
+With $\UFork$ and $\Wait$ we can implement the \emph{init} process,
+which is the initial startup process in
+\UNIX{}~\cite{RitchieT74}. This process remains alive until the
+operating system is shutdown. It is the ancestor of every process
+created by the operating system.
 %
 \[
   \bl
@@ -7806,6 +7868,14 @@ split on the process queue. There are three cases to consider.
   \el
 \]
 %
+We implement $\init$ as a higher-order function. It takes a main
+routine that will be applied when the system has been started. The
+function first performs $\UFork$ to duplicate itself. The child branch
+executes the $main$ routine, whilst the parent branch waits on the
+child. We somewhat arbitrarily choose to exit the parent branch with
+code $1$ such that we can identify the process in the completion list.
+
+Now we can plug everything together.
 %
 \[
   \ba{@{~}l@{~}l}
@@ -7820,10 +7890,10 @@ split on the process queue. There are three cases to consider.
                   \Let\;pid \revto \Do\;\UFork\,\Unit\;\In\\
                   \If\;pid = 0\\
                   \Then\;\bl
-                         \su~\Alice; \Do\;\Wait~pid;
-                         \quoteRitchie\,\Unit; \exit~2
+                         \su~\Alice;
+                         \quoteRitchie\,\Unit; \exit~3
                        \el\\
-                  \Else\; \su~\Bob; \quoteHamlet\,\Unit;\exit~3))})))}
+                  \Else\; \su~\Bob; \Do\;\Wait~pid; \quoteHamlet\,\Unit;\exit~2))})))}
                  \ea
      \el \smallskip\\
      \reducesto^+&
@@ -7839,10 +7909,10 @@ split on the process queue. There are three cases to consider.
              \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"}}];
+                   \texttt{"}&\texttt{UNIX is basically a simple operating system, but }\\
+                             &\texttt{you have to be a genius to understand the simplicity.\nl}\\
+                             &\texttt{To be, or not to be,\nl{}that is the question:\nl{}}\\
+                             &\texttt{Whether 'tis nobler in the mind to suffer\nl{}"}}]
                  \ea\\
                 lnext=1; inext=1}}\\
            \ea
@@ -7853,21 +7923,110 @@ split on the process queue. There are three cases to consider.
   \ea
 \]
 %
-
+The function provided to $\init$ forks itself. The child branch
+switches user to $\Alice$ and invokes the $\quoteRitchie$ process
+which writes to standard out. The process exits with status code
+$3$. The parent branch switches user to $\Bob$ and waits for the child
+process to complete before it invokes the $\quoteHamlet$ process which
+also writes to standard out, and finally exiting with status code $2$.
+%
+It is evident from looking at the file system state that the writes to
+standard out has not been interleaved as the contents of
+$\strlit{stdout}$ appear in order. We can also see from the process
+status list that Alice's process is the first to complete, and the
+second to complete is Bob's process, whilst the last process to
+complete is the $\init$ process.
 
 \section{Related work}
 \label{sec:unix-related-work}
 
-\subsection{Interleaving computation}
+\paragraph{Programming language support for handlers}
 
-\paragraph{The resumption monad} \citet{Milner75},
-\citet{Plotkin76}, \citet{Moggi90}, \citet{Papaspyrou01}, \citet{Harrison06}, \citet{AtkeyJ15}
+\paragraph{Effect-driven concurrency}
+In their tutorial of the Eff programming language \citet{BauerP15}
+implements a simple lightweight thread scheduler. It is different from
+the schedulers presented in this section as their scheduler only uses
+resumptions linearly. This is achieved by making the fork operation
+\emph{higher-order} such that the operation is parameterised by a
+computation. The computation is run under a fresh instance of the
+handler. On one hand this approach has the benefit of making threads
+cheap as it is no stack copying is necessary at runtime. On the other
+hand it loses the guarantee that every operation is handled uniformly
+(when in the setting of deep handlers) as every handler in between the
+fork operation invocation site and the scheduler handler needs to be
+manually reinstalled when the computation argument is
+run. Nevertheless, this is the approach to concurrency that
+\citet{DolanWSYM15} have adopted for Multicore
+OCaml~\citet{DolanWSYM15}.
+%
+In my MSc(R) dissertation I used a similar approach to implement a
+cooperative version of the actor concurrency model of Links with
+effect handlers~\cite{Hillerstrom16}.
+%
+This line of work was further explored by \citet{Convent17}, who
+implemented various cooperative actor-based concurrency abstractions
+using effect handlers in the Frank programming
+language. \citet{Poulson20} expanded upon this work by investigating
+ways to handle preemptive concurrency.
 
-\paragraph{Continuation-based interleaving}
-First implementation of `threads' is due to \citet{Burstall69}. \citet{Wand80} \citet{HaynesF84} \citet{GanzFW99} \citet{HiebD90}
+\citet{FowlerLMD19} used effect handlers in the setting of
+fault-tolerant distributed programming. They codified a distributed
+exception handling mechanism using a single exception-operation and a
+corresponding effect handler, which automatically closes open
+resources upon handling the exception-operation by \emph{aborting} the
+resumption of the operation, which would cause resource finalisers to
+run.
 
-\subsection{Effect-driven concurrency}
-\citet{BauerP15}, \citet{DolanWSYM15}, \citet{Hillerstrom16}, \citet{DolanEHMSW17}, \citet{Convent17}, \citet{Poulson20}
+\citet{DolanEHMSW17} and \citet{Leijen17a} gave two widely different
+implementations of the async/await idiom using effect
+handlers. \citeauthor{DolanEHMSW17}'s implementation is based on
+higher-order operations with linearly used resumptions, whereas
+\citeauthor{Leijen17a}'s implementation is based on first-order
+operations with multi-shot resumptions, and thus, it is close in the
+spirit to the schedulers we have considered in this chapter.
+
+\paragraph{Continuation-based interleaved computation}
+The very first implementation of `lightweight threads' using
+continuations can possibly be credited to
+\citet{Burstall69}. \citeauthor{Burstall69} used
+\citeauthor{Landin65}'s J operator to arrange tree-based search, where
+each branch would be reified as a continuation and put into a
+queue. \citet{Wand80} \citet{HaynesF84} \citet{GanzFW99}
+\citet{HiebD90}
+
+\paragraph{Resumption monad}
+The resumption monad is both a semantic and programmatic abstraction
+for interleaving computation. \citet{Papaspyrou01} applies a
+resumption monad transformer to construct semantic models of
+concurrent computation. A resumption monad transformer, i.e. a monad
+$T$ that transforms an arbitrary monad $M$ to a new monad $T~M$ with
+commands for interrupting computation.
+%
+\citet{Harrison06} demonstrates the resumption monad as a practical
+programming abstraction by implementing a small multi-tasking
+operating system. \citeauthor{Harrison06} implements two variations of
+the resumption monad: basic and reactive. The basic resumption monad
+is a closed environment for interleaving different strands of
+computations. It is closed in the sense that strands of computation
+cannot interact with the ambient context of their environment. The
+reactive resumption monad makes the environment open by essentially
+registering a callback with an interruption action. This provides a
+way to model system calls.
+
+The origins of the (semantic) resumption monad can be traced back to
+at least \citet{Moggi90}, who described a monad for modelling the
+interleaving semantics of \citeauthor{Milner75}'s \emph{calculus of
+  communicating systems}~\cite{Milner75}.
+
+The usage of \emph{resumption} in the name has a slightly different
+meaning than the term `resumption' we have been using throughout this
+chapter. We have used `resumption' to mean delimited continuation. In
+the setting of the resumption monad it has a precise domain-theoretic
+meaning. It is derived from \citeauthor{Plotkin76}'s domain of
+resumptions, which in turn is derived from \citeauthor{Milner75}'s
+domain of processes~\cite{Milner75,Plotkin76}.
+
+\dhil{Briefly mention \citet{AtkeyJ15}}
 
 \part{Implementation}