From 39824fcf1860dfe8fa697d5557a86a64fa5c9c68 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 7 Oct 2020 16:51:08 +0100 Subject: [PATCH] Exceptions example and figures. --- macros.tex | 1 + thesis.tex | 119 ++++++++++++++++++++++++++++++++++++++--------------- 2 files changed, 86 insertions(+), 34 deletions(-) diff --git a/macros.tex b/macros.tex index 5a308d6..10a9673 100644 --- a/macros.tex +++ b/macros.tex @@ -348,6 +348,7 @@ \newcommand{\iter}{\dec{iter}} \newcommand{\stdout}{\dec{stdout}} \newcommand{\IO}{\dec{IO}} +\newcommand{\BIO}{\dec{BIO}} \newcommand{\Alice}{\dec{Alice}} \newcommand{\Bob}{\dec{Bob}} \newcommand{\Root}{\dec{Root}} diff --git a/thesis.tex b/thesis.tex index 511db7f..311d941 100644 --- a/thesis.tex +++ b/thesis.tex @@ -2051,10 +2051,10 @@ model for strings, $\String \defas \List~\Char$, such that we can use string literal notation to denote the $\strlit{contents of a file}$. % The signature of the basic file system will consist of a single -operation $\Putc$ for writing a single character to the file. +operation $\Write$ for writing a list of characters to the file. % \[ - \IO \defas \{\Putc : \Record{\UFD;\Char} \opto \UnitType\} + \BIO \defas \{\Write : \Record{\UFD;\String} \opto \UnitType\} \] % The operation is parameterised by a file descriptor ($\UFD$) and a @@ -2067,51 +2067,52 @@ Let us define a suitable handler for this operation. % \[ \bl - \basicIO : (\UnitType \to \alpha \eff \IO) \to \Record{\alpha; \UFile}\\ + \basicIO : (\UnitType \to \alpha \eff \BIO) \to \Record{\alpha; \UFile}\\ \basicIO~m \defas \ba[t]{@{~}l} \Handle\;m\,\Unit\;\With\\ ~\ba{@{~}l@{~}c@{~}l} \Return\;res &\mapsto& \Record{res;\nil}\\ - \OpCase{\Putc}{\Record{\_;c}}{resume} &\mapsto& - \Let\; \Record{res;file} = resume\,\Unit\;\In\; - \Record{res; c \cons file} + \OpCase{\Write}{\Record{\_;cs}}{resume} &\mapsto& + \ba[t]{@{}l} + \Let\; \Record{res;file} = resume\,\Unit\;\In\\ + \Record{res; cs \concat file} + \ea \ea \ea \el \] % The handler takes as input a computation that produces some value -$\alpha$, and in doing so may perform the $\IO$ effect. +$\alpha$, and in doing so may perform the $\BIO$ effect. % The handler ultimately returns a pair consisting of the return value $\alpha$ and the final state of the file. % The $\Return$-case pairs the result $res$ with the empty file $\nil$ which models the scenario where the computation $m$ performed no -$\Putc$-operations, e.g. +$\Write$-operations, e.g. $\basicIO\,(\lambda\Unit.\Unit) \reducesto^+ \Record{\Unit;\strlit{}}$. % -The $\Putc$-case extends the file by first invoking the resumption, +The $\Write$-case extends the file by first invoking the resumption, whose return type is the same as the handler's return type, thus it returns a pair containing the result of $m$ and the file state. The -file gets extended with the character $c$ before it is returned along -with the original result of $m$. The file is effectively built bottom -up starting with the last character. +file gets extended with the character sequence $cs$ before it is +returned along with the original result of $m$.% The file is +% effectively built bottom up starting with the last character. -Let us define an auxiliary function that writes a string to a given -file. +Let us define an auxiliary function that writes a string to the $\stdout$ file. % \[ \bl - \echo : \String \to \UnitType \eff \{\Putc : \Record{\UFD;\Char} \opto \UnitType\}\\ - \echo~cs \defas \iter\,(\lambda c.\Do\;\Putc\,\Record{\stdout;c})\,cs + \echo : \String \to \UnitType \eff\, \BIO\\%\{\Write : \Record{\UFD;\String} \opto \UnitType\}\\ + \echo~cs \defas \Do\;\Write\,\Record{\stdout;cs} \el \] % -The function $\echo$ invokes the operation $\Putc$ point-wise on the -list of characters $cs$ by using the list iteration function $\iter$. +The function $\echo$ is a simple wrapper around an invocation of +$\Write$. % We can now write some contents to the file and observe the effects. % @@ -2125,17 +2126,44 @@ We can now write some contents to the file and observe the effects. \subsection{Exceptions: non-local exits} \label{sec:tiny-unix-exit} +A process may terminate successfully by running to completion, or it +may terminate with success or failure in the middle of some +computation by performing an \emph{exit} system call. The exit system +call is typically parameterised by an integer value intended to +indicate whether the exit was due to success or failure. By +convention, \UNIX{} interprets the integer zero as success and any +nonzero integer as failure, where the specific value is supposed to +correspond to some known error code. +% + +We can model the exit system call by way of a single operation +$\Exit$. +% \[ \Status \defas \{\Exit : \Int \opto \Zero\} \] - +% +The operation is parameterised by an integer value, however, an +invocation of $\Exit$ can never return, because the type $\Zero$ is +uninhabited. Thus $\Exit$ acts like an exception. +% +It is convenient to abstract invocations of $\Exit$ to make it +possible to invoke the operation in any context. +% \[ \bl \exit : \Int \to \alpha \eff \Status\\ \exit~n \defas \Absurd\;(\Do\;\Exit~n) \el \] - +% +The $\Absurd$ computation term is used to coerce the return type +$\Zero$ of $\Fail$ into $\alpha$. This coercion is safe, because +$\Zero$ is an uninhabited type. +% +An interpretation of $\Fail$ amounts to implementing an exception +handler. +% \[ \bl \status : (\UnitType \to \alpha \eff \Status) \to \Int\\ @@ -2149,7 +2177,17 @@ We can now write some contents to the file and observe the effects. \ea \el \] +% +Following the \UNIX{} convention, the $\Return$-case interprets a +successful completion of $m$ as the integer $0$. The operation case +returns whatever payload the $\Exit$ operation was carrying. As a +consequence, outside of $\status$, an invocation of $\Exit~0$ in $m$ +is indistinguishable from $m$ returning normally, e.g. +$\status\,(\lambda\Unit.\exit~0) = \status\,(\lambda\Unit.\Unit)$. +To illustrate $\status$ and $\exit$ in action consider the following +example, where the computation gets terminated mid-way. +% \[ \ba{@{~}l@{~}l} &\bl @@ -2160,6 +2198,8 @@ We can now write some contents to the file and observe the effects. \reducesto^+& \Record{1;\strlit{dead}} : \Record{\Int;\UFile} \ea \] +% +The (delimited) continuation of $\exit~1$ is effectively dead code. \subsection{Dynamic binding: user-specific environments} \label{sec:tiny-unix-env} @@ -2315,6 +2355,8 @@ string. \el \] +\dhil{This is an instance of non-blind backtracking} + \[ \bl \interrupt : \UnitType \to \UnitType \eff \{\Interrupt : \UnitType \opto \UnitType\}\\ @@ -2377,15 +2419,15 @@ string. \hline \strlit{hamlet}\tikzmark{hamlet}\\ \hline - \strlit{ritchie.txt}\\ + \strlit{ritchie.txt}\tikzmark{ritchie}\\ \hline \multicolumn{1}{| c |}{$\cdots$}\\ \hline - \strlit{act3}\\ + \strlit{stdout}\tikzmark{stdout}\\ \hline \multicolumn{1}{| c |}{$\cdots$}\\ \hline - \strlit{stdout}\\ + \strlit{act3}\tikzmark{act3}\\ \hline \end{tabular} \hspace{1.5cm} @@ -2393,13 +2435,13 @@ string. \hline \multicolumn{1}{| c |}{\textbf{I-List}} \\ \hline - 2\\ + 1\tikzmark{ritchieino}\\ \hline - 1\tikzmark{hamletino}\\ + 2\tikzmark{hamletino}\\ \hline \multicolumn{1}{| c |}{$\cdots$}\\ \hline - 1\\ + 1\tikzmark{stdoutino}\\ \hline \end{tabular} \hspace{1.5cm} @@ -2407,18 +2449,27 @@ string. \hline \multicolumn{1}{| c |}{\textbf{Data region}} \\ \hline - \strlit{UNIX is basically...}\\ + \tikzmark{stdoutdr}\strlit{}\\ \hline \tikzmark{hamletdr}\strlit{To be, or not to be...}\\ \hline \multicolumn{1}{| c |}{$\cdots$}\\ \hline - \strlit{}\\ + \tikzmark{ritchiedr}\strlit{UNIX is basically...}\\ \hline \end{tabular} - \tikz[remember picture,overlay]\draw[->,thick] ([xshift=1.3cm,yshift=0.1cm]pic cs:hamlet) -- ([xshift=-0.85cm,yshift=0.1cm]pic cs:hamletino) node[] {}; - \tikz[remember picture,overlay]\draw[->,thick] ([xshift=0.62cm,yshift=0.1cm]pic cs:hamletino) -- ([xshift=-0.23cm,yshift=0.1cm]pic cs:hamletdr) node[] {}; - \caption{\UNIX{} directory, i-list, and data region mappings}\label{fig:unix-mappings} + %% Hamlet arrows. + \tikz[remember picture,overlay]\draw[->,thick,out=30,in=160] ([xshift=1.3cm,yshift=0.1cm]pic cs:hamlet) to ([xshift=-0.85cm,yshift=0.1cm]pic cs:hamletino) node[] {}; + \tikz[remember picture,overlay]\draw[->,thick,out=30,in=180] ([xshift=0.62cm,yshift=0.1cm]pic cs:hamletino) to ([xshift=-0.23cm,yshift=0.1cm]pic cs:hamletdr) node[] {}; + %% Ritchie arrows. + \tikz[remember picture,overlay]\draw[->,thick,out=-30,in=180] ([xshift=0.22cm,yshift=0.1cm]pic cs:ritchie) to ([xshift=-0.85cm,yshift=0.1cm]pic cs:ritchieino) node[] {}; + \tikz[remember picture,overlay]\draw[->,thick,out=30,in=180] ([xshift=0.62cm,yshift=0.1cm]pic cs:ritchieino) to ([xshift=-0.23cm,yshift=0.1cm]pic cs:ritchiedr) node[] {}; + %% Act3 arrow. + \tikz[remember picture,overlay]\draw[->,thick,out=10,in=210] ([xshift=1.73cm,yshift=0.1cm]pic cs:act3) to ([xshift=-0.85cm,yshift=-0.5mm]pic cs:hamletino) node[] {}; + %% Stdout arrows. + \tikz[remember picture,overlay]\draw[->,thick,out=30,in=180] ([xshift=1.3cm,yshift=0.1cm]pic cs:stdout) to ([xshift=-0.85cm,yshift=0.1cm]pic cs:stdoutino) node[] {}; + \tikz[remember picture,overlay]\draw[->,thick,out=30,in=180] ([xshift=0.62cm,yshift=0.1cm]pic cs:stdoutino) to ([xshift=-0.23cm,yshift=0.1cm]pic cs:stdoutdr) node[] {}; + \caption{\UNIX{} directory, i-list, and data region mappings.}\label{fig:unix-mappings} \end{figure} @@ -2465,9 +2516,9 @@ string. % \draw (client) -- (client_ground); \draw (server) -- (server_ground); - \draw[->] ($(client)!0.25!(client_ground)$) -- node[rotate=-6,above,scale=0.7,midway]{SYN 42} ($(server)!0.40!(server_ground)$); - \draw[<-] ($(client)!0.56!(client_ground)$) -- node[rotate=6,above,scale=0.7,midway]{SYN 84;ACK 43} ($(server)!0.41!(server_ground)$); - \draw[->] ($(client)!0.57!(client_ground)$) -- node[rotate=-6,above,scale=0.7,midway]{ACK 44} ($(server)!0.72!(server_ground)$); + \draw[->,thick] ($(client)!0.25!(client_ground)$) -- node[rotate=-6,above,scale=0.7,midway]{SYN 42} ($(server)!0.40!(server_ground)$); + \draw[<-,thick] ($(client)!0.56!(client_ground)$) -- node[rotate=6,above,scale=0.7,midway]{SYN 84;ACK 43} ($(server)!0.41!(server_ground)$); + \draw[->,thick] ($(client)!0.57!(client_ground)$) -- node[rotate=-6,above,scale=0.7,midway]{ACK 85} ($(server)!0.72!(server_ground)$); \end{tikzpicture} \caption{Sequence diagram for the TCP handshake example.}\label{fig:tcp-handshake} \end{figure}