Add spec of the Disruptor concurrency library. #150
Conversation
Signed-off-by: Nicholas Schultz-Møller <[email protected]>
Signed-off-by: Nicholas Schultz-Møller <[email protected]>
|
Nice spec! Thanks for the contribution. |
|
Thanks, you're welcome. :-) |
|
I can see a lot of checks failing due to different number of states, distinct states, etc. compared to what I get when running the toolbox. Can it be a TLC version issue? Or symmetry vs. non-symmetry sets for model values that differ somehow? Kind regards |
|
Those json fields are optional, although useful as a regression test. I will take a look tomorrow. |
|
It looks like it's not my model that fails but a module called |
|
Sorry, the spec checking has debug output enabled so it's very verbose. You want to search for the text Anyway here is the result: I believe the reason for the failure is that in your model files you have many sets defined as: but this needs to be comma-delimited like: I suggest running TLC locally against these model files (will probably need to be done using the command line) to save time on the debug loop; debug-via-CI-run is very time-consuming! |
| CONSTANTS | ||
| Writers, (* Writer/publisher thread ids. *) | ||
| Readers, (* Reader/consumer thread ids. *) | ||
| MaxPublished, (* Max number of published events. *) |
There was a problem hiding this comment.
I presume this constant is only relevant for model checking? It would be cleaner to separate the logical spec from the bounds imposed for model checking and either add a state constraint such as published < MaxPublished in the cfg file or write a MC version of the spec that adds extra guards to actions.
There was a problem hiding this comment.
Yes and no. I've investigated and the constant does bound the model. So I agree - that would be better to have as a state constraint. But then I can't model check the liveliness property in the model (that all consumers eventually always read all published events) as liveliness cannot be verified when state or action constraints are specified.
Is there a "clean" third option that you know of?
There was a problem hiding this comment.
Beware that "hardcoding" MaxPublished doesn't change anything semantically WRT liveness checking except that it makes TLC not print the warning about action and state-constraints.
There was a problem hiding this comment.
I'm not sure I understand. If I replace MaxPublished with a state-constraint, I cannot make my liveliness property fail (by adding an error in the spec).
As I read the relevant pages in Lamport's book, it's because WF_x(a) is false when adding a state-constraint because a is enabled and thus WF_x(a) is false which in turn never makes the liveliness property fail.
However, if I add the check with the MaxPublished constant as a part of an action then the action is not enabled and therefore the liveliness property can fail (if it's wrong).
There was a problem hiding this comment.
Apologies for the late reply: now I am confused. First, I would rather have defined the liveness property as
Liveliness == \A r \in Readers : \A i \in 1 .. MaxPublished :
<>[](i \in 1 .. published => Len(consumed[r]) >= i /\ consumed[r][i] = i-1)
(with the second conjunct on the right-hand side being optional). The reason is that the property that you assert will not hold if writers are allowed to continue publishing even after reaching the (artificial) bound since readers would then be able to update their consumed sequence as well, whereas the above property should always hold. (Even more general, the bound on i could be Nat but that would require an override of Nat during model checking so that TLC doesn't complain about an infinite quantifier bound, and that would be a little heavy.)
I then tried commenting out the guard next < MaxPublished in BeginWrite and adding the constraint
StateConstraint == published <= MaxPublished
for model checking. This appears to work just fine, and when I comment out the fairness condition on BeginRead, TLC gives me the expected failure of the temporal property.
I would even suggest removing the fairness condition on BeginWrite from the spec, since why should writers be required to publish items forever? The above liveness property (but of course not the original one) continues to hold for the modified spec.
Of course, it's up to you to decide what you intend as your specification.
There was a problem hiding this comment.
Stephan's Liveliness property would allow to model consumed as a counter instead of a sequence (for each reader). This observation also led me to realize that the SPMC specification seems to describe the multicast configuration, since all readers are consuming every value. It might be helpful to include this in a comment for clarity.
There was a problem hiding this comment.
If consumed remains a sequence, you could add the following "action property" (with IsPrefix defined at https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.tla#L219-L225 :
\* We only ever append to the history variable consumed .
Increments ==
[][\A r \in Readers: IsPrefix(consumed[r], consumed'[r])]_varsThere was a problem hiding this comment.
Stephan's
Livelinessproperty would allow to modelconsumedas a counter instead of a sequence (for each reader). This observation also led me to realize that the SPMC specification seems to describe the multicast configuration, since all readers are consuming every value. It might be helpful to include this in a comment for clarity.
Hi @lemmy, I wrote in the top that it's a Single Producer Multiple Consumer Disruptor - that's where I thought I made it clear that it is that configuration of the Disruptor. But perhaps I am assuming that everyone knows all consumers read all events (i.e. "multicast" behaviour) and that is not common knowledge?
There was a problem hiding this comment.
Apologies for the late reply: now I am confused. First, I would rather have defined the liveness property as
Liveliness == \A r \in Readers : \A i \in 1 .. MaxPublished : <>[](i \in 1 .. published => Len(consumed[r]) >= i /\ consumed[r][i] = i-1)(with the second conjunct on the right-hand side being optional). The reason is that the property that you assert will not hold if writers are allowed to continue publishing even after reaching the (artificial) bound since readers would then be able to update their
consumedsequence as well, whereas the above property should always hold. (Even more general, the bound onicould beNatbut that would require an override ofNatduring model checking so that TLC doesn't complain about an infinite quantifier bound, and that would be a little heavy.)I then tried commenting out the guard
next < MaxPublishedinBeginWriteand adding the constraintStateConstraint == published <= MaxPublishedfor model checking. This appears to work just fine, and when I comment out the fairness condition on
BeginRead, TLC gives me the expected failure of the temporal property.I would even suggest removing the fairness condition on
BeginWritefrom the spec, since why should writers be required to publish items forever? The above liveness property (but of course not the original one) continues to hold for the modified spec.Of course, it's up to you to decide what you intend as your specification.
I did the changes (see a new PR) and I quite like it: Getting rid of the artificial model constraint in the BeginWrite action, remove the requirement to have producers publish forever and moving the bounding of the model to a state constraint. Elegant and a better model.
I still have some work to do for the MPMC model as it's more complex to write the liveliness property because there's multiple producers and hence it more difficult to express what sequence number a consumer can actually read. (More details will follow).
There was a problem hiding this comment.
Glad to hear that it worked out! I didn't look very much at the MPMC model, please let me know if you want me to.
|
Hi @muenchnerkindl and @ahelwer - super nice with all the feedback - much appreciated. |
Signed-off-by: Nicholas Schultz-Møller <[email protected]>
…ments. Signed-off-by: Nicholas Schultz-Møller <[email protected]>
Signed-off-by: Nicholas Schultz-Møller <[email protected]>
Signed-off-by: Nicholas Schultz-Møller <[email protected]>
Signed-off-by: Nicholas Schultz-Møller <[email protected]>
|
Hi @muenchnerkindl, @ahelwer and @lemmy, I've fixed all issues related to running the model-checking and I think I've added all your good suggestions. Let me know if you think I can improve the contribution any further. :-) |
|
Hi guys, anything else I can do to improve the contribution? While it's fresh in my head :-) |
| 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. *) |
There was a problem hiding this comment.
Nit: Since the value for each process only alternates between Advance and Access, I would consider renaming the variable to something more descriptive, like hasAccess.
The
Disruptoris a concurrency library originally developed and open sourced by LMAX Exchange for low latency communication via a ring buffer between producer and consumer threads.This PR adds a spec of the Disruptor lib and verifies that data races do not occur.