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 123
    • Issues 123
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 15
    • Merge Requests 15
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI/CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • Iris
  • Issues
  • #120

Closed
Open
Created Dec 04, 2017 by Robbert Krebbers@robbertkrebbersMaintainer

Add atomic fetch-and-add to `heap_lang`

For the sake of demonstrating Iris, it is often useful to have an atomic fetch-and-add instruction (see for example my TTT talk and Derek's MFPS talk). Of course, we can implement such a thing using a CAS loop, but then the proof in Coq becomes quite different from the proof on paper.

Adding an atomic fetch-and-add instruction to heap_lang should be easy, and it makes sense, since many actual architectures have such an instruction.

What do you think? Are there any other common atomic instructions that we may add too? We could add something like:

AtomicBinOp (op : bin_op) (e1 : expr) (e2 : expr).

But it is a bit weird to use it with LeOp, LtOp or EqOp since those change the type of the location.

Edited Dec 04, 2017 by Robbert Krebbers
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None