Repair TLA+ ordered serialisability invariant

.github/workflows/ci-verification.yml

@@ -46,6 +46,8 @@ jobs:
 
       - run: cd tla && ./tlc.py mc consistency/MCSingleNode.tla
       - run: cd tla && ./tlc.py mc consistency/MCSingleNodeReads.tla
+      # Covers the formerly failing seven-event trace.
+      - run: cd tla && ./tlc.py --workers 1 --config consistency/MCSingleNodeOrderedSerializable.cfg mc consistency/MCSingleNode.tla
       - run: cd tla && ./tlc.py mc consistency/MCMultiNode.tla
       - run: cd tla && ./tlc.py mc consistency/MCMultiNodeReads.tla
       - run: cd tla && ./tlc.py mc consistency/MCMultiNodeReadsAlt.tla

tla/consistency/ExternalHistoryInvars.tla

@@ -235,11 +235,17 @@ CommittedRwOrderedRealTimeInv ==
                 /\ i < j 
                 => TxIDStrictlyLessThan(history[i].tx_id, history[k].tx_id)
 
-\* Each transaction observes the previous transaction in the TxID order and its own write
-\* Note that this invariant is only considers committed read-write transactions.
+\* Each later transaction in TxID order extends the earlier observation and
+\* ends with its own write. Intervening ledger writes need not have a response
+\* with an explicitly received committed status.
+\* Note that this invariant only considers committed read-write transactions.
 CommittedRwOrderedSerializableInv ==
     \A i \in 1..Len(CommittedRwResponses)-1:
-        CommittedRwResponses[i+1].observed = Append(CommittedRwResponses[i].observed, CommittedRwResponses[i+1].tx)
+        LET Earlier == CommittedRwResponses[i]
+            Later == CommittedRwResponses[i+1]
+        IN  /\ IsPrefix(Earlier.observed, Later.observed)
+            /\ Len(Earlier.observed) < Len(Later.observed)
+            /\ Last(Later.observed) = Later.tx
 
 \* Ordered speculative linearizability for committed read-write transactions is the primary consistency
 \* guarantee provided by CCF. Note that this invariant is stronger than traditional linearizability.

tla/consistency/MCSingleNodeOrderedSerializable.cfg

@@ -0,0 +1,20 @@
+SPECIFICATION MCSpecSingleNode
+
+CONSTANTS
+    FirstBranch = 1
+    HistoryLimit = 7
+
+    RwTxRequest = T_RwTxRequest
+    RwTxResponse = T_RwTxResponse
+    RoTxRequest = T_RoTxRequest
+    RoTxResponse = T_RoTxResponse
+    TxStatusReceived = T_TxStatusReceived
+
+    CommittedStatus = S_CommittedStatus
+    InvalidStatus = S_InvalidStatus
+
+INVARIANT
+    CommittedRwOrderedSerializableInv
+
+CHECK_DEADLOCK
+    FALSE