From fcf87ccbdd5bc668b7e7a73fef1619988925cf5a Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Sat, 3 Jan 2026 02:59:26 +0700 Subject: [PATCH 01/23] add tla+ spec for transaction lifecycle Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- .gitignore | 3 + transaction_lifecycle.cfg | 9 + transaction_lifecycle.tla | 357 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 369 insertions(+) create mode 100644 transaction_lifecycle.cfg create mode 100644 transaction_lifecycle.tla diff --git a/.gitignore b/.gitignore index d4799022..ae3aa0d5 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,4 @@ deploy_key +transaction_lifecycle.out +.vscode/ +states/ diff --git a/transaction_lifecycle.cfg b/transaction_lifecycle.cfg new file mode 100644 index 00000000..b1b8db16 --- /dev/null +++ b/transaction_lifecycle.cfg @@ -0,0 +1,9 @@ +SPECIFICATION Spec + +CONSTANT N = 2 + +INVARIANT TypeOK +INVARIANT NoTwoLiveUpgradeTxs +INVARIANT ActiveUpgradeTxImpliesConnOpenAndHead + + diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla new file mode 100644 index 00000000..30ce5e26 --- /dev/null +++ b/transaction_lifecycle.tla @@ -0,0 +1,357 @@ +------------------------------ MODULE transaction_lifecycle ------------------------------ +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANT N +VARIABLES transactions, clock, stores, connections, dbVersion, connection_queue +\* TLA+ model of the transaction lifecycle and scheduling rules from: +\* - +\* - + +Stores == 0..N +Transactions == 0..N +Requests == 0..N +Connections == 0..N +Versions == 0..N + +\* Note: by using only a single dbVersion, we do not model multiple databases. +Vars == << transactions, clock, stores, connections, dbVersion, connection_queue >> + +Modes == {"readonly", "readwrite", "versionchange"} +TxStates == {"None", "Active", "Inactive", "Committing", "Finished"} + +TypeOK == + /\ clock \in Nat + /\ stores \in [Stores -> BOOLEAN] + /\ dbVersion \in Versions + /\ connections \in [Connections -> + [ open : BOOLEAN, + pendingUpgrade : BOOLEAN, + requestedVersion: Versions ]] + /\ connection_queue \in Seq(Connections) + /\ transactions \in [Transactions -> + [ conn : Connections, + mode : Modes, + stores : SUBSET Stores, + requests : Seq(Requests), + state : TxStates, + createdAt : Nat ]] + +IsCreated(tx) == transactions[tx].state # "None" + +Live(tx) == IsCreated(tx) /\ transactions[tx].state # "Finished" + +Overlaps(tx1, tx2) == (transactions[tx1].stores \cap transactions[tx2].stores) # {} + +CreatedBefore(tx1, tx2) == transactions[tx1].createdAt < transactions[tx2].createdAt + +ConnOpen(c) == connections[c].open + +ConnPendingUpgrade(c) == connections[c].pendingUpgrade + +TxForConn(c) == { tx \in Transactions : Live(tx) /\ transactions[tx].conn = c } + +AllTxFinishedForConn(c) == + \A tx \in Transactions: + (transactions[tx].conn = c) => (transactions[tx].state \in {"None", "Finished"}) + +HasLiveUpgradeTx(c) == + \E tx \in Transactions: + /\ Live(tx) + /\ transactions[tx].conn = c + /\ transactions[tx].mode = "versionchange" + +\* Safety property: at most one upgrade transaction is live at a time. +NoTwoLiveUpgradeTxs == + Cardinality({ tx \in Transactions : Live(tx) /\ transactions[tx].mode = "versionchange" }) <= 1 + +\* Inductive invariants that implies NoTwoLiveUpgradeTxs. +\* +\* If a versionchange transaction is live, then its connection is open and +\* is at the head of the connection queue. +ActiveUpgradeTxImpliesConnOpenAndHead == + \A tx \in Transactions: + (Live(tx) /\ transactions[tx].mode = "versionchange") + => + /\ ConnOpen(transactions[tx].conn) + /\ Len(connection_queue) > 0 + /\ Head(connection_queue) = transactions[tx].conn + +\* . +CanStart(tx) == + LET m == transactions[tx].mode IN + IF m = "readonly" THEN + ~\E other \in (Transactions \ {tx}): + /\ Live(other) + /\ transactions[other].mode = "readwrite" + /\ CreatedBefore(other, tx) + /\ Overlaps(other, tx) + ELSE IF m = "readwrite" THEN + ~\E other \in (Transactions \ {tx}): + /\ Live(other) + /\ CreatedBefore(other, tx) + /\ Overlaps(other, tx) + ELSE \* versionchange transactions can always start. + TRUE +----------------------------------------------------------------------------------------- + +DefaultTx == + [ conn |-> 0, + mode |-> "readonly", + stores |-> {}, + requests |-> <<>>, + state |-> "None", + createdAt |-> 0 ] + +DefaultConn == + [ open |-> FALSE, + pendingUpgrade |-> FALSE, + requestedVersion|-> 0 ] + +Init == + /\ transactions = [tx \in Transactions |-> DefaultTx] + /\ clock = 0 + /\ stores = [s \in Stores |-> FALSE] + /\ connections = [c \in Connections |-> DefaultConn] + /\ dbVersion = 0 + /\ connection_queue = <<>> + +\* +OpenConnection(c, requestedVersion) == + /\ dbVersion <= requestedVersion + /\ connections[c] = DefaultConn + /\ connections' = [connections EXCEPT + ![c] = [open |-> FALSE, + pendingUpgrade |-> (requestedVersion > dbVersion), + requestedVersion|-> requestedVersion] + ] + /\ connection_queue' = Append(connection_queue, c) + /\ UNCHANGED <> + +\* +\* +\* Note: A non-upgrade open request can be processed once it reaches the head +\* of the queue. +FinishOpenConnection(c) == + /\ Len(connection_queue) > 0 + /\ c = Head(connection_queue) + /\ ~ConnPendingUpgrade(c) + /\ ~ConnOpen(c) + /\ connections[c].requestedVersion = dbVersion + /\ connections' = [connections EXCEPT ![c].open = TRUE] + /\ connection_queue' = Tail(connection_queue) + /\ UNCHANGED <> + +\* +\* When all other connections are closed, and this connection is at the head of queue, +\* create and start the ugrade transaction. +\* The connection is removed from the queue when the transaction is finished. +\* See `Abort` and `CommitDone`. +CreateUpgradeTransaction(tx, c) == + /\ Len(connection_queue) > 0 + /\ c = Head(connection_queue) + /\ ConnPendingUpgrade(c) + /\ ~ConnOpen(c) + /\ \A other \in (Connections \ {c}): ~ConnOpen(other) + /\ ~IsCreated(tx) + /\ transactions' = [transactions EXCEPT + ![tx] = [conn |-> c, + mode |-> "versionchange", + stores |-> { s \in Stores : stores[s] }, + requests |-> <<>>, + state |-> "Active", + createdAt |-> clock] + ] + /\ connections' = [connections EXCEPT + ![c].open = TRUE + ] + /\ dbVersion' = connections[c].requestedVersion + /\ clock' = clock + 1 + /\ UNCHANGED <> + +\* +\* +\* "Wait for all transactions created using connection to complete. +\* Once they are complete, connection is closed." +\* +\* Note: forced close is not modeled right now. +CloseConnection(c) == + /\ ConnOpen(c) + /\ AllTxFinishedForConn(c) + /\ connections' = [connections EXCEPT ![c].open = FALSE] + /\ UNCHANGED <> + +\* +CreateTransaction(tx, c, mode, scope) == + /\ ~IsCreated(tx) + /\ ConnOpen(c) + \* If a live upgrade transaction is associated with the connection, throw + /\ ~HasLiveUpgradeTx(c) + /\ \A s \in scope: stores[s] + /\ transactions' = [transactions EXCEPT + ![tx] = [conn |-> c, + mode |-> mode, + stores |-> scope, + requests |-> <<>>, + state |-> "Active", + createdAt |-> clock] + ] + /\ clock' = clock + 1 + /\ UNCHANGED <> + +\* +\* +\* "New requests can be made against the transaction when it is +\* in [active]" and "The implementation must allow requests to be placed +\* against the transaction whenever it is active". +AddRequest(tx, r) == + /\ Live(tx) + /\ ConnOpen(transactions[tx].conn) + /\ transactions[tx].state = "Active" + /\ Len(transactions[tx].requests) < N + /\ transactions' = [transactions EXCEPT ![tx].requests = Append(@, r)] + /\ UNCHANGED <> + +\* +\* +\* "Requests must be executed in the order in which +\* they were made" and "While the event is being dispatched, the transaction +\* state is set to active". +ProcessRequest(tx) == + /\ Live(tx) + /\ CanStart(tx) + /\ ConnOpen(transactions[tx].conn) + /\ transactions[tx].state \in {"Active", "Inactive", "Committing"} + /\ Len(transactions[tx].requests) > 0 + /\ transactions' = [transactions EXCEPT + ![tx].requests = Tail(@), + ![tx].state = "Active" + ] + /\ UNCHANGED <> + +\* +\* +\* "Once the event dispatch is complete, the transaction's state +\* is set to inactive again". +\* +\* Note: the event is dispatched and the transaction de-activated +\* from within the same task, but we still model these as separate +\* steps to make it easier to model adding any number of requests +\* while the transaction is active. +Deactivate(tx) == + /\ Live(tx) + /\ transactions[tx].state = "Active" + /\ IF Len(transactions[tx].requests) = 0 + THEN transactions' = [transactions EXCEPT ![tx].state = "Finished"] + ELSE transactions' = [transactions EXCEPT ![tx].state = "Inactive"] + /\ UNCHANGED <> + +\* +\* +\* "An explicit call to commit() will initiate a +\* transaction/commit" and "When committing, the transaction state is set to +\* committing". +Commit(tx) == + /\ IsCreated(tx) + /\ transactions[tx].state \notin {"None", "Committing", "Finished"} + /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] + /\ UNCHANGED <> + +CommitDone(tx) == + \* Spec: Transaction lifecycle. + \* + \* + \* "When a transaction is committed or aborted, its state is + \* set to finished". + /\ transactions[tx].state = "Committing" + /\ transactions' = [transactions EXCEPT ![tx].state = "Finished"] + /\ IF transactions[tx].mode = "versionchange" + THEN + /\ connections' = [connections EXCEPT ![transactions[tx].conn].pendingUpgrade = FALSE] + \* Dequeue the corresponding open request once the upgrade tx finishes. + \* This models "Wait for transaction to finish" in the upgrade algorithm: + \* + /\ connection_queue' = Tail(connection_queue) + ELSE + /\ connections' = connections + /\ connection_queue' = connection_queue + /\ UNCHANGED <> + +\* +\* +\* "A transaction can be aborted at any time before it is +\* finished". +Abort(tx) == + /\ IsCreated(tx) + /\ transactions[tx].state \notin {"None", "Finished"} + /\ transactions' = [transactions EXCEPT + ![tx].state = "Finished", + ![tx].requests = <<>> + ] + /\ IF transactions[tx].mode = "versionchange" + THEN + /\ connections' = [connections EXCEPT ![transactions[tx].conn].pendingUpgrade = FALSE] + \* Dequeue the corresponding open request once the upgrade tx finishes. + \* This models "Wait for transaction to finish" in the upgrade algorithm: + \* + /\ connection_queue' = Tail(connection_queue) + ELSE + /\ connections' = connections + /\ connection_queue' = connection_queue + /\ UNCHANGED <> + +\* +\* +\* +\* createObjectStore/deleteObjectStore "Throws +\* InvalidStateError if not called within an upgrade transaction" and require +\* the upgrade transaction to be active. +CreateStore(tx, s) == + /\ Live(tx) + /\ CanStart(tx) + /\ ConnOpen(transactions[tx].conn) + /\ transactions[tx].mode = "versionchange" + /\ transactions[tx].state = "Active" + /\ ~stores[s] + /\ stores' = [stores EXCEPT ![s] = TRUE] + /\ UNCHANGED <> + +\* +\* +\* +\* deleteObjectStore "Throws InvalidStateError if not called within an upgrade +\* transaction" and requires the upgrade transaction to be active. +DeleteStore(tx, s) == + /\ Live(tx) + /\ CanStart(tx) + /\ ConnOpen(transactions[tx].conn) + /\ transactions[tx].mode = "versionchange" + /\ transactions[tx].state = "Active" + /\ stores[s] + /\ stores' = [stores EXCEPT ![s] = FALSE] + /\ UNCHANGED <> + +\* When everything is done, allow infinite stuttering. +AllDone == + /\ \A tx \in Transactions: transactions[tx].state \in {"None", "Finished"} + /\ UNCHANGED Vars + +Next == + \/ \E c \in Connections, v \in Versions: OpenConnection(c, v) + \/ \E c \in Connections: FinishOpenConnection(c) + \/ \E c \in Connections: CloseConnection(c) + \/ \E tx \in Transactions: + (\/ \E c \in Connections: CreateUpgradeTransaction(tx, c) + \/ \E c \in Connections, m \in {"readonly", "readwrite"}, scope \in SUBSET Stores: + CreateTransaction(tx, c, m, scope) + \/ \E r \in Requests: AddRequest(tx, r) + \/ ProcessRequest(tx) + \/ Deactivate(tx) + \/ Commit(tx) + \/ CommitDone(tx) + \/ Abort(tx) + \/ \E s \in Stores: (CreateStore(tx, s) \/ DeleteStore(tx, s))) + \/ AllDone + +Spec == Init /\ [][Next]_Vars + +==== From 99aa7f6c596ef4e4897d2882f3b9f5ebec8838cc Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Sat, 3 Jan 2026 19:40:44 +0700 Subject: [PATCH 02/23] second pass on spec Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.cfg | 11 ++- transaction_lifecycle.tla | 189 ++++++++++++++++++++++---------------- 2 files changed, 118 insertions(+), 82 deletions(-) diff --git a/transaction_lifecycle.cfg b/transaction_lifecycle.cfg index b1b8db16..514153b2 100644 --- a/transaction_lifecycle.cfg +++ b/transaction_lifecycle.cfg @@ -1,9 +1,14 @@ SPECIFICATION Spec -CONSTANT N = 2 +CONSTANT Stores = {s1, s2} +CONSTANT Connections = {c1, c2} +CONSTANT Transactions = {0, 1, 2} +CONSTANT Versions = {0, 1, 2} INVARIANT TypeOK -INVARIANT NoTwoLiveUpgradeTxs -INVARIANT ActiveUpgradeTxImpliesConnOpenAndHead +INVARIANT UpgradeTxExcludesOtherLiveTxs +INVARIANT ActiveUpgradeTxImpliesExclusiveConn + +SYMMETRY Symmetry diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 30ce5e26..34631ac1 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -1,40 +1,37 @@ ------------------------------ MODULE transaction_lifecycle ------------------------------ -EXTENDS Naturals, Sequences, FiniteSets +EXTENDS Naturals, Sequences, FiniteSets, TLC -CONSTANT N -VARIABLES transactions, clock, stores, connections, dbVersion, connection_queue +CONSTANTS Stores, Connections, Transactions, Versions +VARIABLES transactions, stores, pending_stores, connections, dbVersion, connection_queue \* TLA+ model of the transaction lifecycle and scheduling rules from: \* - \* - -Stores == 0..N -Transactions == 0..N -Requests == 0..N -Connections == 0..N -Versions == 0..N - \* Note: by using only a single dbVersion, we do not model multiple databases. -Vars == << transactions, clock, stores, connections, dbVersion, connection_queue >> +Vars == << transactions, stores, pending_stores, connections, dbVersion, connection_queue >> Modes == {"readonly", "readwrite", "versionchange"} TxStates == {"None", "Active", "Inactive", "Committing", "Finished"} TypeOK == - /\ clock \in Nat /\ stores \in [Stores -> BOOLEAN] + /\ pending_stores \in [Stores -> BOOLEAN] /\ dbVersion \in Versions /\ connections \in [Connections -> [ open : BOOLEAN, pendingUpgrade : BOOLEAN, - requestedVersion: Versions ]] + requestedVersion: Versions, + closed : BOOLEAN ]] /\ connection_queue \in Seq(Connections) /\ transactions \in [Transactions -> [ conn : Connections, mode : Modes, stores : SUBSET Stores, - requests : Seq(Requests), - state : TxStates, - createdAt : Nat ]] + \* We model requests as a simple boolean flag indicating pending work. + \* We abstract away the actual list of requests and their side effects on stores + \* because the goal of this spec is to model the concurrency of the transaction lifecycle only. + requests : BOOLEAN, + state : TxStates ]] IsCreated(tx) == transactions[tx].state # "None" @@ -42,7 +39,13 @@ Live(tx) == IsCreated(tx) /\ transactions[tx].state # "Finished" Overlaps(tx1, tx2) == (transactions[tx1].stores \cap transactions[tx2].stores) # {} -CreatedBefore(tx1, tx2) == transactions[tx1].createdAt < transactions[tx2].createdAt +\* Since we allocate transaction IDs in increasing order (using Min), +\* the ID itself serves as a logical clock for creation time. +CreatedBefore(tx1, tx2) == tx1 < tx2 + +Min(S) == CHOOSE x \in S : \A y \in S : x <= y + +Symmetry == Permutations(Stores) \cup Permutations(Connections) ConnOpen(c) == connections[c].open @@ -60,21 +63,25 @@ HasLiveUpgradeTx(c) == /\ transactions[tx].conn = c /\ transactions[tx].mode = "versionchange" -\* Safety property: at most one upgrade transaction is live at a time. -NoTwoLiveUpgradeTxs == - Cardinality({ tx \in Transactions : Live(tx) /\ transactions[tx].mode = "versionchange" }) <= 1 +\* Safety property: A versionchange transaction being live excludes any other live transaction. +UpgradeTxExcludesOtherLiveTxs == + \A tx1 \in Transactions: + (Live(tx1) /\ transactions[tx1].mode = "versionchange") + => \A tx2 \in Transactions: Live(tx2) => (tx1 = tx2) -\* Inductive invariants that implies NoTwoLiveUpgradeTxs. +\* Inductive invariant that implies UpgradeTxExcludesOtherLiveTxs. \* -\* If a versionchange transaction is live, then its connection is open and -\* is at the head of the connection queue. -ActiveUpgradeTxImpliesConnOpenAndHead == +\* If a versionchange transaction is live, then: +\* 1. Its connection is open and is at the head of the connection queue. +\* 2. All other connections are closed. +ActiveUpgradeTxImpliesExclusiveConn == \A tx \in Transactions: (Live(tx) /\ transactions[tx].mode = "versionchange") => /\ ConnOpen(transactions[tx].conn) /\ Len(connection_queue) > 0 /\ Head(connection_queue) = transactions[tx].conn + /\ \A c \in Connections: ConnOpen(c) => c = transactions[tx].conn \* . CanStart(tx) == @@ -95,22 +102,22 @@ CanStart(tx) == ----------------------------------------------------------------------------------------- DefaultTx == - [ conn |-> 0, + [ conn |-> CHOOSE c \in Connections : TRUE, mode |-> "readonly", stores |-> {}, - requests |-> <<>>, - state |-> "None", - createdAt |-> 0 ] + requests |-> FALSE, + state |-> "None" ] DefaultConn == [ open |-> FALSE, pendingUpgrade |-> FALSE, - requestedVersion|-> 0 ] + requestedVersion|-> 0, + closed |-> FALSE ] Init == /\ transactions = [tx \in Transactions |-> DefaultTx] - /\ clock = 0 /\ stores = [s \in Stores |-> FALSE] + /\ pending_stores = [s \in Stores |-> FALSE] /\ connections = [c \in Connections |-> DefaultConn] /\ dbVersion = 0 /\ connection_queue = <<>> @@ -119,13 +126,15 @@ Init == OpenConnection(c, requestedVersion) == /\ dbVersion <= requestedVersion /\ connections[c] = DefaultConn + /\ ~connections[c].closed /\ connections' = [connections EXCEPT ![c] = [open |-> FALSE, pendingUpgrade |-> (requestedVersion > dbVersion), - requestedVersion|-> requestedVersion] + requestedVersion|-> requestedVersion, + closed |-> FALSE] ] /\ connection_queue' = Append(connection_queue, c) - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -139,33 +148,34 @@ FinishOpenConnection(c) == /\ connections[c].requestedVersion = dbVersion /\ connections' = [connections EXCEPT ![c].open = TRUE] /\ connection_queue' = Tail(connection_queue) - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* When all other connections are closed, and this connection is at the head of queue, \* create and start the ugrade transaction. \* The connection is removed from the queue when the transaction is finished. \* See `Abort` and `CommitDone`. -CreateUpgradeTransaction(tx, c) == +CreateUpgradeTransaction(c) == + LET freeTxs == { t \in Transactions : ~IsCreated(t) } IN /\ Len(connection_queue) > 0 /\ c = Head(connection_queue) /\ ConnPendingUpgrade(c) /\ ~ConnOpen(c) /\ \A other \in (Connections \ {c}): ~ConnOpen(other) - /\ ~IsCreated(tx) - /\ transactions' = [transactions EXCEPT + /\ freeTxs # {} + /\ LET tx == Min(freeTxs) IN + /\ transactions' = [transactions EXCEPT ![tx] = [conn |-> c, mode |-> "versionchange", stores |-> { s \in Stores : stores[s] }, - requests |-> <<>>, - state |-> "Active", - createdAt |-> clock] + requests |-> FALSE, + state |-> "Active"] ] /\ connections' = [connections EXCEPT ![c].open = TRUE ] /\ dbVersion' = connections[c].requestedVersion - /\ clock' = clock + 1 + /\ pending_stores' = stores /\ UNCHANGED <> \* @@ -177,39 +187,41 @@ CreateUpgradeTransaction(tx, c) == CloseConnection(c) == /\ ConnOpen(c) /\ AllTxFinishedForConn(c) - /\ connections' = [connections EXCEPT ![c].open = FALSE] - /\ UNCHANGED <> + /\ connections' = [connections EXCEPT + ![c].open = FALSE, + ![c].closed = TRUE] + /\ UNCHANGED <> \* -CreateTransaction(tx, c, mode, scope) == - /\ ~IsCreated(tx) +CreateTransaction(c, mode, scope) == + LET freeTxs == { t \in Transactions : ~IsCreated(t) } IN + /\ freeTxs # {} /\ ConnOpen(c) \* If a live upgrade transaction is associated with the connection, throw /\ ~HasLiveUpgradeTx(c) /\ \A s \in scope: stores[s] - /\ transactions' = [transactions EXCEPT + /\ LET tx == Min(freeTxs) IN + /\ transactions' = [transactions EXCEPT ![tx] = [conn |-> c, mode |-> mode, stores |-> scope, - requests |-> <<>>, - state |-> "Active", - createdAt |-> clock] + requests |-> FALSE, + state |-> "Active"] ] - /\ clock' = clock + 1 - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* \* "New requests can be made against the transaction when it is \* in [active]" and "The implementation must allow requests to be placed \* against the transaction whenever it is active". -AddRequest(tx, r) == +AddRequest(tx) == /\ Live(tx) /\ ConnOpen(transactions[tx].conn) /\ transactions[tx].state = "Active" - /\ Len(transactions[tx].requests) < N - /\ transactions' = [transactions EXCEPT ![tx].requests = Append(@, r)] - /\ UNCHANGED <> + /\ ~transactions[tx].requests + /\ transactions' = [transactions EXCEPT ![tx].requests = TRUE] + /\ UNCHANGED <> \* \* @@ -220,13 +232,13 @@ ProcessRequest(tx) == /\ Live(tx) /\ CanStart(tx) /\ ConnOpen(transactions[tx].conn) - /\ transactions[tx].state \in {"Active", "Inactive", "Committing"} - /\ Len(transactions[tx].requests) > 0 + /\ transactions[tx].state \in {"Active", "Inactive"} + /\ transactions[tx].requests /\ transactions' = [transactions EXCEPT - ![tx].requests = Tail(@), + ![tx].requests = FALSE, ![tx].state = "Active" ] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -240,10 +252,20 @@ ProcessRequest(tx) == Deactivate(tx) == /\ Live(tx) /\ transactions[tx].state = "Active" - /\ IF Len(transactions[tx].requests) = 0 - THEN transactions' = [transactions EXCEPT ![tx].state = "Finished"] - ELSE transactions' = [transactions EXCEPT ![tx].state = "Inactive"] - /\ UNCHANGED <> + /\ transactions' = [transactions EXCEPT ![tx].state = "Inactive"] + /\ UNCHANGED <> + +\* +\* +\* "The implementation must attempt to commit an inactive transaction +\* when all requests placed against the transaction have completed... +\* and no new requests have been placed against the transaction". +AutoCommit(tx) == + /\ Live(tx) + /\ transactions[tx].state = "Inactive" + /\ ~transactions[tx].requests + /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] + /\ UNCHANGED <> \* \* @@ -254,7 +276,7 @@ Commit(tx) == /\ IsCreated(tx) /\ transactions[tx].state \notin {"None", "Committing", "Finished"} /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] - /\ UNCHANGED <> + /\ UNCHANGED <> CommitDone(tx) == \* Spec: Transaction lifecycle. @@ -262,8 +284,13 @@ CommitDone(tx) == \* \* "When a transaction is committed or aborted, its state is \* set to finished". + \* + \* Note: The commit/abort logic is only applied to store operations (CreateStore/DeleteStore) + \* for now. We do not model data operations or their side effects/rollback, as it would + \* make the spec significantly more complicated without adding much value to the + \* transaction lifecycle concurrency model. /\ transactions[tx].state = "Committing" - /\ transactions' = [transactions EXCEPT ![tx].state = "Finished"] + /\ transactions' = [transactions EXCEPT ![tx] = [DefaultTx EXCEPT !.state = "Finished"]] /\ IF transactions[tx].mode = "versionchange" THEN /\ connections' = [connections EXCEPT ![transactions[tx].conn].pendingUpgrade = FALSE] @@ -271,10 +298,13 @@ CommitDone(tx) == \* This models "Wait for transaction to finish" in the upgrade algorithm: \* /\ connection_queue' = Tail(connection_queue) + /\ stores' = pending_stores + /\ UNCHANGED pending_stores ELSE /\ connections' = connections /\ connection_queue' = connection_queue - /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -283,10 +313,7 @@ CommitDone(tx) == Abort(tx) == /\ IsCreated(tx) /\ transactions[tx].state \notin {"None", "Finished"} - /\ transactions' = [transactions EXCEPT - ![tx].state = "Finished", - ![tx].requests = <<>> - ] + /\ transactions' = [transactions EXCEPT ![tx] = [DefaultTx EXCEPT !.state = "Finished"]] /\ IF transactions[tx].mode = "versionchange" THEN /\ connections' = [connections EXCEPT ![transactions[tx].conn].pendingUpgrade = FALSE] @@ -294,10 +321,13 @@ Abort(tx) == \* This models "Wait for transaction to finish" in the upgrade algorithm: \* /\ connection_queue' = Tail(connection_queue) + /\ pending_stores' = stores + /\ UNCHANGED stores ELSE /\ connections' = connections /\ connection_queue' = connection_queue - /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -311,9 +341,9 @@ CreateStore(tx, s) == /\ ConnOpen(transactions[tx].conn) /\ transactions[tx].mode = "versionchange" /\ transactions[tx].state = "Active" - /\ ~stores[s] - /\ stores' = [stores EXCEPT ![s] = TRUE] - /\ UNCHANGED <> + /\ ~pending_stores[s] + /\ pending_stores' = [pending_stores EXCEPT ![s] = TRUE] + /\ UNCHANGED <> \* \* @@ -326,9 +356,9 @@ DeleteStore(tx, s) == /\ ConnOpen(transactions[tx].conn) /\ transactions[tx].mode = "versionchange" /\ transactions[tx].state = "Active" - /\ stores[s] - /\ stores' = [stores EXCEPT ![s] = FALSE] - /\ UNCHANGED <> + /\ pending_stores[s] + /\ pending_stores' = [pending_stores EXCEPT ![s] = FALSE] + /\ UNCHANGED <> \* When everything is done, allow infinite stuttering. AllDone == @@ -339,13 +369,14 @@ Next == \/ \E c \in Connections, v \in Versions: OpenConnection(c, v) \/ \E c \in Connections: FinishOpenConnection(c) \/ \E c \in Connections: CloseConnection(c) + \/ \E c \in Connections: CreateUpgradeTransaction(c) + \/ \E c \in Connections, m \in {"readonly", "readwrite"}, scope \in SUBSET Stores: + CreateTransaction(c, m, scope) \/ \E tx \in Transactions: - (\/ \E c \in Connections: CreateUpgradeTransaction(tx, c) - \/ \E c \in Connections, m \in {"readonly", "readwrite"}, scope \in SUBSET Stores: - CreateTransaction(tx, c, m, scope) - \/ \E r \in Requests: AddRequest(tx, r) + (\/ AddRequest(tx) \/ ProcessRequest(tx) \/ Deactivate(tx) + \/ AutoCommit(tx) \/ Commit(tx) \/ CommitDone(tx) \/ Abort(tx) From 5c42022877e8cf0aacbf9a5d1c6d1af6e00ee4dd Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Sat, 3 Jan 2026 19:56:52 +0700 Subject: [PATCH 03/23] third pass: add invariant for request only processed when can start Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.cfg | 1 + transaction_lifecycle.tla | 13 +++++++++++++ 2 files changed, 14 insertions(+) diff --git a/transaction_lifecycle.cfg b/transaction_lifecycle.cfg index 514153b2..7db9bd6d 100644 --- a/transaction_lifecycle.cfg +++ b/transaction_lifecycle.cfg @@ -8,6 +8,7 @@ CONSTANT Versions = {0, 1, 2} INVARIANT TypeOK INVARIANT UpgradeTxExcludesOtherLiveTxs INVARIANT ActiveUpgradeTxImpliesExclusiveConn +INVARIANT ProcessedRequestsImpliesStarted SYMMETRY Symmetry diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 34631ac1..5669fd19 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -31,6 +31,10 @@ TypeOK == \* We abstract away the actual list of requests and their side effects on stores \* because the goal of this spec is to model the concurrency of the transaction lifecycle only. requests : BOOLEAN, + \* A counter of requests that have been processed. + \* Used to verify the invariant that a transaction must satisfy CanStart + \* before it processes any requests. + processed_requests : Nat, state : TxStates ]] IsCreated(tx) == transactions[tx].state # "None" @@ -99,6 +103,11 @@ CanStart(tx) == /\ Overlaps(other, tx) ELSE \* versionchange transactions can always start. TRUE + +\* Invariant: If a transaction has processed requests, it must have been able to start. +ProcessedRequestsImpliesStarted == + \A tx \in Transactions: + (transactions[tx].processed_requests > 0) => CanStart(tx) ----------------------------------------------------------------------------------------- DefaultTx == @@ -106,6 +115,7 @@ DefaultTx == mode |-> "readonly", stores |-> {}, requests |-> FALSE, + processed_requests |-> 0, state |-> "None" ] DefaultConn == @@ -169,6 +179,7 @@ CreateUpgradeTransaction(c) == mode |-> "versionchange", stores |-> { s \in Stores : stores[s] }, requests |-> FALSE, + processed_requests |-> 0, state |-> "Active"] ] /\ connections' = [connections EXCEPT @@ -206,6 +217,7 @@ CreateTransaction(c, mode, scope) == mode |-> mode, stores |-> scope, requests |-> FALSE, + processed_requests |-> 0, state |-> "Active"] ] /\ UNCHANGED <> @@ -236,6 +248,7 @@ ProcessRequest(tx) == /\ transactions[tx].requests /\ transactions' = [transactions EXCEPT ![tx].requests = FALSE, + ![tx].processed_requests = transactions[tx].processed_requests + 1, ![tx].state = "Active" ] /\ UNCHANGED <> From 4d6dedc123c91d78f5504735ae38570dcfa2711e Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Sun, 4 Jan 2026 23:40:08 +0700 Subject: [PATCH 04/23] remove tabs Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 478 +++++++++++++++++++------------------- 1 file changed, 239 insertions(+), 239 deletions(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 5669fd19..c5072379 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -14,28 +14,28 @@ Modes == {"readonly", "readwrite", "versionchange"} TxStates == {"None", "Active", "Inactive", "Committing", "Finished"} TypeOK == - /\ stores \in [Stores -> BOOLEAN] - /\ pending_stores \in [Stores -> BOOLEAN] - /\ dbVersion \in Versions - /\ connections \in [Connections -> - [ open : BOOLEAN, - pendingUpgrade : BOOLEAN, - requestedVersion: Versions, - closed : BOOLEAN ]] - /\ connection_queue \in Seq(Connections) - /\ transactions \in [Transactions -> - [ conn : Connections, - mode : Modes, - stores : SUBSET Stores, - \* We model requests as a simple boolean flag indicating pending work. - \* We abstract away the actual list of requests and their side effects on stores - \* because the goal of this spec is to model the concurrency of the transaction lifecycle only. - requests : BOOLEAN, - \* A counter of requests that have been processed. - \* Used to verify the invariant that a transaction must satisfy CanStart - \* before it processes any requests. - processed_requests : Nat, - state : TxStates ]] + /\ stores \in [Stores -> BOOLEAN] + /\ pending_stores \in [Stores -> BOOLEAN] + /\ dbVersion \in Versions + /\ connections \in [Connections -> + [open: BOOLEAN, + pendingUpgrade: BOOLEAN, + requestedVersion: Versions, + closed: BOOLEAN ]] + /\ connection_queue \in Seq(Connections) + /\ transactions \in [Transactions -> + [conn: Connections, + mode: Modes, + stores: SUBSET Stores, + \* We model requests as a simple boolean flag indicating pending work. + \* We abstract away the actual list of requests and their side effects on stores + \* because the goal of this spec is to model the concurrency of the transaction lifecycle only. + requests : BOOLEAN, + \* A counter of requests that have been processed. + \* Used to verify the invariant that a transaction must satisfy CanStart + \* before it processes any requests. + processed_requests: Nat, + state: TxStates ]] IsCreated(tx) == transactions[tx].state # "None" @@ -58,20 +58,20 @@ ConnPendingUpgrade(c) == connections[c].pendingUpgrade TxForConn(c) == { tx \in Transactions : Live(tx) /\ transactions[tx].conn = c } AllTxFinishedForConn(c) == - \A tx \in Transactions: - (transactions[tx].conn = c) => (transactions[tx].state \in {"None", "Finished"}) + \A tx \in Transactions: + (transactions[tx].conn = c) => (transactions[tx].state \in {"None", "Finished"}) HasLiveUpgradeTx(c) == - \E tx \in Transactions: - /\ Live(tx) - /\ transactions[tx].conn = c - /\ transactions[tx].mode = "versionchange" + \E tx \in Transactions: + /\ Live(tx) + /\ transactions[tx].conn = c + /\ transactions[tx].mode = "versionchange" \* Safety property: A versionchange transaction being live excludes any other live transaction. UpgradeTxExcludesOtherLiveTxs == - \A tx1 \in Transactions: - (Live(tx1) /\ transactions[tx1].mode = "versionchange") - => \A tx2 \in Transactions: Live(tx2) => (tx1 = tx2) + \A tx1 \in Transactions: + (Live(tx1) /\ transactions[tx1].mode = "versionchange") + => \A tx2 \in Transactions: Live(tx2) => (tx1 = tx2) \* Inductive invariant that implies UpgradeTxExcludesOtherLiveTxs. \* @@ -79,86 +79,86 @@ UpgradeTxExcludesOtherLiveTxs == \* 1. Its connection is open and is at the head of the connection queue. \* 2. All other connections are closed. ActiveUpgradeTxImpliesExclusiveConn == - \A tx \in Transactions: - (Live(tx) /\ transactions[tx].mode = "versionchange") - => - /\ ConnOpen(transactions[tx].conn) - /\ Len(connection_queue) > 0 - /\ Head(connection_queue) = transactions[tx].conn - /\ \A c \in Connections: ConnOpen(c) => c = transactions[tx].conn + \A tx \in Transactions: + (Live(tx) /\ transactions[tx].mode = "versionchange") + => + /\ ConnOpen(transactions[tx].conn) + /\ Len(connection_queue) > 0 + /\ Head(connection_queue) = transactions[tx].conn + /\ \A c \in Connections: ConnOpen(c) => c = transactions[tx].conn \* . CanStart(tx) == - LET m == transactions[tx].mode IN - IF m = "readonly" THEN - ~\E other \in (Transactions \ {tx}): - /\ Live(other) - /\ transactions[other].mode = "readwrite" - /\ CreatedBefore(other, tx) - /\ Overlaps(other, tx) - ELSE IF m = "readwrite" THEN - ~\E other \in (Transactions \ {tx}): - /\ Live(other) - /\ CreatedBefore(other, tx) - /\ Overlaps(other, tx) - ELSE \* versionchange transactions can always start. - TRUE + LET m == transactions[tx].mode IN + IF m = "readonly" THEN + ~\E other \in (Transactions \ {tx}): + /\ Live(other) + /\ transactions[other].mode = "readwrite" + /\ CreatedBefore(other, tx) + /\ Overlaps(other, tx) + ELSE IF m = "readwrite" THEN + ~\E other \in (Transactions \ {tx}): + /\ Live(other) + /\ CreatedBefore(other, tx) + /\ Overlaps(other, tx) + ELSE \* versionchange transactions can always start. + TRUE \* Invariant: If a transaction has processed requests, it must have been able to start. ProcessedRequestsImpliesStarted == - \A tx \in Transactions: - (transactions[tx].processed_requests > 0) => CanStart(tx) + \A tx \in Transactions: + (transactions[tx].processed_requests > 0) => CanStart(tx) ----------------------------------------------------------------------------------------- DefaultTx == - [ conn |-> CHOOSE c \in Connections : TRUE, - mode |-> "readonly", - stores |-> {}, - requests |-> FALSE, - processed_requests |-> 0, - state |-> "None" ] + [ conn |-> CHOOSE c \in Connections : TRUE, + mode |-> "readonly", + stores |-> {}, + requests |-> FALSE, + processed_requests |-> 0, + state |-> "None" ] DefaultConn == - [ open |-> FALSE, - pendingUpgrade |-> FALSE, - requestedVersion|-> 0, - closed |-> FALSE ] + [ open |-> FALSE, + pendingUpgrade |-> FALSE, + requestedVersion|-> 0, + closed |-> FALSE ] Init == - /\ transactions = [tx \in Transactions |-> DefaultTx] - /\ stores = [s \in Stores |-> FALSE] - /\ pending_stores = [s \in Stores |-> FALSE] - /\ connections = [c \in Connections |-> DefaultConn] - /\ dbVersion = 0 - /\ connection_queue = <<>> + /\ transactions = [tx \in Transactions |-> DefaultTx] + /\ stores = [s \in Stores |-> FALSE] + /\ pending_stores = [s \in Stores |-> FALSE] + /\ connections = [c \in Connections |-> DefaultConn] + /\ dbVersion = 0 + /\ connection_queue = <<>> \* OpenConnection(c, requestedVersion) == - /\ dbVersion <= requestedVersion - /\ connections[c] = DefaultConn - /\ ~connections[c].closed - /\ connections' = [connections EXCEPT - ![c] = [open |-> FALSE, - pendingUpgrade |-> (requestedVersion > dbVersion), - requestedVersion|-> requestedVersion, - closed |-> FALSE] - ] - /\ connection_queue' = Append(connection_queue, c) - /\ UNCHANGED <> + /\ dbVersion <= requestedVersion + /\ connections[c] = DefaultConn + /\ ~connections[c].closed + /\ connections' = [connections EXCEPT + ![c] = [open |-> FALSE, + pendingUpgrade |-> (requestedVersion > dbVersion), + requestedVersion|-> requestedVersion, + closed |-> FALSE] + ] + /\ connection_queue' = Append(connection_queue, c) + /\ UNCHANGED <> \* \* \* Note: A non-upgrade open request can be processed once it reaches the head \* of the queue. FinishOpenConnection(c) == - /\ Len(connection_queue) > 0 - /\ c = Head(connection_queue) - /\ ~ConnPendingUpgrade(c) - /\ ~ConnOpen(c) - /\ connections[c].requestedVersion = dbVersion - /\ connections' = [connections EXCEPT ![c].open = TRUE] - /\ connection_queue' = Tail(connection_queue) - /\ UNCHANGED <> + /\ Len(connection_queue) > 0 + /\ c = Head(connection_queue) + /\ ~ConnPendingUpgrade(c) + /\ ~ConnOpen(c) + /\ connections[c].requestedVersion = dbVersion + /\ connections' = [connections EXCEPT ![c].open = TRUE] + /\ connection_queue' = Tail(connection_queue) + /\ UNCHANGED <> \* \* When all other connections are closed, and this connection is at the head of queue, @@ -166,28 +166,28 @@ FinishOpenConnection(c) == \* The connection is removed from the queue when the transaction is finished. \* See `Abort` and `CommitDone`. CreateUpgradeTransaction(c) == - LET freeTxs == { t \in Transactions : ~IsCreated(t) } IN - /\ Len(connection_queue) > 0 - /\ c = Head(connection_queue) - /\ ConnPendingUpgrade(c) - /\ ~ConnOpen(c) - /\ \A other \in (Connections \ {c}): ~ConnOpen(other) - /\ freeTxs # {} - /\ LET tx == Min(freeTxs) IN - /\ transactions' = [transactions EXCEPT - ![tx] = [conn |-> c, - mode |-> "versionchange", - stores |-> { s \in Stores : stores[s] }, - requests |-> FALSE, - processed_requests |-> 0, - state |-> "Active"] - ] - /\ connections' = [connections EXCEPT - ![c].open = TRUE - ] - /\ dbVersion' = connections[c].requestedVersion - /\ pending_stores' = stores - /\ UNCHANGED <> + LET freeTxs == { t \in Transactions : ~IsCreated(t) } IN + /\ Len(connection_queue) > 0 + /\ c = Head(connection_queue) + /\ ConnPendingUpgrade(c) + /\ ~ConnOpen(c) + /\ \A other \in (Connections \ {c}): ~ConnOpen(other) + /\ freeTxs # {} + /\ LET tx == Min(freeTxs) IN + /\ transactions' = [transactions EXCEPT + ![tx] = [conn |-> c, + mode |-> "versionchange", + stores |-> { s \in Stores : stores[s] }, + requests |-> FALSE, + processed_requests |-> 0, + state |-> "Active"] + ] + /\ connections' = [connections EXCEPT + ![c].open = TRUE + ] + /\ dbVersion' = connections[c].requestedVersion + /\ pending_stores' = stores + /\ UNCHANGED <> \* \* @@ -196,31 +196,31 @@ CreateUpgradeTransaction(c) == \* \* Note: forced close is not modeled right now. CloseConnection(c) == - /\ ConnOpen(c) - /\ AllTxFinishedForConn(c) - /\ connections' = [connections EXCEPT - ![c].open = FALSE, - ![c].closed = TRUE] - /\ UNCHANGED <> + /\ ConnOpen(c) + /\ AllTxFinishedForConn(c) + /\ connections' = [connections EXCEPT + ![c].open = FALSE, + ![c].closed = TRUE] + /\ UNCHANGED <> \* CreateTransaction(c, mode, scope) == - LET freeTxs == { t \in Transactions : ~IsCreated(t) } IN - /\ freeTxs # {} - /\ ConnOpen(c) + LET freeTxs == { t \in Transactions : ~IsCreated(t) } IN + /\ freeTxs # {} + /\ ConnOpen(c) \* If a live upgrade transaction is associated with the connection, throw - /\ ~HasLiveUpgradeTx(c) - /\ \A s \in scope: stores[s] - /\ LET tx == Min(freeTxs) IN - /\ transactions' = [transactions EXCEPT - ![tx] = [conn |-> c, - mode |-> mode, - stores |-> scope, - requests |-> FALSE, - processed_requests |-> 0, - state |-> "Active"] - ] - /\ UNCHANGED <> + /\ ~HasLiveUpgradeTx(c) + /\ \A s \in scope: stores[s] + /\ LET tx == Min(freeTxs) IN + /\ transactions' = [transactions EXCEPT + ![tx] = [conn |-> c, + mode |-> mode, + stores |-> scope, + requests |-> FALSE, + processed_requests |-> 0, + state |-> "Active"] + ] + /\ UNCHANGED <> \* \* @@ -228,12 +228,12 @@ CreateTransaction(c, mode, scope) == \* in [active]" and "The implementation must allow requests to be placed \* against the transaction whenever it is active". AddRequest(tx) == - /\ Live(tx) - /\ ConnOpen(transactions[tx].conn) - /\ transactions[tx].state = "Active" - /\ ~transactions[tx].requests - /\ transactions' = [transactions EXCEPT ![tx].requests = TRUE] - /\ UNCHANGED <> + /\ Live(tx) + /\ ConnOpen(transactions[tx].conn) + /\ transactions[tx].state = "Active" + /\ ~transactions[tx].requests + /\ transactions' = [transactions EXCEPT ![tx].requests = TRUE] + /\ UNCHANGED <> \* \* @@ -241,17 +241,17 @@ AddRequest(tx) == \* they were made" and "While the event is being dispatched, the transaction \* state is set to active". ProcessRequest(tx) == - /\ Live(tx) - /\ CanStart(tx) - /\ ConnOpen(transactions[tx].conn) - /\ transactions[tx].state \in {"Active", "Inactive"} - /\ transactions[tx].requests - /\ transactions' = [transactions EXCEPT - ![tx].requests = FALSE, - ![tx].processed_requests = transactions[tx].processed_requests + 1, - ![tx].state = "Active" - ] - /\ UNCHANGED <> + /\ Live(tx) + /\ CanStart(tx) + /\ ConnOpen(transactions[tx].conn) + /\ transactions[tx].state \in {"Active", "Inactive"} + /\ transactions[tx].requests + /\ transactions' = [transactions EXCEPT + ![tx].requests = FALSE, + ![tx].processed_requests = transactions[tx].processed_requests + 1, + ![tx].state = "Active" + ] + /\ UNCHANGED <> \* \* @@ -263,10 +263,10 @@ ProcessRequest(tx) == \* steps to make it easier to model adding any number of requests \* while the transaction is active. Deactivate(tx) == - /\ Live(tx) - /\ transactions[tx].state = "Active" - /\ transactions' = [transactions EXCEPT ![tx].state = "Inactive"] - /\ UNCHANGED <> + /\ Live(tx) + /\ transactions[tx].state = "Active" + /\ transactions' = [transactions EXCEPT ![tx].state = "Inactive"] + /\ UNCHANGED <> \* \* @@ -274,11 +274,11 @@ Deactivate(tx) == \* when all requests placed against the transaction have completed... \* and no new requests have been placed against the transaction". AutoCommit(tx) == - /\ Live(tx) - /\ transactions[tx].state = "Inactive" - /\ ~transactions[tx].requests - /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] - /\ UNCHANGED <> + /\ Live(tx) + /\ transactions[tx].state = "Inactive" + /\ ~transactions[tx].requests + /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] + /\ UNCHANGED <> \* \* @@ -286,61 +286,61 @@ AutoCommit(tx) == \* transaction/commit" and "When committing, the transaction state is set to \* committing". Commit(tx) == - /\ IsCreated(tx) - /\ transactions[tx].state \notin {"None", "Committing", "Finished"} - /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] - /\ UNCHANGED <> + /\ IsCreated(tx) + /\ transactions[tx].state \notin {"None", "Committing", "Finished"} + /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] + /\ UNCHANGED <> CommitDone(tx) == - \* Spec: Transaction lifecycle. - \* - \* - \* "When a transaction is committed or aborted, its state is - \* set to finished". - \* - \* Note: The commit/abort logic is only applied to store operations (CreateStore/DeleteStore) - \* for now. We do not model data operations or their side effects/rollback, as it would - \* make the spec significantly more complicated without adding much value to the - \* transaction lifecycle concurrency model. - /\ transactions[tx].state = "Committing" - /\ transactions' = [transactions EXCEPT ![tx] = [DefaultTx EXCEPT !.state = "Finished"]] - /\ IF transactions[tx].mode = "versionchange" - THEN - /\ connections' = [connections EXCEPT ![transactions[tx].conn].pendingUpgrade = FALSE] - \* Dequeue the corresponding open request once the upgrade tx finishes. - \* This models "Wait for transaction to finish" in the upgrade algorithm: - \* - /\ connection_queue' = Tail(connection_queue) - /\ stores' = pending_stores - /\ UNCHANGED pending_stores - ELSE - /\ connections' = connections - /\ connection_queue' = connection_queue - /\ UNCHANGED <> - /\ UNCHANGED <> + \* Spec: Transaction lifecycle. + \* + \* + \* "When a transaction is committed or aborted, its state is + \* set to finished". + \* + \* Note: The commit/abort logic is only applied to store operations (CreateStore/DeleteStore) + \* for now. We do not model data operations or their side effects/rollback, as it would + \* make the spec significantly more complicated without adding much value to the + \* transaction lifecycle concurrency model. + /\ transactions[tx].state = "Committing" + /\ transactions' = [transactions EXCEPT ![tx] = [DefaultTx EXCEPT !.state = "Finished"]] + /\ IF transactions[tx].mode = "versionchange" + THEN + /\ connections' = [connections EXCEPT ![transactions[tx].conn].pendingUpgrade = FALSE] + \* Dequeue the corresponding open request once the upgrade tx finishes. + \* This models "Wait for transaction to finish" in the upgrade algorithm: + \* + /\ connection_queue' = Tail(connection_queue) + /\ stores' = pending_stores + /\ UNCHANGED pending_stores + ELSE + /\ connections' = connections + /\ connection_queue' = connection_queue + /\ UNCHANGED <> + /\ UNCHANGED <> \* \* \* "A transaction can be aborted at any time before it is \* finished". Abort(tx) == - /\ IsCreated(tx) - /\ transactions[tx].state \notin {"None", "Finished"} - /\ transactions' = [transactions EXCEPT ![tx] = [DefaultTx EXCEPT !.state = "Finished"]] - /\ IF transactions[tx].mode = "versionchange" - THEN - /\ connections' = [connections EXCEPT ![transactions[tx].conn].pendingUpgrade = FALSE] - \* Dequeue the corresponding open request once the upgrade tx finishes. - \* This models "Wait for transaction to finish" in the upgrade algorithm: - \* - /\ connection_queue' = Tail(connection_queue) - /\ pending_stores' = stores - /\ UNCHANGED stores - ELSE - /\ connections' = connections - /\ connection_queue' = connection_queue - /\ UNCHANGED <> - /\ UNCHANGED <> + /\ IsCreated(tx) + /\ transactions[tx].state \notin {"None", "Finished"} + /\ transactions' = [transactions EXCEPT ![tx] = [DefaultTx EXCEPT !.state = "Finished"]] + /\ IF transactions[tx].mode = "versionchange" + THEN + /\ connections' = [connections EXCEPT ![transactions[tx].conn].pendingUpgrade = FALSE] + \* Dequeue the corresponding open request once the upgrade tx finishes. + \* This models "Wait for transaction to finish" in the upgrade algorithm: + \* + /\ connection_queue' = Tail(connection_queue) + /\ pending_stores' = stores + /\ UNCHANGED stores + ELSE + /\ connections' = connections + /\ connection_queue' = connection_queue + /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -349,14 +349,14 @@ Abort(tx) == \* InvalidStateError if not called within an upgrade transaction" and require \* the upgrade transaction to be active. CreateStore(tx, s) == - /\ Live(tx) - /\ CanStart(tx) - /\ ConnOpen(transactions[tx].conn) - /\ transactions[tx].mode = "versionchange" - /\ transactions[tx].state = "Active" - /\ ~pending_stores[s] - /\ pending_stores' = [pending_stores EXCEPT ![s] = TRUE] - /\ UNCHANGED <> + /\ Live(tx) + /\ CanStart(tx) + /\ ConnOpen(transactions[tx].conn) + /\ transactions[tx].mode = "versionchange" + /\ transactions[tx].state = "Active" + /\ ~pending_stores[s] + /\ pending_stores' = [pending_stores EXCEPT ![s] = TRUE] + /\ UNCHANGED <> \* \* @@ -364,37 +364,37 @@ CreateStore(tx, s) == \* deleteObjectStore "Throws InvalidStateError if not called within an upgrade \* transaction" and requires the upgrade transaction to be active. DeleteStore(tx, s) == - /\ Live(tx) - /\ CanStart(tx) - /\ ConnOpen(transactions[tx].conn) - /\ transactions[tx].mode = "versionchange" - /\ transactions[tx].state = "Active" - /\ pending_stores[s] - /\ pending_stores' = [pending_stores EXCEPT ![s] = FALSE] - /\ UNCHANGED <> + /\ Live(tx) + /\ CanStart(tx) + /\ ConnOpen(transactions[tx].conn) + /\ transactions[tx].mode = "versionchange" + /\ transactions[tx].state = "Active" + /\ pending_stores[s] + /\ pending_stores' = [pending_stores EXCEPT ![s] = FALSE] + /\ UNCHANGED <> \* When everything is done, allow infinite stuttering. AllDone == - /\ \A tx \in Transactions: transactions[tx].state \in {"None", "Finished"} - /\ UNCHANGED Vars + /\ \A tx \in Transactions: transactions[tx].state \in {"None", "Finished"} + /\ UNCHANGED Vars Next == - \/ \E c \in Connections, v \in Versions: OpenConnection(c, v) - \/ \E c \in Connections: FinishOpenConnection(c) - \/ \E c \in Connections: CloseConnection(c) - \/ \E c \in Connections: CreateUpgradeTransaction(c) - \/ \E c \in Connections, m \in {"readonly", "readwrite"}, scope \in SUBSET Stores: - CreateTransaction(c, m, scope) - \/ \E tx \in Transactions: - (\/ AddRequest(tx) - \/ ProcessRequest(tx) - \/ Deactivate(tx) - \/ AutoCommit(tx) - \/ Commit(tx) - \/ CommitDone(tx) - \/ Abort(tx) - \/ \E s \in Stores: (CreateStore(tx, s) \/ DeleteStore(tx, s))) - \/ AllDone + \/ \E c \in Connections, v \in Versions: OpenConnection(c, v) + \/ \E c \in Connections: FinishOpenConnection(c) + \/ \E c \in Connections: CloseConnection(c) + \/ \E c \in Connections: CreateUpgradeTransaction(c) + \/ \E c \in Connections, m \in {"readonly", "readwrite"}, scope \in SUBSET Stores: + CreateTransaction(c, m, scope) + \/ \E tx \in Transactions: + (\/ AddRequest(tx) + \/ ProcessRequest(tx) + \/ Deactivate(tx) + \/ AutoCommit(tx) + \/ Commit(tx) + \/ CommitDone(tx) + \/ Abort(tx) + \/ \E s \in Stores: (CreateStore(tx, s) \/ DeleteStore(tx, s))) + \/ AllDone Spec == Init /\ [][Next]_Vars From 7521621e04f194d1aef9bf91c177589be2d87beb Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 00:41:46 +0700 Subject: [PATCH 05/23] remove redundant pre-conditions; add docs Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 75 +++++++++++++++------------------------ 1 file changed, 29 insertions(+), 46 deletions(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index c5072379..76b66395 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -59,7 +59,7 @@ TxForConn(c) == { tx \in Transactions : Live(tx) /\ transactions[tx].conn = c } AllTxFinishedForConn(c) == \A tx \in Transactions: - (transactions[tx].conn = c) => (transactions[tx].state \in {"None", "Finished"}) + (transactions[tx].conn = c) => (transactions[tx].state = "Finished") HasLiveUpgradeTx(c) == \E tx \in Transactions: @@ -133,7 +133,7 @@ Init == /\ connection_queue = <<>> \* -OpenConnection(c, requestedVersion) == +StartOpenConnection(c, requestedVersion) == /\ dbVersion <= requestedVersion /\ connections[c] = DefaultConn /\ ~connections[c].closed @@ -154,27 +154,26 @@ FinishOpenConnection(c) == /\ Len(connection_queue) > 0 /\ c = Head(connection_queue) /\ ~ConnPendingUpgrade(c) - /\ ~ConnOpen(c) /\ connections[c].requestedVersion = dbVersion /\ connections' = [connections EXCEPT ![c].open = TRUE] /\ connection_queue' = Tail(connection_queue) /\ UNCHANGED <> -\* -\* When all other connections are closed, and this connection is at the head of queue, -\* create and start the ugrade transaction. -\* The connection is removed from the queue when the transaction is finished. -\* See `Abort` and `CommitDone`. +\* +\* Wait until all connections in openConnections are closed. +\* Run upgrade a database using connection, version and request. CreateUpgradeTransaction(c) == - LET freeTxs == { t \in Transactions : ~IsCreated(t) } IN + LET + freeTxs == { t \in Transactions : ~IsCreated(t) } + tx == Min(freeTxs) + IN /\ Len(connection_queue) > 0 + /\ ~ConnOpen(c) /\ c = Head(connection_queue) /\ ConnPendingUpgrade(c) - /\ ~ConnOpen(c) /\ \A other \in (Connections \ {c}): ~ConnOpen(other) /\ freeTxs # {} - /\ LET tx == Min(freeTxs) IN - /\ transactions' = [transactions EXCEPT + /\ transactions' = [transactions EXCEPT ![tx] = [conn |-> c, mode |-> "versionchange", stores |-> { s \in Stores : stores[s] }, @@ -193,8 +192,6 @@ CreateUpgradeTransaction(c) == \* \* "Wait for all transactions created using connection to complete. \* Once they are complete, connection is closed." -\* -\* Note: forced close is not modeled right now. CloseConnection(c) == /\ ConnOpen(c) /\ AllTxFinishedForConn(c) @@ -204,11 +201,12 @@ CloseConnection(c) == /\ UNCHANGED <> \* +\* If a live upgrade transaction is associated with the connection, throw +\* If this’s close pending flag is true, then throw. CreateTransaction(c, mode, scope) == LET freeTxs == { t \in Transactions : ~IsCreated(t) } IN /\ freeTxs # {} /\ ConnOpen(c) - \* If a live upgrade transaction is associated with the connection, throw /\ ~HasLiveUpgradeTx(c) /\ \A s \in scope: stores[s] /\ LET tx == Min(freeTxs) IN @@ -222,26 +220,21 @@ CreateTransaction(c, mode, scope) == ] /\ UNCHANGED <> -\* -\* -\* "New requests can be made against the transaction when it is -\* in [active]" and "The implementation must allow requests to be placed -\* against the transaction whenever it is active". +\* +\* Assert: transaction’s state is active. AddRequest(tx) == - /\ Live(tx) - /\ ConnOpen(transactions[tx].conn) /\ transactions[tx].state = "Active" /\ ~transactions[tx].requests /\ transactions' = [transactions EXCEPT ![tx].requests = TRUE] /\ UNCHANGED <> -\* +\* +\* +\* Set request’s processed flag to true. \* -\* "Requests must be executed in the order in which -\* they were made" and "While the event is being dispatched, the transaction -\* state is set to active". +\* Note: just modelling the presence of pending requests, +\* and counting processed requests(for the can start invariant). ProcessRequest(tx) == - /\ Live(tx) /\ CanStart(tx) /\ ConnOpen(transactions[tx].conn) /\ transactions[tx].state \in {"Active", "Inactive"} @@ -263,7 +256,6 @@ ProcessRequest(tx) == \* steps to make it easier to model adding any number of requests \* while the transaction is active. Deactivate(tx) == - /\ Live(tx) /\ transactions[tx].state = "Active" /\ transactions' = [transactions EXCEPT ![tx].state = "Inactive"] /\ UNCHANGED <> @@ -274,7 +266,6 @@ Deactivate(tx) == \* when all requests placed against the transaction have completed... \* and no new requests have been placed against the transaction". AutoCommit(tx) == - /\ Live(tx) /\ transactions[tx].state = "Inactive" /\ ~transactions[tx].requests /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] @@ -286,22 +277,19 @@ AutoCommit(tx) == \* transaction/commit" and "When committing, the transaction state is set to \* committing". Commit(tx) == - /\ IsCreated(tx) /\ transactions[tx].state \notin {"None", "Committing", "Finished"} /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] /\ UNCHANGED <> +\* +\* "When a transaction is committed or aborted, its state is +\* set to finished". +\* +\* Note: The commit/abort logic is only applied to store operations (CreateStore/DeleteStore) +\* for now. We do not model data operations or their side effects/rollback, as it would +\* make the spec significantly more complicated without adding much value to the +\* transaction lifecycle concurrency model. CommitDone(tx) == - \* Spec: Transaction lifecycle. - \* - \* - \* "When a transaction is committed or aborted, its state is - \* set to finished". - \* - \* Note: The commit/abort logic is only applied to store operations (CreateStore/DeleteStore) - \* for now. We do not model data operations or their side effects/rollback, as it would - \* make the spec significantly more complicated without adding much value to the - \* transaction lifecycle concurrency model. /\ transactions[tx].state = "Committing" /\ transactions' = [transactions EXCEPT ![tx] = [DefaultTx EXCEPT !.state = "Finished"]] /\ IF transactions[tx].mode = "versionchange" @@ -324,7 +312,6 @@ CommitDone(tx) == \* "A transaction can be aborted at any time before it is \* finished". Abort(tx) == - /\ IsCreated(tx) /\ transactions[tx].state \notin {"None", "Finished"} /\ transactions' = [transactions EXCEPT ![tx] = [DefaultTx EXCEPT !.state = "Finished"]] /\ IF transactions[tx].mode = "versionchange" @@ -349,9 +336,7 @@ Abort(tx) == \* InvalidStateError if not called within an upgrade transaction" and require \* the upgrade transaction to be active. CreateStore(tx, s) == - /\ Live(tx) /\ CanStart(tx) - /\ ConnOpen(transactions[tx].conn) /\ transactions[tx].mode = "versionchange" /\ transactions[tx].state = "Active" /\ ~pending_stores[s] @@ -364,9 +349,7 @@ CreateStore(tx, s) == \* deleteObjectStore "Throws InvalidStateError if not called within an upgrade \* transaction" and requires the upgrade transaction to be active. DeleteStore(tx, s) == - /\ Live(tx) /\ CanStart(tx) - /\ ConnOpen(transactions[tx].conn) /\ transactions[tx].mode = "versionchange" /\ transactions[tx].state = "Active" /\ pending_stores[s] @@ -379,7 +362,7 @@ AllDone == /\ UNCHANGED Vars Next == - \/ \E c \in Connections, v \in Versions: OpenConnection(c, v) + \/ \E c \in Connections, v \in Versions: StartOpenConnection(c, v) \/ \E c \in Connections: FinishOpenConnection(c) \/ \E c \in Connections: CloseConnection(c) \/ \E c \in Connections: CreateUpgradeTransaction(c) From 2221a0b7291719d52393704d53888b4388f39184 Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 01:05:17 +0700 Subject: [PATCH 06/23] simply start and finish of open Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 28 +++++++--------------------- 1 file changed, 7 insertions(+), 21 deletions(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 76b66395..2d89764d 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -133,6 +133,7 @@ Init == /\ connection_queue = <<>> \* +\* Wait until all previous requests in queue have been processed. StartOpenConnection(c, requestedVersion) == /\ dbVersion <= requestedVersion /\ connections[c] = DefaultConn @@ -147,15 +148,14 @@ StartOpenConnection(c, requestedVersion) == /\ UNCHANGED <> \* -\* -\* Note: A non-upgrade open request can be processed once it reaches the head -\* of the queue. FinishOpenConnection(c) == /\ Len(connection_queue) > 0 /\ c = Head(connection_queue) - /\ ~ConnPendingUpgrade(c) /\ connections[c].requestedVersion = dbVersion - /\ connections' = [connections EXCEPT ![c].open = TRUE] + \* + \* Wait for transaction to finish. + /\ ~HasLiveUpgradeTx(c) + /\ connections' = [connections EXCEPT ![c].open = TRUE, ![c].pendingUpgrade = FALSE] /\ connection_queue' = Tail(connection_queue) /\ UNCHANGED <> @@ -294,18 +294,11 @@ CommitDone(tx) == /\ transactions' = [transactions EXCEPT ![tx] = [DefaultTx EXCEPT !.state = "Finished"]] /\ IF transactions[tx].mode = "versionchange" THEN - /\ connections' = [connections EXCEPT ![transactions[tx].conn].pendingUpgrade = FALSE] - \* Dequeue the corresponding open request once the upgrade tx finishes. - \* This models "Wait for transaction to finish" in the upgrade algorithm: - \* - /\ connection_queue' = Tail(connection_queue) /\ stores' = pending_stores /\ UNCHANGED pending_stores ELSE - /\ connections' = connections - /\ connection_queue' = connection_queue /\ UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -316,18 +309,11 @@ Abort(tx) == /\ transactions' = [transactions EXCEPT ![tx] = [DefaultTx EXCEPT !.state = "Finished"]] /\ IF transactions[tx].mode = "versionchange" THEN - /\ connections' = [connections EXCEPT ![transactions[tx].conn].pendingUpgrade = FALSE] - \* Dequeue the corresponding open request once the upgrade tx finishes. - \* This models "Wait for transaction to finish" in the upgrade algorithm: - \* - /\ connection_queue' = Tail(connection_queue) /\ pending_stores' = stores /\ UNCHANGED stores ELSE - /\ connections' = connections - /\ connection_queue' = connection_queue /\ UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* From e72d28a0536f5f3812ec2c617e11ef3c872a7aa9 Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 01:28:19 +0700 Subject: [PATCH 07/23] fix deadlock in open flow following simplification Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 2d89764d..2940e8ca 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -198,7 +198,11 @@ CloseConnection(c) == /\ connections' = [connections EXCEPT ![c].open = FALSE, ![c].closed = TRUE] - /\ UNCHANGED <> + /\ transactions' = [tx \in Transactions |-> + IF transactions[tx].conn = c + THEN DefaultTx + ELSE transactions[tx]] + /\ UNCHANGED <> \* \* If a live upgrade transaction is associated with the connection, throw @@ -291,7 +295,7 @@ Commit(tx) == \* transaction lifecycle concurrency model. CommitDone(tx) == /\ transactions[tx].state = "Committing" - /\ transactions' = [transactions EXCEPT ![tx] = [DefaultTx EXCEPT !.state = "Finished"]] + /\ transactions' = [transactions EXCEPT ![tx].state = "Finished"] /\ IF transactions[tx].mode = "versionchange" THEN /\ stores' = pending_stores @@ -306,7 +310,7 @@ CommitDone(tx) == \* finished". Abort(tx) == /\ transactions[tx].state \notin {"None", "Finished"} - /\ transactions' = [transactions EXCEPT ![tx] = [DefaultTx EXCEPT !.state = "Finished"]] + /\ transactions' = [transactions EXCEPT ![tx].state = "Finished"] /\ IF transactions[tx].mode = "versionchange" THEN /\ pending_stores' = stores @@ -342,9 +346,9 @@ DeleteStore(tx, s) == /\ pending_stores' = [pending_stores EXCEPT ![s] = FALSE] /\ UNCHANGED <> -\* When everything is done, allow infinite stuttering. -AllDone == - /\ \A tx \in Transactions: transactions[tx].state \in {"None", "Finished"} +\* When all connections went through their open and close cyle: infinite stuttering. +AllClosed == + /\ \A c \in Connections: connections[c].closed /\ UNCHANGED Vars Next == @@ -363,7 +367,7 @@ Next == \/ CommitDone(tx) \/ Abort(tx) \/ \E s \in Stores: (CreateStore(tx, s) \/ DeleteStore(tx, s))) - \/ AllDone + \/ AllClosed Spec == Init /\ [][Next]_Vars From 5b24e3f35b286c47c83bd49f9f106014e5c322db Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 01:49:10 +0700 Subject: [PATCH 08/23] track request processing with just a boolean Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 2940e8ca..2b1c2ed9 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -31,10 +31,10 @@ TypeOK == \* We abstract away the actual list of requests and their side effects on stores \* because the goal of this spec is to model the concurrency of the transaction lifecycle only. requests : BOOLEAN, - \* A counter of requests that have been processed. + \* A flag indicating if any requests have been processed. \* Used to verify the invariant that a transaction must satisfy CanStart \* before it processes any requests. - processed_requests: Nat, + processed_requests: BOOLEAN, state: TxStates ]] IsCreated(tx) == transactions[tx].state # "None" @@ -107,7 +107,7 @@ CanStart(tx) == \* Invariant: If a transaction has processed requests, it must have been able to start. ProcessedRequestsImpliesStarted == \A tx \in Transactions: - (transactions[tx].processed_requests > 0) => CanStart(tx) + (transactions[tx].processed_requests) => CanStart(tx) ----------------------------------------------------------------------------------------- DefaultTx == @@ -115,7 +115,7 @@ DefaultTx == mode |-> "readonly", stores |-> {}, requests |-> FALSE, - processed_requests |-> 0, + processed_requests |-> FALSE, state |-> "None" ] DefaultConn == @@ -178,7 +178,7 @@ CreateUpgradeTransaction(c) == mode |-> "versionchange", stores |-> { s \in Stores : stores[s] }, requests |-> FALSE, - processed_requests |-> 0, + processed_requests |-> FALSE, state |-> "Active"] ] /\ connections' = [connections EXCEPT @@ -219,7 +219,7 @@ CreateTransaction(c, mode, scope) == mode |-> mode, stores |-> scope, requests |-> FALSE, - processed_requests |-> 0, + processed_requests |-> FALSE, state |-> "Active"] ] /\ UNCHANGED <> @@ -236,8 +236,9 @@ AddRequest(tx) == \* \* Set request’s processed flag to true. \* -\* Note: just modelling the presence of pending requests, -\* and counting processed requests(for the can start invariant). +\* Note: just modelling the presence of pending requests +\* and the fact that at least one was processed +\* so that we can check the "can start" invariant. ProcessRequest(tx) == /\ CanStart(tx) /\ ConnOpen(transactions[tx].conn) @@ -245,7 +246,7 @@ ProcessRequest(tx) == /\ transactions[tx].requests /\ transactions' = [transactions EXCEPT ![tx].requests = FALSE, - ![tx].processed_requests = transactions[tx].processed_requests + 1, + ![tx].processed_requests = TRUE, ![tx].state = "Active" ] /\ UNCHANGED <> From 94b663c7858ba392af94f2a17b21d00d42646298 Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 01:59:16 +0700 Subject: [PATCH 09/23] fix transaction ordering Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.cfg | 2 +- transaction_lifecycle.tla | 57 +++++++++++++++++++++------------------ 2 files changed, 32 insertions(+), 27 deletions(-) diff --git a/transaction_lifecycle.cfg b/transaction_lifecycle.cfg index 7db9bd6d..6d66cfcd 100644 --- a/transaction_lifecycle.cfg +++ b/transaction_lifecycle.cfg @@ -2,7 +2,7 @@ SPECIFICATION Spec CONSTANT Stores = {s1, s2} CONSTANT Connections = {c1, c2} -CONSTANT Transactions = {0, 1, 2} +CONSTANT Transactions = {t1, t2, t3} CONSTANT Versions = {0, 1, 2} INVARIANT TypeOK diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 2b1c2ed9..a842b5f3 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -2,13 +2,13 @@ EXTENDS Naturals, Sequences, FiniteSets, TLC CONSTANTS Stores, Connections, Transactions, Versions -VARIABLES transactions, stores, pending_stores, connections, dbVersion, connection_queue +VARIABLES transactions, stores, pending_stores, connections, dbVersion, connection_queue, next_tx_order \* TLA+ model of the transaction lifecycle and scheduling rules from: \* - \* - \* Note: by using only a single dbVersion, we do not model multiple databases. -Vars == << transactions, stores, pending_stores, connections, dbVersion, connection_queue >> +Vars == << transactions, stores, pending_stores, connections, dbVersion, connection_queue, next_tx_order >> Modes == {"readonly", "readwrite", "versionchange"} TxStates == {"None", "Active", "Inactive", "Committing", "Finished"} @@ -23,6 +23,7 @@ TypeOK == requestedVersion: Versions, closed: BOOLEAN ]] /\ connection_queue \in Seq(Connections) + /\ next_tx_order \in Nat /\ transactions \in [Transactions -> [conn: Connections, mode: Modes, @@ -35,7 +36,8 @@ TypeOK == \* Used to verify the invariant that a transaction must satisfy CanStart \* before it processes any requests. processed_requests: BOOLEAN, - state: TxStates ]] + state: TxStates, + creation_time: Nat ]] IsCreated(tx) == transactions[tx].state # "None" @@ -43,13 +45,10 @@ Live(tx) == IsCreated(tx) /\ transactions[tx].state # "Finished" Overlaps(tx1, tx2) == (transactions[tx1].stores \cap transactions[tx2].stores) # {} -\* Since we allocate transaction IDs in increasing order (using Min), -\* the ID itself serves as a logical clock for creation time. -CreatedBefore(tx1, tx2) == tx1 < tx2 +\* Transactions are ordered by their creation time. +CreatedBefore(tx1, tx2) == transactions[tx1].creation_time < transactions[tx2].creation_time -Min(S) == CHOOSE x \in S : \A y \in S : x <= y - -Symmetry == Permutations(Stores) \cup Permutations(Connections) +Symmetry == Permutations(Stores) \cup Permutations(Connections) \cup Permutations(Transactions) ConnOpen(c) == connections[c].open @@ -116,7 +115,8 @@ DefaultTx == stores |-> {}, requests |-> FALSE, processed_requests |-> FALSE, - state |-> "None" ] + state |-> "None", + creation_time |-> 0 ] DefaultConn == [ open |-> FALSE, @@ -131,6 +131,7 @@ Init == /\ connections = [c \in Connections |-> DefaultConn] /\ dbVersion = 0 /\ connection_queue = <<>> + /\ next_tx_order = 0 \* \* Wait until all previous requests in queue have been processed. @@ -145,7 +146,7 @@ StartOpenConnection(c, requestedVersion) == closed |-> FALSE] ] /\ connection_queue' = Append(connection_queue, c) - /\ UNCHANGED <> + /\ UNCHANGED <> \* FinishOpenConnection(c) == @@ -157,7 +158,7 @@ FinishOpenConnection(c) == /\ ~HasLiveUpgradeTx(c) /\ connections' = [connections EXCEPT ![c].open = TRUE, ![c].pendingUpgrade = FALSE] /\ connection_queue' = Tail(connection_queue) - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* Wait until all connections in openConnections are closed. @@ -165,7 +166,7 @@ FinishOpenConnection(c) == CreateUpgradeTransaction(c) == LET freeTxs == { t \in Transactions : ~IsCreated(t) } - tx == Min(freeTxs) + tx == CHOOSE t \in freeTxs : TRUE IN /\ Len(connection_queue) > 0 /\ ~ConnOpen(c) @@ -179,13 +180,15 @@ CreateUpgradeTransaction(c) == stores |-> { s \in Stores : stores[s] }, requests |-> FALSE, processed_requests |-> FALSE, - state |-> "Active"] + state |-> "Active", + creation_time |-> next_tx_order] ] /\ connections' = [connections EXCEPT ![c].open = TRUE ] /\ dbVersion' = connections[c].requestedVersion /\ pending_stores' = stores + /\ next_tx_order' = next_tx_order + 1 /\ UNCHANGED <> \* @@ -202,7 +205,7 @@ CloseConnection(c) == IF transactions[tx].conn = c THEN DefaultTx ELSE transactions[tx]] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* If a live upgrade transaction is associated with the connection, throw @@ -213,15 +216,17 @@ CreateTransaction(c, mode, scope) == /\ ConnOpen(c) /\ ~HasLiveUpgradeTx(c) /\ \A s \in scope: stores[s] - /\ LET tx == Min(freeTxs) IN + /\ LET tx == CHOOSE t \in freeTxs : TRUE IN /\ transactions' = [transactions EXCEPT ![tx] = [conn |-> c, mode |-> mode, stores |-> scope, requests |-> FALSE, processed_requests |-> FALSE, - state |-> "Active"] + state |-> "Active", + creation_time |-> next_tx_order] ] + /\ next_tx_order' = next_tx_order + 1 /\ UNCHANGED <> \* @@ -230,7 +235,7 @@ AddRequest(tx) == /\ transactions[tx].state = "Active" /\ ~transactions[tx].requests /\ transactions' = [transactions EXCEPT ![tx].requests = TRUE] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -249,7 +254,7 @@ ProcessRequest(tx) == ![tx].processed_requests = TRUE, ![tx].state = "Active" ] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -263,7 +268,7 @@ ProcessRequest(tx) == Deactivate(tx) == /\ transactions[tx].state = "Active" /\ transactions' = [transactions EXCEPT ![tx].state = "Inactive"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -274,7 +279,7 @@ AutoCommit(tx) == /\ transactions[tx].state = "Inactive" /\ ~transactions[tx].requests /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -284,7 +289,7 @@ AutoCommit(tx) == Commit(tx) == /\ transactions[tx].state \notin {"None", "Committing", "Finished"} /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* "When a transaction is committed or aborted, its state is @@ -303,7 +308,7 @@ CommitDone(tx) == /\ UNCHANGED pending_stores ELSE /\ UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -318,7 +323,7 @@ Abort(tx) == /\ UNCHANGED stores ELSE /\ UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -332,7 +337,7 @@ CreateStore(tx, s) == /\ transactions[tx].state = "Active" /\ ~pending_stores[s] /\ pending_stores' = [pending_stores EXCEPT ![s] = TRUE] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -345,7 +350,7 @@ DeleteStore(tx, s) == /\ transactions[tx].state = "Active" /\ pending_stores[s] /\ pending_stores' = [pending_stores EXCEPT ![s] = FALSE] - /\ UNCHANGED <> + /\ UNCHANGED <> \* When all connections went through their open and close cyle: infinite stuttering. AllClosed == From 81579753add8d687f0f1cd2c8a7022ba1a763cf2 Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 02:21:43 +0700 Subject: [PATCH 10/23] add rejecting of open Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.cfg | 1 + transaction_lifecycle.tla | 51 ++++++++++++++++++++++++++------------- 2 files changed, 35 insertions(+), 17 deletions(-) diff --git a/transaction_lifecycle.cfg b/transaction_lifecycle.cfg index 6d66cfcd..eb894ff6 100644 --- a/transaction_lifecycle.cfg +++ b/transaction_lifecycle.cfg @@ -9,6 +9,7 @@ INVARIANT TypeOK INVARIANT UpgradeTxExcludesOtherLiveTxs INVARIANT ActiveUpgradeTxImpliesExclusiveConn INVARIANT ProcessedRequestsImpliesStarted +INVARIANT ActiveTransactionImpliesCorrectVersion SYMMETRY Symmetry diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index a842b5f3..a2210556 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -66,6 +66,23 @@ HasLiveUpgradeTx(c) == /\ transactions[tx].conn = c /\ transactions[tx].mode = "versionchange" +\* . +CanStart(tx) == + LET m == transactions[tx].mode IN + IF m = "readonly" THEN + ~\E other \in (Transactions \ {tx}): + /\ Live(other) + /\ transactions[other].mode = "readwrite" + /\ CreatedBefore(other, tx) + /\ Overlaps(other, tx) + ELSE IF m = "readwrite" THEN + ~\E other \in (Transactions \ {tx}): + /\ Live(other) + /\ CreatedBefore(other, tx) + /\ Overlaps(other, tx) + ELSE \* versionchange transactions can always start. + TRUE + \* Safety property: A versionchange transaction being live excludes any other live transaction. UpgradeTxExcludesOtherLiveTxs == \A tx1 \in Transactions: @@ -86,22 +103,11 @@ ActiveUpgradeTxImpliesExclusiveConn == /\ Head(connection_queue) = transactions[tx].conn /\ \A c \in Connections: ConnOpen(c) => c = transactions[tx].conn -\* . -CanStart(tx) == - LET m == transactions[tx].mode IN - IF m = "readonly" THEN - ~\E other \in (Transactions \ {tx}): - /\ Live(other) - /\ transactions[other].mode = "readwrite" - /\ CreatedBefore(other, tx) - /\ Overlaps(other, tx) - ELSE IF m = "readwrite" THEN - ~\E other \in (Transactions \ {tx}): - /\ Live(other) - /\ CreatedBefore(other, tx) - /\ Overlaps(other, tx) - ELSE \* versionchange transactions can always start. - TRUE +\* Invariant: An active transaction implies that the version of the connection is that of the db. +ActiveTransactionImpliesCorrectVersion == + \A tx \in Transactions: + (transactions[tx].state = "Active") => + (connections[transactions[tx].conn].requestedVersion = dbVersion) \* Invariant: If a transaction has processed requests, it must have been able to start. ProcessedRequestsImpliesStarted == @@ -136,7 +142,6 @@ Init == \* \* Wait until all previous requests in queue have been processed. StartOpenConnection(c, requestedVersion) == - /\ dbVersion <= requestedVersion /\ connections[c] = DefaultConn /\ ~connections[c].closed /\ connections' = [connections EXCEPT @@ -160,6 +165,17 @@ FinishOpenConnection(c) == /\ connection_queue' = Tail(connection_queue) /\ UNCHANGED <> +\* +\* If db’s version is greater than version, +\* abort these steps. +RejectOpenConnection(c) == + /\ Len(connection_queue) > 0 + /\ c = Head(connection_queue) + /\ connections[c].requestedVersion < dbVersion + /\ connections' = [connections EXCEPT ![c] = DefaultConn] + /\ connection_queue' = Tail(connection_queue) + /\ UNCHANGED <> + \* \* Wait until all connections in openConnections are closed. \* Run upgrade a database using connection, version and request. @@ -360,6 +376,7 @@ AllClosed == Next == \/ \E c \in Connections, v \in Versions: StartOpenConnection(c, v) \/ \E c \in Connections: FinishOpenConnection(c) + \/ \E c \in Connections: RejectOpenConnection(c) \/ \E c \in Connections: CloseConnection(c) \/ \E c \in Connections: CreateUpgradeTransaction(c) \/ \E c \in Connections, m \in {"readonly", "readwrite"}, scope \in SUBSET Stores: From 08c2f938796e31bed5de734684365971b0e25b6f Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 12:05:57 +0700 Subject: [PATCH 11/23] revert version change on abort Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 79 ++++++++++++++++++++++----------------- 1 file changed, 45 insertions(+), 34 deletions(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index a2210556..98ade888 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -2,13 +2,13 @@ EXTENDS Naturals, Sequences, FiniteSets, TLC CONSTANTS Stores, Connections, Transactions, Versions -VARIABLES transactions, stores, pending_stores, connections, dbVersion, connection_queue, next_tx_order +VARIABLES transactions, stores, pending_stores, connections, dbVersion, pendingDbVersion, connection_queue, next_tx_order \* TLA+ model of the transaction lifecycle and scheduling rules from: \* - \* - \* Note: by using only a single dbVersion, we do not model multiple databases. -Vars == << transactions, stores, pending_stores, connections, dbVersion, connection_queue, next_tx_order >> +Vars == << transactions, stores, pending_stores, connections, dbVersion, pendingDbVersion, connection_queue, next_tx_order >> Modes == {"readonly", "readwrite", "versionchange"} TxStates == {"None", "Active", "Inactive", "Committing", "Finished"} @@ -17,6 +17,7 @@ TypeOK == /\ stores \in [Stores -> BOOLEAN] /\ pending_stores \in [Stores -> BOOLEAN] /\ dbVersion \in Versions + /\ pendingDbVersion \in Versions /\ connections \in [Connections -> [open: BOOLEAN, pendingUpgrade: BOOLEAN, @@ -103,11 +104,14 @@ ActiveUpgradeTxImpliesExclusiveConn == /\ Head(connection_queue) = transactions[tx].conn /\ \A c \in Connections: ConnOpen(c) => c = transactions[tx].conn -\* Invariant: An active transaction implies that the version of the connection is that of the db. +\* Invariant: A live transaction implies that the version of the connection is that of the db, +\* or, in the case of versionchange, that of the pending version of the db. ActiveTransactionImpliesCorrectVersion == \A tx \in Transactions: - (transactions[tx].state = "Active") => - (connections[transactions[tx].conn].requestedVersion = dbVersion) + Live(tx) => + \/ (connections[transactions[tx].conn].requestedVersion = dbVersion) + \/ /\ transactions[tx].mode = "versionchange" + /\ connections[transactions[tx].conn].requestedVersion = pendingDbVersion \* Invariant: If a transaction has processed requests, it must have been able to start. ProcessedRequestsImpliesStarted == @@ -136,6 +140,7 @@ Init == /\ pending_stores = [s \in Stores |-> FALSE] /\ connections = [c \in Connections |-> DefaultConn] /\ dbVersion = 0 + /\ pendingDbVersion = 0 /\ connection_queue = <<>> /\ next_tx_order = 0 @@ -151,19 +156,21 @@ StartOpenConnection(c, requestedVersion) == closed |-> FALSE] ] /\ connection_queue' = Append(connection_queue, c) - /\ UNCHANGED <> + /\ UNCHANGED <> \* FinishOpenConnection(c) == /\ Len(connection_queue) > 0 /\ c = Head(connection_queue) - /\ connections[c].requestedVersion = dbVersion + /\ (connections[c].requestedVersion = dbVersion \/ connections[c].closed) \* \* Wait for transaction to finish. /\ ~HasLiveUpgradeTx(c) - /\ connections' = [connections EXCEPT ![c].open = TRUE, ![c].pendingUpgrade = FALSE] + /\ IF connections[c].closed + THEN connections' = [connections EXCEPT ![c].pendingUpgrade = FALSE] + ELSE connections' = [connections EXCEPT ![c].open = TRUE, ![c].pendingUpgrade = FALSE] /\ connection_queue' = Tail(connection_queue) - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* If db’s version is greater than version, @@ -171,10 +178,11 @@ FinishOpenConnection(c) == RejectOpenConnection(c) == /\ Len(connection_queue) > 0 /\ c = Head(connection_queue) + /\ ~connections[c].pendingUpgrade /\ connections[c].requestedVersion < dbVersion /\ connections' = [connections EXCEPT ![c] = DefaultConn] /\ connection_queue' = Tail(connection_queue) - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* Wait until all connections in openConnections are closed. @@ -187,6 +195,7 @@ CreateUpgradeTransaction(c) == /\ Len(connection_queue) > 0 /\ ~ConnOpen(c) /\ c = Head(connection_queue) + /\ ~connections[c].closed /\ ConnPendingUpgrade(c) /\ \A other \in (Connections \ {c}): ~ConnOpen(other) /\ freeTxs # {} @@ -202,10 +211,10 @@ CreateUpgradeTransaction(c) == /\ connections' = [connections EXCEPT ![c].open = TRUE ] - /\ dbVersion' = connections[c].requestedVersion + /\ pendingDbVersion' = connections[c].requestedVersion /\ pending_stores' = stores /\ next_tx_order' = next_tx_order + 1 - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -221,10 +230,10 @@ CloseConnection(c) == IF transactions[tx].conn = c THEN DefaultTx ELSE transactions[tx]] - /\ UNCHANGED <> + /\ UNCHANGED <> \* -\* If a live upgrade transaction is associated with the connection, throw +\* If a live upgrade transaction is associated with the connection, throw. \* If this’s close pending flag is true, then throw. CreateTransaction(c, mode, scope) == LET freeTxs == { t \in Transactions : ~IsCreated(t) } IN @@ -243,7 +252,7 @@ CreateTransaction(c, mode, scope) == creation_time |-> next_tx_order] ] /\ next_tx_order' = next_tx_order + 1 - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* Assert: transaction’s state is active. @@ -251,7 +260,7 @@ AddRequest(tx) == /\ transactions[tx].state = "Active" /\ ~transactions[tx].requests /\ transactions' = [transactions EXCEPT ![tx].requests = TRUE] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -270,21 +279,16 @@ ProcessRequest(tx) == ![tx].processed_requests = TRUE, ![tx].state = "Active" ] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* \* "Once the event dispatch is complete, the transaction's state \* is set to inactive again". -\* -\* Note: the event is dispatched and the transaction de-activated -\* from within the same task, but we still model these as separate -\* steps to make it easier to model adding any number of requests -\* while the transaction is active. Deactivate(tx) == /\ transactions[tx].state = "Active" /\ transactions' = [transactions EXCEPT ![tx].state = "Inactive"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -295,7 +299,7 @@ AutoCommit(tx) == /\ transactions[tx].state = "Inactive" /\ ~transactions[tx].requests /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -305,14 +309,14 @@ AutoCommit(tx) == Commit(tx) == /\ transactions[tx].state \notin {"None", "Committing", "Finished"} /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* "When a transaction is committed or aborted, its state is \* set to finished". \* \* Note: The commit/abort logic is only applied to store operations (CreateStore/DeleteStore) -\* for now. We do not model data operations or their side effects/rollback, as it would +\* and the db version. We do not model data operations or their side effects/rollback, as it would \* make the spec significantly more complicated without adding much value to the \* transaction lifecycle concurrency model. CommitDone(tx) == @@ -321,10 +325,11 @@ CommitDone(tx) == /\ IF transactions[tx].mode = "versionchange" THEN /\ stores' = pending_stores - /\ UNCHANGED pending_stores + /\ dbVersion' = pendingDbVersion + /\ UNCHANGED <> ELSE - /\ UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -336,10 +341,16 @@ Abort(tx) == /\ IF transactions[tx].mode = "versionchange" THEN /\ pending_stores' = stores - /\ UNCHANGED stores + /\ pendingDbVersion' = dbVersion + \* + \* "If the upgrade transaction was aborted, run the steps to close a database connection with connection" + /\ connections' = [connections EXCEPT + ![transactions[tx].conn].open = FALSE, + ![transactions[tx].conn].closed = TRUE] + /\ UNCHANGED <> ELSE - /\ UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -353,7 +364,7 @@ CreateStore(tx, s) == /\ transactions[tx].state = "Active" /\ ~pending_stores[s] /\ pending_stores' = [pending_stores EXCEPT ![s] = TRUE] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -366,7 +377,7 @@ DeleteStore(tx, s) == /\ transactions[tx].state = "Active" /\ pending_stores[s] /\ pending_stores' = [pending_stores EXCEPT ![s] = FALSE] - /\ UNCHANGED <> + /\ UNCHANGED <> \* When all connections went through their open and close cyle: infinite stuttering. AllClosed == From 9b1018a2f7fa6dac52f211dce292f34dde44c29b Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 12:14:09 +0700 Subject: [PATCH 12/23] add invariant for overlapping started transactions Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.cfg | 1 + transaction_lifecycle.tla | 10 ++++++++++ 2 files changed, 11 insertions(+) diff --git a/transaction_lifecycle.cfg b/transaction_lifecycle.cfg index eb894ff6..dd495dfd 100644 --- a/transaction_lifecycle.cfg +++ b/transaction_lifecycle.cfg @@ -10,6 +10,7 @@ INVARIANT UpgradeTxExcludesOtherLiveTxs INVARIANT ActiveUpgradeTxImpliesExclusiveConn INVARIANT ProcessedRequestsImpliesStarted INVARIANT ActiveTransactionImpliesCorrectVersion +INVARIANT OverlappingStartedTxsAreReadOnly SYMMETRY Symmetry diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 98ade888..9b5e0065 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -117,6 +117,16 @@ ActiveTransactionImpliesCorrectVersion == ProcessedRequestsImpliesStarted == \A tx \in Transactions: (transactions[tx].processed_requests) => CanStart(tx) + +\* Invariant: If two transactions who are not the same are live, have started (processed requests), +\* and have overlapping scopes, then they must be read-only. +OverlappingStartedTxsAreReadOnly == + \A tx1, tx2 \in Transactions: + (tx1 # tx2 + /\ Live(tx1) /\ transactions[tx1].processed_requests + /\ Live(tx2) /\ transactions[tx2].processed_requests + /\ Overlaps(tx1, tx2)) + => (transactions[tx1].mode = "readonly" /\ transactions[tx2].mode = "readonly") ----------------------------------------------------------------------------------------- DefaultTx == From 8eae76f048f9b364cb7ce6b46ba8af82abe79c59 Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 12:15:51 +0700 Subject: [PATCH 13/23] group invariants together Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 57 ++++++++++++++++++++------------------- 1 file changed, 30 insertions(+), 27 deletions(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 9b5e0065..ee9aa5f9 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -13,33 +13,6 @@ Vars == << transactions, stores, pending_stores, connections, dbVersion, pending Modes == {"readonly", "readwrite", "versionchange"} TxStates == {"None", "Active", "Inactive", "Committing", "Finished"} -TypeOK == - /\ stores \in [Stores -> BOOLEAN] - /\ pending_stores \in [Stores -> BOOLEAN] - /\ dbVersion \in Versions - /\ pendingDbVersion \in Versions - /\ connections \in [Connections -> - [open: BOOLEAN, - pendingUpgrade: BOOLEAN, - requestedVersion: Versions, - closed: BOOLEAN ]] - /\ connection_queue \in Seq(Connections) - /\ next_tx_order \in Nat - /\ transactions \in [Transactions -> - [conn: Connections, - mode: Modes, - stores: SUBSET Stores, - \* We model requests as a simple boolean flag indicating pending work. - \* We abstract away the actual list of requests and their side effects on stores - \* because the goal of this spec is to model the concurrency of the transaction lifecycle only. - requests : BOOLEAN, - \* A flag indicating if any requests have been processed. - \* Used to verify the invariant that a transaction must satisfy CanStart - \* before it processes any requests. - processed_requests: BOOLEAN, - state: TxStates, - creation_time: Nat ]] - IsCreated(tx) == transactions[tx].state # "None" Live(tx) == IsCreated(tx) /\ transactions[tx].state # "Finished" @@ -84,6 +57,36 @@ CanStart(tx) == ELSE \* versionchange transactions can always start. TRUE +----------------------------------------------------------------------------------------- + +\* Type invariant. +TypeOK == + /\ stores \in [Stores -> BOOLEAN] + /\ pending_stores \in [Stores -> BOOLEAN] + /\ dbVersion \in Versions + /\ pendingDbVersion \in Versions + /\ connections \in [Connections -> + [open: BOOLEAN, + pendingUpgrade: BOOLEAN, + requestedVersion: Versions, + closed: BOOLEAN ]] + /\ connection_queue \in Seq(Connections) + /\ next_tx_order \in Nat + /\ transactions \in [Transactions -> + [conn: Connections, + mode: Modes, + stores: SUBSET Stores, + \* We model requests as a simple boolean flag indicating pending work. + \* We abstract away the actual list of requests and their side effects on stores + \* because the goal of this spec is to model the concurrency of the transaction lifecycle only. + requests : BOOLEAN, + \* A flag indicating if any requests have been processed. + \* Used to verify the invariant that a transaction must satisfy CanStart + \* before it processes any requests. + processed_requests: BOOLEAN, + state: TxStates, + creation_time: Nat ]] + \* Safety property: A versionchange transaction being live excludes any other live transaction. UpgradeTxExcludesOtherLiveTxs == \A tx1 \in Transactions: From e5ef8d479fde148d196030c295170cc0bdc4baf2 Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 12:17:55 +0700 Subject: [PATCH 14/23] bound connection queue Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 1 + 1 file changed, 1 insertion(+) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index ee9aa5f9..0e76b854 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -162,6 +162,7 @@ Init == StartOpenConnection(c, requestedVersion) == /\ connections[c] = DefaultConn /\ ~connections[c].closed + /\ Len(connection_queue) < Cardinality(Connections) /\ connections' = [connections EXCEPT ![c] = [open |-> FALSE, pendingUpgrade |-> (requestedVersion > dbVersion), From f27a3737b2fc362bfad892a6b0cbdda4805d6330 Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 12:40:25 +0700 Subject: [PATCH 15/23] fix autocommit Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.cfg | 1 + transaction_lifecycle.tla | 82 ++++++++++++++++++++++----------------- 2 files changed, 47 insertions(+), 36 deletions(-) diff --git a/transaction_lifecycle.cfg b/transaction_lifecycle.cfg index dd495dfd..aea616bc 100644 --- a/transaction_lifecycle.cfg +++ b/transaction_lifecycle.cfg @@ -4,6 +4,7 @@ CONSTANT Stores = {s1, s2} CONSTANT Connections = {c1, c2} CONSTANT Transactions = {t1, t2, t3} CONSTANT Versions = {0, 1, 2} +CONSTANT MaxRequests = 3 INVARIANT TypeOK INVARIANT UpgradeTxExcludesOtherLiveTxs diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 0e76b854..0fabe68c 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -1,7 +1,7 @@ ------------------------------ MODULE transaction_lifecycle ------------------------------ EXTENDS Naturals, Sequences, FiniteSets, TLC -CONSTANTS Stores, Connections, Transactions, Versions +CONSTANTS Stores, Connections, Transactions, Versions, MaxRequests VARIABLES transactions, stores, pending_stores, connections, dbVersion, pendingDbVersion, connection_queue, next_tx_order \* TLA+ model of the transaction lifecycle and scheduling rules from: \* - @@ -79,11 +79,12 @@ TypeOK == \* We model requests as a simple boolean flag indicating pending work. \* We abstract away the actual list of requests and their side effects on stores \* because the goal of this spec is to model the concurrency of the transaction lifecycle only. - requests : BOOLEAN, + requests : Nat, \* A flag indicating if any requests have been processed. \* Used to verify the invariant that a transaction must satisfy CanStart \* before it processes any requests. - processed_requests: BOOLEAN, + processed_requests: Nat, + handled_requests: Nat, state: TxStates, creation_time: Nat ]] @@ -119,15 +120,15 @@ ActiveTransactionImpliesCorrectVersion == \* Invariant: If a transaction has processed requests, it must have been able to start. ProcessedRequestsImpliesStarted == \A tx \in Transactions: - (transactions[tx].processed_requests) => CanStart(tx) + (transactions[tx].processed_requests > 0) => CanStart(tx) \* Invariant: If two transactions who are not the same are live, have started (processed requests), \* and have overlapping scopes, then they must be read-only. OverlappingStartedTxsAreReadOnly == \A tx1, tx2 \in Transactions: (tx1 # tx2 - /\ Live(tx1) /\ transactions[tx1].processed_requests - /\ Live(tx2) /\ transactions[tx2].processed_requests + /\ Live(tx1) /\ transactions[tx1].processed_requests > 0 + /\ Live(tx2) /\ transactions[tx2].processed_requests > 0 /\ Overlaps(tx1, tx2)) => (transactions[tx1].mode = "readonly" /\ transactions[tx2].mode = "readonly") ----------------------------------------------------------------------------------------- @@ -136,8 +137,9 @@ DefaultTx == [ conn |-> CHOOSE c \in Connections : TRUE, mode |-> "readonly", stores |-> {}, - requests |-> FALSE, - processed_requests |-> FALSE, + requests |-> 0, + processed_requests |-> 0, + handled_requests |-> 0, state |-> "None", creation_time |-> 0 ] @@ -217,8 +219,9 @@ CreateUpgradeTransaction(c) == ![tx] = [conn |-> c, mode |-> "versionchange", stores |-> { s \in Stores : stores[s] }, - requests |-> FALSE, - processed_requests |-> FALSE, + requests |-> 0, + processed_requests |-> 0, + handled_requests |-> 0, state |-> "Active", creation_time |-> next_tx_order] ] @@ -260,22 +263,15 @@ CreateTransaction(c, mode, scope) == ![tx] = [conn |-> c, mode |-> mode, stores |-> scope, - requests |-> FALSE, - processed_requests |-> FALSE, + requests |-> 0, + processed_requests |-> 0, + handled_requests |-> 0, state |-> "Active", creation_time |-> next_tx_order] ] /\ next_tx_order' = next_tx_order + 1 /\ UNCHANGED <> -\* -\* Assert: transaction’s state is active. -AddRequest(tx) == - /\ transactions[tx].state = "Active" - /\ ~transactions[tx].requests - /\ transactions' = [transactions EXCEPT ![tx].requests = TRUE] - /\ UNCHANGED <> - \* \* \* Set request’s processed flag to true. @@ -287,39 +283,53 @@ ProcessRequest(tx) == /\ CanStart(tx) /\ ConnOpen(transactions[tx].conn) /\ transactions[tx].state \in {"Active", "Inactive"} - /\ transactions[tx].requests + /\ transactions[tx].processed_requests < transactions[tx].requests /\ transactions' = [transactions EXCEPT - ![tx].requests = FALSE, - ![tx].processed_requests = TRUE, + ![tx].processed_requests = @ + 1, ![tx].state = "Active" ] /\ UNCHANGED <> +\* +\* Assert: transaction’s state is active. +AddRequest(tx) == + /\ transactions[tx].state = "Active" + /\ transactions[tx].requests < MaxRequests + /\ transactions' = [transactions EXCEPT ![tx].requests = @ + 1] + /\ UNCHANGED <> + + \* \* \* "Once the event dispatch is complete, the transaction's state \* is set to inactive again". +\* +\* Note: AddRequest and Deactivate modeled as two steps, +\* even though in practice this happens in the same event-loop task. +\* This does not change anything other than making for easier modelling of adding +\* any number of requests while the transaction is active. Deactivate(tx) == /\ transactions[tx].state = "Active" - /\ transactions' = [transactions EXCEPT ![tx].state = "Inactive"] + /\ transactions[tx].handled_requests < transactions[tx].processed_requests + /\ transactions' = [transactions EXCEPT + ![tx].state = "Inactive", + ![tx].handled_requests = @ + 1] /\ UNCHANGED <> -\* -\* -\* "The implementation must attempt to commit an inactive transaction -\* when all requests placed against the transaction have completed... -\* and no new requests have been placed against the transaction". +\* +\* The implementation must attempt to commit an inactive transaction +\* when all requests placed against the transaction have completed +\* and their returned results handled, +\* no new requests have been placed against the transaction, +\* and the transaction has not been aborted AutoCommit(tx) == /\ transactions[tx].state = "Inactive" - /\ ~transactions[tx].requests + /\ transactions[tx].requests = transactions[tx].processed_requests + /\ transactions[tx].requests = transactions[tx].handled_requests /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] /\ UNCHANGED <> -\* -\* -\* "An explicit call to commit() will initiate a -\* transaction/commit" and "When committing, the transaction state is set to -\* committing". +\* Commit(tx) == /\ transactions[tx].state \notin {"None", "Committing", "Finished"} /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] @@ -350,7 +360,7 @@ CommitDone(tx) == \* "A transaction can be aborted at any time before it is \* finished". Abort(tx) == - /\ transactions[tx].state \notin {"None", "Finished"} + /\ transactions[tx].state \notin {"None", "Committing", "Finished"} /\ transactions' = [transactions EXCEPT ![tx].state = "Finished"] /\ IF transactions[tx].mode = "versionchange" THEN From dda4b73056200b518ffc9f91f845f4164a9471e1 Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 12:43:08 +0700 Subject: [PATCH 16/23] fix docs Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.cfg | 2 -- transaction_lifecycle.tla | 13 ++----------- 2 files changed, 2 insertions(+), 13 deletions(-) diff --git a/transaction_lifecycle.cfg b/transaction_lifecycle.cfg index aea616bc..cd1471ed 100644 --- a/transaction_lifecycle.cfg +++ b/transaction_lifecycle.cfg @@ -14,5 +14,3 @@ INVARIANT ActiveTransactionImpliesCorrectVersion INVARIANT OverlappingStartedTxsAreReadOnly SYMMETRY Symmetry - - diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 0fabe68c..d5be1820 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -40,7 +40,7 @@ HasLiveUpgradeTx(c) == /\ transactions[tx].conn = c /\ transactions[tx].mode = "versionchange" -\* . +\* CanStart(tx) == LET m == transactions[tx].mode IN IF m = "readonly" THEN @@ -76,13 +76,7 @@ TypeOK == [conn: Connections, mode: Modes, stores: SUBSET Stores, - \* We model requests as a simple boolean flag indicating pending work. - \* We abstract away the actual list of requests and their side effects on stores - \* because the goal of this spec is to model the concurrency of the transaction lifecycle only. requests : Nat, - \* A flag indicating if any requests have been processed. - \* Used to verify the invariant that a transaction must satisfy CanStart - \* before it processes any requests. processed_requests: Nat, handled_requests: Nat, state: TxStates, @@ -275,10 +269,6 @@ CreateTransaction(c, mode, scope) == \* \* \* Set request’s processed flag to true. -\* -\* Note: just modelling the presence of pending requests -\* and the fact that at least one was processed -\* so that we can check the "can start" invariant. ProcessRequest(tx) == /\ CanStart(tx) /\ ConnOpen(transactions[tx].conn) @@ -404,6 +394,7 @@ DeleteStore(tx, s) == /\ UNCHANGED <> \* When all connections went through their open and close cyle: infinite stuttering. +\* This is a way to avoid deadlock while bounding the spec. AllClosed == /\ \A c \in Connections: connections[c].closed /\ UNCHANGED Vars From ebd91660d00078d4b09a2e868877d4a164141bf3 Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 14:09:19 +0700 Subject: [PATCH 17/23] fix closing of connection interaction with abort Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 112 +++++++++++++++++++++++--------------- 1 file changed, 68 insertions(+), 44 deletions(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index d5be1820..f345793c 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -2,13 +2,13 @@ EXTENDS Naturals, Sequences, FiniteSets, TLC CONSTANTS Stores, Connections, Transactions, Versions, MaxRequests -VARIABLES transactions, stores, pending_stores, connections, dbVersion, pendingDbVersion, connection_queue, next_tx_order +VARIABLES transactions, stores, pending_stores, connections, dbVersion, oldDbVersion, connection_queue, next_tx_order \* TLA+ model of the transaction lifecycle and scheduling rules from: \* - \* - \* Note: by using only a single dbVersion, we do not model multiple databases. -Vars == << transactions, stores, pending_stores, connections, dbVersion, pendingDbVersion, connection_queue, next_tx_order >> +Vars == << transactions, stores, pending_stores, connections, dbVersion, oldDbVersion, connection_queue, next_tx_order >> Modes == {"readonly", "readwrite", "versionchange"} TxStates == {"None", "Active", "Inactive", "Committing", "Finished"} @@ -32,7 +32,7 @@ TxForConn(c) == { tx \in Transactions : Live(tx) /\ transactions[tx].conn = c } AllTxFinishedForConn(c) == \A tx \in Transactions: - (transactions[tx].conn = c) => (transactions[tx].state = "Finished") + (transactions[tx].conn = c /\ IsCreated(tx)) => (transactions[tx].state = "Finished") HasLiveUpgradeTx(c) == \E tx \in Transactions: @@ -64,12 +64,13 @@ TypeOK == /\ stores \in [Stores -> BOOLEAN] /\ pending_stores \in [Stores -> BOOLEAN] /\ dbVersion \in Versions - /\ pendingDbVersion \in Versions + /\ oldDbVersion \in Versions /\ connections \in [Connections -> [open: BOOLEAN, pendingUpgrade: BOOLEAN, requestedVersion: Versions, - closed: BOOLEAN ]] + closed: BOOLEAN, + close_pending: BOOLEAN ]] /\ connection_queue \in Seq(Connections) /\ next_tx_order \in Nat /\ transactions \in [Transactions -> @@ -102,14 +103,11 @@ ActiveUpgradeTxImpliesExclusiveConn == /\ Head(connection_queue) = transactions[tx].conn /\ \A c \in Connections: ConnOpen(c) => c = transactions[tx].conn -\* Invariant: A live transaction implies that the version of the connection is that of the db, -\* or, in the case of versionchange, that of the pending version of the db. +\* Invariant: A live transaction implies that the version of the connection is that of the db. ActiveTransactionImpliesCorrectVersion == \A tx \in Transactions: Live(tx) => \/ (connections[transactions[tx].conn].requestedVersion = dbVersion) - \/ /\ transactions[tx].mode = "versionchange" - /\ connections[transactions[tx].conn].requestedVersion = pendingDbVersion \* Invariant: If a transaction has processed requests, it must have been able to start. ProcessedRequestsImpliesStarted == @@ -141,7 +139,8 @@ DefaultConn == [ open |-> FALSE, pendingUpgrade |-> FALSE, requestedVersion|-> 0, - closed |-> FALSE ] + closed |-> FALSE, + close_pending |-> FALSE ] Init == /\ transactions = [tx \in Transactions |-> DefaultTx] @@ -149,7 +148,7 @@ Init == /\ pending_stores = [s \in Stores |-> FALSE] /\ connections = [c \in Connections |-> DefaultConn] /\ dbVersion = 0 - /\ pendingDbVersion = 0 + /\ oldDbVersion = 0 /\ connection_queue = <<>> /\ next_tx_order = 0 @@ -163,10 +162,11 @@ StartOpenConnection(c, requestedVersion) == ![c] = [open |-> FALSE, pendingUpgrade |-> (requestedVersion > dbVersion), requestedVersion|-> requestedVersion, - closed |-> FALSE] + closed |-> FALSE, + close_pending |-> FALSE] ] /\ connection_queue' = Append(connection_queue, c) - /\ UNCHANGED <> + /\ UNCHANGED <> \* FinishOpenConnection(c) == @@ -177,10 +177,12 @@ FinishOpenConnection(c) == \* Wait for transaction to finish. /\ ~HasLiveUpgradeTx(c) /\ IF connections[c].closed + \* If connection was closed, + \* return a newly created "AbortError" DOMException and abort these steps. THEN connections' = [connections EXCEPT ![c].pendingUpgrade = FALSE] ELSE connections' = [connections EXCEPT ![c].open = TRUE, ![c].pendingUpgrade = FALSE] /\ connection_queue' = Tail(connection_queue) - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* If db’s version is greater than version, @@ -192,7 +194,7 @@ RejectOpenConnection(c) == /\ connections[c].requestedVersion < dbVersion /\ connections' = [connections EXCEPT ![c] = DefaultConn] /\ connection_queue' = Tail(connection_queue) - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* Wait until all connections in openConnections are closed. @@ -205,7 +207,6 @@ CreateUpgradeTransaction(c) == /\ Len(connection_queue) > 0 /\ ~ConnOpen(c) /\ c = Head(connection_queue) - /\ ~connections[c].closed /\ ConnPendingUpgrade(c) /\ \A other \in (Connections \ {c}): ~ConnOpen(other) /\ freeTxs # {} @@ -222,17 +223,44 @@ CreateUpgradeTransaction(c) == /\ connections' = [connections EXCEPT ![c].open = TRUE ] - /\ pendingDbVersion' = connections[c].requestedVersion /\ pending_stores' = stores + /\ oldDbVersion' = dbVersion + /\ dbVersion' = connections[c].requestedVersion /\ next_tx_order' = next_tx_order + 1 - /\ UNCHANGED <> + /\ UNCHANGED <> + +\* +StartCloseConnection(c, forced) == + /\ ConnOpen(c) + /\ ~connections[c].close_pending + /\ IF forced /\ HasLiveUpgradeTx(c) + THEN connections' = [connections EXCEPT ![c].close_pending = TRUE, ![c].requestedVersion = oldDbVersion] + ELSE connections' = [connections EXCEPT ![c].close_pending = TRUE] + /\ IF forced + THEN + \* https://w3c.github.io/IndexedDB/#abort-a-transaction + /\ transactions' = [tx \in Transactions |-> + IF transactions[tx].conn = c /\ transactions[tx].state \notin {"None", "Finished"} + THEN [transactions[tx] EXCEPT !.state = "Finished"] + ELSE transactions[tx]] + /\ IF HasLiveUpgradeTx(c) + \* https://w3c.github.io/IndexedDB/#abort-an-upgrade-transaction + THEN + /\ pending_stores' = stores + /\ dbVersion' = oldDbVersion + /\ UNCHANGED <> + ELSE + /\ UNCHANGED <> + ELSE + /\ UNCHANGED <> + /\ UNCHANGED <> \* \* \* "Wait for all transactions created using connection to complete. \* Once they are complete, connection is closed." CloseConnection(c) == - /\ ConnOpen(c) + /\ connections[c].close_pending /\ AllTxFinishedForConn(c) /\ connections' = [connections EXCEPT ![c].open = FALSE, @@ -241,7 +269,7 @@ CloseConnection(c) == IF transactions[tx].conn = c THEN DefaultTx ELSE transactions[tx]] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* If a live upgrade transaction is associated with the connection, throw. @@ -250,6 +278,7 @@ CreateTransaction(c, mode, scope) == LET freeTxs == { t \in Transactions : ~IsCreated(t) } IN /\ freeTxs # {} /\ ConnOpen(c) + /\ ~connections[c].close_pending /\ ~HasLiveUpgradeTx(c) /\ \A s \in scope: stores[s] /\ LET tx == CHOOSE t \in freeTxs : TRUE IN @@ -264,7 +293,7 @@ CreateTransaction(c, mode, scope) == creation_time |-> next_tx_order] ] /\ next_tx_order' = next_tx_order + 1 - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -278,7 +307,7 @@ ProcessRequest(tx) == ![tx].processed_requests = @ + 1, ![tx].state = "Active" ] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* Assert: transaction’s state is active. @@ -286,7 +315,7 @@ AddRequest(tx) == /\ transactions[tx].state = "Active" /\ transactions[tx].requests < MaxRequests /\ transactions' = [transactions EXCEPT ![tx].requests = @ + 1] - /\ UNCHANGED <> + /\ UNCHANGED <> \* @@ -304,7 +333,7 @@ Deactivate(tx) == /\ transactions' = [transactions EXCEPT ![tx].state = "Inactive", ![tx].handled_requests = @ + 1] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* The implementation must attempt to commit an inactive transaction @@ -317,13 +346,13 @@ AutoCommit(tx) == /\ transactions[tx].requests = transactions[tx].processed_requests /\ transactions[tx].requests = transactions[tx].handled_requests /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Commit(tx) == /\ transactions[tx].state \notin {"None", "Committing", "Finished"} /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* "When a transaction is committed or aborted, its state is @@ -339,31 +368,25 @@ CommitDone(tx) == /\ IF transactions[tx].mode = "versionchange" THEN /\ stores' = pending_stores - /\ dbVersion' = pendingDbVersion - /\ UNCHANGED <> + /\ dbVersion' = connections[transactions[tx].conn].requestedVersion + /\ UNCHANGED <> ELSE - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> -\* -\* -\* "A transaction can be aborted at any time before it is -\* finished". +\* Abort(tx) == - /\ transactions[tx].state \notin {"None", "Committing", "Finished"} + /\ transactions[tx].state \notin {"None", "Finished"} /\ transactions' = [transactions EXCEPT ![tx].state = "Finished"] /\ IF transactions[tx].mode = "versionchange" THEN + \* /\ pending_stores' = stores - /\ pendingDbVersion' = dbVersion - \* - \* "If the upgrade transaction was aborted, run the steps to close a database connection with connection" - /\ connections' = [connections EXCEPT - ![transactions[tx].conn].open = FALSE, - ![transactions[tx].conn].closed = TRUE] - /\ UNCHANGED <> + /\ connections' = [connections EXCEPT ![transactions[tx].conn].requestedVersion = oldDbVersion] + /\ dbVersion' = oldDbVersion + /\ UNCHANGED <> ELSE - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> \* @@ -378,7 +401,7 @@ CreateStore(tx, s) == /\ transactions[tx].state = "Active" /\ ~pending_stores[s] /\ pending_stores' = [pending_stores EXCEPT ![s] = TRUE] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* @@ -391,7 +414,7 @@ DeleteStore(tx, s) == /\ transactions[tx].state = "Active" /\ pending_stores[s] /\ pending_stores' = [pending_stores EXCEPT ![s] = FALSE] - /\ UNCHANGED <> + /\ UNCHANGED <> \* When all connections went through their open and close cyle: infinite stuttering. \* This is a way to avoid deadlock while bounding the spec. @@ -403,6 +426,7 @@ Next == \/ \E c \in Connections, v \in Versions: StartOpenConnection(c, v) \/ \E c \in Connections: FinishOpenConnection(c) \/ \E c \in Connections: RejectOpenConnection(c) + \/ \E c \in Connections, forced \in BOOLEAN: StartCloseConnection(c, forced) \/ \E c \in Connections: CloseConnection(c) \/ \E c \in Connections: CreateUpgradeTransaction(c) \/ \E c \in Connections, m \in {"readonly", "readwrite"}, scope \in SUBSET Stores: From f4d5a478afc96863e5bdda0b632f5af009c98f2e Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 14:27:05 +0700 Subject: [PATCH 18/23] remove redundant pendingUpgrade flag. git ignore states folder Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- .gitignore | 1 + transaction_lifecycle.tla | 12 +++--------- 2 files changed, 4 insertions(+), 9 deletions(-) diff --git a/.gitignore b/.gitignore index ae3aa0d5..a09826dd 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,4 @@ deploy_key transaction_lifecycle.out .vscode/ states/ +.tlacache/ diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index f345793c..666491b1 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -26,8 +26,6 @@ Symmetry == Permutations(Stores) \cup Permutations(Connections) \cup Permutation ConnOpen(c) == connections[c].open -ConnPendingUpgrade(c) == connections[c].pendingUpgrade - TxForConn(c) == { tx \in Transactions : Live(tx) /\ transactions[tx].conn = c } AllTxFinishedForConn(c) == @@ -67,7 +65,6 @@ TypeOK == /\ oldDbVersion \in Versions /\ connections \in [Connections -> [open: BOOLEAN, - pendingUpgrade: BOOLEAN, requestedVersion: Versions, closed: BOOLEAN, close_pending: BOOLEAN ]] @@ -137,7 +134,6 @@ DefaultTx == DefaultConn == [ open |-> FALSE, - pendingUpgrade |-> FALSE, requestedVersion|-> 0, closed |-> FALSE, close_pending |-> FALSE ] @@ -160,7 +156,6 @@ StartOpenConnection(c, requestedVersion) == /\ Len(connection_queue) < Cardinality(Connections) /\ connections' = [connections EXCEPT ![c] = [open |-> FALSE, - pendingUpgrade |-> (requestedVersion > dbVersion), requestedVersion|-> requestedVersion, closed |-> FALSE, close_pending |-> FALSE] @@ -179,8 +174,8 @@ FinishOpenConnection(c) == /\ IF connections[c].closed \* If connection was closed, \* return a newly created "AbortError" DOMException and abort these steps. - THEN connections' = [connections EXCEPT ![c].pendingUpgrade = FALSE] - ELSE connections' = [connections EXCEPT ![c].open = TRUE, ![c].pendingUpgrade = FALSE] + THEN connections' = connections + ELSE connections' = [connections EXCEPT ![c].open = TRUE] /\ connection_queue' = Tail(connection_queue) /\ UNCHANGED <> @@ -190,7 +185,6 @@ FinishOpenConnection(c) == RejectOpenConnection(c) == /\ Len(connection_queue) > 0 /\ c = Head(connection_queue) - /\ ~connections[c].pendingUpgrade /\ connections[c].requestedVersion < dbVersion /\ connections' = [connections EXCEPT ![c] = DefaultConn] /\ connection_queue' = Tail(connection_queue) @@ -207,7 +201,7 @@ CreateUpgradeTransaction(c) == /\ Len(connection_queue) > 0 /\ ~ConnOpen(c) /\ c = Head(connection_queue) - /\ ConnPendingUpgrade(c) + /\ connections[c].requestedVersion > dbVersion /\ \A other \in (Connections \ {c}): ~ConnOpen(other) /\ freeTxs # {} /\ transactions' = [transactions EXCEPT From 268a942957f3739b2ef0d30a965864aeb5b5dbbb Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 14:38:07 +0700 Subject: [PATCH 19/23] fix docs and naming Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 666491b1..81c7f340 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -149,7 +149,6 @@ Init == /\ next_tx_order = 0 \* -\* Wait until all previous requests in queue have been processed. StartOpenConnection(c, requestedVersion) == /\ connections[c] = DefaultConn /\ ~connections[c].closed @@ -166,6 +165,7 @@ StartOpenConnection(c, requestedVersion) == \* FinishOpenConnection(c) == /\ Len(connection_queue) > 0 + \* Wait until all previous requests in queue have been processed. /\ c = Head(connection_queue) /\ (connections[c].requestedVersion = dbVersion \/ connections[c].closed) \* @@ -184,6 +184,7 @@ FinishOpenConnection(c) == \* abort these steps. RejectOpenConnection(c) == /\ Len(connection_queue) > 0 + \* Wait until all previous requests in queue have been processed. /\ c = Head(connection_queue) /\ connections[c].requestedVersion < dbVersion /\ connections' = [connections EXCEPT ![c] = DefaultConn] @@ -200,6 +201,7 @@ CreateUpgradeTransaction(c) == IN /\ Len(connection_queue) > 0 /\ ~ConnOpen(c) + \* Wait until all previous requests in queue have been processed. /\ c = Head(connection_queue) /\ connections[c].requestedVersion > dbVersion /\ \A other \in (Connections \ {c}): ~ConnOpen(other) @@ -253,7 +255,7 @@ StartCloseConnection(c, forced) == \* \* "Wait for all transactions created using connection to complete. \* Once they are complete, connection is closed." -CloseConnection(c) == +FinishCloseConnection(c) == /\ connections[c].close_pending /\ AllTxFinishedForConn(c) /\ connections' = [connections EXCEPT @@ -421,7 +423,7 @@ Next == \/ \E c \in Connections: FinishOpenConnection(c) \/ \E c \in Connections: RejectOpenConnection(c) \/ \E c \in Connections, forced \in BOOLEAN: StartCloseConnection(c, forced) - \/ \E c \in Connections: CloseConnection(c) + \/ \E c \in Connections: FinishCloseConnection(c) \/ \E c \in Connections: CreateUpgradeTransaction(c) \/ \E c \in Connections, m \in {"readonly", "readwrite"}, scope \in SUBSET Stores: CreateTransaction(c, m, scope) From 5b18c7e72dce29904e61b9693f2a040b7d53e79e Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 14:57:25 +0700 Subject: [PATCH 20/23] more docs Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 35 ++++++++++++++--------------------- 1 file changed, 14 insertions(+), 21 deletions(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 81c7f340..5d7d90c4 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -180,20 +180,18 @@ FinishOpenConnection(c) == /\ UNCHANGED <> \* -\* If db’s version is greater than version, -\* abort these steps. RejectOpenConnection(c) == /\ Len(connection_queue) > 0 \* Wait until all previous requests in queue have been processed. /\ c = Head(connection_queue) + \* If db’s version is greater than version, + \* abort these steps. /\ connections[c].requestedVersion < dbVersion /\ connections' = [connections EXCEPT ![c] = DefaultConn] /\ connection_queue' = Tail(connection_queue) /\ UNCHANGED <> \* -\* Wait until all connections in openConnections are closed. -\* Run upgrade a database using connection, version and request. CreateUpgradeTransaction(c) == LET freeTxs == { t \in Transactions : ~IsCreated(t) } @@ -204,8 +202,10 @@ CreateUpgradeTransaction(c) == \* Wait until all previous requests in queue have been processed. /\ c = Head(connection_queue) /\ connections[c].requestedVersion > dbVersion + \* Wait until all connections in openConnections are closed. /\ \A other \in (Connections \ {c}): ~ConnOpen(other) /\ freeTxs # {} + \* Run upgrade a database using connection, version and request. /\ transactions' = [transactions EXCEPT ![tx] = [conn |-> c, mode |-> "versionchange", @@ -252,11 +252,10 @@ StartCloseConnection(c, forced) == /\ UNCHANGED <> \* -\* -\* "Wait for all transactions created using connection to complete. -\* Once they are complete, connection is closed." FinishCloseConnection(c) == /\ connections[c].close_pending + \* "Wait for all transactions created using connection to complete. + \* Once they are complete, connection is closed." /\ AllTxFinishedForConn(c) /\ connections' = [connections EXCEPT ![c].open = FALSE, @@ -268,13 +267,13 @@ FinishCloseConnection(c) == /\ UNCHANGED <> \* -\* If a live upgrade transaction is associated with the connection, throw. -\* If this’s close pending flag is true, then throw. CreateTransaction(c, mode, scope) == LET freeTxs == { t \in Transactions : ~IsCreated(t) } IN /\ freeTxs # {} /\ ConnOpen(c) + \* If this’s close pending flag is true, then throw. /\ ~connections[c].close_pending + \* If a live upgrade transaction is associated with the connection, throw. /\ ~HasLiveUpgradeTx(c) /\ \A s \in scope: stores[s] /\ LET tx == CHOOSE t \in freeTxs : TRUE IN @@ -292,13 +291,12 @@ CreateTransaction(c, mode, scope) == /\ UNCHANGED <> \* -\* -\* Set request’s processed flag to true. ProcessRequest(tx) == /\ CanStart(tx) /\ ConnOpen(transactions[tx].conn) /\ transactions[tx].state \in {"Active", "Inactive"} /\ transactions[tx].processed_requests < transactions[tx].requests + \* Set request’s processed flag to true. /\ transactions' = [transactions EXCEPT ![tx].processed_requests = @ + 1, ![tx].state = "Active" @@ -306,8 +304,8 @@ ProcessRequest(tx) == /\ UNCHANGED <> \* -\* Assert: transaction’s state is active. AddRequest(tx) == + \* Assert: transaction’s state is active. /\ transactions[tx].state = "Active" /\ transactions[tx].requests < MaxRequests /\ transactions' = [transactions EXCEPT ![tx].requests = @ + 1] @@ -385,28 +383,23 @@ Abort(tx) == /\ UNCHANGED <> /\ UNCHANGED <> -\* \* -\* -\* createObjectStore/deleteObjectStore "Throws -\* InvalidStateError if not called within an upgrade transaction" and require -\* the upgrade transaction to be active. CreateStore(tx, s) == /\ CanStart(tx) + \* Let transaction be database’s upgrade transaction if it is not null, or throw. /\ transactions[tx].mode = "versionchange" + \* If transaction’s state is not active, then throw. /\ transactions[tx].state = "Active" /\ ~pending_stores[s] /\ pending_stores' = [pending_stores EXCEPT ![s] = TRUE] /\ UNCHANGED <> -\* \* -\* -\* deleteObjectStore "Throws InvalidStateError if not called within an upgrade -\* transaction" and requires the upgrade transaction to be active. DeleteStore(tx, s) == /\ CanStart(tx) + \* Let transaction be database’s upgrade transaction if it is not null, or throw. /\ transactions[tx].mode = "versionchange" + \* If transaction’s state is not active, then throw. /\ transactions[tx].state = "Active" /\ pending_stores[s] /\ pending_stores' = [pending_stores EXCEPT ![s] = FALSE] From 58e034ada93505d2d325c7cdef6ca7cad8e48176 Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Mon, 5 Jan 2026 15:20:04 +0700 Subject: [PATCH 21/23] fix variable naming and some docs Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 83 ++++++++++++++++++++------------------- 1 file changed, 42 insertions(+), 41 deletions(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 5d7d90c4..66bb8b82 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -2,13 +2,14 @@ EXTENDS Naturals, Sequences, FiniteSets, TLC CONSTANTS Stores, Connections, Transactions, Versions, MaxRequests -VARIABLES transactions, stores, pending_stores, connections, dbVersion, oldDbVersion, connection_queue, next_tx_order +VARIABLES transactions, stores, pending_stores, connections, db_version, old_db_version, connection_queue, next_tx_order \* TLA+ model of the transaction lifecycle and scheduling rules from: \* - \* - -\* Note: by using only a single dbVersion, we do not model multiple databases. -Vars == << transactions, stores, pending_stores, connections, dbVersion, oldDbVersion, connection_queue, next_tx_order >> +\* Note: by using only a singular `stores` and `db_version` variables, +\* we do not model multiple databases. +Vars == << transactions, stores, pending_stores, connections, db_version, old_db_version, connection_queue, next_tx_order >> Modes == {"readonly", "readwrite", "versionchange"} TxStates == {"None", "Active", "Inactive", "Committing", "Finished"} @@ -61,11 +62,11 @@ CanStart(tx) == TypeOK == /\ stores \in [Stores -> BOOLEAN] /\ pending_stores \in [Stores -> BOOLEAN] - /\ dbVersion \in Versions - /\ oldDbVersion \in Versions + /\ db_version \in Versions + /\ old_db_version \in Versions /\ connections \in [Connections -> [open: BOOLEAN, - requestedVersion: Versions, + requested_version: Versions, closed: BOOLEAN, close_pending: BOOLEAN ]] /\ connection_queue \in Seq(Connections) @@ -104,7 +105,7 @@ ActiveUpgradeTxImpliesExclusiveConn == ActiveTransactionImpliesCorrectVersion == \A tx \in Transactions: Live(tx) => - \/ (connections[transactions[tx].conn].requestedVersion = dbVersion) + \/ (connections[transactions[tx].conn].requested_version = db_version) \* Invariant: If a transaction has processed requests, it must have been able to start. ProcessedRequestsImpliesStarted == @@ -134,7 +135,7 @@ DefaultTx == DefaultConn == [ open |-> FALSE, - requestedVersion|-> 0, + requested_version|-> 0, closed |-> FALSE, close_pending |-> FALSE ] @@ -143,31 +144,31 @@ Init == /\ stores = [s \in Stores |-> FALSE] /\ pending_stores = [s \in Stores |-> FALSE] /\ connections = [c \in Connections |-> DefaultConn] - /\ dbVersion = 0 - /\ oldDbVersion = 0 + /\ db_version = 0 + /\ old_db_version = 0 /\ connection_queue = <<>> /\ next_tx_order = 0 \* -StartOpenConnection(c, requestedVersion) == +StartOpenConnection(c, requested_version) == /\ connections[c] = DefaultConn /\ ~connections[c].closed /\ Len(connection_queue) < Cardinality(Connections) /\ connections' = [connections EXCEPT ![c] = [open |-> FALSE, - requestedVersion|-> requestedVersion, + requested_version|-> requested_version, closed |-> FALSE, close_pending |-> FALSE] ] /\ connection_queue' = Append(connection_queue, c) - /\ UNCHANGED <> + /\ UNCHANGED <> \* FinishOpenConnection(c) == /\ Len(connection_queue) > 0 \* Wait until all previous requests in queue have been processed. /\ c = Head(connection_queue) - /\ (connections[c].requestedVersion = dbVersion \/ connections[c].closed) + /\ (connections[c].requested_version = db_version \/ connections[c].closed) \* \* Wait for transaction to finish. /\ ~HasLiveUpgradeTx(c) @@ -177,7 +178,7 @@ FinishOpenConnection(c) == THEN connections' = connections ELSE connections' = [connections EXCEPT ![c].open = TRUE] /\ connection_queue' = Tail(connection_queue) - /\ UNCHANGED <> + /\ UNCHANGED <> \* RejectOpenConnection(c) == @@ -186,10 +187,10 @@ RejectOpenConnection(c) == /\ c = Head(connection_queue) \* If db’s version is greater than version, \* abort these steps. - /\ connections[c].requestedVersion < dbVersion + /\ connections[c].requested_version < db_version /\ connections' = [connections EXCEPT ![c] = DefaultConn] /\ connection_queue' = Tail(connection_queue) - /\ UNCHANGED <> + /\ UNCHANGED <> \* CreateUpgradeTransaction(c) == @@ -201,7 +202,7 @@ CreateUpgradeTransaction(c) == /\ ~ConnOpen(c) \* Wait until all previous requests in queue have been processed. /\ c = Head(connection_queue) - /\ connections[c].requestedVersion > dbVersion + /\ connections[c].requested_version > db_version \* Wait until all connections in openConnections are closed. /\ \A other \in (Connections \ {c}): ~ConnOpen(other) /\ freeTxs # {} @@ -220,8 +221,8 @@ CreateUpgradeTransaction(c) == ![c].open = TRUE ] /\ pending_stores' = stores - /\ oldDbVersion' = dbVersion - /\ dbVersion' = connections[c].requestedVersion + /\ old_db_version' = db_version + /\ db_version' = connections[c].requested_version /\ next_tx_order' = next_tx_order + 1 /\ UNCHANGED <> @@ -230,7 +231,7 @@ StartCloseConnection(c, forced) == /\ ConnOpen(c) /\ ~connections[c].close_pending /\ IF forced /\ HasLiveUpgradeTx(c) - THEN connections' = [connections EXCEPT ![c].close_pending = TRUE, ![c].requestedVersion = oldDbVersion] + THEN connections' = [connections EXCEPT ![c].close_pending = TRUE, ![c].requested_version = old_db_version] ELSE connections' = [connections EXCEPT ![c].close_pending = TRUE] /\ IF forced THEN @@ -243,12 +244,12 @@ StartCloseConnection(c, forced) == \* https://w3c.github.io/IndexedDB/#abort-an-upgrade-transaction THEN /\ pending_stores' = stores - /\ dbVersion' = oldDbVersion - /\ UNCHANGED <> + /\ db_version' = old_db_version + /\ UNCHANGED <> ELSE - /\ UNCHANGED <> + /\ UNCHANGED <> ELSE - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> \* @@ -264,7 +265,7 @@ FinishCloseConnection(c) == IF transactions[tx].conn = c THEN DefaultTx ELSE transactions[tx]] - /\ UNCHANGED <> + /\ UNCHANGED <> \* CreateTransaction(c, mode, scope) == @@ -288,7 +289,7 @@ CreateTransaction(c, mode, scope) == creation_time |-> next_tx_order] ] /\ next_tx_order' = next_tx_order + 1 - /\ UNCHANGED <> + /\ UNCHANGED <> \* ProcessRequest(tx) == @@ -301,7 +302,7 @@ ProcessRequest(tx) == ![tx].processed_requests = @ + 1, ![tx].state = "Active" ] - /\ UNCHANGED <> + /\ UNCHANGED <> \* AddRequest(tx) == @@ -309,7 +310,7 @@ AddRequest(tx) == /\ transactions[tx].state = "Active" /\ transactions[tx].requests < MaxRequests /\ transactions' = [transactions EXCEPT ![tx].requests = @ + 1] - /\ UNCHANGED <> + /\ UNCHANGED <> \* @@ -327,7 +328,7 @@ Deactivate(tx) == /\ transactions' = [transactions EXCEPT ![tx].state = "Inactive", ![tx].handled_requests = @ + 1] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* The implementation must attempt to commit an inactive transaction @@ -340,13 +341,13 @@ AutoCommit(tx) == /\ transactions[tx].requests = transactions[tx].processed_requests /\ transactions[tx].requests = transactions[tx].handled_requests /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Commit(tx) == /\ transactions[tx].state \notin {"None", "Committing", "Finished"} /\ transactions' = [transactions EXCEPT ![tx].state = "Committing"] - /\ UNCHANGED <> + /\ UNCHANGED <> \* \* "When a transaction is committed or aborted, its state is @@ -362,10 +363,10 @@ CommitDone(tx) == /\ IF transactions[tx].mode = "versionchange" THEN /\ stores' = pending_stores - /\ dbVersion' = connections[transactions[tx].conn].requestedVersion - /\ UNCHANGED <> + /\ db_version' = connections[transactions[tx].conn].requested_version + /\ UNCHANGED <> ELSE - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> \* @@ -376,11 +377,11 @@ Abort(tx) == THEN \* /\ pending_stores' = stores - /\ connections' = [connections EXCEPT ![transactions[tx].conn].requestedVersion = oldDbVersion] - /\ dbVersion' = oldDbVersion - /\ UNCHANGED <> + /\ connections' = [connections EXCEPT ![transactions[tx].conn].requested_version = old_db_version] + /\ db_version' = old_db_version + /\ UNCHANGED <> ELSE - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> \* @@ -392,7 +393,7 @@ CreateStore(tx, s) == /\ transactions[tx].state = "Active" /\ ~pending_stores[s] /\ pending_stores' = [pending_stores EXCEPT ![s] = TRUE] - /\ UNCHANGED <> + /\ UNCHANGED <> \* DeleteStore(tx, s) == @@ -403,7 +404,7 @@ DeleteStore(tx, s) == /\ transactions[tx].state = "Active" /\ pending_stores[s] /\ pending_stores' = [pending_stores EXCEPT ![s] = FALSE] - /\ UNCHANGED <> + /\ UNCHANGED <> \* When all connections went through their open and close cyle: infinite stuttering. \* This is a way to avoid deadlock while bounding the spec. From 019b1eec66394d8a645dc96312bf2c0dbfd581bc Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Tue, 6 Jan 2026 20:02:01 +0700 Subject: [PATCH 22/23] more docs and remove redundant condition Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index 66bb8b82..f36e46ac 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -23,6 +23,7 @@ Overlaps(tx1, tx2) == (transactions[tx1].stores \cap transactions[tx2].stores) # \* Transactions are ordered by their creation time. CreatedBefore(tx1, tx2) == transactions[tx1].creation_time < transactions[tx2].creation_time +\* Note: this is a model checker optimization only. Symmetry == Permutations(Stores) \cup Permutations(Connections) \cup Permutations(Transactions) ConnOpen(c) == connections[c].open @@ -57,6 +58,7 @@ CanStart(tx) == TRUE ----------------------------------------------------------------------------------------- +\* Invariants of the spec below. \* Type invariant. TypeOK == @@ -151,8 +153,9 @@ Init == \* StartOpenConnection(c, requested_version) == + \* Note: each connection can be opened only once, + \* in order to reduce the state space. /\ connections[c] = DefaultConn - /\ ~connections[c].closed /\ Len(connection_queue) < Cardinality(Connections) /\ connections' = [connections EXCEPT ![c] = [open |-> FALSE, From 404868a6d9a07f16e11155dedaa0d89d3f93b091 Mon Sep 17 00:00:00 2001 From: gterzian <2792687+gterzian@users.noreply.github.com> Date: Tue, 6 Jan 2026 20:09:54 +0700 Subject: [PATCH 23/23] readability of next Signed-off-by: gterzian <2792687+gterzian@users.noreply.github.com> --- transaction_lifecycle.tla | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/transaction_lifecycle.tla b/transaction_lifecycle.tla index f36e46ac..3b621da9 100644 --- a/transaction_lifecycle.tla +++ b/transaction_lifecycle.tla @@ -432,7 +432,8 @@ Next == \/ Commit(tx) \/ CommitDone(tx) \/ Abort(tx) - \/ \E s \in Stores: (CreateStore(tx, s) \/ DeleteStore(tx, s))) + \/ \E s \in Stores: \/ CreateStore(tx, s) + \/ DeleteStore(tx, s)) \/ AllClosed Spec == Init /\ [][Next]_Vars