@@ -15,11 +15,14 @@
15\newcommand{\sThrow}{\mathtt{throw}}
15\newcommand{\sThrow}{\mathtt{throw}}
16\newcommand{\sReconnect}{\mathtt{reconnect}}
16\newcommand{\sReconnect}{\mathtt{reconnect}}
18−\newcommand{\sParP}{\mathrel{{\parallel}_P}}
18+\newcommand{\sPar}{\mathrel{{\parallel}_P}}
19\newcommand{\sParN}{\mathrel{{\parallel}_N}}
19\newcommand{\sParN}{\mathrel{{\parallel}_N}}
20\newcommand{\sProc}[2]{{#1}_{#2}}
20\newcommand{\sProc}[2]{{#1}_{#2}}
21\newcommand{\sPid}{\ensuremath{\mathit{pid}}}
22\newcommand{\sPid}{\ensuremath{\mathit{pid}}}
22\newcommand{\sNid}{\ensuremath{\mathit{nid}}}
23\newcommand{\sNid}{\ensuremath{\mathit{nid}}}
24+\newcommand{\sId}{\ensuremath{\mathit{id}}}
23\newcommand{\sLinks}{\ensuremath{\mathit{links}}}
26\newcommand{\sLinks}{\ensuremath{\mathit{links}}}
24\newcommand{\sNode}[3]{\left[{#1} ; {#2}\right]_{#3}}
27\newcommand{\sNode}[3]{\left[{#1} ; {#2}\right]_{#3}}
25\newcommand{\sSystem}[3]{\left\langle #1 ; #2 ; #3 \right\rangle}
28\newcommand{\sSystem}[3]{\left\langle #1 ; #2 ; #3 \right\rangle}
@@ -65,31 +68,28 @@
66\subsection{Processes, Nodes, Systems}
69\subsection{Processes, Nodes, Systems}
71+We assume two disjoint enumerable sets $\mathtt{ProcessId}$ and
72+$\mathtt{NodeId}$, ranged over by $\sPid$ and $\sNid$ and representing process
73+identifiers and node identifiers respectively. We do not need to refer to nodes
74+as entities in their own right in the semantics, but simply assume a total
75+function $$\mathtt{node} : \mathtt{ProcessId} \rightarrow \mathtt{NodeId}$$ We
76+also define $\mathtt{Identifier} = \mathtt{ProcessId} \uplus \mathtt{NodeId}$
77+and let $\sId$ range over $\mathtt{Identifier}$.
68−A \emph{process} $\sProc{M}{\sPid}$ is a pair of a term $M$ and a process ID $\sPid$.
79+We represent a process as a pair $\sProc{M}{\sPid}$ of a term $M$ and a process
69−A \emph{node}
80+ID $\sPid$. We will denote a set of processes as
70− $$\sNode{\sProcesses}
81+%
73−is a tuple consisting of a set of
74−processes $\sProcesses$, sometimes written as
75− $$\sProc{M}{\sPid} \sParP \cdots \sParP \sProc{N}{\sPid'}$$
82+ $$\sProc{M}{\sPid} \sPar \cdots \sPar \sProc{N}{\sPid'}$$
76−together with a set \sLinks{} of pairs of process IDs and a node ID \sNid.
83+%
77A \emph{system}
84A \emph{system}
78− $\sSystem{\sNodes}{\sQueue}{\sBlacklist}$
85+ $\sSystem{\sProcesses}{\sQueue}{\sBlacklist}$
79−finally is a tuple containing a set $\sNodes$ of nodes, sometimes written
86+finally is a tuple containing a set $\sProcesses$ of nodes,
80− $$\sNode{\sProcesses}{\sLinks}{\sNid}
84− \sNode{\sProcesses'}{\sLinks'}{\sNid'}
86−a \emph{system queue} $\sQueue$, and a \emph{blacklist} $\sBlacklist$. The
87+a \emph{system queue} $\sQueue$, and a \emph{blacklist} $\sBlacklist$.
87−system queue is a set of triples $(\mathit{to}, \mathit{from},
89+The system queue is a set of triples $(\sId_\mathit{to}, \sId_\mathit{fr},
88\mathit{message})$ of messages that have been sent but not yet processed. The
90\mathit{message})$ of messages that have been sent but not yet processed. The
89−blacklist is a set of pairs $(\mathit{to}, \mathit{from})$. Once a pair
91+blacklist records disconnections and is represented as a of pairs
90−$(\mathit{to}, \mathit{from})$ has been blacklisted messages from
92+$(\sId_\mathit{to}, \sId_\mathit{fr})$.
91−$\mathit{from}$ to $\mathit{to}$ will never be delivered ($\mathit{to}$ and
92−$\mathit{from}$ are node or process identifiers).
94\section{Semantics}
94\section{Semantics}
@@ -105,7 +105,7 @@ A process context, parametrized by a \sPid, identifies a process within a set
105of nodes.
105of nodes.
107\begin{equation*}
107\begin{equation*}
108−\sCtxt{P}_\sPid ::= \sNode{\sProc{\sCtxt{E}}{pid} \sParP \sProcesses}{\sLinks}{\sNid} \sParN \sNodes
108+\sCtxt{P}_\sPid ::= \sNode{\sProc{\sCtxt{E}}{pid} \sPar \sProcesses}{\sLinks}{\sNid} \sParN \sNodes
109\end{equation*}
109\end{equation*}
111We also find it useful to have a process context with two holes, one for a
111We also find it useful to have a process context with two holes, one for a
@@ -115,9 +115,9 @@ This set of processes may or may not live on the same node as \sPid.
115\begin{equation*}
115\begin{equation*}
116\begin{array}{rl}
116\begin{array}{rl}
117\sCtxt{P}_{\sPid,\sNid} ::= &
117\sCtxt{P}_{\sPid,\sNid} ::= &
118− \sNode{\sProc{\sCtxt{E}}{pid} \sParP []}{\sLinks}{\sNid} \sParN \sNodes \\[1em]
118+ \sNode{\sProc{\sCtxt{E}}{pid} \sPar []}{\sLinks}{\sNid} \sParN \sNodes \\[1em]
120− \sNode{\sProc{\sCtxt{E}}{pid} \sParP \sProcesses}{\sLinks}{\sNid'} \sParN \sNode{[]}{\sLinks}{\sNid} \sParN \sNodes
120+ \sNode{\sProc{\sCtxt{E}}{pid} \sPar \sProcesses}{\sLinks}{\sNid'} \sParN \sNode{[]}{\sLinks}{\sNid} \sParN \sNodes
122 (\sNid \neq \sNid')
122 (\sNid \neq \sNid')
123\end{array}
123\end{array}
@@ -125,15 +125,56 @@ This set of processes may or may not live on the same node as \sPid.
126\subsection{System Rules}
126\subsection{System Rules}
128+At the Cloud Haskell level we assume that \emph{nodes} get disconnected, not
129+individual processes. To formalize this, let $\overline{\sNid}$ be the smallest
130+set, given a set of processes $\sProcesses$, such that
135+\sNid \in \overline{\sNid}
141+\sPid \in \sProcesses \qquad
142+\mathtt{node}(\sPid) = \sNid
144+\sPid \in \overline{\sNid}
148+The following rule models random network disconnect between nodes $\sNid_1$ and
128\begin{equation*}
151\begin{equation*}
131− \sSystem{\sNodes}{\sQueue}{\sBlacklist}
154+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}
132\rightarrow
155\rightarrow
133− \sSystem{\sNodes}{\sQueue}{\sBlacklist, (\mathit{to}, \mathit{from})}
156+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist \cup (\overline{\sNid_1} \times \overline{\sNid_2})}
134} \textsc{Disconnect}
157} \textsc{Disconnect}
135\end{equation*}
158\end{equation*}
160+However, connections to and from nodes can be implicitly reconnected:
165+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sNid_\mathit{to}, \sId_\mathit{fr})}
167+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}
172+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sId_\mathit{to}, \sNid_\mathit{fr})}
174+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}
137\subsection{Process rules}
178\subsection{Process rules}
139\subsubsection{Sending}
180\subsubsection{Sending}
@@ -142,27 +183,27 @@ If the communication is blacklisted the send is a no-op.
143\begin{equation*}
184\begin{equation*}
145−(\mathit{to}, \mathit{from}) \notin \sBlacklist
186+(\mathit{to}, \mathit{fr}) \notin \sBlacklist
147− \sSystem{\sCtxt{P}[ \sSend \; \mathit{to} \; V ]_\mathit{from}}
188+ \sSystem{\sCtxt{P}[ \sSend \; \mathit{to} \; V ]_\mathit{fr}}
148 {\sQueue}
189 {\sQueue}
149 {\sBlacklist}
190 {\sBlacklist}
150\rightarrow
191\rightarrow
151− \sSystem{\sCtxt{P}[ \sReturn \; () ]_\mathit{from}}
192+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_\mathit{fr}}
152− {\sQueue, (\mathit{to}, \mathit{from}, V)}
193+ {\sQueue, (\mathit{to}, \mathit{fr}, V)}
153 {\sBlacklist}
194 {\sBlacklist}
154} \textsc{Send-Ok}
195} \textsc{Send-Ok}
155\end{equation*}
196\end{equation*}
157\begin{equation*}
198\begin{equation*}
159−(\mathit{to}, \mathit{from}) \in \sBlacklist
200+(\mathit{to}, \mathit{fr}) \in \sBlacklist
161− \sSystem{\sCtxt{P}[ \sSend \; \mathit{to} \; V ]_\mathit{from}}
202+ \sSystem{\sCtxt{P}[ \sSend \; \mathit{to} \; V ]_\mathit{fr}}
162 {\sQueue}
203 {\sQueue}
163 {\sBlacklist}
204 {\sBlacklist}
164\rightarrow
205\rightarrow
165− \sSystem{\sCtxt{P}[ \sReturn \; () ]_\mathit{from}}
206+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_\mathit{fr}}
166 {\sQueue}
207 {\sQueue}
167 {\sBlacklist}
208 {\sBlacklist}
168} \textsc{Send-No}
209} \textsc{Send-No}
@@ -176,13 +217,13 @@ We return the \emph{first} message of a randomly chosen sender.
177\begin{equation*}
218\begin{equation*}
179− \mathit{from} \notin \sSenders(\sQueue)
220+ \mathit{fr} \notin \sSenders(\sQueue)
181− \sSystem{\sCtxt{P}[ \sExpect ]_\mathit{from}}
222+ \sSystem{\sCtxt{P}[ \sExpect ]_\mathit{fr}}
182− {\sQueue, (\mathit{to}, \mathit{from}, V), \sQueue'}
223+ {\sQueue, (\mathit{to}, \mathit{fr}, V), \sQueue'}
183 {\sBlacklist}
224 {\sBlacklist}
184\rightarrow
225\rightarrow
185− \sSystem{\sCtxt{P}[ \sReturn \; V ]_\mathit{from}}
226+ \sSystem{\sCtxt{P}[ \sReturn \; V ]_\mathit{fr}}
186 {\sQueue, \sQueue'}
227 {\sQueue, \sQueue'}
187 {\sBlacklist}
228 {\sBlacklist}
188} \textsc{Expect}
229} \textsc{Expect}
@@ -199,7 +240,7 @@ We return the \emph{first} message of a randomly chosen sender.
199 {\sQueue}
240 {\sQueue}
200 {\sBlacklist}
241 {\sBlacklist}
201\rightarrow
242\rightarrow
202− \sSystem{\sCtxt{P}[ \sReturn \; (\sJust{\sPid'}) ]_\sPid[\sProcesses \sParP M_{\sPid'}]_\sNid}
243+ \sSystem{\sCtxt{P}[ \sReturn \; (\sJust{\sPid'}) ]_\sPid[\sProcesses \sPar M_{\sPid'}]_\sNid}
203 {\sQueue}
244 {\sQueue}
204 {\sBlacklist}
245 {\sBlacklist}
205} \textsc{Spawn-Ok}
246} \textsc{Spawn-Ok}