Skip to content

State the assumptions and split the models into MCDisruptor #232

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lemmy wants to merge 3 commits into
base: master
Choose a base branch
from
Open

State the assumptions and split the models into MCDisruptor #232

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
17daeb3
Disruptor: name the assumptions of the SPMC and MPMC specs
lemmy Aug 22, 2026
dfd81f2
Disruptor: assume that Writers and Readers are disjoint
lemmy Aug 22, 2026
2c8807d
Factor the TLC concerns out of the Disruptor specs into MCDisruptor
lemmy Aug 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion specifications/Disruptor/APDisruptor_MPMC.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@
\* enumerate, so we only check `NoDataRaces` here.

CONSTANTS
MaxPublished = 4
Writers <- WritersVal
Readers <- ReadersVal
Size = 4
Expand Down
2 changes: 0 additions & 2 deletions specifications/Disruptor/APDisruptor_MPMC.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,6 @@
EXTENDS Integers, FiniteSets, Sequences

CONSTANTS
\* @type: Int;
MaxPublished,
\* @type: Set(THREAD);
Writers,
\* @type: Set(THREAD);
Expand Down
1 change: 0 additions & 1 deletion specifications/Disruptor/APDisruptor_SPMC.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@
\* enumerate, so we only check `NoDataRaces` here.

CONSTANTS
MaxPublished = 4
Writers <- WritersVal
Readers <- ReadersVal
Size = 4
Expand Down
2 changes: 0 additions & 2 deletions specifications/Disruptor/APDisruptor_SPMC.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,6 @@
EXTENDS Integers, FiniteSets, Sequences

CONSTANTS
\* @type: Int;
MaxPublished,
\* @type: Set(THREAD);
Writers,
\* @type: Set(THREAD);
Expand Down
27 changes: 7 additions & 20 deletions specifications/Disruptor/Disruptor_MPMC.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -188,12 +190,6 @@ Fairness ==
Spec ==
Init /\ [][Next]_vars /\ Fairness

(***************************************************************************)
(* State constraint - bounds model: *)
(***************************************************************************)

StateConstraint == next_sequence <= MaxPublished

(***************************************************************************)
(* Invariants: *)
(***************************************************************************)
Expand All @@ -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)

=============================================================================
27 changes: 7 additions & 20 deletions specifications/Disruptor/Disruptor_SPMC.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -140,12 +142,6 @@ Fairness ==
Spec ==
Init /\ [][Next]_vars /\ Fairness

(***************************************************************************)
(* State constraint - bounds model: *)
(***************************************************************************)

StateConstraint == published < MaxPublished

(***************************************************************************)
(* Invariants: *)
(***************************************************************************)
Expand All @@ -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)

=============================================================================
0 specifications/Disruptor/Disruptor_MPMC.cfg → ...ifications/Disruptor/MCDisruptor_MPMC.cfg
View file
Open in desktop
File renamed without changes.
41 changes: 41 additions & 0 deletions specifications/Disruptor/MCDisruptor_MPMC.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)

=============================================================================
0 ...s/Disruptor/Disruptor_MPMC_liveliness.cfg → ...Disruptor/MCDisruptor_MPMC_liveliness.cfg
View file
Open in desktop
File renamed without changes.
0 specifications/Disruptor/Disruptor_SPMC.cfg → ...ifications/Disruptor/MCDisruptor_SPMC.cfg
View file
Open in desktop
File renamed without changes.
40 changes: 40 additions & 0 deletions specifications/Disruptor/MCDisruptor_SPMC.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)

=============================================================================
16 changes: 13 additions & 3 deletions specifications/Disruptor/manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand All @@ -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",
Expand All @@ -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",
Expand Down
Loading