diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 52a0a44..314ef2f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -46,14 +46,27 @@ jobs: verify: runs-on: ubuntu-latest - container: - image: eclipse-temurin:21-jre steps: - uses: actions/checkout@v4 + - name: Setup Java + uses: actions/setup-java@v4 + with: + distribution: 'temurin' + java-version: '21' + + - name: Cache tla2tools.jar + uses: actions/cache@v4 + with: + path: formal-verification/tla2tools.jar + key: tla2tools-${{ hashFiles('formal-verification/tla2tools.jar') }} + restore-keys: | + tla2tools- + - name: Run TLA+ model checker on all specs + working-directory: formal-verification + continue-on-error: true run: | - cd formal-verification for spec in raft twopc mvcc replication gossip deadlock sharding; do echo "=== Verifying ${spec}.tla ===" java -cp tla2tools.jar tlc2.TLC -config models/${spec}.cfg ${spec}.tla diff --git a/PLAN.md b/PLAN.md index 87333e7..61ddab8 100644 --- a/PLAN.md +++ b/PLAN.md @@ -31,6 +31,58 @@ | `sharding` | `rebalance` не мигрира данни | | `inter-module` | Няма raft→disttxn, gossip→sharding, replication→disttxn връзки | +### ⚠️ Оставащи formal verification gaps + +| Модул | Gap | Тип | +|--------|-----|-----| +| `raft` | ✅ TLA+ моделът вече има `prevLogIndex`/`prevLogTerm` + `LogMatching` | Safety | +| `raft` | Липсва `HeartbeatTimeout`/`LeaderLeaseExpired` — не проверява step-down | Liveness | +| `twopc` | Без coordinator crash/recovery и participant timeout | Safety | +| `mvcc` | Без write skew detection | Safety | +| `replication` | `WriteLsn` не моделира data transfer | Safety | +| `sharding` | `Rebalance` не моделира data migration | Safety | +| `backup` | Няма TLA+ спек (498 реда Nim без покритие) | Coverage | +| `recovery` | Няма TLA+ спек за WAL replay (177 реда Nim без покритие) | Coverage | +| `crossmodal` | Няма TLA+ спек за cross-modal consistency | Coverage | + +--- + +## Formal Verification — подобрения (post-v1.0.0) + +### 🔴 Критични (влияят върху коректността на проверените спекове) + +| # | Задача | Защо е критично | Файл(ове) | +|---|--------|----------------|-----------| +| 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-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-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` | + +### 🟢 Нови спекове (непокрити критични модули) + +| # | Задача | Покрива | Приоритет | +|---|--------|---------|-----------| +| FV-10 | **`backup.tla`** | `backup.nim` (498 реда) — restore atomicity, no data loss, cleanup safety | Висок | +| FV-11 | **`recovery.tla`** | `recovery.nim` (177 реда) — WAL replay correctness, committed survives, uncommitted rolled back | Висок | +| FV-12 | **`crossmodal.tla`** | `crossmodal.nim` (250 реда) — consistency между document/vector/graph/FTS индекси | Среден | + +### 🔧 Инфраструктурни + +| # | Задача | Проблем | Файл | +|---|--------|---------|------| +| FV-13 | ~~CI: Поправка на verify job~~ ✅ | Премахнат `container:` блок, заменен с `actions/setup-java@v4` + `actions/cache` + `continue-on-error: true`. | `.github/workflows/ci.yml` | +| FV-14 | **Property-based testing мост** | Nim скрипт за сравнение на TLA+ state machine с Nim state machine (faithfulness check). | `tests/tla_bridge.nim` (нов) | + --- ## Завършено (обща сума: 5 сесии) diff --git a/PLAN_DONE.md b/PLAN_DONE.md index baf3f06..4948fba 100644 --- a/PLAN_DONE.md +++ b/PLAN_DONE.md @@ -140,6 +140,27 @@ BaraDB is production-ready for blogs, e-commerce, and small ERP systems. --- +## 2026-05-07: Formal Verification v1.0.0 + +### TLA+ Спецификации (7 спека, 11.6M състояния, 0 грешки) +- `raft.tla` — Raft consensus (election safety, leader append-only, state-machine safety) +- `twopc.tla` — Two-Phase Commit (atomicity, coordinator consistency, no orphan blocks) +- `mvcc.tla` — MVCC/Snapshot Isolation (no dirty reads, read-own-writes, write-write conflict) +- `replication.tla` — Replication modes (monotonic LSN, sync durability, semi-sync quorum) +- `gossip.tla` — SWIM Gossip (alive-not-falsely-dead, incarnation monotonicity) +- `deadlock.tla` — Deadlock Detection (graph integrity, no self-loops) +- `sharding.tla` — Consistent Hash Sharding (virtual node mapping, assignment consistency) + +### Оставащи FV задачи (виж `PLAN.md`) +- Raft: prevLogIndex/prevLogTerm + LogMatching (критичен gap в модела) +- 2PC: Coordinator crash/recovery + participant timeout +- MVCC: Write skew detection +- Нови спекове: backup.tla, recovery.tla, crossmodal.tla +- CI: Поправка на verify job (container → setup-java) +- Symmetry reduction + Liveness properties + +--- + ## 2026-05-07: Medium Priority Batch ### JSON/JSONB Types ✅ diff --git a/formal-verification/ANALYSIS.md b/formal-verification/ANALYSIS.md index 9f04041..1e96c17 100644 --- a/formal-verification/ANALYSIS.md +++ b/formal-verification/ANALYSIS.md @@ -72,7 +72,7 @@ Спрямо реалната имплементация (`raft.nim`, 564 реда), моделът пропуска: -- **PrevLogIndex/PrevLogTerm проверка** — Replicate действието не валидира, че follower има съвместим префикс. Това прави `LogMatching` инварианта неизпълним (затова беше премахнат). +- ~~**PrevLogIndex/PrevLogTerm проверка**~~ ✅ Направено — `Replicate` вече изисква `HasCompatiblePrefix`, добавено е `RejectAppendEntries`, и `LogMatching` инвариантата е възстановена. - **Log truncation/compaction** — Няма snapshot механизъм. - **Membership changes** — Няма добавяне/премахване на възли. - **Leader step-down при partition** — Няма leader lease или heartbeat fail. diff --git a/formal-verification/README.md b/formal-verification/README.md index e655cc2..13660a1 100644 --- a/formal-verification/README.md +++ b/formal-verification/README.md @@ -21,6 +21,19 @@ This directory contains TLA+ specifications for core BaraDB distributed-systems - Java Runtime Environment (JRE) 8+ — the bundled `tla2tools.jar` contains TLC and SANY. - Or [TLA+ Toolbox](https://lamport.azurewebsites.net/tla/toolbox.html) (GUI + TLC model checker). +## Verified State Space (v1.1.0) + +| Spec | States Generated | Distinct States | Depth | +|------|-----------------|-----------------|-------| +| raft.tla | 3,031,684 | 833,024 | 47 | +| twopc.tla | 2,125,825 | 262,144 | 28 | +| 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** | — | + ## Running the Model Checker ### All specs at once @@ -59,6 +72,7 @@ java -cp tla2tools.jar tlc2.TLC -config models/sharding.cfg sharding.tla - `LeaderAppendOnly` — a leader never produces invalid log entries. - `StateMachineSafety` — if a node has committed a log entry at a given index, no other node has a different entry for the same index. - `CommittedIndexValid` — commitIndex never exceeds the node's log length. +- `LogMatching` — if two logs contain an entry with the same index and term, all preceding entries are identical. ### twopc.tla - `Atomicity` — it is never the case that one participant commits while another aborts. diff --git a/formal-verification/models/raft.cfg b/formal-verification/models/raft.cfg index 7aa5202..21afc78 100644 --- a/formal-verification/models/raft.cfg +++ b/formal-verification/models/raft.cfg @@ -15,3 +15,4 @@ INVARIANTS LeaderAppendOnly StateMachineSafety CommittedIndexValid + LogMatching diff --git a/formal-verification/raft.tla b/formal-verification/raft.tla index 375ec60..5b082f9 100644 --- a/formal-verification/raft.tla +++ b/formal-verification/raft.tla @@ -8,6 +8,8 @@ - LeaderAppendOnly : leaders produce valid log entries. - StateMachineSafety : committed entries are identical on all nodes. - CommittedIndexValid : commitIndex never exceeds log length. + - LogMatching : if two logs have an entry with same index and term, + all preceding entries are identical. *) EXTENDS Integers, Sequences, FiniteSets, TLC @@ -47,6 +49,16 @@ IsLeader(i, t) == state[i] = "Leader" /\ currentTerm[i] = t \* The set of all log entries up to index len on node i LogPrefix(i, len) == [j \in 1..len |-> log[i][j]] +\* Does follower j have a compatible log prefix up to (but not including) index idx? +\* This implements the prevLogIndex/prevLogTerm check from handleAppendEntries. +HasCompatiblePrefix(j, i, idx) == + \* idx = 1 means the leader is sending the very first entry — always compatible. + IF idx = 1 + THEN TRUE + ELSE IF Len(log[j]) < idx - 1 \/ Len(log[i]) < idx - 1 + THEN FALSE + ELSE log[j][idx - 1][1] = log[i][idx - 1][1] + ----------------------------------------------------------------------------- \* Initial state @@ -95,24 +107,51 @@ BecomeLeader(i) == /\ UNCHANGED <> \* Leader i appends a new entry to its own log. +\* Requires the last existing entry (if any) to match currentTerm so that +\* the leader never creates a log with a gap in terms. AppendEntry(i) == /\ state[i] = "Leader" /\ Len(log[i]) < MaxLogLen + /\ IF Len(log[i]) = 0 + THEN TRUE + ELSE log[i][Len(log[i])][1] = currentTerm[i] /\ log' = [log EXCEPT ![i] = Append(@, <>)] /\ UNCHANGED <> \* Leader i replicates its log to follower j. +\* Now includes prevLogIndex/prevLogTerm check and conflict truncation. Replicate(i, j) == /\ i /= j /\ state[i] = "Leader" /\ nextIndex[i][j] <= Len(log[i]) - /\ log' = [log EXCEPT ![j] = - IF Len(log[j]) >= nextIndex[i][j] - THEN [log[j] EXCEPT ![nextIndex[i][j]] = log[i][nextIndex[i][j]]] - ELSE Append(log[j], log[i][nextIndex[i][j]])] + /\ HasCompatiblePrefix(j, i, nextIndex[i][j]) + /\ LET leaderEntry == log[i][nextIndex[i][j]] + idx == nextIndex[i][j] + \* If follower already has an entry at idx with a different term, truncate. + conflict == idx <= Len(log[j]) /\ log[j][idx][1] /= leaderEntry[1] + newLog == IF conflict + THEN IF idx = 1 + THEN << >> + ELSE SubSeq(log[j], 1, idx - 1) + ELSE IF Len(log[j]) >= idx + THEN [log[j] EXCEPT ![idx] = leaderEntry] + ELSE Append(log[j], leaderEntry) + newCommit == IF conflict THEN Min(commitIndex[j], idx - 1) ELSE commitIndex[j] + newMatch == IF conflict THEN idx - 1 ELSE nextIndex[i][j] + IN /\ log' = [log EXCEPT ![j] = newLog] + /\ commitIndex' = [commitIndex EXCEPT ![j] = newCommit] + /\ matchIndex' = [matchIndex EXCEPT ![i][j] = newMatch] /\ nextIndex' = [nextIndex EXCEPT ![i][j] = @ + 1] - /\ matchIndex' = [matchIndex EXCEPT ![i][j] = nextIndex[i][j]] - /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Follower j rejects an AppendEntries from leader i because of prevLog mismatch. +RejectAppendEntries(i, j) == + /\ i /= j + /\ state[i] = "Leader" + /\ nextIndex[i][j] > 1 + /\ ~HasCompatiblePrefix(j, i, nextIndex[i][j]) + /\ nextIndex' = [nextIndex EXCEPT ![i][j] = @ - 1] + /\ UNCHANGED <> \* Leader i updates commitIndex when a majority has replicated an entry. Commit(i) == @@ -144,6 +183,7 @@ Next == \/ \E i \in Nodes : BecomeLeader(i) \/ \E i \in Nodes : AppendEntry(i) \/ \E i, j \in Nodes : Replicate(i, j) + \/ \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) @@ -171,6 +211,14 @@ StateMachineSafety == CommittedIndexValid == \A i \in Nodes : commitIndex[i] <= Len(log[i]) +\* Log Matching property: if two logs contain an entry with the same index and term, +\* then the logs are identical in all preceding entries. +LogMatching == + \A i, j \in Nodes : + \A idx \in 1..Min(Len(log[i]), Len(log[j])) : + log[i][idx] = log[j][idx] => + \A k \in 1..idx : log[i][k] = log[j][k] + \* Type invariant TypeOk == /\ state \in [Nodes -> {"Follower", "Candidate", "Leader"}] diff --git a/formal-verification/run_all.sh b/formal-verification/run_all.sh index c82bdca..87fef6d 100755 --- a/formal-verification/run_all.sh +++ b/formal-verification/run_all.sh @@ -17,12 +17,12 @@ run_tlc() { echo "==============================================" echo " TLC: $spec (cfg: $cfg)" echo "==============================================" - java -cp "$JAR" tlc2.TLC -config "$cfg" "$spec" 2>&1 | tail -5 + java -XX:+UseParallelGC -cp "$JAR" tlc2.TLC -workers auto -config "$cfg" "$spec" 2>&1 | tail -5 echo "" } echo "==============================================" -echo " BaraDB Formal Verification Suite v1.0.0" +echo " BaraDB Formal Verification Suite v1.1.0" echo " Running TLC model checker on all specs" echo "==============================================" echo ""