dimgigov
422df08ab9
Build warnings cleanup (0 warnings): - Suppress threadpool deprecation warning (baradadb.nim) - Remove unused 'os' import (logging.nim) - Fix ImplicitDefaultValue for newNode params (ast.nim) - Add explicit cstring cast for posix.open (wal.nim) - Fix HoleEnumConv for MsgKind parsing (server.nim) TLA+ Formal Verification: - Add symmetry reduction (Permutations) to all 9 existing specs - Add SYMMETRY directive to all .cfg files - New crossmodal.tla: cross-modal consistency spec * MetadataVectorConsistency, HybridResultValid * CommittedAtomicity, AbortedAtomicity, TxnStateValid - New models/crossmodal.cfg Tests: - Add Cross-Modal TLA+ Faithfulness tests (4 tests) Docs: - Update PLAN.md and BUG_AUDIT.md with completed tasks
69 lines
1.9 KiB
Plaintext
69 lines
1.9 KiB
Plaintext
-------------------------------- MODULE deadlock --------------------------------
|
|
(*
|
|
TLA+ specification of the wait-for graph deadlock detection algorithm
|
|
as implemented in BaraDB (core/deadlock.nim).
|
|
|
|
Key properties verified:
|
|
- GraphIntegrity : edges are always between known transactions.
|
|
- NoSelfLoops : no transaction waits on itself.
|
|
*)
|
|
|
|
EXTENDS Integers, Sequences, FiniteSets, TLC
|
|
|
|
CONSTANTS TxnIds, \* set of transaction IDs
|
|
MaxEdges, \* bound number of edges for model checking
|
|
Nil \* distinguished nil value (model value)
|
|
|
|
ASSUME IsFiniteSet(TxnIds)
|
|
|
|
VARIABLES
|
|
edges \* set of <<waiter, holder>> pairs
|
|
|
|
vars == <<edges>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
|
|
Init ==
|
|
/\ edges = {}
|
|
|
|
-----------------------------------------------------------------------------
|
|
\* State transitions
|
|
|
|
AddEdge(waiter, holder) ==
|
|
/\ waiter /= holder
|
|
/\ <<waiter, holder>> \notin edges
|
|
/\ Cardinality(edges) < MaxEdges
|
|
/\ edges' = edges \cup {<<waiter, holder>>}
|
|
|
|
RemoveEdge(waiter, holder) ==
|
|
/\ <<waiter, holder>> \in edges
|
|
/\ edges' = edges \ {<<waiter, holder>>}
|
|
|
|
-----------------------------------------------------------------------------
|
|
\* Next-state relation
|
|
|
|
Next ==
|
|
\/ \E w, h \in TxnIds : AddEdge(w, h)
|
|
\/ \E w, h \in TxnIds : RemoveEdge(w, h)
|
|
|
|
-----------------------------------------------------------------------------
|
|
\* Safety properties
|
|
|
|
\* All edges reference known transactions.
|
|
GraphIntegrity ==
|
|
\A e \in edges : e[1] \in TxnIds /\ e[2] \in TxnIds
|
|
|
|
\* No self-loops.
|
|
NoSelfLoops ==
|
|
\A tx \in TxnIds : <<tx, tx>> \notin edges
|
|
|
|
\* Type invariant
|
|
TypeOk ==
|
|
/\ edges \subseteq (TxnIds \X TxnIds)
|
|
/\ Cardinality(edges) <= MaxEdges
|
|
|
|
\* Symmetry reduction for model checking.
|
|
Symmetry == Permutations({t1, t2, t3, t4, t5})
|
|
|
|
=============================================================================
|