@@ -57,16 +57,56 @@
5757
5858\begin{document}
5959
60−\title{Cloud Haskell Semantics}
60+\title{Cloud Haskell Semantics (DRAFT)}
6161\author{Edsko de Vries, Well-Typed LLP}
6262\date{\today}
6363
6464\maketitle
6565
66−\section{Syntax}
66+\section{Introduction}
67+
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
73+%
74+\begin{enumerate}
75+\item We introduce an explicit notion of \textit{reconnecting} (with potential
76+message loss)
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
81+\end{enumerate}
82+%
83+It differs from the latter in that
84+%
85+\begin{enumerate}
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
89+\end{enumerate}
90+%
91+Current imprecisions with respect to the ``real'' Cloud Haskell are
92+%
93+\begin{enumerate}
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.
102+\end{enumerate}
103+
104+\section{Preliminaries}
67105
68106\subsection{Terms}
69107
108+We assume the usual definitions of values and terms.
109+
70110\begin{equation*}
71111\begin{array}{ll@{\;::=\;}l}
72112\text{value} & V & \sLam{x}{M} \OR
@@ -83,6 +123,12 @@
83123
84124\subsection{Processes, Nodes, Systems}
85125
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.
131+
86132We assume disjoint countable sets $\mathtt{NodeId}$, $\mathtt{ProcessId}$, and
87133$\mathtt{ChannelId}$, changed over by \sNid, \sPid{} and \sCid{} respectively,
88134and 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},
119165blacklist records disconnections and is represented as a of pairs
120166$(\sId_\mathit{to}, \sId_\mathit{fr})$.
121167
122−%Note that we do not need to refer to nodes as entities in their own right in
123−%the semantics.
124−
125168\section{Semantics}
126169
127170\subsection{Contexts}
128171
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.
130175
131176\begin{align*}
132177\sCtxt{E} & ::= [] \OR \sBind{\sCtxt{E}}{M} \\
@@ -135,7 +180,7 @@ We define an evaluation context as usual (TODO: catch?)
135180
136181\subsection{Disconnect}
137182
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
139184individual processes. \emph{Reconnecting} however is on a per process basis. To
140185formalize this, let $\overline{\sNid}$ be the smallest set, given a set of
141186processes $\sProcesses$, such that
@@ -177,6 +222,28 @@ $\sNid_2$:
177222} \textsc{Disconnect}
178223\end{equation*}
179224
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
227+introduce a function
228+%
229+\begin{equation*}
230+\begin{array}{l@{\;=\;}l@{\hspace{3em}}l}
231+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
232+&
233+ \sQueue, (\sId_\mathit{to}, \sId_\mathit{fr}, M)
234+&
235+ \text{if } (\sId_\mathit{to}, \sId_\mathit{fr}) \notin \sBlacklist
236+\\
237+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
238+&
239+ \sQueue
240+&
241+ \text{otherwise}
242+\end{array}
243+\end{equation*}
244+%
245+$(\sExtend{\sBlacklist})$ is only defined for serializable payloads.
246+
180247We provide a primitive to remove a connection from the blacklist:
181248
182249\begin{equation*}
@@ -194,7 +261,10 @@ We provide a primitive to remove a connection from the blacklist:
194261} \textsc{Recon-Ex}
195262\end{equation*}
196263
197−Connections to and from nodes can be implicitly reconnected:
264+Note that using this primitive means giving up on the reliability guarantee: a
265+call to $\sReconnect$ means that message loss is accepted.
266+
267+Connections to and from node controllers can be implicitly reconnected:
198268
199269\begin{equation*}
200270\frac{
@@ -212,31 +282,7 @@ Connections to and from nodes can be implicitly reconnected:
212282} \textsc{Recon-Im2}
213283\end{equation*}
214284
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
217−introduce a function
218−%
219−\begin{equation*}
220−\begin{array}{l@{\;=\;}l@{\hspace{3em}}l}
221− \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
222−&
223− \sQueue, (\sId_\mathit{to}, \sId_\mathit{fr}, M)
224−&
225− \text{if } (\sId_\mathit{to}, \sId_\mathit{fr}) \notin \sBlacklist
226−\\
227− \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
228−&
229− \sQueue
230−&
231− \text{otherwise}
232−\end{array}
233−\end{equation*}
234−%
235−$(\sExtend{\sBlacklist})$ is only defined for serializable payloads.
236−
237−\subsection{Process rules}
238−
239−\subsubsection{Send and Receive}
285+\subsection{Send and Receive}
240286
241287\begin{equation*}
242288\frac{
@@ -271,7 +317,7 @@ We return the \emph{first} message of a randomly chosen sender.
271317} \textsc{Expect}
272318\end{equation*}
273319
274−\subsubsection{Spawning}
320+\subsection{Spawning}
275321
276322Spawning is asynchronous
277323
@@ -311,7 +357,7 @@ Spawning is asynchronous
311357} \textsc{Spawn-Reply}
312358\end{equation*}
313359
314−\subsubsection{Typed Channels}
360+\subsection{Typed Channels}
315361
316362Since the semantics is not type-driven, we represent typed channels simply as
317363an 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.
366412} \textsc{ReceiveChan}
367413\end{equation*}
368414
369−\subsubsection{Monitoring}
415+\subsection{Monitoring}
370416
371417The local node controller is notified immediately of the new monitor, and the
372418remote monitor is sent a message (which may, of course, be lost).
@@ -431,7 +477,7 @@ disconncted from a monitored remote process.
431477} \textsc{Discon}
432478\end{equation*}
433479
434−\subsubsection{Process Termination}
480+\subsection{Process Termination}
435481
436482We remove a terminated process only once all its monitors have been notified.
437483
@@ -472,7 +518,7 @@ monitored remote process terminates.
472518} \textsc{Died}
473519\end{equation*}
474520
475−\subsubsection{Administration}
521+\subsection{Administration}
476522
477523TODO: bind, pure evaluation, maybe exception handling
478524