@@ -0,0 +1,706 @@
1+\documentclass{article}
2+\usepackage[margin=2.5cm]{geometry}
3+\usepackage{amsmath, amssymb, stmaryrd}
4+\usepackage{mathpazo, times}
5+\usepackage{float}
6+\usepackage{listings}
7+
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}}
14+
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}}
24+
25+\DeclareMathOperator{\sNodeOf}{node}
26+\DeclareMathOperator{\sProcessOf}{process}
27+
28+\newcommand{\sSpawned}{\mathtt{spawned}}
29+
30+\newcommand{\sExtend}[1]{\mathrel{\triangleright_{#1}}}
31+
32+\newcommand{\sPar}{\mathrel{\parallel}}
33+\newcommand{\sProc}[2]{{#1}_{#2}}
34+
35+\newcommand{\sNid}{\ensuremath{\mathit{nid}}}
36+\newcommand{\sPid}{\ensuremath{\mathit{pid}}}
37+\newcommand{\sCid}{\ensuremath{\mathit{cid}}}
38+
39+\newcommand{\sId}{\ensuremath{\mathit{id}}}
40+\newcommand{\sRef}{\ensuremath{\mathit{ref}}}
41+
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}}
50+
51+\newcommand{\sJust}[1]{\mathtt{Just} \; {#1}}
52+\newcommand{\sNothing}{\mathtt{Nothing}}
53+
54+\newcommand{\sCtxt}[1]{\mathbb{#1}}
55+
56+\newcommand{\sSenders}{\mathit{senders}}
57+
58+\newcommand{\OR}{\mathrel{|}}
59+\newcommand{\where}{\mathrel{|}}
60+
61+\floatstyle{boxed}
62+\restylefloat{figure}
63+
64+\lstset{basicstyle=\ttfamily\small}
65+
66+\begin{document}
67+
68+\title{Cloud Haskell Semantics (DRAFT)}
69+\author{Well-Typed LLP}
70+\date{\today}
71+
72+\maketitle
73+
74+\section{Introduction}
75+
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
80+the Haskell
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.
85+
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.
91+
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}.}
102+
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
111+different solution.
112+
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
117+be dealt with.
118+
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
123+%
124+\begin{enumerate}
125+\item We introduce an explicit notion of \textit{reconnecting} (with potential
126+message loss)
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
131+\end{enumerate}
132+%
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''
136+Cloud Haskell are
137+%
138+\begin{enumerate}
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.
147+\end{enumerate}
148+
149+\section{Preliminaries}
150+
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).
154+
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
159+%
160+\begin{equation*}
161+\begin{array}{r@{\;:\;}l}
162+\sNodeOf & (\mathtt{ProcessId} \uplus \mathtt{ChannelId}) \rightarrow \mathtt{NodeId} \\
163+\sProcessOf & \mathtt{ChannelId} \rightarrow \mathtt{ProcessId}
164+\end{array}
165+\end{equation*}
166+%
167+and define
168+$$\mathtt{Identifier} = \mathtt{NodeId} \uplus \mathtt{ProcessId} \uplus \mathtt{ChannelId}$$
169+and let $\sId$ range over $\mathtt{Identifier}$.
170+
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
173+%
174+ $$\sProc{M}{\sPid} \sPar \cdots \sPar \sProc{N}{\sPid'}$$
175+%
176+A \emph{system}
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
180+$\sMonitors$.
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})$.
189+
190+\section{Semantics}
191+
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
194+contexts:
195+
196+\begin{equation*}
197+\begin{array}{llll}
198+\text{value} & V & ::= & \sId \OR
199+ \sLam{x}{M} \OR
200+ \sReturn \; M \OR
201+ \sBind{M}{N} \OR
202+ \sThrow{M} \OR \sCatch{M}{N} \OR \\
203+ &&& \sExpect \OR
204+ \sSend \; \sPid \; M \OR
205+ \sSpawn \; \sNid \; M \OR
206+ \sMonitor \; \sId
207+\\
208+\text{term} & M, N & ::= & x \OR
209+ V \OR
210+ \sApp{M}{N} \OR
211+ \cdots \\
212+\\
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
215+\end{array}
216+\end{equation*}
217+%
218+Indeed, the ``administrative'' transitions are identical
219+(Figure~\ref{fig:administrative}).
220+
221+\begin{figure}
222+\small
223+\begin{equation*}
224+\frac{
225+ \llbracket M \rrbracket = V \qquad
226+ M \neq V
227+}{
228+ M \rightarrow V
229+} \textsc{Eval}
230+\qquad
231+\frac{
232+ M \rightarrow N
233+}{
234+ \sSystem{\sCtxt{P}[M]_\sPid}
235+ {\sQueue}
236+ {\sBlacklist}
237+ {\sMonitors}
238+\rightarrow
239+ \sSystem{\sCtxt{P}[N]_\sPid}
240+ {\sQueue}
241+ {\sBlacklist}
242+ {\sMonitors}
243+} \textsc{Admin}
244+\end{equation*}
245+%
246+\begin{equation*}
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 \\
250+\end{array}
251+\end{equation*}
252+%
253+\caption{\label{fig:administrative}Administrative Transitions}
254+\end{figure}
255+
256+\subsection{Disconnect and Reconnect}
257+
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$).
265+
266+\begin{figure}
267+\small
268+\begin{equation*}
269+\frac{
270+ \sNid_1 \neq \sNid_2
271+}{
272+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
273+\rightarrow
274+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist \cup (\overline{\sNid_1} \times \overline{\sNid_2})}{\sMonitors}
275+} \textsc{Disconnect}
276+\end{equation*}
277+%
278+\begin{equation*}
279+\frac{
280+}{
281+ \sSystem{\sCtxt{P}[ \sReconnect \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}
282+ {\sQueue}
283+ {\sBlacklist}
284+ {\sMonitors}
285+\rightarrow
286+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_\sPid}
287+ {\sQueue}
288+ {\sBlacklist \backslash (\sId_\mathit{to}, \sPid_\mathit{fr})}
289+ {\sMonitors}
290+} \textsc{Recon-Ex}
291+\end{equation*}
292+%
293+\begin{equation*}
294+\frac{
295+}{
296+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sNid_\mathit{to}, \sId_\mathit{fr})}{\sMonitors}
297+\rightarrow
298+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
299+} \textsc{Recon-Im}_1
300+\qquad
301+\frac{
302+}{
303+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sId_\mathit{to}, \sNid_\mathit{fr})}{\sMonitors}
304+\rightarrow
305+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
306+} \textsc{Recon-Im}_2
307+\end{equation*}
308+%
309+where
310+%
311+\begin{equation*}
312+\overline{\sNid} \subset \mathtt{Identifier}
313+ = \{ \sNid \} \cup
314+ \{ \sPid \where \sNodeOf(\sPid) = \sNid \} \cup
315+ \{ \sCid \where \sNodeOf(\sCid) = \sNid \}
316+\end{equation*}
317+\caption{\label{fig:disconnect}Disconnect and Reconnect}
318+\end{figure}
319+
320+\subsection{Communication}
321+
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).
325+
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.
330+
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}).
335+
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
343+this document).
344+
345+\begin{figure}
346+\small
347+\begin{equation*}
348+\frac{
349+}{
350+ \sSystem{\sCtxt{P}[ \sSend \; \sPid_\mathit{to} \; M ]_{\sPid_\mathit{fr}}}
351+ {\sQueue}
352+ {\sBlacklist}
353+ {\sMonitors}
354+\rightarrow
355+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_{\sPid_\mathit{fr}}}
356+ {\sQueue \sExtend{\sBlacklist} (\sPid_\mathit{to}, \sPid_\mathit{fr}, M)}
357+ {\sBlacklist}
358+ {\sMonitors}
359+} \textsc{Send}
360+\end{equation*}
361+%
362+\begin{equation*}
363+\frac{
364+ \sId_{\mathit{fr}} \notin \sSenders(\sQueue)
365+}{
366+ \sSystem{\sCtxt{P}[ \sExpect ]_{\sPid_\mathit{to}}}
367+ {\sQueue, (\sPid_\mathit{to}, \sId_\mathit{fr}, M), \sQueue'}
368+ {\sBlacklist}
369+ {\sMonitors}
370+\rightarrow
371+ \sSystem{\sCtxt{P}[ \sReturn \; M ]_{\sPid_\mathit{to}}}
372+ {\sQueue, \sQueue'}
373+ {\sBlacklist}
374+ {\sMonitors}
375+} \textsc{Expect}
376+\end{equation*}
377+%
378+\begin{equation*}
379+\frac{
380+ \sCid \text{ fresh}
381+\qquad
382+ \sProcessOf(\sCid) = \sPid
383+}{
384+ \sSystem{\sCtxt{P}[\sNewChan]_\sPid}
385+ {\sQueue}
386+ {\sBlacklist}
387+ {\sMonitors}
388+\rightarrow
389+ \sSystem{\sCtxt{P}[\sReturn \; (\sCid^s, \sCid^r)]_\sPid}
390+ {\sQueue}
391+ {\sBlacklist}
392+ {\sMonitors}
393+} \textsc{NewChan}
394+\end{equation*}
395+
396+\begin{equation*}
397+\frac{
398+}{
399+ \sSystem{\sCtxt{P}[ \sSendChan \; \sCid_\mathit{to}^s \; M ]_{\sPid_\mathit{fr}}}
400+ {\sQueue}
401+ {\sBlacklist}
402+ {\sMonitors}
403+\rightarrow
404+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_{\sPid_\mathit{fr}}}
405+ {\sQueue \sExtend{\sBlacklist} (\sCid_\mathit{to}, \sPid_\mathit{fr}, M)}
406+ {\sBlacklist}
407+ {\sMonitors}
408+} \textsc{SendChan}
409+\end{equation*}
410+
411+\begin{equation*}
412+\frac{
413+ \sPid_{\mathit{fr}} \notin \sSenders(\sQueue)
414+}{
415+ \sSystem{\sCtxt{P}[ \sReceiveChan \; \sCid_\mathit{to}^r ]_{\sPid}}
416+ {\sQueue, (\sCid_\mathit{to}, \sPid_\mathit{fr}, M), \sQueue'}
417+ {\sBlacklist}
418+ {\sMonitors}
419+\rightarrow
420+ \sSystem{\sCtxt{P}[ \sReturn \; M ]_{\sPid}}
421+ {\sQueue, \sQueue'}
422+ {\sBlacklist}
423+ {\sMonitors}
424+} \textsc{ReceiveChan}
425+\end{equation*}
426+%
427+\begin{equation*}
428+\frac{
429+ \sRef \text{ fresh}
430+}{
431+ \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid}
432+ {\sQueue}
433+ {\sBlacklist}
434+ {\sMonitors}
435+\rightarrow
436+ \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_\sPid}
437+ {\sQueue \sExtend{\sBlacklist} (\sNid, \sPid, \sSpawn \; \sRef \; M)}
438+ {\sBlacklist}
439+ {\sMonitors}
440+} \textsc{Spawn-Async}
441+\end{equation*}
442+%
443+\begin{equation*}
444+\frac{
445+ \sPid \notin \sSenders(\sQueue)
446+\qquad
447+ \sPid' \text{ fresh}
448+\qquad
449+ \sNodeOf(\sPid') = \sNid
450+}{
451+ \sSystem{\sProcesses}
452+ {\sQueue, (\sNid, \sPid, \sSpawn \; \sRef \; M), \sQueue'}
453+ {\sBlacklist}
454+ {\sMonitors}
455+\rightarrow
456+ \sSystem{\sProcesses \sPar M_{\sPid'}}
457+ {\sQueue, \sQueue' \sExtend{\sBlacklist} (\sPid, \sNid, \sSpawned \; \sRef \; \sPid')}
458+ {\sBlacklist}
459+ {\sMonitors}
460+} \textsc{Spawn-Exec}
461+\end{equation*}
462+%
463+where
464+%
465+\begin{equation*}
466+\begin{array}{l@{\;=\;}l@{\hspace{3em}}l}
467+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
468+&
469+ \sQueue, (\sId_\mathit{to}, \sId_\mathit{fr}, M)
470+&
471+ \text{if } (\sId_\mathit{to}, \sId_\mathit{fr}) \notin \sBlacklist
472+\\
473+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
474+&
475+ \sQueue
476+&
477+ \text{otherwise}
478+\end{array}
479+\end{equation*}
480+%
481+$(\sExtend{\sBlacklist})$ is only defined for serializable payloads.
482+\caption{\label{fig:basic}Basic Primitives}
483+\end{figure}
484+
485+\subsection{Monitoring}
486+
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
495+notify $P$.
496+
497+\begin{figure}
498+\small
499+\begin{equation*}
500+\frac{
501+ \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})
502+\qquad
503+ \sNid_\mathit{to} = \sNodeOf(\sId_\mathit{to})
504+\qquad
505+ \sRef \text{ fresh}
506+}{
507+\sSystem{\sCtxt{P}[ \sMonitor \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}
508+ {\sQueue}
509+ {\sBlacklist}
510+ {\sMonitors}
511+\rightarrow
512+ \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_{\sPid_\mathit{fr}}}
513+ {\sQueue \sExtend{\sBlacklist} (\sNid_\mathit{to}, \sPid_\mathit{fr}, \sMonitor \; \sRef \; \sId_\mathit{to})}
514+ {\sBlacklist}
515+ {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{fr}, \sRef)}
516+} \textsc{Mon-Loc}
517+\end{equation*}
518+%
519+\begin{equation*}
520+\frac{
521+ \sPid_\mathit{fr} \notin \sSenders(\sQueue)
522+}{
523+ \sSystem{\sProcesses}
524+ {\sQueue, (\sNid_\mathit{to}, \sPid_\mathit{fr}, \sMonitor \; \sRef \; \sId_\mathit{to}), \sQueue'}
525+ {\sBlacklist}
526+ {\sMonitors}
527+\rightarrow
528+ \sSystem{\sProcesses}
529+ {\sQueue, \sQueue'}
530+ {\sBlacklist}
531+ {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{to}, \sRef)}
532+} \textsc{Mon-Rem}
533+\end{equation*}
534+%
535+\begin{equation*}
536+\frac{
537+ \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})
538+\qquad
539+ (\sId_\mathit{to}, \sPid_\mathit{fr}) \in \sBlacklist
540+}{
541+ \sSystem{\sProcesses}
542+ {\sQueue}
543+ {\sBlacklist}
544+ {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{fr}, \sRef)}
545+\rightarrow
546+ \sSystem{\sProcesses}
547+ {\sQueue, (\sPid_\mathit{fr}, \sId_\mathit{to}, \mathtt{discon} \; \sRef)}
548+ {\sBlacklist}
549+ {\sMonitors}
550+} \textsc{Mon-Dis}
551+\end{equation*}
552+%
553+\begin{equation*}
554+\frac{
555+ \sNodeOf(\sPid) = \sNid
556+}{
557+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
558+ {\sQueue}
559+ {\sBlacklist}
560+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
561+\rightarrow
562+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
563+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{died} \; \sRef)}
564+ {\sBlacklist}
565+ {\sMonitors}
566+} \textsc{Mon-Ret}
567+\end{equation*}
568+%
569+\begin{equation*}
570+\frac{
571+ \sNodeOf(\sPid) = \sNid
572+}{
573+ \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}
574+ {\sQueue}
575+ {\sBlacklist}
576+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
577+\rightarrow
578+ \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}
579+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{exc} \; \sRef \; M)}
580+ {\sBlacklist}
581+ {\sMonitors}
582+} \textsc{Mon-Throw}
583+\end{equation*}
584+%
585+\begin{equation*}
586+\frac{
587+ \sNodeOf(\sPid) = \sNid
588+\qquad
589+ \sPid \notin \sProcesses
590+}{
591+ \sSystem{\sProcesses}
592+ {\sQueue}
593+ {\sBlacklist}
594+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
595+\rightarrow
596+ \sSystem{\sProcesses}
597+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{unknown} \; \sRef)}
598+ {\sBlacklist}
599+ {\sMonitors}
600+} \textsc{Mon-Unknown}
601+\end{equation*}
602+%
603+\caption{Monitoring}
604+\end{figure}
605+
606+\subsection{Process Termination}
607+
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.
611+
612+\begin{figure}
613+\small
614+%
615+\begin{equation*}
616+\frac{
617+ \sNodeOf(\sPid) = \sNid
618+\qquad
619+ \nexists \; \sPid', \sRef \cdot (\sPid', \sPid, \sNid, \sRef) \in \sMonitors
620+}{
621+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
622+ {\sQueue}
623+ {\sBlacklist}
624+ {\sMonitors}
625+\rightarrow
626+ \sSystem{\sProcesses}
627+ {\sQueue}
628+ {\sBlacklist}
629+ {\sMonitors}
630+} \textsc{TermRet}
631+\end{equation*}
632+%
633+\begin{equation*}
634+\frac{
635+ \sNodeOf(\sPid) = \sNid
636+\qquad
637+ \nexists \; \sPid', \sRef \cdot (\sPid', \sPid, \sNid, \sRef) \in \sMonitors
638+}{
639+ \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}
640+ {\sQueue}
641+ {\sBlacklist}
642+ {\sMonitors}
643+\rightarrow
644+ \sSystem{\sProcesses}
645+ {\sQueue}
646+ {\sBlacklist}
647+ {\sMonitors}
648+} \textsc{TermThrow}
649+\end{equation*}
650+%
651+\caption{\label{fig:termination}Process Termination}
652+\end{figure}
653+
654+\section{Open Issues}
655+
656+\subsection{Ordering of Monitor/Link Notifications}
657+
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
662+
663+\begin{lstlisting}
664+receiveWait [
665+ match $ \(Reply reply) -> ...
666+ , match $ \(ProcessMonitorNotification ..) -> ...
667+ ]
668+\end{lstlisting}
669+
670+and process $Q$ does
671+
672+\begin{lstlisting}
673+send pidA (Reply reply)
674+// terminate or indeed throw an exception
675+\end{lstlisting}
676+
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$.
680+
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
683+messages.
684+
685+\subsection{Ordering and Typed Channels}
686+
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.}
696+
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.
702+
703+\bibliographystyle{apalike}
704+\bibliography{references}
705+
706+\end{document}