Commit 6aaabb5 added std/locks usage in vector/engine.nim (HNSW thread-safety).
std/locks requires --threads:on. Local builds worked because /etc/nim/nim.cfg
had threads:on, but GitHub Actions runners (setup-nim-action) compile without
threads by default, causing the test job to fail silently at runtime.
Also updated baradadb.nimble tasks for consistency.
Fixes GitHub Actions CI failure on test / clients-ci workflows.
- backup.tla: models backup/restore/verify/cleanup with properties:
BackupSnapshotsValid, RestoreIntegrity, VerifyIntegrity,
RetentionInvariant, HistoryConsistency, BackupIdValid
- recovery.tla: models WAL replay REDO/UNDO with properties:
RedoCommitted, RecoveryCompleteness, WalIntegrity
- Added models/backup.cfg and models/recovery.cfg with bounded constants
- Updated run_all.sh to include both new specs
- All 9 TLA+ specs pass TLC model checking
Поправени проблеми:
- LSM-Tree: WAL write вече е извън db.lock (отделен walLock) → по-добра concurrency
- MVCC: добавен compactVersions() който се изпълнява на всеки 100 commits
Премахва стари overwritten версии, които не са видими за active транзакции
- DistTxn: commit() вече НЕ rollback-ва commit-нали participants
Ако някой participant е commit-нал, транзакцията се маркира като committed
- Raft: добавен disk persistence за currentTerm, votedFor, log
saveState() при всяка промяна; loadState() при стартиране
292 теста, 0 failure-а.
Поправени проблеми:
- Deadlock detector: cycle reconstruction вече проверява пълен цикъл
- Graph cypher: executeCypher acquire-ва lock при четене
- Graph engine: loadFromFile acquire-ва lock при зареждане
- Graph engine: lock поле е exported за външен достъп
- Query: parseRowData поддържа escape-ване на , и = в стойности
- Query: execUpdateRow escape-ва стойности при сериализация
- Lexer: readNumber спира при втора точка (1.2.3 вече не е валиден float)
- Lexer: skipBlockComment хвърля ValueError при незатворен коментар
292 теста, 0 failure-а.
Поправени проблеми:
- Rate limiter: globalRate вече се enforce-ва; cleanupStaleClients() за memory leak
- Graph engine: addEdge проверява дали src/dst nodes съществуват
- Vector engine: distance() хвърля ValueError при dimension mismatch
- Query: aggregate + * на empty result вече не crash-ва
- Query: exprToSql funcCall вече работи с 0 аргумента
- Query: INSERT trigger вече не crash-ва при празни VALUES
- Server: recvWithTimeout() за всички network reads
- Server: защита от negative activeConnections
292 теста, 0 failure-а.
Поправени проблеми:
- MVCC: aborted транзакции вече не стават видими (добавено abortedTxns множество)
- LSM-Tree: поправена загуба на данни при immutable memtable overwrite
- LSM-Tree: поправена SSTable search order (сортиране по id вместо minKey)
- WAL: sync()/close() вече извикват posix.fsync()
- Auth: simpleHash (djb2) заменен с HMAC-SHA256
- Recovery: summary() вече не мутира базата данни
- Raft: поправена majority calculation за четен брой нодове
- Query: EXISTS subqueries вече изпълняват подзаявката
- Nimble: поправен build (-d:ssl) и bench task
Добавен BUG_AUDIT.md с пълен доклад и план за подобрения.
292 теста, 0 failure-а.
Add tests/tla_faithfulness.nim verifying Nim code against TLA+ invariants:
- Raft: ElectionSafety, LogMatching, CommittedIndexValid
- MVCC: NoDirtyReads, CommittedMustStart
- 2PC: Atomicity, RecoveryConsistency
Documented gap: Nim MVCC allows multiple committed versions per key,
while TLA+ spec enforces first-committer-wins (WriteWriteConflict).
This test ensures future changes to Nim code maintain alignment with specs.
Update PLAN.md (FV-14 done), CHANGELOG.md, test_all.nim includes new suite.
- Add heartbeatReceived variable tracking last term with heartbeat
- Add Heartbeat action: leader sends keep-alive; recipient steps down on higher term
- Add HeartbeatTimeout: follower starts election if no heartbeat in current term
- Add LeaderLeaseExpired: leader steps down if it loses quorum connectivity
- Add LeaderHasSelfHeartbeat invariant: every leader must have valid heartbeat
- raft.tla now models realistic partition behavior (38M states verified)
- Update CHANGELOG -> v1.2.0, VERSION -> 1.2.0, PLAN.md, README.md
- Add Formal Verification section to README and architecture docs
- Document TLA+ specs for Raft, 2PC, MVCC, Replication
- Add new BaraQL features: JSON path (->, ->>), FTS @@, CREATE INDEX USING FTS,
RECOVER TO TIMESTAMP, UNION/INTERSECT/EXCEPT
- Add OpenTelemetry tracing example to README
- Update Quick Start to use nimble test/bench
- Update EN and BG documentation
- applyCommand callback: committed entries applied to state machine
- lastApplied incremented on commit via applyCommitted()
- RaftNetwork.run() started from main() when raftEnabled=true
- asyncCheck replaced with try/await in processMessage
- bindAddr without hardcoded 127.0.0.1
- raft config: raftEnabled/Port/Peers/NodeId + env vars
- 283 tests, 0 failures
dimgigov