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 9237947b..94ac26c1 100644 --- a/specifications/Disruptor/Disruptor_MPMC.tla +++ b/specifications/Disruptor/Disruptor_MPMC.tla @@ -14,16 +14,18 @@ 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. *) 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} + +(* 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, @@ -188,12 +190,6 @@ Fairness == Spec == Init /\ [][Next]_vars /\ Fairness -(***************************************************************************) -(* State constraint - bounds model: *) -(***************************************************************************) - -StateConstraint == next_sequence <= MaxPublished - (***************************************************************************) (* Invariants: *) (***************************************************************************) @@ -209,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 2ccef673..7cc4255a 100644 --- a/specifications/Disruptor/Disruptor_SPMC.tla +++ b/specifications/Disruptor/Disruptor_SPMC.tla @@ -16,16 +16,18 @@ 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. *) 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} + +(* 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, @@ -140,12 +142,6 @@ Fairness == Spec == Init /\ [][Next]_vars /\ Fairness -(***************************************************************************) -(* State constraint - bounds model: *) -(***************************************************************************) - -StateConstraint == published < MaxPublished - (***************************************************************************) (* Invariants: *) (***************************************************************************) @@ -159,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",