@@ -0,0 +1,255 @@
1+\documentclass{article}
2+\usepackage[margin=2.5cm]{geometry}
3+\usepackage{amsmath, amssymb}
4+\usepackage{mathpazo, times}
5+
6+\newcommand{\sLam}[2]{\lambda {#1} \cdot {#2}}
7+\newcommand{\sApp}[2]{{#1} {#2}}
8+\newcommand{\sBind}[2]{{#1} \mathrel{\texttt{>}\!\!\texttt{>}\!\texttt{=}} {#2}}
9+\newcommand{\sReturn}{\mathtt{return}}
10+
11+\newcommand{\sExpect}{\mathtt{expect}}
12+\newcommand{\sSend}{\mathtt{send}}
13+\newcommand{\sSpawn}{\mathtt{spawn}}
14+\newcommand{\sLink}{\mathtt{link}}
15+\newcommand{\sThrow}{\mathtt{throw}}
16+\newcommand{\sReconnect}{\mathtt{reconnect}}
17+
18+\newcommand{\sParP}{\mathrel{{\parallel}_P}}
19+\newcommand{\sParN}{\mathrel{{\parallel}_N}}
20+\newcommand{\sProc}[2]{{#1}_{#2}}
21+\newcommand{\sPid}{\ensuremath{\mathit{pid}}}
22+\newcommand{\sNid}{\ensuremath{\mathit{nid}}}
23+\newcommand{\sLinks}{\ensuremath{\mathit{links}}}
24+\newcommand{\sNode}[3]{\left[{#1} ; {#2}\right]_{#3}}
25+\newcommand{\sSystem}[3]{\left\langle #1 ; #2 ; #3 \right\rangle}
26+\newcommand{\sNodes}{\mathcal{N}}
27+\newcommand{\sQueue}{\mathcal{Q}}
28+\newcommand{\sProcesses}{\mathcal{P}}
29+\newcommand{\sBlacklist}{\mathcal{B}}
30+
31+\newcommand{\sJust}[1]{\mathtt{Just} \; {#1}}
32+\newcommand{\sNothing}{\mathtt{Nothing}}
33+
34+\newcommand{\sCtxt}[1]{\mathbb{#1}}
35+
36+\newcommand{\sSenders}{\mathit{senders}}
37+
38+\newcommand{\OR}{\mathrel{|}}
39+
40+
41+\begin{document}
42+
43+\title{Cloud Haskell Semantics}
44+\author{Edsko de Vries, Well-Typed LLP}
45+\date{\today}
46+
47+\maketitle
48+
49+\section{Syntax}
50+
51+\subsection{Terms}
52+
53+\begin{equation*}
54+\begin{array}{ll@{\;::=\;}l}
55+\text{value} & V & \sLam{x}{M} \OR
56+ \sExpect \OR
57+ \sSend \; \sPid \; V \OR
58+ \sSpawn \; \sNid \; V \OR
59+ \sReturn \; M
60+\\
61+\text{term} & M, N & \sApp{M}{N} \OR
62+ \sBind{M}{N}
63+\end{array}
64+\end{equation*}
65+
66+\subsection{Processes, Nodes, Systems}
67+
68+A \emph{process} $\sProc{M}{\sPid}$ is a pair of a term $M$ and a process ID $\sPid$.
69+A \emph{node}
70+ $$\sNode{\sProcesses}
71+ {\sLinks}
72+ {\sNid}$$
73+is a tuple consisting of a set of
74+processes $\sProcesses$, sometimes written as
75+ $$\sProc{M}{\sPid} \sParP \cdots \sParP \sProc{N}{\sPid'}$$
76+together with a set \sLinks{} of pairs of process IDs and a node ID \sNid.
77+A \emph{system}
78+ $\sSystem{\sNodes}{\sQueue}{\sBlacklist}$
79+finally is a tuple containing a set $\sNodes$ of nodes, sometimes written
80+ $$\sNode{\sProcesses}{\sLinks}{\sNid}
81+ \sParN
82+ \cdots
83+ \sParN
84+ \sNode{\sProcesses'}{\sLinks'}{\sNid'}
85+ $$
86+a \emph{system queue} $\sQueue$, and a \emph{blacklist} $\sBlacklist$. The
87+system queue is a set of triples $(\mathit{to}, \mathit{from},
88+\mathit{message})$ of messages that have been sent but not yet processed. The
89+blacklist is a set of pairs $(\mathit{to}, \mathit{from})$. Once a pair
90+$(\mathit{to}, \mathit{from})$ has been blacklisted messages from
91+$\mathit{from}$ to $\mathit{to}$ will never be delivered ($\mathit{to}$ and
92+$\mathit{from}$ are node or process identifiers).
93+
94+\section{Semantics}
95+
96+\subsection{Contexts}
97+
98+We define an evaluation context as usual (TODO: catch?)
99+
100+\begin{equation*}
101+\sCtxt{E} ::= [] \OR \sBind{\sCtxt{E}}{M}
102+\end{equation*}
103+
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} \sParP \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} \sParP []}{\sLinks}{\sNid} \sParN \sNodes \\[1em]
119+\OR &
120+ \sNode{\sProc{\sCtxt{E}}{pid} \sParP \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}
127+
128+\begin{equation*}
129+\frac{
130+}{
131+ \sSystem{\sNodes}{\sQueue}{\sBlacklist}
132+\rightarrow
133+ \sSystem{\sNodes}{\sQueue}{\sBlacklist, (\mathit{to}, \mathit{from})}
134+} \textsc{Disconnect}
135+\end{equation*}
136+
137+\subsection{Process rules}
138+
139+\subsubsection{Sending}
140+
141+If the communication is blacklisted the send is a no-op.
142+
143+\begin{equation*}
144+\frac{
145+(\mathit{to}, \mathit{from}) \notin \sBlacklist
146+}{
147+ \sSystem{\sCtxt{P}[ \sSend \; \mathit{to} \; V ]_\mathit{from}}
148+ {\sQueue}
149+ {\sBlacklist}
150+\rightarrow
151+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_\mathit{from}}
152+ {\sQueue, (\mathit{to}, \mathit{from}, V)}
153+ {\sBlacklist}
154+} \textsc{Send-Ok}
155+\end{equation*}
156+
157+\begin{equation*}
158+\frac{
159+(\mathit{to}, \mathit{from}) \in \sBlacklist
160+}{
161+ \sSystem{\sCtxt{P}[ \sSend \; \mathit{to} \; V ]_\mathit{from}}
162+ {\sQueue}
163+ {\sBlacklist}
164+\rightarrow
165+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_\mathit{from}}
166+ {\sQueue}
167+ {\sBlacklist}
168+} \textsc{Send-No}
169+\end{equation*}
170+
171+TODO: this allows to send functions
172+
173+\subsubsection{Receiving}
174+
175+We return the \emph{first} message of a randomly chosen sender.
176+
177+\begin{equation*}
178+\frac{
179+ \mathit{from} \notin \sSenders(\sQueue)
180+}{
181+ \sSystem{\sCtxt{P}[ \sExpect ]_\mathit{from}}
182+ {\sQueue, (\mathit{to}, \mathit{from}, V), \sQueue'}
183+ {\sBlacklist}
184+\rightarrow
185+ \sSystem{\sCtxt{P}[ \sReturn \; V ]_\mathit{from}}
186+ {\sQueue, \sQueue'}
187+ {\sBlacklist}
188+} \textsc{Expect}
189+\end{equation*}
190+
191+\subsubsection{Spawning}
192+
193+\begin{equation*}
194+\frac{
195+ \sPid' \text{ fresh} \qquad
196+ (\sNid, \sPid) \notin \sBlacklist
197+}{
198+ \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid[\sProcesses]_\sNid}
199+ {\sQueue}
200+ {\sBlacklist}
201+\rightarrow
202+ \sSystem{\sCtxt{P}[ \sReturn \; (\sJust{\sPid'}) ]_\sPid[\sProcesses \sParP M_{\sPid'}]_\sNid}
203+ {\sQueue}
204+ {\sBlacklist}
205+} \textsc{Spawn-Ok}
206+\end{equation*}
207+
208+\begin{equation*}
209+\frac{
210+ (\sNid, \sPid) \in \sBlacklist
211+}{
212+ \sSystem{\sCtxt{P}[ \sSpawn \; \sNid \; M ]_\sPid}
213+ {\sQueue}
214+ {\sBlacklist}
215+\rightarrow
216+ \sSystem{\sCtxt{P}[ \sReturn \; \sNothing ]_\sPid}
217+ {\sQueue}
218+ {\sBlacklist}
219+} \textsc{Spawn-No}
220+\end{equation*}
221+
222+\subsubsection{Reconnect}
223+
224+\begin{equation*}
225+\frac{
226+}{
227+ \sSystem{\sCtxt{P}[ \sReconnect \; \mathit{id} ]_\sPid}
228+ {\sQueue}
229+ {\sBlacklist, (\mathit{id}, \sPid), \sBlacklist'}
230+\rightarrow
231+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_\sPid}
232+ {\sQueue}
233+ {\sBlacklist, \sBlacklist'}
234+} \textsc{Reconnect-Ok}
235+\end{equation*}
236+
237+\begin{equation*}
238+\frac{
239+ (\mathit{id}, \sPid) \notin \sBlacklist
240+}{
241+ \sSystem{\sCtxt{P}[ \sReconnect \; \mathit{id} ]_\sPid}
242+ {\sQueue}
243+ {\sBlacklist}
244+\rightarrow
245+ \sSystem{\sCtxt{P}[ \sReturn \; () ]_\sPid}
246+ {\sQueue}
247+ {\sBlacklist}
248+} \textsc{Reconnect-No}
249+\end{equation*}
250+
251+\subsubsection{Administration}
252+
253+TODO: bind, pure evaluation, maybe exception handling
254+
255+\end{document}