mirror of
https://github.com/dhil/phd-dissertation
synced 2026-03-13 02:58:26 +00:00
WIP
This commit is contained in:
@@ -519,6 +519,8 @@
|
|||||||
\newcommand{\Algol}{Algol~60}
|
\newcommand{\Algol}{Algol~60}
|
||||||
\newcommand{\qq}[1]{\ensuremath{\ulcorner #1 \urcorner}}
|
\newcommand{\qq}[1]{\ensuremath{\ulcorner #1 \urcorner}}
|
||||||
\newcommand{\prompttype}{\dec{Prompt}}
|
\newcommand{\prompttype}{\dec{Prompt}}
|
||||||
|
\newcommand{\async}{\keyw{async}}
|
||||||
|
\newcommand{\await}{\keyw{await}}
|
||||||
|
|
||||||
% Language macros
|
% Language macros
|
||||||
\newcommand{\Frank}{Frank}
|
\newcommand{\Frank}{Frank}
|
||||||
|
|||||||
57
thesis.bib
57
thesis.bib
@@ -1679,6 +1679,28 @@
|
|||||||
address = {USA}
|
address = {USA}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
# Coroutines
|
||||||
|
@article{MouraI09,
|
||||||
|
author = {Ana L{\'{u}}cia de Moura and
|
||||||
|
Roberto Ierusalimschy},
|
||||||
|
title = {Revisiting coroutines},
|
||||||
|
journal = {{ACM} Trans. Program. Lang. Syst.},
|
||||||
|
volume = {31},
|
||||||
|
number = {2},
|
||||||
|
pages = {6:1--6:31},
|
||||||
|
year = {2009}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{AbadiP10,
|
||||||
|
author = {Mart{\'{\i}}n Abadi and
|
||||||
|
Gordon D. Plotkin},
|
||||||
|
title = {A Model of Cooperative Threads},
|
||||||
|
journal = {Log. Methods Comput. Sci.},
|
||||||
|
volume = {6},
|
||||||
|
number = {4},
|
||||||
|
year = {2010}
|
||||||
|
}
|
||||||
|
|
||||||
# Second-hand reference for call/cc
|
# Second-hand reference for call/cc
|
||||||
@techreport{AbelsonHAKBOBPCRFRHSHW85,
|
@techreport{AbelsonHAKBOBPCRFRHSHW85,
|
||||||
author = {William D. Clinger and others},
|
author = {William D. Clinger and others},
|
||||||
@@ -3103,3 +3125,38 @@
|
|||||||
pages = {61--69},
|
pages = {61--69},
|
||||||
year = {2014}
|
year = {2014}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
# Async/await
|
||||||
|
@article{Claessen99,
|
||||||
|
author = {Koen Claessen},
|
||||||
|
title = {A Poor Man's Concurrency Monad},
|
||||||
|
journal = {J. Funct. Program.},
|
||||||
|
volume = {9},
|
||||||
|
number = {3},
|
||||||
|
pages = {313--323},
|
||||||
|
year = {1999}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{LiZ07,
|
||||||
|
author = {Peng Li and
|
||||||
|
Steve Zdancewic},
|
||||||
|
title = {Combining events and threads for scalable network services implementation
|
||||||
|
and evaluation of monadic, application-level concurrency primitives},
|
||||||
|
booktitle = {{PLDI}},
|
||||||
|
pages = {189--199},
|
||||||
|
publisher = {{ACM}},
|
||||||
|
year = {2007}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{SymePL11,
|
||||||
|
author = {Don Syme and
|
||||||
|
Tomas Petricek and
|
||||||
|
Dmitry Lomov},
|
||||||
|
title = {The F{\#} Asynchronous Programming Model},
|
||||||
|
booktitle = {{PADL}},
|
||||||
|
series = {Lecture Notes in Computer Science},
|
||||||
|
volume = {6539},
|
||||||
|
pages = {175--189},
|
||||||
|
publisher = {Springer},
|
||||||
|
year = {2011}
|
||||||
|
}
|
||||||
70
thesis.tex
70
thesis.tex
@@ -151,15 +151,6 @@
|
|||||||
|
|
||||||
%% Specify the abstract here.
|
%% Specify the abstract here.
|
||||||
\abstract{%
|
\abstract{%
|
||||||
% Virtually every programming language is equipped with multiple
|
|
||||||
% different control operators which enable the programmer to manipulate
|
|
||||||
% the flow of control.
|
|
||||||
% %
|
|
||||||
% For example, the operator \emph{if-then-else} lets the programmer
|
|
||||||
% conditionally select between two distinct \emph{continuations}. The
|
|
||||||
% operator \emph{async-await} lets the programmer run multiple
|
|
||||||
% distinct continuations asynchronously and await their results.
|
|
||||||
%
|
|
||||||
First-class control operators provide programmers with an expressive
|
First-class control operators provide programmers with an expressive
|
||||||
and efficient means for manipulating control through reification of
|
and efficient means for manipulating control through reification of
|
||||||
the current control state as a first-class object, enabling
|
the current control state as a first-class object, enabling
|
||||||
@@ -344,12 +335,55 @@
|
|||||||
%%
|
%%
|
||||||
\chapter{Introduction}
|
\chapter{Introduction}
|
||||||
\label{ch:introduction}
|
\label{ch:introduction}
|
||||||
An enthralling introduction\dots
|
Control is an ample ingredient of virtually every programming
|
||||||
|
language. A programming language typically feature a variety of
|
||||||
|
control constructs, which let the programmer manipulate the control
|
||||||
|
flow of programs in interesting ways. The most well-known control
|
||||||
|
construct may well be $\If\;V\;\Then\;M\;\Else\;N$, which
|
||||||
|
conditionally selects between two possible \emph{continuations} $M$
|
||||||
|
and $N$ depending on whether the condition $V$ is $\True$ or
|
||||||
|
$\False$. Another familiar control construct is function application
|
||||||
|
$\EC[(\lambda x.M)\,W]$, which evaluates some parameterised
|
||||||
|
continuation $M$ at value argument $W$ to normal form and subsequently
|
||||||
|
continues the current continuation induced by the invocation context
|
||||||
|
$\EC$.
|
||||||
%
|
%
|
||||||
Motivation: 1) compiler perspective: unifying control abstraction,
|
At the time of writing the trendiest control construct happen to be
|
||||||
lean runtime, desugaring of async/await, generators/iterators, 2)
|
async/await, which is designed for direct-style asynchronous
|
||||||
giving control to programmers, safer microkernels, everything as a
|
programming~\cite{SymePL11}. It takes the form
|
||||||
library.
|
$\async.\,\EC[\await\;M]$, where $\async$ delimits an asynchronous
|
||||||
|
context $\EC$ in which computations may be interleaved. The $\await$
|
||||||
|
primitive may be used to defer execution of the current continuation
|
||||||
|
until the result of the asynchronous computation $M$ is ready. Prior
|
||||||
|
to async/await the most fashionable control construct was coroutines,
|
||||||
|
which provide the programmer with a construct for performing non-local
|
||||||
|
transfers of control by suspending the current continuation on
|
||||||
|
demand~\cite{MouraI09}, e.g. in
|
||||||
|
$\keyw{co_0}.\,\EC_0[\keyw{suspend}];\keyw{co_1}.\,\EC_1[\Unit]$ the
|
||||||
|
two coroutines $\keyw{co_0}$ and $\keyw{co_1}$ work in tandem by
|
||||||
|
invoking suspend in order to hand over control to the other coroutine;
|
||||||
|
$\keyw{co_0}$ suspends the current continuation $\EC_0$ and transfers
|
||||||
|
control to $\keyw{co_1}$, which resume its continuation $\EC_1$ with
|
||||||
|
the unit value $\Unit$. The continuation $\EC_1$ may later suspend in
|
||||||
|
order to transfer control back to $\keyw{co_0}$ such that it can
|
||||||
|
resume execution of the continuation
|
||||||
|
$\EC_0$~\cite{AbadiP10}. Coroutines are amongst the oldest ideas of
|
||||||
|
the literature as they have been around since the dawn of
|
||||||
|
programming~\cite{DahlMN68,DahlDH72,Knuth97,MouraI09}. Nevertheless
|
||||||
|
coroutines frequently reappear in the literature in various guises.
|
||||||
|
|
||||||
|
% Virtually every programming language is equipped with one or more
|
||||||
|
% control flow operators, which enable the programmer to manipulate the
|
||||||
|
% flow of control of programs in interesting ways. The most well-known
|
||||||
|
% control operator may well be $\If\;V\;\Then\;M\;\Else\;N$, which
|
||||||
|
% conditionally selects between two possible \emph{continuations} $M$
|
||||||
|
% and $N$ depending on whether the condition $V$ is $\True$ or $\False$.
|
||||||
|
% %
|
||||||
|
% Another familiar operator is function application\dots
|
||||||
|
|
||||||
|
Evidently, control is a pervasive phenomenon in programming. However,
|
||||||
|
not every control phenomenon is equal in terms of programmability and
|
||||||
|
expressiveness.
|
||||||
|
|
||||||
\section{Why first-class control matters}
|
\section{Why first-class control matters}
|
||||||
|
|
||||||
@@ -358,7 +392,13 @@ library.
|
|||||||
\paragraph{Delimited control}
|
\paragraph{Delimited control}
|
||||||
\paragraph{Composable control}
|
\paragraph{Composable control}
|
||||||
|
|
||||||
\subsection{Why effect handlers}
|
\subsection{Why effect handlers matter}
|
||||||
|
|
||||||
|
\section{State of effectful programming}
|
||||||
|
\subsection{Monadic programming}
|
||||||
|
Monads have given rise to various popular control-oriented programming
|
||||||
|
abstractions, e.g. async/await originates from monadic
|
||||||
|
programming~\cite{Claessen99,LiZ07,SymePL11}.
|
||||||
|
|
||||||
\section{Thesis outline}
|
\section{Thesis outline}
|
||||||
Thesis outline\dots
|
Thesis outline\dots
|
||||||
|
|||||||
Reference in New Issue
Block a user