From 6b62b7633b161cb7be1efe522206ba3cf07357f7 Mon Sep 17 00:00:00 2001 From: Arseny Sher Date: Mon, 25 Nov 2024 13:19:58 +0300 Subject: [PATCH] address review --- safekeeper/spec/MCProposerAcceptorStatic.tla | 5 +++++ safekeeper/spec/ProposerAcceptorStatic.tla | 10 ++++++---- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/safekeeper/spec/MCProposerAcceptorStatic.tla b/safekeeper/spec/MCProposerAcceptorStatic.tla index 713574ffb3..772e0e588d 100644 --- a/safekeeper/spec/MCProposerAcceptorStatic.tla +++ b/safekeeper/spec/MCProposerAcceptorStatic.tla @@ -14,9 +14,14 @@ ASSUME max_entries \in Nat /\ max_term \in Nat StateConstraint == \A p \in proposers: /\ prop_state[p].term <= max_term /\ Len(prop_state[p].wal) <= max_entries +\* All 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, acc_state |-> acc_state, diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla index 2503245503..2d38e1490e 100644 --- a/safekeeper/spec/ProposerAcceptorStatic.tla +++ b/safekeeper/spec/ProposerAcceptorStatic.tla @@ -249,9 +249,9 @@ BecomeLeader(p) == \* 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 - \* 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). + \* 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, @@ -336,7 +336,7 @@ AppendEntry(p, a) == \* LSN where elected proposer p starts writing its records. PropStartLsn(p) == - prop_state[p].termHistory[Len(prop_state[p].termHistory)].lsn + IF prop_state[p].state = "leader" THEN prop_state[p].termHistory[Len(prop_state[p].termHistory)].lsn ELSE NULL \* Proposer p commits all entries it can using quorum q. Note that unlike \* will62794/logless-reconfig this allows to commit entries from previous terms @@ -391,6 +391,8 @@ ElectionSafety == \* 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 comparison. This is not true +\* in variants of multi Paxos, but in Raft (and here) it is. LogIsMonotonic == \A a \in acceptors: \A i \in DOMAIN acc_state[a].wal: \A j \in DOMAIN acc_state[a].wal: