Documentation

Cslib.Computability.Distributed.Consistency.Hierarchy

Consistency hierarchy #

We prove a number of results about the various notions of consistency for replicated data types. In paricular, we prove that:

Linearizability → SequentialConsistency → CausalConsistency → BasicEventualConsistency

Our proofs follow closely the proofs of Lemma 5.1 and Proposition 5.1 of [Bur14].

References #

Principles of Eventual Consistency

instance Cslib.DistributedConsistency.isTrans_ar {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} {a : AbstractExecution Event Operation Value Session} :

IsTrans Event a.ar

theorem Cslib.DistributedConsistency.so_iff_se_rb {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} {a : AbstractExecution Event Operation Value Session} (s : Session) (x y : Event) :

a.so s x y ↔ a.se x = s ∧ a.se y = s ∧ a.rb x y

theorem Cslib.DistributedConsistency.so_le_rb {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} {a : AbstractExecution Event Operation Value Session} (s : Session) :

a.so s ≤ a.rb

theorem Cslib.DistributedConsistency.se_rval_eq_none {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} {a : AbstractExecution Event Operation Value Session} {s : Session} {x : Event} (h1 : a.se x = s) (h2 : a.rval x = none) :

{y : Event | a.se y = s} = {y : Event | a.se y = s ∧ a.rb y x} ∪ {x}

theorem Cslib.DistributedConsistency.singleOrder_vis_ar_rval_ne_none {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} {a : AbstractExecution Event Operation Value Session} (h : a.SingleOrder) (x y : Event) :

(a.vis x y → a.ar x y) ∧ (a.ar x y → a.rval x ≠ none → a.vis x y)

theorem Cslib.DistributedConsistency.singleOrder_realTime_imp_readMyWrites {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} {a : AbstractExecution Event Operation Value Session} (h1 : a.SingleOrder) (h2 : a.RealTime) :

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

a.SequentialConsistency d

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

a.hb ≤ Relation.TransGen a.vis

theorem Cslib.DistributedConsistency.singleOrder_readMyWrites_imp_causalArbitration {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} {a : AbstractExecution Event Operation Value Session} (h1 : a.SingleOrder) (h2 : a.ReadMyWrites) :

a.CausalArbitration

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

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

a.MonotonicReads

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

a.NoCircularCausality

theorem Cslib.DistributedConsistency.singleOrder_readMyWrites_imp_causalVisibility {Event : Type u_1} {Operation : Type u_2} {Value : Type u_3} {Session : Type u_4} {a : AbstractExecution Event Operation Value Session} (h1 : a.SingleOrder) (h2 : a.ReadMyWrites) :

a.CausalVisibility

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

a.EventualVisibility

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

a.CausalConsistency d

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

a.BasicEventualConsistency d