From 4791434ceab0d3c212172a479c5ade1293f8291c Mon Sep 17 00:00:00 2001 From: dimgigov Date: Thu, 7 May 2026 21:48:03 +0300 Subject: [PATCH] FV-2: Raft leader step-down on partition loss - Add heartbeatReceived variable tracking last term with heartbeat - Add Heartbeat action: leader sends keep-alive; recipient steps down on higher term - Add HeartbeatTimeout: follower starts election if no heartbeat in current term - Add LeaderLeaseExpired: leader steps down if it loses quorum connectivity - Add LeaderHasSelfHeartbeat invariant: every leader must have valid heartbeat - raft.tla now models realistic partition behavior (38M states verified) - Update CHANGELOG -> v1.2.0, VERSION -> 1.2.0, PLAN.md, README.md --- PLAN.md | 2 +- README.md | 2 +- formal-verification/CHANGELOG.md | 23 +++++++++ formal-verification/VERSION | 2 +- formal-verification/models/raft.cfg | 1 + formal-verification/raft.tla | 78 ++++++++++++++++++++++++++--- 6 files changed, 97 insertions(+), 11 deletions(-) diff --git a/PLAN.md b/PLAN.md index 662f7c8..d1f9827 100644 --- a/PLAN.md +++ b/PLAN.md @@ -55,7 +55,7 @@ | # | Задача | Защо е критично | Файл(ове) | |---|--------|----------------|-----------| | FV-1 | ~~Raft: prevLogIndex/prevLogTerm в Replicate~~ ✅ | TLA+ моделът вече проверява prevLogIndex/prevLogTerm, възстановена е `LogMatching` инвариантата, добавено е `RejectAppendEntries` и conflict truncation. | `formal-verification/raft.tla` | -| FV-2 | **Raft: Leader step-down при partition** | Няма `HeartbeatTimeout` или `LeaderLeaseExpired` — моделът не проверява дали leader се отказва при network partition. | `formal-verification/raft.tla` | +| FV-2 | ~~Raft: Leader step-down при partition~~ ✅ | Добавени `Heartbeat`, `HeartbeatTimeout`, `LeaderLeaseExpired`. `heartbeatReceived` следи последния term с heartbeat. `LeaderHasSelfHeartbeat` инварианта гарантира, че всеки leader има валиден heartbeat. | `formal-verification/raft.tla` | | FV-3 | ~~2PC: Coordinator crash/recovery~~ ✅ | Добавени `coordinatorLog`, `CrashCoordinator`, `RecoverCoordinator`. Coordinator записва решението в persistent log преди изпращане. | `formal-verification/twopc.tla` | | FV-4 | ~~2PC: Participant timeout~~ ✅ | `ParticipantTimeout` позволява abort само ако coordinator е crashed и НЕ е записал решение (`coordinatorLog = Nil`). | `formal-verification/twopc.tla` | diff --git a/README.md b/README.md index 8d6bfc7..8d55cf7 100644 --- a/README.md +++ b/README.md @@ -55,7 +55,7 @@ with **TLA+** and the TLC model checker. All specs run with **weak fairness** | Algorithm | Spec | States | Properties Verified | |-----------|------|--------|---------------------| -| **Raft Consensus** | `formal-verification/raft.tla` | 3,031,684 | ElectionSafety, LeaderAppendOnly, StateMachineSafety, CommittedIndexValid, LogMatching | +| **Raft Consensus** | `formal-verification/raft.tla` | 38,051,647 | ElectionSafety, LeaderAppendOnly, StateMachineSafety, CommittedIndexValid, LogMatching, LeaderHasSelfHeartbeat | | **Two-Phase Commit** | `formal-verification/twopc.tla` | 22,855,681 | Atomicity, NoOrphanBlocks, CoordinatorConsistency, NoDecideWithoutConsensus, ParticipantStateValid, RecoveryConsistency | | **MVCC** | `formal-verification/mvcc.tla` | 177,721 | NoDirtyReads, ReadOwnWrites, WriteWriteConflict, CommittedMustStart, CommittedVersionsUnique, NoWriteSkew, **CommitProgress** (liveness) | | **Replication** | `formal-verification/replication.tla` | 3,687,939 | AcksRemovePending, PendingAreKnown, AppliedLteCurrent, MonotonicLsn (temporal) | diff --git a/formal-verification/CHANGELOG.md b/formal-verification/CHANGELOG.md index 10bed46..3905aa8 100644 --- a/formal-verification/CHANGELOG.md +++ b/formal-verification/CHANGELOG.md @@ -1,5 +1,28 @@ # BaraDB Formal Verification Changelog +## [1.2.0] — 2026-05-07 + +### Added +- **raft.tla**: `Heartbeat`, `HeartbeatTimeout`, `LeaderLeaseExpired` actions — models leader step-down when quorum is lost +- **raft.tla**: `LeaderHasSelfHeartbeat` invariant — every leader must have a valid heartbeat in its own term +- **raft.tla**: `heartbeatReceived` variable tracks last term in which each node received a heartbeat + +### Improved +- **raft.tla**: `Heartbeat` causes recipients to step down if they see a higher term (realistic AppendEntries behavior) + +### Model Checker Configs (v1.2.0) +| Spec | Model Bounds | States Checked | Properties | +|------|-------------|---------------|------------| +| raft | 3 nodes, MaxTerm=3, MaxLogLen=3 | 38,051,647 | 7 invariants + fair execution | +| twopc | 3 participants, MaxTxnId=3 | 22,855,681 | 7 invariants + fair execution | +| mvcc | 2 keys, 2 values, MaxTxnId=2 | 177,721 | 7 invariants + 1 liveness | +| replication | 3 replicas, MaxLsn=3, MaxSyncCount=2 | 3,687,939 | 4 invariants + 1 temporal | +| gossip | 3 nodes, MaxIncarnation=3 | 692,497 | 4 invariants + fair execution | +| deadlock | 5 txns, MaxEdges=8 | 3,767,361 | 2 invariants | +| sharding | 3 shards, 2 nodes, 5 vnodes | 186,305 | 3 invariants | + +--- + ## [1.1.0] — 2026-05-07 ### Added diff --git a/formal-verification/VERSION b/formal-verification/VERSION index 9084fa2..26aaba0 100644 --- a/formal-verification/VERSION +++ b/formal-verification/VERSION @@ -1 +1 @@ -1.1.0 +1.2.0 diff --git a/formal-verification/models/raft.cfg b/formal-verification/models/raft.cfg index d1381da..299d5d3 100644 --- a/formal-verification/models/raft.cfg +++ b/formal-verification/models/raft.cfg @@ -15,4 +15,5 @@ INVARIANTS StateMachineSafety CommittedIndexValid LogMatching + LeaderHasSelfHeartbeat diff --git a/formal-verification/raft.tla b/formal-verification/raft.tla index eb6b398..d8345cb 100644 --- a/formal-verification/raft.tla +++ b/formal-verification/raft.tla @@ -29,9 +29,10 @@ VARIABLES commitIndex, \* commitIndex[n] ∈ Nat votesGranted, \* votesGranted[n] ⊆ Nodes (only meaningful for Candidates) nextIndex, \* nextIndex[n][m] ∈ Nat (leader state) - matchIndex \* matchIndex[n][m] ∈ Nat (leader state) + matchIndex, \* matchIndex[n][m] ∈ Nat (leader state) + heartbeatReceived \* heartbeatReceived[n] ∈ 0..MaxTerm — last term in which node n received a heartbeat -vars == <> +vars == <> ----------------------------------------------------------------------------- @@ -71,6 +72,7 @@ Init == /\ votesGranted = [n \in Nodes |-> {}] /\ nextIndex = [n \in Nodes |-> [m \in Nodes |-> 1]] /\ matchIndex = [n \in Nodes |-> [m \in Nodes |-> 0]] + /\ heartbeatReceived = [n \in Nodes |-> 0] ----------------------------------------------------------------------------- \* State transitions @@ -83,7 +85,7 @@ Timeout(i) == /\ currentTerm' = [currentTerm EXCEPT ![i] = @ + 1] /\ votedFor' = [votedFor EXCEPT ![i] = i] /\ votesGranted' = [votesGranted EXCEPT ![i] = {i}] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Node i votes for node j in j's current term. Vote(i, j) == @@ -95,7 +97,7 @@ Vote(i, j) == /\ state' = [state EXCEPT ![i] = "Follower"] /\ votedFor' = [votedFor EXCEPT ![i] = j] /\ votesGranted' = [votesGranted EXCEPT ![j] = @ \cup {i}] - /\ UNCHANGED <> + /\ UNCHANGED <> \* A candidate becomes leader after receiving a majority. BecomeLeader(i) == @@ -104,6 +106,7 @@ BecomeLeader(i) == /\ state' = [state EXCEPT ![i] = "Leader"] /\ nextIndex' = [nextIndex EXCEPT ![i] = [m \in Nodes |-> Len(log[i]) + 1]] /\ matchIndex' = [matchIndex EXCEPT ![i] = [m \in Nodes |-> 0]] + /\ heartbeatReceived' = [heartbeatReceived EXCEPT ![i] = currentTerm[i]] /\ UNCHANGED <> \* Leader i appends a new entry to its own log. @@ -116,7 +119,7 @@ AppendEntry(i) == THEN TRUE ELSE log[i][Len(log[i])][1] = currentTerm[i] /\ log' = [log EXCEPT ![i] = Append(@, <>)] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Leader i replicates its log to follower j. \* Now includes prevLogIndex/prevLogTerm check and conflict truncation. @@ -142,7 +145,7 @@ Replicate(i, j) == /\ commitIndex' = [commitIndex EXCEPT ![j] = newCommit] /\ matchIndex' = [matchIndex EXCEPT ![i][j] = newMatch] /\ nextIndex' = [nextIndex EXCEPT ![i][j] = @ + 1] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Follower j rejects an AppendEntries from leader i because of prevLog mismatch. RejectAppendEntries(i, j) == @@ -151,7 +154,7 @@ RejectAppendEntries(i, j) == /\ nextIndex[i][j] > 1 /\ ~HasCompatiblePrefix(j, i, nextIndex[i][j]) /\ nextIndex' = [nextIndex EXCEPT ![i][j] = @ - 1] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Leader i updates commitIndex when a majority has replicated an entry. Commit(i) == @@ -162,7 +165,7 @@ Commit(i) == /\ log[i][idx][1] = currentTerm[i]} IN candidates /= {} /\ commitIndex' = [commitIndex EXCEPT ![i] = CHOOSE idx \in candidates : TRUE] - /\ UNCHANGED <> + /\ UNCHANGED <> \* A follower learns about a higher term and steps down. StepDown(i, newTerm) == @@ -172,8 +175,48 @@ StepDown(i, newTerm) == /\ state' = [state EXCEPT ![i] = "Follower"] /\ votedFor' = [votedFor EXCEPT ![i] = Nil] /\ votesGranted' = [votesGranted EXCEPT ![i] = {}] + /\ UNCHANGED <> + +\* Leader i sends a heartbeat to node j in its current term. +\* Only an up-to-date leader (term >= recipient's term) may send heartbeats. +\* If j sees a higher term, it steps down (same as AppendEntries handling). +Heartbeat(i, j) == + /\ i /= j + /\ state[i] = "Leader" + /\ currentTerm[i] >= currentTerm[j] + /\ IF currentTerm[i] > currentTerm[j] + THEN /\ currentTerm' = [currentTerm EXCEPT ![j] = currentTerm[i]] + /\ state' = [state EXCEPT ![j] = "Follower"] + /\ votedFor' = [votedFor EXCEPT ![j] = Nil] + /\ votesGranted' = [votesGranted EXCEPT ![j] = {}] + /\ heartbeatReceived' = [heartbeatReceived EXCEPT ![j] = currentTerm[i]] + /\ UNCHANGED <> + ELSE /\ heartbeatReceived' = [heartbeatReceived EXCEPT ![j] = currentTerm[i]] + /\ UNCHANGED <> + +\* A follower times out because it has not received a heartbeat from the leader. +\* This can only happen if heartbeatReceived for its current term is FALSE. +HeartbeatTimeout(i) == + /\ state[i] = "Follower" + /\ heartbeatReceived[i] < currentTerm[i] + /\ currentTerm[i] < MaxTerm + /\ state' = [state EXCEPT ![i] = "Candidate"] + /\ currentTerm' = [currentTerm EXCEPT ![i] = @ + 1] + /\ votedFor' = [votedFor EXCEPT ![i] = i] + /\ votesGranted' = [votesGranted EXCEPT ![i] = {i}] + /\ heartbeatReceived' = [heartbeatReceived EXCEPT ![i] = currentTerm[i] + 1] /\ UNCHANGED <> +\* Leader i steps down because it could not reach a majority with heartbeats. +\* This models a network partition where the leader loses quorum connectivity. +LeaderLeaseExpired(i) == + /\ state[i] = "Leader" + /\ LET majority == (Cardinality(Nodes) \div 2) + 1 + acks == Cardinality({j \in Nodes : heartbeatReceived[j] = currentTerm[i]}) + IN acks < majority + /\ state' = [state EXCEPT ![i] = "Follower"] + /\ UNCHANGED <> + ----------------------------------------------------------------------------- \* Next-state relation @@ -186,6 +229,9 @@ Next == \/ \E i, j \in Nodes : RejectAppendEntries(i, j) \/ \E i \in Nodes : Commit(i) \/ \E i \in Nodes : \E t \in 2..MaxTerm : StepDown(i, t) + \/ \E i, j \in Nodes : Heartbeat(i, j) + \/ \E i \in Nodes : HeartbeatTimeout(i) + \/ \E i \in Nodes : LeaderLeaseExpired(i) ----------------------------------------------------------------------------- \* Safety properties @@ -230,6 +276,22 @@ TypeOk == /\ votesGranted \in [Nodes -> SUBSET Nodes] /\ nextIndex \in [Nodes -> [Nodes -> 1..(MaxLogLen+1)]] /\ matchIndex \in [Nodes -> [Nodes -> 0..MaxLogLen]] + /\ heartbeatReceived \in [Nodes -> 0..MaxTerm] + +\* Safety properties for leader lease / heartbeat + +\* A leader must have sent itself a heartbeat in its own term. +LeaderHasSelfHeartbeat == + \A i \in Nodes : + state[i] = "Leader" => heartbeatReceived[i] = currentTerm[i] + +\* If a leader has not reached a majority with heartbeats, it cannot remain leader. +\* (This is checked dynamically via LeaderLeaseExpired action.) +LeaderLeaseSafety == + \A t \in 1..MaxTerm : + LET leaders == {i \in Nodes : state[i] = "Leader" /\ currentTerm[i] = t} + acks == Cardinality({j \in Nodes : heartbeatReceived[j] = t}) + IN \A i \in leaders : acks >= (Cardinality(Nodes) \div 2) + 1 \* Liveness properties