next up previous
Next: Equivalence of the two Up: Semantical Aspects of an Previous: Semantics for the model


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.


next up previous
Next: Equivalence of the two Up: Semantical Aspects of an Previous: Semantics for the model
Roel Bloo 1999-11-26