baraba/Baradb
1
1
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
398769ff97832a02a5ec4144120339cb8419b610
Baradb/formal-verification/IMPROVEMENT_PLAN.md
T
dimgigov e715454c4e 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.
2026-05-07 18:31:20 +03:00

13 KiB
Raw Blame History

План за подобрения на формалната верификация на 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 View Git Blame Copy Permalink