Skip to content

Commit d97b414

Browse files
lemmylemmy
committed
Add DistributedReplicatedLog example.
The property `IsSync` in `DistributedReplicatedLog.tla` does not hold; the node with the longest log may forever append a value before the other nodes can catch up. TLC finds the following (valid) counterexample (for three nodes): ```tla Error: Temporal properties were violated. Error: The following behavior constitutes a counter-example: State 1: <Initial predicate> cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>) State 2: <Extend(n2) line 35, col 5 to line 38, col 49 of module DistributedReplicatedLog> cLogs = (n1 :> <<>> @@ n2 :> <<v>> @@ n3 :> <<>>) State 3: <Extend(n2) line 35, col 5 to line 38, col 49 of module DistributedReplicatedLog> cLogs = (n1 :> <<>> @@ n2 :> <<v, v>> @@ n3 :> <<>>) State 4: <Copy(n3) line 26, col 9 to line 32, col 96 of module DistributedReplicatedLog> cLogs = (n1 :> <<>> @@ n2 :> <<v, v>> @@ n3 :> <<v>>) Back to state 2: <Copy(n1) line 26, col 9 to line 32, col 96 of module DistributedReplicatedLog> ``` Signed-off-by: Markus Alexander Kuppe <[email protected]>
1 parent b76867a commit d97b414

File tree

6 files changed

+153
-2
lines changed

6 files changed

+153
-2
lines changed

‎README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ Here is a list of specs included in this repository, with links to the relevant
6464
| [Software-Defined Perimeter](specifications/SDP_Verification) | Luming Dong, Zhi Niu | | | | ✔ | |
6565
| [Simplified Fast Paxos](specifications/SimplifiedFastPaxos) | Lim Ngian Xin Terry, Gaurav Gandhi | | | | ✔ | |
6666
| [Checkpoint Coordination](specifications/CheckpointCoordination) | Andrew Helwer | | | | ✔ | |
67-
| [Finitizing Monotonic Systems](specifications/FiniteMonotonic) | Andrew Helwer | | | | ✔ | |
67+
| [Finitizing Monotonic Systems](specifications/FiniteMonotonic) | Andrew Helwer, Stephan Merz, Markus Kuppe | | ✔ | | ✔ | |
6868
| [Multi-Car Elevator System](specifications/MultiCarElevator) | Andrew Helwer | | | | ✔ | |
6969
| [Nano Blockchain Protocol](specifications/NanoBlockchain) | Andrew Helwer | | | | ✔ | |
7070
| [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain | | | | ✔ | |

‎manifest.json

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -623,6 +623,34 @@
623623
"tlaLanguageVersion": 2,
624624
"features": [],
625625
"models": []
626+
},
627+
{
628+
"path": "specifications/FiniteMonotonic/MCDistributedReplicatedLog.tla",
629+
"communityDependencies": ["FiniteSetsExt"],
630+
"tlaLanguageVersion": 2,
631+
"features": [],
632+
"models": [
633+
{
634+
"path": "specifications/FiniteMonotonic/MCDistributedReplicatedLog.cfg",
635+
"runtime": "00:00:05",
636+
"size": "small",
637+
"mode": "exhaustive search",
638+
"features": [
639+
"liveness", "view"
640+
],
641+
"result": "success",
642+
"distinctStates": 37,
643+
"totalStates": 271,
644+
"stateDepth": 4
645+
}
646+
]
647+
},
648+
{
649+
"path": "specifications/FiniteMonotonic/DistributedReplicatedLog.tla",
650+
"communityDependencies": ["SequencesExt", "FiniteSetsExt"],
651+
"tlaLanguageVersion": 2,
652+
"features": [],
653+
"models": []
626654
}
627655
]
628656
},

