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

merged 4 commits into from
Oct 7, 2024

Commits on Sep 22, 2024

  1. Add small improvements to specs. 

    - 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.)

Signed-off-by: Nicholas Schultz-Møller <[email protected]>
    @nicholassm
    nicholassm committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    f0bf738 View commit details
    Browse the repository at this point in the history

  2. Add 'state constraint' to feature list for Disruptor spec. 

    Signed-off-by: Nicholas Schultz-Møller <[email protected]>
    @nicholassm
    nicholassm committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    f8cf49d View commit details
    Browse the repository at this point in the history

Commits on Sep 24, 2024

  1. Flip 'Advance' and 'Access' state - they were flipped. 

    Signed-off-by: Nicholas Schultz-Møller <[email protected]>
    @nicholassm
    nicholassm committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    96e5cb9 View commit details
    Browse the repository at this point in the history

  2. 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]>
    @nicholassm
    nicholassm committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    7fbcd9b View commit details
    Browse the repository at this point in the history