From 6588c0581c62ca47fdc3cb15a64b949368274b41 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 17 Feb 2021 17:27:05 +0000 Subject: [PATCH 1/6] idiom => saying --- thesis.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/thesis.tex b/thesis.tex index 22d0cbf..c2f5f6d 100644 --- a/thesis.tex +++ b/thesis.tex @@ -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} From dd0aaa32f62791db162e81d0ad93510b54b1efa0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 17 Feb 2021 17:39:40 +0000 Subject: [PATCH 2/6] Fix typos --- thesis.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/thesis.tex b/thesis.tex index c2f5f6d..2e76f4b 100644 --- a/thesis.tex +++ b/thesis.tex @@ -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 @@ -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} @@ -5963,7 +5963,7 @@ These structures make up the \fsname{}. Figure~\ref{fig:unix-mappings} depicts an example with the three structures and a mapping between them. % -The only file metadata tracked by \fsname{} is the number of names for +The only file meta data tracked by \fsname{} is the number of names for a file. % The three structures and their mappings can be implemented using @@ -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 \] % From 2b21cfcb4e7c70874c04dd0210dbe8b70ff3ff36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 17 Feb 2021 17:49:34 +0000 Subject: [PATCH 3/6] Minor fixes --- thesis.tex | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/thesis.tex b/thesis.tex index 2e76f4b..26eb665 100644 --- a/thesis.tex +++ b/thesis.tex @@ -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 \] @@ -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 From 2f7a6ec818b1fc80de22927e773acd2f12d7fbca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 17 Feb 2021 17:52:13 +0000 Subject: [PATCH 4/6] More minor fixes --- thesis.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/thesis.tex b/thesis.tex index 26eb665..150e8e3 100644 --- a/thesis.tex +++ b/thesis.tex @@ -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\; @@ -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\; @@ -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;\, From f1e1b75ef71704851d43b157f6e898f2c356684c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 17 Feb 2021 18:02:49 +0000 Subject: [PATCH 5/6] Fix more typos --- thesis.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/thesis.tex b/thesis.tex index 150e8e3..fdbb5a4 100644 --- a/thesis.tex +++ b/thesis.tex @@ -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. % From e9cd4315be4be50a76227adcae401015140b4b62 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 17 Feb 2021 18:04:05 +0000 Subject: [PATCH 6/6] Spacing. --- thesis.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thesis.tex b/thesis.tex index fdbb5a4..7a78af5 100644 --- a/thesis.tex +++ b/thesis.tex @@ -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\\