@@ -0,0 +1,706 @@
1+\documentclass{article}
2+\usepackage[margin=2.5cm]{geometry}
3+\usepackage{amsmath, amssymb, stmaryrd}
4+\usepackage{mathpazo, times}
8+\newcommand{\sLam}[2]{\lambda {#1} \cdot {#2}}
9+\newcommand{\sApp}[2]{{#1} {#2}}
10+\newcommand{\sBind}[2]{{#1} \mathrel{\texttt{>}\!\!\texttt{>}\!\texttt{=}} {#2}}
11+\newcommand{\sReturn}{\mathtt{return}}
12+\newcommand{\sThrow}[1]{\mathtt{throw} \; {#1}}
13+\newcommand{\sCatch}[2]{\mathtt{catch} \; {#1} \; {#2}}
15+\newcommand{\sExpect}{\mathtt{expect}}
16+\newcommand{\sSend}{\mathtt{send}}
17+\newcommand{\sSpawn}{\mathtt{spawn}}
18+\newcommand{\sLink}{\mathtt{link}}
19+\newcommand{\sReconnect}{\mathtt{reconnect}}
20+\newcommand{\sNewChan}{\mathtt{newChan}}
21+\newcommand{\sSendChan}{\mathtt{sendChan}}
22+\newcommand{\sReceiveChan}{\mathtt{receiveChan}}
23+\newcommand{\sMonitor}{\mathtt{monitor}}
25+\DeclareMathOperator{\sNodeOf}{node}
26+\DeclareMathOperator{\sProcessOf}{process}
28+\newcommand{\sSpawned}{\mathtt{spawned}}
30+\newcommand{\sExtend}[1]{\mathrel{\triangleright_{#1}}}
32+\newcommand{\sPar}{\mathrel{\parallel}}
33+\newcommand{\sProc}[2]{{#1}_{#2}}
35+\newcommand{\sNid}{\ensuremath{\mathit{nid}}}
36+\newcommand{\sPid}{\ensuremath{\mathit{pid}}}
37+\newcommand{\sCid}{\ensuremath{\mathit{cid}}}
39+\newcommand{\sId}{\ensuremath{\mathit{id}}}
40+\newcommand{\sRef}{\ensuremath{\mathit{ref}}}
42+\newcommand{\sLinks}{\ensuremath{\mathit{links}}}
43+\newcommand{\sNode}[3]{\left[{#1} ; {#2}\right]_{#3}}
44+\newcommand{\sSystem}[4]{\left\langle #1 ; #2 ; #3 ; #4 \right\rangle}
45+\newcommand{\sNodes}{\mathcal{N}}
46+\newcommand{\sQueue}{\mathcal{Q}}
47+\newcommand{\sProcesses}{\mathcal{P}}
48+\newcommand{\sBlacklist}{\mathcal{B}}
49+\newcommand{\sMonitors}{\mathcal{M}}
51+\newcommand{\sJust}[1]{\mathtt{Just} \; {#1}}
52+\newcommand{\sNothing}{\mathtt{Nothing}}
54+\newcommand{\sCtxt}[1]{\mathbb{#1}}
56+\newcommand{\sSenders}{\mathit{senders}}
58+\newcommand{\OR}{\mathrel{|}}
59+\newcommand{\where}{\mathrel{|}}
64+\lstset{basicstyle=\ttfamily\small}
68+\title{Cloud Haskell Semantics (DRAFT)}
69+\author{Well-Typed LLP}
74+\section{Introduction}
76+Cloud Haskell brings Erlang-style concurrency to Haskell in the form of a
77+library.\footnote{\texttt{http://hackage.haskell.org/package/distributed-process}}
78+The original publication \cite{cloudhaskell} is a good introduction to Cloud
79+Haskell, and is accompanied by an ever-growing number of resouces, collected on
81+Wiki.\footnote{\texttt{http://www.haskell.org/haskellwiki/Cloud\_Haskell}} The
82+current document augments the original publication about Cloud Haskell by
83+giving a precise semantics to the Cloud Haskell primitives. It is meant as a
84+reference, not an introduction.
86+The original Cloud Haskell paper stipulates that messages are ``asynchronous,
87+reliable, and buffered'', but does not describe how this can be achieved.
88+Understanding ``reliable'' to mean ``reliable ordered'' (or ``TCP-like''),
89+the reliability of message delivery comes from the reliability of the
90+underlying network protocol---up to a point.
92+The problem is that the underlying network protocol is connection-oriented, but
93+Cloud Haskell is not. Intuitively, when $P$ sends a message to $Q$, we open a
94+reliable-ordered connection from $P$ to $Q$. Reliability of message delivery
95+now follows from reliability of the network protocol, until $P$ somehow gets
96+disconnected from $Q$. If $P$ now sends another message to $Q$, the
97+implementation cannot simply reconnect: after all, some messages that were sent
98+on the first connection might not have been delivered. This means that $P$
99+might send $m_1, m_2, m_3$ to $Q$, but $Q$ will receive $m_1,
100+m_3$.\footnote{Indeed, message passing in Erlang is ordered but unreliable for
101+the same reason \cite{erlang}.}
103+One (non-)solution is for $P$ to buffer all messages it sends to $Q$, and
104+remove messages from this buffer only when $Q$ acknowledges that it received
105+them. On a reconnect $P$ must ask which message $Q$ last received, and
106+retransmit the rest. This means that when $P$ gets disconnected from $Q$, it
107+must infinitely buffer all messages sent to $Q$ (until a connection is
108+reestablished). However, infinite buffering is too strong a requirement;
109+moreover, this is unsatisfactory because it means implementing a reliable
110+protocol on top of the underlying reliable network protocol. We would like a
113+Instead, Cloud Haskell does \emph{not} attempt to reconnect automatically, but
114+provides a $\sReconnect$ primitive which gives programmers the option of
115+reconnecting manually. This is an explicit acknowledgement from the programmer
116+that message loss might occur, and forces them to consider how such loss might
119+The semantics we present is based on \cite{unified}, which we will refer to the
120+as the ``Unified'' semantics. However, we will present the semantics in a more
121+``Haskell'' style following the semantics for STM \cite{stm}. It differs from
122+the Unified semantics in that
125+\item We introduce an explicit notion of \textit{reconnecting} (with potential
127+\item We simplify the semantics: we ``flatten'' sets of nodes of processes as
128+sets of processes (but assume a mapping from process identifiers to node
129+identifiers), do not have per-process mailboxes (but only the system queue or
130+``ether'') and do not have an explicit concept of node controllers
133+Our semantics differs from the STM semantics in that we pretend that the Cloud
134+Haskell \texttt{Process} monad is the top-level monad, and do not consider the
135+\texttt{IO} monad at all. Current imprecisions with respect to the ``real''
139+\item We ignore the issue of serializability, other than to say that the
140+semantics will get stuck when trying to send a non-serializable payload;
141+consequently, we do not formalize $\mathtt{static}$
142+\item We do not formalize all Cloud Haskell primitives (merging of ports,
143+``advanced messaging'', and others)
144+\item Some of the concepts that we do formalize are lower-level concepts; for
145+instance, the primitive $\sSpawn$ that we formalize is asynchronous (following
146+the Unified semantics); a synchronous construct can be derived.
149+\section{Preliminaries}
151+Cloud Haskell Processes run on \emph{nodes}. Processes communicate by sending
152+messages to each other (directly or using typed channels). Processes can also
153+send messages to nodes (for instance, a request to spawn or monitor a process).
155+We assume disjoint countable sets $\mathtt{NodeId}$, $\mathtt{ProcessId}$, and
156+$\mathtt{ChannelId}$, changed over by \sNid, \sPid{} and \sCid{} respectively,
157+and representing process identifiers, node identifiers, and (typed) channel
158+identifiers. We assume the existence of total functions
161+\begin{array}{r@{\;:\;}l}
162+\sNodeOf & (\mathtt{ProcessId} \uplus \mathtt{ChannelId}) \rightarrow \mathtt{NodeId} \\
163+\sProcessOf & \mathtt{ChannelId} \rightarrow \mathtt{ProcessId}
168+$$\mathtt{Identifier} = \mathtt{NodeId} \uplus \mathtt{ProcessId} \uplus \mathtt{ChannelId}$$
169+and let $\sId$ range over $\mathtt{Identifier}$.
171+We represent a process as a pair $\sProc{M}{\sPid}$ of a term $M$ and a process
172+ID $\sPid$. We will denote a set of processes as
174+ $$\sProc{M}{\sPid} \sPar \cdots \sPar \sProc{N}{\sPid'}$$
177+ $\sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}$
178+is a tuple containing a set $\sProcesses$ of processes, a \emph{system
179+queue} $\sQueue$, a \emph{blacklist} $\sBlacklist$, and a set of monitors
181+The set of monitors $\sMonitors$ is a set of tuples
182+ $(\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid, \sRef)$
183+which records that node \sNid{} knows that process $\sPid_\mathit{fr}$ is
184+monitoring $\sId_\mathit{to}$ ($\sRef$ is the monitor reference). The system
185+queue is a set of triples $(\sId_\mathit{to}, \sId_\mathit{fr},
186+\mathit{message})$ of messages that have been sent but not yet processed. The
187+blacklist records disconnections and is represented as a of pairs
188+$(\sId_\mathit{to}, \sId_\mathit{fr})$.
192+We follow the STM semantics as closely as possible. The language is the same
193+except for the primitives considered, and we use the same concept of evaluation
198+\text{value} & V & ::= & \sId \OR
202+ \sThrow{M} \OR \sCatch{M}{N} \OR \\
204+ \sSend \; \sPid \; M \OR
205+ \sSpawn \; \sNid \; M \OR
208+\text{term} & M, N & ::= & x \OR
213+\text{Evaluation} & \sCtxt{E} & ::= & [] \OR \sBind{\sCtxt{E}}{M} \OR \sCatch{\sCtxt{E}}{M} \\
214+\text{context} & \sCtxt{P}_\sPid & ::= & \sCtxt{E}[]_\sPid \sPar \sProcesses
218+Indeed, the ``administrative'' transitions are identical
219+(Figure~\ref{fig:administrative}).
225+ \llbracket M \rrbracket = V \qquad
234+ \sSystem{\sCtxt{P}[M]_\sPid}
239+ \sSystem{\sCtxt{P}[N]_\sPid}
247+\begin{array}{r@{\;\rightarrow\;}ll@{\hspace{2em}}r@{\;\rightarrow\;}ll}
248+\sBind{\sReturn \; N}{M} & M \; N & \textsc{Bind} & \sCatch{(\sReturn \; M)}{N} & \sReturn \; M & \textsc{Catch}_1 \\
249+\sBind{\sThrow{N}}{M} & \sThrow{N} & \textsc{Throw} & \sCatch{(\sThrow M)}{N} & N \; M & \textsc{Catch}_2 \\
253+\caption{\label{fig:administrative}Administrative Transitions}
256+\subsection{Disconnect and Reconnect}
258+Figure~\ref{fig:disconnect} gives the semantics for disconnecting and
259+reconnecting. Rule \textsc{Disconnect} models random network disconnect
260+between nodes $\sNid_1$ and $\sNid_2$. We assume that entire \emph{nodes} get
261+disconnected from each other, not individual processes. \emph{Reconnecting}
262+however is on a per connection basis (\textsc{Recon-Ex}). Connections to and
263+from node controllers can be implicitly reconnected ($\textsc{Recon-Im}_1$ and
264+$\textsc{Recon-Im}_2$).
270+ \sNid_1 \neq \sNid_2
272+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
274+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist \cup (\overline{\sNid_1} \times \overline{\sNid_2})}{\sMonitors}
275+} \textsc{Disconnect}
281+ \sSystem{\sCtxt{P}[ \sReconnect \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}
286+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_\sPid}
288+ {\sBlacklist \backslash (\sId_\mathit{to}, \sPid_\mathit{fr})}
296+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sNid_\mathit{to}, \sId_\mathit{fr})}{\sMonitors}
298+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
299+} \textsc{Recon-Im}_1
303+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sId_\mathit{to}, \sNid_\mathit{fr})}{\sMonitors}
305+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
306+} \textsc{Recon-Im}_2
312+\overline{\sNid} \subset \mathtt{Identifier}
314+ \{ \sPid \where \sNodeOf(\sPid) = \sNid \} \cup
315+ \{ \sCid \where \sNodeOf(\sCid) = \sNid \}
317+\caption{\label{fig:disconnect}Disconnect and Reconnect}
320+\subsection{Communication}
322+The semantics for the basic primitives are listed in Figure~\ref{fig:basic}.
323+Once a connection has been blacklisted, no further messages can be sent across
324+that connection (until an explicit or implicit reconnect).
326+Message passing is ordered but only for a given sender and receiver; no
327+ordering guarantees exist between messages sent by different processes. For
328+that reason rules \textsc{Expect}, \textsc{ReceiveChan} and \textsc{Spawn-Exec}
329+choose the \emph{first} message of a \emph{randomly chosen} sender.
331+Since the semantics is not type-driven, we represent typed channels simply as
332+an identifier with an annotation whether it is the send-end ($\sCid^s$) or the
333+receive end ($\sCid^r$) of the channel (rules \textsc{NewChan},
334+\textsc{SendChan} and \textsc{ReceiveChan}).
336+Spawning finally is asynchronous. When process $P$ spawns process $Q$ on node
337+$\sNid$ (rule \textsc{Spawn-Async}) a message is sent to node $\sNid$ (which
338+may, of course, never arrive). When the remote node receives the message and
339+actually spawns $Q$ (rule \textsc{Spawn-Exec}) it sends a message back to $P$
340+with $Q$'s process ID. In Cloud Haskell this primitive is called
341+\texttt{spawnAsync}, and the Cloud Haskell \texttt{spawn} primitive is defined
342+in terms of \texttt{spawnAsync} (we do not consider the synchronous version in
350+ \sSystem{\sCtxt{P}[ \sSend \; \sPid_\mathit{to} \; M ]_{\sPid_\mathit{fr}}}
355+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_{\sPid_\mathit{fr}}}
356+ {\sQueue \sExtend{\sBlacklist} (\sPid_\mathit{to}, \sPid_\mathit{fr}, M)}
364+ \sId_{\mathit{fr}} \notin \sSenders(\sQueue)
366+ \sSystem{\sCtxt{P}[ \sExpect ]_{\sPid_\mathit{to}}}
367+ {\sQueue, (\sPid_\mathit{to}, \sId_\mathit{fr}, M), \sQueue'}
371+ \sSystem{\sCtxt{P}[ \sReturn \; M ]_{\sPid_\mathit{to}}}
382+ \sProcessOf(\sCid) = \sPid
384+ \sSystem{\sCtxt{P}[\sNewChan]_\sPid}
389+ \sSystem{\sCtxt{P}[\sReturn \; (\sCid^s, \sCid^r)]_\sPid}
399+ \sSystem{\sCtxt{P}[ \sSendChan \; \sCid_\mathit{to}^s \; M ]_{\sPid_\mathit{fr}}}
404+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_{\sPid_\mathit{fr}}}
405+ {\sQueue \sExtend{\sBlacklist} (\sCid_\mathit{to}, \sPid_\mathit{fr}, M)}
413+ \sPid_{\mathit{fr}} \notin \sSenders(\sQueue)
415+ \sSystem{\sCtxt{P}[ \sReceiveChan \; \sCid_\mathit{to}^r ]_{\sPid}}
416+ {\sQueue, (\sCid_\mathit{to}, \sPid_\mathit{fr}, M), \sQueue'}
420+ \sSystem{\sCtxt{P}[ \sReturn \; M ]_{\sPid}}
424+} \textsc{ReceiveChan}
431+ \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid}
436+ \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_\sPid}
437+ {\sQueue \sExtend{\sBlacklist} (\sNid, \sPid, \sSpawn \; \sRef \; M)}
440+} \textsc{Spawn-Async}
445+ \sPid \notin \sSenders(\sQueue)
447+ \sPid' \text{ fresh}
449+ \sNodeOf(\sPid') = \sNid
451+ \sSystem{\sProcesses}
452+ {\sQueue, (\sNid, \sPid, \sSpawn \; \sRef \; M), \sQueue'}
456+ \sSystem{\sProcesses \sPar M_{\sPid'}}
457+ {\sQueue, \sQueue' \sExtend{\sBlacklist} (\sPid, \sNid, \sSpawned \; \sRef \; \sPid')}
460+} \textsc{Spawn-Exec}
466+\begin{array}{l@{\;=\;}l@{\hspace{3em}}l}
467+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
469+ \sQueue, (\sId_\mathit{to}, \sId_\mathit{fr}, M)
471+ \text{if } (\sId_\mathit{to}, \sId_\mathit{fr}) \notin \sBlacklist
473+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
481+$(\sExtend{\sBlacklist})$ is only defined for serializable payloads.
482+\caption{\label{fig:basic}Basic Primitives}
485+\subsection{Monitoring}
487+When process $P$ on node $\sNid_P$ wants to monitor process $Q$ on node
488+$\sNid_Q$ \emph{both} nodes must be notified. The local node it notified
489+immediately, and a message is sent to to the remote node (rules
490+\textsc{Mon-Loc} and \textsc{Mon-Rem}). As with all messages, the
491+message to the remote node might be lost. When $P$ is disconnected from $Q$ it
492+is the responsibility of $P$'s local node $\sNid_P$ to notify $P$
493+(\textsc{Mon-Dis}); when $Q$ terminates (\textsc{Mon-Ret}) or crashes
494+(\textsc{Mon-Throw}) it is the responsibility of the remote node $\sNid_Q$ to
501+ \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})
503+ \sNid_\mathit{to} = \sNodeOf(\sId_\mathit{to})
507+\sSystem{\sCtxt{P}[ \sMonitor \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}
512+ \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_{\sPid_\mathit{fr}}}
513+ {\sQueue \sExtend{\sBlacklist} (\sNid_\mathit{to}, \sPid_\mathit{fr}, \sMonitor \; \sRef \; \sId_\mathit{to})}
515+ {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{fr}, \sRef)}
521+ \sPid_\mathit{fr} \notin \sSenders(\sQueue)
523+ \sSystem{\sProcesses}
524+ {\sQueue, (\sNid_\mathit{to}, \sPid_\mathit{fr}, \sMonitor \; \sRef \; \sId_\mathit{to}), \sQueue'}
528+ \sSystem{\sProcesses}
531+ {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{to}, \sRef)}
537+ \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})
539+ (\sId_\mathit{to}, \sPid_\mathit{fr}) \in \sBlacklist
541+ \sSystem{\sProcesses}
544+ {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{fr}, \sRef)}
546+ \sSystem{\sProcesses}
547+ {\sQueue, (\sPid_\mathit{fr}, \sId_\mathit{to}, \mathtt{discon} \; \sRef)}
555+ \sNodeOf(\sPid) = \sNid
557+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
560+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
562+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
563+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{died} \; \sRef)}
571+ \sNodeOf(\sPid) = \sNid
573+ \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}
576+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
578+ \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}
579+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{exc} \; \sRef \; M)}
587+ \sNodeOf(\sPid) = \sNid
589+ \sPid \notin \sProcesses
591+ \sSystem{\sProcesses}
594+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
596+ \sSystem{\sProcesses}
597+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{unknown} \; \sRef)}
600+} \textsc{Mon-Unknown}
606+\subsection{Process Termination}
608+The rules for normal and abnormal process termination are defined in
609+Figure~\ref{fig:termination}. When a process crashes it dies
610+silently, unless monitors are setup.
617+ \sNodeOf(\sPid) = \sNid
619+ \nexists \; \sPid', \sRef \cdot (\sPid', \sPid, \sNid, \sRef) \in \sMonitors
621+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
626+ \sSystem{\sProcesses}
635+ \sNodeOf(\sPid) = \sNid
637+ \nexists \; \sPid', \sRef \cdot (\sPid', \sPid, \sNid, \sRef) \in \sMonitors
639+ \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}
644+ \sSystem{\sProcesses}
651+\caption{\label{fig:termination}Process Termination}
654+\section{Open Issues}
656+\subsection{Ordering of Monitor/Link Notifications}
658+The semantics as described above, like the original Unified semantics, does not
659+guarantee that messages send from process $P$ to process $Q$ (\textsc{Send})
660+are ordered with respect to the link or monitor notification sent when process
661+$P$ terminates normally or abnormally (\textsc{Mon-Ret}, \textsc{Mon-Throw}). This means that if process $P$ does
665+ match $ \(Reply reply) -> ...
666+ , match $ \(ProcessMonitorNotification ..) -> ...
673+send pidA (Reply reply)
674+// terminate or indeed throw an exception
677+then the semantics does not guarantee that the reply from process $Q$ will
678+arrive at process $P$ before the monitor notification; hence, this results in
679+an (artificial) race condition in process $P$.
681+One possible solution is to regard such a link notification as a message from
682+process $Q$ to process $P$, which should be ordered along with the other
685+\subsection{Ordering and Typed Channels}
687+The situation is more tricky still than sketched above because we of typed
688+channels. The semantics does not provide ordering guarantees between messages
689+sent directly to the process and messages sent on typed channels. That means
690+that even if we consider a link or monitor notification as a message sent to
691+the process, to be ordered with other messages sent to that process, it is
692+still unordered with respect to messages sent on typed channels. This means
693+that we have similar race conditions\footnote{Even ignoring the fact that we
694+currently don't even provide a way to wait for a message on a typed channel
695+\emph{or} a direct message.}
697+A possible solution is to insist that \emph{all} messages from process $P$ to
698+process $Q$ are ordered, no matter how they are sent. From a implementation
699+point of view, this would entail the use of a single ordered network connection
700+for all messages from $P$ to $Q$, rather than using an ordered connection per
701+typed channel plus one for direct messages.
703+\bibliographystyle{apalike}
704+\bibliography{references}