Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
E
examples
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 0
    • Issues 0
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 1
    • Merge Requests 1
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • examples
  • Merge Requests
  • !37

Closed
Opened Jun 11, 2020 by Simon Friis Vindum@simonfvContributor
  • Report abuse
Report abuse

WIP: MS-queue

  • Overview 6
  • Commits 27
  • Changes 10

This MR adds an additional example to the logrel development: A proof that the Michael-Scott queue, and a variant of it, is a refinement of a course-grained queue.

I've marked the MR WIP as it, at least, needs to be updated with a link to the accompanying notes (they are not hosted anywhere yet, but a draft is here). Additionally, I have an MR with the same proof, but based on ReLoC, here and any feedback on one is probably also applicable to the other.

The MR also makes a few small changes to some of the existing examples better adapting them to changes that have happened in Iris.

Edited Nov 26, 2020 by Ralf Jung
Assignee
Assign to
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Reference: iris/examples!37
Source branch: ms-queue