@@ -57,16 +57,56 @@
58\begin{document}
58\begin{document}
60−\title{Cloud Haskell Semantics}
60+\title{Cloud Haskell Semantics (DRAFT)}
61\author{Edsko de Vries, Well-Typed LLP}
61\author{Edsko de Vries, Well-Typed LLP}
62\date{\today}
62\date{\today}
66−\section{Syntax}
66+\section{Introduction}
68+This is a semantics for Cloud Haskell, based on the \textit{Unified Semantics
69+for a Future Erlang} (Hans Svensson, Lars-\AA{}ke Fredlund and Clara Benac
70+Earle, Erlang '10) but using the semantics style of \textit{Composable Memory
71+Transactions} (Tim Harris, Simon Marlow, Simon Peyton-Jones, Maurice Herlihy,
72+PPoPP '05). It differs from the former in that
75+\item We introduce an explicit notion of \textit{reconnecting} (with potential
77+\item We simplify the semantics: we ``flatten'' sets of nodes of processes as
78+sets of processes (but assume a mapping from process identifiers to node
79+identifiers), do not have per-process mailboxes (but only the system queue or
80+``ether'') and do not have an explicit concept of node controllers
83+It differs from the latter in that
86+\item We pretend that the Cloud Haskell \texttt{Process} monad is the top-level
87+monad, and do not consider the \texttt{IO} monad at all
88+\item We ignore exceptions
91+Current imprecisions with respect to the ``real'' Cloud Haskell are
94+\item We ignore the issue of serializability, other than to say that the
95+semantics will get stuck when trying to send a non-serializable payload;
96+consequently, we do not formalize $\mathtt{static}$
97+\item We do not formalize all Cloud Haskell primitives (merging of ports,
98+``advanced messaging'', and others)
99+\item Some of the concepts that we do formalize are lower-level concepts; for
100+instance, the primitive $\sSpawn$ that we formalize is asynchronous (following
101+the Unified semantics); a synchronous construct can be derived.
104+\section{Preliminaries}
68\subsection{Terms}
106\subsection{Terms}
108+We assume the usual definitions of values and terms.
70\begin{equation*}
110\begin{equation*}
71\begin{array}{ll@{\;::=\;}l}
111\begin{array}{ll@{\;::=\;}l}
72\text{value} & V & \sLam{x}{M} \OR
112\text{value} & V & \sLam{x}{M} \OR
@@ -83,6 +123,12 @@
84\subsection{Processes, Nodes, Systems}
124\subsection{Processes, Nodes, Systems}
126+Processes run on \emph{nodes}. We assume that nodes run a special process
127+called the \emph{node controller} which is responsible for issuing monitor
128+messages, spawning new processes, etc. In the semantics messages to node
129+controllers (for instance, requests to spawn new processes) are recorded as
130+messages sent to the node itself.
86We assume disjoint countable sets $\mathtt{NodeId}$, $\mathtt{ProcessId}$, and
132We assume disjoint countable sets $\mathtt{NodeId}$, $\mathtt{ProcessId}$, and
87$\mathtt{ChannelId}$, changed over by \sNid, \sPid{} and \sCid{} respectively,
133$\mathtt{ChannelId}$, changed over by \sNid, \sPid{} and \sCid{} respectively,
88and representing process identifiers, node identifiers, and (typed) channel
134and representing process identifiers, node identifiers, and (typed) channel
@@ -119,14 +165,13 @@ The system queue is a set of triples $(\sId_\mathit{to}, \sId_\mathit{fr},
119blacklist records disconnections and is represented as a of pairs
165blacklist records disconnections and is represented as a of pairs
120$(\sId_\mathit{to}, \sId_\mathit{fr})$.
166$(\sId_\mathit{to}, \sId_\mathit{fr})$.
122−%Note that we do not need to refer to nodes as entities in their own right in
125\section{Semantics}
168\section{Semantics}
127\subsection{Contexts}
170\subsection{Contexts}
129−We define an evaluation context as usual (TODO: catch?)
172+We define an evaluation context as in the \textit{Composable Memory
173+Transactions} paper, but note that we work with \emph{sets} of processes so the
174+definition of $\sCtxt{P}$ can be slightly simpler.
131\begin{align*}
176\begin{align*}
132\sCtxt{E} & ::= [] \OR \sBind{\sCtxt{E}}{M} \\
177\sCtxt{E} & ::= [] \OR \sBind{\sCtxt{E}}{M} \\
@@ -135,7 +180,7 @@ We define an evaluation context as usual (TODO: catch?)
136\subsection{Disconnect}
181\subsection{Disconnect}
138−At the Cloud Haskell level we assume that \emph{nodes} get disconnected, not
183+We assume that entire \emph{nodes} get disconnected from each other, not
139individual processes. \emph{Reconnecting} however is on a per process basis. To
184individual processes. \emph{Reconnecting} however is on a per process basis. To
140formalize this, let $\overline{\sNid}$ be the smallest set, given a set of
185formalize this, let $\overline{\sNid}$ be the smallest set, given a set of
141processes $\sProcesses$, such that
186processes $\sProcesses$, such that
@@ -177,6 +222,28 @@ $\sNid_2$:
177} \textsc{Disconnect}
222} \textsc{Disconnect}
178\end{equation*}
223\end{equation*}
225+Once a connection has been blacklisted, no further messages can be sent across
226+that connection (until an explicit or implicit reconnect). To model this we
230+\begin{array}{l@{\;=\;}l@{\hspace{3em}}l}
231+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
233+ \sQueue, (\sId_\mathit{to}, \sId_\mathit{fr}, M)
235+ \text{if } (\sId_\mathit{to}, \sId_\mathit{fr}) \notin \sBlacklist
237+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
245+$(\sExtend{\sBlacklist})$ is only defined for serializable payloads.
180We provide a primitive to remove a connection from the blacklist:
247We provide a primitive to remove a connection from the blacklist:
182\begin{equation*}
249\begin{equation*}
@@ -194,7 +261,10 @@ We provide a primitive to remove a connection from the blacklist:
194} \textsc{Recon-Ex}
261} \textsc{Recon-Ex}
195\end{equation*}
262\end{equation*}
264+Note that using this primitive means giving up on the reliability guarantee: a
265+call to $\sReconnect$ means that message loss is accepted.
197−Connections to and from nodes can be implicitly reconnected:
267+Connections to and from node controllers can be implicitly reconnected:
199\begin{equation*}
269\begin{equation*}
@@ -212,31 +282,7 @@ Connections to and from nodes can be implicitly reconnected:
212} \textsc{Recon-Im2}
282} \textsc{Recon-Im2}
213\end{equation*}
283\end{equation*}
215−Once a connection has been blacklisted, no further messages can be sent across
216−that connection (until an explicit or implicit reconnect). To model this we
220−\begin{array}{l@{\;=\;}l@{\hspace{3em}}l}
221− \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
223− \sQueue, (\sId_\mathit{to}, \sId_\mathit{fr}, M)
225− \text{if } (\sId_\mathit{to}, \sId_\mathit{fr}) \notin \sBlacklist
227− \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
235−$(\sExtend{\sBlacklist})$ is only defined for serializable payloads.
237−\subsection{Process rules}
239−\subsubsection{Send and Receive}
285+\subsection{Send and Receive}
241\begin{equation*}
287\begin{equation*}
@@ -271,7 +317,7 @@ We return the \emph{first} message of a randomly chosen sender.
271} \textsc{Expect}
317} \textsc{Expect}
272\end{equation*}
318\end{equation*}
274−\subsubsection{Spawning}
320+\subsection{Spawning}
276Spawning is asynchronous
322Spawning is asynchronous
@@ -311,7 +357,7 @@ Spawning is asynchronous
311} \textsc{Spawn-Reply}
357} \textsc{Spawn-Reply}
312\end{equation*}
358\end{equation*}
314−\subsubsection{Typed Channels}
360+\subsection{Typed Channels}
316Since the semantics is not type-driven, we represent typed channels simply as
362Since the semantics is not type-driven, we represent typed channels simply as
317an identifier with an annotation whether it is the send-end ($\sCid^s$) or the
363an identifier with an annotation whether it is the send-end ($\sCid^s$) or the
@@ -366,7 +412,7 @@ receive end ($\sCid^r$) of the channel.
366} \textsc{ReceiveChan}
412} \textsc{ReceiveChan}
367\end{equation*}
413\end{equation*}
369−\subsubsection{Monitoring}
415+\subsection{Monitoring}
371The local node controller is notified immediately of the new monitor, and the
417The local node controller is notified immediately of the new monitor, and the
372remote monitor is sent a message (which may, of course, be lost).
418remote monitor is sent a message (which may, of course, be lost).
@@ -431,7 +477,7 @@ disconncted from a monitored remote process.
431} \textsc{Discon}
477} \textsc{Discon}
432\end{equation*}
478\end{equation*}
434−\subsubsection{Process Termination}
480+\subsection{Process Termination}
436We remove a terminated process only once all its monitors have been notified.
482We remove a terminated process only once all its monitors have been notified.
@@ -472,7 +518,7 @@ monitored remote process terminates.
472} \textsc{Died}
518} \textsc{Died}
473\end{equation*}
519\end{equation*}
475−\subsubsection{Administration}
521+\subsection{Administration}
477TODO: bind, pure evaluation, maybe exception handling
523TODO: bind, pure evaluation, maybe exception handling