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 all 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
13 changes: 8 additions & 5 deletions manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -459,11 +459,12 @@
"size": "small",
"mode": "exhaustive search",
"features": [
"state constraint",
"ignore deadlock"
],
"result": "success",
"distinctStates": 112929,
"totalStates": 406505,
"totalStates": 422781,
"stateDepth": 81
},
{
Expand All @@ -472,12 +473,13 @@
"size": "small",
"mode": "exhaustive search",
"features": [
"state constraint",
"liveness",
"ignore deadlock"
],
"result": "success",
"distinctStates": 14365,
"totalStates": 42101,
"totalStates": 44581,
"stateDepth": 61
}
]
Expand All @@ -494,13 +496,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
3 changes: 3 additions & 0 deletions specifications/Disruptor/Disruptor_MPMC.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,5 +12,8 @@ INVARIANTS
TypeOk
NoDataRaces

CONSTRAINT
StateConstraint

CHECK_DEADLOCK
FALSE
66 changes: 46 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 @@ -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 Expand Up @@ -63,7 +66,12 @@ Range(f) ==
{ f[x] : x \in DOMAIN(f) }

MinReadSequence ==
CHOOSE min \in Range(read) : \A r \in Readers : min <= read[r]
CHOOSE min \in Range(read) :
\A r \in Readers : min <= read[r]

MinClaimedSequence ==
CHOOSE min \in Range(claimed_sequence) :
\A w \in Writers : min <= claimed_sequence[w]

(***************************************************************************)
(* Encode whether an index is published by tracking if the slot was *)
Expand All @@ -86,6 +94,20 @@ Publish(sequence) ==
\* Flip whether we're at an even or odd round.
IN published' = [ published EXCEPT ![index] = Xor(TRUE, @) ]

(***************************************************************************)
(* Computes the highest published sequence number that can be read. *)
(* This might seem strange but e.g. a producer P1 can be about to publish *)
(* sequence 5 while producer P2 has published sequence 6 and thus *)
(* consumers can neither read sequence 5 nor 6 (yet). *)
(***************************************************************************)
AvailablePublishedSequence ==
LET guaranteed_published == MinClaimedSequence - 1
candidate_sequences == {guaranteed_published} \union Range(claimed_sequence)
IN CHOOSE max \in candidate_sequences :
IsPublished(max) => ~ \E w \in Writers :
/\ claimed_sequence[w] = max + 1
/\ IsPublished(claimed_sequence[w])

(***************************************************************************)
(* Producer Actions: *)
(***************************************************************************)
Expand All @@ -98,10 +120,9 @@ BeginWrite(writer) ==
IN
\* Are we clear of all consumers? (Potentially a full cycle behind).
/\ min_read >= seq - Size
/\ seq < MaxPublished
/\ claimed_sequence' = [ claimed_sequence EXCEPT ![writer] = seq ]
/\ next_sequence' = seq + 1
/\ Transition(writer, Access, Advance)
/\ Transition(writer, Advance, Access)
/\ Buffer!Write(index, writer, seq)
/\ UNCHANGED << consumed, published, read >>

Expand All @@ -110,7 +131,7 @@ EndWrite(writer) ==
seq == claimed_sequence[writer]
index == Buffer!IndexOf(seq)
IN
/\ Transition(writer, Advance, Access)
/\ Transition(writer, Access, Advance)
/\ Buffer!EndWrite(index, writer)
/\ Publish(seq)
/\ UNCHANGED << claimed_sequence, next_sequence, consumed, read >>
Expand All @@ -125,7 +146,7 @@ BeginRead(reader) ==
index == Buffer!IndexOf(next)
IN
/\ IsPublished(next)
/\ Transition(reader, Access, Advance)
/\ Transition(reader, Advance, Access)
/\ Buffer!BeginRead(index, reader)
\* Track what we read from the ringbuffer.
/\ consumed' = [ consumed EXCEPT ![reader] = Append(@, Buffer!Read(index)) ]
Expand All @@ -136,7 +157,7 @@ EndRead(reader) ==
next == read[reader] + 1
index == Buffer!IndexOf(next)
IN
/\ Transition(reader, Advance, Access)
/\ Transition(reader, Access, Advance)
/\ Buffer!EndRead(index, reader)
/\ read' = [ read EXCEPT ![reader] = next ]
/\ UNCHANGED << claimed_sequence, next_sequence, consumed, published >>
Expand All @@ -148,11 +169,11 @@ EndRead(reader) ==
Init ==
/\ Buffer!Init
/\ next_sequence = 0
/\ claimed_sequence = [ w \in Writers |-> -1 ]
/\ published = [ i \in 0..Size |-> FALSE ]
/\ read = [ r \in Readers |-> -1 ]
/\ consumed = [ r \in Readers |-> << >> ]
/\ pc = [ a \in Writers \union Readers |-> Access ]
/\ claimed_sequence = [ w \in Writers |-> -1 ]
/\ published = [ i \in 0..Buffer!LastIndex |-> FALSE ]
/\ read = [ r \in Readers |-> -1 ]
/\ consumed = [ r \in Readers |-> << >> ]
/\ pc = [ a \in Writers \union Readers |-> Advance ]

