mirror of
https://github.com/neondatabase/neon.git
synced 2026-05-17 13:10:38 +00:00
Compare commits
47 Commits
release-pr
...
sk-tla-mem
| Author | SHA1 | Date | |
|---|---|---|---|
|
f5e59cf51b | ||
|
|
691c290280 | ||
|
|
db343caf5d | ||
|
|
6b7af160bf | ||
|
|
a9662b6f64 | ||
|
|
7a580627fc | ||
|
|
176fe2cade | ||
|
|
c846389812 | ||
|
|
cb1ebedc9f | ||
|
|
08b19dd6aa | ||
|
|
ced1903267 | ||
|
|
9584317564 | ||
|
|
4c7bdfa70a | ||
|
|
59cb648457 | ||
|
|
8c880d088b | ||
|
|
c940f196ce | ||
|
|
d0b4b3e64a | ||
|
|
617a8711be | ||
|
|
da5b71b5c1 | ||
|
|
6b62b7633b | ||
|
|
07872b310c | ||
|
|
90aa12c3d8 | ||
|
|
02dc3b2ba2 | ||
|
|
9ab6a89b5c | ||
|
|
79137382e7 | ||
|
|
e87d0813d1 | ||
|
|
ec7c8814f4 | ||
|
|
31c3eb7628 | ||
|
|
a2c67361b0 | ||
|
|
0d057d1374 | ||
|
|
2917e49391 | ||
|
|
91357b05e8 | ||
|
|
765adaf16c | ||
|
|
50a23d5a14 | ||
|
|
1c30e6a61a | ||
|
|
42a9ef3645 | ||
|
|
83b8e5c117 | ||
|
|
5912932de8 | ||
|
|
9aa29712d3 | ||
|
|
443a6fdfdb | ||
|
|
664569ecdb | ||
|
|
a9ced3573a | ||
|
|
f7b9fc1c81 | ||
|
|
979f925949 | ||
|
|
13fd695e3f | ||
|
|
2d0c22d77d | ||
|
|
9cde4ab0a7 |
3
safekeeper/spec/.gitignore
vendored
Normal file
3
safekeeper/spec/.gitignore
vendored
Normal file
@@ -0,0 +1,3 @@
|
||||
*TTrace*
|
||||
*.toolbox/
|
||||
states/
|
||||
41
safekeeper/spec/MCProposerAcceptorReconfig.tla
Normal file
41
safekeeper/spec/MCProposerAcceptorReconfig.tla
Normal file
@@ -0,0 +1,41 @@
|
||||
---- MODULE MCProposerAcceptorReconfig ----
|
||||
EXTENDS TLC, ProposerAcceptorReconfig
|
||||
|
||||
\* Augments the spec with model checking constraints.
|
||||
|
||||
\* It slightly duplicates MCProposerAcceptorStatic, but we can't EXTENDS it
|
||||
\* because it EXTENDS ProposerAcceptorStatic in turn. The duplication isn't big
|
||||
\* anyway.
|
||||
|
||||
\* For model checking.
|
||||
CONSTANTS
|
||||
max_entries, \* model constraint: max log entries acceptor/proposer can hold
|
||||
max_term, \* model constraint: max allowed term
|
||||
max_generation \* mode constraint: max config generation
|
||||
|
||||
ASSUME max_entries \in Nat /\ max_term \in Nat /\ max_generation \in Nat
|
||||
|
||||
\* Model space constraint.
|
||||
StateConstraint == /\ \A p \in proposers:
|
||||
/\ prop_state[p].term <= max_term
|
||||
/\ Len(prop_state[p].wal) <= max_entries
|
||||
/\ conf_store.generation <= max_generation
|
||||
|
||||
\* Sets of proposers and acceptors and symmetric because we don't take any
|
||||
\* actions depending on some concrete proposer/acceptor (like IF p = p1 THEN
|
||||
\* ...)
|
||||
ProposerAcceptorSymmetry == Permutations(proposers) \union Permutations(acceptors)
|
||||
|
||||
\* enforce order of the vars in the error trace with ALIAS
|
||||
\* Note that ALIAS is supported only since version 1.8.0 which is pre-release
|
||||
\* as of writing this.
|
||||
Alias == [
|
||||
prop_state |-> prop_state,
|
||||
prop_conf |-> prop_conf,
|
||||
acc_state |-> acc_state,
|
||||
acc_conf |-> acc_conf,
|
||||
committed |-> committed,
|
||||
conf_store |-> conf_store
|
||||
]
|
||||
|
||||
====
|
||||
31
safekeeper/spec/MCProposerAcceptorStatic.tla
Normal file
31
safekeeper/spec/MCProposerAcceptorStatic.tla
Normal file
@@ -0,0 +1,31 @@
|
||||
---- MODULE MCProposerAcceptorStatic ----
|
||||
EXTENDS TLC, ProposerAcceptorStatic
|
||||
|
||||
\* Augments the spec with model checking constraints.
|
||||
|
||||
\* For model checking.
|
||||
CONSTANTS
|
||||
max_entries, \* model constraint: max log entries acceptor/proposer can hold
|
||||
max_term \* model constraint: max allowed term
|
||||
|
||||
ASSUME max_entries \in Nat /\ max_term \in Nat
|
||||
|
||||
\* Model space constraint.
|
||||
StateConstraint == \A p \in proposers:
|
||||
/\ prop_state[p].term <= max_term
|
||||
/\ Len(prop_state[p].wal) <= max_entries
|
||||
\* Sets of proposers and acceptors are symmetric because we don't take any
|
||||
\* actions depending on some concrete proposer/acceptor (like IF p = p1 THEN
|
||||
\* ...)
|
||||
ProposerAcceptorSymmetry == Permutations(proposers) \union Permutations(acceptors)
|
||||
|
||||
\* enforce order of the vars in the error trace with ALIAS
|
||||
\* Note that ALIAS is supported only since version 1.8.0 which is pre-release
|
||||
\* as of writing this.
|
||||
Alias == [
|
||||
prop_state |-> prop_state,
|
||||
acc_state |-> acc_state,
|
||||
committed |-> committed
|
||||
]
|
||||
|
||||
====
|
||||
@@ -1,34 +0,0 @@
|
||||
\* MV CONSTANT declarations
|
||||
CONSTANT NULL = NULL
|
||||
CONSTANTS
|
||||
p1 = p1
|
||||
p2 = p2
|
||||
p3 = p3
|
||||
a1 = a1
|
||||
a2 = a2
|
||||
a3 = a3
|
||||
\* MV CONSTANT definitions
|
||||
CONSTANT
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3}
|
||||
\* SYMMETRY definition
|
||||
SYMMETRY perms
|
||||
\* CONSTANT definitions
|
||||
CONSTANT
|
||||
max_term = 3
|
||||
CONSTANT
|
||||
max_entries = 3
|
||||
\* INIT definition
|
||||
INIT
|
||||
Init
|
||||
\* NEXT definition
|
||||
NEXT
|
||||
Next
|
||||
\* INVARIANT definition
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafety
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
CommittedNotOverwritten
|
||||
CHECK_DEADLOCK FALSE
|
||||
@@ -1,363 +0,0 @@
|
||||
---- MODULE ProposerAcceptorConsensus ----
|
||||
|
||||
\* Differences from current implementation:
|
||||
\* - unified not-globally-unique epoch & term (node_id)
|
||||
\* Simplifications:
|
||||
\* - instant message delivery
|
||||
\* - feedback is not modeled separately, commit_lsn is updated directly
|
||||
|
||||
EXTENDS Integers, Sequences, FiniteSets, TLC
|
||||
|
||||
VARIABLES
|
||||
prop_state, \* prop_state[p] is state of proposer p
|
||||
acc_state, \* acc_state[a] is state of acceptor a
|
||||
commit_lsns \* map of acceptor -> commit_lsn
|
||||
|
||||
CONSTANT
|
||||
acceptors,
|
||||
proposers,
|
||||
max_entries, \* model constraint: max log entries acceptor/proposer can hold
|
||||
max_term \* model constraint: max allowed term
|
||||
|
||||
CONSTANT NULL
|
||||
|
||||
ASSUME max_entries \in Nat /\ max_term \in Nat
|
||||
|
||||
\* For specifying symmetry set in manual cfg file, see
|
||||
\* https://github.com/tlaplus/tlaplus/issues/404
|
||||
perms == Permutations(proposers) \union Permutations(acceptors)
|
||||
|
||||
\********************************************************************************
|
||||
\* Helpers
|
||||
\********************************************************************************
|
||||
|
||||
Maximum(S) ==
|
||||
(*************************************************************************)
|
||||
(* If S is a set of numbers, then this define Maximum(S) to be the *)
|
||||
(* maximum of those numbers, or -1 if S is empty. *)
|
||||
(*************************************************************************)
|
||||
IF S = {} THEN -1
|
||||
ELSE CHOOSE n \in S : \A m \in S : n \geq m
|
||||
|
||||
\* minimum of numbers in the set, error if set is empty
|
||||
Minimum(S) ==
|
||||
CHOOSE min \in S : \A n \in S : min <= n
|
||||
|
||||
\* Min of two numbers
|
||||
Min(a, b) == IF a < b THEN a ELSE b
|
||||
|
||||
\* Set of values of function f. XXX is there a such builtin?
|
||||
FValues(f) == {f[a] : a \in DOMAIN f}
|
||||
|
||||
\* Sort of 0 for functions
|
||||
EmptyF == [x \in {} |-> 42]
|
||||
IsEmptyF(f) == DOMAIN f = {}
|
||||
|
||||
\* Next entry proposer p will push to acceptor a or NULL.
|
||||
NextEntry(p, a) ==
|
||||
IF Len(prop_state[p].wal) >= prop_state[p].next_send_lsn[a] THEN
|
||||
CHOOSE r \in FValues(prop_state[p].wal) : r.lsn = prop_state[p].next_send_lsn[a]
|
||||
ELSE
|
||||
NULL
|
||||
|
||||
|
||||
\*****************
|
||||
|
||||
NumAccs == Cardinality(acceptors)
|
||||
|
||||
\* does acc_set form the quorum?
|
||||
Quorum(acc_set) == Cardinality(acc_set) >= (NumAccs \div 2 + 1)
|
||||
\* all quorums of acceptors
|
||||
Quorums == {subset \in SUBSET acceptors: Quorum(subset)}
|
||||
|
||||
\* flush_lsn of acceptor a.
|
||||
FlushLsn(a) == Len(acc_state[a].wal)
|
||||
|
||||
|
||||
\********************************************************************************
|
||||
\* Type assertion
|
||||
\********************************************************************************
|
||||
\* Defining sets of all possible tuples and using them in TypeOk in usual
|
||||
\* all-tuples constructor is not practical because such definitions force
|
||||
\* TLC to enumerate them, while they are are horribly enormous
|
||||
\* (TLC screams "Attempted to construct a set with too many elements").
|
||||
\* So instead check types manually.
|
||||
TypeOk ==
|
||||
/\ \A p \in proposers:
|
||||
/\ DOMAIN prop_state[p] = {"state", "term", "votes", "donor_epoch", "vcl", "wal", "next_send_lsn"}
|
||||
\* in campaign proposer sends RequestVote and waits for acks;
|
||||
\* in leader he is elected
|
||||
/\ prop_state[p].state \in {"campaign", "leader"}
|
||||
\* 0..max_term should be actually Nat in the unbounded model, but TLC won't
|
||||
\* swallow it
|
||||
/\ prop_state[p].term \in 0..max_term
|
||||
\* votes received
|
||||
/\ \A voter \in DOMAIN prop_state[p].votes:
|
||||
/\ voter \in acceptors
|
||||
/\ prop_state[p].votes[voter] \in [epoch: 0..max_term, flush_lsn: 0..max_entries]
|
||||
/\ prop_state[p].donor_epoch \in 0..max_term
|
||||
\* wal is sequence of just <lsn, epoch of author> records
|
||||
/\ \A i \in DOMAIN prop_state[p].wal:
|
||||
prop_state[p].wal[i] \in [lsn: 1..max_entries, epoch: 1..max_term]
|
||||
\* Following implementation, we skew the original Aurora meaning of this;
|
||||
\* here it is lsn of highest definitely committed record as set by proposer
|
||||
\* when it is elected; it doesn't change since then
|
||||
/\ prop_state[p].vcl \in 0..max_entries
|
||||
\* map of acceptor -> next lsn to send
|
||||
/\ \A a \in DOMAIN prop_state[p].next_send_lsn:
|
||||
/\ a \in acceptors
|
||||
/\ prop_state[p].next_send_lsn[a] \in 1..(max_entries + 1)
|
||||
/\ \A a \in acceptors:
|
||||
/\ DOMAIN acc_state[a] = {"term", "epoch", "wal"}
|
||||
/\ acc_state[a].term \in 0..max_term
|
||||
/\ acc_state[a].epoch \in 0..max_term
|
||||
/\ \A i \in DOMAIN acc_state[a].wal:
|
||||
acc_state[a].wal[i] \in [lsn: 1..max_entries, epoch: 1..max_term]
|
||||
/\ \A a \in DOMAIN commit_lsns:
|
||||
/\ a \in acceptors
|
||||
/\ commit_lsns[a] \in 0..max_entries
|
||||
|
||||
\********************************************************************************
|
||||
\* Initial
|
||||
\********************************************************************************
|
||||
|
||||
Init ==
|
||||
/\ prop_state = [p \in proposers |-> [
|
||||
state |-> "campaign",
|
||||
term |-> 1,
|
||||
votes |-> EmptyF,
|
||||
donor_epoch |-> 0,
|
||||
vcl |-> 0,
|
||||
wal |-> << >>,
|
||||
next_send_lsn |-> EmptyF
|
||||
]]
|
||||
/\ acc_state = [a \in acceptors |-> [
|
||||
\* there will be no leader in this term, 1 is the first real
|
||||
term |-> 0,
|
||||
epoch |-> 0,
|
||||
wal |-> << >>
|
||||
]]
|
||||
/\ commit_lsns = [a \in acceptors |-> 0]
|
||||
|
||||
|
||||
\********************************************************************************
|
||||
\* Actions
|
||||
\********************************************************************************
|
||||
|
||||
\* Proposer loses all state.
|
||||
\* For simplicity (and to reduct state space), we assume it immediately gets
|
||||
\* current state from quorum q of acceptors determining the term he will request
|
||||
\* to vote for.
|
||||
RestartProposer(p, q) ==
|
||||
/\ Quorum(q)
|
||||
/\ LET
|
||||
new_term == Maximum({acc_state[a].term : a \in q}) + 1
|
||||
IN
|
||||
/\ new_term <= max_term
|
||||
/\ prop_state' = [prop_state EXCEPT ![p].state = "campaign",
|
||||
![p].term = new_term,
|
||||
![p].votes = EmptyF,
|
||||
![p].donor_epoch = 0,
|
||||
![p].vcl = 0,
|
||||
![p].wal = << >>,
|
||||
![p].next_send_lsn = EmptyF]
|
||||
/\ UNCHANGED <<acc_state, commit_lsns>>
|
||||
|
||||
\* Acceptor a immediately votes for proposer p.
|
||||
Vote(p, a) ==
|
||||
/\ prop_state[p].state = "campaign"
|
||||
/\ acc_state[a].term < prop_state[p].term \* main voting condition
|
||||
/\ acc_state' = [acc_state EXCEPT ![a].term = prop_state[p].term]
|
||||
/\ LET
|
||||
vote == [epoch |-> acc_state[a].epoch, flush_lsn |-> FlushLsn(a)]
|
||||
IN
|
||||
prop_state' = [prop_state EXCEPT ![p].votes = prop_state[p].votes @@ (a :> vote)]
|
||||
/\ UNCHANGED <<commit_lsns>>
|
||||
|
||||
|
||||
\* Proposer p gets elected.
|
||||
BecomeLeader(p) ==
|
||||
/\ prop_state[p].state = "campaign"
|
||||
/\ Quorum(DOMAIN prop_state[p].votes)
|
||||
/\ LET
|
||||
max_epoch == Maximum({v.epoch : v \in FValues(prop_state[p].votes)})
|
||||
max_epoch_votes == {v \in FValues(prop_state[p].votes) : v.epoch = max_epoch}
|
||||
donor == CHOOSE dv \in DOMAIN prop_state[p].votes :
|
||||
/\ prop_state[p].votes[dv].epoch = max_epoch
|
||||
/\ \A v \in max_epoch_votes:
|
||||
prop_state[p].votes[dv].flush_lsn >= v.flush_lsn
|
||||
max_vote == prop_state[p].votes[donor]
|
||||
\* Establish lsn to stream from for voters.
|
||||
\* At some point it seemed like we can regard log as correct and only
|
||||
\* append to it if has in the max_epoch, however TLC showed that's not
|
||||
\* the case; we must always stream since first not matching record.
|
||||
next_send_lsn == [voter \in DOMAIN prop_state[p].votes |-> 1]
|
||||
IN
|
||||
\* we fetch log from the most advanced node (this is separate
|
||||
\* roundtrip), make sure node is still on one term with us
|
||||
/\ acc_state[donor].term = prop_state[p].term
|
||||
/\ prop_state' = [prop_state EXCEPT ![p].state = "leader",
|
||||
\* fetch the log from donor
|
||||
![p].wal = acc_state[donor].wal,
|
||||
![p].donor_epoch = max_epoch,
|
||||
![p].vcl = max_vote.flush_lsn,
|
||||
![p].next_send_lsn = next_send_lsn]
|
||||
/\ UNCHANGED <<acc_state, commit_lsns>>
|
||||
|
||||
|
||||
\* acceptor a learns about elected proposer p's term.
|
||||
UpdateTerm(p, a) ==
|
||||
/\ prop_state[p].state = "leader"
|
||||
/\ acc_state[a].term < prop_state[p].term
|
||||
/\ acc_state' = [acc_state EXCEPT ![a].term = prop_state[p].term]
|
||||
/\ UNCHANGED <<prop_state, commit_lsns>>
|
||||
|
||||
|
||||
\* Acceptor a which didn't participate in voting connects to elected proposer p
|
||||
\* and p sets the streaming point
|
||||
HandshakeWithLeader(p, a) ==
|
||||
/\ prop_state[p].state = "leader"
|
||||
/\ acc_state[a].term = prop_state[p].term
|
||||
/\ a \notin DOMAIN prop_state[p].next_send_lsn
|
||||
/\ LET
|
||||
next_send_lsn == prop_state[p].next_send_lsn @@ (a :> 1)
|
||||
IN
|
||||
prop_state' = [prop_state EXCEPT ![p].next_send_lsn = next_send_lsn]
|
||||
/\ UNCHANGED <<acc_state, commit_lsns>>
|
||||
|
||||
|
||||
\* Append new log entry to elected proposer
|
||||
NewEntry(p) ==
|
||||
/\ prop_state[p].state = "leader"
|
||||
/\ Len(prop_state[p].wal) < max_entries \* model constraint
|
||||
/\ LET
|
||||
new_lsn == IF Len(prop_state[p].wal) = 0 THEN
|
||||
prop_state[p].vcl + 1
|
||||
ELSE
|
||||
\* lsn of last record + 1
|
||||
prop_state[p].wal[Len(prop_state[p].wal)].lsn + 1
|
||||
new_entry == [lsn |-> new_lsn, epoch |-> prop_state[p].term]
|
||||
IN
|
||||
/\ prop_state' = [prop_state EXCEPT ![p].wal = Append(prop_state[p].wal, new_entry)]
|
||||
/\ UNCHANGED <<acc_state, commit_lsns>>
|
||||
|
||||
|
||||
\* Write entry new_e to log wal, rolling back all higher entries if e is different.
|
||||
\* If bump_epoch is TRUE, it means we get record with lsn=vcl and going to update
|
||||
\* the epoch. Truncate log in this case as well, as we might have correct <= vcl
|
||||
\* part and some outdated entries behind it which we want to purge before
|
||||
\* declaring us as recovered. Another way to accomplish this (in previous commit)
|
||||
\* is wait for first-entry-from-new-epoch before bumping it.
|
||||
WriteEntry(wal, new_e, bump_epoch) ==
|
||||
(new_e.lsn :> new_e) @@
|
||||
\* If wal has entry with such lsn and it is different, truncate all higher log.
|
||||
IF \/ (new_e.lsn \in DOMAIN wal /\ wal[new_e.lsn] /= new_e)
|
||||
\/ bump_epoch THEN
|
||||
SelectSeq(wal, LAMBDA e: e.lsn < new_e.lsn)
|
||||
ELSE
|
||||
wal
|
||||
|
||||
|
||||
\* Try to transfer entry from elected proposer p to acceptor a
|
||||
TransferEntry(p, a) ==
|
||||
/\ prop_state[p].state = "leader"
|
||||
/\ prop_state[p].term = acc_state[a].term
|
||||
/\ a \in DOMAIN prop_state[p].next_send_lsn
|
||||
/\ LET
|
||||
next_e == NextEntry(p, a)
|
||||
IN
|
||||
/\ next_e /= NULL
|
||||
/\ LET
|
||||
\* Consider bumping epoch if getting this entry recovers the acceptor,
|
||||
\* that is, we reach first record behind VCL.
|
||||
new_epoch ==
|
||||
IF /\ acc_state[a].epoch < prop_state[p].term
|
||||
/\ next_e.lsn >= prop_state[p].vcl
|
||||
THEN
|
||||
prop_state[p].term
|
||||
ELSE
|
||||
acc_state[a].epoch
|
||||
\* Also check whether this entry allows to advance commit_lsn and
|
||||
\* if so, bump it where possible. Modeling this as separate action
|
||||
\* significantly bloats the space (5m vs 15m on max_entries=3 max_term=3,
|
||||
\* so act immediately.
|
||||
entry_owners == {o \in acceptors:
|
||||
/\ o /= a
|
||||
\* only recovered acceptors advance commit_lsn
|
||||
/\ acc_state[o].epoch = prop_state[p].term
|
||||
/\ next_e \in FValues(acc_state[o].wal)} \cup {a}
|
||||
IN
|
||||
/\ acc_state' = [acc_state EXCEPT ![a].wal = WriteEntry(acc_state[a].wal, next_e, new_epoch /= acc_state[a].epoch),
|
||||
![a].epoch = new_epoch]
|
||||
/\ prop_state' = [prop_state EXCEPT ![p].next_send_lsn[a] =
|
||||
prop_state[p].next_send_lsn[a] + 1]
|
||||
/\ commit_lsns' = IF /\ new_epoch = prop_state[p].term
|
||||
/\ Quorum(entry_owners)
|
||||
THEN
|
||||
[acc \in acceptors |->
|
||||
IF /\ acc \in entry_owners
|
||||
/\ next_e.lsn > commit_lsns[acc]
|
||||
THEN
|
||||
next_e.lsn
|
||||
ELSE
|
||||
commit_lsns[acc]]
|
||||
ELSE
|
||||
commit_lsns
|
||||
|
||||
|
||||
\*******************************************************************************
|
||||
\* Final spec
|
||||
\*******************************************************************************
|
||||
|
||||
Next ==
|
||||
\/ \E q \in Quorums: \E p \in proposers: RestartProposer(p, q)
|
||||
\/ \E p \in proposers: \E a \in acceptors: Vote(p, a)
|
||||
\/ \E p \in proposers: BecomeLeader(p)
|
||||
\/ \E p \in proposers: \E a \in acceptors: UpdateTerm(p, a)
|
||||
\/ \E p \in proposers: \E a \in acceptors: HandshakeWithLeader(p, a)
|
||||
\/ \E p \in proposers: NewEntry(p)
|
||||
\/ \E p \in proposers: \E a \in acceptors: TransferEntry(p, a)
|
||||
|
||||
Spec == Init /\ [][Next]_<<prop_state, acc_state, commit_lsns>>
|
||||
|
||||
|
||||
\********************************************************************************
|
||||
\* Invariants
|
||||
\********************************************************************************
|
||||
|
||||
\* we don't track history, but this property is fairly convincing anyway
|
||||
ElectionSafety ==
|
||||
\A p1, p2 \in proposers:
|
||||
(/\ prop_state[p1].state = "leader"
|
||||
/\ prop_state[p2].state = "leader"
|
||||
/\ prop_state[p1].term = prop_state[p2].term) => (p1 = p2)
|
||||
|
||||
LogIsMonotonic ==
|
||||
\A a \in acceptors:
|
||||
\A i \in DOMAIN acc_state[a].wal: \A j \in DOMAIN acc_state[a].wal:
|
||||
(i > j) => (/\ acc_state[a].wal[i].lsn > acc_state[a].wal[j].lsn
|
||||
/\ acc_state[a].wal[i].epoch >= acc_state[a].wal[j].epoch)
|
||||
|
||||
\* Main invariant: log under commit_lsn must match everywhere.
|
||||
LogSafety ==
|
||||
\A a1 \in acceptors: \A a2 \in acceptors:
|
||||
LET
|
||||
common_len == Min(commit_lsns[a1], commit_lsns[a2])
|
||||
IN
|
||||
SubSeq(acc_state[a1].wal, 1, common_len) = SubSeq(acc_state[a2].wal, 1, common_len)
|
||||
|
||||
\* Next record we are going to push to acceptor must never overwrite committed
|
||||
\* different record.
|
||||
CommittedNotOverwritten ==
|
||||
\A p \in proposers: \A a \in acceptors:
|
||||
(/\ prop_state[p].state = "leader"
|
||||
/\ prop_state[p].term = acc_state[a].term
|
||||
/\ a \in DOMAIN prop_state[p].next_send_lsn) =>
|
||||
LET
|
||||
next_e == NextEntry(p, a)
|
||||
IN
|
||||
(next_e /= NULL) =>
|
||||
((commit_lsns[a] >= next_e.lsn) => (acc_state[a].wal[next_e.lsn] = next_e))
|
||||
|
||||
|
||||
====
|
||||
310
safekeeper/spec/ProposerAcceptorReconfig.tla
Normal file
310
safekeeper/spec/ProposerAcceptorReconfig.tla
Normal file
@@ -0,0 +1,310 @@
|
||||
---- MODULE ProposerAcceptorReconfig ----
|
||||
|
||||
(*
|
||||
Spec for https://github.com/neondatabase/neon/blob/538e2312a617c65d489d391892c70b2e4d7407b5/docs/rfcs/035-safekeeper-dynamic-membership-change.md
|
||||
*)
|
||||
|
||||
EXTENDS Integers, Sequences, FiniteSets, TLC
|
||||
|
||||
VARIABLES
|
||||
\* state which is the same in the static spec
|
||||
prop_state,
|
||||
acc_state,
|
||||
committed,
|
||||
elected_history,
|
||||
\* reconfiguration only state
|
||||
prop_conf, \* prop_conf[p] is current configuration of proposer p
|
||||
acc_conf, \* acc_conf[a] is current configuration of acceptor a
|
||||
conf_store \* configuration in the configuration store.
|
||||
|
||||
CONSTANT
|
||||
acceptors,
|
||||
proposers
|
||||
|
||||
CONSTANT NULL
|
||||
|
||||
\* Import ProposerAcceptorStatic under PAS.
|
||||
\*
|
||||
\* Note that all vars and consts are named the same and thus substituted
|
||||
\* implicitly.
|
||||
PAS == INSTANCE ProposerAcceptorStatic
|
||||
|
||||
\********************************************************************************
|
||||
\* Helpers
|
||||
\********************************************************************************
|
||||
|
||||
\********************************************************************************
|
||||
\* Type assertion
|
||||
\********************************************************************************
|
||||
|
||||
\* Is c a valid config?
|
||||
IsConfig(c) ==
|
||||
/\ DOMAIN c = {"generation", "members", "newMembers"}
|
||||
\* Unique id of the configuration.
|
||||
/\ c.generation \in Nat
|
||||
/\ c.members \in SUBSET acceptors
|
||||
\* newMembers is NULL when it is not a joint conf.
|
||||
/\ \/ c.newMembers = NULL
|
||||
\/ c.newMembers \in SUBSET acceptors
|
||||
|
||||
TypeOk ==
|
||||
/\ PAS!TypeOk
|
||||
/\ \A p \in proposers: IsConfig(prop_conf[p])
|
||||
/\ \A a \in acceptors: IsConfig(acc_conf[a])
|
||||
/\ IsConfig(conf_store)
|
||||
|
||||
\********************************************************************************
|
||||
\* Initial
|
||||
\********************************************************************************
|
||||
|
||||
Init ==
|
||||
/\ PAS!Init
|
||||
/\ \E init_members \in SUBSET acceptors:
|
||||
LET init_conf == [generation |-> 1, members |-> init_members, newMembers |-> NULL] IN
|
||||
\* refer to RestartProposer why it is not NULL
|
||||
/\ prop_conf = [p \in proposers |-> init_conf]
|
||||
/\ acc_conf = [a \in acceptors |-> init_conf]
|
||||
/\ conf_store = init_conf
|
||||
\* We could start with anything, but to reduce space state start with
|
||||
\* the most reasonable total acceptors - 1 conf size, which e.g.
|
||||
\* makes basic {a1} -> {a2} change in {a1, a2} acceptors and {a1, a2,
|
||||
\* a3} -> {a2, a3, a4} in {a1, a2, a3, a4} acceptors models even in
|
||||
\* the smallest models with single change.
|
||||
/\ Cardinality(init_members) = Cardinality(acceptors) - 1
|
||||
|
||||
\********************************************************************************
|
||||
\* Actions
|
||||
\********************************************************************************
|
||||
|
||||
\* Proposer p loses all state, restarting. In the static spec we bump restarted
|
||||
\* proposer term to max of some quorum + 1 which is a minimal term which can win
|
||||
\* election. With reconfigurations it's harder to calculate such a term, so keep
|
||||
\* it simple and take random acceptor one + 1.
|
||||
\*
|
||||
\* Also make proposer to adopt configuration of another random acceptor. In the
|
||||
\* impl proposer starts with NULL configuration until handshake with first
|
||||
\* acceptor. Removing this NULL special case makes the spec a bit simpler.
|
||||
RestartProposer(p) ==
|
||||
/\ \E a \in acceptors: PAS!RestartProposerWithTerm(p, acc_state[a].term + 1)
|
||||
/\ \E a \in acceptors: prop_conf' = [prop_conf EXCEPT ![p] = acc_conf[a]]
|
||||
/\ UNCHANGED <<acc_conf, conf_store>>
|
||||
|
||||
\* Acceptor a immediately votes for proposer p.
|
||||
Vote(p, a) ==
|
||||
\* Configuration must be the same.
|
||||
/\ prop_conf[p].generation = acc_conf[a].generation
|
||||
\* And a is expected be a member of it. This is likely redundant as long as
|
||||
\* becoming leader checks membership (though vote also contributes to max
|
||||
\* <term, lsn> calculation).
|
||||
/\ \/ a \in prop_conf[p].members
|
||||
\/ (prop_conf[p].newMembers /= NULL) /\ (a \in prop_conf[p].newMembers)
|
||||
/\ PAS!Vote(p, a)
|
||||
/\ UNCHANGED <<prop_conf, acc_conf, conf_store>>
|
||||
|
||||
\* Proposer p gets elected.
|
||||
BecomeLeader(p) ==
|
||||
/\ prop_state[p].state = "campaign"
|
||||
\* Votes must form quorum in both sets (if the newMembers exists).
|
||||
/\ PAS!FormsQuorum(DOMAIN prop_state[p].votes, prop_conf[p].members)
|
||||
/\ \/ prop_conf[p].newMembers = NULL
|
||||
\* TLA+ disjunction evaluation doesn't short-circuit for a good reason:
|
||||
\* https://groups.google.com/g/tlaplus/c/U6tOJ4dsjVM/m/UdOznPCVBwAJ
|
||||
\* so repeat the null check.
|
||||
\/ (prop_conf[p].newMembers /= NULL) /\ (PAS!FormsQuorum(DOMAIN prop_state[p].votes, prop_conf[p].newMembers))
|
||||
\* DoBecomeLeader will copy WAL of the highest voter to proposer's WAL, so
|
||||
\* ensure its conf is still the same. In the impl WAL fetching also has to
|
||||
\* check the configuration.
|
||||
/\ prop_conf[p].generation = acc_conf[PAS!MaxVoteAcc(p)].generation
|
||||
/\ \A a \in DOMAIN prop_state[p].votes: prop_conf[p].generation = acc_conf[a].generation
|
||||
/\ PAS!DoBecomeLeader(p)
|
||||
/\ UNCHANGED <<prop_conf, acc_conf, conf_store>>
|
||||
|
||||
UpdateTerm(p, a) ==
|
||||
/\ PAS!UpdateTerm(p, a)
|
||||
/\ UNCHANGED <<prop_conf, acc_conf, conf_store>>
|
||||
|
||||
TruncateWal(p, a) ==
|
||||
/\ prop_state[p].state = "leader"
|
||||
\* Configuration must be the same.
|
||||
/\ prop_conf[p].generation = acc_conf[a].generation
|
||||
/\ PAS!TruncateWal(p, a)
|
||||
/\ UNCHANGED <<prop_conf, acc_conf, conf_store>>
|
||||
|
||||
NewEntry(p) ==
|
||||
/\ PAS!NewEntry(p)
|
||||
/\ UNCHANGED <<prop_conf, acc_conf, conf_store>>
|
||||
|
||||
AppendEntry(p, a) ==
|
||||
/\ prop_state[p].state = "leader"
|
||||
\* Configuration must be the same.
|
||||
/\ prop_conf[p].generation = acc_conf[a].generation
|
||||
\* And a is member of it. Ignoring this likely wouldn't hurt, but not useful
|
||||
\* either.
|
||||
/\ \/ a \in prop_conf[p].members
|
||||
\/ (prop_conf[p].newMembers /= NULL) /\ (a \in prop_conf[p].newMembers)
|
||||
/\ PAS!AppendEntry(p, a)
|
||||
/\ UNCHANGED <<prop_conf, acc_conf, conf_store>>
|
||||
|
||||
\* see PAS!CommitEntries for comments.
|
||||
CommitEntries(p) ==
|
||||
/\ prop_state[p].state = "leader"
|
||||
/\ \E q1 \in PAS!AllMinQuorums(prop_conf[p].members):
|
||||
LET q1_commit_lsn == PAS!QuorumCommitLsn(p, q1) IN
|
||||
\* Configuration must be the same.
|
||||
/\ \A a \in q1: prop_conf[p].generation = acc_conf[a].generation
|
||||
/\ q1_commit_lsn /= NULL
|
||||
\* We must collect acks from both quorums, if newMembers is present.
|
||||
/\ IF prop_conf[p].newMembers = NULL THEN
|
||||
PAS!DoCommitEntries(p, q1_commit_lsn)
|
||||
ELSE
|
||||
\E q2 \in PAS!AllMinQuorums(prop_conf[p].newMembers):
|
||||
LET q2_commit_lsn == PAS!QuorumCommitLsn(p, q2) IN
|
||||
\* Configuration must be the same.
|
||||
/\ \A a \in q1: prop_conf[p].generation = acc_conf[a].generation
|
||||
/\ q2_commit_lsn /= NULL
|
||||
/\ PAS!DoCommitEntries(p, PAS!Min(q1_commit_lsn, q2_commit_lsn))
|
||||
/\ UNCHANGED <<prop_conf, acc_conf, conf_store>>
|
||||
|
||||
\* Proposer p adopts higher conf from acceptor a.
|
||||
ProposerSwitchConf(p, a) ==
|
||||
\* p's conf is lower than a's.
|
||||
/\ (acc_conf[a].generation > prop_conf[p].generation)
|
||||
\* We allow to seamlessly bump conf only when proposer is already elected.
|
||||
\* If it isn't, some of the votes already collected could have been from
|
||||
\* non-members of updated conf. It is easier (both here and in the impl) to
|
||||
\* restart instead of figuring and removing these out.
|
||||
\*
|
||||
\* So if proposer is in 'campaign' in the impl we would restart preserving
|
||||
\* conf and increasing term. In the spec this transition is already covered
|
||||
\* by more a generic RestartProposer, so we don't specify it here.
|
||||
/\ prop_state[p].state = "leader"
|
||||
/\ prop_conf' = [prop_conf EXCEPT ![p] = acc_conf[a]]
|
||||
/\ UNCHANGED <<prop_state, acc_state, committed, elected_history, acc_conf, conf_store>>
|
||||
|
||||
\* Do CAS on the conf store, starting change into the new_members conf.
|
||||
StartChange(new_members) ==
|
||||
\* Possible only if we don't already have the change in progress.
|
||||
/\ conf_store.newMembers = NULL
|
||||
\* Not necessary, but reduces space a bit.
|
||||
/\ new_members /= conf_store.members
|
||||
/\ conf_store' = [generation |-> conf_store.generation + 1, members |-> conf_store.members, newMembers |-> new_members]
|
||||
/\ UNCHANGED <<prop_state, acc_state, committed, elected_history, prop_conf, acc_conf>>
|
||||
|
||||
\* Acceptor's last_log_term.
|
||||
AccLastLogTerm(acc) ==
|
||||
PAS!LastLogTerm(PAS!AcceptorTermHistory(acc))
|
||||
|
||||
\* Do CAS on the conf store, transferring joint conf into the newMembers only.
|
||||
FinishChange ==
|
||||
\* have joint conf
|
||||
/\ conf_store.newMembers /= NULL
|
||||
\* The conditions for finishing the change are:
|
||||
/\ \E qo \in PAS!AllMinQuorums(conf_store.members):
|
||||
\* 1) Old majority must be aware of the joint conf.
|
||||
/\ \A a \in qo: conf_store.generation = acc_conf[a].generation
|
||||
\* 2) New member set must have log synced, i.e. some majority needs
|
||||
\* to have <last_log_term, lsn> at least as high as max of some
|
||||
\* old majority.
|
||||
\* 3) Term must be synced, i.e. some majority of the new set must
|
||||
\* have term >= than max term of some old majority.
|
||||
\* This ensures that two leaders are never elected with the same
|
||||
\* term even after config change (which would be bad unless we treat
|
||||
\* generation as a part of term which we don't).
|
||||
\* 4) A majority of the new set must be aware of the joint conf.
|
||||
\* This allows to safely destoy acceptor state if it is not a
|
||||
\* member of its current conf (which is useful for cleanup after
|
||||
\* migration as well as for aborts).
|
||||
/\ LET sync_pos == PAS!MaxTermLsn({[term |-> AccLastLogTerm(a), lsn |-> PAS!FlushLsn(a)]: a \in qo})
|
||||
sync_term == PAS!Maximum({acc_state[a].term: a \in qo})
|
||||
IN
|
||||
\E qn \in PAS!AllMinQuorums(conf_store.newMembers):
|
||||
\A a \in qn:
|
||||
/\ PAS!TermLsnGE([term |-> AccLastLogTerm(a), lsn |-> PAS!FlushLsn(a)], sync_pos)
|
||||
/\ acc_state[a].term >= sync_term
|
||||
/\ conf_store.generation = acc_conf[a].generation
|
||||
/\ conf_store' = [generation |-> conf_store.generation + 1, members |-> conf_store.newMembers, newMembers |-> NULL]
|
||||
/\ UNCHANGED <<prop_state, acc_state, committed, elected_history, prop_conf, acc_conf>>
|
||||
|
||||
\* Do CAS on the conf store, aborting the change in progress.
|
||||
AbortChange ==
|
||||
\* have joint conf
|
||||
/\ conf_store.newMembers /= NULL
|
||||
/\ conf_store' = [generation |-> conf_store.generation + 1, members |-> conf_store.members, newMembers |-> NULL]
|
||||
/\ UNCHANGED <<prop_state, acc_state, committed, elected_history, prop_conf, acc_conf>>
|
||||
|
||||
\* Acceptor a switches to higher configuration (we model it as taken from the
|
||||
\* store, but it can be from proposer/peers as well).
|
||||
AccSwitchConf(a) ==
|
||||
/\ acc_conf[a].generation < conf_store.generation
|
||||
/\ acc_conf' = [acc_conf EXCEPT ![a] = conf_store]
|
||||
/\ UNCHANGED <<prop_state, acc_state, committed, elected_history, prop_conf, conf_store>>
|
||||
|
||||
\* Nuke all acceptor state if it is not a member of its current conf. Models
|
||||
\* cleanup after migration/abort.
|
||||
AccReset(a) ==
|
||||
/\ \/ (acc_conf[a].newMembers = NULL) /\ (a \notin acc_conf[a].members)
|
||||
\/ (acc_conf[a].newMembers /= NULL) /\ (a \notin (acc_conf[a].members \union acc_conf[a].newMembers))
|
||||
/\ acc_state' = [acc_state EXCEPT ![a] = PAS!InitAcc]
|
||||
\* Set nextSendLsn to `a` to NULL everywhere. nextSendLsn serves as a mark
|
||||
\* that elected proposer performed TruncateWal on the acceptor, which isn't
|
||||
\* true anymore after state reset. In the impl local deletion is expected to
|
||||
\* terminate all existing connections.
|
||||
/\ prop_state' = [p \in proposers |-> [prop_state[p] EXCEPT !.nextSendLsn[a] = NULL]]
|
||||
/\ UNCHANGED <<committed, elected_history, prop_conf, acc_conf, conf_store>>
|
||||
|
||||
|
||||
\*******************************************************************************
|
||||
\* Final spec
|
||||
\*******************************************************************************
|
||||
|
||||
Next ==
|
||||
\/ \E p \in proposers: RestartProposer(p)
|
||||
\/ \E p \in proposers: \E a \in acceptors: Vote(p, a)
|
||||
\/ \E p \in proposers: BecomeLeader(p)
|
||||
\/ \E p \in proposers: \E a \in acceptors: UpdateTerm(p, a)
|
||||
\/ \E p \in proposers: \E a \in acceptors: TruncateWal(p, a)
|
||||
\/ \E p \in proposers: NewEntry(p)
|
||||
\/ \E p \in proposers: \E a \in acceptors: AppendEntry(p, a)
|
||||
\/ \E p \in proposers: CommitEntries(p)
|
||||
\/ \E new_members \in SUBSET acceptors: StartChange(new_members)
|
||||
\/ FinishChange
|
||||
\/ AbortChange
|
||||
\/ \E p \in proposers: \E a \in acceptors: ProposerSwitchConf(p, a)
|
||||
\/ \E a \in acceptors: AccSwitchConf(a)
|
||||
\/ \E a \in acceptors: AccReset(a)
|
||||
|
||||
Spec == Init /\ [][Next]_<<prop_state, acc_state, committed, elected_history, prop_conf, acc_conf, conf_store>>
|
||||
|
||||
\********************************************************************************
|
||||
\* Invariants
|
||||
\********************************************************************************
|
||||
|
||||
ElectionSafety == PAS!ElectionSafety
|
||||
|
||||
ElectionSafetyFull == PAS!ElectionSafetyFull
|
||||
|
||||
LogIsMonotonic == PAS!LogIsMonotonic
|
||||
|
||||
LogSafety == PAS!LogSafety
|
||||
|
||||
\********************************************************************************
|
||||
\* Invariants which don't need to hold, but useful for playing/debugging.
|
||||
\********************************************************************************
|
||||
|
||||
CommittedNotTruncated == PAS!CommittedNotTruncated
|
||||
|
||||
MaxTerm == PAS!MaxTerm
|
||||
\* MaxTerm == \A p \in proposers: prop_state[p].term <= 1
|
||||
|
||||
MaxStoreConf == conf_store.generation <= 1
|
||||
|
||||
\* Check that we ever switch into non joint conf.
|
||||
MaxAccConf == ~ \E a \in acceptors:
|
||||
/\ acc_conf[a].generation = 3
|
||||
/\ acc_conf[a].newMembers /= NULL
|
||||
|
||||
MaxAccWalLen == PAS!MaxAccWalLen
|
||||
|
||||
MaxCommitLsn == PAS!MaxCommitLsn
|
||||
|
||||
====
|
||||
517
safekeeper/spec/ProposerAcceptorStatic.tla
Normal file
517
safekeeper/spec/ProposerAcceptorStatic.tla
Normal file
@@ -0,0 +1,517 @@
|
||||
---- MODULE ProposerAcceptorStatic ----
|
||||
|
||||
(*
|
||||
The protocol is very similar to Raft. The key differences are:
|
||||
- Leaders (proposers) are separated from storage nodes (acceptors), which has
|
||||
been already an established way to think about Paxos.
|
||||
- We don't want to stamp each log record with term, so instead carry around
|
||||
term histories which are sequences of <term, LSN where term begins> pairs.
|
||||
As a bonus (and subtlety) this allows the proposer to commit entries from
|
||||
previous terms without writing new records -- if acceptor's log is caught
|
||||
up, update of term history on it updates last_log_term as well.
|
||||
*)
|
||||
|
||||
\* Model simplifications:
|
||||
\* - Instant message delivery. Notably, ProposerElected message (TruncateWal action) is not
|
||||
\* delayed, so we don't attempt to truncate WAL when the same wp already appended something
|
||||
\* on the acceptor since common point had been calculated (this should be rejected).
|
||||
\* - old WAL is immediately copied to proposer on its election, without on-demand fetch later.
|
||||
|
||||
\* Some ideas how to break it to play around to get a feeling:
|
||||
\* - replace Quorum with BadQuorum.
|
||||
\* - remove 'don't commit entries from previous terms separately' rule in
|
||||
\* CommitEntries and observe figure 8 from the raft paper.
|
||||
\* With p2a3t4l4 32 steps error was found in 1h on 80 cores.
|
||||
|
||||
EXTENDS Integers, Sequences, FiniteSets, TLC
|
||||
|
||||
VARIABLES
|
||||
prop_state, \* prop_state[p] is state of proposer p
|
||||
acc_state, \* acc_state[a] is state of acceptor a
|
||||
committed, \* bag (set) of ever committed <<term, lsn>> entries
|
||||
elected_history \* counter for elected terms, see TypeOk for details
|
||||
|
||||
CONSTANT
|
||||
acceptors,
|
||||
proposers
|
||||
|
||||
CONSTANT NULL
|
||||
|
||||
\********************************************************************************
|
||||
\* Helpers
|
||||
\********************************************************************************
|
||||
|
||||
Maximum(S) ==
|
||||
(*************************************************************************)
|
||||
(* If S is a set of numbers, then this define Maximum(S) to be the *)
|
||||
(* maximum of those numbers, or -1 if S is empty. *)
|
||||
(*************************************************************************)
|
||||
IF S = {} THEN -1 ELSE CHOOSE n \in S : \A m \in S : n \geq m
|
||||
|
||||
\* minimum of numbers in the set, error if set is empty
|
||||
Minimum(S) == CHOOSE min \in S : \A n \in S : min <= n
|
||||
|
||||
\* Min of two numbers
|
||||
Min(a, b) == IF a < b THEN a ELSE b
|
||||
|
||||
\* Sort of 0 for functions
|
||||
EmptyF == [x \in {} |-> 42]
|
||||
IsEmptyF(f) == DOMAIN f = {}
|
||||
|
||||
\* Set of values (image) of the function f. Apparently no such builtin.
|
||||
Range(f) == {f[x] : x \in DOMAIN f}
|
||||
|
||||
\* If key k is in function f, map it using l, otherwise insert v. Returns the
|
||||
\* updated function.
|
||||
Upsert(f, k, v, l(_)) ==
|
||||
LET new_val == IF k \in DOMAIN f THEN l(f[k]) ELSE v IN
|
||||
(k :> new_val) @@ f
|
||||
|
||||
\*****************
|
||||
|
||||
\* Does set of acceptors `acc_set` form the quorum in the member set `members`?
|
||||
\* Acceptors not from `members` are excluded (matters only for reconfig).
|
||||
FormsQuorum(acc_set, members) ==
|
||||
Cardinality(acc_set \intersect members) >= (Cardinality(members) \div 2 + 1)
|
||||
|
||||
\* Like FormsQuorum, but for minimal quorum.
|
||||
FormsMinQuorum(acc_set, members) ==
|
||||
Cardinality(acc_set \intersect members) = (Cardinality(members) \div 2 + 1)
|
||||
|
||||
\* All sets of acceptors forming minimal quorums in the member set `members`.
|
||||
AllQuorums(members) == {subset \in SUBSET members: FormsQuorum(subset, members)}
|
||||
AllMinQuorums(members) == {subset \in SUBSET acceptors: FormsMinQuorum(subset, members)}
|
||||
|
||||
\* For substituting Quorum and seeing what happens.
|
||||
FormsBadQuorum(acc_set, members) ==
|
||||
Cardinality(acc_set \intersect members) >= (Cardinality(members) \div 2)
|
||||
FormsMinBadQuorum(acc_set, members) ==
|
||||
Cardinality(acc_set \intersect members) = (Cardinality(members) \div 2)
|
||||
AllBadQuorums(members) == {subset \in SUBSET acceptors: FormsBadQuorum(subset, members)}
|
||||
AllMinBadQuorums(members) == {subset \in SUBSET acceptors: FormsMinBadQuorum(subset, members)}
|
||||
|
||||
\* flushLsn (end of WAL, i.e. index of next entry) of acceptor a.
|
||||
FlushLsn(a) == Len(acc_state[a].wal) + 1
|
||||
|
||||
\* Typedefs. Note that TLA+ Nat includes zero.
|
||||
Terms == Nat
|
||||
Lsns == Nat
|
||||
|
||||
\********************************************************************************
|
||||
\* Type assertion
|
||||
\********************************************************************************
|
||||
\* Defining sets of all possible tuples and using them in TypeOk in usual
|
||||
\* all-tuples constructor is not practical because such definitions force
|
||||
\* TLC to enumerate them, while they are are horribly enormous
|
||||
\* (TLC screams "Attempted to construct a set with too many elements").
|
||||
\* So instead check types manually.
|
||||
|
||||
|
||||
\* Term history is a sequence of <term, LSN where term begins> pairs.
|
||||
IsTermHistory(th) ==
|
||||
\A th_entry \in Range(th): th_entry.term \in Terms /\ th_entry.lsn \in Lsns
|
||||
|
||||
IsWal(w) ==
|
||||
\A i \in DOMAIN w:
|
||||
/\ i \in Lsns
|
||||
/\ w[i] \in Terms
|
||||
|
||||
TypeOk ==
|
||||
/\ \A p \in proposers:
|
||||
\* '_' in field names hinders pretty printing
|
||||
\* https://github.com/tlaplus/tlaplus/issues/1051
|
||||
\* so use camel case.
|
||||
/\ DOMAIN prop_state[p] = {"state", "term", "votes", "termHistory", "wal", "nextSendLsn"}
|
||||
\* In campaign proposer sends RequestVote and waits for acks;
|
||||
\* in leader he is elected.
|
||||
/\ prop_state[p].state \in {"campaign", "leader"}
|
||||
\* term for which it will campaign, or won term in leader state
|
||||
/\ prop_state[p].term \in Terms
|
||||
\* votes received
|
||||
/\ \A voter \in DOMAIN prop_state[p].votes: voter \in acceptors
|
||||
/\ \A vote \in Range(prop_state[p].votes):
|
||||
/\ IsTermHistory(vote.termHistory)
|
||||
/\ vote.flushLsn \in Lsns
|
||||
\* Proposer's term history. Empty while proposer is in "campaign".
|
||||
/\ IsTermHistory(prop_state[p].termHistory)
|
||||
\* In the model we identify WAL entries only by <term, LSN> pairs
|
||||
\* without additional unique id, which is enough for its purposes.
|
||||
\* It means that with term history fully modeled wal becomes
|
||||
\* redundant as it can be computed from term history + WAL length.
|
||||
\* However, we still keep it here and at acceptors as explicit sequence
|
||||
\* where index is LSN and value is the term to avoid artificial mapping to
|
||||
\* figure out real entries. It shouldn't bloat model much because this
|
||||
\* doesn't increase number of distinct states.
|
||||
/\ IsWal(prop_state[p].wal)
|
||||
\* Map of acceptor -> next lsn to send. It is set when truncate_wal is
|
||||
\* done so sending entries is allowed only after that. In the impl TCP
|
||||
\* ensures this ordering. We use NULL instead of missing value to use
|
||||
\* EXCEPT in AccReset.
|
||||
/\ \A a \in DOMAIN prop_state[p].nextSendLsn:
|
||||
/\ a \in acceptors
|
||||
/\ prop_state[p].nextSendLsn[a] \in Lsns \union {NULL}
|
||||
/\ \A a \in acceptors:
|
||||
/\ DOMAIN acc_state[a] = {"term", "termHistory", "wal"}
|
||||
/\ acc_state[a].term \in Terms
|
||||
/\ IsTermHistory(acc_state[a].termHistory)
|
||||
/\ IsWal(acc_state[a].wal)
|
||||
/\ \A c \in committed:
|
||||
/\ c.term \in Terms
|
||||
/\ c.lsn \in Lsns
|
||||
\* elected_history is a retrospective map of term -> number of times it was
|
||||
\* elected, for use in ElectionSafetyFull invariant. For static spec it is
|
||||
\* fairly convincing that it holds, but with membership change it is less
|
||||
\* trivial. And as we identify log entries only with <term, lsn>, importance
|
||||
\* of it is quite high as violation of log safety might go undetected if
|
||||
\* election safety is violated. Note though that this is not always the
|
||||
\* case, i.e. you can imagine (and TLC should find) schedule where log
|
||||
\* safety violation is still detected because two leaders with the same term
|
||||
\* commit histories which are different in previous terms, so it is not that
|
||||
\* crucial. Plus if spec allows ElectionSafetyFull violation, likely
|
||||
\* ElectionSafety will also be violated in some schedules. But neither it
|
||||
\* should bloat the model too much.
|
||||
/\ \A term \in DOMAIN elected_history:
|
||||
/\ term \in Terms
|
||||
/\ elected_history[term] \in Nat
|
||||
|
||||
\********************************************************************************
|
||||
\* Initial
|
||||
\********************************************************************************
|
||||
|
||||
InitAcc ==
|
||||
[
|
||||
\* There will be no leader in zero term, 1 is the first
|
||||
\* real.
|
||||
term |-> 0,
|
||||
\* Again, leader in term 0 doesn't exist, but we initialize
|
||||
\* term histories with it to always have common point in
|
||||
\* them. Lsn is 1 because TLA+ sequences are indexed from 1
|
||||
\* (we don't want to truncate WAL out of range).
|
||||
termHistory |-> << [term |-> 0, lsn |-> 1] >>,
|
||||
wal |-> << >>
|
||||
]
|
||||
|
||||
Init ==
|
||||
/\ prop_state = [p \in proposers |-> [
|
||||
state |-> "campaign",
|
||||
term |-> 1,
|
||||
votes |-> EmptyF,
|
||||
termHistory |-> << >>,
|
||||
wal |-> << >>,
|
||||
nextSendLsn |-> [a \in acceptors |-> NULL]
|
||||
]]
|
||||
/\ acc_state = [a \in acceptors |-> InitAcc]
|
||||
/\ committed = {}
|
||||
/\ elected_history = EmptyF
|
||||
|
||||
|
||||
\********************************************************************************
|
||||
\* Actions
|
||||
\********************************************************************************
|
||||
|
||||
RestartProposerWithTerm(p, new_term) ==
|
||||
/\ prop_state' = [prop_state EXCEPT ![p].state = "campaign",
|
||||
![p].term = new_term,
|
||||
![p].votes = EmptyF,
|
||||
![p].termHistory = << >>,
|
||||
![p].wal = << >>,
|
||||
![p].nextSendLsn = [a \in acceptors |-> NULL]]
|
||||
/\ UNCHANGED <<acc_state, committed, elected_history>>
|
||||
|
||||
\* Proposer p loses all state, restarting.
|
||||
\* For simplicity (and to reduct state space), we assume it immediately gets
|
||||
\* current state from quorum q of acceptors determining the term he will request
|
||||
\* to vote for.
|
||||
RestartProposer(p) ==
|
||||
\E q \in AllQuorums(acceptors):
|
||||
LET new_term == Maximum({acc_state[a].term : a \in q}) + 1 IN
|
||||
RestartProposerWithTerm(p, new_term)
|
||||
|
||||
\* Term history of acceptor a's WAL: the one saved truncated to contain only <=
|
||||
\* local FlushLsn entries. Note that FlushLsn is the end LSN of the last entry
|
||||
\* (and begin LSN of the next). The mental model for non strict comparison is
|
||||
\* that once proposer is elected it immediately writes log record with zero
|
||||
\* length. This allows leader to commit existing log without writing any new
|
||||
\* entries. For example, assume acceptor has WAL
|
||||
\* 1.1, 1.2
|
||||
\* written by prop with term 1; its current <last_log_term, flush_lsn>
|
||||
\* is <1, 3>. Now prop with term 2 and max vote from this acc is elected.
|
||||
\* Once TruncateWAL is done, <last_log_term, flush_lsn> becomes <2, 3>
|
||||
\* without any new records explicitly written.
|
||||
AcceptorTermHistory(a) ==
|
||||
SelectSeq(acc_state[a].termHistory, LAMBDA th_entry: th_entry.lsn <= FlushLsn(a))
|
||||
|
||||
\* Acceptor a immediately votes for proposer p.
|
||||
Vote(p, a) ==
|
||||
/\ prop_state[p].state = "campaign"
|
||||
/\ acc_state[a].term < prop_state[p].term \* main voting condition
|
||||
/\ acc_state' = [acc_state EXCEPT ![a].term = prop_state[p].term]
|
||||
/\ LET
|
||||
vote == [termHistory |-> AcceptorTermHistory(a), flushLsn |-> FlushLsn(a)]
|
||||
IN
|
||||
prop_state' = [prop_state EXCEPT ![p].votes = (a :> vote) @@ prop_state[p].votes]
|
||||
/\ UNCHANGED <<committed, elected_history>>
|
||||
|
||||
|
||||
\* Get lastLogTerm from term history th.
|
||||
LastLogTerm(th) == th[Len(th)].term
|
||||
|
||||
\* Compares <term, lsn> pairs: returns true if tl1 >= tl2.
|
||||
TermLsnGE(tl1, tl2) ==
|
||||
/\ tl1.term >= tl2.term
|
||||
/\ (tl1.term = tl2.term => tl1.lsn >= tl2.lsn)
|
||||
|
||||
\* Choose max <term, lsn> pair in the non empty set of them.
|
||||
MaxTermLsn(term_lsn_set) ==
|
||||
CHOOSE max_tl \in term_lsn_set: \A tl \in term_lsn_set: TermLsnGE(max_tl, tl)
|
||||
|
||||
\* Find acceptor with the highest <last_log_term, lsn> vote in proposer p's votes.
|
||||
MaxVoteAcc(p) ==
|
||||
CHOOSE a \in DOMAIN prop_state[p].votes:
|
||||
LET a_vote == prop_state[p].votes[a]
|
||||
a_vote_term_lsn == [term |-> LastLogTerm(a_vote.termHistory), lsn |-> a_vote.flushLsn]
|
||||
vote_term_lsns == {[term |-> LastLogTerm(v.termHistory), lsn |-> v.flushLsn]: v \in Range(prop_state[p].votes)}
|
||||
IN
|
||||
a_vote_term_lsn = MaxTermLsn(vote_term_lsns)
|
||||
|
||||
\* Workhorse for BecomeLeader.
|
||||
\* Assumes the check prop_state[p] votes is quorum has been done *outside*.
|
||||
DoBecomeLeader(p) ==
|
||||
LET
|
||||
\* Find acceptor with the highest <last_log_term, lsn> vote.
|
||||
max_vote_acc == MaxVoteAcc(p)
|
||||
max_vote == prop_state[p].votes[max_vote_acc]
|
||||
prop_th == Append(max_vote.termHistory, [term |-> prop_state[p].term, lsn |-> max_vote.flushLsn])
|
||||
IN
|
||||
\* We copy all log preceding proposer's term from the max vote node so
|
||||
\* make sure it is still on one term with us. This is a model
|
||||
\* simplification which can be removed, in impl we fetch WAL on demand
|
||||
\* from safekeeper which has it later. Note though that in case of on
|
||||
\* demand fetch we must check on donor not only term match, but that
|
||||
\* truncate_wal had already been done (if it is not max_vote_acc).
|
||||
/\ acc_state[max_vote_acc].term = prop_state[p].term
|
||||
/\ prop_state' = [prop_state EXCEPT ![p].state = "leader",
|
||||
![p].termHistory = prop_th,
|
||||
![p].wal = acc_state[max_vote_acc].wal
|
||||
]
|
||||
/\ elected_history' = Upsert(elected_history, prop_state[p].term, 1, LAMBDA c: c + 1)
|
||||
/\ UNCHANGED <<acc_state, committed>>
|
||||
|
||||
\* Proposer p gets elected.
|
||||
BecomeLeader(p) ==
|
||||
/\ prop_state[p].state = "campaign"
|
||||
/\ FormsQuorum(DOMAIN prop_state[p].votes, acceptors)
|
||||
/\ DoBecomeLeader(p)
|
||||
|
||||
\* Acceptor a learns about elected proposer p's term. In impl it matches to
|
||||
\* VoteRequest/VoteResponse exchange when leader is already elected and is not
|
||||
\* interested in the vote result.
|
||||
UpdateTerm(p, a) ==
|
||||
/\ prop_state[p].state = "leader"
|
||||
/\ acc_state[a].term < prop_state[p].term
|
||||
/\ acc_state' = [acc_state EXCEPT ![a].term = prop_state[p].term]
|
||||
/\ UNCHANGED <<prop_state, committed, elected_history>>
|
||||
|
||||
\* Find highest common point (LSN of the first divergent record) in the logs of
|
||||
\* proposer p and acceptor a. Returns <term, lsn> of the highest common point.
|
||||
FindHighestCommonPoint(prop_th, acc_th, acc_flush_lsn) ==
|
||||
LET
|
||||
\* First find index of the highest common term.
|
||||
\* It must exist because we initialize th with <0, 1>.
|
||||
last_common_idx == Maximum({i \in 1..Min(Len(prop_th), Len(acc_th)): prop_th[i].term = acc_th[i].term})
|
||||
last_common_term == prop_th[last_common_idx].term
|
||||
\* Now find where it ends at both prop and acc and take min. End of term
|
||||
\* is the start of the next unless it is the last one; there it is
|
||||
\* flush_lsn in case of acceptor. In case of proposer it is the current
|
||||
\* writing position, but it can't be less than flush_lsn, so we
|
||||
\* take flush_lsn.
|
||||
acc_common_term_end == IF last_common_idx = Len(acc_th) THEN acc_flush_lsn ELSE acc_th[last_common_idx + 1].lsn
|
||||
prop_common_term_end == IF last_common_idx = Len(prop_th) THEN acc_flush_lsn ELSE prop_th[last_common_idx + 1].lsn
|
||||
IN
|
||||
[term |-> last_common_term, lsn |-> Min(acc_common_term_end, prop_common_term_end)]
|
||||
|
||||
\* Elected proposer p immediately truncates WAL (and sets term history) of
|
||||
\* acceptor a before starting streaming. Establishes nextSendLsn for a.
|
||||
\*
|
||||
\* In impl this happens at each reconnection, here we also allow to do it
|
||||
\* multiple times.
|
||||
TruncateWal(p, a) ==
|
||||
/\ prop_state[p].state = "leader"
|
||||
/\ acc_state[a].term = prop_state[p].term
|
||||
/\ LET
|
||||
hcp == FindHighestCommonPoint(prop_state[p].termHistory, AcceptorTermHistory(a), FlushLsn(a))
|
||||
next_send_lsn == (a :> hcp.lsn) @@ prop_state[p].nextSendLsn
|
||||
IN
|
||||
\* Acceptor persists full history immediately; reads adjust it to the
|
||||
\* really existing wal with AcceptorTermHistory.
|
||||
/\ acc_state' = [acc_state EXCEPT ![a].termHistory = prop_state[p].termHistory,
|
||||
\* note: SubSeq is inclusive, hence -1.
|
||||
![a].wal = SubSeq(acc_state[a].wal, 1, hcp.lsn - 1)
|
||||
]
|
||||
/\ prop_state' = [prop_state EXCEPT ![p].nextSendLsn = next_send_lsn]
|
||||
/\ UNCHANGED <<committed, elected_history>>
|
||||
|
||||
\* Append new log entry to elected proposer
|
||||
NewEntry(p) ==
|
||||
/\ prop_state[p].state = "leader"
|
||||
/\ LET
|
||||
\* entry consists only of term, index serves as LSN.
|
||||
new_entry == prop_state[p].term
|
||||
IN
|
||||
/\ prop_state' = [prop_state EXCEPT ![p].wal = Append(prop_state[p].wal, new_entry)]
|
||||
/\ UNCHANGED <<acc_state, committed, elected_history>>
|
||||
|
||||
\* Immediately append next entry from elected proposer to acceptor a.
|
||||
AppendEntry(p, a) ==
|
||||
/\ prop_state[p].state = "leader"
|
||||
/\ acc_state[a].term = prop_state[p].term
|
||||
/\ prop_state[p].nextSendLsn[a] /= NULL \* did TruncateWal
|
||||
/\ prop_state[p].nextSendLsn[a] <= Len(prop_state[p].wal) \* have smth to send
|
||||
/\ LET
|
||||
send_lsn == prop_state[p].nextSendLsn[a]
|
||||
entry == prop_state[p].wal[send_lsn]
|
||||
\* Since message delivery is instant we don't check that send_lsn follows
|
||||
\* the last acc record, it must always be true.
|
||||
IN
|
||||
/\ prop_state' = [prop_state EXCEPT ![p].nextSendLsn[a] = send_lsn + 1]
|
||||
/\ acc_state' = [acc_state EXCEPT ![a].wal = Append(acc_state[a].wal, entry)]
|
||||
/\ UNCHANGED <<committed, elected_history>>
|
||||
|
||||
\* LSN where elected proposer p starts writing its records.
|
||||
PropStartLsn(p) ==
|
||||
IF prop_state[p].state = "leader" THEN prop_state[p].termHistory[Len(prop_state[p].termHistory)].lsn ELSE NULL
|
||||
|
||||
\* LSN which can be committed by proposer p using min quorum q (check that q
|
||||
\* forms quorum must have been done outside). NULL if there is none.
|
||||
QuorumCommitLsn(p, q) ==
|
||||
IF
|
||||
/\ prop_state[p].state = "leader"
|
||||
/\ \A a \in q:
|
||||
\* Without explicit responses to appends this ensures that append
|
||||
\* up to FlushLsn has been accepted.
|
||||
/\ acc_state[a].term = prop_state[p].term
|
||||
\* nextSendLsn existence means TruncateWal has happened, it ensures
|
||||
\* acceptor's WAL (and FlushLsn) are from proper proposer's history.
|
||||
\* Alternatively we could compare LastLogTerm here, but that's closer to
|
||||
\* what we do in the impl (we check flushLsn in AppendResponse, but
|
||||
\* AppendRequest is processed only if HandleElected handling was good).
|
||||
/\ prop_state[p].nextSendLsn[a] /= NULL
|
||||
THEN
|
||||
\* Now find the LSN present on all the quorum.
|
||||
LET quorum_lsn == Minimum({FlushLsn(a): a \in q}) IN
|
||||
\* This is the basic Raft rule of not committing entries from previous
|
||||
\* terms except along with current term entry (commit them only when
|
||||
\* quorum recovers, i.e. last_log_term on it reaches leader's term).
|
||||
IF quorum_lsn >= PropStartLsn(p) THEN
|
||||
quorum_lsn
|
||||
ELSE
|
||||
NULL
|
||||
ELSE
|
||||
NULL
|
||||
|
||||
\* Commit all entries on proposer p with record lsn < commit_lsn.
|
||||
DoCommitEntries(p, commit_lsn) ==
|
||||
/\ committed' = committed \cup {[term |-> prop_state[p].wal[lsn], lsn |-> lsn]: lsn \in 1..(commit_lsn - 1)}
|
||||
/\ UNCHANGED <<prop_state, acc_state, elected_history>>
|
||||
|
||||
\* Proposer p commits all entries it can using some quorum. Note that unlike
|
||||
\* will62794/logless-reconfig this allows to commit entries from previous terms
|
||||
\* (when conditions for that are met).
|
||||
CommitEntries(p) ==
|
||||
/\ prop_state[p].state = "leader"
|
||||
\* Using min quorums here is better because 1) QuorumCommitLsn for
|
||||
\* simplicity checks min across all accs in q. 2) it probably makes
|
||||
\* evaluation faster.
|
||||
/\ \E q \in AllMinQuorums(acceptors):
|
||||
LET commit_lsn == QuorumCommitLsn(p, q) IN
|
||||
/\ commit_lsn /= NULL
|
||||
/\ DoCommitEntries(p, commit_lsn)
|
||||
|
||||
\*******************************************************************************
|
||||
\* Final spec
|
||||
\*******************************************************************************
|
||||
|
||||
Next ==
|
||||
\/ \E p \in proposers: RestartProposer(p)
|
||||
\/ \E p \in proposers: \E a \in acceptors: Vote(p, a)
|
||||
\/ \E p \in proposers: BecomeLeader(p)
|
||||
\/ \E p \in proposers: \E a \in acceptors: UpdateTerm(p, a)
|
||||
\/ \E p \in proposers: \E a \in acceptors: TruncateWal(p, a)
|
||||
\/ \E p \in proposers: NewEntry(p)
|
||||
\/ \E p \in proposers: \E a \in acceptors: AppendEntry(p, a)
|
||||
\/ \E p \in proposers: CommitEntries(p)
|
||||
|
||||
Spec == Init /\ [][Next]_<<prop_state, acc_state, committed, elected_history>>
|
||||
|
||||
|
||||
\********************************************************************************
|
||||
\* Invariants
|
||||
\********************************************************************************
|
||||
|
||||
\* Lighter version of ElectionSafetyFull which doesn't require elected_history.
|
||||
ElectionSafety ==
|
||||
\A p1, p2 \in proposers:
|
||||
(/\ prop_state[p1].state = "leader"
|
||||
/\ prop_state[p2].state = "leader"
|
||||
/\ prop_state[p1].term = prop_state[p2].term) => (p1 = p2)
|
||||
|
||||
\* Single term must never be elected more than once.
|
||||
ElectionSafetyFull == \A term \in DOMAIN elected_history: elected_history[term] <= 1
|
||||
|
||||
\* Log is expected to be monotonic by <term, lsn> comparison. This is not true
|
||||
\* in variants of multi Paxos, but in Raft (and here) it is.
|
||||
LogIsMonotonic ==
|
||||
\A a \in acceptors:
|
||||
\A i, j \in DOMAIN acc_state[a].wal:
|
||||
(i > j) => (acc_state[a].wal[i] >= acc_state[a].wal[j])
|
||||
|
||||
\* Main invariant: If two entries are committed at the same LSN, they must be
|
||||
\* the same entry.
|
||||
LogSafety ==
|
||||
\A c1, c2 \in committed: (c1.lsn = c2.lsn) => (c1 = c2)
|
||||
|
||||
|
||||
\********************************************************************************
|
||||
\* Invariants which don't need to hold, but useful for playing/debugging.
|
||||
\********************************************************************************
|
||||
|
||||
\* Limits term of elected proposers
|
||||
MaxTerm == \A p \in proposers: (prop_state[p].state = "leader" => prop_state[p].term < 2)
|
||||
|
||||
MaxAccWalLen == \A a \in acceptors: Len(acc_state[a].wal) < 2
|
||||
|
||||
\* Limits max number of committed entries. That way we can check that we'are
|
||||
\* actually committing something.
|
||||
MaxCommitLsn == Cardinality(committed) < 2
|
||||
|
||||
\* How many records with different terms can be removed in single WAL
|
||||
\* truncation.
|
||||
MaxTruncatedTerms ==
|
||||
\A p \in proposers: \A a \in acceptors:
|
||||
(/\ prop_state[p].state = "leader"
|
||||
/\ prop_state[p].term = acc_state[a].term) =>
|
||||
LET
|
||||
hcp == FindHighestCommonPoint(prop_state[p].termHistory, AcceptorTermHistory(a), FlushLsn(a))
|
||||
truncated_lsns == {lsn \in DOMAIN acc_state[a].wal: lsn >= hcp.lsn}
|
||||
truncated_records_terms == {acc_state[a].wal[lsn]: lsn \in truncated_lsns}
|
||||
IN
|
||||
Cardinality(truncated_records_terms) < 2
|
||||
|
||||
\* Check that TruncateWal never deletes committed record.
|
||||
\* It might seem that this should an invariant, but it is not.
|
||||
\* With 5 nodes, it is legit to truncate record which had been
|
||||
\* globally committed: e.g. nodes abc can commit record of term 1 in
|
||||
\* term 3, and after that leader of term 2 can delete such record
|
||||
\* on d. On 10 cores TLC can find such a trace in ~7 hours.
|
||||
CommittedNotTruncated ==
|
||||
\A p \in proposers: \A a \in acceptors:
|
||||
(/\ prop_state[p].state = "leader"
|
||||
/\ prop_state[p].term = acc_state[a].term) =>
|
||||
LET
|
||||
hcp == FindHighestCommonPoint(prop_state[p].termHistory, AcceptorTermHistory(a), FlushLsn(a))
|
||||
truncated_lsns == {lsn \in DOMAIN acc_state[a].wal: lsn >= hcp.lsn}
|
||||
truncated_records == {[term |-> acc_state[a].wal[lsn], lsn |-> lsn]: lsn \in truncated_lsns}
|
||||
IN
|
||||
\A r \in truncated_records: r \notin committed
|
||||
|
||||
====
|
||||
51
safekeeper/spec/modelcheck.sh
Executable file
51
safekeeper/spec/modelcheck.sh
Executable file
@@ -0,0 +1,51 @@
|
||||
#!/bin/bash
|
||||
|
||||
# Usage: ./modelcheck.sh <config_file> <spec_file>, e.g.
|
||||
# ./modelcheck.sh models/MCProposerAcceptorStatic_p2_a3_t3_l3.cfg MCProposerAcceptorStatic.tla
|
||||
# ./modelcheck.sh models/MCProposerAcceptorReconfig_p2_a3_t3_l3_c3.cfg MCProposerAcceptorReconfig.tla
|
||||
CONFIG=$1
|
||||
SPEC=$2
|
||||
|
||||
MEM=7G
|
||||
TOOLSPATH="/opt/TLA+Toolbox/tla2tools.jar"
|
||||
|
||||
mkdir -p "tlc-results"
|
||||
CONFIG_FILE=$(basename -- "$CONFIG")
|
||||
outfilename="$SPEC-${CONFIG_FILE}-$(date --utc +%Y-%m-%d--%H-%M-%S)".log
|
||||
outfile="tlc-results/$outfilename"
|
||||
touch $outfile
|
||||
|
||||
# Save some info about the run.
|
||||
GIT_REV=`git rev-parse --short HEAD`
|
||||
INFO=`uname -a`
|
||||
|
||||
# First for Linux, second for Mac.
|
||||
CPUNAMELinux=$(lscpu | grep 'Model name' | cut -f 2 -d ":" | awk '{$1=$1}1')
|
||||
CPUCORESLinux=`nproc`
|
||||
CPUNAMEMac=`sysctl -n machdep.cpu.brand_string`
|
||||
CPUCORESMac=`sysctl -n machdep.cpu.thread_count`
|
||||
|
||||
echo "git revision: $GIT_REV" >> $outfile
|
||||
echo "Platform: $INFO" >> $outfile
|
||||
echo "CPU Info Linux: $CPUNAMELinux" >> $outfile
|
||||
echo "CPU Cores Linux: $CPUCORESLinux" >> $outfile
|
||||
echo "CPU Info Mac: $CPUNAMEMac" >> $outfile
|
||||
echo "CPU Cores Mac: $CPUCORESMac" >> $outfile
|
||||
echo "Spec: $SPEC" >> $outfile
|
||||
echo "Config: $CONFIG" >> $outfile
|
||||
echo "----" >> $outfile
|
||||
cat $CONFIG >> $outfile
|
||||
echo "" >> $outfile
|
||||
echo "----" >> $outfile
|
||||
echo "" >> $outfile
|
||||
|
||||
# see
|
||||
# https://lamport.azurewebsites.net/tla/current-tools.pdf
|
||||
# for TLC options.
|
||||
# OffHeapDiskFPSet is the optimal fingerprint set implementation
|
||||
# https://docs.tlapl.us/codebase:architecture#fingerprint_sets_fpsets
|
||||
#
|
||||
# Add -simulate to run in infinite simulation mode.
|
||||
# -coverage 1 is useful for profiling (check how many times actions are taken).
|
||||
java -Xmx$MEM -XX:MaxDirectMemorySize=$MEM -XX:+UseParallelGC -Dtlc2.tool.fp.FPSet.impl=tlc2.tool.fp.OffHeapDiskFPSet \
|
||||
-cp "${TOOLSPATH}" tlc2.TLC $SPEC -config $CONFIG -workers auto -gzip | tee -a $outfile
|
||||
@@ -0,0 +1,18 @@
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2}
|
||||
max_term = 2
|
||||
max_entries = 2
|
||||
max_generation = 3
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafetyFull
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
\* CommittedNotTruncated
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
@@ -0,0 +1,18 @@
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2}
|
||||
max_term = 2
|
||||
max_entries = 2
|
||||
max_generation = 5
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafetyFull
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
\* CommittedNotTruncated
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
@@ -0,0 +1,19 @@
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3}
|
||||
max_term = 2
|
||||
max_entries = 2
|
||||
max_generation = 3
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafetyFull
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
CommittedNotTruncated
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
|
||||
@@ -0,0 +1,18 @@
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3, a4}
|
||||
max_term = 2
|
||||
max_entries = 2
|
||||
max_generation = 3
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafetyFull
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
|
||||
@@ -0,0 +1,19 @@
|
||||
\* A very small model just to play.
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3}
|
||||
max_term = 2
|
||||
max_entries = 2
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafetyFull
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
CommittedNotTruncated
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
|
||||
@@ -0,0 +1,19 @@
|
||||
\* A model next to the smallest one.
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3}
|
||||
max_term = 3
|
||||
max_entries = 2
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafetyFull
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
CommittedNotTruncated
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
|
||||
@@ -0,0 +1,17 @@
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3}
|
||||
max_term = 3
|
||||
max_entries = 3
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafety
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
CommittedNotTruncated
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
@@ -0,0 +1,17 @@
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3}
|
||||
max_term = 4
|
||||
max_entries = 4
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafety
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
CommittedNotTruncated
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
@@ -0,0 +1,16 @@
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3, a4, a5}
|
||||
max_term = 2
|
||||
max_entries = 2
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafety
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
@@ -0,0 +1,16 @@
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3, a4, a5}
|
||||
max_term = 3
|
||||
max_entries = 3
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafety
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
@@ -0,0 +1,16 @@
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3, a4, a5}
|
||||
max_term = 4
|
||||
max_entries = 3
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafety
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
12
safekeeper/spec/readme.md
Normal file
12
safekeeper/spec/readme.md
Normal file
@@ -0,0 +1,12 @@
|
||||
The specifications, models and results of running of them of the compute <->
|
||||
safekeepers consensus algorithm for committing WAL on the fleet of safekeepers.
|
||||
Following Paxos parlance, compute which writes WAL is called (WAL) proposer here
|
||||
and safekeepers which persist it are called (WAL) acceptors.
|
||||
|
||||
Directory structure:
|
||||
- Use modelcheck.sh to run TLC.
|
||||
- MC*.tla contains bits of TLA+ needed for TLC like constraining the state space, and models/ actual models.
|
||||
- Other .tla files are the actual specs.
|
||||
|
||||
Structure is partially borrowed from
|
||||
[logless-reconfig](https://github.com/will62794/logless-reconfig), thanks to it.
|
||||
@@ -0,0 +1,63 @@
|
||||
git revision: 864f4667d
|
||||
Platform: Linux neon-dev-arm64-1 6.8.0-48-generic #48-Ubuntu SMP PREEMPT_DYNAMIC Fri Sep 27 14:35:45 UTC 2024 aarch64 aarch64 aarch64 GNU/Linux
|
||||
CPU Info Linux: Neoverse-N1
|
||||
CPU Cores Linux: 80
|
||||
CPU Info Mac:
|
||||
CPU Cores Mac:
|
||||
Spec: MCProposerAcceptorStatic.tla
|
||||
Config: models/MCProposerAcceptorStatic_p2_a3_t2_l2.cfg
|
||||
----
|
||||
\* A very small model just to play.
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3}
|
||||
max_term = 2
|
||||
max_entries = 2
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafety
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
CommittedNotTruncated
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
|
||||
|
||||
----
|
||||
|
||||
TLC2 Version 2.20 of Day Month 20?? (rev: f68cb71)
|
||||
Running breadth-first search Model-Checking with fp 110 and seed 3949669318051689745 with 80 workers on 80 cores with 54613MB heap and 61440MB offheap memory [pid: 46037] (Linux 6.8.0-48-generic aarch64, Ubuntu 21.0.4 x86_64, OffHeapDiskFPSet, DiskStateQueue).
|
||||
Parsing file /home/arseny/neon/safekeeper/spec/MCProposerAcceptorStatic.tla
|
||||
Parsing file /tmp/tlc-11123278435718411444/TLC.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
|
||||
Parsing file /home/arseny/neon/safekeeper/spec/ProposerAcceptorStatic.tla
|
||||
Parsing file /tmp/tlc-11123278435718411444/_TLCTrace.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
|
||||
Parsing file /tmp/tlc-11123278435718411444/Integers.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
|
||||
Parsing file /tmp/tlc-11123278435718411444/Sequences.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
|
||||
Parsing file /tmp/tlc-11123278435718411444/FiniteSets.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
|
||||
Parsing file /tmp/tlc-11123278435718411444/Naturals.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
|
||||
Parsing file /tmp/tlc-11123278435718411444/TLCExt.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
|
||||
Semantic processing of module Naturals
|
||||
Semantic processing of module Sequences
|
||||
Semantic processing of module FiniteSets
|
||||
Semantic processing of module TLC
|
||||
Semantic processing of module Integers
|
||||
Semantic processing of module ProposerAcceptorStatic
|
||||
Semantic processing of module TLCExt
|
||||
Semantic processing of module _TLCTrace
|
||||
Semantic processing of module MCProposerAcceptorStatic
|
||||
Starting... (2024-11-06 13:44:18)
|
||||
Computing initial states...
|
||||
Finished computing initial states: 1 distinct state generated at 2024-11-06 13:44:20.
|
||||
Model checking completed. No error has been found.
|
||||
Estimates of the probability that TLC did not check all reachable states
|
||||
because two distinct states had the same fingerprint:
|
||||
calculated (optimistic): val = 2.9E-9
|
||||
based on the actual fingerprints: val = 4.1E-10
|
||||
922134 states generated, 61249 distinct states found, 0 states left on queue.
|
||||
The depth of the complete state graph search is 31.
|
||||
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 6 and the 95th percentile is 3).
|
||||
Finished in 11s at (2024-11-06 13:44:28)
|
||||
@@ -0,0 +1,69 @@
|
||||
git revision: bcbff084a
|
||||
Platform: Linux nonlibrem 6.10.11-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.10.11-1 (2024-09-22) x86_64 GNU/Linux
|
||||
CPU Info Linux: 13th Gen Intel(R) Core(TM) i7-1355U
|
||||
CPU Cores Linux: 10
|
||||
CPU Info Mac:
|
||||
CPU Cores Mac:
|
||||
Spec: MCProposerAcceptorStatic.tla
|
||||
Config: models/MCProposerAcceptorStatic_p2_a3_t3_l2.cfg
|
||||
----
|
||||
\* A model next to the smallest one.
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3}
|
||||
max_term = 3
|
||||
max_entries = 2
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafety
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
CommittedNotTruncated
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
|
||||
|
||||
----
|
||||
|
||||
TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef)
|
||||
Running breadth-first search Model-Checking with fp 41 and seed -3061068726727581619 with 10 workers on 10 cores with 6372MB heap and 7168MB offheap memory [pid: 1250346] (Linux 6.10.11-amd64 amd64, Debian 21.0.5 x86_64, OffHeapDiskFPSet, DiskStateQueue).
|
||||
Parsing file /home/ars/neon/neon/safekeeper/spec/MCProposerAcceptorStatic.tla
|
||||
Parsing file /tmp/tlc-3023124431504466774/TLC.tla (jar:file:/opt/TLA+Toolbox/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
|
||||
Parsing file /home/ars/neon/neon/safekeeper/spec/ProposerAcceptorStatic.tla
|
||||
Parsing file /tmp/tlc-3023124431504466774/_TLCTrace.tla (jar:file:/opt/TLA+Toolbox/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
|
||||
Parsing file /tmp/tlc-3023124431504466774/Integers.tla (jar:file:/opt/TLA+Toolbox/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
|
||||
Parsing file /tmp/tlc-3023124431504466774/Sequences.tla (jar:file:/opt/TLA+Toolbox/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
|
||||
Parsing file /tmp/tlc-3023124431504466774/FiniteSets.tla (jar:file:/opt/TLA+Toolbox/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
|
||||
Parsing file /tmp/tlc-3023124431504466774/Naturals.tla (jar:file:/opt/TLA+Toolbox/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
|
||||
Parsing file /tmp/tlc-3023124431504466774/TLCExt.tla (jar:file:/opt/TLA+Toolbox/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
|
||||
Semantic processing of module Naturals
|
||||
Semantic processing of module Sequences
|
||||
Semantic processing of module FiniteSets
|
||||
Semantic processing of module TLC
|
||||
Semantic processing of module Integers
|
||||
Semantic processing of module ProposerAcceptorStatic
|
||||
Semantic processing of module TLCExt
|
||||
Semantic processing of module _TLCTrace
|
||||
Semantic processing of module MCProposerAcceptorStatic
|
||||
Starting... (2024-11-15 12:09:59)
|
||||
Computing initial states...
|
||||
Finished computing initial states: 1 distinct state generated at 2024-11-15 12:10:00.
|
||||
Progress(19) at 2024-11-15 12:10:03: 464,696 states generated (464,696 s/min), 57,859 distinct states found (57,859 ds/min), 21,435 states left on queue.
|
||||
Progress(26) at 2024-11-15 12:11:03: 8,813,399 states generated (8,348,703 s/min), 877,254 distinct states found (819,395 ds/min), 214,794 states left on queue.
|
||||
Progress(27) at 2024-11-15 12:12:03: 16,121,858 states generated (7,308,459 s/min), 1,464,707 distinct states found (587,453 ds/min), 274,230 states left on queue.
|
||||
Progress(29) at 2024-11-15 12:13:03: 23,073,903 states generated (6,952,045 s/min), 1,948,802 distinct states found (484,095 ds/min), 263,697 states left on queue.
|
||||
Progress(31) at 2024-11-15 12:14:03: 29,740,681 states generated (6,666,778 s/min), 2,331,052 distinct states found (382,250 ds/min), 185,484 states left on queue.
|
||||
Progress(34) at 2024-11-15 12:15:03: 36,085,876 states generated (6,345,195 s/min), 2,602,370 distinct states found (271,318 ds/min), 31,659 states left on queue.
|
||||
Model checking completed. No error has been found.
|
||||
Estimates of the probability that TLC did not check all reachable states
|
||||
because two distinct states had the same fingerprint:
|
||||
calculated (optimistic): val = 4.9E-6
|
||||
based on the actual fingerprints: val = 6.9E-7
|
||||
36896322 states generated, 2623542 distinct states found, 0 states left on queue.
|
||||
The depth of the complete state graph search is 39.
|
||||
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 7 and the 95th percentile is 3).
|
||||
Finished in 05min 14s at (2024-11-15 12:15:13)
|
||||
@@ -0,0 +1,72 @@
|
||||
git revision: 864f4667d
|
||||
Platform: Linux neon-dev-arm64-1 6.8.0-48-generic #48-Ubuntu SMP PREEMPT_DYNAMIC Fri Sep 27 14:35:45 UTC 2024 aarch64 aarch64 aarch64 GNU/Linux
|
||||
CPU Info Linux: Neoverse-N1
|
||||
CPU Cores Linux: 80
|
||||
CPU Info Mac:
|
||||
CPU Cores Mac:
|
||||
Spec: MCProposerAcceptorStatic.tla
|
||||
Config: models/MCProposerAcceptorStatic_p2_a3_t3_l3.cfg
|
||||
----
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3}
|
||||
max_term = 3
|
||||
max_entries = 3
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafety
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
CommittedNotTruncated
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
|
||||
----
|
||||
|
||||
TLC2 Version 2.20 of Day Month 20?? (rev: f68cb71)
|
||||
Running breadth-first search Model-Checking with fp 126 and seed 2302892334567572769 with 80 workers on 80 cores with 54613MB heap and 61440MB offheap memory [pid: 39701] (Linux 6.8.0-48-generic aarch64, Ubuntu 21.0.4 x86_64, OffHeapDiskFPSet, DiskStateQueue).
|
||||
Parsing file /home/arseny/neon/safekeeper/spec/MCProposerAcceptorStatic.tla
|
||||
Parsing file /tmp/tlc-15178810317173795942/TLC.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
|
||||
Parsing file /home/arseny/neon/safekeeper/spec/ProposerAcceptorStatic.tla
|
||||
Parsing file /tmp/tlc-15178810317173795942/_TLCTrace.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
|
||||
Parsing file /tmp/tlc-15178810317173795942/Integers.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
|
||||
Parsing file /tmp/tlc-15178810317173795942/Sequences.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
|
||||
Parsing file /tmp/tlc-15178810317173795942/FiniteSets.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
|
||||
Parsing file /tmp/tlc-15178810317173795942/Naturals.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
|
||||
Parsing file /tmp/tlc-15178810317173795942/TLCExt.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
|
||||
Semantic processing of module Naturals
|
||||
Semantic processing of module Sequences
|
||||
Semantic processing of module FiniteSets
|
||||
Semantic processing of module TLC
|
||||
Semantic processing of module Integers
|
||||
Semantic processing of module ProposerAcceptorStatic
|
||||
Semantic processing of module TLCExt
|
||||
Semantic processing of module _TLCTrace
|
||||
Semantic processing of module MCProposerAcceptorStatic
|
||||
Starting... (2024-11-06 13:03:52)
|
||||
Computing initial states...
|
||||
Finished computing initial states: 1 distinct state generated at 2024-11-06 13:03:55.
|
||||
Progress(21) at 2024-11-06 13:03:58: 846,240 states generated (846,240 s/min), 106,298 distinct states found (106,298 ds/min), 41,028 states left on queue.
|
||||
Progress(28) at 2024-11-06 13:04:58: 27,538,211 states generated (26,691,971 s/min), 2,768,793 distinct states found (2,662,495 ds/min), 782,984 states left on queue.
|
||||
Progress(30) at 2024-11-06 13:05:58: 54,048,763 states generated (26,510,552 s/min), 5,076,745 distinct states found (2,307,952 ds/min), 1,241,301 states left on queue.
|
||||
Progress(31) at 2024-11-06 13:06:58: 80,554,724 states generated (26,505,961 s/min), 7,199,201 distinct states found (2,122,456 ds/min), 1,541,574 states left on queue.
|
||||
Progress(32) at 2024-11-06 13:07:58: 106,991,261 states generated (26,436,537 s/min), 9,121,549 distinct states found (1,922,348 ds/min), 1,686,289 states left on queue.
|
||||
Progress(33) at 2024-11-06 13:08:58: 133,354,665 states generated (26,363,404 s/min), 10,935,451 distinct states found (1,813,902 ds/min), 1,739,977 states left on queue.
|
||||
Progress(34) at 2024-11-06 13:09:58: 159,631,385 states generated (26,276,720 s/min), 12,605,372 distinct states found (1,669,921 ds/min), 1,677,447 states left on queue.
|
||||
Progress(35) at 2024-11-06 13:10:58: 185,862,196 states generated (26,230,811 s/min), 14,138,409 distinct states found (1,533,037 ds/min), 1,501,760 states left on queue.
|
||||
Progress(36) at 2024-11-06 13:11:58: 212,021,688 states generated (26,159,492 s/min), 15,538,990 distinct states found (1,400,581 ds/min), 1,216,621 states left on queue.
|
||||
Progress(37) at 2024-11-06 13:12:58: 238,046,160 states generated (26,024,472 s/min), 16,778,583 distinct states found (1,239,593 ds/min), 797,230 states left on queue.
|
||||
Progress(39) at 2024-11-06 13:13:58: 263,931,163 states generated (25,885,003 s/min), 17,820,786 distinct states found (1,042,203 ds/min), 209,400 states left on queue.
|
||||
Model checking completed. No error has been found.
|
||||
Estimates of the probability that TLC did not check all reachable states
|
||||
because two distinct states had the same fingerprint:
|
||||
calculated (optimistic): val = 2.5E-4
|
||||
based on the actual fingerprints: val = 7.9E-5
|
||||
270257170 states generated, 18005639 distinct states found, 0 states left on queue.
|
||||
The depth of the complete state graph search is 47.
|
||||
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 7 and the 95th percentile is 3).
|
||||
Finished in 10min 25s at (2024-11-06 13:14:17)
|
||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
@@ -0,0 +1,89 @@
|
||||
git revision: 864f4667d
|
||||
Platform: Linux neon-dev-arm64-1 6.8.0-48-generic #48-Ubuntu SMP PREEMPT_DYNAMIC Fri Sep 27 14:35:45 UTC 2024 aarch64 aarch64 aarch64 GNU/Linux
|
||||
CPU Info Linux: Neoverse-N1
|
||||
CPU Cores Linux: 80
|
||||
CPU Info Mac:
|
||||
CPU Cores Mac:
|
||||
Spec: MCProposerAcceptorStatic.tla
|
||||
Config: models/MCProposerAcceptorStatic_p2_a5_t2_l2.cfg
|
||||
----
|
||||
CONSTANTS
|
||||
NULL = NULL
|
||||
proposers = {p1, p2}
|
||||
acceptors = {a1, a2, a3, a4, a5}
|
||||
max_term = 2
|
||||
max_entries = 2
|
||||
SPECIFICATION Spec
|
||||
CONSTRAINT StateConstraint
|
||||
INVARIANT
|
||||
TypeOk
|
||||
ElectionSafety
|
||||
LogIsMonotonic
|
||||
LogSafety
|
||||
SYMMETRY ProposerAcceptorSymmetry
|
||||
CHECK_DEADLOCK FALSE
|
||||
ALIAS Alias
|
||||
|
||||
----
|
||||
|
||||
TLC2 Version 2.20 of Day Month 20?? (rev: f68cb71)
|
||||
Running breadth-first search Model-Checking with fp 90 and seed 2164066158568118414 with 80 workers on 80 cores with 54613MB heap and 61440MB offheap memory [pid: 30788] (Linux 6.8.0-48-generic aarch64, Ubuntu 21.0.4 x86_64, OffHeapDiskFPSet, DiskStateQueue).
|
||||
Parsing file /home/arseny/neon/safekeeper/spec/MCProposerAcceptorStatic.tla
|
||||
Parsing file /tmp/tlc-13824636513165485309/TLC.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
|
||||
Parsing file /home/arseny/neon/safekeeper/spec/ProposerAcceptorStatic.tla
|
||||
Parsing file /tmp/tlc-13824636513165485309/_TLCTrace.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
|
||||
Parsing file /tmp/tlc-13824636513165485309/Integers.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
|
||||
Parsing file /tmp/tlc-13824636513165485309/Sequences.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
|
||||
Parsing file /tmp/tlc-13824636513165485309/FiniteSets.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
|
||||
Parsing file /tmp/tlc-13824636513165485309/Naturals.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
|
||||
Parsing file /tmp/tlc-13824636513165485309/TLCExt.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
|
||||
Semantic processing of module Naturals
|
||||
Semantic processing of module Sequences
|
||||
Semantic processing of module FiniteSets
|
||||
Semantic processing of module TLC
|
||||
Semantic processing of module Integers
|
||||
Semantic processing of module ProposerAcceptorStatic
|
||||
Semantic processing of module TLCExt
|
||||
Semantic processing of module _TLCTrace
|
||||
Semantic processing of module MCProposerAcceptorStatic
|
||||
Starting... (2024-11-06 12:09:33)
|
||||
Computing initial states...
|
||||
Finished computing initial states: 1 distinct state generated at 2024-11-06 12:09:36.
|
||||
Progress(16) at 2024-11-06 12:09:39: 405,675 states generated (405,675 s/min), 18,042 distinct states found (18,042 ds/min), 7,612 states left on queue.
|
||||
Progress(23) at 2024-11-06 12:10:39: 12,449,257 states generated (12,043,582 s/min), 467,293 distinct states found (449,251 ds/min), 161,057 states left on queue.
|
||||
Progress(25) at 2024-11-06 12:11:39: 24,461,332 states generated (12,012,075 s/min), 861,011 distinct states found (393,718 ds/min), 267,072 states left on queue.
|
||||
Progress(26) at 2024-11-06 12:12:39: 36,440,377 states generated (11,979,045 s/min), 1,234,052 distinct states found (373,041 ds/min), 355,372 states left on queue.
|
||||
Progress(26) at 2024-11-06 12:13:39: 48,327,873 states generated (11,887,496 s/min), 1,583,736 distinct states found (349,684 ds/min), 425,209 states left on queue.
|
||||
Progress(27) at 2024-11-06 12:14:39: 60,246,136 states generated (11,918,263 s/min), 1,933,499 distinct states found (349,763 ds/min), 494,269 states left on queue.
|
||||
Progress(28) at 2024-11-06 12:15:39: 71,977,716 states generated (11,731,580 s/min), 2,265,302 distinct states found (331,803 ds/min), 553,777 states left on queue.
|
||||
Progress(28) at 2024-11-06 12:16:39: 83,644,537 states generated (11,666,821 s/min), 2,575,451 distinct states found (310,149 ds/min), 594,142 states left on queue.
|
||||
Progress(29) at 2024-11-06 12:17:39: 95,287,089 states generated (11,642,552 s/min), 2,888,793 distinct states found (313,342 ds/min), 639,273 states left on queue.
|
||||
Progress(29) at 2024-11-06 12:18:39: 107,000,972 states generated (11,713,883 s/min), 3,194,255 distinct states found (305,462 ds/min), 673,353 states left on queue.
|
||||
Progress(29) at 2024-11-06 12:19:39: 118,305,248 states generated (11,304,276 s/min), 3,467,775 distinct states found (273,520 ds/min), 692,915 states left on queue.
|
||||
Progress(29) at 2024-11-06 12:20:39: 129,954,327 states generated (11,649,079 s/min), 3,763,186 distinct states found (295,411 ds/min), 720,349 states left on queue.
|
||||
Progress(29) at 2024-11-06 12:21:39: 141,251,359 states generated (11,297,032 s/min), 4,020,407 distinct states found (257,221 ds/min), 724,036 states left on queue.
|
||||
Progress(30) at 2024-11-06 12:22:39: 152,551,873 states generated (11,300,514 s/min), 4,284,278 distinct states found (263,871 ds/min), 733,726 states left on queue.
|
||||
Progress(30) at 2024-11-06 12:23:39: 164,324,788 states generated (11,772,915 s/min), 4,569,569 distinct states found (285,291 ds/min), 746,476 states left on queue.
|
||||
Progress(30) at 2024-11-06 12:24:39: 175,121,317 states generated (10,796,529 s/min), 4,779,505 distinct states found (209,936 ds/min), 723,070 states left on queue.
|
||||
Progress(31) at 2024-11-06 12:25:39: 186,238,236 states generated (11,116,919 s/min), 5,016,034 distinct states found (236,529 ds/min), 712,944 states left on queue.
|
||||
Progress(31) at 2024-11-06 12:26:39: 197,884,578 states generated (11,646,342 s/min), 5,276,094 distinct states found (260,060 ds/min), 705,471 states left on queue.
|
||||
Progress(31) at 2024-11-06 12:27:39: 208,535,096 states generated (10,650,518 s/min), 5,463,450 distinct states found (187,356 ds/min), 665,661 states left on queue.
|
||||
Progress(32) at 2024-11-06 12:28:39: 219,424,829 states generated (10,889,733 s/min), 5,673,673 distinct states found (210,223 ds/min), 637,975 states left on queue.
|
||||
Progress(32) at 2024-11-06 12:29:39: 230,906,372 states generated (11,481,543 s/min), 5,903,516 distinct states found (229,843 ds/min), 606,255 states left on queue.
|
||||
Progress(33) at 2024-11-06 12:30:39: 241,261,887 states generated (10,355,515 s/min), 6,065,731 distinct states found (162,215 ds/min), 552,728 states left on queue.
|
||||
Progress(33) at 2024-11-06 12:31:39: 252,028,921 states generated (10,767,034 s/min), 6,255,487 distinct states found (189,756 ds/min), 509,620 states left on queue.
|
||||
Progress(33) at 2024-11-06 12:32:39: 262,856,171 states generated (10,827,250 s/min), 6,431,063 distinct states found (175,576 ds/min), 448,834 states left on queue.
|
||||
Progress(34) at 2024-11-06 12:33:39: 273,211,882 states generated (10,355,711 s/min), 6,586,644 distinct states found (155,581 ds/min), 386,905 states left on queue.
|
||||
Progress(34) at 2024-11-06 12:34:39: 283,843,415 states generated (10,631,533 s/min), 6,743,916 distinct states found (157,272 ds/min), 315,135 states left on queue.
|
||||
Progress(35) at 2024-11-06 12:35:39: 293,931,115 states generated (10,087,700 s/min), 6,878,405 distinct states found (134,489 ds/min), 241,126 states left on queue.
|
||||
Progress(36) at 2024-11-06 12:36:39: 303,903,441 states generated (9,972,326 s/min), 6,996,394 distinct states found (117,989 ds/min), 152,775 states left on queue.
|
||||
Progress(37) at 2024-11-06 12:37:39: 313,501,886 states generated (9,598,445 s/min), 7,093,031 distinct states found (96,637 ds/min), 54,009 states left on queue.
|
||||
Model checking completed. No error has been found.
|
||||
Estimates of the probability that TLC did not check all reachable states
|
||||
because two distinct states had the same fingerprint:
|
||||
calculated (optimistic): val = 1.2E-4
|
||||
based on the actual fingerprints: val = 2.1E-6
|
||||
318172398 states generated, 7127950 distinct states found, 0 states left on queue.
|
||||
The depth of the complete state graph search is 44.
|
||||
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 9 and the 95th percentile is 3).
|
||||
Finished in 28min 43s at (2024-11-06 12:38:16)
|
||||
Reference in New Issue
Block a user