From 22802efc1b781cc17b7c52c197b276ca0869f69f Mon Sep 17 00:00:00 2001 From: achamayou Date: Sun, 9 Aug 2026 08:55:53 +0100 Subject: [PATCH 1/7] Document TLA+ ordered serialisability counterexample Add a dedicated expected-counterexample configuration and explain why the filtered committed-response property is false. Stop checking its composite invariant in normal multi-node models and cover the witness in CI. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> --- .github/workflows/ci-verification.yml | 1 + ...ttedRwOrderedSerializableCounterexample.md | 190 ++++++++++++++++++ tla/consistency/ExternalHistoryInvars.tla | 2 + tla/consistency/MCMultiNode.cfg | 1 - tla/consistency/MCMultiNodeReads.cfg | 1 - ...eNodeOrderedSerializableCounterexample.cfg | 20 ++ 6 files changed, 213 insertions(+), 2 deletions(-) create mode 100644 tla/consistency/CommittedRwOrderedSerializableCounterexample.md create mode 100644 tla/consistency/MCSingleNodeOrderedSerializableCounterexample.cfg diff --git a/.github/workflows/ci-verification.yml b/.github/workflows/ci-verification.yml index b86ec613e629..ba9640f84341 100644 --- a/.github/workflows/ci-verification.yml +++ b/.github/workflows/ci-verification.yml @@ -78,6 +78,7 @@ jobs: - run: ./tlc_debug.sh --config consistency/MCMultiNodeCommitReachability.cfg mc consistency/MCMultiNodeReads.tla - run: ./tlc_debug.sh --config consistency/MCMultiNodeInvalidReachability.cfg mc consistency/MCMultiNodeReads.tla - run: ./tlc_debug.sh --config consistency/MCMultiNodeReadsNotLinearizable.cfg mc consistency/MCMultiNodeReads.tla + - run: ./tlc_debug.sh --config consistency/MCSingleNodeOrderedSerializableCounterexample.cfg mc consistency/MCSingleNode.tla simulation-consistency: name: Simulation - Consistency diff --git a/tla/consistency/CommittedRwOrderedSerializableCounterexample.md b/tla/consistency/CommittedRwOrderedSerializableCounterexample.md new file mode 100644 index 000000000000..b0a51cd07769 --- /dev/null +++ b/tla/consistency/CommittedRwOrderedSerializableCounterexample.md @@ -0,0 +1,190 @@ +# `CommittedRwOrderedSerializableInv` counterexample + +## Result + +`CommittedRwOrderedSerializableInv` is not an invariant of the consistency +transition system. A minimal counterexample has ten actions and seven external +history events. It requires no view change, read-only transaction, invalid +status, or non-client ledger entry, so it occurs in the single-node subset of +the model. + +This is a specification-property failure, not a CCF consistency failure. The +property assumes that responses which are adjacent after filtering for +explicitly reported committed transaction IDs are also adjacent ledger +entries. The transition system does not make that assumption, and CCF does not +require it for serialisability. + +The property remains defined in `ExternalHistoryInvars.tla` as the target of +the dedicated expected-counterexample configuration. It is not checked by the +normal multi-node configurations. + +## The property + +`CommittedRwResponses` contains read-write responses whose transaction IDs +have an explicit committed-status event in `history`, sorted by transaction +ID. The property requires each adjacent pair in that filtered sequence to +differ by exactly the later transaction: + +```tla +CommittedRwOrderedSerializableInv == + \A i \in 1..Len(CommittedRwResponses)-1: + CommittedRwResponses[i+1].observed = + Append( + CommittedRwResponses[i].observed, + CommittedRwResponses[i+1].tx) +``` + +The equality is too strong. An intervening client write can be present in the +ledger and in the later response's observations without having its own +response or committed-status event in the external history. + +## Minimal counterexample + +TLC finds the following breadth-first trace. Transaction IDs are +`<>`. + +| Step | Action | Relevant result | History length | +| ---: | -------------------------------- | ------------------------------------- | -------------: | +| 1 | Request transaction `0` | Request `0` is visible | 1 | +| 2 | Request transaction `1` | Request `1` is visible | 2 | +| 3 | Request transaction `2` | Request `2` is visible | 3 | +| 4 | Execute transaction `0` | Ledger slot 1 is `(view 1, tx 0)` | 3 | +| 5 | Execute transaction `1` | Ledger slot 2 is `(view 1, tx 1)` | 3 | +| 6 | Execute transaction `2` | Ledger slot 3 is `(view 1, tx 2)` | 3 | +| 7 | Respond to transaction `0` | ID `<<1, 1>>`, observes `<<0>>` | 4 | +| 8 | Respond to transaction `2` | ID `<<1, 3>>`, observes `<<0, 1, 2>>` | 5 | +| 9 | Report transaction `0` committed | `<<1, 1>>` enters `CommittedTxIDs` | 6 | +| 10 | Report transaction `2` committed | `<<1, 3>>` enters `CommittedTxIDs` | 7 | + +There is deliberately no response or status event for transaction `1`. In the +final state: + +```tla +CommittedTxIDs = {<<1, 1>>, <<1, 3>>} + +CommittedRwResponses = + << + [tx |-> 0, tx_id |-> <<1, 1>>, observed |-> <<0>>], + [tx |-> 2, tx_id |-> <<1, 3>>, observed |-> <<0, 1, 2>>] + >> +``` + +The property checks the only adjacent pair and compares: + +```text +actual = <<0, 1, 2>> +expected = Append(<<0>>, 2) = <<0, 2>> +``` + +The intervening `1` makes the equality false. The weaker +`CommittedRwSerializableInv` still holds because `<<0>>` is a prefix of +`<<0, 1, 2>>`. + +In a real ledger, committing sequence number 3 commits the preceding ledger +prefix as well. The abstraction's `CommittedTxIDs`, however, represents +committed statuses explicitly observed by clients, not every transaction +implicitly covered by the commit watermark. Filtering responses with that set +can therefore hide transaction `1` even though later execution observes it. + +The trace is minimal for this construction: + +1. Three requests and three executions place an intervening write between the + two compared ledger entries. +2. Two responses expose the observations being compared. +3. Two committed-status events include both outer responses in + `CommittedRwResponses`. + +These are ten actions. The execution actions do not append to `history`, so +the three requests, two responses, and two statuses produce seven history +events. + +## Reproduce with TLC + +On Ubuntu, install Java, `wget`, and the repository's TLC dependencies: + +```bash +sudo apt update +sudo apt install -y default-jre wget +cd tla +python3 install_deps.py +``` + +From the `tla` directory, run the expected-counterexample wrapper: + +```bash +./tlc_debug.sh --workers 1 --difftrace \ + --config consistency/MCSingleNodeOrderedSerializableCounterexample.cfg \ + mc consistency/MCSingleNode.tla +``` + +The dedicated configuration checks only +`CommittedRwOrderedSerializableInv`, as required by `tlc_debug.sh`. TLC +reports: + +```text +Error: Invariant CommittedRwOrderedSerializableInv is violated. +... +Counterexample found as expected. +``` + +`MCSingleNode.tla` provides the smallest state space containing the violating +execution. The same execution is valid in `MCMultiNode.tla` and +`MCMultiNodeReads.tla`. + +## Why existing model checking missed it + +The normal `MCMultiNode.cfg` and `MCMultiNodeReads.cfg` configurations both +set: + +```tla +HistoryLimit = 6 +``` + +Seven external events are necessary: three requests create the ledger entries, +two responses provide the pair to compare, and two committed-status events +include that pair in the filtered sequence. With `HistoryLimit = 6`, TLC +exhaustively checks the bounded state graph but cannot reach the violating +state. Raising only this bound to 7 exposes the counterexample. + +The bound predates the property. It was established with the original +consistency specification in commit +[`724c827247`](https://github.com/microsoft/CCF/commit/724c827247) +([PR #5699](https://github.com/microsoft/CCF/pull/5699)). Commit +[`bf4fcff670`](https://github.com/microsoft/CCF/commit/bf4fcff670) +([PR #6185](https://github.com/microsoft/CCF/pull/6185)) later introduced +`CommittedRwOrderedSpecLinearizableInv` and added it to the two multi-node +model-checking configurations without changing `HistoryLimit`. + +The other configurations did not close the gap: + +- The single-node configurations used a history limit of 7 but did not check + the new property. +- `MCMultiNodeReadsAlt.cfg` used a larger history limit but did not check the + new property. +- The configurations which checked the property remained capped at 6. + +This was a scope-boundary blind spot, not a TLC search failure. + +## Why the property fails + +PR #6185 intended to state that committed read-write transactions are +serialisable in transaction-ID order. Its formula selects only responses with +explicitly observed committed statuses, sorts that filtered set, and then +treats adjacent elements as adjacent ledger writes. + +Those notions of adjacency differ: + +- Adjacent in `CommittedRwResponses` means no other response with an explicit + committed-status event is between the pair. +- Adjacent in the ledger means no client write is between their sequence + numbers. + +The transition system permits a write to execute without a response or status +event. Such a write is absent from `CommittedRwResponses` but remains present +in every later observation of that ledger prefix. The `Append` equality +therefore cannot hold in general. + +A replacement property requires a separate design decision. For example, it +could allow an observed suffix between the compared writes, or the abstraction +could distinguish actual ledger commitment from client receipt of a committed +status. This counterexample does not assert a replacement guarantee. diff --git a/tla/consistency/ExternalHistoryInvars.tla b/tla/consistency/ExternalHistoryInvars.tla index 6714567bb484..abca570e9f7e 100644 --- a/tla/consistency/ExternalHistoryInvars.tla +++ b/tla/consistency/ExternalHistoryInvars.tla @@ -237,6 +237,8 @@ CommittedRwOrderedRealTimeInv == \* 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. +\* This property is false when the committed-response filter hides an +\* intervening ledger write. See CommittedRwOrderedSerializableCounterexample.md. CommittedRwOrderedSerializableInv == \A i \in 1..Len(CommittedRwResponses)-1: CommittedRwResponses[i+1].observed = Append(CommittedRwResponses[i].observed, CommittedRwResponses[i+1].tx) diff --git a/tla/consistency/MCMultiNode.cfg b/tla/consistency/MCMultiNode.cfg index 21f13795e590..5af3c3f99baa 100644 --- a/tla/consistency/MCMultiNode.cfg +++ b/tla/consistency/MCMultiNode.cfg @@ -27,7 +27,6 @@ INVARIANTS CommittedRwSerializableInv InvalidNotObservedByCommittedInv AtMostOnceObservedInv - CommittedRwOrderedSpecLinearizableInv CHECK_DEADLOCK FALSE \ No newline at end of file diff --git a/tla/consistency/MCMultiNodeReads.cfg b/tla/consistency/MCMultiNodeReads.cfg index 7079fead07a1..1a13c6368f50 100644 --- a/tla/consistency/MCMultiNodeReads.cfg +++ b/tla/consistency/MCMultiNodeReads.cfg @@ -27,7 +27,6 @@ INVARIANTS CommittedRwSerializableInv InvalidNotObservedByCommittedInv AtMostOnceObservedInv - CommittedRwOrderedSpecLinearizableInv CHECK_DEADLOCK FALSE \ No newline at end of file diff --git a/tla/consistency/MCSingleNodeOrderedSerializableCounterexample.cfg b/tla/consistency/MCSingleNodeOrderedSerializableCounterexample.cfg new file mode 100644 index 000000000000..959ce4e3d197 --- /dev/null +++ b/tla/consistency/MCSingleNodeOrderedSerializableCounterexample.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 From a77529db28a7ee82bc2790c9f3dfdfc3212d9ebd Mon Sep 17 00:00:00 2001 From: achamayou Date: Sun, 9 Aug 2026 10:41:53 +0100 Subject: [PATCH 2/7] Clarify expected TLC invariant failure Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> --- .github/workflows/ci-verification.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/ci-verification.yml b/.github/workflows/ci-verification.yml index ba9640f84341..89a01cdbeb17 100644 --- a/.github/workflows/ci-verification.yml +++ b/.github/workflows/ci-verification.yml @@ -78,6 +78,8 @@ jobs: - run: ./tlc_debug.sh --config consistency/MCMultiNodeCommitReachability.cfg mc consistency/MCMultiNodeReads.tla - run: ./tlc_debug.sh --config consistency/MCMultiNodeInvalidReachability.cfg mc consistency/MCMultiNodeReads.tla - run: ./tlc_debug.sh --config consistency/MCMultiNodeReadsNotLinearizable.cfg mc consistency/MCMultiNodeReads.tla + # Expected-failure check: tlc_debug.sh succeeds only when TLC reports: + # Error: Invariant CommittedRwOrderedSerializableInv is violated. - run: ./tlc_debug.sh --config consistency/MCSingleNodeOrderedSerializableCounterexample.cfg mc consistency/MCSingleNode.tla simulation-consistency: From f9952a652856452ffce5b7e0f966ee656e87f656 Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Sun, 9 Aug 2026 12:22:24 +0100 Subject: [PATCH 3/7] Add trace-backed counterexample diagrams Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> --- .github/workflows/ci-verification.yml | 5 +- ...ttedRwOrderedSerializableCounterexample.md | 191 +++++++++++++++--- ...iNodeOrderedSerializableCounterexample.cfg | 21 ++ 3 files changed, 184 insertions(+), 33 deletions(-) create mode 100644 tla/consistency/MCMultiNodeOrderedSerializableCounterexample.cfg diff --git a/.github/workflows/ci-verification.yml b/.github/workflows/ci-verification.yml index 89a01cdbeb17..efa04156deac 100644 --- a/.github/workflows/ci-verification.yml +++ b/.github/workflows/ci-verification.yml @@ -78,9 +78,12 @@ jobs: - run: ./tlc_debug.sh --config consistency/MCMultiNodeCommitReachability.cfg mc consistency/MCMultiNodeReads.tla - run: ./tlc_debug.sh --config consistency/MCMultiNodeInvalidReachability.cfg mc consistency/MCMultiNodeReads.tla - run: ./tlc_debug.sh --config consistency/MCMultiNodeReadsNotLinearizable.cfg mc consistency/MCMultiNodeReads.tla - # Expected-failure check: tlc_debug.sh succeeds only when TLC reports: + # tlc_debug.sh converts this exact TLC failure into success: # Error: Invariant CommittedRwOrderedSerializableInv is violated. - run: ./tlc_debug.sh --config consistency/MCSingleNodeOrderedSerializableCounterexample.cfg mc consistency/MCSingleNode.tla + # tlc_debug.sh converts this exact TLC failure into success: + # Error: Invariant CommittedRwOrderedSerializableInv is violated. + - run: ./tlc_debug.sh --config consistency/MCMultiNodeOrderedSerializableCounterexample.cfg mc consistency/MCMultiNode.tla simulation-consistency: name: Simulation - Consistency diff --git a/tla/consistency/CommittedRwOrderedSerializableCounterexample.md b/tla/consistency/CommittedRwOrderedSerializableCounterexample.md index b0a51cd07769..3e4560304db7 100644 --- a/tla/consistency/CommittedRwOrderedSerializableCounterexample.md +++ b/tla/consistency/CommittedRwOrderedSerializableCounterexample.md @@ -2,11 +2,16 @@ ## Result -`CommittedRwOrderedSerializableInv` is not an invariant of the consistency -transition system. A minimal counterexample has ten actions and seven external -history events. It requires no view change, read-only transaction, invalid -status, or non-client ledger entry, so it occurs in the single-node subset of -the model. +`CommittedRwOrderedSerializableInv` is not an invariant of either bounded +consistency transition system. With `HistoryLimit = 7`, TLC reports the same +shortest counterexample from both the single-node model and the multi-node +model with its normal `ViewLimit = 3`. + +The trace has exactly seven external history events, ten transitions, and +eleven states when the initial state is included. Seven is the event count, +not the transition count. The trace requires no view change, read-only +transaction, invalid status, or non-client ledger entry, so it occurs in the +single-node action subset of the multi-node model. This is a specification-property failure, not a CCF consistency failure. The property assumes that responses which are adjacent after filtering for @@ -15,8 +20,8 @@ entries. The transition system does not make that assumption, and CCF does not require it for serialisability. The property remains defined in `ExternalHistoryInvars.tla` as the target of -the dedicated expected-counterexample configuration. It is not checked by the -normal multi-node configurations. +the two dedicated expected-counterexample configurations. It is not checked +by the normal multi-node configurations. ## The property @@ -38,23 +43,73 @@ The equality is too strong. An intervening client write can be present in the ledger and in the later response's observations without having its own response or committed-status event in the external history. -## Minimal counterexample - -TLC finds the following breadth-first trace. Transaction IDs are -`<>`. +## Single-node trace + +TLC finds the following deterministic breadth-first trace with one worker. +Transaction IDs are `<>`. + +```mermaid +flowchart TB + subgraph history["External history: 7 events"] + direction LR + h1["1: request tx 0
transition 1"] + h2["2: request tx 1
transition 2"] + h3["3: request tx 2
transition 3"] + h4["4: response tx 0
ID <<1,1>>
observed <<0>>
transition 7"] + h5["5: response tx 2
ID <<1,3>>
observed <<0,1,2>>
transition 8"] + h6["6: status <<1,1>>
committed
transition 9"] + h7["7: status <<1,3>>
committed
transition 10"] + h1 --> h2 + h2 --> h3 + h3 --> h4 + h4 --> h5 + h5 --> h6 + h6 --> h7 + end + + subgraph ledger["Ledger branch 1"] + direction LR + l1["slot 1: tx 0
transition 4"] + l2["slot 2: tx 1
transition 5"] + l3["slot 3: tx 2
transition 6"] + l1 --> l2 + l2 --> l3 + end + + h1 -.-> l1 + h2 -.-> l2 + h3 -.-> l3 + l1 -.-> h4 + l3 -.-> h5 + l2 -.-> omitted["OMITTED FROM HISTORY
no response for tx 1
no status for tx 1"] + + subgraph comparison["Invariant comparison at state 11"] + direction LR + expected["expected = Append(<<0>>, 2)
= <<0,2>>"] + mismatch["<<0,1,2>> != <<0,2>>"] + actual["actual = <<0,1,2>>"] + expected --> mismatch + actual --> mismatch + end + + h4 -.-> expected + h5 -.-> actual +``` -| Step | Action | Relevant result | History length | -| ---: | -------------------------------- | ------------------------------------- | -------------: | -| 1 | Request transaction `0` | Request `0` is visible | 1 | -| 2 | Request transaction `1` | Request `1` is visible | 2 | -| 3 | Request transaction `2` | Request `2` is visible | 3 | -| 4 | Execute transaction `0` | Ledger slot 1 is `(view 1, tx 0)` | 3 | -| 5 | Execute transaction `1` | Ledger slot 2 is `(view 1, tx 1)` | 3 | -| 6 | Execute transaction `2` | Ledger slot 3 is `(view 1, tx 2)` | 3 | -| 7 | Respond to transaction `0` | ID `<<1, 1>>`, observes `<<0>>` | 4 | -| 8 | Respond to transaction `2` | ID `<<1, 3>>`, observes `<<0, 1, 2>>` | 5 | -| 9 | Report transaction `0` committed | `<<1, 1>>` enters `CommittedTxIDs` | 6 | -| 10 | Report transaction `2` committed | `<<1, 3>>` enters `CommittedTxIDs` | 7 | +| Transition | State reached | TLC action | Relevant result | History length | +| ---------: | ------------: | --------------------------------- | ------------------------------------- | -------------: | +| 1 | 2 | `MCRwTxRequestAction` for `0` | Request `0` is visible | 1 | +| 2 | 3 | `MCRwTxRequestAction` for `1` | Request `1` is visible | 2 | +| 3 | 4 | `MCRwTxRequestAction` for `2` | Request `2` is visible | 3 | +| 4 | 5 | `RwTxExecuteAction` for `0` | Ledger slot 1 is `(view 1, tx 0)` | 3 | +| 5 | 6 | `RwTxExecuteAction` for `1` | Ledger slot 2 is `(view 1, tx 1)` | 3 | +| 6 | 7 | `RwTxExecuteAction` for `2` | Ledger slot 3 is `(view 1, tx 2)` | 3 | +| 7 | 8 | `MCRwTxResponseAction` for `0` | ID `<<1, 1>>`, observes `<<0>>` | 4 | +| 8 | 9 | `MCRwTxResponseAction` for `2` | ID `<<1, 3>>`, observes `<<0, 1, 2>>` | 5 | +| 9 | 10 | `MCStatusCommittedResponseAction` | `<<1, 1>>` enters `CommittedTxIDs` | 6 | +| 10 | 11 | `MCStatusCommittedResponseAction` | `<<1, 3>>` enters `CommittedTxIDs` | 7 | + +State 1 is the initial state. Ten transitions therefore reach state 11. There is deliberately no response or status event for transaction `1`. In the final state: @@ -94,10 +149,65 @@ The trace is minimal for this construction: 3. Two committed-status events include both outer responses in `CommittedRwResponses`. -These are ten actions. The execution actions do not append to `history`, so -the three requests, two responses, and two statuses produce seven history +These are ten transitions. The execution actions do not append to `history`, +so the three requests, two responses, and two statuses produce seven history events. +## Multi-node trace + +The dedicated multi-node configuration uses: + +```tla +SPECIFICATION MCSpecMultiNode +HistoryLimit = 7 +ViewLimit = 3 +``` + +At these bounds TLC produces the same values and action order as the +single-node run. Every selected action comes from +`MCNextSingleNodeAction`. The multi-node-only truncation and invalid-status +actions are enabled by the specification but are not selected by this +shortest counterexample. + +```mermaid +flowchart TB + subgraph multi["MCNextMultiNodeAction"] + direction TB + subgraph single["Included subset: MCNextSingleNodeAction"] + direction LR + s1["State 1
empty history
one empty branch"] + s4["State 4
requests 0, 1, 2"] + s7["State 7
view 1 slots contain 0, 1, 2"] + s9["State 9
responses for 0 and 2"] + s11["State 11
7 history events
invariant violated"] + s1 -->|3 request transitions| s4 + s4 -->|3 execute transitions| s7 + s7 -->|2 response transitions| s9 + s9 -->|2 committed-status transitions| s11 + end + + truncate["MCTruncateLedgerAction
available, not selected"] + invalid["MCStatusInvalidResponseAction
available, not selected"] + end + + s7 -.-> view["ledgerBranches has length 1 throughout
view 1 only; no view change"] + s11 --> result["<<0,1,2>> != <<0,2>>"] +``` + +This is an important containment result rather than a weakness in the +multi-node check. `MCMultiNode.tla` defines: + +```tla +MCNextMultiNodeAction == + \/ MCNextSingleNodeAction + \/ MCTruncateLedgerAction + \/ MCStatusInvalidResponseAction +``` + +Consequently every single-node behavior is also an allowed multi-node +behavior. A property claimed for all multi-node behaviors must hold for the +embedded subset even when the additional view-change actions are unused. + ## Reproduce with TLC On Ubuntu, install Java, `wget`, and the repository's TLC dependencies: @@ -109,15 +219,21 @@ cd tla python3 install_deps.py ``` -From the `tla` directory, run the expected-counterexample wrapper: +From the `tla` directory, run both expected-counterexample checks: ```bash ./tlc_debug.sh --workers 1 --difftrace \ + --trace-name single-node-ordered-serializable \ --config consistency/MCSingleNodeOrderedSerializableCounterexample.cfg \ mc consistency/MCSingleNode.tla + +./tlc_debug.sh --workers 1 --difftrace \ + --trace-name multi-node-ordered-serializable \ + --config consistency/MCMultiNodeOrderedSerializableCounterexample.cfg \ + mc consistency/MCMultiNode.tla ``` -The dedicated configuration checks only +Each dedicated configuration checks only `CommittedRwOrderedSerializableInv`, as required by `tlc_debug.sh`. TLC reports: @@ -127,9 +243,10 @@ Error: Invariant CommittedRwOrderedSerializableInv is violated. Counterexample found as expected. ``` -`MCSingleNode.tla` provides the smallest state space containing the violating -execution. The same execution is valid in `MCMultiNode.tla` and -`MCMultiNodeReads.tla`. +The single-node command generates 12,390 states and 8,846 distinct states. +The multi-node command at `ViewLimit = 3` generates 134,561 states and 63,978 +distinct states. Both stop at the same state 11 violation. Counts are from +deterministic one-worker runs with the repository-installed TLC dependencies. ## Why existing model checking missed it @@ -152,8 +269,18 @@ consistency specification in commit ([PR #5699](https://github.com/microsoft/CCF/pull/5699)). Commit [`bf4fcff670`](https://github.com/microsoft/CCF/commit/bf4fcff670) ([PR #6185](https://github.com/microsoft/CCF/pull/6185)) later introduced -`CommittedRwOrderedSpecLinearizableInv` and added it to the two multi-node -model-checking configurations without changing `HistoryLimit`. +`CommittedRwOrderedSpecLinearizableInv` as a multi-node ordered speculative +linearizability check. That change wired the composite invariant only into +`MCMultiNode.cfg` and `MCMultiNodeReads.cfg`; it did not add it to the +single-node configuration or change `HistoryLimit`. + +The configuration placement does not limit the property's domain. The +multi-node model extends the single-node model, and +`MCNextMultiNodeAction` explicitly contains `MCNextSingleNodeAction`. +`MCSingleNodeOrderedSerializableCounterexample.cfg` is therefore a valid +minimal diagnostic witness for a property that was originally enabled only +in multi-node configurations. The dedicated multi-node run independently +confirms that the same witness is present at the original `ViewLimit = 3`. The other configurations did not close the gap: diff --git a/tla/consistency/MCMultiNodeOrderedSerializableCounterexample.cfg b/tla/consistency/MCMultiNodeOrderedSerializableCounterexample.cfg new file mode 100644 index 000000000000..8cb61f02dfa7 --- /dev/null +++ b/tla/consistency/MCMultiNodeOrderedSerializableCounterexample.cfg @@ -0,0 +1,21 @@ +SPECIFICATION MCSpecMultiNode + +CONSTANTS + FirstBranch = 1 + HistoryLimit = 7 + ViewLimit = 3 + + 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 From 27116d2a4e65c516a541df1eadfe7cf4617d9575 Mon Sep 17 00:00:00 2001 From: achamayou Date: Sun, 9 Aug 2026 15:29:36 +0100 Subject: [PATCH 4/7] Clarify counterexample diagrams Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> --- ...ttedRwOrderedSerializableCounterexample.md | 124 ++++++++---------- 1 file changed, 56 insertions(+), 68 deletions(-) diff --git a/tla/consistency/CommittedRwOrderedSerializableCounterexample.md b/tla/consistency/CommittedRwOrderedSerializableCounterexample.md index 3e4560304db7..3e5d2ed3212d 100644 --- a/tla/consistency/CommittedRwOrderedSerializableCounterexample.md +++ b/tla/consistency/CommittedRwOrderedSerializableCounterexample.md @@ -46,56 +46,32 @@ response or committed-status event in the external history. ## Single-node trace TLC finds the following deterministic breadth-first trace with one worker. -Transaction IDs are `<>`. +Transaction IDs are `<>`. The git graph projects the +final state in transaction order; the table below gives the exact transition +and external-event order. The `main` line is the actual ledger order annotated +with response observations. The `filtered` line branches at transaction `0` +and shows the pair that the invariant constructs after filtering out +transaction `1`. ```mermaid -flowchart TB - subgraph history["External history: 7 events"] - direction LR - h1["1: request tx 0
transition 1"] - h2["2: request tx 1
transition 2"] - h3["3: request tx 2
transition 3"] - h4["4: response tx 0
ID <<1,1>>
observed <<0>>
transition 7"] - h5["5: response tx 2
ID <<1,3>>
observed <<0,1,2>>
transition 8"] - h6["6: status <<1,1>>
committed
transition 9"] - h7["7: status <<1,3>>
committed
transition 10"] - h1 --> h2 - h2 --> h3 - h3 --> h4 - h4 --> h5 - h5 --> h6 - h6 --> h7 - end - - subgraph ledger["Ledger branch 1"] - direction LR - l1["slot 1: tx 0
transition 4"] - l2["slot 2: tx 1
transition 5"] - l3["slot 3: tx 2
transition 6"] - l1 --> l2 - l2 --> l3 - end - - h1 -.-> l1 - h2 -.-> l2 - h3 -.-> l3 - l1 -.-> h4 - l3 -.-> h5 - l2 -.-> omitted["OMITTED FROM HISTORY
no response for tx 1
no status for tx 1"] - - subgraph comparison["Invariant comparison at state 11"] - direction LR - expected["expected = Append(<<0>>, 2)
= <<0,2>>"] - mismatch["<<0,1,2>> != <<0,2>>"] - actual["actual = <<0,1,2>>"] - expected --> mismatch - actual --> mismatch - end - - h4 -.-> expected - h5 -.-> actual +%%{init: {"theme":"base","themeVariables":{"git0":"#0072B2","git1":"#E69F00","gitInv1":"#CC79A7","gitBranchLabel0":"#FFFFFF","gitBranchLabel1":"#000000","commitLabelColor":"#000000","commitLabelBackground":"#FFFFFF"},"gitGraph":{"showBranches":true,"showCommitLabel":true,"rotateCommitLabel":true}}}%% +gitGraph LR: + commit id: "tx0: observed #60;#60;0#62;#62;" type: NORMAL + branch filtered + checkout main + commit id: "tx1: ledger; no response/status" type: REVERSE + commit id: "tx2 actual: observed #60;#60;0,1,2#62;#62;" type: NORMAL + checkout filtered + commit id: "tx2 expected: Append(#60;#60;0#62;#62;,2)#61;#60;#60;0,2#62;#62;" type: HIGHLIGHT ``` +**Legend:** Blue `main` and circular `NORMAL` markers show the actual ledger +and response observations. The crossed `REVERSE` marker is not a rollback: +transaction `1` is in the ledger and in transaction `2`'s observation, but has +no response or status event. Orange `filtered` is a logical projection, not a +second ledger branch. Its rectangular `HIGHLIGHT` marker is the false +expectation where `CommittedRwOrderedSerializableInv` breaks. + | Transition | State reached | TLC action | Relevant result | History length | | ---------: | ------------: | --------------------------------- | ------------------------------------- | -------------: | | 1 | 2 | `MCRwTxRequestAction` for `0` | Request `0` is visible | 1 | @@ -170,30 +146,42 @@ actions are enabled by the specification but are not selected by this shortest counterexample. ```mermaid -flowchart TB - subgraph multi["MCNextMultiNodeAction"] - direction TB - subgraph single["Included subset: MCNextSingleNodeAction"] - direction LR - s1["State 1
empty history
one empty branch"] - s4["State 4
requests 0, 1, 2"] - s7["State 7
view 1 slots contain 0, 1, 2"] - s9["State 9
responses for 0 and 2"] - s11["State 11
7 history events
invariant violated"] - s1 -->|3 request transitions| s4 - s4 -->|3 execute transitions| s7 - s7 -->|2 response transitions| s9 - s9 -->|2 committed-status transitions| s11 - end - - truncate["MCTruncateLedgerAction
available, not selected"] - invalid["MCStatusInvalidResponseAction
available, not selected"] - end - - s7 -.-> view["ledgerBranches has length 1 throughout
view 1 only; no view change"] - s11 --> result["<<0,1,2>> != <<0,2>>"] +%%{init: {"theme":"base","themeVariables":{"git0":"#0072B2","git1":"#E69F00","gitInv1":"#CC79A7","gitBranchLabel0":"#FFFFFF","gitBranchLabel1":"#000000","commitLabelColor":"#000000","commitLabelBackground":"#FFFFFF"},"gitGraph":{"showBranches":true,"showCommitLabel":true,"rotateCommitLabel":true}}}%% +gitGraph LR: + commit id: "tx0 view 1: observed #60;#60;0#62;#62;" type: NORMAL + branch filtered + checkout main + commit id: "tx1 view 1: ledger; no response/status" type: REVERSE + commit id: "tx2 actual view 1: observed #60;#60;0,1,2#62;#62;" type: NORMAL + checkout filtered + commit id: "tx2 expected: Append(#60;#60;0#62;#62;,2)#61;#60;#60;0,2#62;#62;" type: HIGHLIGHT ``` +**Legend:** Blue `main` contains only view `1` and shows the same actual +transaction order as the single-node witness. The crossed transaction `1` is +present in the ledger and later observation but lacks a response or status. +Orange `filtered` is the invariant's projection, not another ledger view; its +rectangular `HIGHLIGHT` marker is the failing expectation. No view change is +drawn because none occurs. + +The configured multi-node action set still contains unused alternatives: + +```mermaid +%%{init: {"theme":"base","themeVariables":{"primaryColor":"#FFFFFF","primaryTextColor":"#000000","primaryBorderColor":"#333333","lineColor":"#333333"}}}%% +flowchart LR + multi["MCNextMultiNodeAction
ViewLimit = 3"] -->|contains| single["MCNextSingleNodeAction
selected for all 10 transitions"] + multi -.->|also contains| extra["View-change / invalid-status alternatives
MCTruncateLedgerAction
MCStatusInvalidResponseAction
available; selected 0 times"] + classDef root fill:#FFFFFF,stroke:#333333,stroke-width:2px,color:#000000 + classDef selected fill:#0072B2,stroke:#003B5C,stroke-width:2px,color:#FFFFFF + classDef unused fill:#E69F00,stroke:#7A5200,stroke-width:2px,color:#000000 + class multi root + class single selected + class extra unused +``` + +**Legend:** Solid blue is the selected single-node subset. Dashed orange is +available under `MCSpecMultiNode` but unused by this witness. + This is an important containment result rather than a weakness in the multi-node check. `MCMultiNode.tla` defines: From a9d18155844d90b33d830c23b939fb58599d6fd2 Mon Sep 17 00:00:00 2001 From: achamayou Date: Sun, 9 Aug 2026 15:45:54 +0100 Subject: [PATCH 5/7] Replace counterexample diagrams with linear trace Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> --- ...ttedRwOrderedSerializableCounterexample.md | 131 +++++++++--------- 1 file changed, 67 insertions(+), 64 deletions(-) diff --git a/tla/consistency/CommittedRwOrderedSerializableCounterexample.md b/tla/consistency/CommittedRwOrderedSerializableCounterexample.md index 3e5d2ed3212d..3141bc2b108e 100644 --- a/tla/consistency/CommittedRwOrderedSerializableCounterexample.md +++ b/tla/consistency/CommittedRwOrderedSerializableCounterexample.md @@ -43,34 +43,61 @@ The equality is too strong. An intervening client write can be present in the ledger and in the later response's observations without having its own response or committed-status event in the external history. -## Single-node trace +## Shared deterministic trace -TLC finds the following deterministic breadth-first trace with one worker. -Transaction IDs are `<>`. The git graph projects the -final state in transaction order; the table below gives the exact transition -and external-event order. The `main` line is the actual ledger order annotated -with response observations. The `filtered` line branches at transaction `0` -and shows the pair that the invariant constructs after filtering out -transaction `1`. +With one worker, both the single-node configuration and the `MCMultiNode.tla` +configuration produce this exact deterministic breadth-first history. The +diagram is the complete transition order, not a projection: its single path +contains all ten transitions and ends at the state 11 violation. Transaction +IDs are `<>`. ```mermaid -%%{init: {"theme":"base","themeVariables":{"git0":"#0072B2","git1":"#E69F00","gitInv1":"#CC79A7","gitBranchLabel0":"#FFFFFF","gitBranchLabel1":"#000000","commitLabelColor":"#000000","commitLabelBackground":"#FFFFFF"},"gitGraph":{"showBranches":true,"showCommitLabel":true,"rotateCommitLabel":true}}}%% -gitGraph LR: - commit id: "tx0: observed #60;#60;0#62;#62;" type: NORMAL - branch filtered - checkout main - commit id: "tx1: ledger; no response/status" type: REVERSE - commit id: "tx2 actual: observed #60;#60;0,1,2#62;#62;" type: NORMAL - checkout filtered - commit id: "tx2 expected: Append(#60;#60;0#62;#62;,2)#61;#60;#60;0,2#62;#62;" type: HIGHLIGHT +%%{init: {"theme":"base","themeVariables":{"fontFamily":"Arial, sans-serif","lineColor":"#333333","primaryTextColor":"#111111"}}}%% +flowchart TB + t1["1. HISTORY 1 - REQUEST tx0
MCRwTxRequestAction; history length 1"] + t2["2. HISTORY 2 - REQUEST tx1
MCRwTxRequestAction; history length 2"] + t3["3. HISTORY 3 - REQUEST tx2
MCRwTxRequestAction; history length 3"] + t4(["4. INTERNAL - EXECUTE tx0
view 1, slot 1; history remains 3"]) + t5(["5. INTERNAL - EXECUTE tx1
view 1, slot 2; history remains 3
Present in ledger; no later response or status"]) + t6(["6. INTERNAL - EXECUTE tx2
view 1, slot 3; history remains 3"]) + t7{{"7. HISTORY 4 - RESPONSE tx0
ID <<1, 1>>; observed <<0>>
Retained once committed at transition 9"}} + t8{{"8. HISTORY 5 - RESPONSE tx2
ID <<1, 3>>; observed <<0, 1 UNEXPECTED, 2>>
Retained once committed at transition 10; unexpected tx1 contribution"}} + t9{{"9. HISTORY 6 - COMMITTED STATUS <<1, 1>>
MCStatusCommittedResponseAction; retains response tx0"}} + t10{{"10. HISTORY 7 - COMMITTED STATUS <<1, 3>>
MCStatusCommittedResponseAction; retains response tx2"}} + failure[["ANALYSIS - INVARIANT VIOLATION
Filtering produces responses tx0 and tx2; tx1 has no response/status.
expected Append(<<0>>, 2) = <<0, 2>>
actual = <<0, 1 UNEXPECTED, 2>>
CommittedRwOrderedSerializableInv is false."]] + + t1 --> t2 + t2 --> t3 + t3 --> t4 + t4 --> t5 + t5 --> t6 + t6 --> t7 + t7 --> t8 + t8 --> t9 + t9 --> t10 + t10 --> failure + + classDef external fill:#D9EAF7,stroke:#0072B2,stroke-width:3px,color:#111111 + classDef internal fill:#E5E7EB,stroke:#4B5563,stroke-width:3px,color:#111111 + classDef intervening fill:#FDE7B0,stroke:#A85D00,stroke-width:4px,color:#111111 + classDef retained fill:#DFF2E1,stroke:#007A3D,stroke-width:3px,color:#111111 + classDef unexpected fill:#DFF2E1,stroke:#B00020,stroke-width:5px,color:#111111 + classDef violation fill:#FFD6D6,stroke:#B00020,stroke-width:6px,color:#660000 + class t1,t2,t3 external + class t4,t6 internal + class t5 intervening + class t7,t9,t10 retained + class t8 unexpected + class failure violation + linkStyle default stroke:#333333,stroke-width:3px ``` -**Legend:** Blue `main` and circular `NORMAL` markers show the actual ledger -and response observations. The crossed `REVERSE` marker is not a rollback: -transaction `1` is in the ledger and in transaction `2`'s observation, but has -no response or status event. Orange `filtered` is a logical projection, not a -second ledger branch. Its rectangular `HIGHLIGHT` marker is the false -expectation where `CommittedRwOrderedSerializableInv` breaks. +**Legend:** Blue rectangles are ordinary external history events. Gray rounded +nodes are internal execute actions and do not change `history`. The amber +rounded node marks transaction `1`, which is present in the ledger but absent +from response/status filtering. Green hexagons are response/status events +retained by that filtering. Red text and heavy red borders mark the unexpected +transaction `1` contribution and the final invariant violation. | Transition | State reached | TLC action | Relevant result | History length | | ---------: | ------------: | --------------------------------- | ------------------------------------- | -------------: | @@ -129,58 +156,34 @@ These are ten transitions. The execution actions do not append to `history`, so the three requests, two responses, and two statuses produce seven history events. -## Multi-node trace +## Configuration-specific reproduction -The dedicated multi-node configuration uses: +### Single-node configuration + +The dedicated single-node configuration uses: ```tla -SPECIFICATION MCSpecMultiNode +SPECIFICATION MCSpecSingleNode HistoryLimit = 7 -ViewLimit = 3 ``` -At these bounds TLC produces the same values and action order as the -single-node run. Every selected action comes from -`MCNextSingleNodeAction`. The multi-node-only truncation and invalid-status -actions are enabled by the specification but are not selected by this -shortest counterexample. - -```mermaid -%%{init: {"theme":"base","themeVariables":{"git0":"#0072B2","git1":"#E69F00","gitInv1":"#CC79A7","gitBranchLabel0":"#FFFFFF","gitBranchLabel1":"#000000","commitLabelColor":"#000000","commitLabelBackground":"#FFFFFF"},"gitGraph":{"showBranches":true,"showCommitLabel":true,"rotateCommitLabel":true}}}%% -gitGraph LR: - commit id: "tx0 view 1: observed #60;#60;0#62;#62;" type: NORMAL - branch filtered - checkout main - commit id: "tx1 view 1: ledger; no response/status" type: REVERSE - commit id: "tx2 actual view 1: observed #60;#60;0,1,2#62;#62;" type: NORMAL - checkout filtered - commit id: "tx2 expected: Append(#60;#60;0#62;#62;,2)#61;#60;#60;0,2#62;#62;" type: HIGHLIGHT -``` +It produces the shared ten-transition, eleven-state trace above. -**Legend:** Blue `main` contains only view `1` and shows the same actual -transaction order as the single-node witness. The crossed transaction `1` is -present in the ledger and later observation but lacks a response or status. -Orange `filtered` is the invariant's projection, not another ledger view; its -rectangular `HIGHLIGHT` marker is the failing expectation. No view change is -drawn because none occurs. +### Multi-node configuration -The configured multi-node action set still contains unused alternatives: +The dedicated `MCMultiNode.tla` configuration uses: -```mermaid -%%{init: {"theme":"base","themeVariables":{"primaryColor":"#FFFFFF","primaryTextColor":"#000000","primaryBorderColor":"#333333","lineColor":"#333333"}}}%% -flowchart LR - multi["MCNextMultiNodeAction
ViewLimit = 3"] -->|contains| single["MCNextSingleNodeAction
selected for all 10 transitions"] - multi -.->|also contains| extra["View-change / invalid-status alternatives
MCTruncateLedgerAction
MCStatusInvalidResponseAction
available; selected 0 times"] - classDef root fill:#FFFFFF,stroke:#333333,stroke-width:2px,color:#000000 - classDef selected fill:#0072B2,stroke:#003B5C,stroke-width:2px,color:#FFFFFF - classDef unused fill:#E69F00,stroke:#7A5200,stroke-width:2px,color:#000000 - class multi root - class single selected - class extra unused +```tla +SPECIFICATION MCSpecMultiNode +HistoryLimit = 7 +ViewLimit = 3 ``` -**Legend:** Solid blue is the selected single-node subset. Dashed orange is -available under `MCSpecMultiNode` but unused by this witness. +At these bounds `MCMultiNode.tla` produces the exact same linear history, +values, and action order as the single-node run. Although `ViewLimit = 3` is +configured, no view change, truncation, or invalidation occurs because the +shortest witness stays entirely in the embedded `MCNextSingleNodeAction` +subset. The multi-node-only alternatives are enabled but selected zero times. This is an important containment result rather than a weakness in the multi-node check. `MCMultiNode.tla` defines: From c0330a2dfb8c88647449a1664dfd9390233216e3 Mon Sep 17 00:00:00 2001 From: achamayou Date: Mon, 10 Aug 2026 18:46:26 +0100 Subject: [PATCH 6/7] Repair ordered serialisability invariant Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> --- .github/workflows/ci-verification.yml | 6 - ...ttedRwOrderedSerializableCounterexample.md | 322 +++++------------- tla/consistency/ExternalHistoryInvars.tla | 14 +- tla/consistency/MCMultiNode.cfg | 1 + ...cfg => MCMultiNodeOrderedSerializable.cfg} | 0 tla/consistency/MCMultiNodeReads.cfg | 1 + ...fg => MCSingleNodeOrderedSerializable.cfg} | 0 7 files changed, 98 insertions(+), 246 deletions(-) rename tla/consistency/{MCMultiNodeOrderedSerializableCounterexample.cfg => MCMultiNodeOrderedSerializable.cfg} (100%) rename tla/consistency/{MCSingleNodeOrderedSerializableCounterexample.cfg => MCSingleNodeOrderedSerializable.cfg} (100%) diff --git a/.github/workflows/ci-verification.yml b/.github/workflows/ci-verification.yml index efa04156deac..b86ec613e629 100644 --- a/.github/workflows/ci-verification.yml +++ b/.github/workflows/ci-verification.yml @@ -78,12 +78,6 @@ jobs: - run: ./tlc_debug.sh --config consistency/MCMultiNodeCommitReachability.cfg mc consistency/MCMultiNodeReads.tla - run: ./tlc_debug.sh --config consistency/MCMultiNodeInvalidReachability.cfg mc consistency/MCMultiNodeReads.tla - run: ./tlc_debug.sh --config consistency/MCMultiNodeReadsNotLinearizable.cfg mc consistency/MCMultiNodeReads.tla - # tlc_debug.sh converts this exact TLC failure into success: - # Error: Invariant CommittedRwOrderedSerializableInv is violated. - - run: ./tlc_debug.sh --config consistency/MCSingleNodeOrderedSerializableCounterexample.cfg mc consistency/MCSingleNode.tla - # tlc_debug.sh converts this exact TLC failure into success: - # Error: Invariant CommittedRwOrderedSerializableInv is violated. - - run: ./tlc_debug.sh --config consistency/MCMultiNodeOrderedSerializableCounterexample.cfg mc consistency/MCMultiNode.tla simulation-consistency: name: Simulation - Consistency diff --git a/tla/consistency/CommittedRwOrderedSerializableCounterexample.md b/tla/consistency/CommittedRwOrderedSerializableCounterexample.md index 3141bc2b108e..4ec441487c71 100644 --- a/tla/consistency/CommittedRwOrderedSerializableCounterexample.md +++ b/tla/consistency/CommittedRwOrderedSerializableCounterexample.md @@ -1,34 +1,54 @@ -# `CommittedRwOrderedSerializableInv` counterexample +# Counterexample to the previous ordered serialisability equality ## Result -`CommittedRwOrderedSerializableInv` is not an invariant of either bounded -consistency transition system. With `HistoryLimit = 7`, TLC reports the same -shortest counterexample from both the single-node model and the multi-node -model with its normal `ViewLimit = 3`. +The previous definition of `CommittedRwOrderedSerializableInv` required +adjacent entries in `CommittedRwResponses` to differ by exactly the later +transaction's write. That equality was too strong because +`CommittedRwResponses` is filtered to responses whose clients explicitly +received committed status. A committed ledger write without a response or +status in `history` can therefore appear between two entries which are +adjacent only after filtering. -The trace has exactly seven external history events, ten transitions, and -eleven states when the initial state is included. Seven is the event count, -not the transition count. The trace requires no view change, read-only -transaction, invalid status, or non-client ledger entry, so it occurs in the -single-node action subset of the multi-node model. +The invariant now requires the earlier observation to be a proper prefix of +the later observation and the later observation to end with its own write: -This is a specification-property failure, not a CCF consistency failure. The -property assumes that responses which are adjacent after filtering for -explicitly reported committed transaction IDs are also adjacent ledger -entries. The transition system does not make that assumption, and CCF does not -require it for serialisability. +```tla +CommittedRwOrderedSerializableInv == + \A i \in 1..Len(CommittedRwResponses)-1: + 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 +``` + +This retains the intended transaction-ID ordering guarantee while allowing +zero or more intervening ledger writes before the later transaction. +`CommittedRwOrderedSpecLinearizableInv` continues to include this invariant +and remains enabled in the normal multi-node configurations. + +## Why this replacement is narrow + +`CommittedRwSerializableInv` allows either observation to be a prefix of the +other. The repaired ordered invariant is deliberately stronger: -The property remains defined in `ExternalHistoryInvars.tla` as the target of -the two dedicated expected-counterexample configurations. It is not checked -by the normal multi-node configurations. +1. `IsPrefix(Earlier.observed, Later.observed)` fixes the prefix direction + according to transaction-ID order. +2. `Len(Earlier.observed) < Len(Later.observed)` requires strict progress, so + equal observations do not satisfy the property. +3. `Last(Later.observed) = Later.tx` preserves the requirement that the later + transaction observes its own write last. -## The property +The replacement is not set inclusion or a subsequence check. Both would allow +observations to be reordered and would lose the ledger-prefix guarantee. + +## The old equality `CommittedRwResponses` contains read-write responses whose transaction IDs have an explicit committed-status event in `history`, sorted by transaction -ID. The property requires each adjacent pair in that filtered sequence to -differ by exactly the later transaction: +ID. The previous property required each adjacent pair in that filtered +sequence to differ by exactly the later transaction: ```tla CommittedRwOrderedSerializableInv == @@ -39,65 +59,16 @@ CommittedRwOrderedSerializableInv == CommittedRwResponses[i+1].tx) ``` -The equality is too strong. An intervening client write can be present in the -ledger and in the later response's observations without having its own -response or committed-status event in the external history. - -## Shared deterministic trace - -With one worker, both the single-node configuration and the `MCMultiNode.tla` -configuration produce this exact deterministic breadth-first history. The -diagram is the complete transition order, not a projection: its single path -contains all ten transitions and ends at the state 11 violation. Transaction -IDs are `<>`. - -```mermaid -%%{init: {"theme":"base","themeVariables":{"fontFamily":"Arial, sans-serif","lineColor":"#333333","primaryTextColor":"#111111"}}}%% -flowchart TB - t1["1. HISTORY 1 - REQUEST tx0
MCRwTxRequestAction; history length 1"] - t2["2. HISTORY 2 - REQUEST tx1
MCRwTxRequestAction; history length 2"] - t3["3. HISTORY 3 - REQUEST tx2
MCRwTxRequestAction; history length 3"] - t4(["4. INTERNAL - EXECUTE tx0
view 1, slot 1; history remains 3"]) - t5(["5. INTERNAL - EXECUTE tx1
view 1, slot 2; history remains 3
Present in ledger; no later response or status"]) - t6(["6. INTERNAL - EXECUTE tx2
view 1, slot 3; history remains 3"]) - t7{{"7. HISTORY 4 - RESPONSE tx0
ID <<1, 1>>; observed <<0>>
Retained once committed at transition 9"}} - t8{{"8. HISTORY 5 - RESPONSE tx2
ID <<1, 3>>; observed <<0, 1 UNEXPECTED, 2>>
Retained once committed at transition 10; unexpected tx1 contribution"}} - t9{{"9. HISTORY 6 - COMMITTED STATUS <<1, 1>>
MCStatusCommittedResponseAction; retains response tx0"}} - t10{{"10. HISTORY 7 - COMMITTED STATUS <<1, 3>>
MCStatusCommittedResponseAction; retains response tx2"}} - failure[["ANALYSIS - INVARIANT VIOLATION
Filtering produces responses tx0 and tx2; tx1 has no response/status.
expected Append(<<0>>, 2) = <<0, 2>>
actual = <<0, 1 UNEXPECTED, 2>>
CommittedRwOrderedSerializableInv is false."]] - - t1 --> t2 - t2 --> t3 - t3 --> t4 - t4 --> t5 - t5 --> t6 - t6 --> t7 - t7 --> t8 - t8 --> t9 - t9 --> t10 - t10 --> failure - - classDef external fill:#D9EAF7,stroke:#0072B2,stroke-width:3px,color:#111111 - classDef internal fill:#E5E7EB,stroke:#4B5563,stroke-width:3px,color:#111111 - classDef intervening fill:#FDE7B0,stroke:#A85D00,stroke-width:4px,color:#111111 - classDef retained fill:#DFF2E1,stroke:#007A3D,stroke-width:3px,color:#111111 - classDef unexpected fill:#DFF2E1,stroke:#B00020,stroke-width:5px,color:#111111 - classDef violation fill:#FFD6D6,stroke:#B00020,stroke-width:6px,color:#660000 - class t1,t2,t3 external - class t4,t6 internal - class t5 intervening - class t7,t9,t10 retained - class t8 unexpected - class failure violation - linkStyle default stroke:#333333,stroke-width:3px -``` +That equality treated adjacency after response filtering as adjacency in the +ledger. The consistency transition system does not equate those notions. + +## Counterexample to the old equality -**Legend:** Blue rectangles are ordinary external history events. Gray rounded -nodes are internal execute actions and do not change `history`. The amber -rounded node marks transaction `1`, which is present in the ledger but absent -from response/status filtering. Green hexagons are response/status events -retained by that filtering. Red text and heavy red borders mark the unexpected -transaction `1` contribution and the final invariant violation. +With `HistoryLimit = 7`, both the single-node model and the multi-node model +with `ViewLimit = 3` reach the same shortest witness. It has seven external +history events, ten transitions, and eleven states including the initial +state. It requires no view change, read-only transaction, invalid status, or +non-client ledger entry. | Transition | State reached | TLC action | Relevant result | History length | | ---------: | ------------: | --------------------------------- | ------------------------------------- | -------------: | @@ -112,8 +83,6 @@ transaction `1` contribution and the final invariant violation. | 9 | 10 | `MCStatusCommittedResponseAction` | `<<1, 1>>` enters `CommittedTxIDs` | 6 | | 10 | 11 | `MCStatusCommittedResponseAction` | `<<1, 3>>` enters `CommittedTxIDs` | 7 | -State 1 is the initial state. Ten transitions therefore reach state 11. - There is deliberately no response or status event for transaction `1`. In the final state: @@ -127,182 +96,65 @@ CommittedRwResponses = >> ``` -The property checks the only adjacent pair and compares: +The old equality compared: ```text actual = <<0, 1, 2>> expected = Append(<<0>>, 2) = <<0, 2>> ``` -The intervening `1` makes the equality false. The weaker -`CommittedRwSerializableInv` still holds because `<<0>>` is a prefix of -`<<0, 1, 2>>`. - +The intervening write `1` made that equality false. This is a +specification-property counterexample, not a CCF consistency counterexample. In a real ledger, committing sequence number 3 commits the preceding ledger -prefix as well. The abstraction's `CommittedTxIDs`, however, represents -committed statuses explicitly observed by clients, not every transaction -implicitly covered by the commit watermark. Filtering responses with that set -can therefore hide transaction `1` even though later execution observes it. - -The trace is minimal for this construction: +prefix as well. The abstraction's `CommittedTxIDs` represents committed +statuses explicitly observed by clients, not every transaction covered by +the commit watermark. -1. Three requests and three executions place an intervening write between the - two compared ledger entries. -2. Two responses expose the observations being compared. -3. Two committed-status events include both outer responses in - `CommittedRwResponses`. +## Why the witness satisfies the repaired invariant -These are ten transitions. The execution actions do not append to `history`, -so the three requests, two responses, and two statuses produce seven history -events. - -## Configuration-specific reproduction - -### Single-node configuration - -The dedicated single-node configuration uses: - -```tla -SPECIFICATION MCSpecSingleNode -HistoryLimit = 7 -``` - -It produces the shared ten-transition, eleven-state trace above. - -### Multi-node configuration - -The dedicated `MCMultiNode.tla` configuration uses: +For the same filtered pair, the repaired property evaluates as follows: ```tla -SPECIFICATION MCSpecMultiNode -HistoryLimit = 7 -ViewLimit = 3 +IsPrefix(<<0>>, <<0, 1, 2>>) = TRUE +Len(<<0>>) < Len(<<0, 1, 2>>) = TRUE +Last(<<0, 1, 2>>) = 2 ``` -At these bounds `MCMultiNode.tla` produces the exact same linear history, -values, and action order as the single-node run. Although `ViewLimit = 3` is -configured, no view change, truncation, or invalidation occurs because the -shortest witness stays entirely in the embedded `MCNextSingleNodeAction` -subset. The multi-node-only alternatives are enabled but selected zero times. +The witness therefore passes for the intended reason: transaction `1` may +intervene, but the observation remains an ordered extension and transaction +`2` remains last. -This is an important containment result rather than a weakness in the -multi-node check. `MCMultiNode.tla` defines: - -```tla -MCNextMultiNodeAction == - \/ MCNextSingleNodeAction - \/ MCTruncateLedgerAction - \/ MCStatusInvalidResponseAction -``` +## Model-checking bounds -Consequently every single-node behavior is also an allowed multi-node -behavior. A property claimed for all multi-node behaviors must hold for the -embedded subset even when the additional view-change actions are unused. +The normal `MCMultiNode.cfg` and `MCMultiNodeReads.cfg` configurations use +`HistoryLimit = 6`. Seven external events are needed to expose the old +equality's mistake: three requests create the ledger entries, two responses +provide the compared pair, and two committed-status events retain that pair +in `CommittedRwResponses`. -## Reproduce with TLC +The bound predates the ordered property. It was established with the original +consistency specification in commit +[`724c827247`](https://github.com/microsoft/CCF/commit/724c827247) +([PR #5699](https://github.com/microsoft/CCF/pull/5699)). Commit +[`bf4fcff670`](https://github.com/microsoft/CCF/commit/bf4fcff670) +([PR #6185](https://github.com/microsoft/CCF/pull/6185)) later introduced +`CommittedRwOrderedSpecLinearizableInv` without changing the bound. -On Ubuntu, install Java, `wget`, and the repository's TLC dependencies: +The dedicated positive-check configurations raise `HistoryLimit` to 7: ```bash -sudo apt update -sudo apt install -y default-jre wget cd tla -python3 install_deps.py -``` - -From the `tla` directory, run both expected-counterexample checks: - -```bash -./tlc_debug.sh --workers 1 --difftrace \ - --trace-name single-node-ordered-serializable \ - --config consistency/MCSingleNodeOrderedSerializableCounterexample.cfg \ +./tlc.py --workers 1 \ + --config consistency/MCSingleNodeOrderedSerializable.cfg \ mc consistency/MCSingleNode.tla -./tlc_debug.sh --workers 1 --difftrace \ - --trace-name multi-node-ordered-serializable \ - --config consistency/MCMultiNodeOrderedSerializableCounterexample.cfg \ +./tlc.py --workers 1 \ + --config consistency/MCMultiNodeOrderedSerializable.cfg \ mc consistency/MCMultiNode.tla ``` -Each dedicated configuration checks only -`CommittedRwOrderedSerializableInv`, as required by `tlc_debug.sh`. TLC -reports: - -```text -Error: Invariant CommittedRwOrderedSerializableInv is violated. -... -Counterexample found as expected. -``` - -The single-node command generates 12,390 states and 8,846 distinct states. -The multi-node command at `ViewLimit = 3` generates 134,561 states and 63,978 -distinct states. Both stop at the same state 11 violation. Counts are from -deterministic one-worker runs with the repository-installed TLC dependencies. - -## Why existing model checking missed it - -The normal `MCMultiNode.cfg` and `MCMultiNodeReads.cfg` configurations both -set: - -```tla -HistoryLimit = 6 -``` - -Seven external events are necessary: three requests create the ledger entries, -two responses provide the pair to compare, and two committed-status events -include that pair in the filtered sequence. With `HistoryLimit = 6`, TLC -exhaustively checks the bounded state graph but cannot reach the violating -state. Raising only this bound to 7 exposes the counterexample. - -The bound predates the property. It was established with the original -consistency specification in commit -[`724c827247`](https://github.com/microsoft/CCF/commit/724c827247) -([PR #5699](https://github.com/microsoft/CCF/pull/5699)). Commit -[`bf4fcff670`](https://github.com/microsoft/CCF/commit/bf4fcff670) -([PR #6185](https://github.com/microsoft/CCF/pull/6185)) later introduced -`CommittedRwOrderedSpecLinearizableInv` as a multi-node ordered speculative -linearizability check. That change wired the composite invariant only into -`MCMultiNode.cfg` and `MCMultiNodeReads.cfg`; it did not add it to the -single-node configuration or change `HistoryLimit`. - -The configuration placement does not limit the property's domain. The -multi-node model extends the single-node model, and -`MCNextMultiNodeAction` explicitly contains `MCNextSingleNodeAction`. -`MCSingleNodeOrderedSerializableCounterexample.cfg` is therefore a valid -minimal diagnostic witness for a property that was originally enabled only -in multi-node configurations. The dedicated multi-node run independently -confirms that the same witness is present at the original `ViewLimit = 3`. - -The other configurations did not close the gap: - -- The single-node configurations used a history limit of 7 but did not check - the new property. -- `MCMultiNodeReadsAlt.cfg` used a larger history limit but did not check the - new property. -- The configurations which checked the property remained capped at 6. - -This was a scope-boundary blind spot, not a TLC search failure. - -## Why the property fails - -PR #6185 intended to state that committed read-write transactions are -serialisable in transaction-ID order. Its formula selects only responses with -explicitly observed committed statuses, sorts that filtered set, and then -treats adjacent elements as adjacent ledger writes. - -Those notions of adjacency differ: - -- Adjacent in `CommittedRwResponses` means no other response with an explicit - committed-status event is between the pair. -- Adjacent in the ledger means no client write is between their sequence - numbers. - -The transition system permits a write to execute without a response or status -event. Such a write is absent from `CommittedRwResponses` but remains present -in every later observation of that ledger prefix. The `Append` equality -therefore cannot hold in general. - -A replacement property requires a separate design decision. For example, it -could allow an observed suffix between the compared writes, or the abstraction -could distinguish actual ledger commitment from client receipt of a committed -status. This counterexample does not assert a replacement guarantee. +An exhaustive one-worker run checks 63,449 distinct single-node states and +21,586,197 distinct multi-node states without an invariant violation. The +multi-node check retains the normal `ViewLimit = 3`. It is intentionally not +added as a permanent CI job because this higher-bound exhaustive check is +substantially more expensive than the normal model-checking configurations. diff --git a/tla/consistency/ExternalHistoryInvars.tla b/tla/consistency/ExternalHistoryInvars.tla index abca570e9f7e..c598ecab829f 100644 --- a/tla/consistency/ExternalHistoryInvars.tla +++ b/tla/consistency/ExternalHistoryInvars.tla @@ -235,13 +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. -\* This property is false when the committed-response filter hides an -\* intervening ledger write. See CommittedRwOrderedSerializableCounterexample.md. +\* 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. diff --git a/tla/consistency/MCMultiNode.cfg b/tla/consistency/MCMultiNode.cfg index 5af3c3f99baa..21f13795e590 100644 --- a/tla/consistency/MCMultiNode.cfg +++ b/tla/consistency/MCMultiNode.cfg @@ -27,6 +27,7 @@ INVARIANTS CommittedRwSerializableInv InvalidNotObservedByCommittedInv AtMostOnceObservedInv + CommittedRwOrderedSpecLinearizableInv CHECK_DEADLOCK FALSE \ No newline at end of file diff --git a/tla/consistency/MCMultiNodeOrderedSerializableCounterexample.cfg b/tla/consistency/MCMultiNodeOrderedSerializable.cfg similarity index 100% rename from tla/consistency/MCMultiNodeOrderedSerializableCounterexample.cfg rename to tla/consistency/MCMultiNodeOrderedSerializable.cfg diff --git a/tla/consistency/MCMultiNodeReads.cfg b/tla/consistency/MCMultiNodeReads.cfg index 1a13c6368f50..7079fead07a1 100644 --- a/tla/consistency/MCMultiNodeReads.cfg +++ b/tla/consistency/MCMultiNodeReads.cfg @@ -27,6 +27,7 @@ INVARIANTS CommittedRwSerializableInv InvalidNotObservedByCommittedInv AtMostOnceObservedInv + CommittedRwOrderedSpecLinearizableInv CHECK_DEADLOCK FALSE \ No newline at end of file diff --git a/tla/consistency/MCSingleNodeOrderedSerializableCounterexample.cfg b/tla/consistency/MCSingleNodeOrderedSerializable.cfg similarity index 100% rename from tla/consistency/MCSingleNodeOrderedSerializableCounterexample.cfg rename to tla/consistency/MCSingleNodeOrderedSerializable.cfg From 5fcdf53406cd2cecdb0ef7b5175fc5014b8cb68c Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Mon, 10 Aug 2026 20:41:30 +0100 Subject: [PATCH 7/7] Add minimal ordered serialisability regression Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> --- .github/workflows/ci-verification.yml | 2 + ...ttedRwOrderedSerializableCounterexample.md | 160 ------------------ .../MCMultiNodeOrderedSerializable.cfg | 21 --- 3 files changed, 2 insertions(+), 181 deletions(-) delete mode 100644 tla/consistency/CommittedRwOrderedSerializableCounterexample.md delete mode 100644 tla/consistency/MCMultiNodeOrderedSerializable.cfg diff --git a/.github/workflows/ci-verification.yml b/.github/workflows/ci-verification.yml index b86ec613e629..cb5b8595776c 100644 --- a/.github/workflows/ci-verification.yml +++ b/.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 diff --git a/tla/consistency/CommittedRwOrderedSerializableCounterexample.md b/tla/consistency/CommittedRwOrderedSerializableCounterexample.md deleted file mode 100644 index 4ec441487c71..000000000000 --- a/tla/consistency/CommittedRwOrderedSerializableCounterexample.md +++ /dev/null @@ -1,160 +0,0 @@ -# Counterexample to the previous ordered serialisability equality - -## Result - -The previous definition of `CommittedRwOrderedSerializableInv` required -adjacent entries in `CommittedRwResponses` to differ by exactly the later -transaction's write. That equality was too strong because -`CommittedRwResponses` is filtered to responses whose clients explicitly -received committed status. A committed ledger write without a response or -status in `history` can therefore appear between two entries which are -adjacent only after filtering. - -The invariant now requires the earlier observation to be a proper prefix of -the later observation and the later observation to end with its own write: - -```tla -CommittedRwOrderedSerializableInv == - \A i \in 1..Len(CommittedRwResponses)-1: - 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 -``` - -This retains the intended transaction-ID ordering guarantee while allowing -zero or more intervening ledger writes before the later transaction. -`CommittedRwOrderedSpecLinearizableInv` continues to include this invariant -and remains enabled in the normal multi-node configurations. - -## Why this replacement is narrow - -`CommittedRwSerializableInv` allows either observation to be a prefix of the -other. The repaired ordered invariant is deliberately stronger: - -1. `IsPrefix(Earlier.observed, Later.observed)` fixes the prefix direction - according to transaction-ID order. -2. `Len(Earlier.observed) < Len(Later.observed)` requires strict progress, so - equal observations do not satisfy the property. -3. `Last(Later.observed) = Later.tx` preserves the requirement that the later - transaction observes its own write last. - -The replacement is not set inclusion or a subsequence check. Both would allow -observations to be reordered and would lose the ledger-prefix guarantee. - -## The old equality - -`CommittedRwResponses` contains read-write responses whose transaction IDs -have an explicit committed-status event in `history`, sorted by transaction -ID. The previous property required each adjacent pair in that filtered -sequence to differ by exactly the later transaction: - -```tla -CommittedRwOrderedSerializableInv == - \A i \in 1..Len(CommittedRwResponses)-1: - CommittedRwResponses[i+1].observed = - Append( - CommittedRwResponses[i].observed, - CommittedRwResponses[i+1].tx) -``` - -That equality treated adjacency after response filtering as adjacency in the -ledger. The consistency transition system does not equate those notions. - -## Counterexample to the old equality - -With `HistoryLimit = 7`, both the single-node model and the multi-node model -with `ViewLimit = 3` reach the same shortest witness. It has seven external -history events, ten transitions, and eleven states including the initial -state. It requires no view change, read-only transaction, invalid status, or -non-client ledger entry. - -| Transition | State reached | TLC action | Relevant result | History length | -| ---------: | ------------: | --------------------------------- | ------------------------------------- | -------------: | -| 1 | 2 | `MCRwTxRequestAction` for `0` | Request `0` is visible | 1 | -| 2 | 3 | `MCRwTxRequestAction` for `1` | Request `1` is visible | 2 | -| 3 | 4 | `MCRwTxRequestAction` for `2` | Request `2` is visible | 3 | -| 4 | 5 | `RwTxExecuteAction` for `0` | Ledger slot 1 is `(view 1, tx 0)` | 3 | -| 5 | 6 | `RwTxExecuteAction` for `1` | Ledger slot 2 is `(view 1, tx 1)` | 3 | -| 6 | 7 | `RwTxExecuteAction` for `2` | Ledger slot 3 is `(view 1, tx 2)` | 3 | -| 7 | 8 | `MCRwTxResponseAction` for `0` | ID `<<1, 1>>`, observes `<<0>>` | 4 | -| 8 | 9 | `MCRwTxResponseAction` for `2` | ID `<<1, 3>>`, observes `<<0, 1, 2>>` | 5 | -| 9 | 10 | `MCStatusCommittedResponseAction` | `<<1, 1>>` enters `CommittedTxIDs` | 6 | -| 10 | 11 | `MCStatusCommittedResponseAction` | `<<1, 3>>` enters `CommittedTxIDs` | 7 | - -There is deliberately no response or status event for transaction `1`. In the -final state: - -```tla -CommittedTxIDs = {<<1, 1>>, <<1, 3>>} - -CommittedRwResponses = - << - [tx |-> 0, tx_id |-> <<1, 1>>, observed |-> <<0>>], - [tx |-> 2, tx_id |-> <<1, 3>>, observed |-> <<0, 1, 2>>] - >> -``` - -The old equality compared: - -```text -actual = <<0, 1, 2>> -expected = Append(<<0>>, 2) = <<0, 2>> -``` - -The intervening write `1` made that equality false. This is a -specification-property counterexample, not a CCF consistency counterexample. -In a real ledger, committing sequence number 3 commits the preceding ledger -prefix as well. The abstraction's `CommittedTxIDs` represents committed -statuses explicitly observed by clients, not every transaction covered by -the commit watermark. - -## Why the witness satisfies the repaired invariant - -For the same filtered pair, the repaired property evaluates as follows: - -```tla -IsPrefix(<<0>>, <<0, 1, 2>>) = TRUE -Len(<<0>>) < Len(<<0, 1, 2>>) = TRUE -Last(<<0, 1, 2>>) = 2 -``` - -The witness therefore passes for the intended reason: transaction `1` may -intervene, but the observation remains an ordered extension and transaction -`2` remains last. - -## Model-checking bounds - -The normal `MCMultiNode.cfg` and `MCMultiNodeReads.cfg` configurations use -`HistoryLimit = 6`. Seven external events are needed to expose the old -equality's mistake: three requests create the ledger entries, two responses -provide the compared pair, and two committed-status events retain that pair -in `CommittedRwResponses`. - -The bound predates the ordered property. It was established with the original -consistency specification in commit -[`724c827247`](https://github.com/microsoft/CCF/commit/724c827247) -([PR #5699](https://github.com/microsoft/CCF/pull/5699)). Commit -[`bf4fcff670`](https://github.com/microsoft/CCF/commit/bf4fcff670) -([PR #6185](https://github.com/microsoft/CCF/pull/6185)) later introduced -`CommittedRwOrderedSpecLinearizableInv` without changing the bound. - -The dedicated positive-check configurations raise `HistoryLimit` to 7: - -```bash -cd tla -./tlc.py --workers 1 \ - --config consistency/MCSingleNodeOrderedSerializable.cfg \ - mc consistency/MCSingleNode.tla - -./tlc.py --workers 1 \ - --config consistency/MCMultiNodeOrderedSerializable.cfg \ - mc consistency/MCMultiNode.tla -``` - -An exhaustive one-worker run checks 63,449 distinct single-node states and -21,586,197 distinct multi-node states without an invariant violation. The -multi-node check retains the normal `ViewLimit = 3`. It is intentionally not -added as a permanent CI job because this higher-bound exhaustive check is -substantially more expensive than the normal model-checking configurations. diff --git a/tla/consistency/MCMultiNodeOrderedSerializable.cfg b/tla/consistency/MCMultiNodeOrderedSerializable.cfg deleted file mode 100644 index 8cb61f02dfa7..000000000000 --- a/tla/consistency/MCMultiNodeOrderedSerializable.cfg +++ /dev/null @@ -1,21 +0,0 @@ -SPECIFICATION MCSpecMultiNode - -CONSTANTS - FirstBranch = 1 - HistoryLimit = 7 - ViewLimit = 3 - - 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