Skip to content
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

Jump to bottom

Add small improvements to the Disruptor spec. #151

Merged
merged 4 commits into from
Oct 7, 2024
Merged

Add small improvements to the Disruptor spec. #151

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
f0bf738
Add small improvements to specs.
nicholassm Sep 22, 2024
f8cf49d
Add 'state constraint' to feature list for Disruptor spec.
nicholassm Sep 22, 2024
96e5cb9
Flip 'Advance' and 'Access' state - they were flipped.
nicholassm Sep 24, 2024
7fbcd9b
Add state constraint, improve model.
nicholassm Sep 24, 2024
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
7 changes: 4 additions & 3 deletions manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -494,13 +494,14 @@
"size": "small",
"mode": "exhaustive search",
"features": [
"state constraint",
ahelwer marked this conversation as resolved.
Show resolved Hide resolved
"liveness",
"ignore deadlock"
],
"result": "success",
"distinctStates": 8153,
"totalStates": 26481,
"stateDepth": 81
"distinctStates": 8496,
"totalStates": 28049,
"stateDepth": 82
}
]
},
Expand Down
11 changes: 7 additions & 4 deletions specifications/Disruptor/Disruptor_MPMC.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
(* *)
(* The model also verifies that no data races occur between the producers *)
(* and consumers and that all consumers eventually read all published *)
(* values. *)
(* values (in a Multicast fashion - i.e. all consumers read all events). *)
(***************************************************************************)

EXTENDS Integers, FiniteSets, Sequences
Expand All @@ -22,16 +22,19 @@ CONSTANTS

ASSUME Writers /= {}
ASSUME Readers /= {}
ASSUME Size \in Nat \ {0}
ASSUME Size \in Nat \ {0}
ASSUME MaxPublished \in Nat \ {0}

VARIABLES
ringbuffer,
next_sequence, (* Shared counter for claiming a sequence for a Writer. *)
claimed_sequence, (* Claimed sequence by each Writer. *)
published, (* Encodes whether each slot is published. *)
read, (* Read Cursors. One per Reader. *)
consumed, (* Sequence of all read events by the Readers. *)
pc (* Program Counter for each Writer/Reader. *)
pc, (* Program Counter for each Writer/Reader. *)
consumed (* Sequence of all read events by the Readers. *)
(* This is a history variable used for liveliness *)
(* checking. *)

vars == <<
ringbuffer,
Expand Down
3 changes: 3 additions & 0 deletions specifications/Disruptor/Disruptor_SPMC.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,5 +15,8 @@ INVARIANTS
PROPERTIES
Liveliness

CONSTRAINT
StateConstraint

CHECK_DEADLOCK
FALSE
25 changes: 16 additions & 9 deletions specifications/Disruptor/Disruptor_SPMC.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
(* *)
(* The model also verifies that no data races occur between the producer *)
(* and consumers and that all consumers eventually read all published *)
(* values. *)
(* values (in a Multicast fashion - i.e. all consumers read all events). *)
(* *)
(* To see a data race, try and run the model with two producers. *)
(***************************************************************************)
Expand All @@ -24,14 +24,17 @@ CONSTANTS

ASSUME Writers /= {}
ASSUME Readers /= {}
ASSUME Size \in Nat \ {0}
ASSUME Size \in Nat \ {0}
ASSUME MaxPublished \in Nat \ {0}

VARIABLES
ringbuffer,
published, (* Write cursor. One for the producer. *)
read, (* Read cursors. One per consumer. *)
consumed, (* Sequence of all read events by the Readers. *)
pc (* Program Counter of each Writer/Reader. *)
pc, (* Program Counter of each Writer/Reader. *)
consumed (* Sequence of all read events by the Readers. *)
(* This is a history variable used for liveliness *)
(* checking. *)

vars == <<
ringbuffer,
Expand Down Expand Up @@ -73,7 +76,6 @@ BeginWrite(writer) ==
IN
\* Are we clear of all consumers? (Potentially a full cycle behind).
/\ min_read >= next - Size
/\ next < MaxPublished
/\ Transition(writer, Access, Advance)
/\ Buffer!Write(index, writer, next)
/\ UNCHANGED << consumed, published, read >>
Expand Down Expand Up @@ -132,14 +134,18 @@ Next ==
\/ \E r \in Readers : EndRead(r)

Fairness ==
/\ \A w \in Writers : WF_vars(BeginWrite(w))
/\ \A w \in Writers : WF_vars(EndWrite(w))
nicholassm marked this conversation as resolved.
Show resolved Hide resolved
/\ \A r \in Readers : WF_vars(BeginRead(r))
/\ \A r \in Readers : WF_vars(EndRead(r))

Spec ==
Init /\ [][Next]_vars /\ Fairness

(***************************************************************************)
(* State constraint to bound model: *)
(***************************************************************************)

StateConstraint == published < MaxPublished

(***************************************************************************)
(* Invariants: *)
(***************************************************************************)
Expand All @@ -159,6 +165,7 @@ NoDataRaces == Buffer!NoDataRaces

(* Eventually always, consumers must have read all published values. *)
Liveliness ==
<>[] (\A r \in Readers : consumed[r] = [i \in 1..MaxPublished |-> i - 1])
\A r \in Readers : \A i \in 0 .. (MaxPublished - 1) :
<>[](i \in 0 .. published => Len(consumed[r]) >= i + 1 /\ consumed[r][i + 1] = i)

=============================================================================
=============================================================================