Semantics for the model with a global dataspace

In this section we define the semantics of our coordination language under the assumption that there is a single global dataspace. We refer to it as the global semantics.

The values of internal variables of a process are represented by a state, which is a function from variables to ${\tt Data}$. Furthermore, let $\mbox{\tt Events}$ be a set of events. The meaning of a program $P$, given an initial state representing the values of the variables at the start of the program, is a set of semantic primitives. Each semantic primitive corresponds to a terminated execution. For simplicity we do not model blocking or infinite computations. Semantic primitives, denoted $sp$, are records in PVS with three fields:

• $st$: the final state of the program, representing the situation after the execution.
• $\mbox{\it evs}$: a subset of $\mbox{\tt Events}$ containing those events that occur during the execution of $P$. An event represents the occurrence of an action. Let $\mbox{\it act}$ be a global function that yields for each event in the set $\mbox{\tt Events}$ the corresponding action. Here we have actions of the form ${\tt R}(d)$ and ${\tt W}(d)$ denoting the reading and writing, resp., of data element $d$. Note that if we replace $\mbox{\it evs}$ and $\mbox{\it act}$ by a multiset of actions, then we cannot order events with the same action and hence it is not possible to distinguish them.
• $\mbox{\it ord}$: a strict (irreflexive & transitive) partial order on the set of events ( $\mbox{\it evs}$). Intuitively, we have $\mbox{\it ord}(E_1,E_2)$ iff $E_1$ is a read event occurring before $E_2$; if $E_2$ is a read event then anything available in the dataspace at the moment of execution of $E_1$ will also be available at the moment of execution of $E_2$, and if $E_2$ is a write event then the value written by $E_2$ can not be available in the dataspace at the moment of execution of $E_1$ (unless there is another write action writing the same value).

Next we present the formal semantics of the language constructs in the setting of the conceptual model with a single global dataspace. This is done by defining a function $\mbox{$[\![\:$}\cdots\mbox{$\:]\!]$}$ which maps a program P, given an initial state s, to a set of semantic primitives, denoted $\mbox{$[\![\:$}P\mbox{$\:]\!]$} (s)$. Here, a semantic primitive, represented in PVS by a record, is denoted by a triple $(s,\mbox{\it eset},\prec )$, where $s$ is a state, $\mbox{\it eset}$ a set of events and $\prec$ a strict partial order on $\mbox{\it eset}$. The functions $st, \mbox{\it evs}$, and $\mbox{\it ord}$ are used to access the first, second and third field of these triples.

$$\begin{eqnarray*} & & \mbox{$[\![\:$}{\tt Skip}\mbox{$\:]\!]$} (s) = \{ (s, \emptyset, \emptyset)\}\rule{10cm}{0cm} \end{eqnarray*}$$

The skip statement performs no visible actions. Hence, the set of events (and its order) are empty, and the final state is equal to the initial state $s$.

$$\begin{eqnarray*} & & \mbox{$[\![\:$}{\tt Write}(e)\mbox{$\:]\!]$} (s)\rule{10c... ...\mbox{\tt Events}\wedge \mbox{\it act}(E) = {\tt W}(e(s)) \big\} \end{eqnarray*}$$

A write statement ${\tt Write}(e)$ performs a single event $E$ that corresponds to a write action with the value of $e$ evaluated in the state $s$. The initial state $s$ is unaffected.

$$\begin{eqnarray*} & & \mbox{$[\![\:$}{\tt Read}(x, q)\mbox{$\:]\!]$} (s)\rule{1... ...ata}\wedge q(d, s) \wedge \mbox{\it act}(E) = {\tt R}(d) \big\} \end{eqnarray*}$$

