Consistency specifications

We formalize several notions of consistency for replicated data types defined in [Bur14], listed below in decreasing order of strength:

• Linearizability,
• Sequential consistency.
• Causal consistency,
• Basic eventual consistency,

We follow [Bur14] closely in the formalization except for one detail: instead of using an equivalence relation "same-session" to model the notion of sessions, we use a map se : Event → Session and regard two events x and y to belong to the same session iff se x = se y. These two approaches are clearly equivalent and se is chosen because it is easier to work with.

NOTE: We left out the definition of quiescent consistency, for two reasons:

• Quiescent consistency is too weak a notion to be practically useful (see the remark on page 44 of [Bur14]).
• We found during the process of formalization that the only theoretic result about quiescent consistency in [Bur14], that it is implied by causal consistency, is incorrect given the definitions in [Bur14].

References

• Principles of Eventual Consistency

structure Cslib.DistributedConsistency.BaseHistory (Event : Type u_5) (Operation : Type u_6) (Value : Type u_7) (Session : Type u_8) : Type (max (max (max u_5 u_6) u_7) u_8)

BaseHistory is an auxiliary definition containing all data fields of History below.

• op : Event → Operation

  op assigns each event its operation.

• se : Event → Session

  se assigns each event its session.

• rval : Event → Option Value

  rval assigns each event its return value, where none indicates that the event never returns.

• rb : Event → Event → Prop

  rb is the "returns before" order on events.

