Skip to content

GitLab

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

Merged
Opened Jun 19, 2019 by Ralf Jung@jungOwner

Turn CAS from compare-and-set to compare-and-swap

  • Overview 53
  • Commits 13
  • Changes 17

heap_lang has always had a compare-and-set operation that just returns a bool indicating success or failure. In contrast, the typical operation provided in "real" languages is compare-and-swap, which returns the old value. Compare-and-set can be written with compare-and-swap, but not vice versa. So I propose we change heap_lang's primitive to be a compare-and-swap instead.

We need this in a case study to faithfully model RDCSS.

The advantage of this is that giving this operation a spec as a single Hoare triple is actually less annoying because one does not need to write the decision thing twice (see atomic_heap.v). This also merges the two reduction rules for CAS into one, so now we finally have exactly one rule per primitive.

The disadvantage is that CAS l v1 v2 = v1 (which is the way to test if the swap happened) is not atomic, so some proofs need adjustment. I tried giving this operation a "logically atomic" spec (not using the full logically atomic triples but the simpler ones that don't support aborts, which makes the spec strictly stronger and much easier to use), but while conceptually helpful it doesn't actually help with the Coq proofs (see counter.v).

Edited Jun 19, 2019 by Ralf Jung
Assignee
Assign to
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Reference: iris/iris!274
Source branch: ralf/cas

Revert this merge request

This will create a new commit in order to revert the existing changes.

Switch branch
Cancel
A new branch will be created in your fork and a new merge request will be started.

Cherry-pick this merge request

Switch branch
Cancel
A new branch will be created in your fork and a new merge request will be started.