@@ -14,27 +14,36 @@
1414\newcommand{\sLink}{\mathtt{link}}
1515\newcommand{\sThrow}{\mathtt{throw}}
1616\newcommand{\sReconnect}{\mathtt{reconnect}}
17+\newcommand{\sNewChan}{\mathtt{newChan}}
18+\newcommand{\sSendChan}{\mathtt{sendChan}}
19+\newcommand{\sReceiveChan}{\mathtt{receiveChan}}
20+\newcommand{\sMonitor}{\mathtt{monitor}}
21+
22+\DeclareMathOperator{\sNodeOf}{node}
23+\DeclareMathOperator{\sProcessOf}{process}
1724
1825\newcommand{\sSpawned}{\mathtt{spawned}}
1926
2027\newcommand{\sExtend}[1]{\mathrel{\triangleright_{#1}}}
2128
2229\newcommand{\sPar}{\mathrel{\parallel}}
23−\newcommand{\sParN}{\mathrel{{\parallel}_N}}
2430\newcommand{\sProc}[2]{{#1}_{#2}}
2531
26−\newcommand{\sPid}{\ensuremath{\mathit{pid}}}
2732\newcommand{\sNid}{\ensuremath{\mathit{nid}}}
33+\newcommand{\sPid}{\ensuremath{\mathit{pid}}}
34+\newcommand{\sCid}{\ensuremath{\mathit{cid}}}
35+
2836\newcommand{\sId}{\ensuremath{\mathit{id}}}
2937\newcommand{\sRef}{\ensuremath{\mathit{ref}}}
3038
3139\newcommand{\sLinks}{\ensuremath{\mathit{links}}}
3240\newcommand{\sNode}[3]{\left[{#1} ; {#2}\right]_{#3}}
33−\newcommand{\sSystem}[3]{\left\langle #1 ; #2 ; #3 \right\rangle}
41+\newcommand{\sSystem}[4]{\left\langle #1 ; #2 ; #3 ; #4 \right\rangle}
3442\newcommand{\sNodes}{\mathcal{N}}
3543\newcommand{\sQueue}{\mathcal{Q}}
3644\newcommand{\sProcesses}{\mathcal{P}}
3745\newcommand{\sBlacklist}{\mathcal{B}}
46+\newcommand{\sMonitors}{\mathcal{M}}
3847
3948\newcommand{\sJust}[1]{\mathtt{Just} \; {#1}}
4049\newcommand{\sNothing}{\mathtt{Nothing}}
@@ -73,13 +82,21 @@
7382
7483\subsection{Processes, Nodes, Systems}
7584
76−We assume two disjoint enumerable sets $\mathtt{ProcessId}$ and
77−$\mathtt{NodeId}$, ranged over by $\sPid$ and $\sNid$ and representing process
78−identifiers and node identifiers respectively. We do not need to refer to nodes
79−as entities in their own right in the semantics, but simply assume a total
80−function $$\mathtt{node} : \mathtt{ProcessId} \rightarrow \mathtt{NodeId}$$ We
81−also define $\mathtt{Identifier} = \mathtt{ProcessId} \uplus \mathtt{NodeId}$
82−and let $\sId$ range over $\mathtt{Identifier}$.
85+We assume disjoint countable sets $\mathtt{NodeId}$, $\mathtt{ProcessId}$, and
86+$\mathtt{ChannelId}$, changed over by \sNid, \sPid{} and \sCid{} respectively,
87+and representing process identifiers, node identifiers, and (typed) channel
88+identifiers. We assume the existence of total functions
89+%
90+\begin{equation*}
91+\begin{array}{r@{\;:\;}l}
92+\sNodeOf & (\mathtt{ProcessId} \uplus \mathtt{ChannelId}) \rightarrow \mathtt{NodeId} \\
93+\sProcessOf & \mathtt{ChannelId} \rightarrow \mathtt{ProcessId}
94+\end{array}
95+\end{equation*}
96+%
97+and define
98+$$\mathtt{Identifier} = \mathtt{NodeId} \uplus \mathtt{ProcessId} \uplus \mathtt{ChannelId}$$
99+and let $\sId$ range over $\mathtt{Identifier}$.
83100
84101We represent a process as a pair $\sProc{M}{\sPid}$ of a term $M$ and a process
85102ID $\sPid$. We will denote a set of processes as
@@ -87,24 +104,34 @@ ID $\sPid$. We will denote a set of processes as
87104 $$\sProc{M}{\sPid} \sPar \cdots \sPar \sProc{N}{\sPid'}$$
88105%
89106A \emph{system}
90− $\sSystem{\sProcesses}{\sQueue}{\sBlacklist}$
91−finally is a tuple containing a set $\sProcesses$ of nodes,
92−a \emph{system queue} $\sQueue$, and a \emph{blacklist} $\sBlacklist$.
107+ $\sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}$
108+finally is a tuple containing a set $\sProcesses$ of nodes, a \emph{system
109+queue} $\sQueue$, a \emph{blacklist} $\sBlacklist$, and a set of monitors
110+$\sMonitors$.
111+
112+The set of monitors $\sMonitors$ is a set of tuples
113+ $(\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid, \sRef)$
114+which records that the node controller at \sNid is aware that process
115+$\sPid_\mathit{fr}$ is monitoring $\sId_\mathit{to}$.
93116
94117The system queue is a set of triples $(\sId_\mathit{to}, \sId_\mathit{fr},
95118\mathit{message})$ of messages that have been sent but not yet processed. The
96119blacklist records disconnections and is represented as a of pairs
97120$(\sId_\mathit{to}, \sId_\mathit{fr})$.
98121
122+Note that we do not need to refer to nodes as entities in their own right in
123+the semantics.
124+
99125\section{Semantics}
100126
101127\subsection{Contexts}
102128
103129We define an evaluation context as usual (TODO: catch?)
104130
105−\begin{equation*}
106−\sCtxt{E} ::= [] \OR \sBind{\sCtxt{E}}{M}
107−\end{equation*}
131+\begin{align*}
132+\sCtxt{E} & ::= [] \OR \sBind{\sCtxt{E}}{M} \\
133+\sCtxt{P}_\sPid & ::= \sCtxt{E}[]_\sPid \sPar \sProcesses
134+\end{align*}
108135
109136\subsection{Disconnect}
110137
@@ -123,10 +150,19 @@ processes $\sProcesses$, such that
123150%
124151\frac{
125152\sPid \in \sProcesses \qquad
126−\mathtt{node}(\sPid) = \sNid
153+\sNodeOf(\sPid) = \sNid
127154}{
128155\sPid \in \overline{\sNid}
129156}
157+%
158+\qquad
159+%
160+\frac{
161+\sCid \in \sProcesses \qquad
162+\sNodeOf(\sCid) = \sNid
163+}{
164+\sCid \in \overline{\sNid}
165+}
130166\end{equation*}
131167
132168The following rule models random network disconnect between nodes $\sNid_1$ and
@@ -135,28 +171,45 @@ $\sNid_2$:
135171\begin{equation*}
136172\frac{
137173}{
138− \sSystem{\sProcesses}{\sQueue}{\sBlacklist}
174+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
139175\rightarrow
140− \sSystem{\sProcesses}{\sQueue}{\sBlacklist \cup (\overline{\sNid_1} \times \overline{\sNid_2})}
176+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist \cup (\overline{\sNid_1} \times \overline{\sNid_2})}{\sMonitors}
141177} \textsc{Disconnect}
142178\end{equation*}
143179
144−However, connections to and from nodes can be implicitly reconnected:
180+We provide a primitive to remove a connection from the blacklist:
181+
182+\begin{equation*}
183+\frac{
184+}{
185+ \sSystem{\sCtxt{P}[ \sReconnect \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}
186+ {\sQueue}
187+ {\sBlacklist}
188+ {\sMonitors}
189+\rightarrow
190+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_\sPid}
191+ {\sQueue}
192+ {\sBlacklist \backslash (\sPid_\mathit{to}, \sPid_\mathit{fr})}
193+ {\sMonitors}
194+} \textsc{Recon-Ex}
195+\end{equation*}
196+
197+Connections to and from nodes can be implicitly reconnected:
145198
146199\begin{equation*}
147200\frac{
148201}{
149− \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sNid_\mathit{to}, \sId_\mathit{fr})}
202+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sNid_\mathit{to}, \sId_\mathit{fr})}{\sMonitors}
150203\rightarrow
151− \sSystem{\sProcesses}{\sQueue}{\sBlacklist}
152−} \textsc{Recon-To}
204+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
205+} \textsc{Recon-Im1}
153206\qquad
154207\frac{
155208}{
156− \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sId_\mathit{to}, \sNid_\mathit{fr})}
209+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sId_\mathit{to}, \sNid_\mathit{fr})}{\sMonitors}
157210\rightarrow
158− \sSystem{\sProcesses}{\sQueue}{\sBlacklist}
159−} \textsc{Recon-Fr}
211+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}
212+} \textsc{Recon-Im2}
160213\end{equation*}
161214
162215Once a connection has been blacklisted, no further messages can be sent across
@@ -179,45 +232,44 @@ introduce a function
179232\end{array}
180233\end{equation*}
181234
235+
236+
182237\subsection{Process rules}
183238
184−\subsubsection{Sending}
239+\subsubsection{Send and Receive}
185240
186−If the communication is blacklisted the send is a no-op.
241+We ignore issues of serializability for the purposes of this semantics.
187242
188243\begin{equation*}
189244\frac{
190245}{
191− \sSystem{ \sCtxt{E}[ \sSend \; \sPid_\mathit{to} \; M ]_{\sPid_\mathit{fr}}
192− \sPar
193− \sProcesses
194− }
246+ \sSystem{\sCtxt{P}[ \sSend \; \sPid_\mathit{to} \; M ]_{\sPid_\mathit{fr}}}
195247 {\sQueue}
196248 {\sBlacklist}
249+ {\sMonitors}
197250\rightarrow
198− \sSystem{\sCtxt{E}[ \sReturn \; () ]_\mathit{fr} \sPar \sProcesses}
251+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_\mathit{fr}}
199252 {\sQueue \sExtend{\sBlacklist} (\sPid_\mathit{to}, \sPid_\mathit{fr}, M)}
200253 {\sBlacklist}
254+ {\sMonitors}
201255} \textsc{Send}
202256\end{equation*}
203257
204−We ignore issues of serializability for the purposes of this semantics.
205−
206−\subsubsection{Receiving}
207−
208258We return the \emph{first} message of a randomly chosen sender.
209259
210260\begin{equation*}
211261\frac{
212262 \sId_{\mathit{fr}} \notin \sSenders(\sQueue)
213263}{
214− \sSystem{\sCtxt{E}[ \sExpect ]_{\sPid_\mathit{to}} \sPar \sProcesses}
264+ \sSystem{\sCtxt{P}[ \sExpect ]_{\sPid_\mathit{to}}}
215265 {\sQueue, (\sPid_\mathit{to}, \sId_\mathit{fr}, M), \sQueue'}
216266 {\sBlacklist}
267+ {\sMonitors}
217268\rightarrow
218− \sSystem{\sCtxt{E}[ \sReturn \; M ]_{\sPid_\mathit{to}} \sPar \sProcesses}
269+ \sSystem{\sCtxt{P}[ \sReturn \; M ]_{\sPid_\mathit{to}}}
219270 {\sQueue, \sQueue'}
220271 {\sBlacklist}
272+ {\sMonitors}
221273} \textsc{Expect}
222274\end{equation*}
223275
@@ -227,48 +279,186 @@ Spawning is asynchronous
227279
228280\begin{equation*}
229281\frac{
230− \text{\sRef fresh}
282+ \sRef \text{ fresh}
231283}{
232− \sSystem{\sCtxt{E}[ \sSpawn \; \sNid \; M ]_\sPid \sPar \sProcesses}
284+ \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid}
233285 {\sQueue}
234286 {\sBlacklist}
287+ {\sMonitors}
235288\rightarrow
236− \sSystem{\sCtxt{E}[ \sReturn \; \sRef ]_\sPid \sPar \sProcesses}
289+ \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_\sPid}
237290 {\sQueue \sExtend{\sBlacklist} (\sNid, \sPid, \sSpawn \; \sRef \; M)}
238291 {\sBlacklist}
292+ {\sMonitors}
239293} \textsc{Spawn-Async}
240294\end{equation*}
241295
242−
243296\begin{equation*}
244297\frac{
245298 \sPid \notin \sSenders(\sQueue)
246299\qquad
247− \text{$\sPid'$ fresh}
300+ \sPid' \text{ fresh}
301+\qquad
302+ \sNodeOf(\sPid') = \sNid
248303}{
249304 \sSystem{\sProcesses}
250305 {\sQueue, (\sNid, \sPid, \sSpawn \; \sRef \; M), \sQueue'}
251306 {\sBlacklist}
307+ {\sMonitors}
252308\rightarrow
253309 \sSystem{\sProcesses \sPar M_{\sPid'}}
254310 {\sQueue, \sQueue' \sExtend{\sBlacklist} (\sPid, \sNid, \sSpawned \; \sRef \; \sPid')}
255311 {\sBlacklist}
312+ {\sMonitors}
256313} \textsc{Spawn-Reply}
257314\end{equation*}
258315
259−\subsubsection{Reconnect}
316+\subsubsection{Typed Channels}
317+
318+Since the semantics is not type-driven, we represent typed channels simply as
319+an identifier with an annotation whether it is the send-end ($\sCid^s$) or the
320+receive end ($\sCid^r$) of the channel.
260321
261322\begin{equation*}
262323\frac{
324+ \sCid \text{ fresh}
325+\qquad
326+ \sProcessOf(\sCid) = \sPid
263327}{
264− \sSystem{\sCtxt{P}[ \sReconnect \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}
328+ \sSystem{\sCtxt{P}[\sNewChan]_\sPid}
265329 {\sQueue}
266330 {\sBlacklist}
331+ {\sMonitors}
267332\rightarrow
268− \sSystem{\sCtxt{P}[ \sReturn \; () ]_\sPid}
333+ \sSystem{\sCtxt{P}[\sReturn \; (\sCid^s, \sCid^r)]_\sPid}
269334 {\sQueue}
270− {\sBlacklist \backslash (\sPid_\mathit{to}, \sPid_\mathit{fr})}
271−} \textsc{Reconnect}
335+ {\sBlacklist}
336+ {\sMonitors}
337+} \textsc{NewChan}
338+\end{equation*}
339+
340+\begin{equation*}
341+\frac{
342+}{
343+ \sSystem{\sCtxt{P}[ \sSendChan \; \sCid_\mathit{to}^s \; M ]_{\sPid_\mathit{fr}}}
344+ {\sQueue}
345+ {\sBlacklist}
346+ {\sMonitors}
347+\rightarrow
348+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_{\sPid_\mathit{fr}}}
349+ {\sQueue \sExtend{\sBlacklist} (\sCid_\mathit{to}, \sPid_\mathit{fr}, M)}
350+ {\sBlacklist}
351+ {\sMonitors}
352+} \textsc{SendChan}
353+\end{equation*}
354+
355+\begin{equation*}
356+\frac{
357+ \sId_{\mathit{fr}} \notin \sSenders(\sQueue)
358+}{
359+ \sSystem{\sCtxt{P}[ \sReceiveChan \; \sCid^r ]_{\sPid}}
360+ {\sQueue, (\sCid_\mathit{to}, \sPid_\mathit{fr}, M), \sQueue'}
361+ {\sBlacklist}
362+ {\sMonitors}
363+\rightarrow
364+ \sSystem{\sCtxt{P}[ \sReturn \; M ]_{\sPid}}
365+ {\sQueue, \sQueue'}
366+ {\sBlacklist}
367+ {\sMonitors}
368+} \textsc{ReceiveChan}
369+\end{equation*}
370+
371+\subsubsection{Monitoring}
372+
373+\begin{equation*}
374+\frac{
375+ \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})
376+\qquad
377+ \sNid_\mathit{to} = \sNodeOf(\sPid_\mathit{to})
378+\qquad
379+ \sRef \text{ fresh}
380+}{
381+\begin{array}{ll}
382+& \sSystem{\sCtxt{P}[ \sMonitor \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}
383+ {\sQueue}
384+ {\sBlacklist}
385+ {\sMonitors}
386+\\
387+\rightarrow &
388+ \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_{\sPid_\mathit{fr}}}
389+ {\sQueue \sExtend{\sBlacklist} (\sNid_\mathit{to}, \sPid_\mathit{fr}, \sMonitor \; \sRef \; \sId_\mathit{to})}
390+ {\sBlacklist}
391+ {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{fr}, \sRef)}
392+\end{array}
393+} \textsc{Monitor}
394+\end{equation*}
395+
396+\begin{equation*}
397+\frac{
398+ \sPid_\mathit{fr} \notin \sSenders(\sQueue)
399+}{
400+ \sSystem{\sProcesses}
401+ {\sQueue, (\sNid_\mathit{to}, \sPid_\mathit{fr}, \sMonitor \; \sRef \; \sId_\mathit{to}), \sQueue'}
402+ {\sBlacklist}
403+ {\sMonitors}
404+\rightarrow
405+ \sSystem{\sProcesses}
406+ {\sQueue, \sQueue'}
407+ {\sBlacklist}
408+ {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{to}, \sRef)}
409+} \textsc{Monitor-Remote}
410+\end{equation*}
411+
412+\begin{equation*}
413+\frac{
414+ \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})
415+}{
416+ \sSystem{\sProcesses}
417+ {\sQueue}
418+ {\sBlacklist, (\sId_\mathit{to}, \sPid_\mathit{fr})}
419+ {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{fr}, \sRef)}
420+\rightarrow
421+ \sSystem{\sProcesses}
422+ {\sQueue, (\sPid_\mathit{fr}, \sId_\mathit{to}, \mathtt{disconnected} \; \sRef)}
423+ {\sBlacklist, (\sId_\mathit{to}, \sPid_\mathit{fr})}
424+ {\sMonitors}
425+}
426+\end{equation*}
427+
428+\subsubsection{Process Termination}
429+
430+\begin{equation*}
431+\frac{
432+ \sNodeOf(\sPid) = \sNid
433+\qquad
434+ \nexists \; \sPid', \sRef \cdot (\sPid, \sPid', \sNid, \sRef) \in \sMonitors
435+}{
436+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
437+ {\sQueue}
438+ {\sBlacklist}
439+ {\sMonitors}
440+\rightarrow
441+ \sSystem{\sProcesses}
442+ {\sQueue}
443+ {\sBlacklist}
444+ {\sMonitors}
445+} \textsc{Term}
446+\end{equation*}
447+
448+\begin{equation*}
449+\frac{
450+ \sNodeOf(\sPid) = \sNid
451+}{
452+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
453+ {\sQueue}
454+ {\sBlacklist}
455+ {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}
456+\rightarrow
457+ \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}
458+ {\sQueue \sExtend{\sBlacklist} (\sPid', \sPid, \mathtt{died} \; \sRef)}
459+ {\sBlacklist}
460+ {\sMonitors}
461+} \textsc{Died}
272462\end{equation*}
273463
274464\subsubsection{Administration}