Is this a legal Bolt-On execution?

BO.md

Is this a legal Bolton Execution ?

Consider the following execution history for a single value, last-writer-wins key-value store:

P_0  wrt (x,1) --> wrt (y,1) --> wrt (z,1)


P_1                                   rd z=>1 --> rd y_2 --> rd t=>2 --> rd x=>1


P_2     wrt (y,2) --> wrt (x,2) --> wrt (t,2)

Should this history be accepted by Bolt-On? Based on the description in the paper and a "partial read" of the implementation, we believe that this history is admitted by Bolt on. In fact, we have found out that this history is reproducible in our idealized Bolt-On model/abstract machine (under a potential causal consistency setting), if you allow the eventual consistent store (ECDS) to deliver messages out of order.

Consider the following idealized Bolt-On execution trace for P_2:

// The initial cut is L = {

 1 deliver y_2 ==> E[y] = y_2
 2 deliver x_2 ==> E[x] = x_2
 3 deliver z_1 ==> E[z] = z_1
 4 cover x_2   ==> L[x] = E [x] = x_2
 5 cover y_2   ==> L[y] = E [y] = y_2
 6 cover z_1   ==> L[z] = E [z] = z_1

// L = { x_2 ; y_2 ; z_1 ; t_0 } is a causal cut

 7 read z ==> z_1
 8 read y ==> y_2
 9 deliver t_2 ==> E[t] = t_2
10 cover t_2 ==> E[t] = t_2

// L = { x_2 ; y_2 ; z_1 ; t_2 } is a causal cut

11 read t ==> t_2
12 deliver x_1 ==> E[x] = x_1
13 cover x_1 ==> L[x] = E[x] = x_1

// L = { x_1 ; y_2 ; z_1 ; t_2 } is a causal cut

14 cover x_1 ==> L[x] = E[x] = x_1
15 read x_1 ==> x_1

Here write w_1 and read w_1are atomic operations writing/reading from a write in the local shim store L, deliver w_1 denotes the underlying ECDS propagation of the write events - \ie. deliver x_2 updates the ECDS store writing x_2 to E[x]-, and cover w_1 updates the value of the local store from the underlying ECDS if the write event w_1 forms a cover/ preserves the causal cut invariant on L.

Lines 1 - 3 represent the underlying weak store delivery of the write events. Then, lines 4 - 6 represent the update of the causal cover from E forced by the read on z on line 7: we are assuming a pessimistic path execution of BoltOn here. Notice that the writes are applied in causal order, preserving the causal cut invariant.

Then, reading y on line 8 does not require to update the cut, and we continue with the delivery of t_2 and its respective covering and reading of t for the rd t_2 event on line 11.

Now, consider the delivery of x_1 on line 12. If we assume that x_2 happens before x_1 in real time, TS (x_1) < TS (x_2), then x_1 will be accepted by the ECDS store. Then, on line 13, since x_1 -/-> x_2, we will succeed to cover x_1, and again, since TS (x_1) < TS (x_2) the local store implementation[*] will effectively write x_1 to the local store, and return it in the read event in line 15.

Thus, unless our abstract machine is missing some some details about the underlying ECDS delivery, such execution is/should be possible in BoltOn.

Are we missing something out?

What's the big deal?

The history above is (weak) causal consistent[2, 1]. Taking the causal relation CO to be the usual happens before relation by Lamport - i.e the transitive union of PO (--> above) and the omitted read-from RF arrows - the resulting order is not acyclic and it does justify each read value.

This history is not, however, a causal (memory) consistent history[3, 1]: there is no serialization of the operations in the history in which a read event returns the last written value on that variable. This follows from the fact that the read event rd y=>2 forces wrt (y,1) to be ordered in the serialization before wrt (y,2), and the other read rd x=>1 forces wrt (x,2) to be ordered before wrt (x,1), and these two orderings are not possible at the same time.

Thus it seems that this is not a CM execution and, therefore it cannot be a convergent causal consistent/causal+ execution[4]? This history does not represent a valid execution of COPS[4] or EIGER[5], for instance. These systems ensure that a version is successfully replicated after all their dependencies has been written.

If this history is accepted by BoltOn then... what does it say about BoltOn consistency? Does this mean that BoltOn consistency under a potential causality setting, yields a consistency criterion which is weaker than causal+? Maybe something in between weak CC and causal+?

Comments and References.

[*] Respectively, the assertion on line 28 and the guard on line 63 of ConcurrentLocalStore.java on BoltOn's implementation on git-hub.

[1] Boujjani, Enea and Hamza - On Verifying Causal Consistency. POPL 17.

presents a formalization of CC, CM, and CV causal consistency in which histories are CC/CM/CV consistent if the absence of certain bad patterns can be proven.

CC: is the weaker notion of causal consistency characterized by Lamport's CO (happens-before) relation CO = (PO \cup RF)^t, i.e. the transitive closure of the union of the read from relation RF and the session/program order (PO), together with the absence of 4 bad patterns (including acyclicity of the causal order CO).

CM: is the notion of causal consistency introduced by the seminal casual memory paper[2]. It strengthens CC by requiring that sites don't forget the ordering imposed by reads in our PO (session) past. Thus, in this formalization, a history is CM if it is CC, and for each event the arbitration HB_o relation is not acyclic for every event o in the history, and other pattern related to reads of initial writes. HB_o is the (smallest) inductive relation defined as follow

    a -->HB_o b <->

       \/ (CO Inclusion)  a -->CO b  /\ a -->CO o /\ b-->CO o

       \/ (Transitivity Closure) \exists c-->CO o, a-->HB_o c /\ c-->HB_o b

       \/ (Write-Order) \exists r -->PO o, a-->HB_o r /\ b-->RF 	

CV: The CV formalization strengthens causal consistency with a convergence requirement. Given a conflict relation

w_x --> CF w_x' <-> \exists r st.  w_x -->CO r /\ w_x'-->RF r

We say a history is CV if (CO \cup CF) is acyclic.

Under this model, a Causal Plus history[4], should be a both a CM and CV history.

Moreover, the history above it is not CV either, as we have a path

wrt x_1 -->CO wrt y_1 -->CF wrt y_2 -->CO wrt x_2 -->CF wrt x_1

[2] L. Lamport. Time, clocks, and the ordering of events in a distributed system.Comm. ACM , 21(7), 1978.

[3] Ahamad et. al.. Causal memory: Definitions, implementation, and programming. Distributed Computing , 9(1), 1995.

This papers present a notion of causal consistency based for causal memory, which is the basis of the Causal+ definition in [4].

[4] W. Lloyd et. al. Don’t settle for eventual: scalable causal consistency for wide-area storage with COPS. SOSP 2011.

[5] W. Lloyd, M. J. Freedman, M. Kaminsky, and D. G. Andersen. Stronger semantics for low-latency geo-replicated storage. NSDI 2013.