From 30f89fcff72a31c31a42fabb39e3ad43d1fb4e24 Mon Sep 17 00:00:00 2001 From: Qian-Cheng-nju Date: Wed, 14 Oct 2026 04:26:25 +0000 Subject: [PATCH 1/2] Correct etcd quorum freshness and add commit liveness --- README.md | 4 +- .../etcd_raft/etcd_raft.tla | 7 + .../etcd_raft/etcd_raftDefs.tla | 77 ++- .../etcd_raft/etcd_raftModel.tla | 7 +- .../proof-from-scratch-module/manifest.json | 8 +- .../etcd_raft/etcd_raftModel.tla | 7 +- .../etcd_raft/etcd_raft_CommitLiveness.tla | 12 + .../etcd_raft_CommitLivenessDefs.tla | 620 ++++++++++++++++++ .../etcd_raft/etcd_raft_MoreUpToDateDefs.tla | 12 +- benchmark/proof-from-scratch/manifest.json | 6 + docs/DATASET.md | 2 +- source/etcd_raft/README.md | 40 +- source/etcd_raft/etcd_raft.tla | 102 ++- tests/dataset/test_etcd_progress.py | 126 ++++ tests/fixtures/etcd_raft/CommitProgress.tla | 66 ++ tests/fixtures/etcd_raft/LogFreshness.tla | 131 ++++ 16 files changed, 1196 insertions(+), 31 deletions(-) create mode 100644 benchmark/proof-from-scratch/etcd_raft/etcd_raft_CommitLiveness.tla create mode 100644 benchmark/proof-from-scratch/etcd_raft/etcd_raft_CommitLivenessDefs.tla create mode 100644 tests/dataset/test_etcd_progress.py create mode 100644 tests/fixtures/etcd_raft/CommitProgress.tla create mode 100644 tests/fixtures/etcd_raft/LogFreshness.tla diff --git a/README.md b/README.md index 0b9405bd..359891d0 100644 --- a/README.md +++ b/README.md @@ -35,11 +35,11 @@ We currently focus on a few hard problems (due to token shortage). | [Cahill’s serializable snapshot isolation](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/CahillSSI/CahillSerializability.tla) | Protocol | 1 | 1 | | [Ivy TLB](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/ivy_examples_tlb/ivy_examples_tlb.tla) | System | 1 | 2 | | [OpenAddressing](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/OpenAddressing/OpenAddressing.tla) | System | 1 | 5 | -| [etcd Raft](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/etcd_raft/etcd_raft.tla) | System | 1 | 8 | +| [etcd Raft](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/etcd_raft/etcd_raft.tla) | System | 1 | 9 | | [HashiCorp Raft](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/HashicorpRaft/HashicorpRaft.tla) | System | 1 | 6 | | [ZooKeeper implementation](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/ZooKeeper_LowLevel/ZkV3_7_0.tla) | System | 1 | 9 | | [MongoDB distributed transactions](https://github.com/specula-org/TLAPS-Bench/blob/main/benchmark/proof-from-scratch-module/MongoDB/MultiShardTxnSnapshot.tla) | System | 1 | 1 | -| **Total** | | 9 | 56 | +| **Total** | | 9 | 57 | For more problems, check out [the full problem set](https://github.com/specula-org/TLAPS-Bench/tree/main/benchmark/proof-from-scratch-module). diff --git a/benchmark/proof-from-scratch-module/etcd_raft/etcd_raft.tla b/benchmark/proof-from-scratch-module/etcd_raft/etcd_raft.tla index 357d6032..c80bf8a5 100644 --- a/benchmark/proof-from-scratch-module/etcd_raft/etcd_raft.tla +++ b/benchmark/proof-from-scratch-module/etcd_raft/etcd_raft.tla @@ -43,4 +43,11 @@ THEOREM QuorumLog == Spec => []QuorumLogInv \* BEGIN AGENT PROOF etcd_raft/etcd_raft_QuorumLog.tla PROOF OMITTED \* END AGENT PROOF etcd_raft/etcd_raft_QuorumLog.tla + +THEOREM CommitLiveness == + \A l \in InitServer : \A Q \in Quorum(InitServer) : \A n \in Nat \ {0} : + LiveSpec(l, Q, n) => CommitProgress(l, n) +\* BEGIN AGENT PROOF etcd_raft/etcd_raft_CommitLiveness.tla +PROOF OMITTED +\* END AGENT PROOF etcd_raft/etcd_raft_CommitLiveness.tla ==== 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 d571d100..6c83c76d 100644 --- a/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftDefs.tla +++ b/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftDefs.tla @@ -38,11 +38,13 @@ QuorumLogInv == IsPrefix(Committed(i), log[j]) MoreUpToDateCorrectInv == - \A i, j \in Server : - (\/ LastTerm(log[i]) > LastTerm(log[j]) - \/ /\ LastTerm(log[i]) = LastTerm(log[j]) - /\ Len(log[i]) >= Len(log[j])) => - IsPrefix(Committed(j), log[i]) + \A i \in Server : + (\E Q \in Quorum(GetConfig(i)) : + \A j \in Q : + \/ LastTerm(log[i]) > LastTerm(log[j]) + \/ /\ LastTerm(log[i]) = LastTerm(log[j]) + /\ Len(log[i]) >= Len(log[j])) => + \A j \in Server : IsPrefix(Committed(j), log[i]) LeaderCompletenessInv == \A c \in commitHistory, e \in electionHistory : @@ -52,5 +54,70 @@ CommittedIsDurableInv == \A i \in Server : state[i] = Leader => commitIndex[i] <= durableState[i].log +StableReplicationNext(l, Q) == + /\ RecordEvents + /\ currentTerm'[l] = currentTerm[l] + /\ state'[l] = Leader + /\ \/ ReplicationNext + \/ \E i \in Server \ Q : Restart(i) + \/ \E i \in Server \ {l} : StepDownToFollower(i) + \/ \E m \in DOMAIN messages : + /\ messages[m] = 1 + /\ \/ DuplicateMessage(m) + \/ /\ ~(m.msource \in Q /\ m.mdest \in Q) + /\ DropMessage(m) + +StableReplication(l, Q) == + /\ l \in Q + /\ <>[] (state[l] = Leader /\ \A j \in Q : currentTerm[j] <= currentTerm[l]) + /\ <>[][StableReplicationNext(l, Q)]_vars + +SendThrough(l, j, n) == + /\ n \in 1..Len(log[l]) + /\ matchIndex[l][j] < n + /\ AppendEntries(l, j, <>) + /\ RecordEvents + +ReceiveThrough(l, j, n) == + /\ \E m \in DOMAIN messages : + /\ m.mtype = AppendEntriesRequest + /\ m.msource = l /\ m.mdest = j + /\ m.mterm = currentTerm[l] + /\ m.msubtype = "app" + /\ m.mprevLogIndex < n + /\ m.mprevLogIndex + Len(m.mentries) >= n + /\ Receive(m) + /\ RecordEvents + +ReceiveAckThrough(l, j, n) == + /\ \E m \in DOMAIN messages : + /\ m.mtype = AppendEntriesResponse + /\ m.msource = j /\ m.mdest = l + /\ m.mterm = currentTerm[l] + /\ m.msuccess /\ m.mmatchIndex >= n + /\ Receive(m) + /\ RecordEvents + +ReplicationFairness(l, Q, n) == + /\ \A j \in Q : WF_vars(Ready(j) /\ RecordEvents) + /\ WF_vars(matchIndex[l][l] < n /\ AppendEntriesToSelf(l) /\ RecordEvents) + /\ WF_vars(AdvanceCommitIndex(l) /\ RecordEvents) + /\ \A j \in Q : SF_vars(ReceiveAckThrough(l, j, n)) + /\ \A j \in Q \ {l} : + /\ WF_vars(SendThrough(l, j, n)) + /\ SF_vars(ReceiveThrough(l, j, n)) + +LiveSpec(l, Q, n) == + /\ Spec + /\ StableReplication(l, Q) + /\ ReplicationFairness(l, Q, n) + +CurrentTermEntry(l, n) == + /\ state[l] = Leader + /\ n \in 1..Len(log[l]) + /\ log[l][n].term = currentTerm[l] + +CommitProgress(l, n) == <>[] (CurrentTermEntry(l, n) ~> commitIndex[l] >= n) + =============================================================================== 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 7fcb570f..07845803 100644 --- a/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftModel.tla +++ b/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftModel.tla @@ -482,7 +482,7 @@ DropMessage(m) == /\ Discard(m) /\ UNCHANGED <> -NextAsync == +ReplicationNext == \/ \E i,j \in Server : RequestVote(i, j) \/ \E i \in Server : BecomeLeader(i) \/ \E i \in Server: ClientRequest(i, 0) @@ -492,8 +492,11 @@ NextAsync == \/ \E i,j \in Server : Heartbeat(i, j) \/ \E i,j \in Server : \E index \in 1..commitIndex[i] : SendSnapshot(i, j, index) \/ \E m \in DOMAIN messages : Receive(m) - \/ \E i \in Server : Timeout(i) \/ \E i \in Server : Ready(i) + +NextAsync == + \/ ReplicationNext + \/ \E i \in Server : Timeout(i) \/ \E i \in Server : StepDownToFollower(i) NextCrash == \E i \in Server : Restart(i) diff --git a/benchmark/proof-from-scratch-module/manifest.json b/benchmark/proof-from-scratch-module/manifest.json index 0cf06ca9..da761437 100644 --- a/benchmark/proof-from-scratch-module/manifest.json +++ b/benchmark/proof-from-scratch-module/manifest.json @@ -1,6 +1,6 @@ { "format_version": 1, - "corpus_sha256": "58395353d2eb2d0d6ee4e0fc6c657a7d0cc508f91e1ef7a0e07bd3675f2cca7d", + "corpus_sha256": "78e9956d3fe3aab33c76b3fa0c83ea74c7b685b9a2347fc025d2d82c93dbfa3d", "complete": true, "module_tasks": [ { @@ -997,7 +997,7 @@ "spec": { "format_version": 1, "task_id": "etcd_raft/etcd_raft.tla", - "source_sha256": "e6aa5a22b17d9556f7cb97a659cdae152d2b9b038d56739068697d8cd3aa3d3f", + "source_sha256": "8c0822bfc40a2af2a0578f2943fb9c448904b59ab27a1e3d812b282ca7004caa", "proof_units": [ { "task_id": "etcd_raft/etcd_raft_LogInv.tla", @@ -1030,6 +1030,10 @@ { "task_id": "etcd_raft/etcd_raft_QuorumLog.tla", "statement_sha256": "042668e54a03ee5119ed166a69f8bfca8fcd98fab0f634430dd53ecff973db9d" + }, + { + "task_id": "etcd_raft/etcd_raft_CommitLiveness.tla", + "statement_sha256": "180e0fe63faa15175f80a0e07b90e16f4aadf9c6074261699bceb4f21e801dce" } ] }, diff --git a/benchmark/proof-from-scratch/etcd_raft/etcd_raftModel.tla b/benchmark/proof-from-scratch/etcd_raft/etcd_raftModel.tla index 7fcb570f..07845803 100644 --- a/benchmark/proof-from-scratch/etcd_raft/etcd_raftModel.tla +++ b/benchmark/proof-from-scratch/etcd_raft/etcd_raftModel.tla @@ -482,7 +482,7 @@ DropMessage(m) == /\ Discard(m) /\ UNCHANGED <> -NextAsync == +ReplicationNext == \/ \E i,j \in Server : RequestVote(i, j) \/ \E i \in Server : BecomeLeader(i) \/ \E i \in Server: ClientRequest(i, 0) @@ -492,8 +492,11 @@ NextAsync == \/ \E i,j \in Server : Heartbeat(i, j) \/ \E i,j \in Server : \E index \in 1..commitIndex[i] : SendSnapshot(i, j, index) \/ \E m \in DOMAIN messages : Receive(m) - \/ \E i \in Server : Timeout(i) \/ \E i \in Server : Ready(i) + +NextAsync == + \/ ReplicationNext + \/ \E i \in Server : Timeout(i) \/ \E i \in Server : StepDownToFollower(i) NextCrash == \E i \in Server : Restart(i) diff --git a/benchmark/proof-from-scratch/etcd_raft/etcd_raft_CommitLiveness.tla b/benchmark/proof-from-scratch/etcd_raft/etcd_raft_CommitLiveness.tla new file mode 100644 index 00000000..f31a0a1f --- /dev/null +++ b/benchmark/proof-from-scratch/etcd_raft/etcd_raft_CommitLiveness.tla @@ -0,0 +1,12 @@ +---- MODULE etcd_raft_CommitLiveness ---- +EXTENDS etcd_raft_CommitLivenessDefs + +\* BEGIN AGENT HELPERS +\* END AGENT HELPERS +THEOREM CommitLiveness == + \A l \in InitServer : \A Q \in Quorum(InitServer) : \A n \in Nat \ {0} : + LiveSpec(l, Q, n) => CommitProgress(l, n) +\* BEGIN AGENT PROOF +PROOF OBVIOUS +\* END AGENT PROOF +==== diff --git a/benchmark/proof-from-scratch/etcd_raft/etcd_raft_CommitLivenessDefs.tla b/benchmark/proof-from-scratch/etcd_raft/etcd_raft_CommitLivenessDefs.tla new file mode 100644 index 00000000..d6990de7 --- /dev/null +++ b/benchmark/proof-from-scratch/etcd_raft/etcd_raft_CommitLivenessDefs.tla @@ -0,0 +1,620 @@ +--------------------------------- MODULE etcd_raft_CommitLivenessDefs --------------------------------- + +EXTENDS Naturals, Integers, Bags, FiniteSets, Sequences, SequencesExt, FiniteSetsExt, BagsExt, TLC + +CONSTANTS InitServer, Server + +CONSTANT ValueEntry, ConfigEntry + +CONSTANTS + + Follower, + + Candidate, + + Leader + +CONSTANTS + + Nil + +CONSTANTS + + RequestVoteRequest, + + RequestVoteResponse, + + AppendEntriesRequest, + + AppendEntriesResponse + +VARIABLE + + messages +VARIABLE + pendingMessages +messageVars == <> + +VARIABLE + + currentTerm + +VARIABLE + + state + +VARIABLE + + votedFor +serverVars == <> + +VARIABLE + + log + +VARIABLE + + commitIndex +logVars == <> + +VARIABLE + + votesResponded + +VARIABLE + + votesGranted + +candidateVars == <> + +VARIABLE + + matchIndex +VARIABLE + pendingConfChangeIndex +leaderVars == <> + +VARIABLE + config +VARIABLE + reconfigCount + +configVars == <> + +VARIABLE + durableState + +protocolVars == <> + +Quorum(c) == {i \in SUBSET(c) : Cardinality(i) * 2 > Cardinality(c)} + +LastTerm(xlog) == IF xlog = <<>> THEN 0 ELSE xlog[Len(xlog)].term + +WithMessage(m, msgs) == msgs (+) SetToBag({m}) + +WithoutMessage(m, msgs) == msgs (-) SetToBag({m}) + +SendDirect(m) == + pendingMessages' = WithMessage(m, pendingMessages) + +PendingMessages(i) == + [m \in {msg \in DOMAIN pendingMessages : msg.msource = i} |-> pendingMessages[m]] + +ClearPendingMessages(i) == + pendingMessages (-) PendingMessages(i) + +SendPendingMessages(i) == + LET msgs == PendingMessages(i) + IN /\ messages' = msgs (+) messages + /\ pendingMessages' = pendingMessages (-) msgs + +DiscardDirect(m) == + messages' = WithoutMessage(m, messages) + +ReplyDirect(response, request) == + /\ pendingMessages' = WithMessage(response, pendingMessages) + /\ messages' = WithoutMessage(request, messages) + + Send(m) == SendDirect(m) + Reply(response, request) == ReplyDirect(response, request) + Discard(m) == DiscardDirect(m) + +GetJointConfig(i) == + config[i].jointConfig + +GetConfig(i) == + GetJointConfig(i)[1] + +GetLearners(i) == + config[i].learners + +CommitTo(i, c) == + commitIndex' = [commitIndex EXCEPT ![i] = Max({@, c})] + +PersistState(i) == + durableState' = [durableState EXCEPT ![i] = [ + currentTerm |-> currentTerm[i], + votedFor |-> votedFor[i], + log |-> Len(log[i]), + logEntries |-> log[i], + commitIndex |-> commitIndex[i], + config |-> config[i] + ]] + +InitMessageVars == /\ messages = EmptyBag + /\ pendingMessages = EmptyBag +InitServerVars == /\ currentTerm = [i \in Server |-> 0] + /\ state = [i \in Server |-> Follower] + /\ votedFor = [i \in Server |-> Nil] +InitCandidateVars == /\ votesResponded = [i \in Server |-> {}] + /\ votesGranted = [i \in Server |-> {}] +InitLeaderVars == /\ matchIndex = [i \in Server |-> [j \in Server |-> 0]] + /\ pendingConfChangeIndex = [i \in Server |-> 0] +InitLogVars == /\ log = [i \in Server |-> <<>>] + /\ commitIndex = [i \in Server |-> 0] +InitConfigVars == /\ config = [i \in Server |-> [ jointConfig |-> <>, learners |-> {}]] + /\ reconfigCount = 0 +InitDurableState == + durableState = [ i \in Server |-> [ + currentTerm |-> currentTerm[i], + votedFor |-> votedFor[i], + log |-> Len(log[i]), + logEntries |-> log[i], + commitIndex |-> commitIndex[i], + config |-> config[i] + ]] + +ProtocolInit == /\ InitMessageVars + /\ InitServerVars + /\ InitCandidateVars + /\ InitLeaderVars + /\ InitLogVars + /\ InitConfigVars + /\ InitDurableState + +Restart(i) == + /\ state' = [state EXCEPT ![i] = Follower] + /\ votesResponded' = [votesResponded EXCEPT ![i] = {}] + /\ votesGranted' = [votesGranted EXCEPT ![i] = {}] + /\ matchIndex' = [matchIndex EXCEPT ![i] = [j \in Server |-> 0]] + /\ pendingConfChangeIndex' = [pendingConfChangeIndex EXCEPT ![i] = 0] + /\ pendingMessages' = ClearPendingMessages(i) + /\ currentTerm' = [currentTerm EXCEPT ![i] = durableState[i].currentTerm] + /\ commitIndex' = [commitIndex EXCEPT ![i] = durableState[i].commitIndex] + /\ votedFor' = [votedFor EXCEPT ![i] = durableState[i].votedFor] + /\ log' = [log EXCEPT ![i] = durableState[i].logEntries] + /\ config' = [config EXCEPT ![i] = durableState[i].config] + /\ UNCHANGED <> + +Timeout(i) == /\ state[i] \in {Follower, Candidate} + /\ i \in GetConfig(i) + /\ state' = [state EXCEPT ![i] = Candidate] + /\ currentTerm' = [currentTerm EXCEPT ![i] = currentTerm[i] + 1] + /\ votedFor' = [votedFor EXCEPT ![i] = i] + /\ votesResponded' = [votesResponded EXCEPT ![i] = {}] + /\ votesGranted' = [votesGranted EXCEPT ![i] = {}] + /\ UNCHANGED <> + +RequestVote(i, j) == + /\ state[i] = Candidate + /\ j \in ((GetConfig(i) \union GetLearners(i)) \ votesResponded[i]) + /\ IF i # j + THEN Send([mtype |-> RequestVoteRequest, + mterm |-> currentTerm[i], + mlastLogTerm |-> LastTerm(log[i]), + mlastLogIndex |-> Len(log[i]), + msource |-> i, + mdest |-> j]) + ELSE Send([mtype |-> RequestVoteResponse, + mterm |-> currentTerm[i], + mvoteGranted |-> TRUE, + msource |-> i, + mdest |-> i]) + /\ UNCHANGED <> + +AppendEntriesInRangeToPeer(subtype, i, j, range) == + /\ i /= j + /\ range[1] <= range[2] + /\ state[i] = Leader + /\ j \in GetConfig(i) \union GetLearners(i) + /\ LET + prevLogIndex == range[1] - 1 + + prevLogTerm == IF prevLogIndex > 0 /\ prevLogIndex <= Len(log[i]) THEN + log[i][prevLogIndex].term + ELSE + 0 + + lastEntry == Min({Len(log[i]), range[2]-1}) + entries == SubSeq(log[i], range[1], lastEntry) + commit == IF subtype = "heartbeat" THEN Min({commitIndex[i], matchIndex[i][j]}) ELSE Min({commitIndex[i], lastEntry}) + IN /\ Send( [mtype |-> AppendEntriesRequest, + msubtype |-> subtype, + mterm |-> currentTerm[i], + mprevLogIndex |-> prevLogIndex, + mprevLogTerm |-> prevLogTerm, + mentries |-> entries, + mcommitIndex |-> commit, + msource |-> i, + mdest |-> j]) + /\ UNCHANGED <> + +AppendEntriesToSelf(i) == + /\ state[i] = Leader + /\ Send([mtype |-> AppendEntriesResponse, + msubtype |-> "app", + mterm |-> currentTerm[i], + msuccess |-> TRUE, + mmatchIndex |-> Len(log[i]), + msource |-> i, + mdest |-> i]) + /\ UNCHANGED <> + +AppendEntries(i, j, range) == + AppendEntriesInRangeToPeer("app", i, j, range) + +Heartbeat(i, j) == + + AppendEntriesInRangeToPeer("heartbeat", i, j, <<1,1>>) + +SendSnapshot(i, j, index) == + AppendEntriesInRangeToPeer("snapshot", i, j, <<1,index+1>>) + +BecomeLeader(i) == + /\ state[i] = Candidate + /\ votesGranted[i] \in Quorum(GetConfig(i)) + /\ state' = [state EXCEPT ![i] = Leader] + /\ matchIndex' = [matchIndex EXCEPT ![i] = + [j \in Server |-> IF j = i THEN Len(log[i]) ELSE 0]] + /\ UNCHANGED <> + +Replicate(i, v, t) == + /\ t \in {ValueEntry, ConfigEntry} + /\ state[i] = Leader + /\ LET entry == [term |-> currentTerm[i], + type |-> t, + value |-> v] + newLog == Append(log[i], entry) + IN /\ log' = [log EXCEPT ![i] = newLog] + +ClientRequest(i, v) == + /\ Replicate(i, [val |-> v], ValueEntry) + /\ UNCHANGED <> + +AdvanceCommitIndex(i) == + /\ state[i] = Leader + /\ LET + Agree(index) == {k \in GetConfig(i) : matchIndex[i][k] >= index} + logSize == Len(log[i]) + + agreeIndexes == {index \in 1..logSize : + Agree(index) \in Quorum(GetConfig(i))} + + newCommitIndex == + IF /\ agreeIndexes /= {} + /\ log[i][Max(agreeIndexes)].term = currentTerm[i] + THEN + Max(agreeIndexes) + ELSE + commitIndex[i] + IN + /\ CommitTo(i, newCommitIndex) + /\ UNCHANGED <> + +Ready(i) == + /\ PersistState(i) + /\ SendPendingMessages(i) + /\ UNCHANGED <> + +BecomeFollowerOfTerm(i, t) == + /\ currentTerm' = [currentTerm EXCEPT ![i] = t] + /\ state' = [state EXCEPT ![i] = Follower] + /\ IF currentTerm[i] # t THEN + votedFor' = [votedFor EXCEPT ![i] = Nil] + ELSE + UNCHANGED <> + +StepDownToFollower(i) == + /\ state[i] \in {Leader, Candidate} + /\ BecomeFollowerOfTerm(i, currentTerm[i]) + /\ UNCHANGED <> + +HandleRequestVoteRequest(i, j, m) == + LET logOk == \/ m.mlastLogTerm > LastTerm(log[i]) + \/ /\ m.mlastLogTerm = LastTerm(log[i]) + /\ m.mlastLogIndex >= Len(log[i]) + grant == /\ m.mterm = currentTerm[i] + /\ logOk + /\ votedFor[i] \in {Nil, j} + IN /\ m.mterm <= currentTerm[i] + /\ \/ grant /\ votedFor' = [votedFor EXCEPT ![i] = j] + \/ ~grant /\ UNCHANGED votedFor + /\ Reply([mtype |-> RequestVoteResponse, + mterm |-> currentTerm[i], + mvoteGranted |-> grant, + msource |-> i, + mdest |-> j], + m) + /\ UNCHANGED <> + +HandleRequestVoteResponse(i, j, m) == + + /\ m.mterm = currentTerm[i] + /\ votesResponded' = [votesResponded EXCEPT ![i] = + votesResponded[i] \cup {j}] + /\ \/ /\ m.mvoteGranted + /\ votesGranted' = [votesGranted EXCEPT ![i] = + votesGranted[i] \cup {j}] + \/ /\ ~m.mvoteGranted + /\ UNCHANGED <> + /\ Discard(m) + /\ UNCHANGED <> + +RejectAppendEntriesRequest(i, j, m, logOk) == + /\ \/ m.mterm < currentTerm[i] + \/ /\ m.mterm = currentTerm[i] + /\ state[i] = Follower + /\ \lnot logOk + /\ Reply([mtype |-> AppendEntriesResponse, + msubtype |-> "app", + mterm |-> currentTerm[i], + msuccess |-> FALSE, + mmatchIndex |-> 0, + msource |-> i, + mdest |-> j], + m) + /\ UNCHANGED <> + +ReturnToFollowerState(i, m) == + /\ m.mterm = currentTerm[i] + /\ state[i] = Candidate + /\ state' = [state EXCEPT ![i] = Follower] + /\ UNCHANGED <> + +HasNoConflict(i, index, ents) == + /\ index <= Len(log[i]) + 1 + /\ \A k \in 1..Len(ents): index + k - 1 <= Len(log[i]) => log[i][index+k-1].term = ents[k].term + +AppendEntriesAlreadyDone(i, j, index, m) == + /\ \/ index <= commitIndex[i] + \/ /\ index > commitIndex[i] + /\ \/ m.mentries = << >> + \/ /\ m.mentries /= << >> + /\ m.mprevLogIndex + Len(m.mentries) <= Len(log[i]) + /\ HasNoConflict(i, index, m.mentries) + /\ IF index <= commitIndex[i] THEN + IF m.msubtype = "heartbeat" THEN CommitTo(i, m.mcommitIndex) ELSE UNCHANGED commitIndex + ELSE + CommitTo(i, Min({m.mcommitIndex, m.mprevLogIndex+Len(m.mentries)})) + /\ Reply([ mtype |-> AppendEntriesResponse, + msubtype |-> m.msubtype, + mterm |-> currentTerm[i], + msuccess |-> TRUE, + mmatchIndex |-> IF m.msubtype = "heartbeat" \/ index > commitIndex[i] THEN m.mprevLogIndex+Len(m.mentries) ELSE commitIndex[i], + msource |-> i, + mdest |-> j], + m) + /\ UNCHANGED <> + +ConflictAppendEntriesRequest(i, index, m) == + /\ m.mentries /= << >> + /\ index > commitIndex[i] + /\ ~HasNoConflict(i, index, m.mentries) + /\ log' = [log EXCEPT ![i] = SubSeq(@, 1, Len(@) - 1)] + /\ UNCHANGED <> + +NoConflictAppendEntriesRequest(i, index, m) == + /\ m.mentries /= << >> + /\ index > commitIndex[i] + /\ HasNoConflict(i, index, m.mentries) + /\ log' = [log EXCEPT ![i] = @ \o SubSeq(m.mentries, Len(@)-index+2, Len(m.mentries))] + /\ UNCHANGED <> + +AcceptAppendEntriesRequest(i, j, logOk, m) == + + /\ m.mterm = currentTerm[i] + /\ state[i] = Follower + /\ logOk + /\ LET index == m.mprevLogIndex + 1 + IN \/ AppendEntriesAlreadyDone(i, j, index, m) + \/ ConflictAppendEntriesRequest(i, index, m) + \/ NoConflictAppendEntriesRequest(i, index, m) + +HandleAppendEntriesRequest(i, j, m) == + LET logOk == \/ m.mprevLogIndex = 0 + \/ /\ m.mprevLogIndex > 0 + /\ m.mprevLogIndex <= Len(log[i]) + /\ m.mprevLogTerm = log[i][m.mprevLogIndex].term + IN + /\ m.mterm <= currentTerm[i] + /\ \/ RejectAppendEntriesRequest(i, j, m, logOk) + \/ ReturnToFollowerState(i, m) + \/ AcceptAppendEntriesRequest(i, j, logOk, m) + /\ UNCHANGED <> + +HandleAppendEntriesResponse(i, j, m) == + /\ m.mterm = currentTerm[i] + /\ \/ /\ m.msuccess + /\ matchIndex' = [matchIndex EXCEPT ![i][j] = Max({@, m.mmatchIndex})] + /\ UNCHANGED <> + \/ /\ \lnot m.msuccess + /\ UNCHANGED <> + /\ Discard(m) + /\ UNCHANGED <> + +UpdateTerm(i, j, m) == + /\ m.mterm > currentTerm[i] + /\ BecomeFollowerOfTerm(i, m.mterm) + + /\ UNCHANGED <> + +DropStaleResponse(i, j, m) == + /\ m.mterm < currentTerm[i] + /\ Discard(m) + /\ UNCHANGED <> + +ReceiveDirect(m) == + LET i == m.mdest + j == m.msource + IN + + \/ UpdateTerm(i, j, m) + \/ /\ m.mtype = RequestVoteRequest + /\ HandleRequestVoteRequest(i, j, m) + \/ /\ m.mtype = RequestVoteResponse + /\ \/ DropStaleResponse(i, j, m) + \/ HandleRequestVoteResponse(i, j, m) + \/ /\ m.mtype = AppendEntriesRequest + /\ HandleAppendEntriesRequest(i, j, m) + \/ /\ m.mtype = AppendEntriesResponse + /\ \/ DropStaleResponse(i, j, m) + \/ HandleAppendEntriesResponse(i, j, m) + +Receive(m) == ReceiveDirect(m) + +DuplicateMessage(m) == + /\ m \in DOMAIN messages + /\ messages' = WithMessage(m, messages) + /\ UNCHANGED <> + +DropMessage(m) == + + /\ Discard(m) + /\ UNCHANGED <> + +ReplicationNext == + \/ \E i,j \in Server : RequestVote(i, j) + \/ \E i \in Server : BecomeLeader(i) + \/ \E i \in Server: ClientRequest(i, 0) + \/ \E i \in Server : AdvanceCommitIndex(i) + \/ \E i,j \in Server : \E b,e \in matchIndex[i][j]+1..Len(log[i])+1 : AppendEntries(i, j, <>) + \/ \E i \in Server : AppendEntriesToSelf(i) + \/ \E i,j \in Server : Heartbeat(i, j) + \/ \E i,j \in Server : \E index \in 1..commitIndex[i] : SendSnapshot(i, j, index) + \/ \E m \in DOMAIN messages : Receive(m) + \/ \E i \in Server : Ready(i) + +NextAsync == + \/ ReplicationNext + \/ \E i \in Server : Timeout(i) + \/ \E i \in Server : StepDownToFollower(i) + +NextCrash == \E i \in Server : Restart(i) + +NextUnreliable == + + \/ \E m \in DOMAIN messages : + /\ messages[m] = 1 + /\ DuplicateMessage(m) + + \/ \E m \in DOMAIN messages : + /\ messages[m] = 1 + /\ DropMessage(m) + +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 + +ASSUME FiniteServers == IsFiniteSet(InitServer) + +ASSUME NilNotServer == Nil \notin Server + +ASSUME DistinctRoles == /\ Leader /= Candidate + /\ Candidate /= Follower + /\ Follower /= Leader + +ASSUME DistinctMessageTypes == /\ RequestVoteRequest /= AppendEntriesRequest + /\ RequestVoteRequest /= RequestVoteResponse + /\ RequestVoteRequest /= AppendEntriesResponse + /\ AppendEntriesRequest /= RequestVoteResponse + /\ AppendEntriesRequest /= AppendEntriesResponse + /\ RequestVoteResponse /= AppendEntriesResponse + +StableReplicationNext(l, Q) == + /\ RecordEvents + /\ currentTerm'[l] = currentTerm[l] + /\ state'[l] = Leader + /\ \/ ReplicationNext + \/ \E i \in Server \ Q : Restart(i) + \/ \E i \in Server \ {l} : StepDownToFollower(i) + \/ \E m \in DOMAIN messages : + /\ messages[m] = 1 + /\ \/ DuplicateMessage(m) + \/ /\ ~(m.msource \in Q /\ m.mdest \in Q) + /\ DropMessage(m) + +StableReplication(l, Q) == + /\ l \in Q + /\ <>[] (state[l] = Leader /\ \A j \in Q : currentTerm[j] <= currentTerm[l]) + /\ <>[][StableReplicationNext(l, Q)]_vars + +SendThrough(l, j, n) == + /\ n \in 1..Len(log[l]) + /\ matchIndex[l][j] < n + /\ AppendEntries(l, j, <>) + /\ RecordEvents + +ReceiveThrough(l, j, n) == + /\ \E m \in DOMAIN messages : + /\ m.mtype = AppendEntriesRequest + /\ m.msource = l /\ m.mdest = j + /\ m.mterm = currentTerm[l] + /\ m.msubtype = "app" + /\ m.mprevLogIndex < n + /\ m.mprevLogIndex + Len(m.mentries) >= n + /\ Receive(m) + /\ RecordEvents + +ReceiveAckThrough(l, j, n) == + /\ \E m \in DOMAIN messages : + /\ m.mtype = AppendEntriesResponse + /\ m.msource = j /\ m.mdest = l + /\ m.mterm = currentTerm[l] + /\ m.msuccess /\ m.mmatchIndex >= n + /\ Receive(m) + /\ RecordEvents + +ReplicationFairness(l, Q, n) == + /\ \A j \in Q : WF_vars(Ready(j) /\ RecordEvents) + /\ WF_vars(matchIndex[l][l] < n /\ AppendEntriesToSelf(l) /\ RecordEvents) + /\ WF_vars(AdvanceCommitIndex(l) /\ RecordEvents) + /\ \A j \in Q : SF_vars(ReceiveAckThrough(l, j, n)) + /\ \A j \in Q \ {l} : + /\ WF_vars(SendThrough(l, j, n)) + /\ SF_vars(ReceiveThrough(l, j, n)) + +LiveSpec(l, Q, n) == + /\ Spec + /\ StableReplication(l, Q) + /\ ReplicationFairness(l, Q, n) + +CurrentTermEntry(l, n) == + /\ state[l] = Leader + /\ n \in 1..Len(log[l]) + /\ log[l][n].term = currentTerm[l] + +CommitProgress(l, n) == <>[] (CurrentTermEntry(l, n) ~> commitIndex[l] >= n) + +=============================================================================== + diff --git a/benchmark/proof-from-scratch/etcd_raft/etcd_raft_MoreUpToDateDefs.tla b/benchmark/proof-from-scratch/etcd_raft/etcd_raft_MoreUpToDateDefs.tla index a49dd4ec..47c0ec72 100644 --- a/benchmark/proof-from-scratch/etcd_raft/etcd_raft_MoreUpToDateDefs.tla +++ b/benchmark/proof-from-scratch/etcd_raft/etcd_raft_MoreUpToDateDefs.tla @@ -5,11 +5,13 @@ EXTENDS etcd_raftModel Committed(i) == SubSeq(log[i],1,commitIndex[i]) MoreUpToDateCorrectInv == - \A i, j \in Server : - (\/ LastTerm(log[i]) > LastTerm(log[j]) - \/ /\ LastTerm(log[i]) = LastTerm(log[j]) - /\ Len(log[i]) >= Len(log[j])) => - IsPrefix(Committed(j), log[i]) + \A i \in Server : + (\E Q \in Quorum(GetConfig(i)) : + \A j \in Q : + \/ LastTerm(log[i]) > LastTerm(log[j]) + \/ /\ LastTerm(log[i]) = LastTerm(log[j]) + /\ Len(log[i]) >= Len(log[j])) => + \A j \in Server : IsPrefix(Committed(j), log[i]) =============================================================================== diff --git a/benchmark/proof-from-scratch/manifest.json b/benchmark/proof-from-scratch/manifest.json index 31cb4e71..4538a312 100644 --- a/benchmark/proof-from-scratch/manifest.json +++ b/benchmark/proof-from-scratch/manifest.json @@ -776,6 +776,12 @@ "ZooKeeper_LowLevel/ZkV3_7_0_TotalOrderDefs.tla" ] }, + "etcd_raft/etcd_raft_CommitLiveness.tla": { + "spec_id": "etcd_raft/etcd_raft.tla", + "context": [ + "etcd_raft/etcd_raft_CommitLivenessDefs.tla" + ] + }, "etcd_raft/etcd_raft_CommittedIsDurable.tla": { "spec_id": "etcd_raft/etcd_raft.tla", "context": [ diff --git a/docs/DATASET.md b/docs/DATASET.md index 9a509428..96bec17e 100644 --- a/docs/DATASET.md +++ b/docs/DATASET.md @@ -57,7 +57,7 @@ This file is generated; regenerate it with `python3 scripts/dataset_table.py`. | [ZooKeeper_LowLevel](https://github.com/Disalg-ICS-NJU/zookeeper-tla-spec/tree/main/low-level-spec/zk-3.7) | ZooKeeper (Remix) | – | 9 | 9 | | [ben-or83](https://github.com/konnov/apalache-examples/tree/af360379b7cbcd1e16c1a801ff8ac64eb9aca038/ben-or83) | apalache-examples (Konnov) | 209 | – | 209 | | [tendermint](https://github.com/konnov/apalache-examples/tree/af360379b7cbcd1e16c1a801ff8ac64eb9aca038/tendermint) | apalache-examples (Konnov) | 48 | – | 48 | -| [etcd_raft](https://github.com/specula-org/Specula/blob/main/skills/spec_generation/examples/etcdraft.tla) | etcd (Specula) | – | 8 | 8 | +| [etcd_raft](https://github.com/specula-org/Specula/blob/main/skills/spec_generation/examples/etcdraft.tla) | etcd (Specula) | – | 9 | 9 | | [ewd998](https://github.com/tlaplus/Examples/tree/master/specifications/ewd998) | tlaplus/Examples | 52 | 7 | 59 | | [byzpaxos](https://github.com/tlaplus/Examples/tree/master/specifications/byzpaxos) | tlaplus/Examples | 41 | 11 | 52 | | [lamport_mutex](https://github.com/tlaplus/Examples/tree/master/specifications/lamport_mutex) | tlaplus/Examples | 20 | 2 | 22 | diff --git a/source/etcd_raft/README.md b/source/etcd_raft/README.md index 3d3b3ccb..612329d7 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 and task IDs are preserved; the definition of `LeaderCompletenessInv` is corrected below. +The model is derived from the etcd Raft example distributed with Specula. Its eight safety theorem statements and task IDs are preserved. `MoreUpToDateCorrectInv` and `LeaderCompletenessInv` are corrected below; `CommitLiveness` adds a ninth target. 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. @@ -36,3 +36,41 @@ 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. + +## Quorum log freshness + +A single voter can have a committed old-term prefix while a disconnected server +has a conflicting, uncommitted entry with a larger last term. The original +pointwise freshness predicate incorrectly rejected this legal execution. +`MoreUpToDateCorrectInv` now requires freshness relative to an entire quorum +before concluding that a log contains every committed prefix. Raft requires +quorum votes, not one vote, to elect a leader (Raft sections 5.4.1–5.4.3). + +`LogFreshness.tla` in `tests/fixtures/etcd_raft` replays a five-server, 70-step +late-commit execution under `Spec`. The old predicate fails; the corrected +predicate holds. A control that disables vote freshness and elects an +incomplete leader is rejected by the corrected predicate. + +## Stable-period commit progress + +`CommitLiveness` concerns replication after a stable period begins; it does not +prove leader election or unconditional availability. Its parameters range over +a leader, a quorum and an arbitrary positive log index. The environment eventually +stops election timeouts, keeps that leader in the same term, and stops crashes +and RPC loss within the quorum; minority failures remain allowed. Persistence, +retries and commitment are weakly fair. Processing relevant replication requests +and successful acknowledgments is strongly fair, so an enabled RPC class cannot +be perpetually starved by other traffic. + +Under those conditions, after finite disruption, a current-term entry at that +index eventually becomes committed. These are explicit scheduling and failure +assumptions, not an assumption that commitment occurs. `Spec` and the eight +safety targets retain their original failure model; `ReplicationNext` only +factors existing actions out of `NextAsync`. + +The progress fixture explores finite interleavings from a real election with +two uncommitted entries. A separate fair witness checks that the assumptions +are satisfiable. Removing commit fairness or replacing commitment with a no-op +produces a liveness counterexample. These checks are finite regressions, not an +unbounded TLAPS proof. Old eight-target results retain their original version; +new nine-target runs start with fresh sessions and separate result directories. diff --git a/source/etcd_raft/etcd_raft.tla b/source/etcd_raft/etcd_raft.tla index 878f619b..b95b54bd 100644 --- a/source/etcd_raft/etcd_raft.tla +++ b/source/etcd_raft/etcd_raft.tla @@ -706,7 +706,7 @@ DropMessage(m) == ---- \* Defines how the variables may transition. -NextAsync == +ReplicationNext == \/ \E i,j \in Server : RequestVote(i, j) \/ \E i \in Server : BecomeLeader(i) \/ \E i \in Server: ClientRequest(i, 0) @@ -716,8 +716,11 @@ NextAsync == \/ \E i,j \in Server : Heartbeat(i, j) \/ \E i,j \in Server : \E index \in 1..commitIndex[i] : SendSnapshot(i, j, index) \/ \E m \in DOMAIN messages : Receive(m) - \/ \E i \in Server : Timeout(i) \/ \E i \in Server : Ready(i) + +NextAsync == + \/ ReplicationNext + \/ \E i \in Server : Timeout(i) \/ \E i \in Server : StepDownToFollower(i) NextCrash == \E i \in Server : Restart(i) @@ -871,16 +874,17 @@ QuorumLogInv == \E j \in S : IsPrefix(Committed(i), log[j]) -\* The "up-to-date" check performed by servers -\* before issuing a vote implies that i receives -\* a vote from j only if i has all of j's committed -\* entries +\* Freshness relative to a quorum protects committed prefixes. Freshness +\* relative to one voter alone does not: an older uncommitted branch can have +\* a higher last-entry term than that voter's indirectly committed prefix. MoreUpToDateCorrectInv == - \A i, j \in Server : - (\/ LastTerm(log[i]) > LastTerm(log[j]) - \/ /\ LastTerm(log[i]) = LastTerm(log[j]) - /\ Len(log[i]) >= Len(log[j])) => - IsPrefix(Committed(j), log[i]) + \A i \in Server : + (\E Q \in Quorum(GetConfig(i)) : + \A j \in Q : + \/ LastTerm(log[i]) > LastTerm(log[j]) + \/ /\ LastTerm(log[i]) = LastTerm(log[j]) + /\ Len(log[i]) >= Len(log[j])) => + \A j \in Server : IsPrefix(Committed(j), log[i]) \* A commit observation uses the server's term when its commit index advances, \* including when a follower learns a committed prefix. Entry creation terms @@ -925,6 +929,82 @@ PROOF OBVIOUS THEOREM QuorumLog == Spec => []QuorumLogInv PROOF OBVIOUS +\* A stable replication period may still have failures outside Q. Within Q, +\* nodes do not restart and RPCs are not lost. Election timeouts stop during +\* this period; leader election itself is not the liveness claim below. +StableReplicationNext(l, Q) == + /\ RecordEvents + /\ currentTerm'[l] = currentTerm[l] + /\ state'[l] = Leader + /\ \/ ReplicationNext + \/ \E i \in Server \ Q : Restart(i) + \/ \E i \in Server \ {l} : StepDownToFollower(i) + \/ \E m \in DOMAIN messages : + /\ messages[m] = 1 + /\ \/ DuplicateMessage(m) + \/ /\ ~(m.msource \in Q /\ m.mdest \in Q) + /\ DropMessage(m) + +StableReplication(l, Q) == + /\ l \in Q + /\ <>[] (state[l] = Leader /\ \A j \in Q : currentTerm[j] <= currentTerm[l]) + /\ <>[][StableReplicationNext(l, Q)]_vars + +\* Fairly retry a suffix covering index n until this peer acknowledges it. +SendThrough(l, j, n) == + /\ n \in 1..Len(log[l]) + /\ matchIndex[l][j] < n + /\ AppendEntries(l, j, <>) + /\ RecordEvents + +ReceiveThrough(l, j, n) == + /\ \E m \in DOMAIN messages : + /\ m.mtype = AppendEntriesRequest + /\ m.msource = l /\ m.mdest = j + /\ m.mterm = currentTerm[l] + /\ m.msubtype = "app" + /\ m.mprevLogIndex < n + /\ m.mprevLogIndex + Len(m.mentries) >= n + /\ Receive(m) + /\ RecordEvents + +ReceiveAckThrough(l, j, n) == + /\ \E m \in DOMAIN messages : + /\ m.mtype = AppendEntriesResponse + /\ m.msource = j /\ m.mdest = l + /\ m.mterm = currentTerm[l] + /\ m.msuccess /\ m.mmatchIndex >= n + /\ Receive(m) + /\ RecordEvents + +ReplicationFairness(l, Q, n) == + /\ \A j \in Q : WF_vars(Ready(j) /\ RecordEvents) + /\ WF_vars(matchIndex[l][l] < n /\ AppendEntriesToSelf(l) /\ RecordEvents) + /\ WF_vars(AdvanceCommitIndex(l) /\ RecordEvents) + /\ \A j \in Q : SF_vars(ReceiveAckThrough(l, j, n)) + /\ \A j \in Q \ {l} : + /\ WF_vars(SendThrough(l, j, n)) + /\ SF_vars(ReceiveThrough(l, j, n)) + +LiveSpec(l, Q, n) == + /\ Spec + /\ StableReplication(l, Q) + /\ ReplicationFairness(l, Q, n) + +CurrentTermEntry(l, n) == + /\ state[l] = Leader + /\ n \in 1..Len(log[l]) + /\ log[l][n].term = currentTerm[l] + +\* Finite disruption before stabilization may discard uncommitted entries. +\* After stabilization, each current-term entry must eventually be committed. +CommitProgress(l, n) == <>[] (CurrentTermEntry(l, n) ~> commitIndex[l] >= n) + +THEOREM CommitLiveness == + \A l \in InitServer : \A Q \in Quorum(InitServer) : \A n \in Nat \ {0} : + LiveSpec(l, Q, n) => CommitProgress(l, n) +PROOF OBVIOUS + =============================================================================== diff --git a/tests/dataset/test_etcd_progress.py b/tests/dataset/test_etcd_progress.py new file mode 100644 index 00000000..5a3d3838 --- /dev/null +++ b/tests/dataset/test_etcd_progress.py @@ -0,0 +1,126 @@ +"""Reachable freshness witnesses and non-vacuous commit-progress checks.""" + +from __future__ import annotations + +import os +import shutil +import subprocess +from pathlib import Path + +import pytest + +REPO = Path(__file__).resolve().parents[2] +LIB = REPO / "lib" +CONSTANTS = """ +CONSTANTS + Server = {1,2,3} + InitServer = {1,2,3} + ValueEntry = ValueEntry + ConfigEntry = ConfigEntry + Follower = Follower + Candidate = Candidate + Leader = Leader + Nil = Nil + RequestVoteRequest = RequestVoteRequest + RequestVoteResponse = RequestVoteResponse + AppendEntriesRequest = AppendEntriesRequest + AppendEntriesResponse = AppendEntriesResponse +CHECK_DEADLOCK FALSE +""" + + +def stage(tmp_path, fixture, layout="module"): + if not shutil.which("java") or not (LIB / "tla2tools.jar").is_file(): + pytest.skip("TLC dependencies are not installed") + text = (REPO / "tests/fixtures/etcd_raft" / f"{fixture}.tla").read_text() + if layout == "source": + model = tmp_path / "etcd_raft.tla" + shutil.copyfile(REPO / "source/etcd_raft/etcd_raft.tla", model) + text = text.replace("EXTENDS etcd_raftDefs", "EXTENDS etcd_raft") + else: + context = ( + REPO + / "benchmark" + / ("proof-from-scratch-module" if layout == "module" else "proof-from-scratch") + / "etcd_raft" + ) + model = tmp_path / "etcd_raftModel.tla" + shutil.copyfile(context / model.name, model) + defs = "etcd_raftDefs" if layout == "module" else "etcd_raft_MoreUpToDateDefs" + shutil.copyfile(context / f"{defs}.tla", tmp_path / f"{defs}.tla") + text = text.replace("EXTENDS etcd_raftDefs", f"EXTENDS {defs}") + (tmp_path / f"{fixture}.tla").write_text(text) + return model + + +def check(tmp_path, fixture, config): + (tmp_path / f"{fixture}.cfg").write_text(config) + cp = os.pathsep.join(str(LIB / n) for n in ["tla2tools.jar", "community", "tlapm"]) + result = subprocess.run( + [ + "java", + "-XX:+UseParallelGC", + "-Xmx1g", + "-cp", + cp, + "tlc2.TLC", + "-workers", + "1", + "-config", + f"{fixture}.cfg", + f"{fixture}.tla", + ], + cwd=tmp_path, + capture_output=True, + text=True, + timeout=90, + ) + output = result.stdout + result.stderr + (tmp_path / "check.log").write_text(output) + return result.returncode, output + + +@pytest.mark.parametrize("layout", ["source", "flat", "module"]) +@pytest.mark.parametrize("case", ["fixed", "old", "fault"]) +def test_quorum_freshness(tmp_path, layout, case): + model = stage(tmp_path, "LogFreshness", layout) + if case == "fault": + text = model.read_text() + guard = " /\\ logOk\n" + assert text.count(guard) == 1 + model.write_text(text.replace(guard, " /\\ TRUE\n")) + invariant = "PointwiseFreshness" if case == "old" else "MoreUpToDateCorrectInv" + config = CONSTANTS.replace("{1,2,3}", "{a,b,c,d,e}") + config += "\nCONSTANTS a=a b=b c=c d=d e=e\n" + config += f"FaultyElection = {str(case == 'fault').upper()}\n" + config += f"SPECIFICATION TraceSpec\nINVARIANTS {invariant} LateCommitWitness\nPROPERTY Spec\nPROPERTY EventuallyCompletes\n" + code, output = check(tmp_path, "LogFreshness", config) + assert code == (0 if case == "fixed" else 12), output + if case != "fixed": + assert f"Invariant {invariant} is violated" in output + else: + assert "71 distinct states found" in output + + +@pytest.mark.parametrize("entry", [1, 2]) +@pytest.mark.parametrize("case", ["progress", "witness", "unfair", "fault"]) +def test_commit_progress(tmp_path, entry, case): + stage(tmp_path, "CommitProgress") + defs = tmp_path / "etcd_raftDefs.tla" + model = tmp_path / "etcd_raftModel.tla" + if case == "unfair": + text = defs.read_text() + fair = " /\\ WF_vars(AdvanceCommitIndex(l) /\\ RecordEvents)\n" + assert fair in text + defs.write_text(text.replace(fair, "")) + elif case == "fault": + text = model.read_text() + commit = " /\\ CommitTo(i, newCommitIndex)" + assert commit in text + model.write_text(text.replace(commit, " /\\ UNCHANGED commitIndex")) + spec = "WitnessSpec" if case == "witness" else "TestSpec" + props = "WitnessAssumptions WitnessCompletes" if case == "witness" else "ProgressClaim NonVacuous" + config = CONSTANTS + f"\nCONSTANT EntryIndex = {entry}\nSPECIFICATION {spec}\nPROPERTY Spec\nPROPERTY {props}\n" + code, output = check(tmp_path, "CommitProgress", config) + assert code == (13 if case in {"unfair", "fault"} else 0), output + assert ("Temporal property ProgressClaim was violated" in output) == (case in {"unfair", "fault"}) diff --git a/tests/fixtures/etcd_raft/CommitProgress.tla b/tests/fixtures/etcd_raft/CommitProgress.tla new file mode 100644 index 00000000..3bdfe27c --- /dev/null +++ b/tests/fixtures/etcd_raft/CommitProgress.tla @@ -0,0 +1,66 @@ +---- MODULE CommitProgress ---- +EXTENDS etcd_raftDefs +CONSTANT EntryIndex +VARIABLE pc + +Message(ty, src, dst) == + CHOOSE m \in DOMAIN messages : + m.mtype = ty /\ m.msource = src /\ m.mdest = dst + +PrefixAction == + CASE pc = 0 -> Timeout(1) + [] pc = 1 -> RequestVote(1,1) + [] pc = 2 -> RequestVote(1,2) + [] pc = 3 -> Ready(1) + [] pc = 4 -> Receive(Message(RequestVoteRequest,1,2)) + [] pc = 5 -> Receive(Message(RequestVoteRequest,1,2)) + [] pc = 6 -> Ready(2) + [] pc = 7 -> Receive(Message(RequestVoteResponse,1,1)) + [] pc = 8 -> Receive(Message(RequestVoteResponse,2,1)) + [] pc = 9 -> BecomeLeader(1) + [] pc = 10 -> ClientRequest(1,0) + [] pc = 11 -> ClientRequest(1,0) + [] pc = 12 -> Ready(1) + [] OTHER -> FALSE + +PrefixNext == PrefixAction /\ RecordEvents /\ pc' = pc + 1 +NetworkIdle == messages = EmptyBag /\ pendingMessages = EmptyBag + +LoopNext == + /\ pc = 13 /\ UNCHANGED pc + /\ \/ \E j \in {1,2} : Ready(j) /\ RecordEvents + \/ /\ NetworkIdle /\ SendThrough(1,2,EntryIndex) + \/ /\ NetworkIdle /\ matchIndex[1][1] < EntryIndex + /\ AppendEntriesToSelf(1) /\ RecordEvents + \/ /\ \E m \in DOMAIN messages : Receive(m) + /\ RecordEvents + \/ AdvanceCommitIndex(1) /\ RecordEvents + +TestSpec == Init /\ pc = 0 /\ [][PrefixNext \/ LoopNext]_<> + /\ WF_<>(PrefixNext) + +ProgressClaim == (StableReplication(1,{1,2}) /\ ReplicationFairness(1,{1,2},EntryIndex)) => CommitProgress(1,EntryIndex) +NonVacuous == <> (pc = 13 /\ CurrentTermEntry(1,EntryIndex)) + +\* A deterministic fair witness must satisfy the actual liveness assumptions. +WitnessAction == + CASE pc < 13 -> PrefixAction + [] pc = 13 -> AppendEntriesToSelf(1) + [] pc = 14 -> Ready(1) + [] pc = 15 -> Receive(Message(AppendEntriesResponse,1,1)) + [] pc = 16 -> AppendEntries(1,2,<<1,3>>) + [] pc = 17 -> Ready(1) + [] pc = 18 -> Receive(Message(AppendEntriesRequest,1,2)) + [] pc = 19 -> /\ Receive(Message(AppendEntriesRequest,1,2)) + /\ AppendEntriesAlreadyDone(2,1,1,Message(AppendEntriesRequest,1,2)) + [] pc = 20 -> Ready(2) + [] pc = 21 -> Receive(Message(AppendEntriesResponse,2,1)) + [] pc = 22 -> AdvanceCommitIndex(1) + [] pc = 23 -> Ready(1) + [] OTHER -> FALSE +WitnessNext == WitnessAction /\ RecordEvents /\ pc' = pc+1 +WitnessSpec == Init /\ pc = 0 /\ [][WitnessNext]_<> + /\ WF_<>(WitnessNext) +WitnessAssumptions == StableReplication(1,{1,2}) /\ ReplicationFairness(1,{1,2},EntryIndex) +WitnessCompletes == <> (pc = 24 /\ commitIndex[1] = 2) +==== diff --git a/tests/fixtures/etcd_raft/LogFreshness.tla b/tests/fixtures/etcd_raft/LogFreshness.tla new file mode 100644 index 00000000..d1ed1104 --- /dev/null +++ b/tests/fixtures/etcd_raft/LogFreshness.tla @@ -0,0 +1,131 @@ +---- MODULE LogFreshness ---- +EXTENDS etcd_raftDefs + +CONSTANTS a, b, c, d, e, FaultyElection +VARIABLE pc + +TO(s) == Timeout(s) +RV(s, t) == RequestVote(s, t) +RD(s) == Ready(s) +UT(s, t) == \E m \in DOMAIN messages : m.mdest = s /\ m.mterm = t /\ UpdateTerm(s, m.msource, m) +HRVQ(s, from) == \E m \in DOMAIN messages : m.mtype = RequestVoteRequest /\ m.mdest = s /\ m.msource = from /\ HandleRequestVoteRequest(s, from, m) +HRVR(s, from) == \E m \in DOMAIN messages : m.mtype = RequestVoteResponse /\ m.mdest = s /\ m.msource = from /\ m.mterm = currentTerm[s] /\ HandleRequestVoteResponse(s, from, m) +BL(s) == BecomeLeader(s) +CR(s) == ClientRequest(s, 0) +SD(s) == StepDownToFollower(s) +AE(s, t, x, y) == AppendEntries(s, t, <>) +AES(s) == AppendEntriesToSelf(s) +HAEQL(s) == \E m \in DOMAIN messages : m.mtype = AppendEntriesRequest /\ m.mdest = s /\ HandleAppendEntriesRequest(s, m.msource, m) /\ log' # log +HAEQD(s) == \E m \in DOMAIN messages : m.mtype = AppendEntriesRequest /\ m.mdest = s /\ HandleAppendEntriesRequest(s, m.msource, m) /\ log' = log /\ messages' # messages +HAER(s, from) == \E m \in DOMAIN messages : m.mtype = AppendEntriesResponse /\ m.mdest = s /\ m.msource = from /\ m.mterm = currentTerm[s] /\ HandleAppendEntriesResponse(s, from, m) +ACI(s) == AdvanceCommitIndex(s) + +Step(k) == + CASE k = 1 -> TO(a) + [] k = 2 -> RV(a,a) + [] k = 3 -> RV(a,b) + [] k = 4 -> RV(a,c) + [] k = 5 -> RD(a) + [] k = 6 -> HRVR(a,a) + [] k = 7 -> UT(b,1) + [] k = 8 -> HRVQ(b,a) + [] k = 9 -> RD(b) + [] k = 10 -> HRVR(a,b) + [] k = 11 -> UT(c,1) + [] k = 12 -> HRVQ(c,a) + [] k = 13 -> RD(c) + [] k = 14 -> HRVR(a,c) + [] k = 15 -> BL(a) + [] k = 16 -> CR(a) + [] k = 17 -> TO(d) + [] k = 18 -> TO(d) + [] k = 19 -> RV(d,d) + [] k = 20 -> RV(d,b) + [] k = 21 -> RV(d,e) + [] k = 22 -> RD(d) + [] k = 23 -> HRVR(d,d) + [] k = 24 -> UT(b,2) + [] k = 25 -> HRVQ(b,d) + [] k = 26 -> RD(b) + [] k = 27 -> HRVR(d,b) + [] k = 28 -> UT(e,2) + [] k = 29 -> HRVQ(e,d) + [] k = 30 -> RD(e) + [] k = 31 -> HRVR(d,e) + [] k = 32 -> BL(d) + [] k = 33 -> CR(d) + [] k = 34 -> SD(a) + [] k = 35 -> TO(a) + [] k = 36 -> TO(a) + [] k = 37 -> RV(a,a) + [] k = 38 -> RV(a,b) + [] k = 39 -> RV(a,c) + [] k = 40 -> RD(a) + [] k = 41 -> HRVR(a,a) + [] k = 42 -> UT(b,3) + [] k = 43 -> HRVQ(b,a) + [] k = 44 -> RD(b) + [] k = 45 -> HRVR(a,b) + [] k = 46 -> UT(c,3) + [] k = 47 -> HRVQ(c,a) + [] k = 48 -> RD(c) + [] k = 49 -> HRVR(a,c) + [] k = 50 -> BL(a) + [] k = 51 -> CR(a) + [] k = 52 -> AE(a,b,1,3) + [] k = 53 -> AE(a,c,1,3) + [] k = 54 -> AES(a) + [] k = 55 -> RD(a) + [] k = 56 -> HAER(a,a) + [] k = 57 -> HAEQL(b) + [] k = 58 -> HAEQD(b) + [] k = 59 -> RD(b) + [] k = 60 -> HAER(a,b) + [] k = 61 -> HAEQL(c) + [] k = 62 -> HAEQD(c) + [] k = 63 -> RD(c) + [] k = 64 -> HAER(a,c) + [] k = 65 -> ACI(a) + [] k = 66 -> AE(a,e,1,2) + [] k = 67 -> RD(a) + [] k = 68 -> UT(e,3) + [] k = 69 -> HAEQL(e) + [] k = 70 -> HAEQD(e) + [] k = 71 -> FaultyElection /\ SD(d) + [] k = 72 -> TO(d) + [] k = 73 -> TO(d) + [] k = 74 -> RV(d,d) + [] k = 75 -> RV(d,b) + [] k = 76 -> RV(d,e) + [] k = 77 -> RD(d) + [] k = 78 -> HRVR(d,d) + [] k = 79 -> UT(b,4) + [] k = 80 -> HRVQ(b,d) + [] k = 81 -> RD(b) + [] k = 82 -> HRVR(d,b) + [] k = 83 -> UT(e,4) + [] k = 84 -> HRVQ(e,d) + [] k = 85 -> RD(e) + [] k = 86 -> HRVR(d,e) + [] k = 87 -> BL(d) + [] k = 88 -> CR(d) + [] OTHER -> FALSE + +MCInit == Init /\ pc = 1 +MCNext == Next /\ Step(pc) /\ pc' = pc + 1 + +TraceSpec == MCInit /\ [][MCNext]_<> /\ WF_<>(MCNext) +EventuallyCompletes == <> (pc = IF FaultyElection THEN 89 ELSE 71) +PointwiseFreshness == + \A i,j \in Server : + (\/ LastTerm(log[i]) > LastTerm(log[j]) + \/ /\ LastTerm(log[i]) = LastTerm(log[j]) + /\ Len(log[i]) >= Len(log[j])) => + IsPrefix(Committed(j), log[i]) +LateCommitWitness == pc = 71 => + /\ LastTerm(log[d]) > LastTerm(log[e]) + /\ ~IsPrefix(Committed(e), log[d]) + /\ commitIndex[e] = 1 + /\ \A j \in {a,b,c}: LastTerm(log[a]) >= LastTerm(log[j]) + /\ {a,b,c} \in Quorum(GetConfig(a)) +==== From 71d648a917f5321a5f11804808e675f050e3597c Mon Sep 17 00:00:00 2001 From: Qian-Cheng-nju Date: Wed, 14 Oct 2026 05:02:42 +0000 Subject: [PATCH 2/2] Update current suite counts for etcd liveness --- tests/evaluator/test_problem_sets.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/evaluator/test_problem_sets.py b/tests/evaluator/test_problem_sets.py index 48003d1b..7d153ddf 100644 --- a/tests/evaluator/test_problem_sets.py +++ b/tests/evaluator/test_problem_sets.py @@ -21,7 +21,7 @@ "CahillSSI/CahillSerializability.tla": 1, "ivy_examples_tlb/ivy_examples_tlb.tla": 2, "OpenAddressing/OpenAddressing.tla": 5, - "etcd_raft/etcd_raft.tla": 8, + "etcd_raft/etcd_raft.tla": 9, "HashicorpRaft/HashicorpRaft.tla": 6, "ZooKeeper_LowLevel/ZkV3_7_0.tla": 9, "MongoDB/MultiShardTxnSnapshot.tla": 1, @@ -52,7 +52,7 @@ def test_default_and_explicit_current_are_the_nine_official_modules(extra, previ assert cli.main(["run", *extra, "--dry-run", "--output-dir", str(output)]) == 0 printed = capsys.readouterr().out assert set(_selected(printed)) == set(CURRENT) - assert "9 specifications, 56 proof units" in printed + assert "9 specifications, 57 proof units" in printed assert not output.exists()