‎specifications/FiniteMonotonic/DistributedReplicatedLog.tla

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
This spec was inspired by https://github.com/microsoft/CCF/blob/main/tla/consensus/abs.tla.
2+
3+
This spec has a machine-closed fairness constraint, which differs from the the CRDT and
4+
ReplicatedLog examples. However, this spec assumes that a server can consistently read the
5+
state of all other servers, which is clearly not a realistic assumption for a real
6+
distributed system. A real system would rely on some messaging protocol to determine the
7+
lag between servers (compare Raft).
8+
9+
---- MODULE DistributedReplicatedLog ----
10+
EXTENDS Sequences, SequencesExt, Integers, FiniteSets, FiniteSetsExt
11+
12+
CONSTANT Lag, Servers, Values
13+
ASSUME Lag \in Nat /\ IsFiniteSet(Servers)
14+
15+
VARIABLE cLogs
16+
vars == <<cLogs>>
17+
18+
TypeOK ==
19+
/\ cLogs \in [Servers -> Seq(Values)]
20+
21+
Init ==
22+
/\ cLogs \in [Servers -> {<< >>}]
23+
24+
Copy(i) ==
25+
\E j \in Servers:
26+
/\ Len(cLogs[j]) > Len(cLogs[i])
27+
/\ \* Sync some prefix up to prefix = suffix of the unsynced suffix.
28+
LET L == (Len(cLogs[j]) - Len(cLogs[i]))
29+
\* Force to proportionally to the lag L copy more.
30+
\* Lag: 1 -> 0..L, 2 -> 1..L, 3 -> 2..L
31+
IN \E l \in L-1 .. L:
32+
cLogs' = [cLogs EXCEPT ![i] = @ \o SubSeq(cLogs[j], Len(@) + 1, Len(@) + l)]
33+
34+
Extend(i) ==
35+
/\ \A j \in Servers:
36+
Len(cLogs[j]) \leq Len(cLogs[i])
37+
/\ \E s \in BoundedSeq(Values, Lag - Max({Len(cLogs[i]) - Len(cLogs[j]) : j \in Servers})):
38+
cLogs' = [cLogs EXCEPT ![i] = @ \o s]
39+
40+
Next ==
41+
\E i \in Servers:
42+
\/ Copy(i)
43+
\/ Extend(i)
44+
45+
Spec ==
46+
/\ Init
47+
/\ [][Next]_vars
48+
/\ \A s \in Servers: WF_vars(Extend(s)) /\ WF_vars(Copy(s))
49+
50+
----
51+
\* Invariants
52+
53+
Abs(n) ==
54+
IF n < 0 THEN -n ELSE n
55+
56+
BoundedLag ==
57+
\A i, j \in Servers: Abs(Len(cLogs[i]) - Len(cLogs[j])) <= Lag
58+
59+
THEOREM Spec => []BoundedLag
60+
61+
----
62+
\* Liveness
63+
64+
AllExtending ==
65+
\A s \in Servers: []<><<IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs
66+
67+
THEOREM Spec => AllExtending
68+
69+
InSync ==
70+
\* TLC correctly verifies that InSync is not a property of the system because
71+
\* followers are permitted to copy only a prefix of the missing suffix.
72+
\A i, j \in Servers : []<>(cLogs[i] = cLogs[j])
73+
74+
====

‎specifications/FiniteMonotonic/MCDistributedReplicatedLog.cfg

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
SPECIFICATION
2+
Spec
3+
4+
CONSTANTS
5+
Servers = {n1, n2, n3}
6+
Values = {v}
7+
Lag = 3
8+
9+
INVARIANTS
10+
TypeOK
11+
BoundedLag
12+
13+
PROPERTIES
14+
AllExtending
15+
\* TLC correctly reconstructs a counterexample to InSync. However,
16+
\* in general, the VIEW approach (e.g. DropCommonPrefix) can prevent
17+
\* TLC from reconstructing a counterexample correctly. For more
18+
\* details, refer to https://github.com/tlaplus/tlaplus/issues/1045.
19+
InSync
20+
21+
VIEW
22+
DropCommonPrefix
23+
24+
CHECK_DEADLOCK
25+
TRUE

‎specifications/FiniteMonotonic/MCDistributedReplicatedLog.tla

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
---- MODULE MCDistributedReplicatedLog ----
2+
EXTENDS DistributedReplicatedLog, FiniteSetsExt
3+
4+
ASSUME
5+
\* LongestCommonPrefix in View for a single server would always shorten the
6+
\* log to <<>>, reducing the state-space to a single state.
7+
Cardinality(Servers) > 1
8+
9+
----
10+
11+
\* Combining the following conditions makes the state space finite:
12+
\* 1) The divergence of any two logs is bounded (See Extend action)
13+
\*
14+
\* 2) Terms is a *finite* set.
15+
ASSUME IsFiniteSet(Values)
16+
\*
17+
\* 3) The longest common prefix of all logs is discarded.
18+
DropCommonPrefix ==
19+
LET commonPrefixBound == Len(LongestCommonPrefix(Range(cLogs)))
20+
Drop(seq, idx) == SubSeq(seq, idx + 1, Len(seq))
21+
IN [ s \in Servers |-> Drop(cLogs[s], commonPrefixBound) ]
22+
23+
====

‎specifications/FiniteMonotonic/README.md

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,5 @@ Neither this approach nor the older approach have a proof of soundness and compl
44

55
Specs & models include:
66
- `CRDT.tla`: the spec of a basic grow-only counter CRDT
7-
- `ReplicatedLog.tla`: the "spec of a basic append-only replicated log
7+
- `ReplicatedLog.tla`: the spec of a basic append-only replicated log
8+
- `DistributedReplicatedLog.tla`: a spec of a distributed replicated log that demonstrates how the technique can be used to find violations of a liveness property (`Insync`).

0 commit comments

Comments
 (0)