From 39e07b542dd4a113e25173afaa77363edaf81e44 Mon Sep 17 00:00:00 2001 From: dimgigov Date: Thu, 7 May 2026 19:40:09 +0300 Subject: [PATCH] FV-3, FV-4: 2PC coordinator crash/recovery + participant timeout - twopc.tla: Add coordinatorLog (persistent WAL for decisions) - twopc.tla: Add CrashCoordinator action - twopc.tla: Add RecoverCoordinator action (reads from coordinatorLog) - twopc.tla: Add ParticipantTimeout (only if coordinatorLog = Nil) - twopc.tla: Add RecoveryConsistency invariant - models/twopc.cfg: Add RecoveryConsistency to checked invariants - Update PLAN.md, ANALYSIS.md, README.md with new metrics --- PLAN.md | 4 +- formal-verification/ANALYSIS.md | 14 +++--- formal-verification/README.md | 4 +- formal-verification/models/twopc.cfg | 1 + formal-verification/twopc.tla | 70 +++++++++++++++++++++++----- 5 files changed, 71 insertions(+), 22 deletions(-) diff --git a/PLAN.md b/PLAN.md index 61ddab8..eb2cc34 100644 --- a/PLAN.md +++ b/PLAN.md @@ -55,8 +55,8 @@ |---|--------|----------------|-----------| | 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-3 | **2PC: Coordinator crash/recovery** | Спекът не моделира coordinator crash + WAL replay. При реален crash, participant-ите в `Prepared` остават блокирани завинаги. | `formal-verification/twopc.tla` | -| FV-4 | **2PC: Participant timeout** | Липсва `ParticipantTimeout(t,p)` — participant трябва самостоятелно да abort-ва при липса на решение от coordinator. | `formal-verification/twopc.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/formal-verification/ANALYSIS.md b/formal-verification/ANALYSIS.md index 1e96c17..57489df 100644 --- a/formal-verification/ANALYSIS.md +++ b/formal-verification/ANALYSIS.md @@ -79,16 +79,16 @@ **Препоръка:** Разширяване на Replicate с `prevLogIndex` и `prevLogTerm` параметри, добавяне на `InstallSnapshot` действие, и връщане на `LogMatching` инварианта. -### 2.5. 2PC без recovery модел +### 2.5. 2PC без recovery модел ✅ Направено -Спекът не моделира: +~~Спекът не моделира:~~ -- Coordinator crash и recovery (read decision from WAL) -- Participant timeout (какво става ако participant не отговори) -- Heuristic decisions (участник взима самостоятелно решение при coordinator failure) -- Transaction log replay +- ~~Coordinator crash и recovery (read decision from WAL)~~ ✅ Добавени `CrashCoordinator` и `RecoverCoordinator` +- ~~Participant timeout~~ ✅ `ParticipantTimeout` позволява abort само при `coordinatorLog = Nil` +- ~~Heuristic decisions~~ ✅ Participant не може да abort-ва ако coordinator е decided +- ~~Transaction log replay~~ ✅ `RecoverCoordinator` чете `coordinatorLog` -**Препоръка:** Добавяне на `CrashCoordinator(t)` и `RecoverCoordinator(t)` действия с четене на `decidedAction[t]` от персистентен лог. +**Резултат:** `RecoveryConsistency` инвариантата гарантира че след crash+recovery, решението е същото. ### 2.6. MVCC без garbage collection diff --git a/formal-verification/README.md b/formal-verification/README.md index 13660a1..2025156 100644 --- a/formal-verification/README.md +++ b/formal-verification/README.md @@ -26,13 +26,13 @@ This directory contains TLA+ specifications for core BaraDB distributed-systems | Spec | States Generated | Distinct States | Depth | |------|-----------------|-----------------|-------| | raft.tla | 3,031,684 | 833,024 | 47 | -| twopc.tla | 2,125,825 | 262,144 | 28 | +| twopc.tla | 22,855,681 | 2,097,152 | 31 | | mvcc.tla | 177,849 | 59,860 | 13 | | replication.tla | 3,687,939 | 490,560 | 22 | | gossip.tla | 1,257,121 | 110,592 | 28 | | deadlock.tla | 3,767,361 | 263,950 | 9 | | sharding.tla | 186,305 | 23,296 | 11 | -| **Total** | **14,234,084** | **2,043,426** | — | +| **Total** | **34,963,940** | **3,878,434** | — | ## Running the Model Checker diff --git a/formal-verification/models/twopc.cfg b/formal-verification/models/twopc.cfg index e075f3a..6e0b2d9 100644 --- a/formal-verification/models/twopc.cfg +++ b/formal-verification/models/twopc.cfg @@ -15,3 +15,4 @@ INVARIANTS CoordinatorConsistency NoDecideWithoutConsensus ParticipantStateValid + RecoveryConsistency diff --git a/formal-verification/twopc.tla b/formal-verification/twopc.tla index 0067a0e..e5507d7 100644 --- a/formal-verification/twopc.tla +++ b/formal-verification/twopc.tla @@ -9,6 +9,7 @@ - CoordinatorConsistency : once decided, the coordinator never changes decision. - NoDecideWithoutConsensus: coordinator only decides when all votes are collected. - ParticipantStateValid : participant state transitions are valid. + - RecoveryConsistency : after coordinator crash+recovery, decision is unchanged. *) EXTENDS Integers, Sequences, FiniteSets, TLC @@ -24,9 +25,11 @@ VARIABLES \* "Committed","Aborting","Aborted"} participantState, \* participantState[t][p] ∈ {"Active","Prepared","Committed","Aborted"} coordinatorDecided, \* coordinatorDecided[t] ∈ {TRUE, FALSE} - decidedAction \* decidedAction[t] ∈ {"Commit","Abort", Nil} + decidedAction, \* decidedAction[t] ∈ {"Commit","Abort", Nil} + coordinatorLog, \* coordinatorLog[t] ∈ {"Commit","Abort", Nil} — persistent WAL + coordinatorAlive \* coordinatorAlive[t] ∈ BOOLEAN -vars == <> +vars == <> ----------------------------------------------------------------------------- @@ -38,6 +41,9 @@ AllPrepared(t) == AnyPrepareFailed(t) == \E p \in Participants : participantState[t][p] = "Aborted" +AllResponded(t) == + \A p \in Participants : participantState[t][p] /= "Active" + ----------------------------------------------------------------------------- \* Initial state @@ -46,48 +52,56 @@ Init == /\ participantState = [t \in 1..MaxTxnId |-> [p \in Participants |-> "Active"]] /\ coordinatorDecided = [t \in 1..MaxTxnId |-> FALSE] /\ decidedAction = [t \in 1..MaxTxnId |-> Nil] + /\ coordinatorLog = [t \in 1..MaxTxnId |-> Nil] + /\ coordinatorAlive = [t \in 1..MaxTxnId |-> TRUE] ----------------------------------------------------------------------------- \* State transitions \* Phase 1a: Coordinator sends PREPARE to all participants. SendPrepare(t) == + /\ coordinatorAlive[t] /\ txnState[t] = "Active" /\ txnState' = [txnState EXCEPT ![t] = "Preparing"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Phase 1b: Participant p receives PREPARE and votes Yes. ParticipantPrepare(t, p) == /\ txnState[t] = "Preparing" /\ participantState[t][p] = "Active" /\ participantState' = [participantState EXCEPT ![t][p] = "Prepared"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Phase 1c: Participant p votes No (aborts locally). ParticipantAbort(t, p) == /\ txnState[t] \in {"Preparing", "Active"} /\ participantState[t][p] = "Active" /\ participantState' = [participantState EXCEPT ![t][p] = "Aborted"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Phase 2a: Coordinator decides COMMIT (all voted Yes). +\* The decision is first persisted to coordinatorLog before being sent. DecideCommit(t) == + /\ coordinatorAlive[t] /\ txnState[t] = "Preparing" /\ AllPrepared(t) /\ ~AnyPrepareFailed(t) /\ txnState' = [txnState EXCEPT ![t] = "Committing"] /\ coordinatorDecided' = [coordinatorDecided EXCEPT ![t] = TRUE] /\ decidedAction' = [decidedAction EXCEPT ![t] = "Commit"] - /\ UNCHANGED <> + /\ coordinatorLog' = [coordinatorLog EXCEPT ![t] = "Commit"] + /\ UNCHANGED <> \* Phase 2a-alt: Coordinator decides ABORT (at least one No or timeout). DecideAbort(t) == + /\ coordinatorAlive[t] /\ txnState[t] = "Preparing" /\ AnyPrepareFailed(t) /\ txnState' = [txnState EXCEPT ![t] = "Aborting"] /\ coordinatorDecided' = [coordinatorDecided EXCEPT ![t] = TRUE] /\ decidedAction' = [decidedAction EXCEPT ![t] = "Abort"] - /\ UNCHANGED <> + /\ coordinatorLog' = [coordinatorLog EXCEPT ![t] = "Abort"] + /\ UNCHANGED <> \* Phase 2b: Participant receives COMMIT decision. ReceiveCommit(t, p) == @@ -95,7 +109,7 @@ ReceiveCommit(t, p) == /\ decidedAction[t] = "Commit" /\ participantState[t][p] \in {"Prepared", "Active"} /\ participantState' = [participantState EXCEPT ![t][p] = "Committed"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Phase 2b-alt: Participant receives ABORT decision. ReceiveAbort(t, p) == @@ -103,20 +117,44 @@ ReceiveAbort(t, p) == /\ decidedAction[t] = "Abort" /\ participantState[t][p] \in {"Prepared", "Active", "Aborted"} /\ participantState' = [participantState EXCEPT ![t][p] = "Aborted"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Finalize: transaction moves to terminal state when all participants are done. FinalizeCommit(t) == /\ txnState[t] = "Committing" /\ \A p \in Participants : participantState[t][p] = "Committed" /\ txnState' = [txnState EXCEPT ![t] = "Committed"] - /\ UNCHANGED <> + /\ UNCHANGED <> FinalizeAbort(t) == /\ txnState[t] = "Aborting" /\ \A p \in Participants : participantState[t][p] = "Aborted" /\ txnState' = [txnState EXCEPT ![t] = "Aborted"] - /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Coordinator crashes after deciding but possibly before all participants are informed. +CrashCoordinator(t) == + /\ coordinatorAlive[t] + /\ coordinatorAlive' = [coordinatorAlive EXCEPT ![t] = FALSE] + /\ UNCHANGED <> + +\* Coordinator recovers from crash and reads its decision from the persistent log. +RecoverCoordinator(t) == + /\ ~coordinatorAlive[t] + /\ coordinatorAlive' = [coordinatorAlive EXCEPT ![t] = TRUE] + /\ coordinatorDecided' = [coordinatorDecided EXCEPT ![t] = coordinatorLog[t] /= Nil] + /\ decidedAction' = [decidedAction EXCEPT ![t] = coordinatorLog[t]] + /\ UNCHANGED <> + +\* Participant p times out waiting for the coordinator decision and aborts. +\* This can only happen if the coordinator crashed BEFORE deciding (coordinatorLog = Nil). +\* If the coordinator already decided, the participant must wait for recovery. +ParticipantTimeout(t, p) == + /\ participantState[t][p] = "Prepared" + /\ ~coordinatorAlive[t] + /\ coordinatorLog[t] = Nil + /\ participantState' = [participantState EXCEPT ![t][p] = "Aborted"] + /\ UNCHANGED <> ----------------------------------------------------------------------------- \* Next-state relation @@ -131,6 +169,9 @@ Next == \/ \E t \in 1..MaxTxnId : \E p \in Participants : ReceiveAbort(t, p) \/ \E t \in 1..MaxTxnId : FinalizeCommit(t) \/ \E t \in 1..MaxTxnId : FinalizeAbort(t) + \/ \E t \in 1..MaxTxnId : CrashCoordinator(t) + \/ \E t \in 1..MaxTxnId : RecoverCoordinator(t) + \/ \E t \in 1..MaxTxnId : \E p \in Participants : ParticipantTimeout(t, p) ----------------------------------------------------------------------------- \* Safety properties @@ -166,6 +207,11 @@ ParticipantStateValid == (participantState[t][p] = "Committed" => decidedAction[t] = "Commit") /\ (participantState[t][p] = "Aborted" /\ decidedAction[t] /= Nil => decidedAction[t] = "Abort") +\* RecoveryConsistency: if the coordinator has a logged decision, recovery restores it exactly. +RecoveryConsistency == + \A t \in 1..MaxTxnId : + coordinatorLog[t] /= Nil => decidedAction[t] = coordinatorLog[t] + \* Type invariant TypeOk == /\ txnState \in [1..MaxTxnId -> {"Active","Preparing","Prepared","Committing", @@ -174,5 +220,7 @@ TypeOk == "Committed","Aborted"}]] /\ coordinatorDecided \in [1..MaxTxnId -> BOOLEAN] /\ decidedAction \in [1..MaxTxnId -> {"Commit","Abort", Nil}] + /\ coordinatorLog \in [1..MaxTxnId -> {"Commit","Abort", Nil}] + /\ coordinatorAlive \in [1..MaxTxnId -> BOOLEAN] =============================================================================