Examples of non-equivalent variations

Note that the goal above is not trivial, since there are many variations of Splice-like languages where the meaning differs, depending on the dataspace model. We present a few cases where the equivalence does not hold:

• Suppose a read statement returns the set of all data items that satisfy the query. Moreover, assume read statements are blocking, so the result of a read is never the empty set. Consider the following program, where $X$ and $Y$ range over sets of data items.

  ${\tt Write}(0)~~\vert\vert~~{\tt Read}(Y, \mbox{\tt true})$
  $\qquad~~\vert\vert~~({\tt Read}(X, \mbox{\tt true}) ~;~{\tt Write}(1))$

  In this and the following examples in this section, we assume that all programs are ``closed'' in the sense that there are no other write actions than the ones shown - this is formalized later. In the distributed implementation (where write actions are distributed to the local dataspaces non-atomically), $Y$ might get the value $\{ 1 \}$, since it is possible that $0$ arrives much later in the local dataspace of the third process.

  In the conceptual model with a single global dataspace, however, $Y$ never becomes $\{ 1 \}$ since $0$ should be available in the dataspace before $1$ can be written, so the third process can read $\{ 0 \}$ or $\{ 0, 1 \}$.

• Now again assume that a read statement returns the set of all data items that satisfy the query, but suppose read statements are non-blocking (returning the empty set if there are no data items satisfying the query). First observe that the program above yields the same results in both models; $X$ might get the values $\emptyset$ or $\{ 0 \}$ (i.e. item $1$ is never available for the first read) and $Y$ can read any combination of $0$ and $1$ (i.e. $\emptyset$, $\{ 0 \}$, $\{ 1 \}$, or $\{ 0, 1 \}$). However, then the following program shows a difference.

  ${\tt Write}(0)~~\vert\vert~~{\tt Read}(Y, \mbox{\tt true})$
  $\qquad~~\vert\vert~~\big({\tt Read}(X, \mbox{\tt true}) ~;~ {\bf if} \ X \neq \emptyset \ {\bf then} \ {\tt Write}(1) \ {\bf fi} \big)$

  In the conceptual model with a global dataspace, value $1$ is written when $0$ is already available in the dataspace and, as in the previous example, $Y$ cannot get the value $\{ 1 \}$. The implementation with local dataspaces allows an execution where $Y$ becomes $\{ 1 \}$; then the value $0$ becomes available in the dataspace of the second process much earlier than in that of the third process, where it arrives even after the value $1$ written by the second process.

  The problem here is that in this example we have constructs by which we can observe whether a data item is present or not. This can be exploited to observe the difference between the conceptual global dataspace model and the implementation with distributed dataspaces.

• As another example, suppose read statements are blocking and return a single data item that satisfies the query. If queries are restricted to predicates on state-variables and data, this is the language for which we show equivalence of the two semantics. However, the equivalence does not hold if the queries are predicates on the dataspace. Consider, for instance, the possibility of reading minimal or maximal values (e.g., ${\tt Read}(x, \mbox{\tt min})$ yields the minimal value available in the (local) dataspace at the moment), and the following program.

  $( {\tt Write}(0) ~;~{\tt Write}(1))$
  $\qquad~~\vert\vert~~({\tt Read}(x, \mbox{\tt min}) ~;~{\tt Read}(y, \mbox{\tt min}))$
  $\qquad~~\vert\vert~~({\tt Read}(u, \mbox{\tt max}) ~;~{\tt Read}(v, \mbox{\tt max}))$

  In the implementation model with local dataspaces, $x, y, u,v$ may get values $1,0,0,1$ respectively, since in the dataspace of the second process $1$ may arrive before ${\tt Read}(x, \mbox{\tt min})$ is executed and $0$ may arrive afterwards (but before execution of the statement ${\tt Read}(y, \mbox{\tt min})$), whereas in the dataspace of the third process $0$ may arrive before $1$ does. This is of course impossible in the conceptual model with one global dataspace. Observe that this example again depends on the possibility of testing for absence of data (if ${\tt Read}(x, \mbox{\tt min})$ returns value $1$ then the value $0$ must be absent in the dataspace).

  Note that if read statements are non-blocking and return an error value when no data item satisfies the query (and otherwise a single data item satisfying the query), then we can also observe whether a data item is present, even for queries that are restricted to predicates on data only.