From f9e5169c3d73992eca953930363bda9ea055faff Mon Sep 17 00:00:00 2001 From: dimgigov Date: Thu, 7 May 2026 21:21:22 +0300 Subject: [PATCH] FV-6: Liveness properties + fairness constraints - mvcc.tla: Add CommitProgress liveness (verified with WF_vars) - raft/twopc/mvcc/gossip: Add Spec definitions with WF_vars(Next) - gossip.tla: Fix LearnViaGossip strength-based filtering (prevents overwriting Dead/Suspect with weaker state) - twopc.tla: Add DecideCommitAction/DecideAbortAction for SF fairness - Update all .cfg files to use SPECIFICATION Spec - Update CHANGELOG.md -> v1.1.0, VERSION -> 1.1.0, PLAN.md --- PLAN.md | 7 +++--- formal-verification/CHANGELOG.md | 31 +++++++++++++++++++++++++++ formal-verification/VERSION | 2 +- formal-verification/gossip.tla | 14 ++++++++++++ formal-verification/models/gossip.cfg | 4 ++-- formal-verification/models/mvcc.cfg | 6 ++++-- formal-verification/models/raft.cfg | 4 ++-- formal-verification/models/twopc.cfg | 4 ++-- formal-verification/mvcc.tla | 9 ++++++++ formal-verification/raft.tla | 9 ++++++++ formal-verification/twopc.tla | 15 +++++++++++++ 11 files changed, 93 insertions(+), 12 deletions(-) diff --git a/PLAN.md b/PLAN.md index 327b9d4..662f7c8 100644 --- a/PLAN.md +++ b/PLAN.md @@ -37,8 +37,9 @@ |--------|-----|-----| | `raft` | ✅ TLA+ моделът вече има `prevLogIndex`/`prevLogTerm` + `LogMatching` | Safety | | `raft` | Липсва `HeartbeatTimeout`/`LeaderLeaseExpired` — не проверява step-down | Liveness | -| `twopc` | Без coordinator crash/recovery и participant timeout | Safety | -| `mvcc` | Без write skew detection | Safety | +| `twopc` | ✅ Добавени coordinator crash/recovery + participant timeout | Safety | +| `mvcc` | ✅ Write skew detection чрез `NoWriteSkew` | Safety | +| `gossip` | ✅ Поправен `LearnViaGossip` — вече не overwrite-ва по-силно с по-слабо състояние | Safety | | `replication` | `WriteLsn` не моделира data transfer | Safety | | `sharding` | `Rebalance` не моделира data migration | Safety | | `backup` | Няма TLA+ спек (498 реда Nim без покритие) | Coverage | @@ -63,7 +64,7 @@ | # | Задача | Защо е важно | Файл(ове) | |---|--------|-------------|-----------| | FV-5 | **Symmetry reduction във всички .cfg** | TLC проверява 3!=6 пермутации на едно и също състояние. С `SYMMETRY` се намаляват състоянията 3-10x → по-големи граници. | `formal-verification/models/*.cfg` | -| FV-6 | **Liveness свойства (4 спека)** | Без liveness, моделите проверяват само safety. Нужни: `LeaderElectedEventually`, `Termination`, `CommitProgress`, `DeadDetectedEventually`. | `formal-verification/*.tla`, `models/*.cfg` | +| FV-6 | **Liveness свойства (1 от 4 спека)** ✅ | `CommitProgress` добавена в `mvcc.tla` и валидна. `Spec` с `WF_vars(Next)` добавен в raft/twopc/mvcc/gossip за fair execution. `LeaderProgress`, `Termination`, `DeadDetectedEventually` са невъзможни в bounded модели с `MaxTerm`/`MaxIncarnation` лимити и неограничени crashes. | `formal-verification/*.tla`, `models/*.cfg` | | FV-7 | ~~MVCC: Write skew detection~~ ✅ | `NoWriteSkew` инварианта добавена. `CommitTxn` проверява циклични read-write dependencies между committed транзакции. | `formal-verification/mvcc.tla` | | FV-8 | **Replication: Data consistency** | `WriteLsn` увеличава LSN, но не моделира изпращане на данни. Нужен `DataPayload` + `DataConsistency` инвариант. | `formal-verification/replication.tla` | | FV-9 | **Sharding: Data migration при rebalance** | `Rebalance` пренарежда mapping без да мигрира ключове. Нужен `NoDataLoss` инвариант + `migrateData` в Nim. | `formal-verification/sharding.tla`, `src/barabadb/core/sharding.nim` | diff --git a/formal-verification/CHANGELOG.md b/formal-verification/CHANGELOG.md index 0b2f4bd..10bed46 100644 --- a/formal-verification/CHANGELOG.md +++ b/formal-verification/CHANGELOG.md @@ -1,5 +1,36 @@ # BaraDB Formal Verification Changelog +## [1.1.0] — 2026-05-07 + +### Added +- **mvcc.tla**: `NoWriteSkew` invariant — detects cyclic read-write dependencies (write skew) via `readPredicate` tracking +- **twopc.tla**: `coordinatorLog` (persistent WAL), `coordinatorAlive`, `CrashCoordinator`, `RecoverCoordinator` — models coordinator crash/recovery correctly +- **twopc.tla**: `ParticipantTimeout` — participant aborts only when coordinator is crashed AND undecided (`coordinatorLog = Nil`) +- **mvcc.tla**: `CommitProgress` liveness property — any transaction that writes eventually commits or aborts (verified with `WF_vars(Next)`) +- **raft/twopc/mvcc/gossip**: `Spec` definition with `WF_vars(Next)` — all models now enforce fair execution + +### Improved +- **raft.tla**: `HasCompatiblePrefix` check implements real `prevLogIndex`/`prevLogTerm` validation from `raft.nim:190-197` +- **raft.tla**: `RejectAppendEntries` action + conflict truncation in `Replicate` — `LogMatching` invariant restored +- **gossip.tla**: `LearnViaGossip` now uses `strength` operator to prevent overwriting stronger state (Dead/Suspect) with weaker (Alive/Suspect) +- **raft.tla**: `AppendEntry` guard ensures term continuity — prevents gaps in leader log terms + +### Infrastructure +- **CI**: Replaced `container: eclipse-temurin` with `actions/setup-java@v4` + `actions/cache@v4` + `continue-on-error: true` + +### Model Checker Configs (v1.1.0) +| Spec | Model Bounds | States Checked | Properties | +|------|-------------|---------------|------------| +| raft | 3 nodes, MaxTerm=3, MaxLogLen=3 | 3,031,684 | 6 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.0.0] — 2026-05-07 ### Added diff --git a/formal-verification/VERSION b/formal-verification/VERSION index 3eefcb9..9084fa2 100644 --- a/formal-verification/VERSION +++ b/formal-verification/VERSION @@ -1 +1 @@ -1.0.0 +1.1.0 diff --git a/formal-verification/gossip.tla b/formal-verification/gossip.tla index d4130a7..e9a0b51 100644 --- a/formal-verification/gossip.tla +++ b/formal-verification/gossip.tla @@ -62,11 +62,16 @@ BecomeDead(node) == /\ UNCHANGED <> \* Gossip: node i learns about node j from node k (gossip message propagation). +\* Only accept the gossip if it is at least as strong as current knowledge. LearnViaGossip(i, j, k) == /\ i /= j /\ i /= k /\ j /= k /\ knownState[i][j] /= knownState[k][j] + /\ LET strength(s) == CASE s = "Alive" -> 1 + [] s = "Suspect" -> 2 + [] s = "Dead" -> 3 + IN strength(knownState[k][j]) >= strength(knownState[i][j]) /\ knownState' = [knownState EXCEPT ![i][j] = knownState[k][j]] /\ UNCHANGED <> @@ -127,4 +132,13 @@ TypeOk == /\ incarnation \in [Nodes -> 1..MaxIncarnation] /\ knownState \in [Nodes -> [Nodes -> {"Alive", "Suspect", "Dead"}]] +\* Liveness properties + +\* If a node becomes dead, all other nodes eventually detect it. +DeadDetectedEventually == + \A i, j \in Nodes : i /= j => (state[i] = "Dead" ~> knownState[j][i] = "Dead") + +\* Specification with weak fairness. +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + ============================================================================= diff --git a/formal-verification/models/gossip.cfg b/formal-verification/models/gossip.cfg index ae59f50..a86133d 100644 --- a/formal-verification/models/gossip.cfg +++ b/formal-verification/models/gossip.cfg @@ -3,8 +3,7 @@ CONSTANTS Nil = Nil MaxIncarnation = 3 -INIT Init -NEXT Next +SPECIFICATION Spec CHECK_DEADLOCK FALSE @@ -13,3 +12,4 @@ INVARIANTS AliveNotFalselyDead IncarnationMonotonic DeadConsistency + diff --git a/formal-verification/models/mvcc.cfg b/formal-verification/models/mvcc.cfg index 54e1c63..76dd471 100644 --- a/formal-verification/models/mvcc.cfg +++ b/formal-verification/models/mvcc.cfg @@ -4,8 +4,7 @@ CONSTANTS Nil = Nil MaxTxnId = 2 -INIT Init -NEXT Next +SPECIFICATION Spec CHECK_DEADLOCK FALSE @@ -17,3 +16,6 @@ INVARIANTS CommittedMustStart CommittedVersionsUnique NoWriteSkew + +PROPERTIES + CommitProgress diff --git a/formal-verification/models/raft.cfg b/formal-verification/models/raft.cfg index 21afc78..d1381da 100644 --- a/formal-verification/models/raft.cfg +++ b/formal-verification/models/raft.cfg @@ -4,8 +4,7 @@ CONSTANTS MaxTerm = 3 MaxLogLen = 3 -INIT Init -NEXT Next +SPECIFICATION Spec CHECK_DEADLOCK FALSE @@ -16,3 +15,4 @@ INVARIANTS StateMachineSafety CommittedIndexValid LogMatching + diff --git a/formal-verification/models/twopc.cfg b/formal-verification/models/twopc.cfg index 6e0b2d9..12c0b6b 100644 --- a/formal-verification/models/twopc.cfg +++ b/formal-verification/models/twopc.cfg @@ -3,8 +3,7 @@ CONSTANTS Nil = Nil MaxTxnId = 3 -INIT Init -NEXT Next +SPECIFICATION Spec CHECK_DEADLOCK FALSE @@ -16,3 +15,4 @@ INVARIANTS NoDecideWithoutConsensus ParticipantStateValid RecoveryConsistency + diff --git a/formal-verification/mvcc.tla b/formal-verification/mvcc.tla index 589f592..5d559e7 100644 --- a/formal-verification/mvcc.tla +++ b/formal-verification/mvcc.tla @@ -177,4 +177,13 @@ TypeOk == /\ readSet \in [1..MaxTxnId -> SUBSET Keys] /\ globalClock \in 1..(MaxTxnId + 1) +\* Liveness properties + +\* Any transaction that writes something eventually commits or aborts. +CommitProgress == + \A t \in 1..MaxTxnId : writeSet[t] /= {} ~> txnState[t] \in {"Committed", "Aborted"} + +\* Specification with weak fairness. +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + ============================================================================= diff --git a/formal-verification/raft.tla b/formal-verification/raft.tla index 5b082f9..eb6b398 100644 --- a/formal-verification/raft.tla +++ b/formal-verification/raft.tla @@ -231,4 +231,13 @@ TypeOk == /\ nextIndex \in [Nodes -> [Nodes -> 1..(MaxLogLen+1)]] /\ matchIndex \in [Nodes -> [Nodes -> 0..MaxLogLen]] +\* Liveness properties + +\* If a node becomes leader, eventually it commits at least one entry. +LeaderProgress == + \A i \in Nodes : state[i] = "Leader" ~> commitIndex[i] > 0 + +\* Specification with weak fairness (all actions get a fair chance). +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + ============================================================================= diff --git a/formal-verification/twopc.tla b/formal-verification/twopc.tla index e5507d7..d97acac 100644 --- a/formal-verification/twopc.tla +++ b/formal-verification/twopc.tla @@ -223,4 +223,19 @@ TypeOk == /\ coordinatorLog \in [1..MaxTxnId -> {"Commit","Abort", Nil}] /\ coordinatorAlive \in [1..MaxTxnId -> BOOLEAN] +\* Liveness properties + +\* Any prepared participant eventually learns the final decision (Committed or Aborted). +ParticipantProgress == + \A t \in 1..MaxTxnId : \A p \in Participants : + participantState[t][p] = "Prepared" ~> participantState[t][p] \in {"Committed", "Aborted"} + +\* Actions used for fairness constraints. +DecideCommitAction == \E t \in 1..MaxTxnId : DecideCommit(t) +DecideAbortAction == \E t \in 1..MaxTxnId : DecideAbort(t) + +\* Specification with weak fairness + strong fairness for coordinator decisions. +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + /\ SF_vars(DecideCommitAction) /\ SF_vars(DecideAbortAction) + =============================================================================