|
| 1 | +---------------------------- MODULE Serializability ---------------------------- |
| 2 | +\* SPDX-License-Identifier: PMPL-1.0-or-later |
| 3 | +\* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 4 | +\* |
| 5 | +\* V10: Conflict serializability for concurrent transactions on an octad. |
| 6 | +\* Corresponds to rust-core/verisim-octad/src/transaction.rs (concurrent path). |
| 7 | +\* |
| 8 | +\* V5 proved atomicity for a single transaction under crashes. V10 extends |
| 9 | +\* that to *multiple* concurrent transactions: the spec asserts that any |
| 10 | +\* concurrent execution is conflict-equivalent to some serial execution of |
| 11 | +\* the same transactions. |
| 12 | +\* |
| 13 | +\* Concurrency protocol modelled: atomic two-phase locking (2PL+atomic-acquire). |
| 14 | +\* - Each transaction has a fixed access-set (reads \cup writes) declared at |
| 15 | +\* design time (the TxnAccess constant). |
| 16 | +\* - Begin(t) atomically acquires the full access-set, or blocks. |
| 17 | +\* - Commit(t) releases locks and appends to the commit log. |
| 18 | +\* This rules out deadlock by construction (atomic acquisition) and by the |
| 19 | +\* same stroke makes the commit-log a valid serial schedule of the concurrent |
| 20 | +\* execution. The spec's job is to verify both claims. |
| 21 | + |
| 22 | +EXTENDS Naturals, FiniteSets, Sequences, TLC |
| 23 | + |
| 24 | +\* Scenario is fixed at module level because TLC config files cannot express |
| 25 | +\* record literals for TxnReads/TxnWrites, and this keeps a single-file spec |
| 26 | +\* straightforwardly model-checkable. Alternative scenarios live as separate |
| 27 | +\* .tla files. |
| 28 | +\* |
| 29 | +\* The scenario chosen: 3 transactions and 3 modalities, with pairwise |
| 30 | +\* conflicts forming a simple chain. This is the smallest non-trivial |
| 31 | +\* serializability test: |
| 32 | +\* - t1 reads {m1, m2}, writes {m1}. (conflicts with t2 on m1) |
| 33 | +\* - t2 reads {m1}, writes {m2}. (conflicts with t1 on m1, |
| 34 | +\* with t3 on m2) |
| 35 | +\* - t3 reads {m2}, writes {m3}. (conflicts with t2 on m2) |
| 36 | +\* Every pair of txns has an overlapping access-set, so 2PL must serialise |
| 37 | +\* *some* total order on them. TLC explores all possible commit orders. |
| 38 | + |
| 39 | +Txns == {"t1", "t2", "t3"} |
| 40 | +Modalities == {"m1", "m2", "m3"} |
| 41 | + |
| 42 | +TxnReads == [t \in Txns |-> |
| 43 | + CASE t = "t1" -> {"m1", "m2"} |
| 44 | + [] t = "t2" -> {"m1"} |
| 45 | + [] t = "t3" -> {"m2"}] |
| 46 | + |
| 47 | +TxnWrites == [t \in Txns |-> |
| 48 | + CASE t = "t1" -> {"m1"} |
| 49 | + [] t = "t2" -> {"m2"} |
| 50 | + [] t = "t3" -> {"m3"}] |
| 51 | + |
| 52 | +ASSUME Cardinality(Txns) >= 2 \* serializability is trivial for 1 txn |
| 53 | +ASSUME Cardinality(Modalities) >= 1 |
| 54 | +ASSUME TxnReads \in [Txns -> SUBSET Modalities] |
| 55 | +ASSUME TxnWrites \in [Txns -> SUBSET Modalities] |
| 56 | + |
| 57 | +\* A transaction's access-set is everything it reads or writes. 2PL acquires |
| 58 | +\* the whole set atomically at Begin. |
| 59 | +AccessSet(t) == TxnReads[t] \cup TxnWrites[t] |
| 60 | + |
| 61 | +VARIABLES |
| 62 | + txnStatus, \* [Txns -> {"IDLE", "ACTIVE", "COMMITTED"}] |
| 63 | + holdsLocks, \* [Txns -> SUBSET Modalities] -- currently held |
| 64 | + commitLog \* Seq(Txns) -- commit order (the serial schedule) |
| 65 | + |
| 66 | +vars == <<txnStatus, holdsLocks, commitLog>> |
| 67 | + |
| 68 | +Status == {"IDLE", "ACTIVE", "COMMITTED"} |
| 69 | + |
| 70 | +TypeOK == |
| 71 | + /\ txnStatus \in [Txns -> Status] |
| 72 | + /\ holdsLocks \in [Txns -> SUBSET Modalities] |
| 73 | + /\ commitLog \in Seq(Txns) |
| 74 | + |
| 75 | +Init == |
| 76 | + /\ txnStatus = [t \in Txns |-> "IDLE"] |
| 77 | + /\ holdsLocks = [t \in Txns |-> {}] |
| 78 | + /\ commitLog = << >> |
| 79 | + |
| 80 | +-------------------------------------------------------------------------------- |
| 81 | +\* Begin: atomically acquire all locks in AccessSet(t). Fires only if no other |
| 82 | +\* transaction currently holds any lock in AccessSet(t). Atomic acquisition |
| 83 | +\* is what rules out deadlock -- no partial lock sets ever exist. |
| 84 | +-------------------------------------------------------------------------------- |
| 85 | +Begin(t) == |
| 86 | + /\ txnStatus[t] = "IDLE" |
| 87 | + /\ \A other \in Txns: |
| 88 | + (other /= t) => (holdsLocks[other] \cap AccessSet(t) = {}) |
| 89 | + /\ txnStatus' = [txnStatus EXCEPT ![t] = "ACTIVE"] |
| 90 | + /\ holdsLocks' = [holdsLocks EXCEPT ![t] = AccessSet(t)] |
| 91 | + /\ UNCHANGED commitLog |
| 92 | + |
| 93 | +-------------------------------------------------------------------------------- |
| 94 | +\* Commit: release all locks, mark COMMITTED, append to serial log. Only an |
| 95 | +\* ACTIVE transaction (= one that has successfully acquired) can commit. |
| 96 | +-------------------------------------------------------------------------------- |
| 97 | +Commit(t) == |
| 98 | + /\ txnStatus[t] = "ACTIVE" |
| 99 | + /\ holdsLocks[t] = AccessSet(t) |
| 100 | + /\ txnStatus' = [txnStatus EXCEPT ![t] = "COMMITTED"] |
| 101 | + /\ holdsLocks' = [holdsLocks EXCEPT ![t] = {}] |
| 102 | + /\ commitLog' = Append(commitLog, t) |
| 103 | + |
| 104 | +Next == |
| 105 | + \/ \E t \in Txns: Begin(t) |
| 106 | + \/ \E t \in Txns: Commit(t) |
| 107 | + |
| 108 | +\* Fairness: every ACTIVE txn eventually commits, every IDLE txn eventually |
| 109 | +\* begins (or has no opportunity because all other txns hold its locks -- |
| 110 | +\* but atomic acquisition means some txn always makes progress, so an IDLE |
| 111 | +\* txn cannot be permanently starved in this model). |
| 112 | +Spec == Init /\ [][Next]_vars |
| 113 | + /\ \A t \in Txns: WF_vars(Begin(t) \/ Commit(t)) |
| 114 | + |
| 115 | +-------------------------------------------------------------------------------- |
| 116 | +\* Safety properties |
| 117 | +-------------------------------------------------------------------------------- |
| 118 | + |
| 119 | +\* I1. Lock mutex: no two transactions hold overlapping locks simultaneously. |
| 120 | +\* This is the 2PL invariant; its violation would be a direct serializability |
| 121 | +\* failure. |
| 122 | +NoSharedLocks == |
| 123 | + \A t1, t2 \in Txns: |
| 124 | + (t1 /= t2) => (holdsLocks[t1] \cap holdsLocks[t2] = {}) |
| 125 | + |
| 126 | +\* I2. Locks are held only by ACTIVE transactions. IDLE and COMMITTED txns |
| 127 | +\* own no locks. |
| 128 | +LocksOnlyWhileActive == |
| 129 | + \A t \in Txns: |
| 130 | + (txnStatus[t] \in {"IDLE", "COMMITTED"}) => (holdsLocks[t] = {}) |
| 131 | + |
| 132 | +\* I3. Lock-set matches the txn's AccessSet when ACTIVE. No partial acquisitions. |
| 133 | +\* This is what atomic-Begin enforces structurally. |
| 134 | +ActiveHoldsFullAccessSet == |
| 135 | + \A t \in Txns: |
| 136 | + (txnStatus[t] = "ACTIVE") => (holdsLocks[t] = AccessSet(t)) |
| 137 | + |
| 138 | +\* I4. No duplicate commit log entries -- each txn commits at most once. |
| 139 | +CommitLogInjective == |
| 140 | + \A i, j \in 1..Len(commitLog): |
| 141 | + (commitLog[i] = commitLog[j]) => (i = j) |
| 142 | + |
| 143 | +\* I5. Commit log only contains COMMITTED txns. |
| 144 | +CommitLogSound == |
| 145 | + \A i \in 1..Len(commitLog): |
| 146 | + txnStatus[commitLog[i]] = "COMMITTED" |
| 147 | + |
| 148 | +\* I6. CENTRAL serializability claim: for any two committed conflicting txns |
| 149 | +\* (sharing a written modality), the one that appears earlier in the commit |
| 150 | +\* log is the one that accessed first. Because 2PL prevents overlap, this is |
| 151 | +\* always true -- the commit log IS a conflict-equivalent serial order. |
| 152 | +\* |
| 153 | +\* Formal statement: if t1 and t2 both appear in commitLog and they conflict |
| 154 | +\* (t1 writes some m that t2 reads or writes, or vice versa), then their |
| 155 | +\* relative order in commitLog is consistent with the (trivially unique) |
| 156 | +\* sequential order in which they held the shared lock. Since only one txn |
| 157 | +\* can hold a given lock at a time and locks are released at Commit, the txn |
| 158 | +\* committed earlier necessarily ran earlier. So the log IS the schedule. |
| 159 | +\* |
| 160 | +\* Operationally this reduces to: two conflicting txns both committed implies |
| 161 | +\* they don't appear "simultaneously" in the log -- which is trivially true |
| 162 | +\* of a sequence. What we really want to check is that ACTIVE sets of |
| 163 | +\* conflicting txns never co-exist. That is exactly NoSharedLocks when |
| 164 | +\* combined with ActiveHoldsFullAccessSet -- two ACTIVE txns have disjoint |
| 165 | +\* access-sets, so no WW / WR / RW conflict can be concurrent. |
| 166 | +NoConcurrentConflict == |
| 167 | + \A t1, t2 \in Txns: |
| 168 | + (t1 /= t2 |
| 169 | + /\ txnStatus[t1] = "ACTIVE" /\ txnStatus[t2] = "ACTIVE" |
| 170 | + /\ ((TxnWrites[t1] \cap (TxnReads[t2] \cup TxnWrites[t2])) /= {} |
| 171 | + \/ (TxnWrites[t2] \cap (TxnReads[t1] \cup TxnWrites[t1])) /= {})) |
| 172 | + => FALSE |
| 173 | + |
| 174 | +SerializabilitySafe == |
| 175 | + /\ TypeOK |
| 176 | + /\ NoSharedLocks |
| 177 | + /\ LocksOnlyWhileActive |
| 178 | + /\ ActiveHoldsFullAccessSet |
| 179 | + /\ CommitLogInjective |
| 180 | + /\ CommitLogSound |
| 181 | + /\ NoConcurrentConflict |
| 182 | + |
| 183 | +-------------------------------------------------------------------------------- |
| 184 | +\* Liveness |
| 185 | +-------------------------------------------------------------------------------- |
| 186 | + |
| 187 | +\* Every transaction eventually commits. Under atomic-acquire 2PL + WF, no |
| 188 | +\* transaction can be starved forever: every state has at least one enabled |
| 189 | +\* action (either some IDLE txn can Begin, since at most |Txns|-1 txns can |
| 190 | +\* be ACTIVE at once -- and a fully ACTIVE state has at least one Commit |
| 191 | +\* enabled; and after any Commit, freed locks re-enable some IDLE Begin). |
| 192 | +EveryTxnCommits == |
| 193 | + \A t \in Txns: <>(txnStatus[t] = "COMMITTED") |
| 194 | + |
| 195 | +THEOREM SerializabilitySafety == Spec => []SerializabilitySafe |
| 196 | +THEOREM AllCommit == Spec => EveryTxnCommits |
| 197 | + |
| 198 | +================================================================================ |
0 commit comments