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