UNIX example figures.

code/unix2.links

@@ -441,6 +441,59 @@ fun init(fsys, main) {
   })
 }
 
+###
+### Stream redirection
+###
+sig >> : (Comp(a, { Create: (String) -> FileDescr
+                  , Open: (String) {}-> Option (FileDescr)
+                  , Write:(FileDescr, String) -> () |e}), String)
+             { Create:(String) -> FileDescr
+             , Open:(String) -> Option (FileDescr)
+             , Write:(FileDescr, String) -> ()      |e}~> ()
+op f >> fname {
+  var fd = create(fname);
+  handle(f()) {
+    case Return(_) -> ()
+    case Write(_, cs, resume) ->
+      resume(write(fd, cs))
+  }
+}
+
+sig >>> : (Comp(a, { Create: (String) -> FileDescr
+                   , Open: (String)   -> Option (FileDescr)
+                   , Write:(FileDescr, String) -> () |e}), String)
+             { Create:(String) -> FileDescr
+             , Open:(String) -> Option (FileDescr)
+             , Write:(FileDescr, String) -> ()      |e}~> ()
+op f >>> fname {
+  var fd = switch (open'(fname)) {
+      case None -> create(fname)
+      case Some(fd) -> fd
+  };
+  handle(f()) {
+    case Return(_) -> ()
+    case Write(_, cs, resume) ->
+      resume(write(fd, cs))
+  }
+}
+
+fun example6() {
+  if (fork()) {
+    su(Alice);
+    var fd = create("ritchie.txt");
+    fun(){echo("UNIX is basically a simple operating system, ")} >> "ritchie.txt";
+    fun(){echo("but you have to be a genius to understand the simplicity.")} >>> "ritchie.txt"
+  } else {
+    su(Bob);
+    var hamlet = "hamlet";
+    fun(){echo("To be, or not to be, that is the question:\n")}    >> hamlet;
+    fun(){echo("Whether 'tis nobler in the mind to suffer\n")}    >>> hamlet;
+    fun(){echo("The slings and arrows of outrageous fortune,\n")} >>> hamlet;
+    fun(){echo("Or to take arms against a sea of troubles\n")}    >>> hamlet;
+    fun(){echo("And by opposing end them.")}                      >>> hamlet
+  }
+}
+
 ###
 ### TCP threeway handshake
 ###

macros.tex

@@ -333,6 +333,7 @@
 \newcommand{\conf}{\mathcal{C}}
 
 % UNIX example
+\newcommand{\UNIX}{UNIX}
 \newcommand{\OSname}[0]{Tiny UNIX}
 \newcommand{\exit}{\dec{exit}}
 \newcommand{\Exit}{\dec{Exit}}

thesis.tex

@@ -54,7 +54,7 @@
 \usepackage{tikz}
 \usetikzlibrary{fit,calc,trees,positioning,arrows,chains,shapes.geometric,%
     decorations.pathreplacing,decorations.pathmorphing,shapes,%
-    matrix,shapes.symbols,intersections}
+    matrix,shapes.symbols,intersections,tikzmark}
 
 \usepackage[customcolors,shade]{hf-tikz}  % Shaded backgrounds.
 \hfsetfillcolor{gray!40}
@@ -2011,18 +2011,18 @@ and demonstrate how we can use the power of (deep) effect handlers to
 implement a tiny operating system that supports multiple users,
 time-sharing, and file i/o.
 %
-The operating system will be a variation of UNIX~\cite{RitchieT74},
+The operating system will be a variation of \UNIX{}~\cite{RitchieT74},
 which we will call \OSname{}.
 %
 To make the task tractable we will occasionally jump some hops and
 make some simplifying assumptions, nevertheless the resulting
-implementation will capture the essence of a UNIX-like operating
+implementation will capture the essence of a \UNIX{}-like operating
 system.
 %
 The implementation will be composed of several small modular effect
 handlers, that each handles a particular set of system commands. In
 this respect, we will truly realise \OSname{} in the spirit of the
-UNIX philosophy~\cite[Section~1.6]{Raymond03}.  The implementation of
+\UNIX{} philosophy~\cite[Section~1.6]{Raymond03}.  The implementation of
 the operating system will showcase several computational effects in
 action including \emph{dynamic binding}, \emph{nondeterminism}, and
 \emph{state}.
@@ -2030,22 +2030,22 @@ action including \emph{dynamic binding}, \emph{nondeterminism}, and
 \subsection{Basic i/o}
 \label{sec:tiny-unix-bio}
 
