Start reconfig

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
+         ]
+
+====

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 <<prop_state, acc_state, committed, elected_history, prop_conf, acc_conf>>
+
+\*******************************************************************************
+\* 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]_<<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
+
+====

safekeeper/spec/modelcheck.sh

@@ -2,6 +2,7 @@
 
 # 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
 

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
+