@@ -1,18 +1,20 @@
11\documentclass{article}
22\usepackage[margin=2.5cm]{geometry}
3−\usepackage{amsmath, amssymb}
3+\usepackage{amsmath, amssymb, stmaryrd}
44\usepackage{mathpazo, times}
5+\usepackage{float}
56
67\newcommand{\sLam}[2]{\lambda {#1} \cdot {#2}}
78\newcommand{\sApp}[2]{{#1} {#2}}
89\newcommand{\sBind}[2]{{#1} \mathrel{\texttt{>}\!\!\texttt{>}\!\texttt{=}} {#2}}
910\newcommand{\sReturn}{\mathtt{return}}
11+\newcommand{\sThrow}[1]{\mathtt{throw} \; {#1}}
12+\newcommand{\sCatch}[2]{\mathtt{catch} \; {#1} \; {#2}}
1013
1114\newcommand{\sExpect}{\mathtt{expect}}
1215\newcommand{\sSend}{\mathtt{send}}
1316\newcommand{\sSpawn}{\mathtt{spawn}}
1417\newcommand{\sLink}{\mathtt{link}}
15−\newcommand{\sThrow}{\mathtt{throw}}
1618\newcommand{\sReconnect}{\mathtt{reconnect}}
1719\newcommand{\sNewChan}{\mathtt{newChan}}
1820\newcommand{\sSendChan}{\mathtt{sendChan}}
@@ -53,23 +55,68 @@
5355\newcommand{\sSenders}{\mathit{senders}}
5456
5557\newcommand{\OR}{\mathrel{|}}
58+\newcommand{\where}{\mathrel{|}}
5659
60+\floatstyle{boxed}
61+\restylefloat{figure}
5762
5863\begin{document}
5964
6065\title{Cloud Haskell Semantics (DRAFT)}
61−\author{Edsko de Vries, Well-Typed LLP}
66+\author{Well-Typed LLP}
6267\date{\today}
6368
6469\maketitle
6570
6671\section{Introduction}
6772
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+Cloud Haskell brings Erlang-style concurrency to Haskell in the form of a
74+library.\footnote{\texttt{http://hackage.haskell.org/package/distributed-process}}
75+The original publication \cite{cloudhaskell} is a good introduction to Cloud
76+Haskell, and is accompanied by an ever-growing number of resouces, collected on
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.
82+
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.
88+
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}.}
99+
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
108+different solution.
109+
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
114+be dealt with.
115+
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
73120%
74121\begin{enumerate}
75122\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
80127``ether'') and do not have an explicit concept of node controllers
81128\end{enumerate}
82129%
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
130+Our semantics differs from the STM semantics in that we pretend that the Cloud
131+Haskell \texttt{Process} monad is the top-level monad, and do not consider the
132+\texttt{IO} monad at all. Current imprecisions with respect to the ``real''
133+Cloud Haskell are
92134%
93135\begin{enumerate}
94136\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.
103145
104146\section{Preliminaries}
105147
106−\subsection{Terms}
107−
108−We assume the usual definitions of values and terms.
109−
110−\begin{equation*}
111−\begin{array}{ll@{\;::=\;}l}
112−\text{value} & V & \sLam{x}{M} \OR
113− \sExpect \OR
114− \sSend \; \sPid \; M \OR
115− \sSpawn \; \sNid \; M \OR
116− \sReturn \; M \OR
117− \cdots
118−\\
119−\text{term} & M, N & \sApp{M}{N} \OR
120− \sBind{M}{N}
121−\end{array}
122−\end{equation*}
123−
124−\subsection{Processes, Nodes, Systems}
125−
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.
148+Cloud Haskell Processes run on \emph{nodes}. Processes communicate by sending
149+messages to each other (directly or using typed channels). Processes can also
150+send messages to nodes (for instance, a request to spawn or monitor a process).
131151
132152We assume disjoint countable sets $\mathtt{NodeId}$, $\mathtt{ProcessId}$, and
133153$\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
157177$\sMonitors$.
158178The set of monitors $\sMonitors$ is a set of tuples
159179 $(\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid, \sRef)$
160−which records that the node controller at \sNid{} knows that process
161−$\sPid_\mathit{fr}$ is monitoring $\sId_\mathit{to}$ ($\sRef$ is the monitor
162−reference).
163−The system queue is a set of triples $(\sId_\mathit{to}, \sId_\mathit{fr},
180+which records that node \sNid{} knows that process $\sPid_\mathit{fr}$ is
181+monitoring $\sId_\mathit{to}$ ($\sRef$ is the monitor reference). The system
182+queue is a set of triples $(\sId_\mathit{to}, \sId_\mathit{fr},
164183\mathit{message})$ of messages that have been sent but not yet processed. The
165184blacklist records disconnections and is represented as a of pairs
166185$(\sId_\mathit{to}, \sId_\mathit{fr})$.
167186
168187\section{Semantics}
169188
170−\subsection{Contexts}
171−
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.
175−
176−\begin{align*}
177−\sCtxt{E} & ::= [] \OR \sBind{\sCtxt{E}}{M} \\
178−\sCtxt{P}_\sPid & ::= \sCtxt{E}[]_\sPid \sPar \sProcesses
179−\end{align*}
180−
181−\subsection{Disconnect}
189+We follow the STM semantics as closely as possible. The language is the same
190+except for the primitives considered, and we use the same concept of evaluation
191+contexts:
182192
183−We assume that entire \emph{nodes} get disconnected from each other, not
184−individual processes. \emph{Reconnecting} however is on a per process basis. To
185−formalize this, let $\overline{\sNid}$ be the smallest set, given a set of
186−processes $\sProcesses$, such that
193+\begin{equation*}
194+\begin{array}{llll}
195+\text{value} & V & ::= & \sId \OR
196+ \sLam{x}{M} \OR
197+ \sReturn \; M \OR
198+ \sBind{M}{N} \OR
199+ \sThrow{M} \OR \sCatch{M}{N} \OR \\
200+ &&& \sExpect \OR
201+ \sSend \; \sPid \; M \OR
202+ \sSpawn \; \sNid \; M \OR
203+ \sMonitor \; \sId
204+\\
205+\text{term} & M, N & ::= & x \OR
206+ V \OR
207+ \sApp{M}{N} \OR
208+ \cdots \\
209+\\
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
212+\end{array}
213+\end{equation*}
187214%
215+Indeed, the ``administrative'' transitions are identical
216+(Figure~\ref{fig:administrative}).
217+
218+\begin{figure}
219+\small
188220\begin{equation*}
189221\frac{
222+ \llbracket M \rrbracket = V \qquad
223+ M \neq V
190224}{
191−\sNid \in \overline{\sNid}
192−}
193−%
225+ M \rightarrow V
226+} \textsc{Eval}
194227\qquad
195−%
196228\frac{
197−\sPid \in \sProcesses \qquad
198−\sNodeOf(\sPid) = \sNid
229+ M \rightarrow N
199230}{
200−\sPid \in \overline{\sNid}
201−}
202−%
203−\qquad
231+ \sSystem{\sCtxt{P}[M]_\sPid}
232+ {\sQueue}
233+ {\sBlacklist}
234+ {\sMonitors}
235+\rightarrow
236+ \sSystem{\sCtxt{P}[N]_\sPid}
237+ {\sQueue}
238+ {\sBlacklist}
239+ {\sMonitors}
240+} \textsc{Admin}
241+\end{equation*}
204242%
205−\frac{
206−\sCid \in \sProcesses \qquad
207−\sNodeOf(\sCid) = \sNid
208−}{
209−\sCid \in \overline{\sNid}
210−}
243+\begin{equation*}
244+\begin{array}{r@{\;\rightarrow\;}ll@{\hspace{2em}}r@{\;\rightarrow\;}ll}
245+\sBind{\sReturn \; N}{M} & M \; N & \textsc{Bind} & \sCatch{(\sReturn \; M)}{N} & \sReturn \; M & \textsc{Catch}_1 \\
246+\sBind{\sThrow{N}}{M} & \sThrow{N} & \textsc{Throw} & \sCatch{(\sThrow M)}{N} & N \; M & \textsc{Catch}_2 \\
247+\end{array}
211248\end{equation*}
249+%
250+\caption{\label{fig:administrative}Administrative Transitions}
251+\end{figure}
252+
253+\subsection{Disconnect and Reconnect}
212254
213−The following rule models random network disconnect between nodes $\sNid_1$ and
214−$\sNid_2$:
255+Figure~\ref{fig:disconnect} gives the semantics for disconnecting and
256+reconnecting. Rule \textsc{Disconnect} models random network disconnect
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$).
215262
263+\begin{figure}
264+\small
216265\begin{equation*}
217266\frac{
267+ \sNid_1 \neq \sNid_2
218268}{
219269 \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
220270\rightarrow
221271 \sSystem{\sProcesses}{\sQueue}{\sBlacklist \cup (\overline{\sNid_1} \times \overline{\sNid_2})}{\sMonitors}
222272} \textsc{Disconnect}
223273\end{equation*}
224−
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*}
244274%
245−$(\sExtend{\sBlacklist})$ is only defined for serializable payloads.
246−
247−We provide a primitive to remove a connection from the blacklist:
248−
249275\begin{equation*}
250276\frac{
251277}{
@@ -260,30 +286,61 @@ We provide a primitive to remove a connection from the blacklist:
260286 {\sMonitors}
261287} \textsc{Recon-Ex}
262288\end{equation*}
263−
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:
268−
289+%
269290\begin{equation*}
270291\frac{
271292}{
272293 \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sNid_\mathit{to}, \sId_\mathit{fr})}{\sMonitors}
273294\rightarrow
274295 \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
275−} \textsc{Recon-Im1}
296+} \textsc{Recon-Im}_1
276297\qquad
277298\frac{
278299}{
279300 \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sId_\mathit{to}, \sNid_\mathit{fr})}{\sMonitors}
280301\rightarrow
281302 \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
282−} \textsc{Recon-Im2}
303+} \textsc{Recon-Im}_2
304+\end{equation*}
305+%
306+where
307+%
308+\begin{equation*}
309+\overline{\sNid} \subset \mathtt{Identifier}
310+ = \{ \sNid \} \cup
311+ \{ \sPid \where \sNodeOf(\sPid) = \sNid \} \cup
312+ \{ \sCid \where \sNodeOf(\sCid) = \sNid \}
283313\end{equation*}
314+\caption{\label{fig:disconnect}Disconnect and Reconnect}
315+\end{figure}
284316
285−\subsection{Send and Receive}
317+\subsection{Communication}
286318
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).
322+
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.
327+
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}).
332+
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
340+this document).
341+
342+\begin{figure}
343+\small
287344\begin{equation*}
288345\frac{
289346}{
@@ -298,9 +355,7 @@ Connections to and from node controllers can be implicitly reconnected:
298355 {\sMonitors}
299356} \textsc{Send}
300357\end{equation*}
301−
302−We return the \emph{first} message of a randomly chosen sender.
303−
358+%
304359\begin{equation*}
305360\frac{
306361 \sId_{\mathit{fr}} \notin \sSenders(\sQueue)
@@ -316,53 +371,7 @@ We return the \emph{first} message of a randomly chosen sender.
316371 {\sMonitors}
317372} \textsc{Expect}
318373\end{equation*}
319−
320−\subsection{Spawning}
321−
322−Spawning is asynchronous
323−
324−\begin{equation*}
325−\frac{
326− \sRef \text{ fresh}
327−}{
328− \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid}
329− {\sQueue}
330− {\sBlacklist}
331− {\sMonitors}
332−\rightarrow
333− \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_\sPid}
334− {\sQueue \sExtend{\sBlacklist} (\sNid, \sPid, \sSpawn \; \sRef \; M)}
335− {\sBlacklist}
336− {\sMonitors}
337−} \textsc{Spawn-Async}
338−\end{equation*}
339−
340−\begin{equation*}
341−\frac{
342− \sPid \notin \sSenders(\sQueue)
343−\qquad
344− \sPid' \text{ fresh}
345−\qquad
346− \sNodeOf(\sPid') = \sNid
347−}{
348− \sSystem{\sProcesses}
349− {\sQueue, (\sNid, \sPid, \sSpawn \; \sRef \; M), \sQueue'}
350− {\sBlacklist}
351− {\sMonitors}
352−\rightarrow
353− \sSystem{\sProcesses \sPar M_{\sPid'}}
354− {\sQueue, \sQueue' \sExtend{\sBlacklist} (\sPid, \sNid, \sSpawned \; \sRef \; \sPid')}
355− {\sBlacklist}
356− {\sMonitors}
357−} \textsc{Spawn-Reply}
358−\end{equation*}
359−
360−\subsection{Typed Channels}
361−
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.
365−
374+%
366375\begin{equation*}
367376\frac{
368377 \sCid \text{ fresh}
@@ -411,12 +420,79 @@ receive end ($\sCid^r$) of the channel.
411420 {\sMonitors}
412421} \textsc{ReceiveChan}
413422\end{equation*}
423+%
424+\begin{equation*}
425+\frac{
426+ \sRef \text{ fresh}
427+}{
428+ \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid}
429+ {\sQueue}
430+ {\sBlacklist}
431+ {\sMonitors}
432+\rightarrow
433+ \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_\sPid}
434+ {\sQueue \sExtend{\sBlacklist} (\sNid, \sPid, \sSpawn \; \sRef \; M)}
435+ {\sBlacklist}
436+ {\sMonitors}
437+} \textsc{Spawn-Async}
438+\end{equation*}
439+%
440+\begin{equation*}
441+\frac{
442+ \sPid \notin \sSenders(\sQueue)
443+\qquad
444+ \sPid' \text{ fresh}
445+\qquad
446+ \sNodeOf(\sPid') = \sNid
447+}{
448+ \sSystem{\sProcesses}
449+ {\sQueue, (\sNid, \sPid, \sSpawn \; \sRef \; M), \sQueue'}
450+ {\sBlacklist}
451+ {\sMonitors}
452+\rightarrow
453+ \sSystem{\sProcesses \sPar M_{\sPid'}}
454+ {\sQueue, \sQueue' \sExtend{\sBlacklist} (\sPid, \sNid, \sSpawned \; \sRef \; \sPid')}
455+ {\sBlacklist}
456+ {\sMonitors}
457+} \textsc{Spawn-Exec}
458+\end{equation*}
459+%
460+where
461+%
462+\begin{equation*}
463+\begin{array}{l@{\;=\;}l@{\hspace{3em}}l}
464+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
465+&
466+ \sQueue, (\sId_\mathit{to}, \sId_\mathit{fr}, M)
467+&
468+ \text{if } (\sId_\mathit{to}, \sId_\mathit{fr}) \notin \sBlacklist
469+\\
470+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
471+&
472+ \sQueue
473+&
474+ \text{otherwise}
475+\end{array}
476+\end{equation*}
477+%
478+$(\sExtend{\sBlacklist})$ is only defined for serializable payloads.
479+\caption{\label{fig:basic}Basic Primitives}
480+\end{figure}
414481
415482\subsection{Monitoring}
416483
417−The local node controller is notified immediately of the new monitor, and the
418−remote monitor is sent a message (which may, of course, be lost).
419−
484+When process $P$ on node $\sNid_P$ wants to monitor process $Q$ on node
485+$\sNid_Q$ \emph{both} nodes must be notified. The local node it notified
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
492+notify $P$.
493+
494+\begin{figure}
495+\small
420496\begin{equation*}
421497\frac{
422498 \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})
@@ -425,21 +501,18 @@ remote monitor is sent a message (which may, of course, be lost).
425501\qquad
426502 \sRef \text{ fresh}
427503}{
428−\begin{array}{ll}
429−& \sSystem{\sCtxt{P}[ \sMonitor \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}
504+\sSystem{\sCtxt{P}[ \sMonitor \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}
430505 {\sQueue}
431506 {\sBlacklist}
432507 {\sMonitors}
433−\\
434−\rightarrow &
508+\rightarrow
435509 \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_{\sPid_\mathit{fr}}}
436510 {\sQueue \sExtend{\sBlacklist} (\sNid_\mathit{to}, \sPid_\mathit{fr}, \sMonitor \; \sRef \; \sId_\mathit{to})}
437511 {\sBlacklist}
438512 {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{fr}, \sRef)}
439−\end{array}
440−} \textsc{Monitor}
513+} \textsc{Mon-Loc}
441514\end{equation*}
442−
515+%
443516\begin{equation*}
444517\frac{
445518 \sPid_\mathit{fr} \notin \sSenders(\sQueue)
@@ -453,12 +526,9 @@ remote monitor is sent a message (which may, of course, be lost).
453526 {\sQueue, \sQueue'}
454527 {\sBlacklist}
455528 {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{to}, \sRef)}
456−} \textsc{Monitor-Remote}
529+} \textsc{Mon-Rem}
457530\end{equation*}
458−
459−The \emph{local} node controller notifies a monitoring process when it gets
460−disconncted from a monitored remote process.
461−
531+%
462532\begin{equation*}
463533\frac{
464534 \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})
@@ -474,13 +544,71 @@ disconncted from a monitored remote process.
474544 {\sQueue, (\sPid_\mathit{fr}, \sId_\mathit{to}, \mathtt{discon} \; \sRef)}
475545 {\sBlacklist}
476546 {\sMonitors}
477−} \textsc{Discon}
547+} \textsc{Mon-Dis}
548+\end{equation*}
549+%
550+\begin{equation*}
551+\frac{
552+ \sNodeOf(\sPid) = \sNid
553+}{
554+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
555+ {\sQueue}
556+ {\sBlacklist}
557+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
558+\rightarrow
559+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
560+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{died} \; \sRef)}
561+ {\sBlacklist}
562+ {\sMonitors}
563+} \textsc{Mon-Ret}
478564\end{equation*}
565+%
566+\begin{equation*}
567+\frac{
568+ \sNodeOf(\sPid) = \sNid
569+}{
570+ \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}
571+ {\sQueue}
572+ {\sBlacklist}
573+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
574+\rightarrow
575+ \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}
576+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{exc} \; \sRef \; M)}
577+ {\sBlacklist}
578+ {\sMonitors}
579+} \textsc{Mon-Throw}
580+\end{equation*}
581+%
582+\begin{equation*}
583+\frac{
584+ \sNodeOf(\sPid) = \sNid
585+\qquad
586+ \sPid \notin \sProcesses
587+}{
588+ \sSystem{\sProcesses}
589+ {\sQueue}
590+ {\sBlacklist}
591+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
592+\rightarrow
593+ \sSystem{\sProcesses}
594+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{unknown} \; \sRef)}
595+ {\sBlacklist}
596+ {\sMonitors}
597+} \textsc{Mon-Unknown}
598+\end{equation*}
599+%
600+\caption{Monitoring}
601+\end{figure}
479602
480603\subsection{Process Termination}
481604
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.
483608
609+\begin{figure}
610+\small
611+%
484612\begin{equation*}
485613\frac{
486614 \sNodeOf(\sPid) = \sNid
@@ -496,30 +624,31 @@ We remove a terminated process only once all its monitors have been notified.
496624 {\sQueue}
497625 {\sBlacklist}
498626 {\sMonitors}
499−} \textsc{Term}
627+} \textsc{TermRet}
500628\end{equation*}
501−
502−The \emph{remote} node controller notifies a monitoring process when its
503−monitored remote process terminates.
504−
629+%
505630\begin{equation*}
506631\frac{
507632 \sNodeOf(\sPid) = \sNid
633+\qquad
634+ \nexists \; \sPid', \sRef \cdot (\sPid', \sPid, \sNid, \sRef) \in \sMonitors
508635}{
509− \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
636+ \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}
510637 {\sQueue}
511638 {\sBlacklist}
512− {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
513−\rightarrow
514− \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
515− {\sQueue \sExtend{\sBlacklist} (\sPid', \sPid, \mathtt{died} \; \sRef)}
639+ {\sMonitors}
640+\rightarrow
641+ \sSystem{\sProcesses}
642+ {\sQueue}
516643 {\sBlacklist}
517644 {\sMonitors}
518−} \textsc{Died}
645+} \textsc{TermThrow}
519646\end{equation*}
647+%
648+\caption{\label{fig:termination}Process Termination}
649+\end{figure}
520650
521−\subsection{Administration}
522−
523−TODO: bind, pure evaluation, maybe exception handling
651+\bibliographystyle{apalike}
652+\bibliography{references}
524653
525654\end{document}