Next ==
\/ \E w \in Writers : BeginWrite(w)
Expand All @@ -161,14 +182,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))
/\ \A r \in Readers : WF_vars(BeginRead(r))
/\ \A r \in Readers : WF_vars(EndRead(r))

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

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

StateConstraint == next_sequence <= MaxPublished

(***************************************************************************)
(* Invariants: *)
(***************************************************************************)
Expand All @@ -179,7 +204,7 @@ TypeOk ==
/\ Buffer!TypeOk
/\ next_sequence \in Nat
/\ claimed_sequence \in [ Writers -> Int ]
/\ published \in [ 0..Size -> { TRUE, FALSE } ]
/\ published \in [ 0..Buffer!LastIndex -> { TRUE, FALSE } ]
/\ read \in [ Readers -> Int ]
/\ consumed \in [ Readers -> Seq(Nat) ]
/\ pc \in [ Writers \union Readers -> { Access, Advance } ]
Expand All @@ -188,8 +213,9 @@ TypeOk ==
(* Properties: *)
(***************************************************************************)

(* Eventually always, consumers must have read all published values. *)
(* 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..AvailablePublishedSequence => Len(consumed[r]) >= i + 1 /\ consumed[r][i + 1] = i)

=============================================================================
3 changes: 3 additions & 0 deletions specifications/Disruptor/Disruptor_MPMC_liveliness.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
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
39 changes: 23 additions & 16 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,8 +76,7 @@ BeginWrite(writer) ==
IN
\* Are we clear of all consumers? (Potentially a full cycle behind).
/\ min_read >= next - Size
/\ next < MaxPublished
/\ Transition(writer, Access, Advance)
/\ Transition(writer, Advance, Access)
/\ Buffer!Write(index, writer, next)
/\ UNCHANGED << consumed, published, read >>

Expand All @@ -83,7 +85,7 @@ EndWrite(writer) ==
next == published + 1
index == Buffer!IndexOf(next)
IN
/\ Transition(writer, Advance, Access)
/\ Transition(writer, Access, Advance)
/\ Buffer!EndWrite(index, writer)
/\ published' = next
/\ UNCHANGED << consumed, read >>
Expand All @@ -98,7 +100,7 @@ BeginRead(reader) ==
index == Buffer!IndexOf(next)
IN
/\ published >= next
/\ Transition(reader, Access, Advance)
/\ Transition(reader, Advance, Access)
/\ Buffer!BeginRead(index, reader)
\* Track what we read from the ringbuffer.
/\ consumed' = [ consumed EXCEPT ![reader] = Append(@, Buffer!Read(index)) ]
Expand All @@ -109,7 +111,7 @@ EndRead(reader) ==
next == read[reader] + 1
index == Buffer!IndexOf(next)
IN
/\ Transition(reader, Advance, Access)
/\ Transition(reader, Access, Advance)
/\ Buffer!EndRead(index, reader)
/\ read' = [ read EXCEPT ![reader] = next ]
/\ UNCHANGED << consumed, published >>
Expand All @@ -121,9 +123,9 @@ EndRead(reader) ==
Init ==
/\ Buffer!Init
/\ published = -1
/\ read = [ r \in Readers |-> -1 ]
/\ consumed = [ r \in Readers |-> << >> ]
/\ pc = [ a \in Writers \union Readers |-> Access ]
/\ read = [ r \in Readers |-> -1 ]
/\ consumed = [ r \in Readers |-> << >> ]
/\ pc = [ a \in Writers \union Readers |-> Advance ]

Next ==
\/ \E w \in Writers : BeginWrite(w)
Expand All @@ -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 - bounds 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)

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