diff --git a/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftDefs.tla b/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftDefs.tla index bebd6af9..d571d100 100644 --- a/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftDefs.tla +++ b/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftDefs.tla @@ -4,8 +4,6 @@ EXTENDS etcd_raftModel MaxOrZero(s) == IF s = {} THEN 0 ELSE Max(s) -CurrentLeaders == {i \in Server : state[i] = Leader} - Committed(i) == SubSeq(log[i],1,commitIndex[i]) LogInv == @@ -46,17 +44,9 @@ MoreUpToDateCorrectInv == /\ Len(log[i]) >= Len(log[j])) => IsPrefix(Committed(j), log[i]) -LeaderCompletenessInv == - \A i \in Server : - LET committed == Committed(i) IN - \A idx \in 1..Len(committed) : - LET entry == log[i][idx] IN - - \A l \in CurrentLeaders : - - currentTerm[l] > entry.term => - - log[l][idx] = entry +LeaderCompletenessInv == + \A c \in commitHistory, e \in electionHistory : + c.term < e.term => IsPrefix(c.entries, e.entries) CommittedIsDurableInv == \A i \in Server : diff --git a/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftModel.tla b/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftModel.tla index 629b457e..7fcb570f 100644 --- a/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftModel.tla +++ b/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftModel.tla @@ -84,7 +84,7 @@ configVars == <> VARIABLE durableState -vars == <> +protocolVars == <> Quorum(c) == {i \in SUBSET(c) : Cardinality(i) * 2 > Cardinality(c)} @@ -164,7 +164,7 @@ InitDurableState == config |-> config[i] ]] -Init == /\ InitMessageVars +ProtocolInit == /\ InitMessageVars /\ InitServerVars /\ InitCandidateVars /\ InitLeaderVars @@ -508,10 +508,27 @@ NextUnreliable == /\ messages[m] = 1 /\ DropMessage(m) -Next == \/ NextAsync +ProtocolNext == \/ NextAsync \/ NextCrash \/ NextUnreliable +VARIABLE commitHistory, electionHistory +historyVars == <> +vars == <> + +Init == ProtocolInit /\ commitHistory = {} /\ electionHistory = {} + +RecordEvents == + /\ commitHistory' = commitHistory \cup + {[server |-> s, term |-> currentTerm'[s], + entries |-> SubSeq(log'[s], 1, commitIndex'[s])] : + s \in {i \in Server : commitIndex'[i] > commitIndex[i]}} + /\ electionHistory' = electionHistory \cup + {[server |-> s, term |-> currentTerm'[s], entries |-> log'[s]] : + s \in {i \in Server : state[i] # Leader /\ state'[i] = Leader}} + +Next == ProtocolNext /\ RecordEvents + Spec == Init /\ [][Next]_vars ASSUME InitServerSubset == InitServer \subseteq Server diff --git a/benchmark/proof-from-scratch-module/manifest.json b/benchmark/proof-from-scratch-module/manifest.json index f7787815..0cf06ca9 100644 --- a/benchmark/proof-from-scratch-module/manifest.json +++ b/benchmark/proof-from-scratch-module/manifest.json @@ -997,7 +997,7 @@ "spec": { "format_version": 1, "task_id": "etcd_raft/etcd_raft.tla", - "source_sha256": "5a8441bde8cd7051dad1c59be8b9ec7870a26ce99d28002ff3ccf83387fd35db", + "source_sha256": "e6aa5a22b17d9556f7cb97a659cdae152d2b9b038d56739068697d8cd3aa3d3f", "proof_units": [ { "task_id": "etcd_raft/etcd_raft_LogInv.tla", diff --git a/benchmark/proof-from-scratch/etcd_raft/etcd_raftModel.tla b/benchmark/proof-from-scratch/etcd_raft/etcd_raftModel.tla index 629b457e..7fcb570f 100644 --- a/benchmark/proof-from-scratch/etcd_raft/etcd_raftModel.tla +++ b/benchmark/proof-from-scratch/etcd_raft/etcd_raftModel.tla @@ -84,7 +84,7 @@ configVars == <> VARIABLE durableState -vars == <> +protocolVars == <> Quorum(c) == {i \in SUBSET(c) : Cardinality(i) * 2 > Cardinality(c)} @@ -164,7 +164,7 @@ InitDurableState == config |-> config[i] ]] -Init == /\ InitMessageVars +ProtocolInit == /\ InitMessageVars /\ InitServerVars /\ InitCandidateVars /\ InitLeaderVars @@ -508,10 +508,27 @@ NextUnreliable == /\ messages[m] = 1 /\ DropMessage(m) -Next == \/ NextAsync +ProtocolNext == \/ NextAsync \/ NextCrash \/ NextUnreliable +VARIABLE commitHistory, electionHistory +historyVars == <> +vars == <> + +Init == ProtocolInit /\ commitHistory = {} /\ electionHistory = {} + +RecordEvents == + /\ commitHistory' = commitHistory \cup + {[server |-> s, term |-> currentTerm'[s], + entries |-> SubSeq(log'[s], 1, commitIndex'[s])] : + s \in {i \in Server : commitIndex'[i] > commitIndex[i]}} + /\ electionHistory' = electionHistory \cup + {[server |-> s, term |-> currentTerm'[s], entries |-> log'[s]] : + s \in {i \in Server : state[i] # Leader /\ state'[i] = Leader}} + +Next == ProtocolNext /\ RecordEvents + Spec == Init /\ [][Next]_vars ASSUME InitServerSubset == InitServer \subseteq Server diff --git a/benchmark/proof-from-scratch/etcd_raft/etcd_raft_LeaderCompletenessDefs.tla b/benchmark/proof-from-scratch/etcd_raft/etcd_raft_LeaderCompletenessDefs.tla index 9660d6e1..f1081fcb 100644 --- a/benchmark/proof-from-scratch/etcd_raft/etcd_raft_LeaderCompletenessDefs.tla +++ b/benchmark/proof-from-scratch/etcd_raft/etcd_raft_LeaderCompletenessDefs.tla @@ -2,21 +2,9 @@ EXTENDS etcd_raftModel -CurrentLeaders == {i \in Server : state[i] = Leader} - -Committed(i) == SubSeq(log[i],1,commitIndex[i]) - -LeaderCompletenessInv == - \A i \in Server : - LET committed == Committed(i) IN - \A idx \in 1..Len(committed) : - LET entry == log[i][idx] IN - - \A l \in CurrentLeaders : - - currentTerm[l] > entry.term => - - log[l][idx] = entry +LeaderCompletenessInv == + \A c \in commitHistory, e \in electionHistory : + c.term < e.term => IsPrefix(c.entries, e.entries) =============================================================================== diff --git a/source/etcd_raft/README.md b/source/etcd_raft/README.md index a61647fb..3d3b3ccb 100644 --- a/source/etcd_raft/README.md +++ b/source/etcd_raft/README.md @@ -1,6 +1,6 @@ # etcd Raft benchmark model -The model is derived from the etcd Raft example distributed with Specula. Its eight selected safety theorem statements are preserved. +The model is derived from the etcd Raft example distributed with Specula. Its eight selected safety theorem statements and task IDs are preserved; the definition of `LeaderCompletenessInv` is corrected below. The local constant-domain and pending-message repairs remain in place. The crash-recovery repair stores `logEntries` alongside the existing numeric `durableState[i].log` field in `InitDurableState` and `PersistState`. `Restart` restores the saved entries directly. @@ -9,3 +9,30 @@ Previously, recovery took a prefix of the current volatile log using the last pe Implementation reference: `etcd-io/raft` at `3cbf6a74be3fa392edd8b64253fcd11c3ce5649b`. `raftLog.storage` and `raftLog.unstable` hold stable and volatile entries separately; `newLogWithSize` reconstructs the log from storage, while `append` updates the unstable portion. See [log.go](https://github.com/etcd-io/raft/blob/3cbf6a74be3fa392edd8b64253fcd11c3ce5649b/log.go) and the [persistence contract](https://github.com/etcd-io/raft/blob/3cbf6a74be3fa392edd8b64253fcd11c3ce5649b/README.md). `tests/fixtures/etcd_raft/DurableLogRecovery.tla` follows real model actions through an election, persistence, a conflicting newer-term append, and a restart. Three cases check recovery after truncation, after an unpersisted same-length replacement, and after persisting the replacement. Each trace also checks all eight benchmark safety predicates and its transition relation against the original `Next` relation. These regression traces validate the repair; they are not proofs of all eight unbounded theorems. + +## Leader completeness + +An entry created in term 1 can remain uncommitted until term 3. A disconnected +term-2 leader need not contain that entry. The previous predicate compared each +current leader's term with the entry's creation term and incorrectly rejected +this legal execution. Raft's [Leader Completeness property](https://raft.github.io/raft.pdf) +(Figure 3 and sections 5.4.2-5.4.3) instead concerns entries committed in an +earlier term. + +`commitHistory` records the current term and full log prefix whenever a server's +commit index advances, including when a follower learns a committed prefix. +`electionHistory` records each leader's term and log at election time. The +corrected predicate requires every later-term election to contain each earlier +committed prefix. Both histories survive restart. They are passive observers: +`ProtocolInit`, `ProtocolNext` and the protocol actions preserve the previous +state-machine behavior and assumptions; `Init` and `Next` add history updates. +`NextAsyncCrash` and `NextDynamic` also update the observers. + +`tests/fixtures/etcd_raft/LeaderCompleteness.tla` replays the late commit, elects +a term-4 leader, and restarts servers. The creation-term predicate fails on the +same execution; the corrected predicate holds, with its later-election condition +actually exercised. A fault control removes vote log-freshness checking and is +rejected when an incomplete log wins the later election. These finite +regressions do not constitute an unbounded proof. Frozen experiments using the +old context retain their original results and must be distinguished from runs +against the corrected model. diff --git a/source/etcd_raft/etcd_raft.tla b/source/etcd_raft/etcd_raft.tla index dfeca11a..878f619b 100644 --- a/source/etcd_raft/etcd_raft.tla +++ b/source/etcd_raft/etcd_raft.tla @@ -143,8 +143,8 @@ VARIABLE \* End of per server variables. ---- -\* All variables; used for stuttering (asserting state hasn't changed). -vars == <> +\* Protocol variables, before adding passive history observers below. +protocolVars == <> ---- @@ -263,7 +263,7 @@ InitDurableState == config |-> config[i] ]] -Init == /\ InitMessageVars +ProtocolInit == /\ InitMessageVars /\ InitServerVars /\ InitCandidateVars /\ InitLeaderVars @@ -722,7 +722,7 @@ NextAsync == NextCrash == \E i \in Server : Restart(i) -NextAsyncCrash == +ProtocolNextAsyncCrash == \/ NextAsync \/ NextCrash @@ -737,20 +737,40 @@ NextUnreliable == /\ DropMessage(m) \* Most pessimistic network model -Next == \/ NextAsync +ProtocolNext == \/ NextAsync \/ NextCrash \/ NextUnreliable \* Membership changes -NextDynamic == - \/ Next +ProtocolNextDynamic == + \/ ProtocolNext \/ \E i, j \in Server : AddNewServer(i, j) \/ \E i, j \in Server : AddLearner(i, j) \/ \E i, j \in Server : DeleteServer(i, j) \/ \E i \in Server : ApplySimpleConfChange(i) -\* The specification must start with the initial state and transition according -\* to Next. +\* Observers retain commit and election events across crashes. Protocol actions +\* never read these variables or use them as guards. +VARIABLE commitHistory, electionHistory +historyVars == <> +vars == <> + +Init == ProtocolInit /\ commitHistory = {} /\ electionHistory = {} + +RecordEvents == + /\ commitHistory' = commitHistory \cup + {[server |-> s, term |-> currentTerm'[s], + entries |-> SubSeq(log'[s], 1, commitIndex'[s])] : + s \in {i \in Server : commitIndex'[i] > commitIndex[i]}} + /\ electionHistory' = electionHistory \cup + {[server |-> s, term |-> currentTerm'[s], entries |-> log'[s]] : + s \in {i \in Server : state[i] # Leader /\ state'[i] = Leader}} + +Next == ProtocolNext /\ RecordEvents +NextAsyncCrash == ProtocolNextAsyncCrash /\ RecordEvents +NextDynamic == ProtocolNextDynamic /\ RecordEvents + +\* The specification includes the observers without restricting protocol steps. Spec == Init /\ [][Next]_vars (***************************************************************************) @@ -862,21 +882,13 @@ MoreUpToDateCorrectInv == /\ Len(log[i]) >= Len(log[j])) => IsPrefix(Committed(j), log[i]) -\* If a log entry is committed in a given term, then that -\* entry will be present in the logs of the leaders -\* for all higher-numbered terms -\* See: https://github.com/uwplse/verdi-raft/blob/master/raft/LeaderCompletenessInterface.v -LeaderCompletenessInv == - \A i \in Server : - LET committed == Committed(i) IN - \A idx \in 1..Len(committed) : - LET entry == log[i][idx] IN - \* if the entry is committed - \A l \in CurrentLeaders : - \* all leaders with higher-number terms - currentTerm[l] > entry.term => - \* have the entry at the same log position - log[l][idx] = entry +\* A commit observation uses the server's term when its commit index advances, +\* including when a follower learns a committed prefix. Entry creation terms +\* can precede commitment; only later-term elections must contain that prefix. +\* See Raft Figure 3 and sections 5.4.2-5.4.3: https://raft.github.io/raft.pdf +LeaderCompletenessInv == + \A c \in commitHistory, e \in electionHistory : + c.term < e.term => IsPrefix(c.entries, e.entries) \* Any entry committed by leader shall be persisted already CommittedIsDurableInv == diff --git a/tests/dataset/test_etcd_raft.py b/tests/dataset/test_etcd_raft.py index fc5d4dfc..2c7d714f 100644 --- a/tests/dataset/test_etcd_raft.py +++ b/tests/dataset/test_etcd_raft.py @@ -1,4 +1,4 @@ -"""Regression coverage for the etcd Raft constant domain.""" +"""Regression coverage for etcd Raft assumptions, recovery and commit terms.""" from __future__ import annotations @@ -161,3 +161,96 @@ def test_restart_recovers_the_last_persisted_log(tmp_path, recovery_case): assert "Model checking completed. No error has been found." in output depth = re.search(r"depth of the complete state graph search is (\d+)", output) assert depth is not None and int(depth.group(1)) == 34, output + + +def _stage_leader_completeness(tmp_path, layout): + if shutil.which("java") is None or not TLA2TOOLS.is_file() or not COMMUNITY.is_dir(): + pytest.skip("TLC dependencies are not installed; run make setup") + fixture = REPO / "tests/fixtures/etcd_raft/LeaderCompleteness.tla" + text = fixture.read_text() + if layout == "source": + shutil.copyfile(SOURCE, tmp_path / SOURCE.name) + text = text.replace("EXTENDS etcd_raftDefs", "EXTENDS etcd_raft") + model = tmp_path / SOURCE.name + else: + context = REPO / "benchmark/proof-from-scratch-module/etcd_raft" if layout == "module" else TASK_DIR + defs = "etcd_raftDefs.tla" if layout == "module" else "etcd_raft_LeaderCompletenessDefs.tla" + shutil.copyfile(context / "etcd_raftModel.tla", tmp_path / "etcd_raftModel.tla") + shutil.copyfile(context / defs, tmp_path / defs) + text = text.replace("EXTENDS etcd_raftDefs", f"EXTENDS {Path(defs).stem}") + model = tmp_path / "etcd_raftModel.tla" + (tmp_path / fixture.name).write_text(text) + return model + + +def _check_leader_completeness( + tmp_path, *, crash=False, follower=False, election_node=3, invariant="LeaderCompletenessInv", all_goals=True +): + config = CONFIG.format(invariant=invariant, init_server="{1, 2, 3}", server="{1, 2, 3}", nil="0") + config = config.replace("SPECIFICATION Spec", "SPECIFICATION TraceSpec") + config += ( + f"\nCONSTANTS CrashBeforeElection = {str(crash).upper()}\n" + f"CommitOnFollower = {str(follower).upper()}\nElectionNode = {election_node}\n" + "PROPERTY Spec\nPROPERTY RefinesProtocol\nPROPERTY EventuallyCompletes\n" + "INVARIANTS LateCommitWitness HistoryRetained Completed\n" + ) + if invariant == "LeaderCompletenessInv" and election_node == 3 and all_goals: + config += ( + "INVARIANTS LogInv CommittedIsDurableInv ElectionSafetyInv LogMatchingInv\n" + "MoreThanOneLeaderInv MoreUpToDateCorrectInv QuorumLogInv\n" + ) + (tmp_path / "LeaderCompleteness.cfg").write_text(config) + classpath = os.pathsep.join((str(TLA2TOOLS), str(COMMUNITY))) + result = subprocess.run( + [ + "java", + "-XX:+UseParallelGC", + "-Xmx1g", + "-cp", + classpath, + "tlc2.TLC", + "-workers", + "1", + "-config", + "LeaderCompleteness.cfg", + "LeaderCompleteness.tla", + ], + cwd=tmp_path, + capture_output=True, + text=True, + timeout=60, + ) + output = result.stdout + result.stderr + (tmp_path / "tlc.log").write_text(output) + return result.returncode, output + + +@pytest.mark.parametrize("layout", ["source", "flat", "module"]) +@pytest.mark.parametrize("crash,follower", [(False, False), (True, False), (False, True)]) +def test_leader_completeness_uses_commit_terms_and_retains_history(tmp_path, layout, crash, follower): + _stage_leader_completeness(tmp_path, layout) + code, output = _check_leader_completeness(tmp_path, crash=crash, follower=follower, all_goals=layout != "flat") + assert code == 0, output + assert "Model checking completed. No error has been found." in output + assert "67 distinct states found, 0 states left on queue" in output + + +@pytest.mark.parametrize("layout", ["source", "flat", "module"]) +def test_creation_term_predicate_rejects_a_legal_late_commit(tmp_path, layout): + _stage_leader_completeness(tmp_path, layout) + code, output = _check_leader_completeness(tmp_path, invariant="CreationTermCompleteness") + assert code == 12, output + assert "Invariant CreationTermCompleteness is violated" in output + assert "48 distinct states found, 0 states left on queue" in output + + +@pytest.mark.parametrize("layout", ["source", "flat", "module"]) +def test_leader_completeness_rejects_election_without_log_freshness(tmp_path, layout): + model = _stage_leader_completeness(tmp_path, layout) + text = model.read_text() + guard = " /\\ logOk\n" + assert text.count(guard) == 1 + model.write_text(text.replace(guard, " /\\ TRUE\n")) + code, output = _check_leader_completeness(tmp_path, election_node=2) + assert code == 12, output + assert "Invariant LeaderCompletenessInv is violated" in output diff --git a/tests/fixtures/etcd_raft/DurableLogRecovery.tla b/tests/fixtures/etcd_raft/DurableLogRecovery.tla index ee404cf8..f4d1c039 100644 --- a/tests/fixtures/etcd_raft/DurableLogRecovery.tla +++ b/tests/fixtures/etcd_raft/DurableLogRecovery.tla @@ -12,7 +12,7 @@ RecvT(ty, d) == \E m \in DOMAIN messages : m.mtype = ty /\ m.mdest = d /\ Receiv SInit == Init /\ pc = 0 -SNext == +SProtocolNext == \/ Step(0, Timeout(s1)) \/ Step(1, Ready(s1)) \/ Step(2, RequestVote(s1,s1)) @@ -49,6 +49,8 @@ SNext == \/ Step(32, Restart(s1)) \/ (pc = 33 /\ UNCHANGED <>) +SNext == SProtocolNext /\ RecordEvents + SSpec == SInit /\ [][SNext]_<> DurLogLeqLen == \A i \in Server : durableState[i].log <= Len(log[i]) diff --git a/tests/fixtures/etcd_raft/LeaderCompleteness.tla b/tests/fixtures/etcd_raft/LeaderCompleteness.tla new file mode 100644 index 00000000..8b895ff3 --- /dev/null +++ b/tests/fixtures/etcd_raft/LeaderCompleteness.tla @@ -0,0 +1,116 @@ +---- MODULE LeaderCompleteness ---- +EXTENDS etcd_raftDefs +CONSTANTS CommitOnFollower, CrashBeforeElection, ElectionNode +VARIABLE pc + +Voter == IF ElectionNode = 2 THEN 3 ELSE 1 +TraceMessage(ty, src, dst, t) == + CHOOSE m \in DOMAIN messages : + m.mtype = ty /\ m.msource = src /\ m.mdest = dst /\ m.mterm = t + +TraceInit == Init /\ pc = 0 + +\* Terms 1 and 2 elect leaders with conflicting, uncommitted entries. +\* Term 3 commits the term-1 entry; term 4 must retain that committed prefix. +TraceAction == + CASE pc = 0 -> Timeout(1) + [] pc = 1 -> RequestVote(1,1) + [] pc = 2 -> RequestVote(1,3) + [] pc = 3 -> Ready(1) + [] pc = 4 -> Receive(TraceMessage(RequestVoteRequest,1,3,1)) + [] pc = 5 -> Receive(TraceMessage(RequestVoteRequest,1,3,1)) + [] pc = 6 -> Ready(3) + [] pc = 7 -> Receive(TraceMessage(RequestVoteResponse,1,1,1)) + [] pc = 8 -> Receive(TraceMessage(RequestVoteResponse,3,1,1)) + [] pc = 9 -> BecomeLeader(1) + [] pc = 10 -> ClientRequest(1,0) + [] pc = 11 -> Ready(1) + [] pc = 12 -> Timeout(2) + [] pc = 13 -> Timeout(2) + [] pc = 14 -> RequestVote(2,2) + [] pc = 15 -> RequestVote(2,3) + [] pc = 16 -> Ready(2) + [] pc = 17 -> Receive(TraceMessage(RequestVoteRequest,2,3,2)) + [] pc = 18 -> Receive(TraceMessage(RequestVoteRequest,2,3,2)) + [] pc = 19 -> Ready(3) + [] pc = 20 -> Receive(TraceMessage(RequestVoteResponse,2,2,2)) + [] pc = 21 -> Receive(TraceMessage(RequestVoteResponse,3,2,2)) + [] pc = 22 -> BecomeLeader(2) + [] pc = 23 -> ClientRequest(2,0) + [] pc = 24 -> Ready(2) + [] pc = 25 -> StepDownToFollower(1) + [] pc = 26 -> Timeout(1) + [] pc = 27 -> Timeout(1) + [] pc = 28 -> RequestVote(1,1) + [] pc = 29 -> RequestVote(1,3) + [] pc = 30 -> Ready(1) + [] pc = 31 -> Receive(TraceMessage(RequestVoteRequest,1,3,3)) + [] pc = 32 -> Receive(TraceMessage(RequestVoteRequest,1,3,3)) + [] pc = 33 -> Ready(3) + [] pc = 34 -> Receive(TraceMessage(RequestVoteResponse,1,1,3)) + [] pc = 35 -> Receive(TraceMessage(RequestVoteResponse,3,1,3)) + [] pc = 36 -> BecomeLeader(1) + [] pc = 37 -> ClientRequest(1,0) + [] pc = 38 -> AppendEntriesToSelf(1) + [] pc = 39 -> AppendEntries(1,3,<<1,3>>) + [] pc = 40 -> Ready(1) + [] pc = 41 -> Receive(TraceMessage(AppendEntriesResponse,1,1,3)) + [] pc = 42 -> Receive(TraceMessage(AppendEntriesRequest,1,3,3)) + [] pc = 43 -> (Receive(TraceMessage(AppendEntriesRequest,1,3,3)) /\ AppendEntriesAlreadyDone(3,1,1,TraceMessage(AppendEntriesRequest,1,3,3))) + [] pc = 44 -> Ready(3) + [] pc = 45 -> Receive(TraceMessage(AppendEntriesResponse,3,1,3)) + [] pc = 46 -> AdvanceCommitIndex(1) + [] pc = 47 -> IF CommitOnFollower THEN AppendEntries(1,3,<<3,3>>) ELSE UNCHANGED vars + [] pc = 48 -> IF CommitOnFollower THEN Ready(1) ELSE UNCHANGED vars + [] pc = 49 -> IF CommitOnFollower THEN (Receive(TraceMessage(AppendEntriesRequest,1,3,3)) /\ AppendEntriesAlreadyDone(3,1,3,TraceMessage(AppendEntriesRequest,1,3,3))) ELSE UNCHANGED vars + [] pc = 50 -> IF CommitOnFollower THEN Ready(3) ELSE UNCHANGED vars + [] pc = 51 -> IF CrashBeforeElection THEN Restart(1) ELSE Ready(1) + [] pc = 52 -> IF ElectionNode = 2 THEN StepDownToFollower(2) ELSE UNCHANGED vars + [] pc = 53 -> IF ElectionNode = 2 THEN Timeout(2) ELSE UNCHANGED vars + [] pc = 54 -> Timeout(ElectionNode) + [] pc = 55 -> RequestVote(ElectionNode,ElectionNode) + [] pc = 56 -> RequestVote(ElectionNode,Voter) + [] pc = 57 -> Ready(ElectionNode) + [] pc = 58 -> Receive(TraceMessage(RequestVoteRequest,ElectionNode,Voter,4)) + [] pc = 59 -> Receive(TraceMessage(RequestVoteRequest,ElectionNode,Voter,4)) + [] pc = 60 -> Ready(Voter) + [] pc = 61 -> Receive(TraceMessage(RequestVoteResponse,ElectionNode,ElectionNode,4)) + [] pc = 62 -> Receive(TraceMessage(RequestVoteResponse,Voter,ElectionNode,4)) + [] pc = 63 -> BecomeLeader(ElectionNode) + [] pc = 64 -> Restart(ElectionNode) + [] pc = 65 -> Restart(1) + [] OTHER -> FALSE + +TraceNext == TraceAction /\ RecordEvents /\ pc' = pc+1 +TraceSpec == TraceInit /\ [][TraceNext]_<> + /\ WF_<>(TraceNext) +EventuallyCompletes == <>(pc = 66) +RefinesProtocol == [][ProtocolNext]_protocolVars + +ExpectedPrefix == <<[term |-> 1, type |-> ValueEntry, value |-> [val |-> 0]], + [term |-> 3, type |-> ValueEntry, value |-> [val |-> 0]]>> + +\* The previous predicate is retained only as a regression oracle. +CreationTermCompleteness == + \A i \in Server : + \A idx \in 1..commitIndex[i] : + \A l \in {s \in Server : state[s] = Leader} : + currentTerm[l] > log[i][idx].term => log[l][idx] = log[i][idx] + +LateCommitWitness == pc = 47 => + /\ currentTerm = <<3, 2, 3>> + /\ state = <> + /\ commitIndex = <<2, 0, 0>> + /\ log[1] = ExpectedPrefix + /\ ~CreationTermCompleteness + +HistoryRetained == pc >= 47 => + [server |-> 1, term |-> 3, entries |-> ExpectedPrefix] \in commitHistory + +Completed == pc = 66 => + /\ [server |-> ElectionNode, term |-> 4, entries |-> ExpectedPrefix] + \in electionHistory + /\ (CommitOnFollower => + [server |-> 3, term |-> 3, entries |-> ExpectedPrefix] \in commitHistory) + /\ (CrashBeforeElection => commitIndex[1] = 0) +====