From 17daeb38235d77d7362d1b14068f242afb3fe149 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sat, 22 Aug 2026 07:21:26 -0700 Subject: [PATCH 1/3] Disruptor: name the assumptions of the SPMC and MPMC specs The assumptions were already there, but anonymous, so nothing could refer to one: not a proof, not a comment, and not TLC, which names the failing assumption when it reports that one is false. Three of the four repeat what RingBuffer assumes about Size, Writers and Readers. The repetition is not redundant, because TLC ignores the assumptions of an instantiated module, and RingBuffer is instantiated. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- specifications/Disruptor/Disruptor_MPMC.tla | 8 ++++---- specifications/Disruptor/Disruptor_SPMC.tla | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/specifications/Disruptor/Disruptor_MPMC.tla b/specifications/Disruptor/Disruptor_MPMC.tla index 9237947b..831db91e 100644 --- a/specifications/Disruptor/Disruptor_MPMC.tla +++ b/specifications/Disruptor/Disruptor_MPMC.tla @@ -20,10 +20,10 @@ CONSTANTS Size, (* Ringbuffer size. *) NULL -ASSUME Writers /= {} -ASSUME Readers /= {} -ASSUME Size \in Nat \ {0} -ASSUME MaxPublished \in Nat \ {0} +ASSUME AtLeastOneWriter == Writers /= {} +ASSUME AtLeastOneReader == Readers /= {} +ASSUME SizeIsPositive == Size \in Nat \ {0} +ASSUME MaxPublishedIsPositive == MaxPublished \in Nat \ {0} VARIABLES ringbuffer, diff --git a/specifications/Disruptor/Disruptor_SPMC.tla b/specifications/Disruptor/Disruptor_SPMC.tla index 2ccef673..0953351b 100644 --- a/specifications/Disruptor/Disruptor_SPMC.tla +++ b/specifications/Disruptor/Disruptor_SPMC.tla @@ -22,10 +22,10 @@ CONSTANTS Size, (* Ringbuffer size. *) NULL -ASSUME Writers /= {} -ASSUME Readers /= {} -ASSUME Size \in Nat \ {0} -ASSUME MaxPublished \in Nat \ {0} +ASSUME AtLeastOneWriter == Writers /= {} +ASSUME AtLeastOneReader == Readers /= {} +ASSUME SizeIsPositive == Size \in Nat \ {0} +ASSUME MaxPublishedIsPositive == MaxPublished \in Nat \ {0} VARIABLES ringbuffer, From dfd81f2a6a9e93e3e8a5016892e96e8eddbd0731 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sat, 22 Aug 2026 07:28:09 -0700 Subject: [PATCH 2/3] Disruptor: assume that Writers and Readers are disjoint Both specs require the assumption but neither states it. The variable pc holds one program counter per thread id, so an id in both Writers and Readers shares a single counter between its writer and its reader role. Since pc[t] = "Access" is the sole guard of EndWrite and of EndRead, the Begin action of either role enables the End action of the other. In SPMC, EndWrite after BeginRead advances published past a sequence number that no writer wrote; a consumer then reads the unwritten slot and appends NULL to the consumed history, which violates TypeOk. In MPMC, EndRead after BeginWrite abandons a write in progress and leaves the writer registered in ringbuffer.writers for that slot; a consumer that subsequently enters the slot violates NoDataRaces. Both reports ascribe a defect of the model to the algorithm. Producers and consumers are distinct threads in the Disruptor and every configuration already keeps the two sets disjoint, so the state spaces are unchanged. RingBuffer is not the place for the assumption: TLC ignores the assumptions of an instantiated module, and pc is not declared there. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- specifications/Disruptor/Disruptor_MPMC.tla | 4 ++++ specifications/Disruptor/Disruptor_SPMC.tla | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/specifications/Disruptor/Disruptor_MPMC.tla b/specifications/Disruptor/Disruptor_MPMC.tla index 831db91e..6d174672 100644 --- a/specifications/Disruptor/Disruptor_MPMC.tla +++ b/specifications/Disruptor/Disruptor_MPMC.tla @@ -25,6 +25,10 @@ ASSUME AtLeastOneReader == Readers /= {} ASSUME SizeIsPositive == Size \in Nat \ {0} ASSUME MaxPublishedIsPositive == MaxPublished \in Nat \ {0} +(* A thread id in both sets would share one pc between its writer and its *) +(* reader role, so BeginRead would enable EndWrite and vice versa. *) +ASSUME WritersReadersDisjoint == Writers \cap Readers = {} + VARIABLES ringbuffer, next_sequence, (* Shared counter for claiming a sequence for a Writer. *) diff --git a/specifications/Disruptor/Disruptor_SPMC.tla b/specifications/Disruptor/Disruptor_SPMC.tla index 0953351b..13f83fb9 100644 --- a/specifications/Disruptor/Disruptor_SPMC.tla +++ b/specifications/Disruptor/Disruptor_SPMC.tla @@ -27,6 +27,10 @@ ASSUME AtLeastOneReader == Readers /= {} ASSUME SizeIsPositive == Size \in Nat \ {0} ASSUME MaxPublishedIsPositive == MaxPublished \in Nat \ {0} +(* A thread id in both sets would share one pc between its writer and its *) +(* reader role, so BeginRead would enable EndWrite and vice versa. *) +ASSUME WritersReadersDisjoint == Writers \cap Readers = {} + VARIABLES ringbuffer, published, (* Write cursor. One for the producer. *) From 2c8807d18da122d5980e4c564bd9d444b6d8e13f Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sat, 22 Aug 2026 07:28:31 -0700 Subject: [PATCH 3/3] Factor the TLC concerns out of the Disruptor specs into MCDisruptor MaxPublished bounds the model rather than the Disruptor. The producers publish without end, and the constant exists solely to keep the sequence numbers and the consumed history finite. StateConstraint and Liveliness are both expressed in terms of it, the latter by quantifying i over a range that ends at MaxPublished, so the constant, its assumption MaxPublishedIsPositive, the constraint and the property move together. Disruptor_SPMC and Disruptor_MPMC now hold the algorithms alone, MCDisruptor_SPMC and MCDisruptor_MPMC the models. The state spaces are unchanged. Liveliness moves verbatim. A comment at its new location records that TLC checks it on the state graph pruned by StateConstraint, in which a behavior may terminate in a state whose successors were all pruned; a positive result is therefore weaker than it appears. The Apalache wrappers declared MaxPublished and their configurations assigned it, although both check NoDataRaces alone, under neither the state constraint nor the property. The declarations and the assignments are removed. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- specifications/Disruptor/APDisruptor_MPMC.cfg | 1 - specifications/Disruptor/APDisruptor_MPMC.tla | 2 - specifications/Disruptor/APDisruptor_SPMC.cfg | 1 - specifications/Disruptor/APDisruptor_SPMC.tla | 2 - specifications/Disruptor/Disruptor_MPMC.tla | 17 -------- specifications/Disruptor/Disruptor_SPMC.tla | 17 -------- ...isruptor_MPMC.cfg => MCDisruptor_MPMC.cfg} | 0 specifications/Disruptor/MCDisruptor_MPMC.tla | 41 +++++++++++++++++++ ...ss.cfg => MCDisruptor_MPMC_liveliness.cfg} | 0 ...isruptor_SPMC.cfg => MCDisruptor_SPMC.cfg} | 0 specifications/Disruptor/MCDisruptor_SPMC.tla | 40 ++++++++++++++++++ specifications/Disruptor/manifest.json | 16 ++++++-- 12 files changed, 94 insertions(+), 43 deletions(-) rename specifications/Disruptor/{Disruptor_MPMC.cfg => MCDisruptor_MPMC.cfg} (100%) create mode 100644 specifications/Disruptor/MCDisruptor_MPMC.tla rename specifications/Disruptor/{Disruptor_MPMC_liveliness.cfg => MCDisruptor_MPMC_liveliness.cfg} (100%) rename specifications/Disruptor/{Disruptor_SPMC.cfg => MCDisruptor_SPMC.cfg} (100%) create mode 100644 specifications/Disruptor/MCDisruptor_SPMC.tla diff --git a/specifications/Disruptor/APDisruptor_MPMC.cfg b/specifications/Disruptor/APDisruptor_MPMC.cfg index db97c263..8ab90bf4 100644 --- a/specifications/Disruptor/APDisruptor_MPMC.cfg +++ b/specifications/Disruptor/APDisruptor_MPMC.cfg @@ -4,7 +4,6 @@ \* enumerate, so we only check `NoDataRaces` here. CONSTANTS - MaxPublished = 4 Writers <- WritersVal Readers <- ReadersVal Size = 4 diff --git a/specifications/Disruptor/APDisruptor_MPMC.tla b/specifications/Disruptor/APDisruptor_MPMC.tla index 6f527a9f..69258806 100644 --- a/specifications/Disruptor/APDisruptor_MPMC.tla +++ b/specifications/Disruptor/APDisruptor_MPMC.tla @@ -5,8 +5,6 @@ EXTENDS Integers, FiniteSets, Sequences CONSTANTS - \* @type: Int; - MaxPublished, \* @type: Set(THREAD); Writers, \* @type: Set(THREAD); diff --git a/specifications/Disruptor/APDisruptor_SPMC.cfg b/specifications/Disruptor/APDisruptor_SPMC.cfg index db97c263..8ab90bf4 100644 --- a/specifications/Disruptor/APDisruptor_SPMC.cfg +++ b/specifications/Disruptor/APDisruptor_SPMC.cfg @@ -4,7 +4,6 @@ \* enumerate, so we only check `NoDataRaces` here. CONSTANTS - MaxPublished = 4 Writers <- WritersVal Readers <- ReadersVal Size = 4 diff --git a/specifications/Disruptor/APDisruptor_SPMC.tla b/specifications/Disruptor/APDisruptor_SPMC.tla index d2a2b6ec..57fc1e54 100644 --- a/specifications/Disruptor/APDisruptor_SPMC.tla +++ b/specifications/Disruptor/APDisruptor_SPMC.tla @@ -5,8 +5,6 @@ EXTENDS Integers, FiniteSets, Sequences CONSTANTS - \* @type: Int; - MaxPublished, \* @type: Set(THREAD); Writers, \* @type: Set(THREAD); diff --git a/specifications/Disruptor/Disruptor_MPMC.tla b/specifications/Disruptor/Disruptor_MPMC.tla index 6d174672..94ac26c1 100644 --- a/specifications/Disruptor/Disruptor_MPMC.tla +++ b/specifications/Disruptor/Disruptor_MPMC.tla @@ -14,7 +14,6 @@ EXTENDS Integers, FiniteSets, Sequences CONSTANTS - MaxPublished, (* Max number of published events. Bounds the model. *) Writers, (* Writer/producer thread ids. *) Readers, (* Reader/consumer thread ids. *) Size, (* Ringbuffer size. *) @@ -23,7 +22,6 @@ CONSTANTS ASSUME AtLeastOneWriter == Writers /= {} ASSUME AtLeastOneReader == Readers /= {} ASSUME SizeIsPositive == Size \in Nat \ {0} -ASSUME MaxPublishedIsPositive == MaxPublished \in Nat \ {0} (* A thread id in both sets would share one pc between its writer and its *) (* reader role, so BeginRead would enable EndWrite and vice versa. *) @@ -192,12 +190,6 @@ Fairness == Spec == Init /\ [][Next]_vars /\ Fairness -(***************************************************************************) -(* State constraint - bounds model: *) -(***************************************************************************) - -StateConstraint == next_sequence <= MaxPublished - (***************************************************************************) (* Invariants: *) (***************************************************************************) @@ -213,13 +205,4 @@ TypeOk == /\ consumed \in [ Readers -> Seq(Nat) ] /\ pc \in [ Writers \union Readers -> { Access, Advance } ] -(***************************************************************************) -(* Properties: *) -(***************************************************************************) - -(* Eventually always, consumers must have read all published values. *) -Liveliness == - \A r \in Readers : \A i \in 0..(MaxPublished - 1) : - <>[](i \in 0..AvailablePublishedSequence => Len(consumed[r]) >= i + 1 /\ consumed[r][i + 1] = i) - ============================================================================= diff --git a/specifications/Disruptor/Disruptor_SPMC.tla b/specifications/Disruptor/Disruptor_SPMC.tla index 13f83fb9..7cc4255a 100644 --- a/specifications/Disruptor/Disruptor_SPMC.tla +++ b/specifications/Disruptor/Disruptor_SPMC.tla @@ -16,7 +16,6 @@ EXTENDS Integers, FiniteSets, Sequences CONSTANTS - MaxPublished, (* Max number of published events. Bounds the model. *) Writers, (* Writer/producer thread ids. *) Readers, (* Reader/consumer thread ids. *) Size, (* Ringbuffer size. *) @@ -25,7 +24,6 @@ CONSTANTS ASSUME AtLeastOneWriter == Writers /= {} ASSUME AtLeastOneReader == Readers /= {} ASSUME SizeIsPositive == Size \in Nat \ {0} -ASSUME MaxPublishedIsPositive == MaxPublished \in Nat \ {0} (* A thread id in both sets would share one pc between its writer and its *) (* reader role, so BeginRead would enable EndWrite and vice versa. *) @@ -144,12 +142,6 @@ Fairness == Spec == Init /\ [][Next]_vars /\ Fairness -(***************************************************************************) -(* State constraint - bounds model: *) -(***************************************************************************) - -StateConstraint == published < MaxPublished - (***************************************************************************) (* Invariants: *) (***************************************************************************) @@ -163,13 +155,4 @@ TypeOk == NoDataRaces == Buffer!NoDataRaces -(***************************************************************************) -(* Properties: *) -(***************************************************************************) - -(* Eventually always, consumers must have read all published values. *) -Liveliness == - \A r \in Readers : \A i \in 0 .. (MaxPublished - 1) : - <>[](i \in 0 .. published => Len(consumed[r]) >= i + 1 /\ consumed[r][i + 1] = i) - ============================================================================= \ No newline at end of file diff --git a/specifications/Disruptor/Disruptor_MPMC.cfg b/specifications/Disruptor/MCDisruptor_MPMC.cfg similarity index 100% rename from specifications/Disruptor/Disruptor_MPMC.cfg rename to specifications/Disruptor/MCDisruptor_MPMC.cfg diff --git a/specifications/Disruptor/MCDisruptor_MPMC.tla b/specifications/Disruptor/MCDisruptor_MPMC.tla new file mode 100644 index 00000000..f3e5b927 --- /dev/null +++ b/specifications/Disruptor/MCDisruptor_MPMC.tla @@ -0,0 +1,41 @@ +-------------------------- MODULE MCDisruptor_MPMC -------------------------- +(***************************************************************************) +(* Bounds Disruptor_MPMC for TLC. *) +(* *) +(* The producers in Disruptor_MPMC publish forever, so the claimed *) +(* sequence numbers - and with them the history variable `consumed' - *) +(* grow without bound. MaxPublished caps how many sequence numbers are *) +(* claimed, which both makes the state space finite and makes *) +(* Disruptor_MPMC!Liveliness checkable by turning its quantification over *) +(* Nat into a finite conjunction. *) +(***************************************************************************) + +EXTENDS Disruptor_MPMC + +CONSTANT + MaxPublished (* Max number of published events. Bounds the model. *) + +ASSUME MaxPublishedIsPositive == MaxPublished \in Nat \ {0} + +(***************************************************************************) +(* State constraint - bounds the model: *) +(***************************************************************************) + +StateConstraint == next_sequence <= MaxPublished + +(***************************************************************************) +(* Properties: *) +(***************************************************************************) + +(* Eventually always, consumers must have read all published values. *) +(* *) +(* This lives here rather than in Disruptor_MPMC because the range of i is *) +(* a model bound. Note that TLC checks it on the state graph pruned by *) +(* StateConstraint, where a behavior may end in a state whose successors *) +(* were all pruned; a liveness result under a state constraint is thus *) +(* weaker than it appears. *) +Liveliness == + \A r \in Readers : \A i \in 0..(MaxPublished - 1) : + <>[](i \in 0..AvailablePublishedSequence => Len(consumed[r]) >= i + 1 /\ consumed[r][i + 1] = i) + +============================================================================= diff --git a/specifications/Disruptor/Disruptor_MPMC_liveliness.cfg b/specifications/Disruptor/MCDisruptor_MPMC_liveliness.cfg similarity index 100% rename from specifications/Disruptor/Disruptor_MPMC_liveliness.cfg rename to specifications/Disruptor/MCDisruptor_MPMC_liveliness.cfg diff --git a/specifications/Disruptor/Disruptor_SPMC.cfg b/specifications/Disruptor/MCDisruptor_SPMC.cfg similarity index 100% rename from specifications/Disruptor/Disruptor_SPMC.cfg rename to specifications/Disruptor/MCDisruptor_SPMC.cfg diff --git a/specifications/Disruptor/MCDisruptor_SPMC.tla b/specifications/Disruptor/MCDisruptor_SPMC.tla new file mode 100644 index 00000000..06843a80 --- /dev/null +++ b/specifications/Disruptor/MCDisruptor_SPMC.tla @@ -0,0 +1,40 @@ +-------------------------- MODULE MCDisruptor_SPMC -------------------------- +(***************************************************************************) +(* Bounds Disruptor_SPMC for TLC. *) +(* *) +(* The producer in Disruptor_SPMC publishes forever, so its sequence *) +(* numbers - and with them the history variable `consumed' - grow without *) +(* bound. MaxPublished caps how far the producer gets, which both makes *) +(* the state space finite and makes Disruptor_SPMC!Liveliness checkable *) +(* by turning its quantification over Nat into a finite conjunction. *) +(***************************************************************************) + +EXTENDS Disruptor_SPMC + +CONSTANT + MaxPublished (* Max number of published events. Bounds the model. *) + +ASSUME MaxPublishedIsPositive == MaxPublished \in Nat \ {0} + +(***************************************************************************) +(* State constraint - bounds the model: *) +(***************************************************************************) + +StateConstraint == published < MaxPublished + +(***************************************************************************) +(* Properties: *) +(***************************************************************************) + +(* Eventually always, consumers must have read all published values. *) +(* *) +(* This lives here rather than in Disruptor_SPMC because the range of i is *) +(* a model bound. Note that TLC checks it on the state graph pruned by *) +(* StateConstraint, where a behavior may end in a state whose successors *) +(* were all pruned; a liveness result under a state constraint is thus *) +(* weaker than it appears. *) +Liveliness == + \A r \in Readers : \A i \in 0 .. (MaxPublished - 1) : + <>[](i \in 0 .. published => Len(consumed[r]) >= i + 1 /\ consumed[r][i + 1] = i) + +============================================================================= diff --git a/specifications/Disruptor/manifest.json b/specifications/Disruptor/manifest.json index f8432347..0ef19190 100644 --- a/specifications/Disruptor/manifest.json +++ b/specifications/Disruptor/manifest.json @@ -39,9 +39,14 @@ { "path": "specifications/Disruptor/Disruptor_MPMC.tla", "features": [], + "models": [] + }, + { + "path": "specifications/Disruptor/MCDisruptor_MPMC.tla", + "features": [], "models": [ { - "path": "specifications/Disruptor/Disruptor_MPMC.cfg", + "path": "specifications/Disruptor/MCDisruptor_MPMC.cfg", "runtime": "00:00:10", "mode": "exhaustive search", "result": "success", @@ -50,7 +55,7 @@ "stateDepth": 81 }, { - "path": "specifications/Disruptor/Disruptor_MPMC_liveliness.cfg", + "path": "specifications/Disruptor/MCDisruptor_MPMC_liveliness.cfg", "runtime": "00:00:10", "mode": "exhaustive search", "result": "success", @@ -63,9 +68,14 @@ { "path": "specifications/Disruptor/Disruptor_SPMC.tla", "features": [], + "models": [] + }, + { + "path": "specifications/Disruptor/MCDisruptor_SPMC.tla", + "features": [], "models": [ { - "path": "specifications/Disruptor/Disruptor_SPMC.cfg", + "path": "specifications/Disruptor/MCDisruptor_SPMC.cfg", "runtime": "00:00:10", "mode": "exhaustive search", "result": "success",