dimgigov
215df1cdf3
- 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
1.6 KiB
1.6 KiB
Transactions & MVCC
MVCC (Multi-Version Concurrency Control) with snapshot isolation and deadlock detection.
Usage
import barabadb/core/mvcc
var tm = newTxnManager()
let txn = tm.beginTxn()
# Write operations
discard tm.write(txn, "key1", cast[seq[byte]]("value1"))
discard tm.write(txn, "key2", cast[seq[byte]]("value2"))
# Savepoint
tm.savepoint(txn)
discard tm.write(txn, "key3", cast[seq[byte]]("value3"))
discard tm.rollbackToSavepoint(txn) # undo key3
# Commit
discard tm.commit(txn)
Transaction Isolation
BaraDB uses snapshot isolation:
- Readers don't block writers
- Writers don't block readers
- Each transaction sees a consistent snapshot
Deadlock Detection
import barabadb/core/deadlock
var detector = newDeadlockDetector()
if detector.detectCycle(txn1, txn2):
echo "Deadlock detected!"
Write-Ahead Log
import barabadb/storage/wal
var wal = newWAL("./wal")
wal.append(txnId, "SET key value")
wal.flush()
Savepoints
Nested transaction savepoints:
tm.savepoint(txn, "sp1")
# ... operations ...
tm.rollbackToSavepoint(txn, "sp1")
Formal Verification
The MVCC / Snapshot Isolation protocol is formally specified in TLA+:
- Spec:
formal-verification/mvcc.tla - Verified properties:
NoDirtyReads— transactions never read uncommitted dataReadOwnWrites— transactions always see their own writesWriteWriteConflict— first-committer-wins (no two committed transactions write the same key)
Run TLC locally:
cd formal-verification
java -cp tla2tools.jar tlc2.TLC -config models/mvcc.cfg mvcc.tla