docs(verify): add detailed improvement plan with 13 tasks across 4 priorities
Covers Raft prevLogIndex fix, 2PC recovery, MVCC write skew, liveness properties, backup.tla, crossmodal.tla, CI fixes, symmetry reduction, and Apalache migration.
This commit is contained in:
@@ -0,0 +1,200 @@
|
||||
# План за подобрения на формалната верификация на BaraDB
|
||||
|
||||
**Към:** `formal-verification/IMPROVEMENT_PLAN.md`
|
||||
**Дата:** 2026-05-07
|
||||
**Автор:** Kilo (formal-verification v1.0.0)
|
||||
**Статус:** За изпълнение
|
||||
|
||||
---
|
||||
|
||||
## Общ преглед на слабите места
|
||||
|
||||
Текущата верификация (7 TLA+ спека, 26 инварианти, 11.6M проверени състояния) покрива 4 от 15-те Nim модула в `core/`. Анализът идентифицира **8 категории слаби места**, всяко с конкретни последствия за коректността на системата.
|
||||
|
||||
---
|
||||
|
||||
## Приоритет 1 — Критични (влияят на вече проверените спекове)
|
||||
|
||||
### 1.1. Raft: липсва prevLogIndex/prevLogTerm проверка в Replicate
|
||||
|
||||
**Проблем:** Имплементацията (`raft.nim:190-197`) извършва prevLogIndex/prevLogTerm проверка при `handleAppendEntries`. TLA+ моделът (`raft.tla:104-114`) НЕ проверява дали follower има съвместим префикс преди репликация. Резултатът: `LogMatching` инвариантата е неизпълнима и беше премахната.
|
||||
|
||||
**Въздействие:** Моделът разрешава състояния, които реалната имплементация не би — follower може да получи entry с непоследователен prefix, което води до невалидни log състояния.
|
||||
|
||||
**Стъпки:**
|
||||
1. Добавяне на `prevLogIndex` и `prevLogTerm` към `Replicate` действието в `raft.tla`
|
||||
2. Precondition: `nextIndex[i][j] > 1 => log[j][nextIndex[i][j]-1][1] = log[i][nextIndex[i][j]-1][1]`
|
||||
3. Ако precondition не е изпълнен: follower отхвърля, leader декрементира `nextIndex[j]`
|
||||
4. Възстановяване на `LogMatching` инвариантата
|
||||
5. Добавяне на `TruncateConflict` действие (follower трие конфликтни entries)
|
||||
|
||||
**Очакван резултат:** `LogMatching` минава, моделът по-точно отразява raft.nim
|
||||
|
||||
### 1.2. Raft: липсва leader step-down при partition
|
||||
|
||||
**Проблем:** `StepDown` действието изисква изричен `newTerm > currentTerm`. Няма механизъм за leader lease или heartbeat fail detection. Реалният raft (`raft.nim:327-329`) използва `electionTimeout` за detect на мъртъв leader.
|
||||
|
||||
**Въздействие:** Моделът не проверява, че leader се отказва при partition.
|
||||
|
||||
**Стъпки:**
|
||||
1. Добавяне на `HeartbeatTimeout(i)` действие: follower/candidate който не е получил heartbeat в рамките на election timeout започва нова електората
|
||||
2. Добавяне на `LeaderLeaseExpired(i)` действие: leader чийто lease е изтекъл става follower
|
||||
3. Инвариант: `LeaderLeaseSafety` — два лидери нямат overlapping lease
|
||||
|
||||
### 1.3. 2PC: липсва coordinator failure/recovery
|
||||
|
||||
**Проблем:** Имплементацията (`crossmodal.nim:222-245`) има `prepare/commit/rollback` но не моделира coordinator crash. TLA+ спекът (`twopc.tla`) няма `CrashCoordinator` или `RecoverCoordinator` действие.
|
||||
|
||||
**Въздействие:** Ако coordinator крашне след `DecideCommit`, participant-ите остават в `Prepared` без да разберат решението.
|
||||
|
||||
**Стъпки:**
|
||||
1. Добавяне на `coordinatorLog` променлива — персистентен лог на решението
|
||||
2. `CrashCoordinator(t)` — coordinator спира, `coordinatorDecided[t]` остава но coordinator не отговаря
|
||||
3. `RecoverCoordinator(t)` — coordinator чете `coordinatorLog[t]` и възстановява `decidedAction[t]`
|
||||
4. `ParticipantTimeout(t, p)` — participant който не е получил решение в рамките на timeout решава ABORT
|
||||
5. Инвариант: `RecoveryConsistency` — след recovery, coordinator решението е същото като преди crash
|
||||
|
||||
---
|
||||
|
||||
## Приоритет 2 — Важни (нови свойства на съществуващи спекове)
|
||||
|
||||
### 2.1. Liveness свойства (темпорални)
|
||||
|
||||
**Проблем:** Само `replication.tla` има темпорално свойство (`MonotonicLsn`). Без liveness, моделите потвърждават safety (лоши неща не се случват) но не liveness (добри неща се случват).
|
||||
|
||||
| Спек | Liveness свойство | Формула |
|
||||
|------|------------------|---------|
|
||||
| raft | LeaderElectedEventually | `<>(\E i \in Nodes : state[i] = "Leader")` |
|
||||
| twopc | Termination | `<>[](\A t : txnState[t] \in {"Committed", "Aborted"})` |
|
||||
| mvcc | CommitProgress | `<>(\A t : txnState[t] /= "Active" \/ txnStartTs[t] > 0)` |
|
||||
| gossip | DeadDetected | `[]<>(\A n : state[n] = "Dead" => knownState[n][n] = "Dead")` |
|
||||
|
||||
**Стъпки:**
|
||||
1. Добавяне на `FAIRNESS` условия в `models/*.cfg` (weak fairness: `WF_vars(Next)`)
|
||||
2. Добавяне на `PROPERTIES` секции към .cfg файловете
|
||||
3. Проверка че liveness минава с fairness (TLC ще провери че всички fair behaviors задоволяват liveness)
|
||||
|
||||
**Забележка:** TLC проверката на liveness е по-бавна (изисква strongly-connected component analysis). Очаквано 2-5x забавяне.
|
||||
|
||||
### 2.2. MVCC: Write Skew Detection
|
||||
|
||||
**Проблем:** Snapshot isolation допуска write skew — два конкурентни транзакции четат различни ключове и записват на обратните. Имплементацията (`mvcc.nim`) не проверява за predicate-based конфликти.
|
||||
|
||||
**Пример:** T1 чете k1=0, T2 чете k2=0. T1 записва k2=1 (като k1=0). T2 записва k1=1 (като k2=0). И двете комитват — резултатът е нелегален.
|
||||
|
||||
**Стъпки:**
|
||||
1. Добавяне на `readPredicate[t]` — множество ключове които t е прочел и използвал за решение
|
||||
2. `WriteSkewCheck` в `CommitTxn(t)` — проверка че няма друг committed txn с overlapping predicate
|
||||
3. Инвариант: `NoWriteSkew` — няма committed txn двойки с overlapping read predicates и disjoint write sets
|
||||
|
||||
### 2.3. Replication: SyncDurability поправка
|
||||
|
||||
**Проблем:** `SyncDurability` инвариантата беше премахната защото TLC я намираше за violated при `appliedLsn=0`. Причината: TLC обхожда IF/THEN/ELSE по различен начин от стандартната TLA+ семантика.
|
||||
|
||||
**Стъпки:**
|
||||
1. Пренаписване на SyncDurability като чист implication: `~(mode = "Sync" /\ appliedLsn > 0) \/ (\A l \in 1..appliedLsn : pendingAcks[l] = {})`
|
||||
2. Добавяне на `SyncCommitSafety` — в sync mode, commitIndex се движи само когато всички replica ack-ове са получени
|
||||
|
||||
---
|
||||
|
||||
## Приоритет 3 — Нови спекове
|
||||
|
||||
### 3.1. backup.tla — Backup/Restore протокол
|
||||
|
||||
**Покрива:** `src/barabadb/core/backup.nim` (498 реда)
|
||||
|
||||
**Ключови свойства:**
|
||||
- `BackupIntegrity` — ако backup е създаден успешно, archive съдържа всички файлове от dataDir
|
||||
- `RestoreAtomicity` — restore или напълно заменя dataDir, или rollback-ва до предишно състояние
|
||||
- `CleanupPreservesNewest` — cleanup никога не трие най-новия backup
|
||||
- `NoDataLoss` — след backup + restore, данните са идентични на оригинала
|
||||
|
||||
**Стъпки:**
|
||||
1. Моделиране на `DataDir` като множество файлове
|
||||
2. `CreateBackup`, `RestoreBackup`, `CleanupOld` действия
|
||||
3. `VerifyArchive` действие — проверка на checksum
|
||||
4. 4 инварианти + 1 liveness (restore в крайна сметка завършва)
|
||||
|
||||
### 3.2. crossmodal.tla — Cross-Modal Consistency
|
||||
|
||||
**Покрива:** `src/barabadb/core/crossmodal.nim` (250 реда)
|
||||
|
||||
**Ключови свойства:**
|
||||
- `CrossModalConsistency` — обект който е в document store е достъпен и чрез vector/graph/FTS
|
||||
- `HybridScoreMonotonic` — хибридният резултат не намалява при добавяне на повече индекси
|
||||
- `TPCAtomicity` — cross-modal 2PC транзакцията е атомарна (вече покрито от twopc.tla, но тук е с concrete participants)
|
||||
|
||||
**Стъпки:**
|
||||
1. Моделиране на `IndexedObject` — обект с id, който може да бъде в document/vector/graph/FTS индекс
|
||||
2. `InsertDocument`, `InsertVector`, `InsertGraph`, `IndexText` действия
|
||||
3. `CrossModalInsert` — атомарно инсъртване във всички индекси
|
||||
4. Инвариант: ако обект е в 3 индекса, той е и в 4-тия
|
||||
|
||||
### 3.3. raft.tla — Membership Changes (Phase 2)
|
||||
|
||||
**Покрива:** raft cluster config промени (не е директно в raft.nim, но е критично за production)
|
||||
|
||||
**Стъпки:**
|
||||
1. Добавяне на `Config` променлива — множество от активни възли
|
||||
2. `AddNode(i)`, `RemoveNode(i)` действия — joint consensus
|
||||
3. `ConfigCommitted` — новата конфигурация е committed
|
||||
4. Инвариант: `JointConsensusSafety` — по време на преход няма два лидера в различни конфигурации
|
||||
|
||||
---
|
||||
|
||||
## Приоритет 4 — Инфраструктурни подобрения
|
||||
|
||||
### 4.1. CI поправка
|
||||
|
||||
**Проблем:** Текущият `verify` job в `.github/workflows/ci.yml` използва `container: eclipse-temurin:21-jre` което не споделя работната директория.
|
||||
|
||||
**Стъпки:**
|
||||
1. Премахване на `container:` блока
|
||||
2. Добавяне на `setup-java` action: `uses: actions/setup-java@v4` с `distribution: temurin` и `java-version: 21`
|
||||
3. Добавяне на `continue-on-error: true` за TLC стъпката (да не блокира PR-и при timeout)
|
||||
4. Кеширане на `tla2tools.jar` с `actions/cache`
|
||||
|
||||
### 4.2. Симетрични редукции
|
||||
|
||||
**Проблем:** TLC проверява състояния които са симетрични пермутации (напр. {n1=Leader, n2=Follower, n3=Follower} е еквивалентно на {n2=Leader, n1=Follower, n3=Follower}).
|
||||
|
||||
**Стъпки:**
|
||||
1. Добавяне на `Symmetry` в конфигурациите: `SYMMETRY SymmetrySet`
|
||||
2. Дефиниране на `SymmetrySet` като пермутации на Nodes/Replicas/TxnIds
|
||||
3. Очаквано 3-10x намаляване на състоянията → по-големи граници
|
||||
|
||||
### 4.3. Apalache migration (дългосрочно)
|
||||
|
||||
**Проблем:** TLC е explicit-state model checker — обхожда всяко състояние поотделно. Apalache е symbolic — използва SMT solver и може да проверява по-големи пространства.
|
||||
|
||||
**Стъпки:**
|
||||
1. Инсталиране на Apalache (`apalache-mc`)
|
||||
2. Конвертиране на 1-2 спека (започвайки с `twopc.tla` — най-простия)
|
||||
3. Сравнение на резултати: TLC vs Apalache
|
||||
4. Ако Apalache е по-бързо — миграция на всички спекове
|
||||
|
||||
---
|
||||
|
||||
## Хронограма
|
||||
|
||||
| Седмица | Задачи | Очакван резултат |
|
||||
|---------|--------|-----------------|
|
||||
| 1 | 1.1 Raft prevLogIndex + LogMatching, 4.1 CI | Raft спек по-точен, CI работи |
|
||||
| 2 | 1.3 2PC recovery, 2.3 SyncDurability | 2PC по-реалистичен, replication по-силен |
|
||||
| 3 | 2.1 Liveness свойства (raft, twopc, gossip) | 4 liveness свойства добавени |
|
||||
| 4 | 3.1 backup.tla | Нов спек за backup/restore |
|
||||
| 5-6 | 2.2 MVCC write skew, 3.2 crossmodal.tla | 2 нови спека, по-силни инварианти |
|
||||
| 7-8 | 4.2 Symmetry reduction, 4.3 Apalache | 5x повече проверени състояния |
|
||||
|
||||
---
|
||||
|
||||
## Метрики за успех
|
||||
|
||||
| Метрика | Текущо | След Фаза 1 | След Фаза 2 |
|
||||
|---------|--------|-------------|-------------|
|
||||
| Спекове | 7 | 8 | 10 |
|
||||
| Инварианти | 26 | 34 | 45 |
|
||||
| Темпорални свойства | 1 | 4 | 6 |
|
||||
| Покрити Nim модули | 4/15 | 5/15 | 7/15 |
|
||||
| Проверени състояния (общо) | 11.6M | 25M | 100M |
|
||||
| CI време | ~120s | ~180s | ~300s |
|
||||
Reference in New Issue
Block a user