- Conflict-Free Replicated Data Types
- Instead of shared central state, shared state in distributed replicas
- Fast, not blocking local reads
- Fast, not blocking local writes - temporary inconsistencies between replicas
- Conflict-free replica synchronisation at arbitrary times - eventual consistency
- No central state - no single point of failure
- Replacement for RPC-like APIs
- Advatageous even when single replica
- Irrefutable writes - accepting writes as undeniable facts
- Append-only writes - data can only "grow"
- Transaction-less - consequence of the above
- Contradictory writes - possible but explicitly modeled
- New ACID
- Let
a
,b
, andc
be replicas and+
be a replicat "merge" operation - Associativity -
a + (b + c) == (a + b) + c
, handles arbitrary grouping of merges - Commutativity -
a + b == b + a
- handles out-of-order merges - Idempotence -
a + a == a
- handles duplicate merges - Distributed - remote replicas merges
- Let
- Instead of shared central state, shared state in distributed replicas
- Maths behind CRDTs
- Type - a collection of values
- Partial order - values of type can be compared with
+>
(a kind of "greater or equal")a +> a
- reflexivitya +> b, b +> a => a == b
- antisymmetrya +> b +> c => a +> c
- transitivity- note that there might be that neither
a +> b
norb +> a
,a
andb
not comparable, that's why "partial"
- Lattice
- Algebra
(S, \/, /\)
whereS
is a type\/
(join) is a binary operator- closed under
S
- ifa
andb
belongs toS
thena \/ b
also belongs toS
- associative -
a \/ (b \/ c) = (a \/ b) \/ c
- commutative -
a \/ b = b \/ a
- idempotent -
a \/ a = a
a \/ b +> a
- closed under
/\
(meet) is a binary operator- closed under
S
- associative -
a /\ (b /\ c) = (a /\ b) /\ c
- commutative -
a /\ b = b /\ a
- idempotent -
a /\ a = a
a +> a /\ b
- closed under
- Algebra
- Bounded lattice
- Algebra
(S, /\, \/, 0, 1)
0
(bottom) is a value belonging toS
- for all
a
inS
,0 \/ a == a == a \/ 0
- for all
1
(top) is a value belonging toS
- for all
a
inS
,1 /\ a == a == a /\ 1
- for all
- Algebra
- Finite lattice
- Lattice
(S, \/, /\)
whereS
is finite
- Lattice
- Distributive lattice
a /\ (b \/ c) = (a /\ b) \/ (a \/ c)
- Dual 1.
- (Bounded) join semilattices examples
GrowingSet
is BJS- Set that can only grow in time
S
is a set of values of arbitrary type\/
is sum0
is an empty set
ShrinkingSet
is JS - set that can only shrink in timeShrinkingSet
is BJS if we know the largest possible setIncreasingValue
is JS - value that can only increase in timeIncreasingValue
is BJS if we know minimal possible valueDecreasingValue
is JS - value that can only decrease in timeDecreasingValue
is BJS if we know maximal possible valuePredAnd a
is BJS - functionsa -> Bool
,Bool
s andedPredOr a
is BJS - functionsa -> Bool
,Bool
s ored- Time-stamped value is JS - pairs
(a, Time)
(under assumptions about clocks synchronization)
- Higher-kinded (bounded) join semilattices
- If
v
is a JS thenGrowingMap k s
is BJSGrowingMap
is a map where we can only add entries or join existing ones
- If
e
is a JS thenGrowingList w
is BJSGrowingList
is a list where we can only append values or join existing ones
- If
a
andb
are BJSs than(a, b)
is BJS - If
a
andb
are BJSs thanEither a b
is BJS (what are\/
and0
?) - If
a
is JS thanMaybe a
is BJS (equivalent toEither () a
) - We can combine the above:
GrowingMap A (GrowingMap B ((GrowingList (DecreasingValue C), (Either (IncreasingValue D) (GrowingSet E)))))
is a BJS as long asinstance Bounded C
so that we know maximum value ofC
instance Bounded D
so that we know minimum value ofD
instance Ord E
so that we can compare values ofE
s
- If
- Modeling contradictions
- Assume a value that we expect to be set at some time and should stay the same since then, what if we get different values?
Same a
is a (union) type that can have valueUnknown
,Unambiguous a
orAmbiguous
Same a
is BJS as long as we can comparea
s -instance Eq a
- Note we can get the same
Unambiguous a
multiple times without contradiction (what are\/
and0
?)
- Order in join semilattice
- If
a \/ b == a
then we saya +> b
,b <+ a
,a
is greater or equal tob
,b
is lesser or equal toa
- In particular, as
a \/ a == a
because of idempotence, indeed,a
is greater or equal to itself anda
is lesser or equal to itself, thereforea
is equal to itself. - Intuitively, when
a +> b
then joininga
withb
will not introduce anything new thana
,a
already containsb
,a
has already containedb
- Checking if
a +> b
is a kind of read operation: it checkes whetherb
is already contained ina
- Example:
isPersonOlderThan :: Person -> Age -> GrowingMap Person (Increasing Age) -> Bool isPersonOlderThan person age personMap = personMap +> singleton person (Increasing age)
- If
- Mappings between join semilattices
- Let's analyse more useful read operation:
personsAge :: Person -> GrowingMap Person (Increasing Age) -> Maybe (Increasing Age) personsAge personMap person = lookup person personMap
- Notice this is a function from one BJS to another BJS
- Left-hand side BJS will only grow, so will the right-hand side BJS
- As left-hand side BJS grows, so will the right-hand side BJS - it's a monotonic function
- Monotonic mappings between JSs are a category
- If
f (a \/ b) = f a \/ f b
andf 0 = 0
thenf
it's not only monotonic but homomorphic- Homomorphic mappings between JSs are a category
- Propagators concept
- References
- Introduction to Lattices and Order, 2nd edition, 2012, B. A. Davey, H. A. Priestley
- Edward Kmett: Propagators - Boston Haskell
- Edward Kmett: Propagators - YOW! Lambda Jam 2016
- John Mumm: A CRDT Primer: Defanging Order Theory
- Marc Shapiro: Strong Eventual Consistency and Conflict-free Replicated Data Types
-
Notifications
You must be signed in to change notification settings - Fork 0
License
erykciepiela/semilattice
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
About
No description, website, or topics provided.
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published