|
| 1 | +------------------------------ MODULE OctadAtomicity ------------------------------ |
| 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 | +\* V5: Transaction atomicity across the 8 modalities of a VeriSimDB octad. |
| 6 | +\* Corresponds to rust-core/verisim-octad/src/transaction.rs. |
| 7 | +\* |
| 8 | +\* A VeriSimDB octad is a record with 8 per-modality projections. A transaction |
| 9 | +\* touches a subset of the 8 modality projections and must be either fully |
| 10 | +\* committed (all 8 projections updated) or fully aborted (none visible). No |
| 11 | +\* PARTIAL state is ever observable outside a transaction's own PENDING scope. |
| 12 | +\* |
| 13 | +\* This spec models the transaction lifecycle (PENDING -> COMMITTED | ABORTED) |
| 14 | +\* together with fault injection (crashes during a PENDING transaction) and |
| 15 | +\* proves the Atomicity invariant under an adversary that can interleave |
| 16 | +\* multiple concurrent transactions and crashes. |
| 17 | + |
| 18 | +EXTENDS Naturals, FiniteSets, TLC |
| 19 | + |
| 20 | +CONSTANTS |
| 21 | + Txns, \* finite set of transaction identifiers |
| 22 | + MaxCrashes \* bound on the number of crash events per run |
| 23 | + |
| 24 | +ASSUME Cardinality(Txns) >= 1 |
| 25 | +ASSUME MaxCrashes \in Nat |
| 26 | + |
| 27 | +\* The 8 modalities of a VeriSimDB octad. |
| 28 | +Modalities == {"graph", "vector", "tensor", "semantic", |
| 29 | + "document", "temporal", "provenance", "spatial"} |
| 30 | + |
| 31 | +Status == {"PENDING", "COMMITTED", "ABORTED"} |
| 32 | + |
| 33 | +VARIABLES |
| 34 | + txnStatus, \* [Txns -> Status] - each transaction's lifecycle stage |
| 35 | + modalityUpdates, \* [Txns -> SUBSET Modalities] - modalities already applied |
| 36 | + crashes \* Nat - bounded counter for fault-injection events |
| 37 | + |
| 38 | +vars == <<txnStatus, modalityUpdates, crashes>> |
| 39 | + |
| 40 | +TypeOK == |
| 41 | + /\ txnStatus \in [Txns -> Status] |
| 42 | + /\ modalityUpdates \in [Txns -> SUBSET Modalities] |
| 43 | + /\ crashes \in 0..MaxCrashes |
| 44 | + |
| 45 | +Init == |
| 46 | + /\ txnStatus = [t \in Txns |-> "PENDING"] |
| 47 | + /\ modalityUpdates = [t \in Txns |-> {}] |
| 48 | + /\ crashes = 0 |
| 49 | + |
| 50 | +-------------------------------------------------------------------------------- |
| 51 | +\* Incremental per-modality application during a PENDING transaction. |
| 52 | +\* Each modality can be applied at most once per transaction (enforced by the |
| 53 | +\* set-union: \cup already-applied is idempotent, but we also disallow reapply |
| 54 | +\* via the `m \notin` guard so TLC bounds the state space by 2^|Modalities|). |
| 55 | +-------------------------------------------------------------------------------- |
| 56 | +ApplyModality(t, m) == |
| 57 | + /\ txnStatus[t] = "PENDING" |
| 58 | + /\ m \notin modalityUpdates[t] |
| 59 | + /\ modalityUpdates' = [modalityUpdates EXCEPT ![t] = @ \cup {m}] |
| 60 | + /\ UNCHANGED <<txnStatus, crashes>> |
| 61 | + |
| 62 | +-------------------------------------------------------------------------------- |
| 63 | +\* Commit: only allowed once all 8 modalities have been applied. The commit |
| 64 | +\* is itself atomic in the spec (single state transition); the Rust source is |
| 65 | +\* expected to implement this via a 2-phase commit or equivalent mechanism. |
| 66 | +-------------------------------------------------------------------------------- |
| 67 | +Commit(t) == |
| 68 | + /\ txnStatus[t] = "PENDING" |
| 69 | + /\ modalityUpdates[t] = Modalities |
| 70 | + /\ txnStatus' = [txnStatus EXCEPT ![t] = "COMMITTED"] |
| 71 | + /\ UNCHANGED <<modalityUpdates, crashes>> |
| 72 | + |
| 73 | +-------------------------------------------------------------------------------- |
| 74 | +\* Abort: unilateral rollback. Clears all applied updates and transitions to |
| 75 | +\* ABORTED. Can fire at any time during PENDING. |
| 76 | +-------------------------------------------------------------------------------- |
| 77 | +Abort(t) == |
| 78 | + /\ txnStatus[t] = "PENDING" |
| 79 | + /\ txnStatus' = [txnStatus EXCEPT ![t] = "ABORTED"] |
| 80 | + /\ modalityUpdates' = [modalityUpdates EXCEPT ![t] = {}] |
| 81 | + /\ UNCHANGED crashes |
| 82 | + |
| 83 | +-------------------------------------------------------------------------------- |
| 84 | +\* Crash during PENDING. Recovery must act as an abort: rollback applied |
| 85 | +\* updates, transition to ABORTED. This is the adversarial event that the |
| 86 | +\* Atomicity invariant is designed to defeat: without the rollback, a crash |
| 87 | +\* mid-transaction would leave some modalities updated and the txnStatus |
| 88 | +\* visible, i.e. a partial commit. |
| 89 | +-------------------------------------------------------------------------------- |
| 90 | +Crash(t) == |
| 91 | + /\ crashes < MaxCrashes |
| 92 | + /\ txnStatus[t] = "PENDING" |
| 93 | + /\ txnStatus' = [txnStatus EXCEPT ![t] = "ABORTED"] |
| 94 | + /\ modalityUpdates' = [modalityUpdates EXCEPT ![t] = {}] |
| 95 | + /\ crashes' = crashes + 1 |
| 96 | + |
| 97 | +Next == |
| 98 | + \/ \E t \in Txns, m \in Modalities: ApplyModality(t, m) |
| 99 | + \/ \E t \in Txns: Commit(t) |
| 100 | + \/ \E t \in Txns: Abort(t) |
| 101 | + \/ \E t \in Txns: Crash(t) |
| 102 | + |
| 103 | +\* Fairness: every transaction eventually resolves (either commits or aborts). |
| 104 | +\* WF on (Commit \/ Abort) is sufficient because Abort is always enabled while |
| 105 | +\* the transaction is PENDING, so the disjunction is continuously enabled. |
| 106 | +Spec == Init |
| 107 | + /\ [][Next]_vars |
| 108 | + /\ \A t \in Txns: WF_vars(Commit(t) \/ Abort(t)) |
| 109 | + |
| 110 | +-------------------------------------------------------------------------------- |
| 111 | +\* Safety properties |
| 112 | +-------------------------------------------------------------------------------- |
| 113 | + |
| 114 | +\* I1. The central atomicity claim: |
| 115 | +\* COMMITTED => all 8 modalities updated |
| 116 | +\* ABORTED => no modalities updated |
| 117 | +\* This is the "all-or-nothing" observation externally visible on an octad. |
| 118 | +Atomicity == |
| 119 | + \A t \in Txns: |
| 120 | + /\ (txnStatus[t] = "COMMITTED" => modalityUpdates[t] = Modalities) |
| 121 | + /\ (txnStatus[t] = "ABORTED" => modalityUpdates[t] = {}) |
| 122 | + |
| 123 | +\* I2. No observable partial state: once a transaction is no longer PENDING, |
| 124 | +\* its modalityUpdates set is either empty or the full 8. This is derivable |
| 125 | +\* from Atomicity but stated separately because it is the property consumers |
| 126 | +\* of the octad actually rely on ("if I read a committed octad, I never see a |
| 127 | +\* half-update"). |
| 128 | +NoObservablePartial == |
| 129 | + \A t \in Txns: |
| 130 | + (txnStatus[t] \in {"COMMITTED", "ABORTED"}) => |
| 131 | + (modalityUpdates[t] = Modalities \/ modalityUpdates[t] = {}) |
| 132 | + |
| 133 | +\* I3. Status monotonicity: PENDING can move to COMMITTED or ABORTED, but |
| 134 | +\* never the reverse. (This is implicitly enforced by Next -- every action |
| 135 | +\* that changes txnStatus requires it was PENDING -- but stating it as an |
| 136 | +\* invariant on (txnStatus, txnStatus') is not trivial without action vars; |
| 137 | +\* instead we check a weaker "never COMMITTED AND ABORTED" which is trivially |
| 138 | +\* true by type but confirms no action flips between terminal statuses.) |
| 139 | +StatusMonotone == |
| 140 | + \A t \in Txns: |
| 141 | + \neg (txnStatus[t] = "COMMITTED" /\ modalityUpdates[t] = {}) |
| 142 | + |
| 143 | +OctadSafe == |
| 144 | + /\ TypeOK |
| 145 | + /\ Atomicity |
| 146 | + /\ NoObservablePartial |
| 147 | + /\ StatusMonotone |
| 148 | + |
| 149 | +-------------------------------------------------------------------------------- |
| 150 | +\* Liveness |
| 151 | +-------------------------------------------------------------------------------- |
| 152 | + |
| 153 | +\* Every transaction eventually reaches a terminal state. |
| 154 | +EveryTxnResolves == |
| 155 | + \A t \in Txns: <>(txnStatus[t] \in {"COMMITTED", "ABORTED"}) |
| 156 | + |
| 157 | +THEOREM AtomicitySafety == Spec => []OctadSafe |
| 158 | +THEOREM Resolution == Spec => EveryTxnResolves |
| 159 | + |
| 160 | +================================================================================ |
0 commit comments