From c90a7d6e9cfa0a25d353718bc05a25ba4ec2ff13 Mon Sep 17 00:00:00 2001 From: Arseny Sher Date: Fri, 15 Nov 2024 12:05:24 +0300 Subject: [PATCH] Add elected_history --- safekeeper/spec/ProposerAcceptorStatic.tla | 46 +++++++++++++++++----- 1 file changed, 36 insertions(+), 10 deletions(-) diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla index c3f1c7a3a118..2503245503ef 100644 --- a/safekeeper/spec/ProposerAcceptorStatic.tla +++ b/safekeeper/spec/ProposerAcceptorStatic.tla @@ -28,7 +28,8 @@ 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 <> entries + committed, \* bag (set) of ever committed <> entries + elected_history \* counter for elected terms, see TypeOk for details CONSTANT acceptors, @@ -62,6 +63,11 @@ 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 + \***************** NumAccs == Cardinality(acceptors) @@ -141,6 +147,21 @@ TypeOk == /\ \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 , 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 @@ -167,6 +188,7 @@ Init == wal |-> << >> ]] /\ committed = {} + /\ elected_history = EmptyF \******************************************************************************** @@ -188,7 +210,7 @@ RestartProposer(p, q) == ![p].termHistory = << >>, ![p].wal = << >>, ![p].nextSendLsn = EmptyF] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Term history of acceptor a's WAL: the one saved truncated to contain only <= \* local FlushLsn entries. @@ -204,7 +226,7 @@ Vote(p, a) == vote == [termHistory |-> AcceptorTermHistory(a), flushLsn |-> FlushLsn(a)] IN prop_state' = [prop_state EXCEPT ![p].votes = (a :> vote) @@ prop_state[p].votes] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Get lastLogTerm from term history th. @@ -235,6 +257,7 @@ BecomeLeader(p) == ![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 <> @@ -245,7 +268,7 @@ 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 <> + /\ UNCHANGED <> \* Find highest common point (LSN of the first divergent record) in the logs of \* proposer p and acceptor a. Returns of the highest common point. @@ -283,7 +306,7 @@ TruncateWal(p, a) == ![a].wal = SubSeq(acc_state[a].wal, 1, hcp.lsn - 1) ] /\ prop_state' = [prop_state EXCEPT ![p].nextSendLsn = next_send_lsn] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Append new log entry to elected proposer NewEntry(p) == @@ -293,7 +316,7 @@ NewEntry(p) == new_entry == prop_state[p].term IN /\ prop_state' = [prop_state EXCEPT ![p].wal = Append(prop_state[p].wal, new_entry)] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Immediately append next entry from elected proposer to acceptor a. AppendEntry(p, a) == @@ -309,7 +332,7 @@ AppendEntry(p, a) == 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 <> + /\ UNCHANGED <> \* LSN where elected proposer p starts writing its records. PropStartLsn(p) == @@ -335,7 +358,7 @@ CommitEntries(p, q) == \* quorum recovers, i.e. last_log_term on it reaches leader's term). /\ quorum_lsn >= PropStartLsn(p) /\ committed' = committed \cup {[term |-> prop_state[p].wal[lsn], lsn |-> lsn]: lsn \in 1..(quorum_lsn - 1)} - /\ UNCHANGED <> + /\ UNCHANGED <> \******************************************************************************* \* Final spec @@ -351,20 +374,23 @@ Next == \/ \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]_<> +Spec == Init /\ [][Next]_<> \******************************************************************************** \* Invariants \******************************************************************************** -\* we don't track history, but this property is fairly convincing anyway +\* 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 + LogIsMonotonic == \A a \in acceptors: \A i \in DOMAIN acc_state[a].wal: \A j \in DOMAIN acc_state[a].wal: