66dded2 · distributed-process

git.iko.soy/distributed-process

on master help sign in

Clean up what's there.

66dded2Edsko de Vries14 years ago

doc/reconnect/blacklist.tex+62−80

compare with master

unifiedsplit

@@ -15,13 +15,18 @@

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

16\newcommand{\sReconnect}{\mathtt{reconnect}}

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

19+

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

21+

18−\newcommand{\sPar}{\mathrel{{\parallel}_P}}

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

19\newcommand{\sParN}{\mathrel{{\parallel}_N}}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -101,33 +106,12 @@ We define an evaluation context as usual (TODO: catch?)

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

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

102\end{equation*}

107\end{equation*}

103

108

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}

127

110

128At the Cloud Haskell level we assume that \emph{nodes} get disconnected, not

111At the Cloud Haskell level we assume that \emph{nodes} get disconnected, not

112+individual processes. \emph{Reconnecting} however is on a per process basis. To

129−individual processes. To formalize this, let $\overline{\sNid}$ be the smallest

113+formalize this, let $\overline{\sNid}$ be the smallest set, given a set of

130−set, given a set of processes $\sProcesses$, such that

114+processes $\sProcesses$, such that

131%

115%

132\begin{equation*}

116\begin{equation*}

133\frac{

117\frac{

@@ -175,6 +159,26 @@ However, connections to and from nodes can be implicitly reconnected:

175} \textsc{Recon-Fr}

159} \textsc{Recon-Fr}

176\end{equation*}

160\end{equation*}

177

161

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+

178\subsection{Process rules}

182\subsection{Process rules}

179

183

180\subsubsection{Sending}

184\subsubsection{Sending}

@@ -183,33 +187,21 @@ If the communication is blacklisted the send is a no-op.

183

187

184\begin{equation*}

188\begin{equation*}

185\frac{

189\frac{

186−(\mathit{to}, \mathit{fr}) \notin \sBlacklist

187}{

190}{

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+ }

189 {\sQueue}

195 {\sQueue}

190 {\sBlacklist}

196 {\sBlacklist}

191\rightarrow

197\rightarrow

192− \sSystem{\sCtxt{P}[ \sReturn \; () ]_\mathit{fr}}

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

193− {\sQueue, (\mathit{to}, \mathit{fr}, V)}

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

194 {\sBlacklist}

200 {\sBlacklist}

195−} \textsc{Send-Ok}

201+} \textsc{Send}

196\end{equation*}

202\end{equation*}

197

203

198−\begin{equation*}

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

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

213

205

214\subsubsection{Receiving}

206\subsubsection{Receiving}

215

207

@@ -217,13 +209,13 @@ We return the \emph{first} message of a randomly chosen sender.

217

209

218\begin{equation*}

210\begin{equation*}

219\frac{

211\frac{

220− \mathit{fr} \notin \sSenders(\sQueue)

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

221}{

213}{

222− \sSystem{\sCtxt{P}[ \sExpect ]_\mathit{fr}}

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

223− {\sQueue, (\mathit{to}, \mathit{fr}, V), \sQueue'}

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

224 {\sBlacklist}

216 {\sBlacklist}

225\rightarrow

217\rightarrow

226− \sSystem{\sCtxt{P}[ \sReturn \; V ]_\mathit{fr}}

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

227 {\sQueue, \sQueue'}

219 {\sQueue, \sQueue'}

228 {\sBlacklist}

220 {\sBlacklist}

229} \textsc{Expect}

221} \textsc{Expect}

@@ -231,33 +223,37 @@ We return the \emph{first} message of a randomly chosen sender.

231

223

232\subsubsection{Spawning}

224\subsubsection{Spawning}

233

225

226+Spawning is asynchronous

227+

234\begin{equation*}

228\begin{equation*}

235\frac{

229\frac{

236− \sPid' \text{ fresh} \qquad

230+ \text{\sRef fresh}

237− (\sNid, \sPid) \notin \sBlacklist

238}{

231}{

239− \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid[\sProcesses]_\sNid}

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

240 {\sQueue}

233 {\sQueue}

241 {\sBlacklist}

234 {\sBlacklist}

242\rightarrow

235\rightarrow

243− \sSystem{\sCtxt{P}[ \sReturn \; (\sJust{\sPid'}) ]_\sPid[\sProcesses \sPar M_{\sPid'}]_\sNid}

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

244− {\sQueue}

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

245 {\sBlacklist}

238 {\sBlacklist}

246−} \textsc{Spawn-Ok}

239+} \textsc{Spawn-Async}

247\end{equation*}

240\end{equation*}

248

241

242+

249\begin{equation*}

243\begin{equation*}

250\frac{

244\frac{

251− (\sNid, \sPid) \in \sBlacklist

245+ \sPid \notin \sSenders(\sQueue)

246+\qquad

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

252}{

248}{

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

249+ \sSystem{\sProcesses}

254− {\sQueue}

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

255 {\sBlacklist}

251 {\sBlacklist}

256−\rightarrow

252+\rightarrow

257− \sSystem{\sCtxt{P}[ \sReturn \; \sNothing ]_\sPid}

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

258− {\sQueue}

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

259 {\sBlacklist}

255 {\sBlacklist}

260−} \textsc{Spawn-No}

256+} \textsc{Spawn-Reply}

261\end{equation*}

257\end{equation*}

262

258

263\subsubsection{Reconnect}

259\subsubsection{Reconnect}

@@ -265,28 +261,14 @@ We return the \emph{first} message of a randomly chosen sender.

265\begin{equation*}

261\begin{equation*}

266\frac{

262\frac{

267}{

263}{

268− \sSystem{\sCtxt{P}[ \sReconnect \; \mathit{id} ]_\sPid}

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

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}

283 {\sQueue}

265 {\sQueue}

284 {\sBlacklist}

266 {\sBlacklist}

285\rightarrow

267\rightarrow

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

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

287 {\sQueue}

269 {\sQueue}

288− {\sBlacklist}

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

289−} \textsc{Reconnect-No}

271+} \textsc{Reconnect}

290\end{equation*}

272\end{equation*}

291

273

292\subsubsection{Administration}

274\subsubsection{Administration}