|
|
|
@ -4383,7 +4383,7 @@ the programmer, from continuations in continuation passing style |
|
|
|
(Chapter~\ref{ch:cps}) and continuations in abstract machines |
|
|
|
(Chapter~\ref{ch:abstract-machine}). In the remainder of this |
|
|
|
dissertation I refer to programmatic continuations as `resumptions', |
|
|
|
and reserve the term `continuation' for continuations concerning the |
|
|
|
and reserve the term `continuation' for continuations concerning |
|
|
|
implementation details. |
|
|
|
|
|
|
|
\paragraph{Relation to prior work} The deep and shallow handler |
|
|
|
@ -5394,7 +5394,7 @@ above computations are run concurrently. |
|
|
|
\qquad\qquad\sessionmgr\,\Record{\Root;\lambda\Unit.\\ |
|
|
|
\qquad\qquad\qquad\status\,(\lambda\Unit. |
|
|
|
\ba[t]{@{}l} |
|
|
|
\If\;\fork~\Unit\;\Then\; |
|
|
|
\If\;\fork\,\Unit\;\Then\; |
|
|
|
\su~\Alice;\, |
|
|
|
\quoteRitchie~\Unit\\ |
|
|
|
\Else\; |
|
|
|
@ -5671,7 +5671,7 @@ happens. |
|
|
|
\qquad\qquad\qquad\sessionmgr\,\Record{\Root;\lambda\Unit.\\ |
|
|
|
\qquad\qquad\qquad\qquad\status\,(\lambda\Unit. |
|
|
|
\ba[t]{@{}l} |
|
|
|
\If\;\fork~\Unit\;\Then\; |
|
|
|
\If\;\fork\,\Unit\;\Then\; |
|
|
|
\su~\Alice;\, |
|
|
|
\quoteRitchie~\Unit\\ |
|
|
|
\Else\; |
|
|
|
@ -5701,8 +5701,8 @@ mishmash poetry of Shakespeare and \UNIX{}. |
|
|
|
% |
|
|
|
I will leave it to the reader to be the judge of whether this new |
|
|
|
poetry belongs under the category of either classic arts vandalism or |
|
|
|
novel contemporary reinterpretations. As the idiom goes: \emph{art is |
|
|
|
in the eye of the beholder}. |
|
|
|
novel contemporary reinterpretations. As the saying goes: \emph{art |
|
|
|
is in the eye of the beholder}. |
|
|
|
|
|
|
|
\subsection{State: file i/o} |
|
|
|
\label{sec:tiny-unix-io} |
|
|
|
@ -5953,7 +5953,7 @@ essential administrative structures for file organisation. |
|
|
|
files. In general, a file may have multiple names. Each name is |
|
|
|
stored along with a pointer into the i-list. |
|
|
|
\item The \emph{i-list} is a collection of i-nodes. Each i-node |
|
|
|
contains the meta-data for a file along with a pointer into the data |
|
|
|
contains the meta data for a file along with a pointer into the data |
|
|
|
region. |
|
|
|
\item The \emph{data region} contains the actual file contents. |
|
|
|
\end{enumerate} |
|
|
|
@ -5973,10 +5973,10 @@ have the advantage of having a simple, straightforward implementation. |
|
|
|
% |
|
|
|
\[ |
|
|
|
\ba{@{~}l@{\qquad}c@{~}l} |
|
|
|
\Directory \defas \List~\Record{\String;\Int} &&% |
|
|
|
\DataRegion \defas \List~\Record{\Int;\UFile} \smallskip\\ |
|
|
|
\Directory \defas \List\,\Record{\String;\Int} &&% |
|
|
|
\DataRegion \defas \List\,\Record{\Int;\UFile} \smallskip\\ |
|
|
|
\INode \defas \Record{lno:\Int;loc:\Int} &&% |
|
|
|
\IList \defas \List~\Record{\Int;\INode} |
|
|
|
\IList \defas \List\,\Record{\Int;\INode} |
|
|
|
\ea |
|
|
|
\] |
|
|
|
% |
|
|
|
@ -6147,7 +6147,7 @@ $\URead$ and $\UWrite$ operations. |
|
|
|
\bl |
|
|
|
\Let\;cs\revto \faild\,\Record{\None;\lambda\Unit.\\ |
|
|
|
\quad\Some\,(\fread\,\Record{ino;\Uget\,\Unit})}\\ |
|
|
|
\In\;resume\,cs |
|
|
|
\In\;resume~cs |
|
|
|
\el\\ |
|
|
|
\OpCase{\UWrite}{\Record{ino;cs}}{resume} &\mapsto& |
|
|
|
\ba[t]{@{}l} |
|
|
|
@ -6172,7 +6172,7 @@ writing to a file. Again the file system state is retrieved using |
|
|
|
$\Uget$. The $\Uput$ operation is used to update the file system state |
|
|
|
with the state produced by the successful invocation of |
|
|
|
$\fwrite$. Failure is interpreted as unit, meaning that from the |
|
|
|
caller perspective the operation fails silently. |
|
|
|
caller's perspective the operation fails silently. |
|
|
|
|
|
|
|
\paragraph{File creation and opening} |
|
|
|
The signature of file creation and opening is unsurprisingly comprised |
|
|
|
@ -6212,7 +6212,7 @@ from the functions we already have at our disposal. |
|
|
|
% |
|
|
|
\[ |
|
|
|
\bl |
|
|
|
\dec{has} : \Record{\alpha;\List~\Record{\alpha;\beta}} \to \Bool\\ |
|
|
|
\dec{has} : \Record{\alpha;\List\,\Record{\alpha;\beta}} \to \Bool\\ |
|
|
|
\dec{has}\,\Record{k;xs} \defas \faild\,\Record{\False;(\lambda\Unit.\lookup\,\Record{k;xs};\True)} |
|
|
|
\el |
|
|
|
\] |
|
|
|
@ -6269,11 +6269,11 @@ the new i-node. The last line returns the identifier for the i-node |
|
|
|
along with the modified file system, where the next location ($lnext$) |
|
|
|
and next i-node identifier ($inext$) have been incremented. |
|
|
|
% |
|
|
|
It is worth noting that the effect signature of $\dec{has}$ mentions |
|
|
|
$\Fail$ even though it will (most likely) never fail. It is present in |
|
|
|
the effect row due to the use of $\lookup$ in the $\Then$-branch. This |
|
|
|
application of $\lookup$ can only fail if the file system is in an |
|
|
|
inconsistent state, where the index $ino$ has become stale. The |
|
|
|
It is worth noting that the effect signature of $\fcreate$ mentions |
|
|
|
$\Fail$ even though it will never fail. It is present in the effect |
|
|
|
row due to the use of $\fopen$ and $\lookup$ in the |
|
|
|
$\Then$-branch. Either application can only fail if the file system is |
|
|
|
in an inconsistent state, where the index $ino$ has become stale. The |
|
|
|
$\dec{f}$-family of functions have been carefully engineered to always |
|
|
|
leave the file system in a consistent state. |
|
|
|
% |
|
|
|
@ -6297,13 +6297,13 @@ implementation of $\fileRW$. |
|
|
|
\Let\;\Record{ino;fs} = \fcreate\,\Record{\,fname;\Uget\,\Unit}\\ |
|
|
|
\In\;\Uput~fs;\,\Some~ino} |
|
|
|
\el\\ |
|
|
|
\In\; resume\,ino |
|
|
|
\In\; resume~ino |
|
|
|
\el\\ |
|
|
|
\OpCase{\UOpen}{fname}{resume} &\mapsto& |
|
|
|
\ba[t]{@{}l} |
|
|
|
\Let\; ino \revto \faild~\Record{\None; \lambda \Unit.\\ |
|
|
|
\quad\Some\,(\fopen\,\Record{fname;\Uget\,\Unit})}\\ |
|
|
|
\In\;resume\,ino |
|
|
|
\In\;resume~ino |
|
|
|
\ea |
|
|
|
\ea |
|
|
|
\ea |
|
|
|
@ -6333,7 +6333,7 @@ that allow us to redefine the target of $\Write$ operations locally. |
|
|
|
\ba[t]{@{}l} |
|
|
|
\Let\;ino \revto \Case\;\Do\;\UCreate~fname\;\{ |
|
|
|
\ba[t]{@{~}l@{~}c@{~}l} |
|
|
|
\None &\mapsto& \exit\,1\\ |
|
|
|
\None &\mapsto& \exit~1\\ |
|
|
|
\Some~ino &\mapsto& ino\} |
|
|
|
\ea\\ |
|
|
|
\In\;\Handle\;m\,\Unit\;\With\\ |
|
|
|
@ -6407,7 +6407,7 @@ system in action. |
|
|
|
\qquad\qquad\sessionmgr\,\Record{\Root;\lambda\Unit.\\ |
|
|
|
\qquad\qquad\quad\status\,(\lambda\Unit. |
|
|
|
\ba[t]{@{}l} |
|
|
|
\If\;\fork~\Unit\;\Then\; |
|
|
|
\If\;\fork\,\Unit\;\Then\; |
|
|
|
\su~\Alice;\, |
|
|
|
\quoteRitchie~\redirect~\strlit{ritchie.txt}\\ |
|
|
|
\Else\; |
|
|
|
@ -6612,7 +6612,7 @@ implementation of \fsname{}. |
|
|
|
\bl |
|
|
|
\FileIO \defas \{\FileRW;\FileCO;\FileLU\} \medskip\\ |
|
|
|
\fileIO : (\UnitType \to \alpha \eff \FileIO) \to \alpha \eff \State~\FileSystem \\ |
|
|
|
\fileIO~m \defas \fileRW\,(\lambda\Unit. \fileAlloc\,(\lambda\Unit.\fileLU\,m)) |
|
|
|
\fileIO~m \defas \fileRW\,(\lambda\Unit. \fileAlloc\,(\lambda\Unit.\fileLU~m)) |
|
|
|
\el |
|
|
|
\] |
|
|
|
% |
|
|
|
@ -6686,7 +6686,7 @@ We can now plug it all together. |
|
|
|
\qquad\quad\sessionmgr\,\Record{\Root;\lambda\Unit.\\ |
|
|
|
\qquad\qquad\status\,(\lambda\Unit. |
|
|
|
\ba[t]{@{}l} |
|
|
|
\If\;\fork~\Unit\;\\ |
|
|
|
\If\;\fork\,\Unit\;\\ |
|
|
|
\Then\; |
|
|
|
\bl |
|
|
|
\su~\Alice;\, |
|
|
|
|
