Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • E examples
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 0
    • Issues 0
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 2
    • Merge requests 2
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • examples
  • Merge requests
  • !49

Added petersons algorithm as an example of sequential consistency

  • Review changes

  • Download
  • Patches
  • Plain diff
Open Jonas Kastberg requested to merge jihgfee/examples:petersons into master Feb 01, 2022
  • Overview 5
  • Commits 2
  • Pipelines 0
  • Changes 1

A port of Peterson's algorithm--A CAS-free lock for a fixed number of participants (here 2), that relies on sequential consistency--to HeapLang. This is a direct port of the implementation and proof presented in the Cosmo'ICFP20 paper, available online, and all credit goes to the authors (Glen Mével, Jacques-Henri Jourdan, François Pottier) for the original implementation, as the port was very straightforward.

I thought that the lock was quite cute (being CAS-free), and thus could make sense to include in the library of HeapLang (for one as evidence of how its sequentially consistent nature can be used for reasoning), although it is of course up for debate.

I am willing to improve the structure/proof if need be.

NB: Moved from iris!775 (closed) per request

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: petersons