Skip to content

Commit

Permalink
Add small improvements to the Disruptor spec. (#151)
Browse files Browse the repository at this point in the history 
- Add comment on 'Multicast' behaviour.
- Add ASSUME for MaxPublished constant.
- Add comment on the usage of the 'consumed' variable.
- Remove WF from write actions.
- Remove bounding of model happening in BeginWrite action. Use a State
  constraint instead. Use suggestion for liveliness property.
- (The last two items are not done yet for the MPMC spec - it's less
  straight forward to do because of the multiple producers behaviour.)
- Add 'state constraint' to feature list for Disruptor spec.
- Flip 'Advance' and 'Access' state - they were flipped.
- Add state constraint, improve model.
- Flip 'Advance' and 'Access' states - they were flipped.
- Remove model boundary from 'BeginWrite' action - separates spec and
  verification.
- Fix 'published' variable which had an unused mapping.

Signed-off-by: Nicholas Schultz-Møller <[email protected]>
  • Loading branch information
@nicholassm
nicholassm authored Oct 7, 2024
1 parent 7ebd914 commit cfa1614
Show file tree
Hide file tree
Showing 6 changed files with 86 additions and 41 deletions.
13 changes: 8 additions & 5 deletions manifest.json
View file
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",
"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
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
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
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
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
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))
/\ \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)

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

0 comments on commit cfa1614

Please sign in to comment.