From c940f196ce97ca7180c414ec3b76999f93bfff53 Mon Sep 17 00:00:00 2001 From: Arseny Sher Date: Tue, 26 Nov 2024 15:00:16 +0300 Subject: [PATCH] Start reconfig --- .../spec/MCProposerAcceptorReconfig.tla | 41 +++++++ safekeeper/spec/ProposerAcceptorReconfig.tla | 104 ++++++++++++++++++ safekeeper/spec/modelcheck.sh | 1 + ...roposerAcceptorReconfig_p2_a3_t2_l2_c3.cfg | 20 ++++ 4 files changed, 166 insertions(+) create mode 100644 safekeeper/spec/MCProposerAcceptorReconfig.tla create mode 100644 safekeeper/spec/ProposerAcceptorReconfig.tla create mode 100644 safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a3_t2_l2_c3.cfg diff --git a/safekeeper/spec/MCProposerAcceptorReconfig.tla b/safekeeper/spec/MCProposerAcceptorReconfig.tla new file mode 100644 index 0000000000..a4b25e383a --- /dev/null +++ b/safekeeper/spec/MCProposerAcceptorReconfig.tla @@ -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 + ] + +==== diff --git a/safekeeper/spec/ProposerAcceptorReconfig.tla b/safekeeper/spec/ProposerAcceptorReconfig.tla new file mode 100644 index 0000000000..b150d82fad --- /dev/null +++ b/safekeeper/spec/ProposerAcceptorReconfig.tla @@ -0,0 +1,104 @@ +---- MODULE ProposerAcceptorReconfig ---- + +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. For some operators this makes sense and for some (which we don' +\* use here and mostly create own versions of them) it doesn't. +PAS == INSTANCE ProposerAcceptorStatic + +\* Is c a valid config? +IsConfig(c) == + /\ DOMAIN c = {"generation", "members", "newMembers"} + /\ 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: + \/ prop_conf[p] = NULL + \/ IsConfig(prop_conf[p]) + /\ \A a \in acceptors: IsConfig(acc_conf[a]) + /\ IsConfig(conf_store) + +\******************************************************************************** +\* Initial +\******************************************************************************** + +Init == + /\ PAS!Init + /\ prop_conf = [p \in proposers |-> NULL] + /\ \E init_members \in SUBSET acceptors: + LET init_conf == [generation |-> 1, members |-> init_members, newMembers |-> NULL] IN + /\ acc_conf = [a \in acceptors |-> init_conf] + /\ conf_store = init_conf + +\******************************************************************************** +\* Actions +\******************************************************************************** + +\* 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 + /\ conf_store' = [generation |-> conf_store.generation + 1, members |-> conf_store.members, newMembers |-> new_members] + /\ UNCHANGED <> + +\******************************************************************************* +\* Final spec +\******************************************************************************* + +Next == + \/ \E new_members \in SUBSET acceptors: StartChange(new_members) +\* \/ \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: TruncateWal(p, a) +\* \/ \E p \in proposers: NewEntry(p) +\* \/ \E p \in proposers: \E a \in acceptors: AppendEntry(p, a) +\* \/ \E q \in Quorums: \E p \in proposers: CommitEntries(p, q) + +Spec == Init /\ [][Next]_<> + +\******************************************************************************** +\* 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 + +==== diff --git a/safekeeper/spec/modelcheck.sh b/safekeeper/spec/modelcheck.sh index 21ead7dad8..2b9ba0e071 100755 --- a/safekeeper/spec/modelcheck.sh +++ b/safekeeper/spec/modelcheck.sh @@ -2,6 +2,7 @@ # Usage: ./modelcheck.sh , 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 diff --git a/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a3_t2_l2_c3.cfg b/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a3_t2_l2_c3.cfg new file mode 100644 index 0000000000..8e59737af0 --- /dev/null +++ b/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a3_t2_l2_c3.cfg @@ -0,0 +1,20 @@ +\* A very small model just to play. +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 +