doc/semantics/CloudHaskellSemantics.tex · distributed-process

git.iko.soy/distributed-process

on 3606f3d help sign in

distributed-process/doc/semantics/CloudHaskellSemantics.tex

706 lines 24 kB history raw

1\documentclass{article}

2\usepackage[margin=2.5cm]{geometry}

3\usepackage{amsmath, amssymb, stmaryrd}

4\usepackage{mathpazo, times}

5\usepackage{float}

6\usepackage{listings}

8\newcommand{\sLam}[2]{\lambda {#1} \cdot {#2}}

9\newcommand{\sApp}[2]{{#1} {#2}}

10\newcommand{\sBind}[2]{{#1} \mathrel{\texttt{>}\!\!\texttt{>}\!\texttt{=}} {#2}}

11\newcommand{\sReturn}{\mathtt{return}}

12\newcommand{\sThrow}[1]{\mathtt{throw} \; {#1}}

13\newcommand{\sCatch}[2]{\mathtt{catch} \; {#1} \; {#2}}

15\newcommand{\sExpect}{\mathtt{expect}}

16\newcommand{\sSend}{\mathtt{send}}

17\newcommand{\sSpawn}{\mathtt{spawn}}

18\newcommand{\sLink}{\mathtt{link}}

19\newcommand{\sReconnect}{\mathtt{reconnect}}

20\newcommand{\sNewChan}{\mathtt{newChan}}

21\newcommand{\sSendChan}{\mathtt{sendChan}}

22\newcommand{\sReceiveChan}{\mathtt{receiveChan}}

23\newcommand{\sMonitor}{\mathtt{monitor}}

25\DeclareMathOperator{\sNodeOf}{node}

26\DeclareMathOperator{\sProcessOf}{process}

28\newcommand{\sSpawned}{\mathtt{spawned}}

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

32\newcommand{\sPar}{\mathrel{\parallel}}

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

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

36\newcommand{\sPid}{\ensuremath{\mathit{pid}}}

37\newcommand{\sCid}{\ensuremath{\mathit{cid}}}

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

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

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

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

44\newcommand{\sSystem}[4]{\left\langle #1 ; #2 ; #3 ; #4 \right\rangle}

45\newcommand{\sNodes}{\mathcal{N}}

46\newcommand{\sQueue}{\mathcal{Q}}

47\newcommand{\sProcesses}{\mathcal{P}}

48\newcommand{\sBlacklist}{\mathcal{B}}

49\newcommand{\sMonitors}{\mathcal{M}}

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

52\newcommand{\sNothing}{\mathtt{Nothing}}

54\newcommand{\sCtxt}[1]{\mathbb{#1}}

56\newcommand{\sSenders}{\mathit{senders}}

58\newcommand{\OR}{\mathrel{|}}

59\newcommand{\where}{\mathrel{|}}

61\floatstyle{boxed}

62\restylefloat{figure}

64\lstset{basicstyle=\ttfamily\small}

66\begin{document}

68\title{Cloud Haskell Semantics (DRAFT)}

69\author{Well-Typed LLP}

70\date{\today}

72\maketitle

74\section{Introduction}

76Cloud Haskell brings Erlang-style concurrency to Haskell in the form of a

77library.\footnote{\texttt{http://hackage.haskell.org/package/distributed-process}}

78The original publication \cite{cloudhaskell} is a good introduction to Cloud

79Haskell, and is accompanied by an ever-growing number of resouces, collected on

80the Haskell

81Wiki.\footnote{\texttt{http://www.haskell.org/haskellwiki/Cloud\_Haskell}} The

82current document augments the original publication about Cloud Haskell by

83giving a precise semantics to the Cloud Haskell primitives. It is meant as a

84reference, not an introduction.

86The original Cloud Haskell paper stipulates that messages are ``asynchronous,

87reliable, and buffered'', but does not describe how this can be achieved.

88Understanding ``reliable'' to mean ``reliable ordered'' (or ``TCP-like''),

89the reliability of message delivery comes from the reliability of the

90underlying network protocol---up to a point.

92The problem is that the underlying network protocol is connection-oriented, but

93Cloud Haskell is not. Intuitively, when $P$ sends a message to $Q$, we open a

94reliable-ordered connection from $P$ to $Q$. Reliability of message delivery

95now follows from reliability of the network protocol, until $P$ somehow gets

96disconnected from $Q$. If $P$ now sends another message to $Q$, the

97implementation cannot simply reconnect: after all, some messages that were sent

98on the first connection might not have been delivered. This means that $P$

99might send $m_1, m_2, m_3$ to $Q$, but $Q$ will receive $m_1,

100m_3$.\footnote{Indeed, message passing in Erlang is ordered but unreliable for

101the same reason \cite{erlang}.}

102

103One (non-)solution is for $P$ to buffer all messages it sends to $Q$, and

104remove messages from this buffer only when $Q$ acknowledges that it received

105them. On a reconnect $P$ must ask which message $Q$ last received, and

106retransmit the rest. This means that when $P$ gets disconnected from $Q$, it

107must infinitely buffer all messages sent to $Q$ (until a connection is

108reestablished). However, infinite buffering is too strong a requirement;

109moreover, this is unsatisfactory because it means implementing a reliable

110protocol on top of the underlying reliable network protocol. We would like a

111different solution.

112

113Instead, Cloud Haskell does \emph{not} attempt to reconnect automatically, but

114provides a $\sReconnect$ primitive which gives programmers the option of

115reconnecting manually. This is an explicit acknowledgement from the programmer

116that message loss might occur, and forces them to consider how such loss might

117be dealt with.

118

119The semantics we present is based on \cite{unified}, which we will refer to the

120as the ``Unified'' semantics. However, we will present the semantics in a more

121``Haskell'' style following the semantics for STM \cite{stm}. It differs from

122the Unified semantics in that

123%

124\begin{enumerate}

125\item We introduce an explicit notion of \textit{reconnecting} (with potential

126message loss)

127\item We simplify the semantics: we ``flatten'' sets of nodes of processes as

128sets of processes (but assume a mapping from process identifiers to node

129identifiers), do not have per-process mailboxes (but only the system queue or

130``ether'') and do not have an explicit concept of node controllers

131\end{enumerate}

132%

133Our semantics differs from the STM semantics in that we pretend that the Cloud

134Haskell \texttt{Process} monad is the top-level monad, and do not consider the

135\texttt{IO} monad at all. Current imprecisions with respect to the ``real''

136Cloud Haskell are

137%

138\begin{enumerate}

139\item We ignore the issue of serializability, other than to say that the

140semantics will get stuck when trying to send a non-serializable payload;

141consequently, we do not formalize $\mathtt{static}$

142\item We do not formalize all Cloud Haskell primitives (merging of ports,

143``advanced messaging'', and others)

144\item Some of the concepts that we do formalize are lower-level concepts; for

145instance, the primitive $\sSpawn$ that we formalize is asynchronous (following

146the Unified semantics); a synchronous construct can be derived.

147\end{enumerate}

148

149\section{Preliminaries}

150

151Cloud Haskell Processes run on \emph{nodes}. Processes communicate by sending

152messages to each other (directly or using typed channels). Processes can also

153send messages to nodes (for instance, a request to spawn or monitor a process).

154

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

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

157and representing process identifiers, node identifiers, and (typed) channel

158identifiers. We assume the existence of total functions

159%

160\begin{equation*}

161\begin{array}{r@{\;:\;}l}

162\sNodeOf & (\mathtt{ProcessId} \uplus \mathtt{ChannelId}) \rightarrow \mathtt{NodeId} \\

163\sProcessOf & \mathtt{ChannelId} \rightarrow \mathtt{ProcessId}

164\end{array}

165\end{equation*}

166%

167and define

168$$\mathtt{Identifier} = \mathtt{NodeId} \uplus \mathtt{ProcessId} \uplus \mathtt{ChannelId}$$

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

170

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

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

173%

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

175%

176A \emph{system}

177 $\sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}$

178is a tuple containing a set $\sProcesses$ of processes, a \emph{system

179queue} $\sQueue$, a \emph{blacklist} $\sBlacklist$, and a set of monitors

180$\sMonitors$.

181The set of monitors $\sMonitors$ is a set of tuples

182 $(\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid, \sRef)$

183which records that node \sNid{} knows that process $\sPid_\mathit{fr}$ is

184monitoring $\sId_\mathit{to}$ ($\sRef$ is the monitor reference). The system

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

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

187blacklist records disconnections and is represented as a of pairs

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

189

190\section{Semantics}

191

192We follow the STM semantics as closely as possible. The language is the same

193except for the primitives considered, and we use the same concept of evaluation

194contexts:

195

196\begin{equation*}

197\begin{array}{llll}

198\text{value} & V & ::= & \sId \OR

199 \sLam{x}{M} \OR

200 \sReturn \; M \OR

201 \sBind{M}{N} \OR

202 \sThrow{M} \OR \sCatch{M}{N} \OR \\

203 &&& \sExpect \OR

204 \sSend \; \sPid \; M \OR

205 \sSpawn \; \sNid \; M \OR

206 \sMonitor \; \sId

207\\

208\text{term} & M, N & ::= & x \OR

209 V \OR

210 \sApp{M}{N} \OR

211 \cdots \\

212\\

213\text{Evaluation} & \sCtxt{E} & ::= & [] \OR \sBind{\sCtxt{E}}{M} \OR \sCatch{\sCtxt{E}}{M} \\

214\text{context} & \sCtxt{P}_\sPid & ::= & \sCtxt{E}[]_\sPid \sPar \sProcesses

215\end{array}

216\end{equation*}

217%

218Indeed, the ``administrative'' transitions are identical

219(Figure~\ref{fig:administrative}).

220

221\begin{figure}

222\small

223\begin{equation*}

224\frac{

225 \llbracket M \rrbracket = V \qquad

226 M \neq V

227}{

228 M \rightarrow V

229} \textsc{Eval}

230\qquad

231\frac{

232 M \rightarrow N

233}{

234 \sSystem{\sCtxt{P}[M]_\sPid}

235 {\sQueue}

236 {\sBlacklist}

237 {\sMonitors}

238\rightarrow

239 \sSystem{\sCtxt{P}[N]_\sPid}

240 {\sQueue}

241 {\sBlacklist}

242 {\sMonitors}

243} \textsc{Admin}

244\end{equation*}

245%

246\begin{equation*}

247\begin{array}{r@{\;\rightarrow\;}ll@{\hspace{2em}}r@{\;\rightarrow\;}ll}

248\sBind{\sReturn \; N}{M} & M \; N & \textsc{Bind} & \sCatch{(\sReturn \; M)}{N} & \sReturn \; M & \textsc{Catch}_1 \\

249\sBind{\sThrow{N}}{M} & \sThrow{N} & \textsc{Throw} & \sCatch{(\sThrow M)}{N} & N \; M & \textsc{Catch}_2 \\

250\end{array}

251\end{equation*}

252%

253\caption{\label{fig:administrative}Administrative Transitions}

254\end{figure}

255

256\subsection{Disconnect and Reconnect}

257

258Figure~\ref{fig:disconnect} gives the semantics for disconnecting and

259reconnecting. Rule \textsc{Disconnect} models random network disconnect

260between nodes $\sNid_1$ and $\sNid_2$. We assume that entire \emph{nodes} get

261disconnected from each other, not individual processes. \emph{Reconnecting}

262however is on a per connection basis (\textsc{Recon-Ex}). Connections to and

263from node controllers can be implicitly reconnected ($\textsc{Recon-Im}_1$ and

264$\textsc{Recon-Im}_2$).

265

266\begin{figure}

267\small

268\begin{equation*}

269\frac{

270 \sNid_1 \neq \sNid_2

271}{

272 \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}

273\rightarrow

274 \sSystem{\sProcesses}{\sQueue}{\sBlacklist \cup (\overline{\sNid_1} \times \overline{\sNid_2})}{\sMonitors}

275} \textsc{Disconnect}

276\end{equation*}

277%

278\begin{equation*}

279\frac{

280}{

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

282 {\sQueue}

283 {\sBlacklist}

284 {\sMonitors}

285\rightarrow

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

287 {\sQueue}

288 {\sBlacklist \backslash (\sId_\mathit{to}, \sPid_\mathit{fr})}

289 {\sMonitors}

290} \textsc{Recon-Ex}

291\end{equation*}

292%

293\begin{equation*}

294\frac{

295}{

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

297\rightarrow

298 \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}

299} \textsc{Recon-Im}_1

300\qquad

301\frac{

302}{

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

304\rightarrow

305 \sSystem{\sProcesses}{\sQueue}{\sBlacklist}{\sMonitors}

306} \textsc{Recon-Im}_2

307\end{equation*}

308%

309where

310%

311\begin{equation*}

312\overline{\sNid} \subset \mathtt{Identifier}

313 = \{ \sNid \} \cup

314 \{ \sPid \where \sNodeOf(\sPid) = \sNid \} \cup

315 \{ \sCid \where \sNodeOf(\sCid) = \sNid \}

316\end{equation*}

317\caption{\label{fig:disconnect}Disconnect and Reconnect}

318\end{figure}

319

320\subsection{Communication}

321

322The semantics for the basic primitives are listed in Figure~\ref{fig:basic}.

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

324that connection (until an explicit or implicit reconnect).

325

326Message passing is ordered but only for a given sender and receiver; no

327ordering guarantees exist between messages sent by different processes. For

328that reason rules \textsc{Expect}, \textsc{ReceiveChan} and \textsc{Spawn-Exec}

329choose the \emph{first} message of a \emph{randomly chosen} sender.

330

331Since the semantics is not type-driven, we represent typed channels simply as

332an identifier with an annotation whether it is the send-end ($\sCid^s$) or the

333receive end ($\sCid^r$) of the channel (rules \textsc{NewChan},

334\textsc{SendChan} and \textsc{ReceiveChan}).

335

336Spawning finally is asynchronous. When process $P$ spawns process $Q$ on node

337$\sNid$ (rule \textsc{Spawn-Async}) a message is sent to node $\sNid$ (which

338may, of course, never arrive). When the remote node receives the message and

339actually spawns $Q$ (rule \textsc{Spawn-Exec}) it sends a message back to $P$

340with $Q$'s process ID. In Cloud Haskell this primitive is called

341\texttt{spawnAsync}, and the Cloud Haskell \texttt{spawn} primitive is defined

342in terms of \texttt{spawnAsync} (we do not consider the synchronous version in

343this document).

344

345\begin{figure}

346\small

347\begin{equation*}

348\frac{

349}{

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

351 {\sQueue}

352 {\sBlacklist}

353 {\sMonitors}

354\rightarrow

355 \sSystem{\sCtxt{P}[ \sReturn \; () ]_{\sPid_\mathit{fr}}}

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

357 {\sBlacklist}

358 {\sMonitors}

359} \textsc{Send}

360\end{equation*}

361%

362\begin{equation*}

363\frac{

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

365}{

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

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

368 {\sBlacklist}

369 {\sMonitors}

370\rightarrow

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

372 {\sQueue, \sQueue'}

373 {\sBlacklist}

374 {\sMonitors}

375} \textsc{Expect}

376\end{equation*}

377%

378\begin{equation*}

379\frac{

380 \sCid \text{ fresh}

381\qquad

382 \sProcessOf(\sCid) = \sPid

383}{

384 \sSystem{\sCtxt{P}[\sNewChan]_\sPid}

385 {\sQueue}

386 {\sBlacklist}

387 {\sMonitors}

388\rightarrow

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

390 {\sQueue}

391 {\sBlacklist}

392 {\sMonitors}

393} \textsc{NewChan}

394\end{equation*}

395

396\begin{equation*}

397\frac{

398}{

399 \sSystem{\sCtxt{P}[ \sSendChan \; \sCid_\mathit{to}^s \; M ]_{\sPid_\mathit{fr}}}

400 {\sQueue}

401 {\sBlacklist}

402 {\sMonitors}

403\rightarrow

404 \sSystem{\sCtxt{P}[ \sReturn \; () ]_{\sPid_\mathit{fr}}}

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

406 {\sBlacklist}

407 {\sMonitors}

408} \textsc{SendChan}

409\end{equation*}

410

411\begin{equation*}

412\frac{

413 \sPid_{\mathit{fr}} \notin \sSenders(\sQueue)

414}{

415 \sSystem{\sCtxt{P}[ \sReceiveChan \; \sCid_\mathit{to}^r ]_{\sPid}}

416 {\sQueue, (\sCid_\mathit{to}, \sPid_\mathit{fr}, M), \sQueue'}

417 {\sBlacklist}

418 {\sMonitors}

419\rightarrow

420 \sSystem{\sCtxt{P}[ \sReturn \; M ]_{\sPid}}

421 {\sQueue, \sQueue'}

422 {\sBlacklist}

423 {\sMonitors}

424} \textsc{ReceiveChan}

425\end{equation*}

426%

427\begin{equation*}

428\frac{

429 \sRef \text{ fresh}

430}{

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

432 {\sQueue}

433 {\sBlacklist}

434 {\sMonitors}

435\rightarrow

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

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

438 {\sBlacklist}

439 {\sMonitors}

440} \textsc{Spawn-Async}

441\end{equation*}

442%

443\begin{equation*}

444\frac{

445 \sPid \notin \sSenders(\sQueue)

446\qquad

447 \sPid' \text{ fresh}

448\qquad

449 \sNodeOf(\sPid') = \sNid

450}{

451 \sSystem{\sProcesses}

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

453 {\sBlacklist}

454 {\sMonitors}

455\rightarrow

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

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

458 {\sBlacklist}

459 {\sMonitors}

460} \textsc{Spawn-Exec}

461\end{equation*}

462%

463where

464%

465\begin{equation*}

466\begin{array}{l@{\;=\;}l@{\hspace{3em}}l}

467 \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)

468&

469 \sQueue, (\sId_\mathit{to}, \sId_\mathit{fr}, M)

470&

471 \text{if } (\sId_\mathit{to}, \sId_\mathit{fr}) \notin \sBlacklist

472\\

473 \sQueue \sExtend{\sBlacklist} (\sId_\mathit{to}, \sId_\mathit{fr}, M)

474&

475 \sQueue

476&

477 \text{otherwise}

478\end{array}

479\end{equation*}

480%

481$(\sExtend{\sBlacklist})$ is only defined for serializable payloads.

482\caption{\label{fig:basic}Basic Primitives}

483\end{figure}

484

485\subsection{Monitoring}

486

487When process $P$ on node $\sNid_P$ wants to monitor process $Q$ on node

488$\sNid_Q$ \emph{both} nodes must be notified. The local node it notified

489immediately, and a message is sent to to the remote node (rules

490\textsc{Mon-Loc} and \textsc{Mon-Rem}). As with all messages, the

491message to the remote node might be lost. When $P$ is disconnected from $Q$ it

492is the responsibility of $P$'s local node $\sNid_P$ to notify $P$

493(\textsc{Mon-Dis}); when $Q$ terminates (\textsc{Mon-Ret}) or crashes

494(\textsc{Mon-Throw}) it is the responsibility of the remote node $\sNid_Q$ to

495notify $P$.

496

497\begin{figure}

498\small

499\begin{equation*}

500\frac{

501 \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})

502\qquad

503 \sNid_\mathit{to} = \sNodeOf(\sId_\mathit{to})

504\qquad

505 \sRef \text{ fresh}

506}{

507\sSystem{\sCtxt{P}[ \sMonitor \; \sId_\mathit{to} ]_{\sPid_\mathit{fr}}}

508 {\sQueue}

509 {\sBlacklist}

510 {\sMonitors}

511\rightarrow

512 \sSystem{\sCtxt{P}[ \sReturn \; \sRef ]_{\sPid_\mathit{fr}}}

513 {\sQueue \sExtend{\sBlacklist} (\sNid_\mathit{to}, \sPid_\mathit{fr}, \sMonitor \; \sRef \; \sId_\mathit{to})}

514 {\sBlacklist}

515 {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{fr}, \sRef)}

516} \textsc{Mon-Loc}

517\end{equation*}

518%

519\begin{equation*}

520\frac{

521 \sPid_\mathit{fr} \notin \sSenders(\sQueue)

522}{

523 \sSystem{\sProcesses}

524 {\sQueue, (\sNid_\mathit{to}, \sPid_\mathit{fr}, \sMonitor \; \sRef \; \sId_\mathit{to}), \sQueue'}

525 {\sBlacklist}

526 {\sMonitors}

527\rightarrow

528 \sSystem{\sProcesses}

529 {\sQueue, \sQueue'}

530 {\sBlacklist}

531 {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{to}, \sRef)}

532} \textsc{Mon-Rem}

533\end{equation*}

534%

535\begin{equation*}

536\frac{

537 \sNid_\mathit{fr} = \sNodeOf(\sPid_\mathit{fr})

538\qquad

539 (\sId_\mathit{to}, \sPid_\mathit{fr}) \in \sBlacklist

540}{

541 \sSystem{\sProcesses}

542 {\sQueue}

543 {\sBlacklist}

544 {\sMonitors, (\sId_\mathit{to}, \sPid_\mathit{fr}, \sNid_\mathit{fr}, \sRef)}

545\rightarrow

546 \sSystem{\sProcesses}

547 {\sQueue, (\sPid_\mathit{fr}, \sId_\mathit{to}, \mathtt{discon} \; \sRef)}

548 {\sBlacklist}

549 {\sMonitors}

550} \textsc{Mon-Dis}

551\end{equation*}

552%

553\begin{equation*}

554\frac{

555 \sNodeOf(\sPid) = \sNid

556}{

557 \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}

558 {\sQueue}

559 {\sBlacklist}

560 {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}

561\rightarrow

562 \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}

563 {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{died} \; \sRef)}

564 {\sBlacklist}

565 {\sMonitors}

566} \textsc{Mon-Ret}

567\end{equation*}

568%

569\begin{equation*}

570\frac{

571 \sNodeOf(\sPid) = \sNid

572}{

573 \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}

574 {\sQueue}

575 {\sBlacklist}

576 {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}

577\rightarrow

578 \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}

579 {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{exc} \; \sRef \; M)}

580 {\sBlacklist}

581 {\sMonitors}

582} \textsc{Mon-Throw}

583\end{equation*}

584%

585\begin{equation*}

586\frac{

587 \sNodeOf(\sPid) = \sNid

588\qquad

589 \sPid \notin \sProcesses

590}{

591 \sSystem{\sProcesses}

592 {\sQueue}

593 {\sBlacklist}

594 {\sMonitors, (\sPid, \sPid', \sNid, \sRef)}

595\rightarrow

596 \sSystem{\sProcesses}

597 {\sQueue \sExtend{\sBlacklist} (\sPid', \sNid, \mathtt{unknown} \; \sRef)}

598 {\sBlacklist}

599 {\sMonitors}

600} \textsc{Mon-Unknown}

601\end{equation*}

602%

603\caption{Monitoring}

604\end{figure}

605

606\subsection{Process Termination}

607

608The rules for normal and abnormal process termination are defined in

609Figure~\ref{fig:termination}. When a process crashes it dies

610silently, unless monitors are setup.

611

612\begin{figure}

613\small

614%

615\begin{equation*}

616\frac{

617 \sNodeOf(\sPid) = \sNid

618\qquad

619 \nexists \; \sPid', \sRef \cdot (\sPid', \sPid, \sNid, \sRef) \in \sMonitors

620}{

621 \sSystem{{(\sReturn \; ())}_\sPid \sPar \sProcesses}

622 {\sQueue}

623 {\sBlacklist}

624 {\sMonitors}

625\rightarrow

626 \sSystem{\sProcesses}

627 {\sQueue}

628 {\sBlacklist}

629 {\sMonitors}

630} \textsc{TermRet}

631\end{equation*}

632%

633\begin{equation*}

634\frac{

635 \sNodeOf(\sPid) = \sNid

636\qquad

637 \nexists \; \sPid', \sRef \cdot (\sPid', \sPid, \sNid, \sRef) \in \sMonitors

638}{

639 \sSystem{{(\sThrow{M})}_\sPid \sPar \sProcesses}

640 {\sQueue}

641 {\sBlacklist}

642 {\sMonitors}

643\rightarrow

644 \sSystem{\sProcesses}

645 {\sQueue}

646 {\sBlacklist}

647 {\sMonitors}

648} \textsc{TermThrow}

649\end{equation*}

650%

651\caption{\label{fig:termination}Process Termination}

652\end{figure}

653

654\section{Open Issues}

655

656\subsection{Ordering of Monitor/Link Notifications}

657

658The semantics as described above, like the original Unified semantics, does not

659guarantee that messages send from process $P$ to process $Q$ (\textsc{Send})

660are ordered with respect to the link or monitor notification sent when process

661$P$ terminates normally or abnormally (\textsc{Mon-Ret}, \textsc{Mon-Throw}). This means that if process $P$ does

662

663\begin{lstlisting}

664receiveWait [

665 match $ \(Reply reply) -> ...

666 , match $ \(ProcessMonitorNotification ..) -> ...

667 ]

668\end{lstlisting}

669

670and process $Q$ does

671

672\begin{lstlisting}

673send pidA (Reply reply)

674// terminate or indeed throw an exception

675\end{lstlisting}

676

677then the semantics does not guarantee that the reply from process $Q$ will

678arrive at process $P$ before the monitor notification; hence, this results in

679an (artificial) race condition in process $P$.

680

681One possible solution is to regard such a link notification as a message from

682process $Q$ to process $P$, which should be ordered along with the other

683messages.

684

685\subsection{Ordering and Typed Channels}

686

687The situation is more tricky still than sketched above because we of typed

688channels. The semantics does not provide ordering guarantees between messages

689sent directly to the process and messages sent on typed channels. That means

690that even if we consider a link or monitor notification as a message sent to

691the process, to be ordered with other messages sent to that process, it is

692still unordered with respect to messages sent on typed channels. This means

693that we have similar race conditions\footnote{Even ignoring the fact that we

694currently don't even provide a way to wait for a message on a typed channel

695\emph{or} a direct message.}

696

697A possible solution is to insist that \emph{all} messages from process $P$ to

698process $Q$ are ordered, no matter how they are sent. From a implementation

699point of view, this would entail the use of a single ordered network connection

700for all messages from $P$ to $Q$, rather than using an ordered connection per

701typed channel plus one for direct messages.

702

703\bibliographystyle{apalike}

704\bibliography{references}

705

706\end{document}