This spec was inspired by https://github.com/microsoft/CCF/blob/main/tla/consensus/abs.tla.
This spec has a machine-closed fairness constraint, which differs from the the CRDT and
ReplicatedLog examples. However, this spec assumes that a server can consistently read the
state of all other servers, which is clearly not a realistic assumption for a real
distributed system. A real system would rely on some messaging protocol to determine the
lag between servers (compare Raft).
---- MODULE DistributedReplicatedLog ----
EXTENDS Sequences, SequencesExt, Integers, FiniteSets, FiniteSetsExt
CONSTANT Lag, Servers, Values
ASSUME Lag \in Nat /\ IsFiniteSet(Servers)
VARIABLE cLogs
vars == <<cLogs>>
TypeOK ==
/\ cLogs \in [Servers -> Seq(Values)]
Init ==
/\ cLogs \in [Servers -> {<< >>}]
Copy(i) ==
\E j \in Servers:
/\ Len(cLogs[j]) > Len(cLogs[i])
/\ \* Sync some prefix up to prefix = suffix of the unsynced suffix.
LET L == (Len(cLogs[j]) - Len(cLogs[i]))
\* Force to proportionally to the lag L copy more.
\* Lag: 1 -> 0..L, 2 -> 1..L, 3 -> 2..L
IN \E l \in L-1 .. L:
cLogs' = [cLogs EXCEPT ![i] = @ \o SubSeq(cLogs[j], Len(@) + 1, Len(@) + l)]
Extend(i) ==
/\ \A j \in Servers:
Len(cLogs[j]) \leq Len(cLogs[i])
/\ \E s \in BoundedSeq(Values, Lag - Max({Len(cLogs[i]) - Len(cLogs[j]) : j \in Servers})):
cLogs' = [cLogs EXCEPT ![i] = @ \o s]
Next ==
\E i \in Servers:
\/ Copy(i)
\/ Extend(i)
Spec ==
/\ Init
/\ [][Next]_vars
/\ \A s \in Servers: WF_vars(Extend(s)) /\ WF_vars(Copy(s))
----
\* Invariants
Abs(n) ==
IF n < 0 THEN -n ELSE n
BoundedLag ==
\A i, j \in Servers: Abs(Len(cLogs[i]) - Len(cLogs[j])) <= Lag
THEOREM Spec => []BoundedLag
----
\* Liveness
AllExtending ==
\A s \in Servers: []<><<IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs
THEOREM Spec => AllExtending
InSync ==
\* TLC correctly verifies that InSync is not a property of the system because
\* followers are permitted to copy only a prefix of the missing suffix.
\A i, j \in Servers : []<>(cLogs[i] = cLogs[j])
====