Minor edits

thesis.bib

@@ -750,6 +750,16 @@
   year      = {2019}
 }
 
+@inproceedings{GibbonsH11,
+  author    = {Jeremy Gibbons and
+               Ralf Hinze},
+  title     = {Just do it: simple monadic equational reasoning},
+  booktitle = {{ICFP}},
+  pages     = {2--14},
+  publisher = {{ACM}},
+  year      = {2011}
+}
+
 # Hop.js
 @inproceedings{SerranoP16,
   author    = {Manuel Serrano and

thesis.tex

@@ -4936,8 +4936,7 @@ returned along with the original result of $m$.
 %
 Intuitively, we may think of this implementation of $\Write$ as a
 peculiar instance of buffered writing, where the contents of the
-operation are committed to the file in last-in-first-out order,
+operation are committed to the file when the computation $m$ finishes.
-i.e. the contents of the last write will be committed first.
 
 Let us define an auxiliary function that writes a string to the
 $\stdout$ file.
@@ -5038,6 +5037,18 @@ example, where the computation gets terminated mid-way.
 \]
 %
 The (delimited) continuation of $\exit~1$ is effectively dead code.
+%
+Here, we have a choice as to how we compose the handlers. Swapping the
+order of handlers would cause the whole computation to return just
+$1 : \Int$, because the $\status$ handler discards the return value of
+its computation. Thus with the alternative layering of handlers the
+system would throw away the file state after the computation
+finishes. However, in this particular instance the semantics the
+(local) behaviour of the operations $\Write$ and $\Exit$ would be
+unaffected if the handlers were swapped. In general the behaviour of
+operations may be affected by the order of handlers. The canonical
+example of this phenomenon is the composition of nondeterminism and
+state, which we will discuss in Section~\ref{sec:tiny-unix-io}.
 
 \subsection{Dynamic binding: user-specific environments}
 \label{sec:tiny-unix-env}
@@ -5248,7 +5259,7 @@ the three user names.
 The above example demonstrates that we now have the basic building
 blocks to build a multi-user system.
 %
-\dhil{Remark on the concrete layering of handlers.}
+%\dhil{Remark on the concrete layering of handlers.}
 
 \subsection{Nondeterminism: time sharing}
 \label{sec:tiny-unix-time}
@@ -5688,9 +5699,10 @@ happens.
 Evidently, each write operation has been interleaved, resulting in a
 mishmash poetry of Shakespeare and \UNIX{}.
 %
-% To some this may be a shambolic treatment of classical arts, whilst to
+I will leave it to the reader to be the judge of whether this new
-% others this may be a modern contemporaneous treatment. As the saying
+poetry belongs under the category of either classic arts vandalism or
-% goes: art is in the eye of the beholder.
+novel contemporary reinterpretations.  As the idiom goes: \emph{art is
+  in the eye of the beholder}.
 
 \subsection{State: file i/o}
 \label{sec:tiny-unix-io}
@@ -5811,8 +5823,30 @@ invoking $\Get$ or $\Put$, the handler returns a function that accepts
 the initial state. The function gets bound to $run$ which is
 subsequently applied to the provided initial state $st_0$ which causes
 evaluation of the stateful fragment of $m$ to continue.
-%
+
-\dhil{Discuss briefly local vs global state~\cite{PauwelsSM19}}
+\paragraph{Local state vs global state} The meaning of stateful
+operations may depend on whether the ambient environment is
+nondeterministic.  Post-composing nondeterminism with state gives rise
+to the so-called \emph{local state} phenomenon, where state
+modifications are local to each strand of nondeterminism, that is each
+strand maintains its own copy of the state. Local state is also known
+as `backtrackable state' in the literature~\cite{GibbonsH11}, because
+returning back to a branch point restores the state as it were prior
+to the branch. In contrast, post-composing state with nondeterminism
+results in a \emph{global state} interpretation, where the state is
+shared across every strand of nondeterminism. In terms of backtracking
+this means the original state does not get restored upon a return to
+some branch point.
+
+For modelling the file system we opt for the global state
+interpretation such that changes made to file system are visible to
+all processes. The local state interpretation could prove useful if we
+were to model a virtual file system per process such that each process
+would have its own unique standard out file.
+
+The two state phenomena are inter-encodable. \citet{PauwelsSM19} give
+a systematic behaviour-preserving transformation for nondeterminism
+with local state into nondeterminism with global state and vice versa.
 
 
 \subsubsection{Basic serial file system}
@@ -7758,25 +7792,26 @@ 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
+completed processes. The scheduler will return an association list of
-there are no more processes to be run. The process queue will consist
+process identifiers mapped to the return value of their respective
-of reified processes, which we will represent using parameterised
+process when there are no more processes to be run. The process queue
-resumptions. To make the type signatures understandable we will make
+will consist of reified processes, which we will represent using
-use of three mutually recursive type aliases.
+parameterised resumptions. To make the type signatures understandable
+we will make use of three mutually recursive type aliases.
 %
 \[
   \ba{@{~}l@{~}l@{~}c@{~}l}
-    \Proc   &\alpha~\varepsilon   &\defas& \Sstate~\alpha~\varepsilon \to \List~\alpha \eff \varepsilon\\
+    \Proc   &\alpha~\varepsilon   &\defas& \Sstate~\alpha~\varepsilon \to \List\,\Record{\Int;\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
 \]
 %
 The $\Proc$ alias is the type of reified processes. It is defined as a
-function that takes the current scheduler state and returns a list of
+function that takes the current scheduler state and returns an
-$\alpha$s. This is almost the type of a parameterised resumption as
+association list of $\alpha$s indexed by integers. This is almost the
-the only thing missing is the a component for the interpretation of an
+type of a parameterised resumption as the only thing missing is the a
-operation.
+component for the interpretation of an operation.
 %
 The second alias $\Pstate$ enumerates the possible process
 states. Either a process is \emph{ready} to be run or it is
@@ -7787,12 +7822,12 @@ 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
+quadruple, where the first label $q$ is the process queue. It is
-as an association list indexed by process identifiers. The label
+implemented as an association list indexed by process identifiers. The
-$done$ is used to store the return values of completed processes. The
+second label $done$ is used to store the return values of completed
-label $pid$ is used to remember the identifier of currently executing
+processes. The third label $pid$ is used to remember the identifier of
-process, and finally $pnext$ is used to compute a unique identifier
+currently executing process, and the fourth label $pnext$ is used to
-for new processes.
+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