From 112ed4764d983ffed86e2c6047ca7e513eddf98b Mon Sep 17 00:00:00 2001 From: dimgigov Date: Thu, 7 May 2026 19:43:58 +0300 Subject: [PATCH] FV-7: MVCC write skew detection - mvcc.tla: Add NoWriteSkew invariant - mvcc.tla: CommitTxn checks for circular read-write dependencies - models/mvcc.cfg: Add NoWriteSkew to checked invariants - Update PLAN.md, ANALYSIS.md, README.md --- PLAN.md | 2 +- formal-verification/ANALYSIS.md | 4 ++-- formal-verification/README.md | 1 + formal-verification/models/mvcc.cfg | 1 + formal-verification/mvcc.tla | 13 +++++++++++++ 5 files changed, 18 insertions(+), 3 deletions(-) diff --git a/PLAN.md b/PLAN.md index eb2cc34..327b9d4 100644 --- a/PLAN.md +++ b/PLAN.md @@ -64,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-7 | **MVCC: Write skew detection** | Snapshot isolation допуска write skew — класически бъг. Нито TLA+, нито Nim го проверяват. | `formal-verification/mvcc.tla`, `src/barabadb/core/mvcc.nim` | +| 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/ANALYSIS.md b/formal-verification/ANALYSIS.md index 57489df..f9457ac 100644 --- a/formal-verification/ANALYSIS.md +++ b/formal-verification/ANALYSIS.md @@ -96,9 +96,9 @@ - Version cleanup (стари версии се трият при compaction) - Long-running transaction handling (транзакции със стар snapshot) -- Write skew detection (класически проблем на snapshot isolation) +- ~~Write skew detection~~ ✅ Направено — `NoWriteSkew` инвариантата е добавена в `mvcc.tla` -**Препоръка:** Добавяне на `CleanupOldVersions` действие и `NoWriteSkew` инвариант (изисква tracking на predicate-based read/write конфликти). +**Препоръка:** Добавяне на `CleanupOldVersions` действие. ### 2.7. Няма интеграция с Nim тестовете diff --git a/formal-verification/README.md b/formal-verification/README.md index 2025156..d65f5ac 100644 --- a/formal-verification/README.md +++ b/formal-verification/README.md @@ -87,6 +87,7 @@ java -cp tla2tools.jar tlc2.TLC -config models/sharding.cfg sharding.tla - `WriteWriteConflict` — no two committed transactions write the same key (first-committer-wins). - `CommittedMustStart` — committed transactions have a valid start timestamp. - `CommittedVersionsUnique` — no two committed versions for a key share the same txnId. +- `NoWriteSkew` — no two committed transactions have a circular read-write dependency. ### replication.tla - `MonotonicLsn` (temporal) — the applied LSN never decreases. diff --git a/formal-verification/models/mvcc.cfg b/formal-verification/models/mvcc.cfg index acf4744..54e1c63 100644 --- a/formal-verification/models/mvcc.cfg +++ b/formal-verification/models/mvcc.cfg @@ -16,3 +16,4 @@ INVARIANTS WriteWriteConflict CommittedMustStart CommittedVersionsUnique + NoWriteSkew diff --git a/formal-verification/mvcc.tla b/formal-verification/mvcc.tla index 7c0158e..589f592 100644 --- a/formal-verification/mvcc.tla +++ b/formal-verification/mvcc.tla @@ -84,11 +84,16 @@ Write(t, k, v) == /\ UNCHANGED <> \* Commit transaction t: mark its versions as committed (first-committer-wins). +\* Also checks for write skew: if another committed txn read a key we wrote, +\* and wrote a key we read, that's a circular dependency and we must abort. CommitTxn(t) == /\ txnState[t] = "Active" /\ txnStartTs[t] > 0 /\ ~(\E t2 \in 1..MaxTxnId : t2 /= t /\ txnState[t2] = "Committed" /\ \E k \in Keys : k \in writeSet[t] /\ k \in writeSet[t2]) + /\ ~(\E t2 \in 1..MaxTxnId : t2 /= t /\ txnState[t2] = "Committed" /\ + \E k1 \in Keys : k1 \in writeSet[t] /\ k1 \in readSet[t2] /\ + \E k2 \in Keys : k2 \in writeSet[t2] /\ k2 \in readSet[t]) /\ txnState' = [txnState EXCEPT ![t] = "Committed"] /\ db' = [k \in Keys |-> IF k \in writeSet[t] @@ -142,6 +147,14 @@ WriteWriteConflict == t1 /= t2 /\ txnState[t1] = "Committed" /\ txnState[t2] = "Committed" => ~(\E k \in Keys : k \in writeSet[t1] /\ k \in writeSet[t2]) +\* No write skew: two committed transactions cannot have a circular read-write dependency. +\* If t1 writes a key that t2 read, then t2 cannot write a key that t1 read. +NoWriteSkew == + \A t1, t2 \in 1..MaxTxnId : + t1 /= t2 /\ txnState[t1] = "Committed" /\ txnState[t2] = "Committed" => + ~(\E k1 \in Keys : k1 \in writeSet[t1] /\ k1 \in readSet[t2] /\ + \E k2 \in Keys : k2 \in writeSet[t2] /\ k2 \in readSet[t1]) + \* A committed transaction must have been started (has start timestamp > 0). CommittedMustStart == \A t \in 1..MaxTxnId :