-The file system is a cornerstone of UNIX as the notion of \emph{file}
-in UNIX provides a unified abstraction for storing text, interprocess
+The file system is a cornerstone of \UNIX{} as the notion of \emph{file}
+in \UNIX{} provides a unified abstraction for storing text, interprocess
 communication, and access to devices such as terminals, printers,
 network, etc.
 %
 Initially, we shall take a rather basic view of the file system. In
 fact, our initial system will only contain a single file, and
 moreover, the system will only support writing operations. This system
-hardly qualifies as a UNIX file system. Nevertheless, it serves a
+hardly qualifies as a \UNIX{} file system. Nevertheless, it serves a
 crucial role for development of \OSname{}, because it provides the
 only means for us to be able to observe the effects of processes.
 %
 We defer development of a more advanced file system to
 Section~\ref{sec:tiny-unix-io}.
 
-Much like UNIX we shall model a file as a list of characters, that is
+Much like \UNIX{} we shall model a file as a list of characters, that is
 $\UFile \defas \List~\Char$. For convenience we will use the same
 model for strings, $\String \defas \List~\Char$, such that we can use
 string literal notation to denote the $\strlit{contents of a file}$.
@@ -2164,7 +2164,7 @@ We can now write some contents to the file and observe the effects.
 \subsection{Dynamic binding: user-specific environments}
 \label{sec:tiny-unix-env}
 
-In UNIX an environment maps keys to string-values. A key-value pair is
+In \UNIX{} an environment maps keys to string-values. A key-value pair is
 referred to as an \emph{environment variable}. Each user gets their
 own environment with their own set of environment variables. Some
 environment variable names are common to all environments, but their
@@ -2245,7 +2245,7 @@ an arbitrary number of variables. This can be done by parameterising
 the $\Ask$ operation by some name representation (e.g. a string),
 which the environment handler can use to index into a list of string
 values. In case the name is unbound the environment handler can
-embrace UNIX's laissez-faire attitude and resume with the empty
+embrace \UNIX{}'s laissez-faire attitude and resume with the empty
 string.
 
 \paragraph{Session management}
@@ -2369,6 +2369,59 @@ string.
 \subsection{State: file i/o}
 \label{sec:tiny-unix-io}
 
+\begin{figure}
+  \centering
+  \begin{tabular}[t]{| l |}
+    \hline
+    \multicolumn{1}{| c |}{\textbf{Directory}} \\
+    \hline
+    \strlit{hamlet}\tikzmark{hamlet}\\
+    \hline
+    \strlit{ritchie.txt}\\
+    \hline
+    \multicolumn{1}{| c |}{$\cdots$}\\
+    \hline
+    \strlit{act3}\\
+    \hline
+    \multicolumn{1}{| c |}{$\cdots$}\\
+    \hline
+    \strlit{stdout}\\
+    \hline
+  \end{tabular}
+  \hspace{1.5cm}
+  \begin{tabular}[t]{| c |}
+    \hline
+    \multicolumn{1}{| c |}{\textbf{I-List}} \\
+    \hline
+    2\\
+    \hline
+    1\tikzmark{hamletino}\\
+    \hline
+    \multicolumn{1}{| c |}{$\cdots$}\\
+    \hline
+    1\\
+    \hline
+  \end{tabular}
+  \hspace{1.5cm}
+  \begin{tabular}[t]{| l |}
+    \hline
+    \multicolumn{1}{| c |}{\textbf{Data region}} \\
+    \hline
+    \strlit{UNIX is basically...}\\
+    \hline
+    \tikzmark{hamletdr}\strlit{To be, or not to be...}\\
+    \hline
+    \multicolumn{1}{| c |}{$\cdots$}\\
+    \hline
+    \strlit{}\\
+    \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}
+\end{figure}
+
+
 \[
   \State~\alpha \defas \{\Get:\UnitType \opto \alpha;\Put:\alpha \opto \UnitType\}
 \]
@@ -2402,6 +2455,25 @@ string.
   \el
 \]
 
+\begin{figure}
+  \centering
+  \begin{tikzpicture}[node distance=4cm,auto,>=stealth']
+    \node[] (server) {\bfseries Bob (server)};
+    \node[left = of server] (client) {\bfseries Alice (client)};
+    \node[below of=server, node distance=5cm] (server_ground) {};
+    \node[below of=client, node distance=5cm] (client_ground) {};
+    %
+    \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)$);
+  \end{tikzpicture}
+  \caption{Sequence diagram for the TCP handshake example.}\label{fig:tcp-handshake}
+\end{figure}
+
+\paragraph{TCP threeway handshake}
+
 % The existing literature already contain an extensive amount of
 % introductory examples of programming with (deep) effect
 % handlers~\cite{KammarLO13,Pretnar15,Leijen17}.