@@ -15,13 +15,18 @@
1515\newcommand{\sThrow}{\mathtt{throw}}
1616\newcommand{\sReconnect}{\mathtt{reconnect}}
1717
18−\newcommand{\sPar}{\mathrel{{\parallel}_P}}
18+\newcommand{\sSpawned}{\mathtt{spawned}}
19+
20+\newcommand{\sExtend}[1]{\mathrel{\triangleright_{#1}}}
21+
22+\newcommand{\sPar}{\mathrel{\parallel}}
1923\newcommand{\sParN}{\mathrel{{\parallel}_N}}
2024\newcommand{\sProc}[2]{{#1}_{#2}}
2125
2226\newcommand{\sPid}{\ensuremath{\mathit{pid}}}
2327\newcommand{\sNid}{\ensuremath{\mathit{nid}}}
2428\newcommand{\sId}{\ensuremath{\mathit{id}}}
29+\newcommand{\sRef}{\ensuremath{\mathit{ref}}}
2530
2631\newcommand{\sLinks}{\ensuremath{\mathit{links}}}
2732\newcommand{\sNode}[3]{\left[{#1} ; {#2}\right]_{#3}}
@@ -101,33 +106,12 @@ We define an evaluation context as usual (TODO: catch?)
101106\sCtxt{E} ::= [] \OR \sBind{\sCtxt{E}}{M}
102107\end{equation*}
103108
104−A process context, parametrized by a \sPid, identifies a process within a set
105−of nodes.
106−
107−\begin{equation*}
108−\sCtxt{P}_\sPid ::= \sNode{\sProc{\sCtxt{E}}{pid} \sPar \sProcesses}{\sLinks}{\sNid} \sParN \sNodes
109−\end{equation*}
110−
111−We also find it useful to have a process context with two holes, one for a
112−process identified by \sPid{} and one for the set of processes on node \sNid.
113−This set of processes may or may not live on the same node as \sPid.
114−
115−\begin{equation*}
116−\begin{array}{rl}
117−\sCtxt{P}_{\sPid,\sNid} ::= &
118− \sNode{\sProc{\sCtxt{E}}{pid} \sPar []}{\sLinks}{\sNid} \sParN \sNodes \\[1em]
119−\OR &
120− \sNode{\sProc{\sCtxt{E}}{pid} \sPar \sProcesses}{\sLinks}{\sNid'} \sParN \sNode{[]}{\sLinks}{\sNid} \sParN \sNodes
121− \qquad
122− (\sNid \neq \sNid')
123−\end{array}
124−\end{equation*}
125−
126−\subsection{System Rules}
109+\subsection{Disconnect}
127110
128111At 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
112+individual processes. \emph{Reconnecting} however is on a per process basis. To
113+formalize this, let $\overline{\sNid}$ be the smallest set, given a set of
114+processes $\sProcesses$, such that
131115%
132116\begin{equation*}
133117\frac{
@@ -175,6 +159,26 @@ However, connections to and from nodes can be implicitly reconnected:
175159} \textsc{Recon-Fr}
176160\end{equation*}
177161
162+Once a connection has been blacklisted, no further messages can be sent across
163+that connection (until an explicit or implicit reconnect). To model this we
164+introduce a function
165+%
166+\begin{equation*}
167+\begin{array}{l@{\;=\;}l@{\hspace{3em}}l}
168+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
169+&
170+ \sQueue, (\sId_\mathit{to}, \sId_\mathit{fr}, M)
171+&
172+ \text{if } (\sId_\mathit{to}, \sId_\mathit{fr}) \notin \sBlacklist
173+\\
174+ \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)
175+&
176+ \sQueue
177+&
178+ \text{otherwise}
179+\end{array}
180+\end{equation*}
181+
178182\subsection{Process rules}
179183
180184\subsubsection{Sending}
@@ -183,33 +187,21 @@ If the communication is blacklisted the send is a no-op.
183187
184188\begin{equation*}
185189\frac{
186−(\mathit{to}, \mathit{fr}) \notin \sBlacklist
187190}{
188− \sSystem{\sCtxt{P}[ \sSend \; \mathit{to} \; V ]_\mathit{fr}}
191+ \sSystem{ \sCtxt{E}[ \sSend \; \sPid_\mathit{to} \; M ]_{\sPid_\mathit{fr}}
192+ \sPar
193+ \sProcesses
194+ }
189195 {\sQueue}
190196 {\sBlacklist}
191197\rightarrow
192− \sSystem{\sCtxt{P}[ \sReturn \; () ]_\mathit{fr}}
193− {\sQueue, (\mathit{to}, \mathit{fr}, V)}
198+ \sSystem{\sCtxt{E}[ \sReturn \; () ]_\mathit{fr} \sPar \sProcesses}
199+ {\sQueue \sExtend{\sBlacklist} (\sPid_\mathit{to}, \sPid_\mathit{fr}, M)}
194200 {\sBlacklist}
195−} \textsc{Send-Ok}
201+} \textsc{Send}
196202\end{equation*}
197203
198−\begin{equation*}
199−\frac{
200−(\mathit{to}, \mathit{fr}) \in \sBlacklist
201−}{
202− \sSystem{\sCtxt{P}[ \sSend \; \mathit{to} \; V ]_\mathit{fr}}
203− {\sQueue}
204− {\sBlacklist}
205−\rightarrow
206− \sSystem{\sCtxt{P}[ \sReturn \; () ]_\mathit{fr}}
207− {\sQueue}
208− {\sBlacklist}
209−} \textsc{Send-No}
210−\end{equation*}
211−
212−TODO: this allows to send functions
204+We ignore issues of serializability for the purposes of this semantics.
213205
214206\subsubsection{Receiving}
215207
@@ -217,13 +209,13 @@ We return the \emph{first} message of a randomly chosen sender.
217209
218210\begin{equation*}
219211\frac{
220− \mathit{fr} \notin \sSenders(\sQueue)
212+ \sId_{\mathit{fr}} \notin \sSenders(\sQueue)
221213}{
222− \sSystem{\sCtxt{P}[ \sExpect ]_\mathit{fr}}
223− {\sQueue, (\mathit{to}, \mathit{fr}, V), \sQueue'}
214+ \sSystem{\sCtxt{E}[ \sExpect ]_{\sPid_\mathit{to}} \sPar \sProcesses}
215+ {\sQueue, (\sPid_\mathit{to}, \sId_\mathit{fr}, M), \sQueue'}
224216 {\sBlacklist}
225217\rightarrow
226− \sSystem{\sCtxt{P}[ \sReturn \; V ]_\mathit{fr}}
218+ \sSystem{\sCtxt{E}[ \sReturn \; M ]_{\sPid_\mathit{to}} \sPar \sProcesses}
227219 {\sQueue, \sQueue'}
228220 {\sBlacklist}
229221} \textsc{Expect}
@@ -231,33 +223,37 @@ We return the \emph{first} message of a randomly chosen sender.
231223
232224\subsubsection{Spawning}
233225
226+Spawning is asynchronous
227+
234228\begin{equation*}
235229\frac{
236− \sPid' \text{ fresh} \qquad
237− (\sNid, \sPid) \notin \sBlacklist
230+ \text{\sRef fresh}
238231}{
239− \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid[\sProcesses]_\sNid}
232+ \sSystem{\sCtxt{E}[ \sSpawn \; \sNid \; M ]_\sPid \sPar \sProcesses}
240233 {\sQueue}
241234 {\sBlacklist}
242235\rightarrow
243− \sSystem{\sCtxt{P}[ \sReturn \; (\sJust{\sPid'}) ]_\sPid[\sProcesses \sPar M_{\sPid'}]_\sNid}
244− {\sQueue}
236+ \sSystem{\sCtxt{E}[ \sReturn \; \sRef ]_\sPid \sPar \sProcesses}
237+ {\sQueue \sExtend{\sBlacklist} (\sNid, \sPid, \sSpawn \; \sRef \; M)}
245238 {\sBlacklist}
246−} \textsc{Spawn-Ok}
239+} \textsc{Spawn-Async}
247240\end{equation*}
248241
242+
249243\begin{equation*}
250244\frac{
251− (\sNid, \sPid) \in \sBlacklist
245+ \sPid \notin \sSenders(\sQueue)
246+\qquad
247+ \text{$\sPid'$ fresh}
252248}{
253− \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid}
254− {\sQueue}
249+ \sSystem{\sProcesses}
250+ {\sQueue, (\sNid, \sPid, \sSpawn \; \sRef \; M), \sQueue'}
255251 {\sBlacklist}
256−\rightarrow
257− \sSystem{\sCtxt{P}[ \sReturn \; \sNothing ]_\sPid}
258− {\sQueue}
252+\rightarrow
253+ \sSystem{\sProcesses \sPar M_{\sPid'}}
254+ {\sQueue, \sQueue' \sExtend{\sBlacklist} (\sPid, \sNid, \sSpawned \; \sRef \; \sPid')}
259255 {\sBlacklist}
260−} \textsc{Spawn-No}
256+} \textsc{Spawn-Reply}
261257\end{equation*}
262258
263259\subsubsection{Reconnect}
@@ -265,28 +261,14 @@ We return the \emph{first} message of a randomly chosen sender.
265261\begin{equation*}
266262\frac{
267263}{
268− \sSystem{\sCtxt{P}[ \sReconnect \; \mathit{id} ]_\sPid}
269− {\sQueue}
270− {\sBlacklist, (\mathit{id}, \sPid), \sBlacklist'}
271−\rightarrow
272− \sSystem{\sCtxt{P}[ \sReturn \; () ]_\sPid}
273− {\sQueue}
274− {\sBlacklist, \sBlacklist'}
275−} \textsc{Reconnect-Ok}
276−\end{equation*}
277−
278−\begin{equation*}
279−\frac{
280− (\mathit{id}, \sPid) \notin \sBlacklist
281−}{
282− \sSystem{\sCtxt{P}[ \sReconnect \; \mathit{id} ]_\sPid}
264+ \sSystem{\sCtxt{P}[ \sReconnect \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}
283265 {\sQueue}
284266 {\sBlacklist}
285267\rightarrow
286268 \sSystem{\sCtxt{P}[ \sReturn \; () ]_\sPid}
287269 {\sQueue}
288− {\sBlacklist}
289−} \textsc{Reconnect-No}
270+ {\sBlacklist \backslash (\sPid_\mathit{to}, \sPid_\mathit{fr})}
271+} \textsc{Reconnect}
290272\end{equation*}
291273
292274\subsubsection{Administration}