@@ -1,18 +1,20 @@
1\documentclass{article}
1\documentclass{article}
2\usepackage[margin=2.5cm]{geometry}
2\usepackage[margin=2.5cm]{geometry}
3−\usepackage{amsmath, amssymb}
3+\usepackage{amsmath, amssymb, stmaryrd}
4\usepackage{mathpazo, times}
4\usepackage{mathpazo, times}
6\newcommand{\sLam}[2]{\lambda {#1} \cdot {#2}}
7\newcommand{\sLam}[2]{\lambda {#1} \cdot {#2}}
7\newcommand{\sApp}[2]{{#1} {#2}}
8\newcommand{\sApp}[2]{{#1} {#2}}
8\newcommand{\sBind}[2]{{#1} \mathrel{\texttt{>}\!\!\texttt{>}\!\texttt{=}} {#2}}
9\newcommand{\sBind}[2]{{#1} \mathrel{\texttt{>}\!\!\texttt{>}\!\texttt{=}} {#2}}
9\newcommand{\sReturn}{\mathtt{return}}
10\newcommand{\sReturn}{\mathtt{return}}
11+\newcommand{\sThrow}[1]{\mathtt{throw} \; {#1}}
12+\newcommand{\sCatch}[2]{\mathtt{catch} \; {#1} \; {#2}}
11\newcommand{\sExpect}{\mathtt{expect}}
14\newcommand{\sExpect}{\mathtt{expect}}
12\newcommand{\sSend}{\mathtt{send}}
15\newcommand{\sSend}{\mathtt{send}}
13\newcommand{\sSpawn}{\mathtt{spawn}}
16\newcommand{\sSpawn}{\mathtt{spawn}}
14\newcommand{\sLink}{\mathtt{link}}
17\newcommand{\sLink}{\mathtt{link}}
15−\newcommand{\sThrow}{\mathtt{throw}}
16\newcommand{\sReconnect}{\mathtt{reconnect}}
18\newcommand{\sReconnect}{\mathtt{reconnect}}
17\newcommand{\sNewChan}{\mathtt{newChan}}
19\newcommand{\sNewChan}{\mathtt{newChan}}
18\newcommand{\sSendChan}{\mathtt{sendChan}}
20\newcommand{\sSendChan}{\mathtt{sendChan}}
@@ -53,23 +55,68 @@
53\newcommand{\sSenders}{\mathit{senders}}
55\newcommand{\sSenders}{\mathit{senders}}
55\newcommand{\OR}{\mathrel{|}}
57\newcommand{\OR}{\mathrel{|}}
58+\newcommand{\where}{\mathrel{|}}
58\begin{document}
63\begin{document}
60\title{Cloud Haskell Semantics (DRAFT)}
65\title{Cloud Haskell Semantics (DRAFT)}
61−\author{Edsko de Vries, Well-Typed LLP}
66+\author{Well-Typed LLP}
62\date{\today}
67\date{\today}
66\section{Introduction}
71\section{Introduction}
68−This is a semantics for Cloud Haskell, based on the \textit{Unified Semantics
73+Cloud Haskell brings Erlang-style concurrency to Haskell in the form of a
69−for a Future Erlang} (Hans Svensson, Lars-\AA{}ke Fredlund and Clara Benac
74+library.\footnote{\texttt{http://hackage.haskell.org/package/distributed-process}}
70−Earle, Erlang '10) but using the semantics style of \textit{Composable Memory
75+The original publication \cite{cloudhaskell} is a good introduction to Cloud
71−Transactions} (Tim Harris, Simon Marlow, Simon Peyton-Jones, Maurice Herlihy,
76+Haskell, and is accompanied by an ever-growing number of resouces, collected on
72−PPoPP '05). It differs from the former in that
77+the Haskell
78+Wiki.\footnote{\texttt{http://www.haskell.org/haskellwiki/Cloud\_Haskell}} The
79+current document augments the original publication about Cloud Haskell by
80+giving a precise semantics to the Cloud Haskell primitives. It is meant as a
81+reference, not an introduction.
83+The original Cloud Haskell paper stipulates that messages are ``asynchronous,
84+reliable, and buffered'', but does not describe how this can be achieved.
85+Understanding ``reliable'' to mean ``reliable ordered'' (or ``TCP-like''),
86+the reliability of message delivery comes from the reliability of the
87+underlying network protocol---up to a point.
89+The problem is that the underlying network protocol is connection-oriented, but
90+Cloud Haskell is not. Intuitively, when $P$ sends a message to $Q$, we open a
91+reliable-ordered connection from $P$ to $Q$. Reliability of message delivery
92+now follows from reliability of the network protocol, until $P$ somehow gets
93+disconnected from $Q$. If $P$ now sends another message to $Q$, the
94+implementation cannot simply reconnect: after all, some messages that were sent
95+on the first connection might not have been delivered. This means that $P$
96+might send $m_1, m_2, m_3$ to $Q$, but $Q$ will receive $m_1,
97+m_3$.\footnote{Indeed, message passing in Erlang is ordered but unreliable for
98+the same reason \cite{erlang}.}
100+One (non-)solution is for $P$ to buffer all messages it sends to $Q$, and
101+remove messages from this buffer only when $Q$ acknowledges that it received
102+them. On a reconnect $P$ must ask which message $Q$ last received, and
103+retransmit the rest. This means that when $P$ gets disconnected from $Q$, it
104+must infinitely buffer all messages sent to $Q$ (until a connection is
105+reestablished). However, infinite buffering is too strong a requirement;
106+moreover, this is unsatisfactory because it means implementing a reliable
107+protocol on top of the underlying reliable network protocol. We would like a
110+Instead, Cloud Haskell does \emph{not} attempt to reconnect automatically, but
111+provides a $\sReconnect$ primitive which gives programmers the option of
112+reconnecting manually. This is an explicit acknowledgement from the programmer
113+that message loss might occur, and forces them to consider how such loss might
116+The semantics we present is based on \cite{unified}, which we will refer to the
117+as the ``Unified'' semantics. However, we will present the semantics in a more
118+``Haskell'' style following the semantics for STM \cite{stm}. It differs from
119+the Unified semantics in that
74\begin{enumerate}
121\begin{enumerate}
75\item We introduce an explicit notion of \textit{reconnecting} (with potential
122\item We introduce an explicit notion of \textit{reconnecting} (with potential
@@ -80,15 +127,10 @@ 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
127``ether'') and do not have an explicit concept of node controllers
81\end{enumerate}
128\end{enumerate}
83−It differs from the latter in that
130+Our semantics differs from the STM semantics in that we pretend that the Cloud
86−\item We pretend that the Cloud Haskell \texttt{Process} monad is the top-level
131+Haskell \texttt{Process} monad is the top-level monad, and do not consider the
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
132+\texttt{IO} monad at all. Current imprecisions with respect to the ``real''
93\begin{enumerate}
135\begin{enumerate}
94\item We ignore the issue of serializability, other than to say that the
136\item We ignore the issue of serializability, other than to say that the
@@ -103,31 +145,9 @@ the Unified semantics); a synchronous construct can be derived.
104\section{Preliminaries}
146\section{Preliminaries}
106−\subsection{Terms}
148+Cloud Haskell Processes run on \emph{nodes}. Processes communicate by sending
107−
149+messages to each other (directly or using typed channels). Processes can also
108−We assume the usual definitions of values and terms.
150+send messages to nodes (for instance, a request to spawn or monitor a process).
111−\begin{array}{ll@{\;::=\;}l}
112−\text{value} & V & \sLam{x}{M} \OR
114− \sSend \; \sPid \; M \OR
115− \sSpawn \; \sNid \; M \OR
119−\text{term} & M, N & \sApp{M}{N} \OR
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.
132We assume disjoint countable sets $\mathtt{NodeId}$, $\mathtt{ProcessId}$, and
152We assume disjoint countable sets $\mathtt{NodeId}$, $\mathtt{ProcessId}$, and
133$\mathtt{ChannelId}$, changed over by \sNid, \sPid{} and \sCid{} respectively,
153$\mathtt{ChannelId}$, changed over by \sNid, \sPid{} and \sCid{} respectively,
@@ -157,95 +177,101 @@ queue} $\sQueue$, a \emph{blacklist} $\sBlacklist$, and a set of monitors
157$\sMonitors$.
177$\sMonitors$.
158The set of monitors $\sMonitors$ is a set of tuples
178The set of monitors $\sMonitors$ is a set of tuples
159 $(\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid, \sRef)$
179 $(\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid, \sRef)$
160−which records that the node controller at \sNid{} knows that process
180+which records that node \sNid{} knows that process $\sPid_\mathit{fr}$ is
161−$\sPid_\mathit{fr}$ is monitoring $\sId_\mathit{to}$ ($\sRef$ is the monitor
181+monitoring $\sId_\mathit{to}$ ($\sRef$ is the monitor reference). The system
163−The system queue is a set of triples $(\sId_\mathit{to}, \sId_\mathit{fr},
182+queue is a set of triples $(\sId_\mathit{to}, \sId_\mathit{fr},
164\mathit{message})$ of messages that have been sent but not yet processed. The
183\mathit{message})$ of messages that have been sent but not yet processed. The
165blacklist records disconnections and is represented as a of pairs
184blacklist records disconnections and is represented as a of pairs
166$(\sId_\mathit{to}, \sId_\mathit{fr})$.
185$(\sId_\mathit{to}, \sId_\mathit{fr})$.
168\section{Semantics}
187\section{Semantics}
170−\subsection{Contexts}
189+We follow the STM semantics as closely as possible. The language is the same
171−
190+except for the primitives considered, and we use the same concept of evaluation
172−We define an evaluation context as in the \textit{Composable Memory
191+contexts:
173−Transactions} paper, but note that we work with \emph{sets} of processes so the
174−definition of $\sCtxt{P}$ can be slightly simpler.
177−\sCtxt{E} & ::= [] \OR \sBind{\sCtxt{E}}{M} \\
178−\sCtxt{P}_\sPid & ::= \sCtxt{E}[]_\sPid \sPar \sProcesses
181−\subsection{Disconnect}
183−We assume that entire \emph{nodes} get disconnected from each other, not
193+\begin{equation*}
184−individual processes. \emph{Reconnecting} however is on a per process basis. To
194+\begin{array}{llll}
185−formalize this, let $\overline{\sNid}$ be the smallest set, given a set of
195+\text{value} & V & ::= & \sId \OR
186−processes $\sProcesses$, such that
196+ \sLam{x}{M} \OR
199+ \sThrow{M} \OR \sCatch{M}{N} \OR \\
201+ \sSend \; \sPid \; M \OR
202+ \sSpawn \; \sNid \; M \OR
205+\text{term} & M, N & ::= & x \OR
210+\text{Evaluation} & \sCtxt{E} & ::= & [] \OR \sBind{\sCtxt{E}}{M} \OR \sCatch{\sCtxt{E}}{M} \\
211+\text{context} & \sCtxt{P}_\sPid & ::= & \sCtxt{E}[]_\sPid \sPar \sProcesses
215+Indeed, the ``administrative'' transitions are identical
216+(Figure~\ref{fig:administrative}).
188\begin{equation*}
220\begin{equation*}
222+ \llbracket M \rrbracket = V \qquad
191−\sNid \in \overline{\sNid}
225+ M \rightarrow V
192−}
226+} \textsc{Eval}
197−\sPid \in \sProcesses \qquad
229+ M \rightarrow N
198−\sNodeOf(\sPid) = \sNid
200−\sPid \in \overline{\sNid}
231+ \sSystem{\sCtxt{P}[M]_\sPid}
203−\qquad
234+ {\sMonitors}
236+ \sSystem{\sCtxt{P}[N]_\sPid}
205−\frac{
243+\begin{equation*}
206−\sCid \in \sProcesses \qquad
244+\begin{array}{r@{\;\rightarrow\;}ll@{\hspace{2em}}r@{\;\rightarrow\;}ll}
207−\sNodeOf(\sCid) = \sNid
245+\sBind{\sReturn \; N}{M} & M \; N & \textsc{Bind} & \sCatch{(\sReturn \; M)}{N} & \sReturn \; M & \textsc{Catch}_1 \\
208−}{
246+\sBind{\sThrow{N}}{M} & \sThrow{N} & \textsc{Throw} & \sCatch{(\sThrow M)}{N} & N \; M & \textsc{Catch}_2 \\
209−\sCid \in \overline{\sNid}
247+\end{array}
211\end{equation*}
248\end{equation*}
250+\caption{\label{fig:administrative}Administrative Transitions}
253+\subsection{Disconnect and Reconnect}
255+Figure~\ref{fig:disconnect} gives the semantics for disconnecting and
213−The following rule models random network disconnect between nodes $\sNid_1$ and
256+reconnecting. Rule \textsc{Disconnect} models random network disconnect
214−$\sNid_2$:
257+between nodes $\sNid_1$ and $\sNid_2$. We assume that entire \emph{nodes} get
258+disconnected from each other, not individual processes. \emph{Reconnecting}
259+however is on a per process basis (\textsc{Recon-Ex}). Connections to and from
260+node controllers can be implicitly reconnected ($\textsc{Recon-Im}_1$ and
261+$\textsc{Recon-Im}_2$).
216\begin{equation*}
265\begin{equation*}
267+ \sNid_1 \neq \sNid_2
219 \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
269 \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
220\rightarrow
270\rightarrow
221 \sSystem{\sProcesses}{\sQueue}{\sBlacklist \cup (\overline{\sNid_1} \times \overline{\sNid_2})}{\sMonitors}
271 \sSystem{\sProcesses}{\sQueue}{\sBlacklist \cup (\overline{\sNid_1} \times \overline{\sNid_2})}{\sMonitors}
222} \textsc{Disconnect}
272} \textsc{Disconnect}
223\end{equation*}
273\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.
247−We provide a primitive to remove a connection from the blacklist:
249\begin{equation*}
275\begin{equation*}
@@ -260,30 +286,61 @@ We provide a primitive to remove a connection from the blacklist:
260 {\sMonitors}
286 {\sMonitors}
261} \textsc{Recon-Ex}
287} \textsc{Recon-Ex}
262\end{equation*}
288\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.
267−Connections to and from node controllers can be implicitly reconnected:
269\begin{equation*}
290\begin{equation*}
272 \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sNid_\mathit{to}, \sId_\mathit{fr})}{\sMonitors}
293 \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sNid_\mathit{to}, \sId_\mathit{fr})}{\sMonitors}
273\rightarrow
294\rightarrow
274 \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
295 \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
275−} \textsc{Recon-Im1}
296+} \textsc{Recon-Im}_1
279 \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sId_\mathit{to}, \sNid_\mathit{fr})}{\sMonitors}
300 \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sId_\mathit{to}, \sNid_\mathit{fr})}{\sMonitors}
280\rightarrow
301\rightarrow
281 \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
302 \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
282−} \textsc{Recon-Im2}
303+} \textsc{Recon-Im}_2
309+\overline{\sNid} \subset \mathtt{Identifier}
311+ \{ \sPid \where \sNodeOf(\sPid) = \sNid \} \cup
312+ \{ \sCid \where \sNodeOf(\sCid) = \sNid \}
283\end{equation*}
313\end{equation*}
314+\caption{\label{fig:disconnect}Disconnect and Reconnect}
285−\subsection{Send and Receive}
317+\subsection{Communication}
319+The semantics for the basic primitives are listed in Figure~\ref{fig:basic}.
320+Once a connection has been blacklisted, no further messages can be sent across
321+that connection (until an explicit or implicit reconnect).
323+Message passing is ordered but only for a given sender and receiver; no
324+ordering guarantees exist between messages sent by different processes. For
325+that reason rules \textsc{Expect}, \textsc{ReceiveChan} and \textsc{Spawn-Exec}
326+choose the \emph{first} message of a \emph{randomly chosen} sender.
328+Since the semantics is not type-driven, we represent typed channels simply as
329+an identifier with an annotation whether it is the send-end ($\sCid^s$) or the
330+receive end ($\sCid^r$) of the channel (rules \textsc{NewChan},
331+\textsc{SendChan} and \textsc{ReceiveChan}).
333+Spawning finally is asynchronous. When process $P$ spawns process $Q$ on node
334+$\sNid$ (rule \textsc{Spawn-Async}) a message is sent to node $\sNid$ (which
335+may, of course, never arrive). When the remote node receives the message and
336+actually spawns $Q$ (rule \textsc{Spawn-Exec}) it sends a message back to $P$
337+with $Q$'s process ID. In Cloud Haskell this primitive is called
338+\texttt{spawnAsync}, and the Cloud Haskell \texttt{spawn} primitive is defined
339+in terms of \texttt{spawnAsync} (we do not consider the synchronous version in
287\begin{equation*}
344\begin{equation*}
@@ -298,9 +355,7 @@ Connections to and from node controllers can be implicitly reconnected:
298 {\sMonitors}
355 {\sMonitors}
299} \textsc{Send}
356} \textsc{Send}
300\end{equation*}
357\end{equation*}
302−We return the \emph{first} message of a randomly chosen sender.
304\begin{equation*}
359\begin{equation*}
306 \sId_{\mathit{fr}} \notin \sSenders(\sQueue)
361 \sId_{\mathit{fr}} \notin \sSenders(\sQueue)
@@ -316,53 +371,7 @@ We return the \emph{first} message of a randomly chosen sender.
316 {\sMonitors}
371 {\sMonitors}
317} \textsc{Expect}
372} \textsc{Expect}
318\end{equation*}
373\end{equation*}
320−\subsection{Spawning}
322−Spawning is asynchronous
328− \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid}
333− \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_\sPid}
334− {\sQueue \sExtend{\sBlacklist} (\sNid, \sPid, \sSpawn \; \sRef \; M)}
337−} \textsc{Spawn-Async}
342− \sPid \notin \sSenders(\sQueue)
344− \sPid' \text{ fresh}
346− \sNodeOf(\sPid') = \sNid
348− \sSystem{\sProcesses}
349− {\sQueue, (\sNid, \sPid, \sSpawn \; \sRef \; M), \sQueue'}
353− \sSystem{\sProcesses \sPar M_{\sPid'}}
354− {\sQueue, \sQueue' \sExtend{\sBlacklist} (\sPid, \sNid, \sSpawned \; \sRef \; \sPid')}
357−} \textsc{Spawn-Reply}
360−\subsection{Typed Channels}
362−Since the semantics is not type-driven, we represent typed channels simply as
363−an identifier with an annotation whether it is the send-end ($\sCid^s$) or the
364−receive end ($\sCid^r$) of the channel.
366\begin{equation*}
375\begin{equation*}
368 \sCid \text{ fresh}
377 \sCid \text{ fresh}
@@ -411,12 +420,79 @@ receive end ($\sCid^r$) of the channel.
411 {\sMonitors}
420 {\sMonitors}
412} \textsc{ReceiveChan}
421} \textsc{ReceiveChan}
413\end{equation*}
422\end{equation*}
428+ \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid}
433+ \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_\sPid}
434+ {\sQueue \sExtend{\sBlacklist} (\sNid, \sPid, \sSpawn \; \sRef \; M)}
437+} \textsc{Spawn-Async}
442+ \sPid \notin \sSenders(\sQueue)
444+ \sPid' \text{ fresh}
446+ \sNodeOf(\sPid') = \sNid
448+ \sSystem{\sProcesses}
449+ {\sQueue, (\sNid, \sPid, \sSpawn \; \sRef \; M), \sQueue'}
453+ \sSystem{\sProcesses \sPar M_{\sPid'}}
454+ {\sQueue, \sQueue' \sExtend{\sBlacklist} (\sPid, \sNid, \sSpawned \; \sRef \; \sPid')}
457+} \textsc{Spawn-Exec}
463+\begin{array}{l@{\;=\;}l@{\hspace{3em}}l}
464+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
466+ \sQueue, (\sId_\mathit{to}, \sId_\mathit{fr}, M)
468+ \text{if } (\sId_\mathit{to}, \sId_\mathit{fr}) \notin \sBlacklist
470+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
478+$(\sExtend{\sBlacklist})$ is only defined for serializable payloads.
479+\caption{\label{fig:basic}Basic Primitives}
415\subsection{Monitoring}
482\subsection{Monitoring}
417−The local node controller is notified immediately of the new monitor, and the
484+When process $P$ on node $\sNid_P$ wants to monitor process $Q$ on node
418−remote monitor is sent a message (which may, of course, be lost).
485+$\sNid_Q$ \emph{both} nodes must be notified. The local node it notified
419−
486+immediately, and a message is sent to to the remote node (rules
487+\textsc{Mon-Loc} and \textsc{Mon-Rem}). As with all messages, the
488+message to the remote node might be lost. When $P$ is disconnected from $Q$ it
489+is the responsibility of $P$'s local node $\sNid_P$ to notify $P$
490+(\textsc{Mon-Dis}); when $Q$ terminates (\textsc{Mon-Ret}) or crashes
491+(\textsc{Mon-Throw}) it is the responsibility of the remote node $\sNid_Q$ to
420\begin{equation*}
496\begin{equation*}
422 \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})
498 \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})
@@ -425,21 +501,18 @@ remote monitor is sent a message (which may, of course, be lost).
426 \sRef \text{ fresh}
502 \sRef \text{ fresh}
429−& \sSystem{\sCtxt{P}[ \sMonitor \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}
504+\sSystem{\sCtxt{P}[ \sMonitor \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}
430 {\sQueue}
505 {\sQueue}
431 {\sBlacklist}
506 {\sBlacklist}
432 {\sMonitors}
507 {\sMonitors}
434−\rightarrow &
508+\rightarrow
435 \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_{\sPid_\mathit{fr}}}
509 \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_{\sPid_\mathit{fr}}}
436 {\sQueue \sExtend{\sBlacklist} (\sNid_\mathit{to}, \sPid_\mathit{fr}, \sMonitor \; \sRef \; \sId_\mathit{to})}
510 {\sQueue \sExtend{\sBlacklist} (\sNid_\mathit{to}, \sPid_\mathit{fr}, \sMonitor \; \sRef \; \sId_\mathit{to})}
437 {\sBlacklist}
511 {\sBlacklist}
438 {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{fr}, \sRef)}
512 {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{fr}, \sRef)}
440−} \textsc{Monitor}
513+} \textsc{Mon-Loc}
441\end{equation*}
514\end{equation*}
443\begin{equation*}
516\begin{equation*}
445 \sPid_\mathit{fr} \notin \sSenders(\sQueue)
518 \sPid_\mathit{fr} \notin \sSenders(\sQueue)
@@ -453,12 +526,9 @@ remote monitor is sent a message (which may, of course, be lost).
453 {\sQueue, \sQueue'}
526 {\sQueue, \sQueue'}
454 {\sBlacklist}
527 {\sBlacklist}
455 {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{to}, \sRef)}
528 {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{to}, \sRef)}
456−} \textsc{Monitor-Remote}
529+} \textsc{Mon-Rem}
457\end{equation*}
530\end{equation*}
459−The \emph{local} node controller notifies a monitoring process when it gets
460−disconncted from a monitored remote process.
462\begin{equation*}
532\begin{equation*}
464 \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})
534 \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})
@@ -474,13 +544,71 @@ disconncted from a monitored remote process.
474 {\sQueue, (\sPid_\mathit{fr}, \sId_\mathit{to}, \mathtt{discon} \; \sRef)}
544 {\sQueue, (\sPid_\mathit{fr}, \sId_\mathit{to}, \mathtt{discon} \; \sRef)}
475 {\sBlacklist}
545 {\sBlacklist}
476 {\sMonitors}
546 {\sMonitors}
477−} \textsc{Discon}
547+} \textsc{Mon-Dis}
552+ \sNodeOf(\sPid) = \sNid
554+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
557+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
559+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
560+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{died} \; \sRef)}
478\end{equation*}
564\end{equation*}
568+ \sNodeOf(\sPid) = \sNid
570+ \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}
573+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
575+ \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}
576+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{exc} \; \sRef \; M)}
584+ \sNodeOf(\sPid) = \sNid
586+ \sPid \notin \sProcesses
588+ \sSystem{\sProcesses}
591+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
593+ \sSystem{\sProcesses}
594+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{unknown} \; \sRef)}
597+} \textsc{Mon-Unknown}
480\subsection{Process Termination}
603\subsection{Process Termination}
482−We remove a terminated process only once all its monitors have been notified.
605+The rules for normal and abnormal process termination are defined in
606+Figure~\ref{fig:termination}. When a process crashes it dies
607+silently, unless monitors are setup.
484\begin{equation*}
612\begin{equation*}
486 \sNodeOf(\sPid) = \sNid
614 \sNodeOf(\sPid) = \sNid
@@ -496,30 +624,31 @@ We remove a terminated process only once all its monitors have been notified.
496 {\sQueue}
624 {\sQueue}
497 {\sBlacklist}
625 {\sBlacklist}
498 {\sMonitors}
626 {\sMonitors}
499−} \textsc{Term}
627+} \textsc{TermRet}
500\end{equation*}
628\end{equation*}
502−The \emph{remote} node controller notifies a monitoring process when its
503−monitored remote process terminates.
505\begin{equation*}
630\begin{equation*}
507 \sNodeOf(\sPid) = \sNid
632 \sNodeOf(\sPid) = \sNid
634+ \nexists \; \sPid', \sRef \cdot (\sPid', \sPid, \sNid, \sRef) \in \sMonitors
509− \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
636+ \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}
510 {\sQueue}
637 {\sQueue}
511 {\sBlacklist}
638 {\sBlacklist}
512− {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
639+ {\sMonitors}
513−\rightarrow
640+\rightarrow
514− \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
641+ \sSystem{\sProcesses}
515− {\sQueue \sExtend{\sBlacklist} (\sPid', \sPid, \mathtt{died} \; \sRef)}
642+ {\sQueue}
516 {\sBlacklist}
643 {\sBlacklist}
517 {\sMonitors}
644 {\sMonitors}
518−} \textsc{Died}
645+} \textsc{TermThrow}
519\end{equation*}
646\end{equation*}
648+\caption{\label{fig:termination}Process Termination}
521−\subsection{Administration}
651+\bibliographystyle{apalike}
522−
652+\bibliography{references}
523−TODO: bind, pure evaluation, maybe exception handling
525\end{document}
654\end{document}