To understand the semantics of statement ${\tt Read}(x, q)$, it is important to recall that we aim at a denotational, i.e. compositional, framework. This means that the semantics of a read statement should allow the combination with any context, where in principle every possible data item could be written. So we have to take an arbitrary environment into account. This is done by including semantic primitives for all data items $d \in {\tt Data}$ that satisfy the query in the initial state (i.e., $q(d, s)$ holds). So the semantics includes all possibilities and only at the point of applying a closure operation we decide about the actual values read. We use $s[x \mapsto d]$ to denote the state that equals $s$ except that the value of $x$ has been replaced by $d$.

$$\begin{eqnarray*} & & \mbox{$[\![\:$}P_1 ~;~P_2\mbox{$\:]\!]$} (s)\rule{10cm}{0... ...{\it sp}_2)(E_1, E_2) \vee {\tt R?}(E_1)\big) \big] \big] \big\} \end{eqnarray*}$$

Here ${\tt R?}(E_1)$ is an abbreviation for $\exists d [ \mbox{\it act}(E_1) = {\tt R}(d)]$. The meaning of $P_1 ~;~P_2$ expresses that the final state of this construct is produced by $P_2$, starting in the final state of $P_1$. The latter executes from the original initial state $s$. We require that the event sets of the two components be different. This requirement can always be met simply by renaming common events, assuming that there are sufficiently many events to make this possible. The events of $P_1; P_2$ are those performed by $P_1$ or $P_2$. The order on the resulting event set respects the orders of $P_1$ and $P_2$; additionally, the order requires that each read action by $P_1$ occurs before any event of $P_2$.

$$\begin{eqnarray*} & & \mbox{$[\![\:$}P_1 ~\vert\vert~P_2\mbox{$\:]\!]$}(s)\rule... ...ox{\it sp}_1) \vee \mbox{\it ord}(\mbox{\it sp}_2) \big]\big\} \end{eqnarray*}$$

In $P_1 ~\vert\vert~P_2$ both processes start from the initial state $s$ and, since there are no shared variables, the final state of the parallel construct is obtained by simply combining the two final states. Similar to sequential composition, the event sets of $P_1$ and $P_2$ are assumed to be disjoint, and the events of $P_1 ~\vert\vert~P_2$ are those that occur in $P_1$ or $P_2$. No additional ordering is imposed by the parallel composition.

$$\begin{eqnarray*} & & \mbox{$[\![\:$}{\tt Close}(P)\mbox{$\:]\!]$}(s)\rule{10cm... ...ec} ~\wedge~\mbox{\it act}(E_1) = {\tt W}(d)]]\big]\big]\big\} \end{eqnarray*}$$

The semantics of the ${\tt Close}$ operation formalizes the relation between read and write actions. Recall that the semantics of a read statement includes all possible data items and only at closure it can be checked which data items are actually available. This is done by imposing a strict total order on the events of $P$, extending the existing order $\mbox{\it ord}$, such that each read action ${\tt R}(d)$ is preceded by a corresponding write action ${\tt W}(d)$. Only the semantic primitives from $P$ for which such a total order exists are retained in the semantics of ${\tt Close}( P )$.

Examples We present a few simple examples to illustrate the semantics. In the following program, the variable $x$ might become $0$ or $1$, which is reflected in its denotational semantics.

$$\begin{eqnarray*} & & \mbox{$[\![\:$}{\tt Close}\big(({\tt Write}(0) ~;~{\tt Wr... ...1) = {\tt W}(0) \wedge \mbox{\it act}(E_2) = {\tt W}(1) ]\big\} \end{eqnarray*}$$

The following example illustrates how read actions are delayed until the requested data item arrives in the shared dataspace. Let $P$ be the program

$$({\tt Write}(0) ~;~{\tt Write}(1)) ~\vert\vert~({\tt Read}(x, x>0) ~;~{\tt Read}(y, y<x)).$$

Then

$$\begin{eqnarray*} & & \mbox{$[\![\:$}{\tt Close}(P)\mbox{$\:]\!]$}(s) \rule{10c... ..._1) = {\tt W}(0) \wedge \mbox{\it act}(E_2) = {\tt W}(1) ]\big\} \end{eqnarray*}$$