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:
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), might get the value , since it is possible that arrives much later in the local dataspace of the third process.
In the conceptual model with a single global dataspace, however, never becomes since should be available in the dataspace before can be written, so the third process can read or .
In the conceptual model with a global dataspace, value is written when is already available in the dataspace and, as in the previous example, cannot get the value . The implementation with local dataspaces allows an execution where becomes ; then the value 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 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.
In the implementation model with local dataspaces, may get values respectively, since in the dataspace of the second process may arrive before is executed and may arrive afterwards (but before execution of the statement ), whereas in the dataspace of the third process may arrive before 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 returns value then the value 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.