Conversation
SamuelSchlesinger
changed the title
ctchou
changed the title
…ta types and prove their relationships
9e9e2e4 to
a0084df
Compare
ctchou
changed the title
|
|
||
| /-- The `happens before` order is the per-session transitive closure of the union of | ||
| the `so` and `vis` orders. -/ | ||
| def hb (a : AbstractExecution Event Operation Value Session) |
There was a problem hiding this comment.
Am I understanding correctly that hb should include session-order edges from all sessions before taking the transitive closure? I wonder if fixing a single session here can miss cycles that alternate between sessions. For example, session edges 0 → 1 and 2 → 3, together with visibility edges 1 → 2 and 3 → 0, seem to form a global cycle even though each individual hb s is acyclic. Would it make sense to use (∃ s, a.so s x y) ∨ a.vis x y as the generating relation instead?
There was a problem hiding this comment.
It is not the job of this definition to impose constraints on either so or vis. It is the job of other, Prop-valued definitions to do that. For example, the next three definitions all have the effect of making "hb" acyclic.
|
|
||
| /-- 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. -/ | ||
| structure OperationContext (Event Operation : Type*) where |
There was a problem hiding this comment.
I may be missing something, but should OperationContext also carry the validity conditions from Definition 4.4: finiteness of events, acyclicity of vis, and a strict total order for ar on those events? My concern is that ReadOnlyOp currently quantifies over arbitrary contexts, so an RDT could distinguish infinite or otherwise invalid contexts. Would it make sense to enforce those conditions here?
There was a problem hiding this comment.
The only way OperationContext will be constructed is via the AbstractExecution.context function below, which inherits the constraints of an AbstractExecution such as acyclicity. Note that the only use of AbstractExecution.context is in RVal, which will ensure that the set of events is finite. (There is another use of AbstractExecution.context in a proof which is unfortunately incorrect and hence will not be formalized. Even there the set of events will be finite.). Note that I do take care in the definition of OperationContext.Equiv below to say that two contexts are equivalent when there is an isomorphism between the two and in ReplicatedDataType to say that its rval function cannot distinguish between equivalent contexts.
There was a problem hiding this comment.
BTW, perhaps we should drop ReadOnlyOp altogether. It is used only in the definition of QuiescentConsistency, which is too weak a consistency condition to be of any practical value. And we know that BasicEventualConsistency => QuiescentConsistency is not true anyway, so no interesting formal theory is lost by dropping QuiescentConsistency.
|
@SamuelSchlesinger Any further comments? Thanks! |
2 participants
This PR formalizes several notions of consistency for replicated data types and proves a hierarchy theorem for them:
Linearizability → SequentialConsistency → CausalConsistency → BasicEventualConsistency
The main reference is the book "Principles of eventual consistency" by Sebastian Burckhardt (which is freely downloadable; see the URL in the reference).
The proofs of
causalVisibility_imp_readMyWritesandcausalVisibility_imp_monotonicReadsare constructed by Claude (Opus 5.5). But all definitions, theorem statements, and comments are human-written.