dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00
Code Issues Releases Wiki Activity

Update parameterised example.

Browse Source
This commit is contained in:
Daniel Hillerström
2021-02-10 18:34:16 +00:00
parent cf2422a312
commit 617fd1112c
1 changed files with 24 additions and 21 deletions
Download Patch File Download Diff File Expand all files Collapse all files

45
thesis.tex
View File

@@ -7805,14 +7805,14 @@ a handler that implements a process scheduler.
% %
\[ \[
\bl \bl
\scheduler : \Record{\alpha \eff \{\Co;\varepsilon\};\Sstate~\alpha~\varepsilon} \Harrow^\param \List~\alpha \eff \varepsilon\\ \scheduler : \Record{\alpha \eff \{\Co;\varepsilon\};\Sstate~\alpha~\varepsilon} \Harrow^\param \List\,\Record{\Int;\alpha} \eff \varepsilon\\
\scheduler \defas \scheduler \defas
\bl \bl
st.\\ st.\\
\bl \bl
\Return\;x \mapsto \\ \Return\;x \mapsto \\
\quad\bl \quad\bl
\Let\;done' \revto x \cons st.done\;\In\\ \Let\;done' \revto \Record{st.pid;x} \cons st.done\;\In\\
\runNext\,\Record{st\;\With\;done = done'} \runNext\,\Record{st\;\With\;done = done'}
\el\\ \el\\
\OpCase{\UFork}{\Unit}{resume} \mapsto\\ \OpCase{\UFork}{\Unit}{resume} \mapsto\\
@@ -7855,7 +7855,8 @@ $\Co$-operations have been handled.
In the definition the scheduler state is bound by the name $st$. In the definition the scheduler state is bound by the name $st$.
The $\return$ case is invoked when a process completes. The return The $\return$ case is invoked when a process completes. The return
value $x$ is consed onto the list $done$. Subsequently, the function value $x$ is paired with the identifier of the currently executing
process and consed onto the list $done$. Subsequently, the function
$\runNext$ is invoked in order to the next ready process. $\runNext$ is invoked in order to the next ready process.
The $\UFork$ case implements the semantics for process forking. First The $\UFork$ case implements the semantics for process forking. First
@@ -7890,7 +7891,7 @@ system.
% %
\[ \[
\bl \bl
\timesharee : (\UnitType \to \alpha \eff \Co) \to \List~\alpha\\ \timesharee : (\UnitType \to \alpha \eff \Co) \to \List\,\Record{\Int;\alpha}\\
\timesharee~m \defas \timesharee~m \defas
\bl \bl
\Let\;st_0 \revto \Record{q=\nil;done=\nil;pid=1;pnext=2}\;\In\\ \Let\;st_0 \revto \Record{q=\nil;done=\nil;pid=1;pnext=2}\;\In\\
@@ -7914,13 +7915,13 @@ created by the operating system.
% %
\[ \[
\bl \bl
\init : (\Unit \to \alpha \eff \varepsilon) \to \alpha \eff \{\Co;\Exit : \Int \opto \ZeroType;\varepsilon\}\\ \init : (\Unit \to \alpha \eff \varepsilon) \to \alpha \eff \{\Co;\varepsilon\}\\
\init~main \defas \init~main \defas
\bl \bl
\Let\;pid \revto \Do\;\UFork~\Unit\;\In\\ \Let\;pid \revto \Do\;\UFork~\Unit\;\In\\
\If\;pid = 0\\ \If\;pid = 0\\
\Then\;main\,\Unit\\ \Then\;main\,\Unit\\
\Else\;\Do\;\Wait~pid; \exit~1 \Else\;\Do\;\Wait~pid
\el \el
\el \el
\] \]
@@ -7929,8 +7930,7 @@ We implement $\init$ as a higher-order function. It takes a main
routine that will be applied when the system has been started. The routine that will be applied when the system has been started. The
function first performs $\UFork$ to duplicate itself. The child branch function first performs $\UFork$ to duplicate itself. The child branch
executes the $main$ routine, whilst the parent branch waits on the executes the $main$ routine, whilst the parent branch waits on the
child. We somewhat arbitrarily choose to exit the parent branch with child.
code $1$ such that we can identify the process in the completion list.
Now we can plug everything together. Now we can plug everything together.
% %
@@ -7948,16 +7948,16 @@ Now we can plug everything together.
\If\;pid = 0\\ \If\;pid = 0\\
\Then\;\bl \Then\;\bl
\su~\Alice; \su~\Alice;
\quoteRitchie\,\Unit; \exit~3 \quoteRitchie\,\Unit
\el\\ \el\\
\Else\; \su~\Bob; \Do\;\Wait~pid; \quoteHamlet\,\Unit;\exit~2))})))} \Else\; \su~\Bob; \Do\;\Wait~pid; \quoteHamlet\,\Unit))})))}
\ea \ea
\el \smallskip\\ \el \smallskip\\
\reducesto^+& \reducesto^+&
\bl \bl
\Record{ \Record{
\ba[t]{@{}l} \ba[t]{@{}l}
[1;2;3];\\ [\Record{1;0};\Record{2;0};\Record{3;0}];\\
\Record{ \Record{
\ba[t]{@{}l} \ba[t]{@{}l}
dir=[\Record{\strlit{stdout};0}];\\ dir=[\Record{\strlit{stdout};0}];\\
@@ -7975,24 +7975,27 @@ Now we can plug everything together.
\ea \ea
\ea \ea
\ea\\ \ea\\
: \Record{\List~\Int; \FileSystem} : \Record{\List\,\Record{\Int;\Int}; \FileSystem}
\el \el
\ea \ea
\] \]
% %
The function provided to $\init$ forks itself. The child branch Process number $1$ is $\init$, which forks itself to run its
switches user to $\Alice$ and invokes the $\quoteRitchie$ process argument. The argument runs as process $2$, which also forks itself,
which writes to standard out. The process exits with status code thus creating a process $3$. Process $3$ executes the child branch,
$3$. The parent branch switches user to $\Bob$ and waits for the child which switches user to $\Alice$ and invokes the $\quoteRitchie$
process to complete before it invokes the $\quoteHamlet$ process which process which writes to standard out. Process $2$ executes the parent
also writes to standard out, and finally exiting with status code $2$. branch, which switches user to $\Bob$ and waits for the child process
to complete before it invokes the routine $\quoteHamlet$ which also
writes to standard out.
% %
It is evident from looking at the file system state that the writes to It is evident from looking at the file system state that the writes to
standard out has not been interleaved as the contents of standard out has not been interleaved as the contents of
$\strlit{stdout}$ appear in order. We can also see from the process $\strlit{stdout}$ appear in order. We can also see from the process
status list that Alice's process is the first to complete, and the completion list that Alice's process (pid $3$) is the first to
second to complete is Bob's process, whilst the last process to complete with status $0$, and the second to complete is Bob's process
complete is the $\init$ process. (pid $2$) with status $0$, whilst the last process to complete is the
$\init$ process (pid $1$) with status $0$.
\paragraph{Retrofitting fork} In the previous program we replaced the \paragraph{Retrofitting fork} In the previous program we replaced the
original implementation of $\timeshare$ original implementation of $\timeshare$