You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In this chapter, we will give the syntax of the \emph{asynchronous} \picalc\ and a discussion of its features.\footnote{Several versions of the \picalc\ have been proposed. We will loosely follow the recent presentation given in \cite{henn07}.} Following this, we will introduce a notion of equivalence of terms in the language. Finally, we will give some semantic reduction rules that provide computational behavior via steps of reduction.
4
+
In this chapter, we will give the syntax of the \emph{asynchronous} \picalc\ and a discussion of its features.We will loosely follow the style of a recent presentation given in \cite{henn07}. Following this, we will introduce a notion of equivalence of terms in the language. Finally, we will give some semantic reduction rules that provide computational behavior via steps of reduction.
5
5
\section{Syntax}\label{spisyntax}
6
-
The terms of the \picalc\ operate on a space of \defmargin{identifiers} $v,w,...$which for the time being will consist of names $n,m,...$ for communication channels, and variables $x,y,...$ which, as we will see below, can refer to channels or to recursive process bodies.
6
+
The terms of the \picalc\ operate on a space of \defmargin{identifiers} which consists of names $a,b,c,...,n,m,o$ for communication channels, and variables $v,w,x$ which can refer to channels, and recursive variables $p,q,r$, explained in more detail below. In general, we will use capital letter to denote a process.
$\sys{M,N} :=$ &$\new{c_1,...,c_n} R_1\comp...\comp R_m$ & $n, m > 0$\\
21
+
\multicolumn{3}{c}{\emph{System}} \\
22
+
& $\new{c_1,...,c_n} R_1\comp...\comp R_m$ & $n, m >=0$\\
23
23
\end{tabular}
24
24
\emph{\caption{Terms in the asynchronous \picalc}\label{apicalcterms}}
25
25
\end{center}
26
26
\end{insettable}
27
-
% \subsection{Names}
28
27
Given two or more processes, we can compose them using the $\comp$ operator, which means that the composed processes will be executed concurrently.
29
28
30
-
We denote the sending of a tuple $V$ over a channel $n$ by \send{n}{V}. Here $V$ is a tuple of identifiers in the form $V=(v_1,...,v_k):k\geq0$. We say that $V$ has \defmargin{arity} $k$. In the case $n=0$ nothing is being transmitted; the communication acts as a \defmargin{handshake} or signal. We will denote this case by \send{n}{}. It is a feature of the language that sending is not a blocking operation -- that is, the process will not wait or depend on the value actually being received or operated on by another process, but will simply terminate after sending the value. Non-blocking sends make our \picalc\ an \emph{asynchronous} language - processes that send values do not wait to sync operation with the processes that consume the values. However, we will show in \refex{exsynchronous} that synchronous behavior can still be modeled in our language.
29
+
We denote the sending of a tuple $\tuple{V}$ over a channel $n$ by \send{n}{\tuple{V}}. Here $\tuple{V}$ is a tuple of identifiers in the form $\tuple{V}=(v_1,...,v_k):k\geq0$. We say that $\tuple{V}$ has \defmargin{arity} $k$. In the case $k=0$ nothing is being transmitted; the communication acts as a \defmargin{handshake} or signal. We will denote this case by \send{n}{}. When $k=0$, only a single value $v_1$ is being transmitted, in which case we write $\send{n}{v_1}$. It is a feature of the language that sending is not a blocking operation -- that is, the process will not wait or depend on the value actually being received or operated on by another process, but will simply terminate after sending the value. Non-blocking sends make our \picalc\ an \emph{asynchronous} language - processes that send values do not wait to sync operation with the processes that consume the values. However, we will show in \refex{exsynchronous} that synchronous behavior can still be modeled in our language.
31
30
32
-
The term \receive{n}{X}$R$ describes a process waiting to receive a tuple along $k$ before continuing with $R$. Here $X$ is a \defmargin[pattern]{patterns}, or a tuple of variables of arity $k$. Patterns allow us to decompose the transmitted tuple into its component values by naming them with $x_1,...,x_k$, which can be referred to in $R$. Thus, in the term
31
+
The term \receive{n}{\tuple{X}}$R$ describes a process waiting to receive a tuple along $k$ before continuing with $R$. Here $\tuple{X}$ is a \defmargin[pattern]{patterns}, or a tuple of variables of arity $k$. Patterns allow us to decompose the transmitted tuple into its component values by naming them with $x_1,...,x_k$, which can be referred to in $R$. Thus, in the term
the names $n_1,n_2,n_3$ are received via $c$ and bound via matching to $x_1,x_2,x_3$ (the use of $x_1,x_2,x_3$ is limited to being within the process $R$). Similarly to sending, the case of arity 0 is denoted \receive{n}{}$R$ -- here $R$ will not happen until a handshake is received on $n$. Notice that in contrast to the case of sending, receiving is a \defmargin{guarded} operation -- that is, the process $R$ will not execute until $X$ has been received via $n$. For example, the term
35
+
the names $n_1,n_2,n_3$ are received via $c$ and bound via matching to $x_1,x_2,x_3$ (the use of $x_1,x_2,x_3$ is limited to being within the process $R$). Similarly to sending, the case of arity 0 is denoted \receive{n}{}$R$ -- here $R$ will not happen until a handshake is received on $n$. Notice that in contrast to the case of sending, receiving is a \defmargin{guarded} operation -- that is, the process $R$ will not execute until $\tuple{X}$ has been received via $n$. For example, the term
Recursion is built into the language using the syntax $\rec{x}B$. The process $\rec{x}B$ itself is referred to by the variable $x$, which is used somewhere in $B$ to express a recursive call. For example, consider the recursive responder term below, which receives a channel $x_1$ via $c$. It then sends a handshake response on $x_1$, while another responder process is run in parallel.
52
+
Recursion is built into the language using the syntax $\rec{x}R$. The process $\rec{x}R$ itself is referred to by the variable $x$, which is used somewhere in $R$ to express a recursive call. For example, consider the recursive responder term below, which receives a channel $x_1$ via $c$. It then sends a handshake response on $x_1$, while another responder process is run in parallel.
54
53
\begin{align}
55
54
\rec{x}\receive{c}{x_1}(\send{x_1}{} \comp x)
56
55
\label{reclistenerterm}
@@ -93,7 +92,7 @@ \subsection{Identifier Substitution and $\alpha$-equivalence}
We denote the substitution of values in $V$ for free identifiers $X$ in $R$ by $R$\subst{V}{X}. Of course, during the course of a substitution, we might inadvertently `capture' a bound term -- suppose for example we wanted to perform the substitution $P_1(c)$\subst{n}{c} where
95
+
We denote the substitution of values in $\tuple{V}$ for free identifiers $V$ in $R$ by $R$\subst{\tuple{V}}{\tuple{X}}. Of course, during the course of a substitution, we might inadvertently `capture' a bound term -- suppose for example we wanted to perform the substitution $P_1(c)$\subst{n}{c} where
We will give a demonstration of how scope extrusion is defined using the rules and axioms of reduction and structural equivalence. Consider the expression
Thanks to the reduction relation's contextuality, we can use (R-COMM) inside of the restriction operator and apply a substitution. Using this in conjunction with the above structural equality and (R-STRUCT), we get:
Then we have shown that if we drop $P(d)$ into the context $\mathbb{C}$ (forming $\mathbb{C}[P(d)]$), it will establish a new channel $c$ and extend its scope using $d$. Hence it is (S-REST-COMP) which allows our system's communication topology to change dynamically via scope extrusion.
185
184
\end{example}
@@ -261,9 +260,9 @@ \section{Action Semantics}
261
260
\end{definition}
262
261
Hence, the transition $P \evolves{a} Q$ indicates that there is an action under which the process P becomes Q. We will refer to $Q$ is the \defmargin{residual} of $P$ after $a$.
263
262
264
-
There are three types of actions that may cause a process to evolve. Note that we will use $\alpha$ to refer to an action of arbitrary type. First, the process might receive a value. That is, a process $P$ can be said to be capable of the transition $P \evolves{\receives{c}{X}} Q$, which is to say $P$ can receive $X$ along $c$ resulting in the residual $Q$.
263
+
There are three types of actions that may cause a process to evolve. Note that we will use $\alpha$ to refer to an action of arbitrary type. First, the process might receive a value. That is, a process $P$ can be said to be capable of the transition $P \evolves{\receives{c}{\tuple{X}}} Q$, which is to say $P$ can receive $\tuple{X}$ along $c$ resulting in the residual $Q$.
265
264
266
-
The second type of action available is sending. Here we need to be a bit more careful. In the case of receiving, the received name is always bound to a new name $X$ - so we needn't worry about issues of scoping. In sending, however, we might be transmitting either a free or a bound name (or a mix of them in a tuple). In the latter case, we need to take account of the fact that the\refmargin{scope extrusion}scope of the name is being extruded to whatever process receives the name. We denote the set of bound names in the send action by $\exports{B}$, and we say that this set of names is \defmargin{exported} by the process. Hence, the transition $P \evolves{\exports{B}\sends{c}{V}} Q$ represents that P can send $V$ over $c$, exporting $\exports{B}$ and resulting in $Q$. For example,
265
+
The second type of action available is sending. Here we need to be a bit more careful. In the case of receiving, the received names are always bound to new names in $\tuple{X}$ - so we needn't worry about issues of scoping. In sending, however, we might be transmitting either free or a bound names, or a mix of them. In the latter case, we need to take account of the fact that the\refmargin{scope extrusion}scope of the name is being extruded to whatever process receives the name. We denote the set of bound names in the send action by $\exports{\tuple{B}}$, and we say that this set of names is \defmargin{exported} by the process. Hence, the transition $P \evolves{\exports{\tuple{B}}\sends{c}{\tuple{V}}} Q$ represents that P can send $\tuple{V}$ over $c$, exporting $\exports{\tuple{B}}$ and resulting in $Q$. For example,
The \emph{action relation} \evolves{} is the smallest relation between processes that satisfy the following rules:\todo{make the arrow for evolution size according to the text above it}
The first of two of these rules simply describe the ability of processes to evolve under input or output. For example, a process $\send{c}{V}\comp P$ will evolve to $stop \comp P \sequiv P$ when it exercises its capability for output on $c$. For a receiving process, evolution under (A-IN) is only possible when the substitution $\subst{V}{X}$ makes sense. That is, $V$ and $X$ must have the same arity\refmargin{arity}and in a typed system we'd want to ensure that their types were compatible\footnote{See \cite{henn07} for a discussion off type systems in the \picalc}.
301
+
The first of two of these rules simply describe the ability of processes to evolve under input or output. For example, a process $\send{c}{\tuple{V}}\comp P$ will evolve to $stop \comp P \sequiv P$ when it exercises its capability for output on $c$. For a receiving process, evolution under (A-IN) is only possible when the substitution $\subst{\tuple{V}}{\tuple{X}}$ makes sense. That is, $\tuple{V}$ and $\tuple{X}$ must have the same arity\refmargin{arity}and in a typed system we'd want to ensure that their types were compatible\footnote{See \cite{henn07} for a discussion off type systems in the \picalc}.
303
302
304
303
Meanwhile, (A-REP), (A-EQ) and (A-NEQ) serve the provide the same interval evolution capabilities as (R-REP), (R-EQ) and (R-NEQ) do in the reduction semantics.
305
304
@@ -317,9 +316,9 @@ \section{Action Semantics}
317
316
\end{tabular}\end{center}
318
317
Above, we have a process sending on $b$ but the scope of $b$ has not actually been extruded (ie by being received on $c$). Hence, we need to be careful not to `capture' a channel like $b$ by allowing exported channels to have the same name as free variables outside the original scope of the process.
319
318
320
-
(A-OPEN) expresses scope extrusion of a name $n$. If we have that a process $P$ can evolves to $P'$ under the action $\exports{B}\sends{c}{V}$, then we can infer that some name $n$, whose scope is now bound to $P$, can be exported in the the action $\exports{n,B}\sends{c}{V}$. Note that $n$ must actually occur in $V$ if it is to be exported; note also that $n$ cannot be $c$ since restricting $n$ (ie $c$) to $P$ would cause a scoping issue that interfered with an outside processes ability to receive on $c$.
319
+
(A-OPEN) expresses scope extrusion of a name $n$. If we have that a process $P$ can evolves to $P'$ under the action $\exports{\tuple{B}}\sends{c}{\tuple{V}}$, then we can infer that some name $n$, whose scope is now bound to $P$, can be exported in the the action $\exports{n,\tuple{B}}\sends{c}{\tuple{V}}$. Note that $n$ must actually occur in $\tuple{V}$ if it is to be exported; note also that $n$ cannot be $c$ since restricting $n$ (ie $c$) to $P$ would cause a scoping issue that interfered with an outside processes ability to receive on $c$.
321
320
322
-
Finally we have (A-COMM), which expresses scope extrusion as well but this time in the context of the internal action $\tau$. According to (A-COMM), $\tau$ is defined as the simultaneous (compositionally) occurrence of an input action and a matching output action on the same channel. In the inferred process $P\comp Q$, no external contributions are needed for evolution, which results in the process $P'\comp Q'$, with the exported names $\exports{B}$ now being scopes to both.
321
+
Finally we have (A-COMM), which expresses scope extrusion as well but this time in the context of the internal action $\tau$. According to (A-COMM), $\tau$ is defined as the simultaneous (compositionally) occurrence of an input action and a matching output action on the same channel. In the inferred process $P\comp Q$, no external contributions are needed for evolution, which results in the process $P'\comp Q'$, with the exported names $\exports{\tuple{B}}$ now being scopes to both.
323
322
324
323
\begin{example}{exsynchronous_actions}
325
324
In \refex{exsynchronous}, we defined a simple process for modeling synchronous sends:
0 commit comments