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.3 KiB
1.3 KiB
Транзакции & MVCC
Multi-Version Concurrency Control със snapshot изолация.
Употреба
import barabadb/core/mvcc
var tm = newTxnManager()
let txn = tm.beginTxn()
discard tm.write(txn, "key1", cast[seq[byte]]("value1"))
discard tm.write(txn, "key2", cast[seq[byte]]("value2"))
tm.savepoint(txn)
discard tm.rollbackToSavepoint(txn)
discard tm.commit(txn)
Изолация
BaraDB използва snapshot isolation:
- Читателите не блокират писатели
- Писателите не блокират читатели
- Всяка транзакция вижда консистентен моментна снимка
Формална Верификация
MVCC / Snapshot Isolation протоколът е формално специфициран в TLA+:
- Спецификация:
formal-verification/mvcc.tla - Проверени свойства:
NoDirtyReads— транзакциите никога не четат неcommit-нати данниReadOwnWrites— транзакциите винаги виждат собствените си записиWriteWriteConflict— first-committer-wins
Пускане на TLC:
cd formal-verification
java -cp tla2tools.jar tlc2.TLC -config models/mvcc.cfg mvcc.tla