FinishChange

safekeeper/spec/ProposerAcceptorReconfig.tla

@@ -171,6 +171,42 @@ StartChange(new_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>>
+
+
 \*******************************************************************************
 \* Final spec
 \*******************************************************************************
@@ -186,6 +222,7 @@ Next ==
   \/ \E p \in proposers: CommitEntries(p)
   \/ \E p \in proposers: \E a \in acceptors: ProposerBumpConf(p, a)
   \/ \E new_members \in SUBSET acceptors: StartChange(new_members)
+  \/ FinishChange
 
 Spec == Init /\ [][Next]_<<prop_state, acc_state, committed, elected_history, prop_conf, acc_conf, conf_store>>
 

safekeeper/spec/ProposerAcceptorStatic.tla

@@ -224,7 +224,16 @@ RestartProposer(p) ==
             RestartProposerWithTerm(p, new_term)
 
 \* Term history of acceptor a's WAL: the one saved truncated to contain only <=
-\* local FlushLsn entries.
+\* 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))
 
@@ -243,17 +252,27 @@ Vote(p, a) ==
 \* 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)
+
 \* 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 ==
-             CHOOSE a \in DOMAIN prop_state[p].votes:
-                 LET v == prop_state[p].votes[a]
-                 IN \A v2 \in Range(prop_state[p].votes):
-                        /\ LastLogTerm(v.termHistory) >= LastLogTerm(v2.termHistory)
-                        /\ (LastLogTerm(v.termHistory) = LastLogTerm(v2.termHistory) => v.flushLsn >= v2.flushLsn)
+            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)
         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