@@ -1,409 +0,0 @@
1−\documentclass[10pt]{article}
2−\usepackage[margin=2.5cm]{geometry}
3−\usepackage{listings}
4−\usepackage{amsmath,amssymb,stmaryrd}
5−\usepackage{mathpazo,times}
6−
7−\begin{document}
8−
9−\newcommand{\semNs}{\mathit{ns}}
10−\newcommand{\semEth}{\mathit{eth}}
11−\newcommand{\semPg}{\mathit{pg}}
12−\newcommand{\semNid}{\mathit{nid}}
13−\newcommand{\semNc}{\mathit{nc}}
14−\newcommand{\semRecon}{\mathrm{reconnect}}
15−\newcommand{\semDisconnect}{\mathrm{disconnect}}
16−\newcommand{\semDropped}{\mathrm{dropped}}
17−\newcommand{\semMessage}{\mathrm{message}}
18−\newcommand{\semPid}{\mathit{pid}}
19−
20−\newcommand{\semSystem}[2]{\llbracket #1, #2 \rrbracket}
21−\newcommand{\semNode}[3]{[ #1, #2, #3 ]}
22−\newcommand{\semStdNode}[1]{\semNode{\semPg_{#1}}{\semNid_{#1}}{\semNc_{#1}}}
23−\newcommand{\semProc}[3]{\langle #1, #2, #3 \rangle}
24−\newcommand{\semStdProc}[1]{\semProc{e}{\semPid}{q}}
25−
26−\newcommand{\semDied}[2]{\mathrm{died}(#1, #2)}
27−\newcommand{\semParN}{\mathrel{{\parallel}_N}}
28−\newcommand{\semParP}{\mathrel{{\parallel}_P}}
29−\newcommand{\semEthMatch}[3]{\mathrm{ethMatch}(#1, #2, #3)}
30−
31−\lstset{basicstyle=\ttfamily\small}
32−
33−\title{An Explicit $\semRecon$ Primitive for Cloud Haskell \\ (or a Future Erlang)}
34−\author{\small \begin{tabular}{ll}
35−Edsko de Vries & Duncan Coutts \\
36−Well-Typed LLP & Well-Typed LLP \\
37−\texttt{edsko@well-typed.com} & \texttt{duncan@well-typed.com}
38−\end{tabular}}
39−\maketitle
40−
41−\section*{Introduction}
42−
43−The original Cloud Haskell paper stipulates that messages are ``asynchronous,
44−reliable, and buffered'', but does not describe how this can be achieved.
45−Understanding ``reliable'' to mean ``reliable ordered'' (or ``TCP-like''),
46−the reliability of message delivery comes from the reliability of the
47−underlying network protocol---up to a point.
48−
49−The problem is that the underlying network protocol is connection-oriented, but
50−Cloud Haskell is not. Intuitively, when $P$ sends a message to $Q$, we open a
51−reliable-ordered connection from $P$ to $Q$. Reliability of message delivery
52−now follows from reliability of the network protocol, until $P$ somehow gets
53−disconnected from $Q$. If $P$ now sends another message to $Q$, the
54−implementation cannot simply reconnect: after all, some messages that were sent
55−on the first connection might not have been delivered. This means that $P$
56−might send $m_1, m_2, m_3$ to $Q$, but $Q$ will receive $m_1, m_3$.
57−
58−One (non-)solution is for $P$ to buffer all messages it sends to $Q$, and
59−remove messages from this buffer only when $Q$ acknowledges that it received
60−them. On a reconnect $P$ must ask which message $Q$ last received, and
61−retransmit the rest. This means that when $P$ gets disconnected from $Q$, it
62−must infinitely buffer all messages sent to $Q$ (until a connection is
63−reestablished). However, infinite buffering is too strong a requirement;
64−moreover, this is unsatisfactory because it means implementing a reliable
65−protocol on top of the underlying reliable network protocol. We would like a
66−different solution.
67−
68−But even more important than the exact solution we adopt is a precise
69−semantics of Cloud Haskell message delivery. A good starting point (one that
70−has been used in the new implementation of Cloud Haskell) is \textit{A
71−Unified Semantics for Future Erlang} by Hans Svensson, Lars-\AA{}ke Fredlund
72−and Clara Benac Earle (Erlang '10)---although this semantics leaves the issue
73−of reconnect open.
74−
75−Here we give an overview of the relevant aspects of the Unified semantics,
76−discuss where reconnect comes into the picture, and then propose a new
77−primitive for Cloud Haskell called $\semRecon$, which essentially gives the
78−programmer the ability to explicitly accept message loss.
79−
80−\section*{Overview of the original semantics}
81−
82−The top-level semantics is a labelled transition relation between
83−\textit{systems}
84−%
85−\begin{equation}
86−\semSystem{\semNs}{\semEth} \xrightarrow{\tilde{\mu}} \semSystem{\semNs'}{\semEth'}
87−\end{equation}
88−%
89−A system $\semSystem{\semNs}{\semEth}$ consists of a bunch of nodes $\semNs$
90−and an ``ether'' or system message queue $\semEth$. The ether models, globally,
91−all messages that have been sent but not yet delivered. The label $\tilde{\mu}$
92−is a list of actions, and is only used in the semantics to define fairness (see
93−below).
94−
95−A node is a triplet $\semStdNode{}$ consisting of a bunch of processes
96−$\semPg$, a node ID $\semNid$ and a node controller $\semNc$. The node
97−controller is responsible for all administrative actions on a node (spawning
98−new processes, establishing links, etc.).
99−A process $\semStdProc{}$ consists of an expression $e$, process ID $\semPid$
100−and message queue (mailbox) $q$. Finally, $(\semParN)$ is used for the parallel
101−composition of nodes, and $(\semParP)$ is used for the parallel composition of
102−processes.
103−
104−\subsubsection*{Ordering}
105−
106−The ether contains messages of the form
107−%
108−\begin{equation*}
109−(\mathit{recipient}, \mathit{sender}, \mathit{message})
110−\end{equation*}
111−%
112−where $\mathit{recipient}$ and $\mathit{sender}$ are process IDs or node IDs
113−(for messages to or from node controllers). Ordering of message delivery in
114−the semantics is embodied by a function
115−%
116−\begin{equation*}
117−\semEthMatch{\semEth}{\mathit{to}}{\mathit{from}}
118−\end{equation*}
119−%
120−(Def.~11, p.~25) which selects the \emph{first} message in $\semEth$ from
121−$\mathit{from}$ to $\mathit{to}$. Many of the semantic rules look like
122−%
123−\begin{equation*}
124−\frac{%
125−\semEthMatch{\semEth}{\mathit{to}}{\mathit{from}} = \mathit{sig}
126−}{%
127−\semSystem{\semNs}{\semEth} \rightarrow \text{(do something with $\mathit{sig}$)}
128−}
129−\end{equation*}
130−
131−where $\mathit{to}$ and $\mathit{from}$ are universally quantified over the
132−rule. This means that messages between pairs of processes (or nodes) are
133−ordered, but there is no global ordering guarantee.
134−
135−\subsubsection*{Disconnects}
136−
137−Although the semantics is not connection oriented, it includes a
138−non-deterministic rule $\mathit{node}_\mathit{disconnect}$ which models
139−arbitrary disconnects (Table 9, p.~28):
140−%
141−{\small
142−\begin{equation*}
143−\frac{}{%
144− \begin{array}{l}
145− \semSystem{\semStdNode{1} \semParN \semStdNode{2} \semParN \semNs}{\semEth}
146−\xrightarrow{\semDisconnect(nid_1, nid_2)} \\[0.5em]
147− \semSystem{\semStdNode{1} \semParN \semStdNode{2} \semParN \semNs}
148− {\semEth \cdot (nid_1, nid_2, \semDied{nid_2}{\semDisconnect})
149− \cdot (nid_2, nid_1, \semDied{nid_1}{\semDisconnect})
150− }
151− \end{array}
152−}
153−\end{equation*}
154−}
155−%
156−So at any one point a node controller may receive a message that it got
157−disconnected from another node controller. These messages are handled by the
158−bottom rule in Table 12 (p.~30): local processes that link to (or monitor)
159−processes on the disconnected remote node are killed (or notified).
160−
161−\subsubsection*{Node or process failure}
162−
163−When a process dies (throws an exception) a message is sent to its local node
164−controller (rule $\mathit{exiting}$, Table~4, p.~27). Failure of an entire
165−node is handled by a non-deterministic rule like the one above (rule
166−$\mathit{node}_\mathit{failure}$, Table~9, p.~28). The resulting message is
167−handled in a similar way to a disconnect (Table~12, p.~30).
168−
169−When a process or a node \emph{dies} (but \emph{not} when it gets disconnected)
170−messages to that process (or node) can be removed from the ether (rules
171−$\mathit{missing}_\mathit{process}$ and $\mathit{missing}_\mathit{node}$,
172−Table~6, p.~28).
173−
174−\subsubsection*{Fairness}
175−
176−Since the semantic rules pick an (more or less) arbitrary message from the
177−ether to process, the rules do not guarantee that all messages are eventually
178−delivered. In the paper this is added ``on top'' of the semantic rules by Def.~20
179−(p.~29), which essentially states that all messages that have been sent must be
180−delivered (or explicitly removed by rules $\mathit{missing}_\mathit{process}$
181−and $\mathit{missing}_\mathit{node}$).
182−
183−\section*{Reconnect}
184−
185−\subsubsection*{In the Unified semantics}
186−
187−The original semantics state that
188−
189−\begin{enumerate}
190−\item all messages sent must eventually be delivered or explicitly removed from the ether (fairness)
191−\item only messages to died (not disconnected) processes or nodes can be removed from the ether
192−\end{enumerate}
193−
194−From a practical perspective this means that messages sent from process $P$ to
195−process $Q$ must be infinitely buffered when $P$ gets disconnected to $Q$, and
196−the system should keep retrying to connect to $Q$ until it receives evidence
197−(for instance, from $Q$'s node controller) that $Q$ has died.
198−
199−For messages sent to node controllers (such as attempts to spawn new processes)
200−this is even more problematic: when process $P$ gets disconnected from node
201−$N$, all messages from $P$ to $N$ must be infinitely buffered until a
202−reconnection is established, or dropped when $P$ learns $N$ has died. However,
203−process $P$ might never be able to distinguish a (temporary) disconnect from
204−$N$ from a crash of $N$.
205−
206−\subsubsection*{Permanent disconnects}
207−
208−The simplest solution to avoid infinite buffering is to drop the fairness
209−requirement from the semantics. Now the implementation is free to attempt to
210−reconnect only a finite number of times---or indeed never---and then simply
211−drop all subsequent messages and never reconnect again. This is a correct
212−implementation of the semantics, because without the fairness requirement
213−messages sent from $P$ to $Q$ can be left in the ether forever.\footnote{From a
214−purely formal perspective, the semantics without the fairness guarantee is too
215−permissive: it would allow a message never to be sent even when no disconnect
216−occurs. If we wanted to fix this, we would have to remove messages from the
217−ether on a disconnect, so that fairness can be satisfied, and keep an explicit
218−history of disconnects.}
219−
220−\subsubsection*{Implicit reconnect with potential message loss (Erlang-style)}
221−
222−The solution adopted by Erlang is an implicit reconnect but without
223−buffering. As described in the introduction, this means that it is possible for
224−$P$ to send messages $m_1, m_2, m_3$ to $Q$ and for $Q$ to receive messages
225−$m_1$ and $m_3$, but not $m_2$. We could model this in the semantics by
226−modifying the rule for disconnect so that it removes messages from the ether.
227−
228−\subsubsection*{Explicit Reconnects}
229−
230−Erlang-style implicit reconnects are not very satisfying semantically because
231−it means we cannot really make any claims about the reliability of message
232−delivery. Permanent disconnects are nicer semantically, but might be too
233−limiting (some musings on that below). The solution we propose is to introduce
234−a new primitive called $\semRecon$. Here's the rule:
235−%
236−\begin{equation*}
237−\frac{%
238−e \xrightarrow{\semRecon(i)} e' \qquad
239−(\semEth_0, \semEth_1) = \mathrm{partition} \; (\lambda (\mathit{to}, \mathit{from}, \_) \rightarrow \mathit{to} = i \wedge \mathit{from} = \semPid) \; \semEth
240−}{%
241− \semSystem{\semNode{\semProc{e}{\semPid}{q} \semParP \semPg}{\semNid}{\semNc} \semParN \semNs}{\semEth}
242−\xrightarrow{\semDropped(\semEth_0)}
243− \semSystem{\semNode{\semProc{e'}{\semPid}{q} \semParP \semPg}{\semNid}{\semNc} \semParN \semNs}{\semEth_1}
244−}
245−\end{equation*}
246−%
247−Semantically, when process $P$ calls $\semRecon(Q)$ it explicitly accepts that
248−some the messages it sent to $Q$ might be lost. Note that this is the only
249−change we need to make the Unified semantics. In particular, the fairness
250−requirement stays: since the rule explicitly records that some messages have
251−been dropped, fairness now means:
252−
253−\begin{quote}
254−All messages sent must eventually be delivered, removed from the ether because
255−a process or a node died, or removed from the ether by an explicit $\semRecon$.
256−\end{quote}
257−
258−From an implementation point of view, once $P$'s connection to $Q$ breaks we do
259−not implicitly reconnect (because doing so would mean losing the reliability
260−guarantee). When $P$ calls $\semRecon(Q)$, however, the implementation is
261−free to reestablish a connection from $P$ to $Q$, either immediately or when
262−$P$ sends its next message to $Q$.
263−
264−\section*{Example}
265−
266−Suppose we start with two nodes, both of which run a single process. The system
267−ether and both process queues are empty ($\epsilon$):
268−%
269−\begin{equation*}
270−\semSystem
271− {\semNode{\semProc{p_1}{\semPid_1}{\epsilon}}{\semNid_1}{\semNc_1}
272− \semParN
273− \underbrace{\semNode{\semProc{p_2}{\semPid_2}{\epsilon}}{\semNid_2}{\semNc_2}}_{N_2}
274− }
275− {\epsilon}
276−\end{equation*}
277−%
278−Now $p_1$ sends a message to $p_2$ (Rule $\mathit{output}$, Table~5, p.~28):
279−%
280−\begin{equation*}
281−\frac{%
282− p_1 \xrightarrow{\semPid_2 \; {!_{\semPid_1}} \; \semMessage(v)} p_1'
283−}{%
284−\semSystem
285− {\semNode{\semProc{p_1}{\semPid_1}{\epsilon}}{\semNid_1}{\semNc_1}
286− \semParN
287− N_2
288− }
289− {\epsilon}
290−\xrightarrow{\semPid_2 \; {!_{\semPid_1}} \; \semMessage(v)}
291−\semSystem
292− {\underbrace{\semNode{\semProc{p_1}{\semPid_1}{\epsilon}}{\semNid_1}{\semNc_1}}_{N_1'}
293− \semParN
294− N_2
295− }
296− {\underbrace{(\semPid_2, \semPid_1, \semMessage(v))}_{M_1}}
297−}
298−\end{equation*}
299−%
300−Note that the message has been sent but not yet delivered (i.e., it is in the
301−ether, not in $p_2$'s queue). Now suppose that node $\semNid_1$ gets
302−disconnected from node $\semNid_2$ (Table~9, p.~28):
303−%
304−\begin{equation*}
305−\frac{%
306−}{%
307−\begin{array}{l}
308−\semSystem{N_1' \semParN N_2}{M_1}
309−\xrightarrow{\semDisconnect(\semNid_1, \semNid_2)} \\
310−\semSystem{N_1' \semParN N_2}{M_1 \cdot (nid_1, nid_2, \semDied{nid_2}{\semDisconnect})
311− \cdot (nid_2, nid_1, \semDied{nid_1}{\semDisconnect})}
312−\end{array}
313−}
314−\end{equation*}
315−%
316−Assume that $p_1$ had previously set up monitoring for $p_2$. It gets notified of the disconnect (Table 12), and it receives the monitor message; at this point we're in a state
317−%
318−\begin{equation*}
319−\semSystem{N_1'' \semParN N_2}{M_1}
320−\end{equation*}
321−%
322−where the original message $M_1$ is still in the ether. If at this point $p_1$ sends another message to $p_2$ we end up with an ether
323−%
324−\begin{equation*}
325−M_1 \cdot \underbrace{(\semPid_2, \semPid_1, \semMessage(v_2))}_{M_2}
326−\end{equation*}
327−%
328−which implies that we must deliver $M_1$ before $M_2$. This is of course
329−precisely the ``ordered'' reliability guarantee. If however, $p_1$ calls
330−$\semRecon$ when it receives the monitor message, we remove $M_1$ from the ether;
331−when $p_1$ then sends the next message we can establish a new connection.
332−
333−\section*{The Need for Reconnect}
334−
335−Ordering guarantees are between pairs of processes/nodes. Thus, when $P$ gets
336−disconnected from $Q$, the easiest way to reestablish a connection is for $P$
337−to restart to become a new process $P'$. This will happen naturally when $P$
338−links to $Q$ and can be restarted by some supervisor process.
339−
340−However, if there are many processes connected to $P$, then $P$ might not want
341−to restart (breaking all connections with its own clients) simply in order to
342−be able to reconnect to Q. For instance, maybe $P$ is a webserver and $Q$ is a
343−domain name server; if $P$ gets temporarily disconnected from $Q$, it does not
344−make much sense to require $P$ to restart (and get a new process ID) before it
345−can send new domain name requests (indeed, in this particular example, lost
346−messages to a domain name server may not matter at all).
347−
348−The situation is even more severe for messages sent from processes to
349−\emph{nodes}. For instance, suppose process $P$ does
350−%
351−\begin{lstlisting}[mathescape,keywords={do}]
352−do spawnAsync nid p1 ; spawnAsync nid p2 ; spawnAsync nid p3
353−\end{lstlisting}
354−%
355−and receives a confirmation that $p_3$ was spawned successfully.\footnote{In
356−the unified paper spawn is asynchronous, which is why the new implementation of
357−Cloud Haskell offers \texttt{spawnAsync}; \texttt{spawn} is then implemented in
358−terms of \texttt{spawnAsync} and \texttt{expect}.} Intuitively this seems to
359−suggest that \emph{all} of $p_1$, $p_2$ and $p_3$ should have been spawned, and
360−this is guaranteed by the reliable-ordered guarantee for messages:
361−\texttt{spawnAsync} is nothing more than a message from the process to the node
362−controller of the node $\mathit{nid}$.
363−
364−But the same problem with reconnect occurs here, too. If the connection from
365−the process to the remote node controller is lost, we cannot guarantee ordered
366−delivery. Permanent disconnect would mean that the process would have to
367−restart before it can spawn new processes on this remote node; if the process
368−is some sort of supervisor process, then this might not be what we want to do.
369−Implicit reconnects means we lose the reliability guarantee; an explicit
370−reconnect (probably after a monitor notification about the disconnect from the
371−remote node) allows the process to reestablish a connection to the remote node
372−controller, and forces the programmer of the process to think about how to
373−handle the potential loss of messages.
374−
375−\section*{Alternative Solutions}
376−
377−\begin{itemize}
378−
379−\item A hybrid solution is possible, too. For instance, we might guarantee
380−reliable-ordered message passing for messages sent from process-to-process, but
381−not for process-to-node. In other words, no explicit call is necessary when
382−spawning a new process on a remote node after a disconnect from that remote
383−node. This might muddle the semantics (in particular, if processes don't
384−monitor remote nodes, programmers might get a false sense of security and rely
385−on non-existing ordering guarantees). On the other hand, requiring an explicit
386−reconnect to a remote node before a spawn (or similar primitive) might be
387−confusing.
388−
389−\item Another hybrid solution is to have an implicit reconnect when sending a
390−monitor notification. So, if $P$ monitors $Q$, and gets a monitor notification,
391−then it must expect potential message loss. If $P$ does not monitor $Q$ then
392−disconnects are permanent.
393−
394−\item Since Cloud Haskell supports typed channels as well as sending messages
395−directly to processes, we could decide not to offer any reliability guarantees
396−for messages sent directly to processes, but provide reliable-ordered message
397−delivery on typed channels. This is an attractive solution, because a typed
398−channel could be considered a connection. When $P$ wants to communicate with
399−$Q$, it sends a message to $Q$ requesting a send port. It then communicates
400−with $Q$ through this send port; when it gets disconnected, it could request a
401−\empty{new} typed channel. Importantly, the send port $P$ receives must indeed
402−be a \emph{new} channel (at least from $P$s perspective).
403−
404−\end{itemize}
405−
406−
407−
408−
409−\end{document}