def Cslib.DistributedConsistency.BaseHistory.so {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (h : BaseHistory Event Operation Value Session) (s : Session) : Event → Event → Prop

so (for "session order") is rb restricted to a single session.

Equations

• h.so s = Relation.restrict h.rb {x : Event | h.se x = s}

structure Cslib.DistributedConsistency.History (Event : Type u_5) (Operation : Type u_6) (Value : Type u_7) (Session : Type u_8) extends Cslib.DistributedConsistency.BaseHistory Event Operation Value Session : Type (max (max (max u_5 u_6) u_7) u_8)

History extends BaseHistory with well-formedness conditions.

• op : Event → Operation
• se : Event → Session
• rval : Event → Option Value
• rb : Event → Event → Prop
• rb_strict_order : IsStrictOrder Event self.rb

  rb is a strict order on events (namely, it is irreflexive and transitive).

• rb_pred_finite (x : Event) : (Relation.predecessors self.rb x).Finite

  Each event has only a finite number of predecessors in the rb order.

• rb_interval_order : Relation.IsIntervalOrder self.rb

  The rb order is an interval order.

• rb_rval_ne_none (x y : Event) : self.rb x y → self.rval x ≠ none

  If an event x returns before another event y, then x cannot return none.

• so_strict_total_order (s : Session) : IsStrictTotalOrder ↑{x : Event | self.se x = s} fun (a b : ↑{x : Event | self.se x = s}) => self.so s ↑a ↑b

  The so order is a strict total order of the events of each session.

structure Cslib.DistributedConsistency.AbstractExecution (Event : Type u_5) (Operation : Type u_6) (Value : Type u_7) (Session : Type u_8) extends Cslib.DistributedConsistency.History Event Operation Value Session : Type (max (max (max u_5 u_6) u_7) u_8)

AbstractExecution extends History with two more orders and additional well-formedness conditions.

• op : Event → Operation
• se : Event → Session
• rval : Event → Option Value
• rb : Event → Event → Prop
• rb_strict_order : IsStrictOrder Event self.rb
• rb_pred_finite (x : Event) : (Relation.predecessors self.rb x).Finite
• rb_interval_order : Relation.IsIntervalOrder self.rb
• rb_rval_ne_none (x y : Event) : self.rb x y → self.rval x ≠ none
• so_strict_total_order (s : Session) : IsStrictTotalOrder ↑{x : Event | self.se x = s} fun (a b : ↑{x : Event | self.se x = s}) => self.so s ↑a ↑b
• vis : Event → Event → Prop

  vis x y means that x is visible to y.

• ar : Event → Event → Prop

  ar is the arbitration order of the whole system.

• vis_acyclic : Relation.Acyclic self.vis

  The visibility order vis is acyclic.

• vis_pred_finite (x : Event) : (Relation.predecessors self.vis x).Finite

  Each event has only a finite number of predecessors in the vis order.

• ar_strict_total_order : IsStrictTotalOrder Event self.ar

  The arbitration order is a strict total order of all events.

def Cslib.DistributedConsistency.History.Satisfies {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (h : History Event Operation Value Session) (p : AbstractExecution Event Operation Value Session → Prop) : Prop

A history satisfies a predicte p on abstract executions iff it can be extended to an abstract execution satisfying p.

Equations

• h.Satisfies p = ∃ (a : Cslib.DistributedConsistency.AbstractExecution Event Operation Value Session), a.toHistory = h ∧ p a

def Cslib.DistributedConsistency.AbstractExecution.ReadMyWrites {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) : Prop

ReadMyWrites says that if two events are ordered by so, then they are also ordered by vis.

Equations

• a.ReadMyWrites = ∀ (s : Session), a.so s ≤ a.vis

def Cslib.DistributedConsistency.AbstractExecution.MonotonicReads {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) : Prop

MonotonicReads says that if x is visible to y, then x is also visible to all successors of y under the so order.

Equations

• a.MonotonicReads = ∀ (s : Session) (x y z : Event), a.vis x y → a.so s y z → a.vis x z

def Cslib.DistributedConsistency.AbstractExecution.ConsistentPrefix {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) : Prop

ConsistentPrefix says that if x is visible to y in a different session, then all predecessors of x in the arbitration order are also visible to y.

Equations

• a.ConsistentPrefix = ∀ (x y : Event), a.se x ≠ a.se y → a.vis x y → ∀ (z : Event), a.ar z x → a.vis z y

def Cslib.DistributedConsistency.AbstractExecution.hb {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) : Event → Event → Prop

The happens before order is transitive closure of the union of the vis order and the so s orders for all sessions s.

Equations

• a.hb = Relation.TransGen fun (x y : Event) => a.vis x y ∨ ∃ (s : Session), a.so s x y

def Cslib.DistributedConsistency.AbstractExecution.NoCircularCausality {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) : Prop

NoCircularCausality says that the hb order is acyclic.

Equations

• a.NoCircularCausality = Relation.Acyclic a.hb

def Cslib.DistributedConsistency.AbstractExecution.CausalArbitration {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) : Prop

CausalArbitration says that if two events are ordered by hb, then they are also ordered by ar.

Equations

• a.CausalArbitration = (a.hb ≤ a.ar)

def Cslib.DistributedConsistency.AbstractExecution.CausalVisibility {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) : Prop

CausalVisibility says that if two events are ordered by hb, then they are also ordered by vis.

Equations

• a.CausalVisibility = (a.hb ≤ a.vis)

def Cslib.DistributedConsistency.AbstractExecution.Causality {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) : Prop

Causality is the conjunction of CausalArbitration and CausalVisibility.

Equations

• a.Causality = (a.CausalArbitration ∧ a.CausalVisibility)

def Cslib.DistributedConsistency.AbstractExecution.SingleOrder {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) : Prop

SingleOrder says that vis and ar are the same order except that there may be a set of events which never returns and are not visible.

Equations

• a.SingleOrder = ∃ (xs : Set Event), (∀ (x : Event), x ∈ xs → a.rval x = none) ∧ ∀ (x y : Event), a.vis x y ↔ a.ar x y ∧ ¬x ∈ xs

def Cslib.DistributedConsistency.AbstractExecution.RealTime {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) : Prop

RealTime says that if two events are ordered by rb, then they are also ordered by ar.

Equations

• a.RealTime = (a.rb ≤ a.ar)

def Cslib.DistributedConsistency.AbstractExecution.nonVisibleEvents {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) (x : Event) (s : Session) : Set Event

a.nonVisibleEvents x s is the set of events in session s which returns after x but does not see x.

Equations

• a.nonVisibleEvents x s = {y : Event | a.se y = s ∧ a.rb x y ∧ ¬a.vis x y}

def Cslib.DistributedConsistency.AbstractExecution.EventualVisibility {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) : Prop

EventualVisibility says that for any event x and any session s, there can be at most finitely many events in s that return after x and do not see x.

Equations

• a.EventualVisibility = ∀ (x : Event) (s : Session), (a.nonVisibleEvents x s).Finite

structure Cslib.DistributedConsistency.OperationContext (Event : Type u_5) (Operation : Type u_6) : Type (max u_5 u_6)

An OperationContext is the data used by a replicated data type to determine the return value of an operation. It is an abstraction of the notion of states.

• events : Set Event

  The set of events in the operation context.

• op : Event → Operation

  Operation labeling of events.

• vis : Event → Event → Prop

  Visibility order.

• ar : Event → Event → Prop

  Arbitration order.

structure Cslib.DistributedConsistency.OperationContext.Equiv {Event : Type u_1} {Operation : Type u_2} (c1 c2 : OperationContext Event Operation) : Type u_1

The notion of equivalence on OperationContext, which is essentially an isomorphism that ignores the identities of events and the behavior of op, vis, and ar outside the set of events in the operation context.

• equiv : { x : Event // x ∈ c1.events } ≃ { x : Event // x ∈ c2.events }

  A bijection from c1's events to c2's events.

• op_equiv (x : { x : Event // x ∈ c1.events }) : c1.op ↑x = c2.op ↑(self.equiv x)

  op is preserved by the bijection.

• vis_equiv (x y : { x : Event // x ∈ c1.events }) : c1.vis ↑x ↑y ↔ c2.vis ↑(self.equiv x) ↑(self.equiv y)

  vis is preserved by the bijection.

• ar_equiv (x y : { x : Event // x ∈ c1.events }) : c1.ar ↑x ↑y ↔ c2.ar ↑(self.equiv x) ↑(self.equiv y)

  ar is preserved by the bijection.

structure Cslib.DistributedConsistency.ReplicatedDataType (Event : Type u_5) (Operation : Type u_6) (Value : Type u_7) : Type (max (max u_5 u_6) u_7)

The notion of a replicated data type.

• rval : Operation → OperationContext Event Operation → Option Value

  rval takes an operation and an operation context and returns a value.

• rval_equiv (o : Operation) (c1 c2 : OperationContext Event Operation) : ∀ (x : c1.Equiv c2), self.rval o c1 = self.rval o c2

  For any operation, rval must returns the same value on equivalent operation contexts.

def Cslib.DistributedConsistency.AbstractExecution.context {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) (xs : Set Event) : OperationContext Event Operation

a.context xs is the operation context obtained by restricting a to xs.

Equations

• a.context xs = { events := xs, op := a.op, vis := a.vis, ar := a.ar }

def Cslib.DistributedConsistency.AbstractExecution.RVal {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) (d : ReplicatedDataType Event Operation Value) : Prop

a.RVal d says that the return value of any event in the abstract execution a is the same as the value returned by the replicated data type d in the context consisting of the predecessors of the event.

Equations

• a.RVal d = ∀ (x : Event), a.rval x = d.rval (a.op x) (a.context (Relation.predecessors a.vis x))

def Cslib.DistributedConsistency.AbstractExecution.Linearizability {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) (d : ReplicatedDataType Event Operation Value) : Prop

Linearizability is the conjunction of SingleOrder, RealTime, and RVal.

Equations

• a.Linearizability d = (a.SingleOrder ∧ a.RealTime ∧ a.RVal d)

def Cslib.DistributedConsistency.AbstractExecution.SequentialConsistency {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) (d : ReplicatedDataType Event Operation Value) : Prop

SequentialConsistency is the conjunction of SingleOrder, ReadMyWrites, and RVal.

Equations

• a.SequentialConsistency d = (a.SingleOrder ∧ a.ReadMyWrites ∧ a.RVal d)

def Cslib.DistributedConsistency.AbstractExecution.CausalConsistency {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) (d : ReplicatedDataType Event Operation Value) : Prop

CausalConsistency is the conjunction of EventualVisibility, Causality, and RVal.

Equations

• a.CausalConsistency d = (a.EventualVisibility ∧ a.Causality ∧ a.RVal d)

def Cslib.DistributedConsistency.AbstractExecution.BasicEventualConsistency {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} (a : AbstractExecution Event Operation Value Session) (d : ReplicatedDataType Event Operation Value) : Prop

BasicEventualConsistency is the conjunction of EventualVisibility, NoCircularCausality, and RVal.

Equations

• a.BasicEventualConsistency d = (a.EventualVisibility ∧ a.NoCircularCausality ∧ a.RVal d)