dimgigov
ce3b078979
Covers both TLA+ specs and Nim code: - P1: Raft prevLogIndex/LogMatching, replication data transfer, sharding migration (14 tasks) - P2: backup.tla, crossmodal.tla, recovery.tla + Nim tests (14 tasks) - P3: Liveness properties, write skew, 2PC crash recovery (12 tasks) - P4: CI fixes, symmetry reduction, missing tests, inter-module integration (13 tasks) Ties verification improvements directly to code improvements.
232 lines
13 KiB
Markdown
232 lines
13 KiB
Markdown
# БарaDB — Обединен план за подобрение (верификация + софтуер)
|
||
|
||
**Версия:** 2.0
|
||
**Дата:** 2026-05-07
|
||
**Контекст:** 7 TLA+ спека (11.6M състояния), 51 Nim модула (16K реда), 262 теста
|
||
|
||
---
|
||
|
||
## Принцип
|
||
|
||
Формалната верификация е безползна ако не води до подобряване на кода. Всяка
|
||
стъпка по-долу има две страни: какво трябва да се **докаже** (TLA+) и какво
|
||
трябва да се **поправи/добави** в Nim кода. Когато TLA+ моделът открие
|
||
несъответствие с кода — това е **бъг в кода или в модела**. И двете се оправят.
|
||
|
||
---
|
||
|
||
## Приоритет 1 — Критични разминавания между модел и код
|
||
|
||
### 1.1. Raft: Replicate без prevLogIndex проверка
|
||
|
||
**Състояние:**
|
||
- Nim (`raft.nim:190-197`): `handleAppendEntries` проверява `prevLogIndex` и `prevLogTerm` — ако follower няма entry на този индекс с този term, заявката се отхвърля.
|
||
- TLA+ (`raft.tla:104-114`): `Replicate` действието НЕ проверява това. LogMatching инвариантата беше премахната защото моделът я нарушава.
|
||
|
||
**Какво да се направи:**
|
||
|
||
| # | Задача | Файл | Тип |
|
||
|---|--------|------|-----|
|
||
| 1 | Добави `prevLogIndex`/`prevLogTerm` precondition към `Replicate` | `raft.tla` | TLA+ |
|
||
| 2 | Добави `RejectAppendEntries` действие (follower отхвърля при mismatch) | `raft.tla` | TLA+ |
|
||
| 3 | Върни `LogMatching` инвариантата | `raft.tla` | TLA+ |
|
||
| 4 | Добави тест "follower rejects append with wrong prevLogTerm" | `test_all.nim` | Nim |
|
||
| 5 | Поправи `handleAppendEntries` ако тестът покаже бъг | `raft.nim` | Nim |
|
||
|
||
**Критерий за успех:** `LogMatching` минава в TLC + Nim тестът минава.
|
||
|
||
### 1.2. Replication: writeLsn не изпраща данни
|
||
|
||
**Състояние:**
|
||
- `PLAN.md` казва: "replication: writeLsn не изпраща данни към replicas"
|
||
- TLA+ (`replication.tla`): `WriteLsn` действието увеличава `currentLsn` и създава `pendingAcks`, но не моделира реален data transfer.
|
||
- Nim (`replication.nim`): `writeLsn` вероятно само increment-ва LSN без да праща data.
|
||
|
||
**Какво да се направи:**
|
||
|
||
| # | Задача | Файл | Тип |
|
||
|---|--------|------|-----|
|
||
| 6 | Добави `DataPayload` променлива в TLA+ модела (кой LSN има какви данни) | `replication.tla` | TLA+ |
|
||
| 7 | Инвариант: `DataConsistency` — ако replica ack-не LSN, данните са изпратени | `replication.tla` | TLA+ |
|
||
| 8 | Имплементирай реално data изпращане в `writeLsn` | `replication.nim` | Nim |
|
||
| 9 | Добави тест "replica receives data for acked LSN" | `test_all.nim` | Nim |
|
||
|
||
**Критерий за успех:** `DataConsistency` минава + Nim тестът потвърждава data transfer.
|
||
|
||
### 1.3. Sharding: rebalance не мигрира данни
|
||
|
||
**Състояние:**
|
||
- `PLAN.md`: "sharding: rebalance не мигрира данни"
|
||
- TLA+ (`sharding.tla`): `Rebalance` действието само променя `shardToNodes` mapping, не мигрира записи.
|
||
- Nim (`sharding.nim:126-137`): `rebalance()` само пренарежда `nodeIds` в shard-овете.
|
||
|
||
**Какво да се направи:**
|
||
|
||
| # | Задача | Файл | Тип |
|
||
|---|--------|------|-----|
|
||
| 10 | Добави `DataKeys` променлива — множество ключове на всеки shard | `sharding.tla` | TLA+ |
|
||
| 11 | `Rebalance` да мигрира ключове: `DataKeys' = migrate(DataKeys, shardToNodes')` | `sharding.tla` | TLA+ |
|
||
| 12 | Инвариант: `NoDataLoss` — след rebalance, всички ключове са достъпни | `sharding.tla` | TLA+ |
|
||
| 13 | Имплементирай `migrateData()` в Nim — read от стар shard, write в нов | `sharding.nim` | Nim |
|
||
| 14 | Тест "rebalance preserves all data" | `test_all.nim` | Nim |
|
||
|
||
---
|
||
|
||
## Приоритет 2 — Непокрити критични модули
|
||
|
||
### 2.1. Backup/Restore
|
||
|
||
**Състояние:** `backup.nim` (498 реда) няма тестове нито в TLA+, нито в Nim.
|
||
Това е **единственият** голям модул без никакво покритие.
|
||
|
||
| # | Задача | Файл | Тип |
|
||
|---|--------|------|-----|
|
||
| 15 | TLA+ спек `backup.tla` — модел на backup/restore/cleanup цикъл | `backup.tla` | TLA+ |
|
||
| 16 | Инвариант: `RestoreAtomicity` — restore или succeed-ва напълно, или rollback-ва | `backup.tla` | TLA+ |
|
||
| 17 | Инвариант: `CleanupPreservesNewest` — cleanup никога не трие последния backup | `backup.tla` | TLA+ |
|
||
| 18 | Nim тест suite: backup create, verify, restore, cleanup, history | `test_all.nim` | Nim |
|
||
| 19 | Nim тест: backup + restore round-trip с проверка на съдържанието | `test_all.nim` | Nim |
|
||
|
||
**Критерий за успех:** TLC минава + 5+ Nim теста за backup.
|
||
|
||
### 2.2. Cross-Modal Consistency
|
||
|
||
**Състояние:** `crossmodal.nim` (250 реда) има тест в `test_all.nim`, но TLA+
|
||
моделът не проверява consistency между storage engines.
|
||
|
||
| # | Задача | Файл | Тип |
|
||
|---|--------|------|-----|
|
||
| 20 | TLA+ спек `crossmodal.tla` — обект индексиран в 4-те engine-а | `crossmodal.tla` | TLA+ |
|
||
| 21 | Инвариант: `IndexConsistency` — ако обект е в 3 индекса, е и в 4-тия | `crossmodal.tla` | TLA+ |
|
||
| 22 | Инвариант: `HybridScoreMonotonic` — повече индекси → по-добър score | `crossmodal.tla` | TLA+ |
|
||
| 23 | Nim тест: insert във всички engines → hybrid search намира обекта | `test_all.nim` | Nim |
|
||
|
||
### 2.3. WAL Recovery
|
||
|
||
**Състояние:** `recovery.nim` (177 реда) има REDO/UNDO логика. TLA+ не я
|
||
моделира. Ако recovery е грешно — **загуба на данни при crash**.
|
||
|
||
| # | Задача | Файл | Тип |
|
||
|---|--------|------|-----|
|
||
| 24 | TLA+ спек `recovery.tla` — модел на WAL replay с committed/uncommitted | `recovery.tla` | TLA+ |
|
||
| 25 | Инвариант: `CommittedSurvives` — committed записи оцеляват след crash+recovery | `recovery.tla` | TLA+ |
|
||
| 26 | Инвариант: `UncommittedRolledBack` — uncommitted записи се undo-ват | `recovery.tla` | TLA+ |
|
||
| 27 | Nim тест: write → crash (без flush) → reopen → verify recovery | `test_all.nim` | Nim |
|
||
| 28 | Nim тест: write+commit → crash → reopen → committed данни са налице | `test_all.nim` | Nim |
|
||
|
||
---
|
||
|
||
## Приоритет 3 — Liveness и по-силни свойства
|
||
|
||
### 3.1. Liveness свойства (TLA+)
|
||
|
||
Без liveness, TLA+ проверява safety (лоши неща не се случват) но не
|
||
прогрес (добри неща се случват).
|
||
|
||
| # | Спек | Liveness свойство | Защо |
|
||
|---|------|------------------|------|
|
||
| 29 | raft.tla | `LeaderElectedEventually` | Клъстерът в крайна сметка има лидер |
|
||
| 30 | twopc.tla | `Termination` | Всички транзакции в крайна сметка commit или abort |
|
||
| 31 | gossip.tla | `DeadDetectedEventually` | Мъртъв възел в крайна сметка е открит |
|
||
| 32 | replication.tla | `LsnProgresses` | appliedLsn в крайна сметка расте |
|
||
|
||
**Изисква:** `FAIRNESS WF_vars(Next)` в `.cfg` файловете.
|
||
**Внимание:** TLC liveness проверката е 2-5x по-бавна от safety.
|
||
|
||
### 3.2. MVCC Write Skew Detection
|
||
|
||
**Състояние:** Snapshot isolation допуска write skew — класически проблем.
|
||
Нито TLA+ моделът, нито Nim кодът го проверяват.
|
||
|
||
| # | Задача | Файл | Тип |
|
||
|---|--------|------|-----|
|
||
| 33 | Добави `readPredicate[t]` в `mvcc.tla` | `mvcc.tla` | TLA+ |
|
||
| 34 | Инвариант: `NoWriteSkew` — два committed txn не могат да имат overlapping predicates | `mvcc.tla` | TLA+ |
|
||
| 35 | Имплементирай predicate tracking в `mvcc.nim` | `mvcc.nim` | Nim |
|
||
| 36 | Тест "write skew is detected/prevented" | `test_all.nim` | Nim |
|
||
|
||
### 3.3. 2PC Coordinator Crash/Recovery
|
||
|
||
**Състояние:** `disttxn.nim` има 2PC но без coordinator failure handling.
|
||
|
||
| # | Задача | Файл | Тип |
|
||
|---|--------|------|-----|
|
||
| 37 | Добави `CrashCoordinator(t)` и `RecoverCoordinator(t)` в `twopc.tla` | `twopc.tla` | TLA+ |
|
||
| 38 | Инвариант: `RecoveryConsistency` — решението е същото след recovery | `twopc.tla` | TLA+ |
|
||
| 39 | Добави coordinator WAL в `disttxn.nim` — записва решението преди изпращане | `disttxn.nim` | Nim |
|
||
| 40 | Тест "coordinator recovery after crash" | `test_all.nim` | Nim |
|
||
|
||
---
|
||
|
||
## Приоритет 4 — Инфраструктурни подобрения
|
||
|
||
### 4.1. CI поправка
|
||
|
||
**Проблем:** `verify` job в CI използва `container:` което не работи с `actions/checkout`.
|
||
|
||
| # | Задача | Файл |
|
||
|---|--------|------|
|
||
| 41 | Замени `container: eclipse-temurin:21-jre` с `setup-java` action | `.github/workflows/ci.yml` |
|
||
| 42 | Добави `continue-on-error: true` за TLC стъпката | `.github/workflows/ci.yml` |
|
||
| 43 | Кеширай `tla2tools.jar` с `actions/cache` | `.github/workflows/ci.yml` |
|
||
|
||
### 4.2. Symmetry Reduction
|
||
|
||
**Проблем:** TLC проверява симетрични пермутации отделно. С 3 нода има 3!=6
|
||
еквивалентни състояния за всяко реално състояние.
|
||
|
||
| # | Задача | Файл |
|
||
|---|--------|------|
|
||
| 44 | Добави `Symmetry` sets в raft.cfg, gossip.cfg, replication.cfg | `models/*.cfg` |
|
||
| 45 | Увеличи границите: raft 5 nodes, gossip 5 nodes | `models/*.cfg` |
|
||
|
||
### 4.3. Липсващи Nim тестове
|
||
|
||
**Проблем:** 4 модула нямат dedicated тест suite.
|
||
|
||
| # | Модул | Тестове за добавяне |
|
||
|---|-------|-------------------|
|
||
| 46 | `core/logging` | JSON формат, нива, файл output |
|
||
| 47 | `core/websocket` | Frame parsing, SUBSCRIBE/UNSUBSCRIBE |
|
||
| 48 | `core/config` | Env vars, JSON файл, defaults, validation |
|
||
| 49 | `core/backup` | Вж. 2.1 по-горе |
|
||
|
||
### 4.4. Inter-module интеграция
|
||
|
||
**Проблем:** `PLAN.md` казва "няма raft→disttxn, gossip→sharding, replication→disttxn връзки".
|
||
|
||
| # | Връзка | Какво липсва | Тип |
|
||
|---|--------|-------------|-----|
|
||
| 50 | Raft → DistTxn | 2PC решенията трябва да се replic-ват през Raft | Nim |
|
||
| 51 | Gossip → Sharding | При node failure, gossip нотифицира sharding за rebalance | Nim |
|
||
| 52 | Replication → DistTxn | Distributed txn commit изисква replication ack | Nim |
|
||
| 53 | TLA+ модел на интеграцията | Raft + 2PC + Replication в един спек | TLA+ (дългосрочно) |
|
||
|
||
---
|
||
|
||
## Хронограма
|
||
|
||
| Седмица | Задачи | Резултат |
|
||
|---------|--------|---------|
|
||
| **1** | #1-5 (Raft prevLogIndex + LogMatching) | Raft модел по-точен от кода, 1 нов тест |
|
||
| **2** | #6-14 (Replication data + Sharding migration) | 2 distributed gap-а затворени, 3 нови теста |
|
||
| **3** | #15-28 (Backup, CrossModal, Recovery спекове + тестове) | 3 нови TLA+ спека, 8+ нови теста |
|
||
| **4** | #29-32 (Liveness) | 4 темпорални свойства добавени |
|
||
| **5** | #33-40 (Write skew, 2PC crash) | 2 критични safety gap-а затворени |
|
||
| **6** | #41-53 (CI, Symmetry, тестове, интеграция) | Инфраструктурата стабилна |
|
||
|
||
---
|
||
|
||
## Метрики за успех
|
||
|
||
| Метрика | Сега | След плана |
|
||
|---------|------|-----------|
|
||
| TLA+ спекове | 7 | 10 (+backup, crossmodal, recovery) |
|
||
| TLA+ инварианти | 26 | 42 |
|
||
| TLA+ темпорални свойства | 1 | 5 |
|
||
| Проверени състояния | 11.6M | 50M+ (със symmetry) |
|
||
| Nim тестове | 262 | 285+ |
|
||
| Покрити модули (test) | 47/51 | 51/51 |
|
||
| Distributed gaps (PLAN.md) | 4 | 0 |
|
||
| Inter-module връзки | 0 | 3 |
|