diff --git a/macros.tex b/macros.tex index 987f418..cf51537 100644 --- a/macros.tex +++ b/macros.tex @@ -383,4 +383,5 @@ \newcommand{\quoteRitchie}{\dec{ritchie}} \newcommand{\quoteHamlet}{\dec{hamlet}} \newcommand{\Proc}{\dec{Proc}} -\newcommand{\schedule}{\dec{schedule}} \ No newline at end of file +\newcommand{\schedule}{\dec{schedule}} +\newcommand{\fsname}{BSFS} \ No newline at end of file diff --git a/thesis.bib b/thesis.bib index e8d5dc8..75dafd8 100644 --- a/thesis.bib +++ b/thesis.bib @@ -318,6 +318,14 @@ year = {2020} } +@MastersThesis{Poulson20, + author = {Leo Poulson}, + title = {Asynchronous Effect Handling}, + school = {School of Informatics, The University of Edinburgh}, + address = {Scotland}, + year = 2020, +} + # Effekt @article{BrachthauserSO18, author = {Jonathan Immanuel Brachth{\"{a}}user and diff --git a/thesis.tex b/thesis.tex index 2a3b83c..614012f 100644 --- a/thesis.tex +++ b/thesis.tex @@ -2759,10 +2759,10 @@ to suspend and continue. % If our core calculi had an integrated notion of asynchrony and effects along the lines of \citeauthor{AhmanP20}'s core calculus -$\lambda_{\text{\ae}}$~\cite{AhmanP20}, then we could possibly treat -interruption signals as asynchronous effectful operations, which can -occur spontaneously and, as suggested by \citet{DolanEHMSW17}, be -handled by a user-definable handler. +$\lambda_{\text{\ae}}$~\cite{AhmanP20}, then we could potentially +treat interruption signals as asynchronous effectful operations, which +can occur spontaneously and, as suggested by \citet{DolanEHMSW17} and +realised by \citet{Poulson20}, be handled by a user-definable handler. % In the absence of asynchronous effects we have to inject synchronous @@ -2867,10 +2867,130 @@ 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 +others this may be a modern contemporaneous treatment. As the saying +goes: art is in the eye of the beholder. \subsection{State: file i/o} \label{sec:tiny-unix-io} +Thus far the system supports limited I/O, abnormal process +termination, multiple user sessions, and multi-tasking via concurrent +processes. With the notable exception of I/O the system models the +core features of a practical operating system. The current I/O model +provides an incomplete file system consisting of a single write-only +file. +% +In this section we will complete the file system by implementing a +\UNIX{}-like file system that supports file creation, opening, +truncation, read and write operations, and file linking. +% + +To implement a file system we will need to use state. State can +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. +% +As demonstrated in the previous sections, it is possible to achieve +many things that have a stateful flavour without explicit state by +harnessing the implicit state provided by the program stack. + +In the following subsection, I will provide an interface for stateful +operations and their implementation in terms of a handler. The +stateful operations will be put to use in the subsequent subsection to +implement a basic sequential file system. + +\subsubsection{Handling state} + +The interface for accessing and updating a state cell consists of two +operations. +% +\[ + \State~\beta \defas \{\Get:\UnitType \opto \beta;\Put:\beta \opto \UnitType\} +\] +% +The intended operational behaviour of $\Get$ operation is to read the +value of type $\beta$ of the state cell, whilst the $\Put$ operation +is intended to replace the current value held by the state cell with +another value of type $\beta$. As per usual business, the following +functions abstract the invocation of the operations. +% +\[ + \ba{@{~}l@{\quad\qquad\quad}c@{~}l} + \Uget : \UnitType \to \beta \eff \{\Get:\UnitType \opto \beta\} + & & + \Uput : \UnitType \to \beta \eff \{\Put:\beta \opto \UnitType\}\\ + \Uget~\Unit \defas \Do\;\Get~\Unit + & & + \Uput~st \defas \Do\;\Put~st + \el +\] +% +The following handler interprets the operations. +% +\[ + \bl + \runState : \Record{\beta;\UnitType \to \alpha \eff \State~\beta} \to \Record{\alpha;\beta}\\ + \runState~\Record{st_0;m} \defas + \ba[t]{@{}l} + \Let\;run \revto + \ba[t]{@{}l} + \Handle\;m\,\Unit\;\With\\ + ~\ba{@{~}l@{~}c@{~}l} + \Return\;res &\mapsto& \lambda st.\Record{res;st}\\ + \OpCase{\Get}{\Unit}{resume} &\mapsto& \lambda st.resume~st~st\\ + \OpCase{\Put}{st'}{resume} &\mapsto& \lambda st.resume~\Unit~st' + \ea + \ea\\ + \In\;run~st_0 + \ea + \el +\] +% +The $\runState$ handler provides a generic way to interpret any +stateful computation. It takes as its first parameter the initial +value of the state cell. The second parameter is a potentially +stateful computation. Ultimately, the handler returns the value of the +input computation along with the current value of the state cell. + +This formulation of state handling is analogous to the standard +monadic implementation of state handling~\citep{Wadler95}. In the +context of handlers, the implementation uses a technique known as +\emph{parameter-passing}~\citep{PlotkinP09,Pretnar15}. +% +Each case returns a state-accepting function. +% +The $\Return$-case returns a function that produces a pair consisting +of return value of $m$ and the final state $st$. +% +The $\Get$-case returns a function that applies the resumption +$resume$ to the current state $st$. Recall that return type of a +resumption is the same as its handler's return type, so since the +handler returns a function, it follows that +$resume : \beta \to \beta \to \Record{\alpha, \beta}$. In other words, +the invocation of $resume$ produces another state-accepting +function. This function arises from the next activation of the handler +either by way of a subsequent operation invocation in $m$ or the +completion of $m$ to invoke the $\Return$-case. Since $\Get$ does not +modify the value of the state cell it passes $st$ unmodified to the +next handler activation. +% +The $\Put$-case discards the current state value $st$ and replaces it +by the value $st'$. + +Operationally, evaluation of the sub-computation $m$ gets suspended +when it either invokes an operation or returns a value upon which the +corresponding clause in the handler definition returns a state +accepting function. This function gets bound to $run$ which is +subsequently applied to the initial state $init$, thereby continuing +evaluation of the stateful fragment of $m$. + + +\subsubsection{Basic sequential file system} + \begin{figure} \centering \begin{tabular}[t]{| l |} @@ -2933,39 +3053,6 @@ mishmash poetry of Shakespeare and \UNIX{}. \end{figure} -\[ - \State~\alpha \defas \{\Get:\UnitType \opto \alpha;\Put:\alpha \opto \UnitType\} -\] - -\[ - \bl - \Uget : \UnitType \to \alpha \eff \{\Get:\UnitType \opto \alpha\}\\ - \Uget~\Unit \defas \Do\;\Get~\Unit \medskip\\ - - \Uput : \UnitType \to \alpha \eff \{\Put:\alpha \opto \Unit\}\\ - \Uput~st \defas \Do\;\Put~st - \el -\] - -\[ - \bl - \runState : \Record{\beta;\UnitType \to \alpha \eff \State~\beta} \to \Record{\alpha;\beta}\\ - \runState~\Record{st_0;m} \defas - \ba[t]{@{}l} - \Let\;f \revto - \ba[t]{@{}l} - \Handle\;m\,\Unit\;\With\\ - ~\ba{@{~}l@{~}c@{~}l} - \Return\;res &\mapsto& \lambda st.\Record{res;st}\\ - \OpCase{\Get}{\Unit}{resume} &\mapsto& \lambda st.resume~st~st\\ - \OpCase{\Put}{st'}{resume} &\mapsto& \lambda st.resume~\Unit~st' - \ea - \ea\\ - \In\; f\,st_0 - \ea - \el -\] - \begin{figure} \centering \begin{tikzpicture}[node distance=4cm,auto,>=stealth']