From afb7c4b5cbb4b177f8d643b694b1cf458e492602 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 4 Feb 2021 23:23:21 +0000 Subject: [PATCH] Related work --- thesis.bib | 14 ++++++ thesis.tex | 128 +++++++++++++++++++++++++++++++++++++++++++---------- 2 files changed, 118 insertions(+), 24 deletions(-) diff --git a/thesis.bib b/thesis.bib index c806996..3ab8dc2 100644 --- a/thesis.bib +++ b/thesis.bib @@ -264,6 +264,20 @@ year = {2019} } +@article{FowlerLMD19, + author = {Simon Fowler and + Sam Lindley and + J. Garrett Morris and + S{\'{a}}ra Decova}, + title = {Exceptional asynchronous session types: session types without tiers}, + journal = {Proc. {ACM} Program. Lang.}, + volume = {3}, + number = {{POPL}}, + pages = {28:1--28:29}, + year = {2019} +} + + @phdthesis{Kammar14, author = {Ohad Kammar}, title = {Algebraic theory of type-and-effect systems}, diff --git a/thesis.tex b/thesis.tex index aa980b1..2c63329 100644 --- a/thesis.tex +++ b/thesis.tex @@ -5396,22 +5396,19 @@ some return value $\alpha$ and a set of effects $\varepsilon$ that the process may perform. % \[ - \Pstate~\alpha~\varepsilon \defas \forall \theta. - \ba[t]{@{}l@{}l} + \Pstate~\alpha~\varepsilon~\theta \defas + \ba[t]{@{}l@{}l} [&\Done:\alpha;\\ - &\Suspended:\UnitType \to \Pstate~\alpha~\varepsilon \eff \{\Interrupt:\theta;\varepsilon\} ] + &\Suspended:\UnitType \to \Pstate~\alpha~\varepsilon~\theta \eff \{\Interrupt:\theta;\varepsilon\} ] \ea \] % -\dhil{Cite resumption monad} -% -The $\Done$-tag simply carries the return value of type $\alpha$. The -$\Suspended$-tag carries a suspended computation, which returns -another instance of $\Pstate$, and may or may not perform any further -invocations of $\Interrupt$. Note that, the presence variable $\theta$ -in the effect row is universally quantified in the type alias -definition. The reason for this particular definition is that the type -of a value carried by $\Suspended$ is precisely the type of a +This data type definition is an instance of the \emph{resumption + monad}~\cite{Papaspyrou01}. The $\Done$-tag simply carries the +return value of type $\alpha$. The $\Suspended$-tag carries a +suspended computation, which returns another instance of $\Pstate$, +and may or may not perform any further invocations of +$\Interrupt$. Payload type of $\Suspended$ is precisely the type of a resumption originating from a handler that handles only the operation $\Interrupt$ such as the following handler. % @@ -5431,7 +5428,13 @@ $\Interrupt$ such as the following handler. % This handler tags and returns values with $\Done$. It also tags and returns the resumption provided by the $\Interrupt$-case with -$\Suspended$. If we compose this handler with the nondeterminism +$\Suspended$. +% +This particular implementation is amounts to a handler-based variation +of \citeauthor{Harrison06}'s non-reactive resumption +monad~\cite{Harrison06}. +% +If we compose this handler with the nondeterminism handler, then we obtain a term with the following type. % \[ @@ -5655,7 +5658,7 @@ readily be implemented with an effect handler~\cite{KammarLO13}. % It is a deliberate choice to leave state for last, because once you have state it is tempting to use it excessively --- to the extent it -becomes platitudinous. +becomes a cliche. % As demonstrated in the previous sections, it is possible to achieve many things that have a stateful flavour without explicit state by @@ -7937,16 +7940,93 @@ complete is the $\init$ process. \section{Related work} \label{sec:unix-related-work} -\subsection{Interleaving computation} - -\paragraph{The resumption monad} \citet{Milner75}, -\citet{Plotkin76}, \citet{Moggi90}, \citet{Papaspyrou01}, \citet{Harrison06}, \citet{AtkeyJ15} - -\paragraph{Continuation-based interleaving} -First implementation of `threads' is due to \citet{Burstall69}. \citet{Wand80} \citet{HaynesF84} \citet{GanzFW99} \citet{HiebD90} - -\subsection{Effect-driven concurrency} -\citet{BauerP15}, \citet{DolanWSYM15}, \citet{Hillerstrom16}, \citet{DolanEHMSW17}, \citet{Convent17}, \citet{Poulson20} +\paragraph{Programming language support for handlers} + +\paragraph{Effect-driven concurrency} +In their tutorial of the Eff programming language \citet{BauerP15} +implements a simple lightweight thread scheduler. It is different from +the schedulers presented in this section as their scheduler only uses +resumptions linearly. This is achieved by making the fork operation +\emph{higher-order} such that the operation is parameterised by a +computation. The computation is run under a fresh instance of the +handler. On one hand this approach has the benefit of making threads +cheap as it is no stack copying is necessary at runtime. On the other +hand it loses the guarantee that every operation is handled uniformly +(when in the setting of deep handlers) as every handler in between the +fork operation invocation site and the scheduler handler needs to be +manually reinstalled when the computation argument is +run. Nevertheless, this is the approach to concurrency that +\citet{DolanWSYM15} have adopted for Multicore +OCaml~\citet{DolanWSYM15}. +% +In my MSc(R) dissertation I used a similar approach to implement a +cooperative version of the actor concurrency model of Links with +effect handlers~\cite{Hillerstrom16}. +% +This line of work was further explored by \citet{Convent17}, who +implemented various cooperative actor-based concurrency abstractions +using effect handlers in the Frank programming +language. \citet{Poulson20} expanded upon this work by investigating +ways to handle preemptive concurrency. + +\citet{FowlerLMD19} used effect handlers in the setting of +fault-tolerant distributed programming. They codified a distributed +exception handling mechanism using a single exception-operation and a +corresponding effect handler, which automatically closes open +resources upon handling the exception-operation by \emph{aborting} the +resumption of the operation, which would cause resource finalisers to +run. + +\citet{DolanEHMSW17} and \citet{Leijen17a} gave two widely different +implementations of the async/await idiom using effect +handlers. \citeauthor{DolanEHMSW17}'s implementation is based on +higher-order operations with linearly used resumptions, whereas +\citeauthor{Leijen17a}'s implementation is based on first-order +operations with multi-shot resumptions, and thus, it is close in the +spirit to the schedulers we have considered in this chapter. + +\paragraph{Continuation-based interleaved computation} +The very first implementation of `lightweight threads' using +continuations can possibly be credited to +\citet{Burstall69}. \citeauthor{Burstall69} used +\citeauthor{Landin65}'s J operator to arrange tree-based search, where +each branch would be reified as a continuation and put into a +queue. \citet{Wand80} \citet{HaynesF84} \citet{GanzFW99} +\citet{HiebD90} + +\paragraph{Resumption monad} +The resumption monad is both a semantic and programmatic abstraction +for interleaving computation. \citet{Papaspyrou01} applies a +resumption monad transformer to construct semantic models of +concurrent computation. A resumption monad transformer, i.e. a monad +$T$ that transforms an arbitrary monad $M$ to a new monad $T~M$ with +commands for interrupting computation. +% +\citet{Harrison06} demonstrates the resumption monad as a practical +programming abstraction by implementing a small multi-tasking +operating system. \citeauthor{Harrison06} implements two variations of +the resumption monad: basic and reactive. The basic resumption monad +is a closed environment for interleaving different strands of +computations. It is closed in the sense that strands of computation +cannot interact with the ambient context of their environment. The +reactive resumption monad makes the environment open by essentially +registering a callback with an interruption action. This provides a +way to model system calls. + +The origins of the (semantic) resumption monad can be traced back to +at least \citet{Moggi90}, who described a monad for modelling the +interleaving semantics of \citeauthor{Milner75}'s \emph{calculus of + communicating systems}~\cite{Milner75}. + +The usage of \emph{resumption} in the name has a slightly different +meaning than the term `resumption' we have been using throughout this +chapter. We have used `resumption' to mean delimited continuation. In +the setting of the resumption monad it has a precise domain-theoretic +meaning. It is derived from \citeauthor{Plotkin76}'s domain of +resumptions, which in turn is derived from \citeauthor{Milner75}'s +domain of processes~\cite{Milner75,Plotkin76}. + +\citet{AtkeyJ15} \part{Implementation}