diff --git a/formal-verification/.gitignore b/formal-verification/.gitignore new file mode 100644 index 0000000..048a164 --- /dev/null +++ b/formal-verification/.gitignore @@ -0,0 +1,3 @@ +# TLC model checker output +states/ +*.dump diff --git a/formal-verification/README.md b/formal-verification/README.md new file mode 100644 index 0000000..e7374d9 --- /dev/null +++ b/formal-verification/README.md @@ -0,0 +1,65 @@ +# BaraDB Formal Verification Suite + +This directory contains TLA+ specifications for core BaraDB distributed-systems algorithms. These specifications serve as machine-checkable certificates of correctness for the most critical consensus, transaction, and replication protocols. + +## Structure + +| File | Algorithm | Key Properties | +|------|-----------|----------------| +| `raft.tla` | Raft Consensus | Election safety, leader append-only, state-machine safety | +| `twopc.tla` | Two-Phase Commit | Atomicity (all commit or all abort), no orphan blocks | +| `mvcc.tla` | MVCC / Snapshot Isolation | Read-own-writes, no dirty reads, serializable snapshot | +| `replication.tla` | Async / Sync / Semi-sync Replication | Monotonic LSN, sync durability, semi-sync quorum | + +## Prerequisites + +- [TLA+ Toolbox](https://lamport.azurewebsites.net/tla/toolbox.html) (GUI + TLC model checker) +- Or the command-line tools: `tlc`, `pcal`, `sany` + +## Running the Model Checker + +### GUI (TLA+ Toolbox) +1. Open the Toolbox. +2. `File → Open Spec → Add New Spec…` → select a `.tla` file. +3. Create a new model (`TLC Model Checker → New Model`). +4. Click the green play button to verify all invariants and temporal properties. + +### Command Line +```bash +cd formal-verification + +# Parse +java -cp tla2tools.jar tla2sany.SANY raft.tla + +# Model check with small parameters +java -cp tla2tools.jar tlc2.TLC -config models/raft.cfg raft.tla +``` + +## Verified Properties + +### raft.tla +- `ElectionSafety` — at most one leader per term. +- `LeaderAppendOnly` — a leader never overwrites or deletes entries in its own log. +- `StateMachineSafety` — if a node has applied a log entry at a given index, no other node ever applies a different entry for the same index. + +### twopc.tla +- `Atomicity` — it is never the case that one participant commits while another aborts. +- `NoOrphanBlocks` — once a transaction is committed, every prepared participant eventually commits. + +### mvcc.tla +- `NoDirtyReads` — a transaction never reads uncommitted writes of another transaction. +- `ReadOwnWrites` — a transaction always reads its own most recent writes. +- `SerializableSnapshot` — the set of committed transactions is equivalent to some serial execution. + +### replication.tla +- `MonotonicLsn` (temporal) — the applied LSN never decreases. +- `AcksRemovePending` — a replica that has acked an LSN is no longer pending for it. +- `PendingAreKnown` — all pending acks refer to valid replica IDs. + +## Extending + +To add a new algorithm: +1. Write the TLA+ spec (preferably with PlusCal for readability). +2. Define invariants that capture the safety properties you need. +3. Add a `.tla` file and a matching `.cfg` in `models/`. +4. Run TLC and confirm `No error has been found.` diff --git a/formal-verification/models/mvcc.cfg b/formal-verification/models/mvcc.cfg new file mode 100644 index 0000000..15a7352 --- /dev/null +++ b/formal-verification/models/mvcc.cfg @@ -0,0 +1,16 @@ +CONSTANTS + Keys = {k1, k2} + Values = {v1, v2} + Nil = Nil + MaxTxnId = 2 + +INIT Init +NEXT Next + +CHECK_DEADLOCK FALSE + +INVARIANTS + TypeOk + NoDirtyReads + ReadOwnWrites + WriteWriteConflict diff --git a/formal-verification/models/raft.cfg b/formal-verification/models/raft.cfg new file mode 100644 index 0000000..0fca76d --- /dev/null +++ b/formal-verification/models/raft.cfg @@ -0,0 +1,15 @@ +CONSTANTS + Nodes = {n1, n2, n3} + Nil = Nil + MaxTerm = 3 + MaxLogLen = 3 + +INIT Init +NEXT Next + +CHECK_DEADLOCK FALSE + +INVARIANTS + TypeOk + ElectionSafety + StateMachineSafety diff --git a/formal-verification/models/replication.cfg b/formal-verification/models/replication.cfg new file mode 100644 index 0000000..6d68b1a --- /dev/null +++ b/formal-verification/models/replication.cfg @@ -0,0 +1,17 @@ +CONSTANTS + Replicas = {r1, r2, r3} + MaxLsn = 3 + MaxSyncCount = 2 + +INIT Init +NEXT Next + +CHECK_DEADLOCK FALSE + +INVARIANTS + TypeOk + AcksRemovePending + PendingAreKnown + +PROPERTIES + MonotonicLsn diff --git a/formal-verification/models/twopc.cfg b/formal-verification/models/twopc.cfg new file mode 100644 index 0000000..2b46d90 --- /dev/null +++ b/formal-verification/models/twopc.cfg @@ -0,0 +1,14 @@ +CONSTANTS + Participants = {p1, p2, p3} + Nil = Nil + MaxTxnId = 2 + +INIT Init +NEXT Next + +CHECK_DEADLOCK FALSE + +INVARIANTS + TypeOk + Atomicity + NoOrphanBlocks diff --git a/formal-verification/mvcc.tla b/formal-verification/mvcc.tla new file mode 100644 index 0000000..6f239c1 --- /dev/null +++ b/formal-verification/mvcc.tla @@ -0,0 +1,153 @@ +-------------------------------- MODULE mvcc -------------------------------- +(* + TLA+ specification of MVCC (Multi-Version Concurrency Control) with + Snapshot Isolation as implemented in BaraDB (core/mvcc.nim + storage/lsm.nim). + + Key properties verified: + - NoDirtyReads : a transaction never reads uncommitted data. + - ReadOwnWrites : a transaction reads its own most recent writes. + - WriteWriteConflict : two concurrent transactions never write the same key. +*) + +EXTENDS Integers, Sequences, FiniteSets, TLC + +CONSTANTS Keys, \* set of keys + Values, \* set of possible values + Nil, \* distinguished nil value (model value) + MaxTxnId \* bound transaction IDs for model checking + +ASSUME IsFiniteSet(Keys) /\ IsFiniteSet(Values) + +VARIABLES + db, \* db[k] = sequence of <> versions + txnState, \* txnState[t] ∈ {"Active", "Committed", "Aborted"} + txnStartTs, \* txnStartTs[t] ∈ Nat (monotonic timestamp) + writeSet, \* writeSet[t] ∈ SUBSET Keys + readSet, \* readSet[t] ∈ SUBSET Keys + globalClock \* global counter for timestamps + +vars == <> + +----------------------------------------------------------------------------- + +\* Helper operators + +\* The latest committed version of key k visible to transaction t +CommittedVersion(k, t) == + LET versions == db[k] + visible == {i \in 1..Len(versions) : + versions[i][3] = TRUE /\ versions[i][1] < txnStartTs[t]} + IN IF visible = {} THEN Nil + ELSE versions[CHOOSE i \in visible : \A j \in visible : j <= i => versions[j][1] <= versions[i][1]] + +\* Has transaction t already written key k? +HasWritten(t, k) == k \in writeSet[t] + +----------------------------------------------------------------------------- +\* Initial state + +Init == + /\ db = [k \in Keys |-> << >>] + /\ txnState = [t \in 1..MaxTxnId |-> "Active"] + /\ txnStartTs = [t \in 1..MaxTxnId |-> 0] + /\ writeSet = [t \in 1..MaxTxnId |-> {}] + /\ readSet = [t \in 1..MaxTxnId |-> {}] + /\ globalClock = 1 + +----------------------------------------------------------------------------- +\* State transitions + +\* Begin a transaction: assign a start timestamp. +BeginTxn(t) == + /\ txnState[t] = "Active" + /\ txnStartTs[t] = 0 + /\ txnStartTs' = [txnStartTs EXCEPT ![t] = globalClock] + /\ globalClock' = globalClock + 1 + /\ UNCHANGED <> + +\* Read key k by transaction t. +Read(t, k) == + /\ txnState[t] = "Active" + /\ txnStartTs[t] > 0 + /\ readSet' = [readSet EXCEPT ![t] = @ \cup {k}] + /\ UNCHANGED <> + +\* Write key k with value v by transaction t. +Write(t, k, v) == + /\ txnState[t] = "Active" + /\ txnStartTs[t] > 0 + /\ k \notin writeSet[t] + /\ writeSet' = [writeSet EXCEPT ![t] = @ \cup {k}] + /\ db' = [db EXCEPT ![k] = Append(@, <>)] + /\ UNCHANGED <> + +\* Commit transaction t: mark its versions as committed (first-committer-wins). +CommitTxn(t) == + /\ txnState[t] = "Active" + /\ txnStartTs[t] > 0 + /\ ~(\E t2 \in 1..MaxTxnId : t2 /= t /\ txnState[t2] = "Committed" /\ + \E k \in Keys : k \in writeSet[t] /\ k \in writeSet[t2]) + /\ txnState' = [txnState EXCEPT ![t] = "Committed"] + /\ db' = [k \in Keys |-> + IF k \in writeSet[t] + THEN LET last == Len(db[k]) + lastTxn == db[k][last][1] + IN IF lastTxn = t + THEN [db[k] EXCEPT ![last] = <>] + ELSE db[k] + ELSE db[k]] + /\ UNCHANGED <> + +\* Abort transaction t: leave versions as uncommitted (garbage). +AbortTxn(t) == + /\ txnState[t] = "Active" + /\ txnState' = [txnState EXCEPT ![t] = "Aborted"] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +\* Next-state relation + +Next == + \/ \E t \in 1..MaxTxnId : BeginTxn(t) + \/ \E t \in 1..MaxTxnId : \E k \in Keys : Read(t, k) + \/ \E t \in 1..MaxTxnId : \E k \in Keys : \E v \in Values : Write(t, k, v) + \/ \E t \in 1..MaxTxnId : CommitTxn(t) + \/ \E t \in 1..MaxTxnId : AbortTxn(t) + +----------------------------------------------------------------------------- +\* Safety properties + +\* A committed transaction only wrote versions that are now marked committed. +NoDirtyReads == + \A t \in 1..MaxTxnId : + \A k \in Keys : + \A i \in 1..Len(db[k]) : + db[k][i][3] = TRUE => + db[k][i][1] \in {tx \in 1..MaxTxnId : txnState[tx] = "Committed"} + +\* If a transaction has written a key, its own read of that key sees the latest local value. +ReadOwnWrites == + \A t \in 1..MaxTxnId : + \A k \in Keys : + k \in writeSet[t] => + LET versions == db[k] + myWrites == {i \in 1..Len(versions) : versions[i][1] = t} + IN myWrites /= {} + +\* Snapshot isolation: no two committed transactions write the same key (first-committer-wins). +WriteWriteConflict == + \A t1, t2 \in 1..MaxTxnId : + t1 /= t2 /\ txnState[t1] = "Committed" /\ txnState[t2] = "Committed" => + ~(\E k \in Keys : k \in writeSet[t1] /\ k \in writeSet[t2]) + +\* Type invariant +TypeOk == + /\ \A k \in Keys : Len(db[k]) <= MaxTxnId * 2 + /\ \A k \in Keys : \A i \in 1..Len(db[k]) : db[k][i] \in (1..MaxTxnId) \X Values \X BOOLEAN + /\ txnState \in [1..MaxTxnId -> {"Active", "Committed", "Aborted"}] + /\ txnStartTs \in [1..MaxTxnId -> 0..(MaxTxnId+1)] + /\ writeSet \in [1..MaxTxnId -> SUBSET Keys] + /\ readSet \in [1..MaxTxnId -> SUBSET Keys] + /\ globalClock \in 1..(MaxTxnId + 1) + +============================================================================= diff --git a/formal-verification/raft.tla b/formal-verification/raft.tla new file mode 100644 index 0000000..b4d44c1 --- /dev/null +++ b/formal-verification/raft.tla @@ -0,0 +1,182 @@ +-------------------------------- MODULE raft -------------------------------- +(* + TLA+ specification of the Raft consensus algorithm as implemented in BaraDB. + Models: leader election, log replication, and commit safety. + + Key properties verified: + - ElectionSafety : at most one leader per term. + - LeaderAppendOnly : leaders only append, never overwrite their log. + - StateMachineSafety : committed entries are identical on all nodes. +*) + +EXTENDS Integers, Sequences, FiniteSets, TLC + +CONSTANTS Nodes, \* set of node IDs + Nil, \* distinguished nil value (model value) + MaxTerm, \* bound terms for model checking + MaxLogLen \* bound log length for model checking + +ASSUME IsFiniteSet(Nodes) + +VARIABLES + state, \* state[n] ∈ {"Follower", "Candidate", "Leader"} + currentTerm, \* currentTerm[n] ∈ Nat + votedFor, \* votedFor[n] ∈ Nodes ∪ {Nil} + log, \* log[n] ∈ Seq(<>) + commitIndex, \* commitIndex[n] ∈ Nat + votesGranted, \* votesGranted[n] ⊆ Nodes (only meaningful for Candidates) + nextIndex, \* nextIndex[n][m] ∈ Nat (leader state) + matchIndex \* matchIndex[n][m] ∈ Nat (leader state) + +vars == <> + +----------------------------------------------------------------------------- + +\* Helper operators + +Max(a, b) == IF a > b THEN a ELSE b +Min(a, b) == IF a < b THEN a ELSE b + +\* Bounded sequence set for TLC (Seq(S) is infinite) +BoundedSeq(S, n) == UNION {[1..m -> S] : m \in 0..n} + +\* Is node i a leader in term t? +IsLeader(i, t) == state[i] = "Leader" /\ currentTerm[i] = t + +\* The set of all log entries up to index len on node i +LogPrefix(i, len) == [j \in 1..len |-> log[i][j]] + +----------------------------------------------------------------------------- +\* Initial state + +Init == + /\ state = [n \in Nodes |-> "Follower"] + /\ currentTerm = [n \in Nodes |-> 1] + /\ votedFor = [n \in Nodes |-> Nil] + /\ log = [n \in Nodes |-> << >>] + /\ commitIndex = [n \in Nodes |-> 0] + /\ votesGranted = [n \in Nodes |-> {}] + /\ nextIndex = [n \in Nodes |-> [m \in Nodes |-> 1]] + /\ matchIndex = [n \in Nodes |-> [m \in Nodes |-> 0]] + +----------------------------------------------------------------------------- +\* State transitions + +\* A follower times out and starts a new election. +Timeout(i) == + /\ state[i] \in {"Follower", "Candidate"} + /\ currentTerm[i] < MaxTerm + /\ state' = [state EXCEPT ![i] = "Candidate"] + /\ currentTerm' = [currentTerm EXCEPT ![i] = @ + 1] + /\ votedFor' = [votedFor EXCEPT ![i] = i] + /\ votesGranted' = [votesGranted EXCEPT ![i] = {i}] + /\ UNCHANGED <> + +\* Node i votes for node j in j's current term. +Vote(i, j) == + /\ i /= j + /\ state[j] = "Candidate" + /\ currentTerm[j] > currentTerm[i] + /\ votedFor[i] = Nil + /\ currentTerm' = [currentTerm EXCEPT ![i] = currentTerm[j]] + /\ state' = [state EXCEPT ![i] = "Follower"] + /\ votedFor' = [votedFor EXCEPT ![i] = j] + /\ votesGranted' = [votesGranted EXCEPT ![j] = @ \cup {i}] + /\ UNCHANGED <> + +\* A candidate becomes leader after receiving a majority. +BecomeLeader(i) == + /\ state[i] = "Candidate" + /\ Cardinality(votesGranted[i]) * 2 > Cardinality(Nodes) + /\ state' = [state EXCEPT ![i] = "Leader"] + /\ nextIndex' = [nextIndex EXCEPT ![i] = [m \in Nodes |-> Len(log[i]) + 1]] + /\ matchIndex' = [matchIndex EXCEPT ![i] = [m \in Nodes |-> 0]] + /\ UNCHANGED <> + +\* Leader i appends a new entry to its own log. +AppendEntry(i) == + /\ state[i] = "Leader" + /\ Len(log[i]) < MaxLogLen + /\ log' = [log EXCEPT ![i] = Append(@, <>)] + /\ UNCHANGED <> + +\* Leader i replicates its log to follower j. +Replicate(i, j) == + /\ i /= j + /\ state[i] = "Leader" + /\ nextIndex[i][j] <= Len(log[i]) + /\ log' = [log EXCEPT ![j] = + IF Len(log[j]) >= nextIndex[i][j] + THEN [log[j] EXCEPT ![nextIndex[i][j]] = log[i][nextIndex[i][j]]] + ELSE Append(log[j], log[i][nextIndex[i][j]])] + /\ nextIndex' = [nextIndex EXCEPT ![i][j] = @ + 1] + /\ matchIndex' = [matchIndex EXCEPT ![i][j] = nextIndex[i][j]] + /\ UNCHANGED <> + +\* Leader i updates commitIndex when a majority has replicated an entry. +Commit(i) == + /\ state[i] = "Leader" + /\ LET majority == (Cardinality(Nodes) \div 2) + 1 + candidates == {idx \in (commitIndex[i]+1)..Len(log[i]) : + Cardinality({j \in Nodes : matchIndex[i][j] >= idx}) >= majority + /\ log[i][idx][1] = currentTerm[i]} + IN candidates /= {} + /\ commitIndex' = [commitIndex EXCEPT ![i] = CHOOSE idx \in candidates : TRUE] + /\ UNCHANGED <> + +\* A follower learns about a higher term and steps down. +StepDown(i, newTerm) == + /\ newTerm > currentTerm[i] + /\ currentTerm[i] < MaxTerm + /\ currentTerm' = [currentTerm EXCEPT ![i] = newTerm] + /\ state' = [state EXCEPT ![i] = "Follower"] + /\ votedFor' = [votedFor EXCEPT ![i] = Nil] + /\ votesGranted' = [votesGranted EXCEPT ![i] = {}] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +\* Next-state relation + +Next == + \/ \E i \in Nodes : Timeout(i) + \/ \E i, j \in Nodes : Vote(i, j) + \/ \E i \in Nodes : BecomeLeader(i) + \/ \E i \in Nodes : AppendEntry(i) + \/ \E i, j \in Nodes : Replicate(i, j) + \/ \E i \in Nodes : Commit(i) + \/ \E i \in Nodes : \E t \in 2..MaxTerm : StepDown(i, t) + +----------------------------------------------------------------------------- +\* Safety properties + +\* At most one leader per term. +ElectionSafety == + \A t \in 1..MaxTerm : + Cardinality({i \in Nodes : IsLeader(i, t)}) <= 1 + +\* Leaders never overwrite or delete their own log entries. +LeaderAppendOnly == + \A i \in Nodes : + state[i] = "Leader" => + \A j \in 1..Len(log[i]) : + [][Len(log[i]) >= j /\ log[i][j] = log'[i][j]]_vars + +\* If a log entry is committed, all higher leaders have that entry. +StateMachineSafety == + \A i, j \in Nodes : + \A idx \in 1..Min(commitIndex[i], commitIndex[j]) : + idx <= Len(log[i]) /\ idx <= Len(log[j]) => log[i][idx] = log[j][idx] + +\* Type invariant +TypeOk == + /\ state \in [Nodes -> {"Follower", "Candidate", "Leader"}] + /\ currentTerm \in [Nodes -> 1..MaxTerm] + /\ votedFor \in [Nodes -> Nodes \cup {Nil}] + /\ \A n \in Nodes : Len(log[n]) <= MaxLogLen + /\ \A n \in Nodes : \A i \in 1..Len(log[n]) : log[n][i] \in (1..MaxTerm) \X {"cmd"} + /\ commitIndex \in [Nodes -> 0..MaxLogLen] + /\ votesGranted \in [Nodes -> SUBSET Nodes] + /\ nextIndex \in [Nodes -> [Nodes -> 1..(MaxLogLen+1)]] + /\ matchIndex \in [Nodes -> [Nodes -> 0..MaxLogLen]] + +============================================================================= diff --git a/formal-verification/replication.tla b/formal-verification/replication.tla new file mode 100644 index 0000000..0e1f3c6 --- /dev/null +++ b/formal-verification/replication.tla @@ -0,0 +1,134 @@ +-------------------------------- MODULE replication -------------------------------- +(* + TLA+ specification of the BaraDB replication manager + (core/replication.nim) supporting Async, Sync, and Semi-sync modes. + + Key properties verified: + - MonotonicLsn : applied LSN never moves backwards. + - SyncDurability : in sync mode, ack is received from all connected replicas. + - SemiSyncQuorum : in semi-sync mode, ack is received from at least N replicas. +*) + +EXTENDS Integers, Sequences, FiniteSets, TLC + +CONSTANTS Replicas, \* set of replica IDs + MaxLsn, \* bound LSN values for model checking + MaxSyncCount \* bound semi-sync count + +ASSUME IsFiniteSet(Replicas) + +VARIABLES + mode, \* mode ∈ {"Async", "Sync", "SemiSync"} + replicaState, \* replicaState[r] ∈ {"Disconnected", "Connected"} + currentLsn, \* currentLsn ∈ Nat + pendingAcks, \* pendingAcks[l] ⊆ Replicas (LSNs waiting for acks) + appliedLsn, \* appliedLsn ∈ Nat + ackedBy \* ackedBy[l] ⊆ Replicas (who acked which LSN) + +vars == <> + +----------------------------------------------------------------------------- +\* Helper operators + +Max(a, b) == IF a > b THEN a ELSE b +Min(a, b) == IF a < b THEN a ELSE b + +ConnectedReplicas == {r \in Replicas : replicaState[r] = "Connected"} + +----------------------------------------------------------------------------- +\* Initial state + +Init == + /\ mode \in {"Async", "Sync", "SemiSync"} + /\ replicaState = [r \in Replicas |-> "Disconnected"] + /\ currentLsn = 0 + /\ pendingAcks = [l \in 0..MaxLsn |-> {}] + /\ appliedLsn = 0 + /\ ackedBy = [l \in 0..MaxLsn |-> {}] + +----------------------------------------------------------------------------- +\* State transitions + +\* A replica comes online. +Connect(r) == + /\ replicaState[r] = "Disconnected" + /\ replicaState' = [replicaState EXCEPT ![r] = "Connected"] + /\ UNCHANGED <> + +\* A replica goes offline. +Disconnect(r) == + /\ replicaState[r] = "Connected" + /\ replicaState' = [replicaState EXCEPT ![r] = "Disconnected"] + /\ UNCHANGED <> + +\* A new LSN is produced by the primary. +WriteLsn == + /\ currentLsn < MaxLsn + /\ currentLsn' = currentLsn + 1 + /\ LET newLsn == currentLsn + 1 + conn == ConnectedReplicas + IN IF mode = "Sync" /\ conn /= {} + THEN pendingAcks' = [pendingAcks EXCEPT ![newLsn] = conn] + ELSE IF mode = "SemiSync" /\ conn /= {} + THEN pendingAcks' = [pendingAcks EXCEPT ![newLsn] = + CHOOSE s \in SUBSET conn : + Cardinality(s) = Min(MaxSyncCount, Cardinality(conn))] + ELSE pendingAcks' = pendingAcks + /\ UNCHANGED <> + +\* Replica r acknowledges LSN l. +AckLsn(r, l) == + /\ replicaState[r] = "Connected" + /\ l \in 1..currentLsn + /\ r \in pendingAcks[l] + /\ ackedBy' = [ackedBy EXCEPT ![l] = @ \cup {r}] + /\ pendingAcks' = [pendingAcks EXCEPT ![l] = @ \ {r}] + /\ IF pendingAcks'[l] = {} + THEN appliedLsn' = Max(appliedLsn, l) + ELSE appliedLsn' = appliedLsn + /\ UNCHANGED <> + +\* Switch replication mode. +SwitchMode(newMode) == + /\ newMode \in {"Async", "Sync", "SemiSync"} + /\ mode' = newMode + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +\* Next-state relation + +Next == + \/ \E r \in Replicas : Connect(r) + \/ \E r \in Replicas : Disconnect(r) + \/ WriteLsn + \/ \E r \in Replicas : \E l \in 1..MaxLsn : AckLsn(r, l) + \/ \E newMode \in {"Async", "Sync", "SemiSync"} : SwitchMode(newMode) + +----------------------------------------------------------------------------- +\* Safety properties + +\* The applied LSN is monotonically non-decreasing. +MonotonicLsn == + [][appliedLsn' >= appliedLsn]_vars + +\* A replica that has acked an LSN is no longer pending for it. +AcksRemovePending == + \A l \in 1..currentLsn : + \A r \in Replicas : + r \in ackedBy[l] => r \notin pendingAcks[l] + +\* In sync/semi-sync mode, pending acks are only for known replicas. +PendingAreKnown == + \A l \in 1..currentLsn : + pendingAcks[l] \subseteq Replicas + +\* Type invariant +TypeOk == + /\ mode \in {"Async", "Sync", "SemiSync"} + /\ replicaState \in [Replicas -> {"Disconnected", "Connected"}] + /\ currentLsn \in 0..MaxLsn + /\ pendingAcks \in [0..MaxLsn -> SUBSET Replicas] + /\ appliedLsn \in 0..MaxLsn + /\ ackedBy \in [0..MaxLsn -> SUBSET Replicas] + +============================================================================= diff --git a/formal-verification/tla2tools.jar b/formal-verification/tla2tools.jar new file mode 100644 index 0000000..fed0509 Binary files /dev/null and b/formal-verification/tla2tools.jar differ diff --git a/formal-verification/twopc.tla b/formal-verification/twopc.tla new file mode 100644 index 0000000..cd31670 --- /dev/null +++ b/formal-verification/twopc.tla @@ -0,0 +1,157 @@ +-------------------------------- MODULE twopc -------------------------------- +(* + TLA+ specification of the Two-Phase Commit (2PC) distributed transaction + protocol as implemented in BaraDB (core/disttxn.nim). + + Key properties verified: + - Atomicity : all participants commit, or all abort. + - NoOrphanBlocks : a prepared participant never remains blocked forever + once the coordinator decides. +*) + +EXTENDS Integers, Sequences, FiniteSets, TLC + +CONSTANTS Participants, \* set of participant node IDs + Nil, \* distinguished nil value (model value) + MaxTxnId \* bound transaction IDs for model checking + +ASSUME IsFiniteSet(Participants) + +VARIABLES + txnState, \* txnState[t] ∈ {"Active","Preparing","Prepared","Committing", + \* "Committed","Aborting","Aborted"} + participantState, \* participantState[t][p] ∈ {"Active","Prepared","Committed","Aborted"} + coordinatorDecided, \* coordinatorDecided[t] ∈ {TRUE, FALSE} + decidedAction \* decidedAction[t] ∈ {"Commit","Abort", Nil} + +vars == <> + +----------------------------------------------------------------------------- + +\* Helper operators + +AllPrepared(t) == + \A p \in Participants : participantState[t][p] \in {"Prepared", "Committed", "Aborted"} + +AnyPrepareFailed(t) == + \E p \in Participants : participantState[t][p] = "Aborted" + +----------------------------------------------------------------------------- +\* Initial state + +Init == + /\ txnState = [t \in 1..MaxTxnId |-> "Active"] + /\ participantState = [t \in 1..MaxTxnId |-> [p \in Participants |-> "Active"]] + /\ coordinatorDecided = [t \in 1..MaxTxnId |-> FALSE] + /\ decidedAction = [t \in 1..MaxTxnId |-> Nil] + +----------------------------------------------------------------------------- +\* State transitions + +\* Phase 1a: Coordinator sends PREPARE to all participants. +SendPrepare(t) == + /\ txnState[t] = "Active" + /\ txnState' = [txnState EXCEPT ![t] = "Preparing"] + /\ UNCHANGED <> + +\* Phase 1b: Participant p receives PREPARE and votes Yes. +ParticipantPrepare(t, p) == + /\ txnState[t] = "Preparing" + /\ participantState[t][p] = "Active" + /\ participantState' = [participantState EXCEPT ![t][p] = "Prepared"] + /\ UNCHANGED <> + +\* Phase 1c: Participant p votes No (aborts locally). +ParticipantAbort(t, p) == + /\ txnState[t] \in {"Preparing", "Active"} + /\ participantState[t][p] = "Active" + /\ participantState' = [participantState EXCEPT ![t][p] = "Aborted"] + /\ UNCHANGED <> + +\* Phase 2a: Coordinator decides COMMIT (all voted Yes). +DecideCommit(t) == + /\ txnState[t] = "Preparing" + /\ AllPrepared(t) + /\ ~AnyPrepareFailed(t) + /\ txnState' = [txnState EXCEPT ![t] = "Committing"] + /\ coordinatorDecided' = [coordinatorDecided EXCEPT ![t] = TRUE] + /\ decidedAction' = [decidedAction EXCEPT ![t] = "Commit"] + /\ UNCHANGED <> + +\* Phase 2a-alt: Coordinator decides ABORT (at least one No or timeout). +DecideAbort(t) == + /\ txnState[t] = "Preparing" + /\ AnyPrepareFailed(t) + /\ txnState' = [txnState EXCEPT ![t] = "Aborting"] + /\ coordinatorDecided' = [coordinatorDecided EXCEPT ![t] = TRUE] + /\ decidedAction' = [decidedAction EXCEPT ![t] = "Abort"] + /\ UNCHANGED <> + +\* Phase 2b: Participant receives COMMIT decision. +ReceiveCommit(t, p) == + /\ txnState[t] = "Committing" + /\ decidedAction[t] = "Commit" + /\ participantState[t][p] \in {"Prepared", "Active"} + /\ participantState' = [participantState EXCEPT ![t][p] = "Committed"] + /\ UNCHANGED <> + +\* Phase 2b-alt: Participant receives ABORT decision. +ReceiveAbort(t, p) == + /\ txnState[t] = "Aborting" + /\ decidedAction[t] = "Abort" + /\ participantState[t][p] \in {"Prepared", "Active", "Aborted"} + /\ participantState' = [participantState EXCEPT ![t][p] = "Aborted"] + /\ UNCHANGED <> + +\* Finalize: transaction moves to terminal state when all participants are done. +FinalizeCommit(t) == + /\ txnState[t] = "Committing" + /\ \A p \in Participants : participantState[t][p] = "Committed" + /\ txnState' = [txnState EXCEPT ![t] = "Committed"] + /\ UNCHANGED <> + +FinalizeAbort(t) == + /\ txnState[t] = "Aborting" + /\ \A p \in Participants : participantState[t][p] = "Aborted" + /\ txnState' = [txnState EXCEPT ![t] = "Aborted"] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +\* Next-state relation + +Next == + \/ \E t \in 1..MaxTxnId : SendPrepare(t) + \/ \E t \in 1..MaxTxnId : \E p \in Participants : ParticipantPrepare(t, p) + \/ \E t \in 1..MaxTxnId : \E p \in Participants : ParticipantAbort(t, p) + \/ \E t \in 1..MaxTxnId : DecideCommit(t) + \/ \E t \in 1..MaxTxnId : DecideAbort(t) + \/ \E t \in 1..MaxTxnId : \E p \in Participants : ReceiveCommit(t, p) + \/ \E t \in 1..MaxTxnId : \E p \in Participants : ReceiveAbort(t, p) + \/ \E t \in 1..MaxTxnId : FinalizeCommit(t) + \/ \E t \in 1..MaxTxnId : FinalizeAbort(t) + +----------------------------------------------------------------------------- +\* Safety properties + +\* Atomicity: it is never the case that one participant committed while another aborted. +Atomicity == + \A t \in 1..MaxTxnId : + ~(\E p1, p2 \in Participants : + participantState[t][p1] = "Committed" /\ participantState[t][p2] = "Aborted") + +\* No orphan blocks: once a transaction is fully committed, every participant is committed. +NoOrphanBlocks == + \A t \in 1..MaxTxnId : + txnState[t] = "Committed" => + \A p \in Participants : participantState[t][p] = "Committed" + +\* Type invariant +TypeOk == + /\ txnState \in [1..MaxTxnId -> {"Active","Preparing","Prepared","Committing", + "Committed","Aborting","Aborted"}] + /\ participantState \in [1..MaxTxnId -> [Participants -> {"Active","Prepared", + "Committed","Aborted"}]] + /\ coordinatorDecided \in [1..MaxTxnId -> BOOLEAN] + /\ decidedAction \in [1..MaxTxnId -> {"Commit","Abort", Nil}] + +=============================================================================