Semantics for the model with distributed local dataspaces

Here we present the semantics of an implementation-biased model with distributed local dataspaces, henceforth called the local semantics. To formalize that in this model, read statements of different components might observe the write events in different order, we introduce a set $\mbox{\tt ProcIds}$ of process identifiers and extend the semantic primitives of the previous section. In addition to the three fields $st$, $\mbox{\it evs}$ and $\mbox{\it ord}$, we add a fourth $\mbox{\it pid}$ field, which is a function that assigns a process identifier to each event in $\mbox{\it evs}$. This leads to so-called local semantic primitives (denoted $\mbox{\it lsp}$).

For simplicity, we restrict ourselves to so-called non-nested Splice programs, denoted by $S$, where parallel composition does not occur inside sequential composition. In this way, we avoid a complex definition of assigning pids to processes. Consider, e.g., a program of the form $(P_1 ~\vert\vert~P_2) ~;~P_3$. Here it is unclear whether the pid of program $P_3$ should be equal to the pid of $P_1$, $P_2$ or none of them.

The semantics of a non-nested Splice program $S$, given an initial state $s$, to a set of local semantic primitives, denoted $\mbox{\tt {SemL}$($}S\mbox{$)$} (s)$, is obtained by adapting the semantics of the previous section as follows.

• The local semantics of the three atomic statements ${\tt Skip}$, ${\tt Write}(e)$ and ${\tt Read}(x, q)$ is basically equal to the global semantics extended with a $\mbox{\it pid}$ field. The value of this field is not restricted and may take any possible value, e.g.:

  $\mbox{\tt {SemL}$($}{\tt Write}(e)\mbox{$)$}(s)$
           $=~\big\{ (s, \{ E \}, \emptyset, p) \mid E \in \mbox{\tt Events}$
           $~\wedge~p: \{ E \} \rightarrow \mbox{\tt ProcIds} \wedge \mbox{\it act}(E) = {\tt W}(e(s)) \big\}$.

• For sequential composition we require, in addition to the global semantics, that the events of both components be assigned the same pid.
• The semantics of parallel composition extends the global semantics by requiring that the events of both components are assigned different pids.
• The new semantics of ${\tt Close}$ becomes more complex, as explained below.
  $$\begin{eqnarray*} & & \rule{-0.62cm}{0cm}\mbox{\tt {SemL}$($}{\tt Close}(S)\mbo... ... ~\wedge~\mbox{\it act}(E_1) = {\tt W}(d)]]\big]\big]\big]\big\} \end{eqnarray*}$$
  
  
  
  
  
  Observe that the events of ${\tt Close}(S)$ are assigned the same pid as in $S$ (line 5) and that the main difference with the semantics of the previous section concerns the order on the events. The requirement of a single, total order on all events is replaced by two conditions:
  1. There should be a global total order $\prec _1$ on the read events which extends $\mbox{\it ord}$ but does not order write events before others (lines 6 to 9).
  2. For each process identifier $p$ there exists a local total order $\prec _2$ which extends $\prec _1$ (lines 10 and 11) and is such that each read event with process identifier $p$ has a preceding (w.r.t. $\prec _2$) write event with the same value (lines 12 to 15). This local order allows write actions to be ordered differently for each process, modelling the non-atomicity of write actions.
  To understand the reason for the complexity of this definition, it might be instructive to mention that in an early attempt we did not include the first condition and used only the second condition, with $\prec _2$ extending $\mbox{\it ord}$. Then the proof of equivalence in PVS failed and we found that the definition was wrong. Consider, for instance,
  $$\begin{eqnarray*} & & {\tt Close}\big(({\tt Read}(x, x=0) ~;~{\tt Write}(1))\ru... ...\qquad~~\vert\vert~~({\tt Read}(y, y=1) ~;~{\tt Write}(0))\big). \end{eqnarray*}$$
  
  
  
  
  
  As we have shown in PVS, the global semantics of this program leads to the empty set. This conforms to the intuition that for both processes the read statement blocks, i.e. the complete program leads to deadlock. Our erroneous local semantics however did not yield the empty set because for each process we could order the two read events differently.