7005503 · distributed-process

git.iko.soy/distributed-process

on master help sign in

Extend semantics

7005503Edsko de Vries14 years ago

doc/reconnect/blacklist.tex+239−49

compare with master

unifiedsplit

@@ -14,27 +14,36 @@

14\newcommand{\sLink}{\mathtt{link}}

15\newcommand{\sThrow}{\mathtt{throw}}

16\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}

18\newcommand{\sSpawned}{\mathtt{spawned}}

25\newcommand{\sSpawned}{\mathtt{spawned}}

20\newcommand{\sExtend}[1]{\mathrel{\triangleright_{#1}}}

27\newcommand{\sExtend}[1]{\mathrel{\triangleright_{#1}}}

22\newcommand{\sPar}{\mathrel{\parallel}}

29\newcommand{\sPar}{\mathrel{\parallel}}

23−\newcommand{\sParN}{\mathrel{{\parallel}_N}}

24\newcommand{\sProc}[2]{{#1}_{#2}}

30\newcommand{\sProc}[2]{{#1}_{#2}}

26−\newcommand{\sPid}{\ensuremath{\mathit{pid}}}

27\newcommand{\sNid}{\ensuremath{\mathit{nid}}}

32\newcommand{\sNid}{\ensuremath{\mathit{nid}}}

33+\newcommand{\sPid}{\ensuremath{\mathit{pid}}}

34+\newcommand{\sCid}{\ensuremath{\mathit{cid}}}

35+

28\newcommand{\sId}{\ensuremath{\mathit{id}}}

36\newcommand{\sId}{\ensuremath{\mathit{id}}}

29\newcommand{\sRef}{\ensuremath{\mathit{ref}}}

37\newcommand{\sRef}{\ensuremath{\mathit{ref}}}

31\newcommand{\sLinks}{\ensuremath{\mathit{links}}}

39\newcommand{\sLinks}{\ensuremath{\mathit{links}}}

32\newcommand{\sNode}[3]{\left[{#1} ; {#2}\right]_{#3}}

40\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}

34\newcommand{\sNodes}{\mathcal{N}}

42\newcommand{\sNodes}{\mathcal{N}}

35\newcommand{\sQueue}{\mathcal{Q}}

43\newcommand{\sQueue}{\mathcal{Q}}

36\newcommand{\sProcesses}{\mathcal{P}}

44\newcommand{\sProcesses}{\mathcal{P}}

37\newcommand{\sBlacklist}{\mathcal{B}}

45\newcommand{\sBlacklist}{\mathcal{B}}

46+\newcommand{\sMonitors}{\mathcal{M}}

39\newcommand{\sJust}[1]{\mathtt{Just} \; {#1}}

48\newcommand{\sJust}[1]{\mathtt{Just} \; {#1}}

40\newcommand{\sNothing}{\mathtt{Nothing}}

49\newcommand{\sNothing}{\mathtt{Nothing}}

@@ -73,13 +82,21 @@

74\subsection{Processes, Nodes, Systems}

83\subsection{Processes, Nodes, Systems}

76−We assume two disjoint enumerable sets $\mathtt{ProcessId}$ and

85+We assume disjoint countable sets $\mathtt{NodeId}$, $\mathtt{ProcessId}$, and

77−$\mathtt{NodeId}$, ranged over by $\sPid$ and $\sNid$ and representing process

86+$\mathtt{ChannelId}$, changed over by \sNid, \sPid{} and \sCid{} respectively,

78−identifiers and node identifiers respectively. We do not need to refer to nodes

87+and representing process identifiers, node identifiers, and (typed) channel

79−as entities in their own right in the semantics, but simply assume a total

88+identifiers. We assume the existence of total functions

89+%

90+\begin{equation*}

91+\begin{array}{r@{\;:\;}l}

80−function $$\mathtt{node} : \mathtt{ProcessId} \rightarrow \mathtt{NodeId}$$ We

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

81−also define $\mathtt{Identifier} = \mathtt{ProcessId} \uplus \mathtt{NodeId}$

98+$$\mathtt{Identifier} = \mathtt{NodeId} \uplus \mathtt{ProcessId} \uplus \mathtt{ChannelId}$$

82−and let $\sId$ range over $\mathtt{Identifier}$.

99+and let $\sId$ range over $\mathtt{Identifier}$.

100

84We represent a process as a pair $\sProc{M}{\sPid}$ of a term $M$ and a process

101We represent a process as a pair $\sProc{M}{\sPid}$ of a term $M$ and a process

85ID $\sPid$. We will denote a set of processes as

102ID $\sPid$. We will denote a set of processes as

@@ -87,24 +104,34 @@ ID $\sPid$. We will denote a set of processes as

87 $$\sProc{M}{\sPid} \sPar \cdots \sPar \sProc{N}{\sPid'}$$

104 $$\sProc{M}{\sPid} \sPar \cdots \sPar \sProc{N}{\sPid'}$$

88%

105%

89A \emph{system}

106A \emph{system}

90− $\sSystem{\sProcesses}{\sQueue}{\sBlacklist}$

107+ $\sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}$

91−finally is a tuple containing a set $\sProcesses$ of nodes,

108+finally is a tuple containing a set $\sProcesses$ of nodes, a \emph{system

92−a \emph{system queue} $\sQueue$, and a \emph{blacklist} $\sBlacklist$.

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}$.

116

94The system queue is a set of triples $(\sId_\mathit{to}, \sId_\mathit{fr},

117The system queue is a set of triples $(\sId_\mathit{to}, \sId_\mathit{fr},

95\mathit{message})$ of messages that have been sent but not yet processed. The

118\mathit{message})$ of messages that have been sent but not yet processed. The

96blacklist records disconnections and is represented as a of pairs

119blacklist records disconnections and is represented as a of pairs

97$(\sId_\mathit{to}, \sId_\mathit{fr})$.

120$(\sId_\mathit{to}, \sId_\mathit{fr})$.

121

122+Note that we do not need to refer to nodes as entities in their own right in

123+the semantics.

124+

99\section{Semantics}

125\section{Semantics}

100

126

101\subsection{Contexts}

127\subsection{Contexts}

102

128

103We define an evaluation context as usual (TODO: catch?)

129We define an evaluation context as usual (TODO: catch?)

104

130

105−\begin{equation*}

131+\begin{align*}

106−\sCtxt{E} ::= [] \OR \sBind{\sCtxt{E}}{M}

132+\sCtxt{E} & ::= [] \OR \sBind{\sCtxt{E}}{M} \\

107−\end{equation*}

133+\sCtxt{P}_\sPid & ::= \sCtxt{E}[]_\sPid \sPar \sProcesses

134+\end{align*}

108

135

109\subsection{Disconnect}

136\subsection{Disconnect}

110

137

@@ -123,10 +150,19 @@ processes $\sProcesses$, such that

123%

150%

124\frac{

151\frac{

125\sPid \in \sProcesses \qquad

152\sPid \in \sProcesses \qquad

126−\mathtt{node}(\sPid) = \sNid

153+\sNodeOf(\sPid) = \sNid

127}{

154}{

128\sPid \in \overline{\sNid}

155\sPid \in \overline{\sNid}

129}

156}

157+%

158+\qquad

159+%

160+\frac{

161+\sCid \in \sProcesses \qquad

162+\sNodeOf(\sCid) = \sNid

163+}{

164+\sCid \in \overline{\sNid}

165+}

130\end{equation*}

166\end{equation*}

131

167

132The following rule models random network disconnect between nodes $\sNid_1$ and

168The following rule models random network disconnect between nodes $\sNid_1$ and

@@ -135,28 +171,45 @@ $\sNid_2$:

135\begin{equation*}

171\begin{equation*}

136\frac{

172\frac{

137}{

173}{

138− \sSystem{\sProcesses}{\sQueue}{\sBlacklist}

174+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}

139\rightarrow

175\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}

141} \textsc{Disconnect}

177} \textsc{Disconnect}

142\end{equation*}

178\end{equation*}

143

179

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+

144−However, connections to and from nodes can be implicitly reconnected:

197+Connections to and from nodes can be implicitly reconnected:

145

198

146\begin{equation*}

199\begin{equation*}

147\frac{

200\frac{

148}{

201}{

149− \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sNid_\mathit{to}, \sId_\mathit{fr})}

202+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sNid_\mathit{to}, \sId_\mathit{fr})}{\sMonitors}

150\rightarrow

203\rightarrow

151− \sSystem{\sProcesses}{\sQueue}{\sBlacklist}

204+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}

152−} \textsc{Recon-To}

205+} \textsc{Recon-Im1}

153\qquad

206\qquad

154\frac{

207\frac{

155}{

208}{

156− \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sId_\mathit{to}, \sNid_\mathit{fr})}

209+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist, (\sId_\mathit{to}, \sNid_\mathit{fr})}{\sMonitors}

157\rightarrow

210\rightarrow

158− \sSystem{\sProcesses}{\sQueue}{\sBlacklist}

211+ \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}

159−} \textsc{Recon-Fr}

212+} \textsc{Recon-Im2}

160\end{equation*}

213\end{equation*}

161

214

162Once a connection has been blacklisted, no further messages can be sent across

215Once a connection has been blacklisted, no further messages can be sent across

@@ -179,45 +232,44 @@ introduce a function

179\end{array}

232\end{array}

180\end{equation*}

233\end{equation*}

181

234

235+

236+

182\subsection{Process rules}

237\subsection{Process rules}

183

238

184−\subsubsection{Sending}

239+\subsubsection{Send and Receive}

185

240

186−If the communication is blacklisted the send is a no-op.

241+We ignore issues of serializability for the purposes of this semantics.

187

242

188\begin{equation*}

243\begin{equation*}

189\frac{

244\frac{

190}{

245}{

191− \sSystem{ \sCtxt{E}[ \sSend \; \sPid_\mathit{to} \; M ]_{\sPid_\mathit{fr}}

246+ \sSystem{\sCtxt{P}[ \sSend \; \sPid_\mathit{to} \; M ]_{\sPid_\mathit{fr}}}

192− \sPar

193− \sProcesses

194− }

195 {\sQueue}

247 {\sQueue}

196 {\sBlacklist}

248 {\sBlacklist}

249+ {\sMonitors}

197\rightarrow

250\rightarrow

198− \sSystem{\sCtxt{E}[ \sReturn \; () ]_\mathit{fr} \sPar \sProcesses}

251+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_\mathit{fr}}

199 {\sQueue \sExtend{\sBlacklist} (\sPid_\mathit{to}, \sPid_\mathit{fr}, M)}

252 {\sQueue \sExtend{\sBlacklist} (\sPid_\mathit{to}, \sPid_\mathit{fr}, M)}

200 {\sBlacklist}

253 {\sBlacklist}

254+ {\sMonitors}

201} \textsc{Send}

255} \textsc{Send}

202\end{equation*}

256\end{equation*}

203

257

204−We ignore issues of serializability for the purposes of this semantics.

205−

206−\subsubsection{Receiving}

207−

208We return the \emph{first} message of a randomly chosen sender.

258We return the \emph{first} message of a randomly chosen sender.

209

259

210\begin{equation*}

260\begin{equation*}

211\frac{

261\frac{

212 \sId_{\mathit{fr}} \notin \sSenders(\sQueue)

262 \sId_{\mathit{fr}} \notin \sSenders(\sQueue)

213}{

263}{

214− \sSystem{\sCtxt{E}[ \sExpect ]_{\sPid_\mathit{to}} \sPar \sProcesses}

264+ \sSystem{\sCtxt{P}[ \sExpect ]_{\sPid_\mathit{to}}}

215 {\sQueue, (\sPid_\mathit{to}, \sId_\mathit{fr}, M), \sQueue'}

265 {\sQueue, (\sPid_\mathit{to}, \sId_\mathit{fr}, M), \sQueue'}

216 {\sBlacklist}

266 {\sBlacklist}

267+ {\sMonitors}

217\rightarrow

268\rightarrow

218− \sSystem{\sCtxt{E}[ \sReturn \; M ]_{\sPid_\mathit{to}} \sPar \sProcesses}

269+ \sSystem{\sCtxt{P}[ \sReturn \; M ]_{\sPid_\mathit{to}}}

219 {\sQueue, \sQueue'}

270 {\sQueue, \sQueue'}

220 {\sBlacklist}

271 {\sBlacklist}

272+ {\sMonitors}

221} \textsc{Expect}

273} \textsc{Expect}

222\end{equation*}

274\end{equation*}

223

275

@@ -227,48 +279,186 @@ Spawning is asynchronous

227

279

228\begin{equation*}

280\begin{equation*}

229\frac{

281\frac{

230− \text{\sRef fresh}

282+ \sRef \text{ fresh}

231}{

283}{

232− \sSystem{\sCtxt{E}[ \sSpawn \; \sNid \; M ]_\sPid \sPar \sProcesses}

284+ \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid}

233 {\sQueue}

285 {\sQueue}

234 {\sBlacklist}

286 {\sBlacklist}

287+ {\sMonitors}

235\rightarrow

288\rightarrow

236− \sSystem{\sCtxt{E}[ \sReturn \; \sRef ]_\sPid \sPar \sProcesses}

289+ \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_\sPid}

237 {\sQueue \sExtend{\sBlacklist} (\sNid, \sPid, \sSpawn \; \sRef \; M)}

290 {\sQueue \sExtend{\sBlacklist} (\sNid, \sPid, \sSpawn \; \sRef \; M)}

238 {\sBlacklist}

291 {\sBlacklist}

292+ {\sMonitors}

239} \textsc{Spawn-Async}

293} \textsc{Spawn-Async}

240\end{equation*}

294\end{equation*}

241

295

242−

243\begin{equation*}

296\begin{equation*}

244\frac{

297\frac{

245 \sPid \notin \sSenders(\sQueue)

298 \sPid \notin \sSenders(\sQueue)

246\qquad

299\qquad

247− \text{$\sPid'$ fresh}

300+ \sPid' \text{ fresh}

301+\qquad

302+ \sNodeOf(\sPid') = \sNid

248}{

303}{

249 \sSystem{\sProcesses}

304 \sSystem{\sProcesses}

250 {\sQueue, (\sNid, \sPid, \sSpawn \; \sRef \; M), \sQueue'}

305 {\sQueue, (\sNid, \sPid, \sSpawn \; \sRef \; M), \sQueue'}

251 {\sBlacklist}

306 {\sBlacklist}

307+ {\sMonitors}

252\rightarrow

308\rightarrow

253 \sSystem{\sProcesses \sPar M_{\sPid'}}

309 \sSystem{\sProcesses \sPar M_{\sPid'}}

254 {\sQueue, \sQueue' \sExtend{\sBlacklist} (\sPid, \sNid, \sSpawned \; \sRef \; \sPid')}

310 {\sQueue, \sQueue' \sExtend{\sBlacklist} (\sPid, \sNid, \sSpawned \; \sRef \; \sPid')}

255 {\sBlacklist}

311 {\sBlacklist}

312+ {\sMonitors}

256} \textsc{Spawn-Reply}

313} \textsc{Spawn-Reply}

257\end{equation*}

314\end{equation*}

258

315

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.

260

321

261\begin{equation*}

322\begin{equation*}

262\frac{

323\frac{

324+ \sCid \text{ fresh}

325+\qquad

326+ \sProcessOf(\sCid) = \sPid

263}{

327}{

264− \sSystem{\sCtxt{P}[ \sReconnect \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}

328+ \sSystem{\sCtxt{P}[\sNewChan]_\sPid}

265 {\sQueue}

329 {\sQueue}

266 {\sBlacklist}

330 {\sBlacklist}

331+ {\sMonitors}

267\rightarrow

332\rightarrow

268− \sSystem{\sCtxt{P}[ \sReturn \; () ]_\sPid}

333+ \sSystem{\sCtxt{P}[\sReturn \; (\sCid^s, \sCid^r)]_\sPid}

269 {\sQueue}

334 {\sQueue}

270− {\sBlacklist \backslash (\sPid_\mathit{to}, \sPid_\mathit{fr})}

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}

271−} \textsc{Reconnect}

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}

272\end{equation*}

462\end{equation*}

273

463

274\subsubsection{Administration}

464\subsubsection{Administration}