A Causal+ history which should not be?

CP.md

A Causal+ history which should not be?

Consider the following execution history for a single value, last-writer-wins (LWW) 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)

This history 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.

Our question is then, whether the history above should be a valid Causal+ history? Our initial understanding from reading the COPS paper is that causal+ builds upon causal (memory) consistency by adding the convergent handlers. If this intuition is correct, the history above should not be accepted by the definition of Causal+.[*]

However, after reading the technical definitions in the COPS paper's Appendix, we are not longer sure that is the case. In particular, it is not clear to us which write events must appear in the conflict-free put set for each site: Are we required to include only those that have been read? Or, on the contrary, a put set must include all write events in a read event's causal past?

In the first case, I could ignore just ignore the events from the handler threads and define the conflict-free put set for P_1 as:

CF_1 = { wrt (x,1); wrt (y,2); wrt (z,1); wrt (t,2) }

Then, the following serialization of P_1 and CF_1 respects the casual order CO:

S_1 = wrt (y,2) ; wrt (x,1) ; wrt (z,1) ; rd z=>1 ; rd y=>2 ; 
	  wrt (t,2) ; rd t=>2 ; rd x=>1

In the second case, let us consider a LWW-like handler h defined as:

h (wrt (x,1), wrt (x,2)) = h (wrt (x,2), wrt (x,1)) = wrt (x,1)

h (wrt (y,1), wrt (y,2)) = h (wrt (y,2), wrt (y,1)) = wrt (y,2)

Of course, such a handler is not a standard LWW handler (say, one based on global time-stamps), and it does not preserve PO/CO orders between writes to different keys. But, it still does satisfy the required properties of associativity and commutativity for a convergent handler.

Then, I can construct the following conflict-free put set:

	CF_2 = { wrt (y,2) ; wrt (x,2) ; h (wrt (x,1), wrt (x,2)) ; 
		    h (wrt (y,1) , wrt (y,2)) ; wrt (z,1) ; wrt (t,2) }

This put set is conflict free and, moreover, the following serialization of P_1 with CF_2 respects the causal order CO:

S_2 = wrt (y,2) ; wrt (x,2) ; h(x_1, x_2) ; h(y_1, y_2) ; 
	  wrt (z,1) ; rd z=>1; rd y=>2; wrt (t,2) ; rd t=>2 ; rd x=>1 

Hence, our confusion... Is our reasoning flawed? Are we missing out on some assumption about how put sets should be defined? Or some restriction on convergent handlers?

Or, on the contrary, is it the case that this history should be accepted - and what was wrong was our intuition that Causal+ entails causal memory[2].

Comments and References.

[*] We do not expect this history to represent a valid execution of COPS or EIGER, for instance. As the paper says, COPS ensures that a version is replicated after all their dependencies has been written. In fact, the history above is also not accepted by the formalization of an EIGER-like, one hop KVS in CHAPAR[4].

[1] A. Boujjani, C. Enea and J. Hamza. On Verifying Causal Consistency (POPL 17).

This paper presents a formalization of CC, CM, and CV causal consistency in which histories are CC/CM/CV consistent iff the histories can be shown to avoid certain bad patterns. In this paper's convention, CC, CM, and CV are 3 different flavours of causal consistency:

CC: is the weaker notion of causal consistency characterized by Lamport's (happens-before) relation:

   CO = (PO \cup RF)^t

That is, the causal order is the transitive closure of the union of the read from relation RF and the session/program order PO. CO is subjected to the absence of 4 bad patterns (including acyclicity of the causal order CO).

CM: is the (stronger) 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 a the HB_o relation is not acyclic for every event o in the history.

Given an event o HB_o is defined as the (smallest) inductive relation:

    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 	

Given this definition, we construct the HB_o order for an event o in P_2 in the history above, such that rd x=>1 ---><=PO o:

1. wrt (x,1) -->HB_o wrt y _1, by CO inclusion.

2. wrt (y,1) -->HB_o wrt (y,2), by Write-Order since we have wrt (y,1) -->HB_o rd y_2 and also wrt (y,2) -->RF rd y_2.

3. wrt (y,2) -->HB_o wrt (x,2), by CO inclusion.

4. wrt (x,2) -->HB_o wrt (x,1) by Write-Order since we have wrt x_2 -->HB_o rd x=>1 and also wrt (x,1) -->RF rd x=>1.

Then, we have a cycle in HB_o:

	wrt (x,1) -->HB_o wrt (y,1) -->HB_o wrt (y,2) -->HB_o wrt (x,2) -->HB_o wrt (x,1)

CV: strengthens causal consistency with a convergence requirement. Given a conflict relation CF defined as:

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

we say a history is CV if it CC and (CO \cup CF) is acyclic.

Under this formalization's definitions, a Causal+ history should be both a CM and CV history. Notice that, moreover, the history above it is also not CV, as we would have a cyclyc 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.

[4] M. Lesani, C. J. Bell, and A. Chlipala. CHAPAR: certified causally consistent distributed key-value stores. (POPL 2016).