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
  • Issues
  • #107

Closed
Open
Opened Oct 27, 2017 by Amin Timany@amintimanyDeveloper

Reverting to old (stronger) definition of atomicity

In Iris 3.0 the definition of atomicity was changed to its new definition, i.e., roughly: e is atomic if for any e' such that e reduces to e' we have that e' is stuck.

The old definition was: e is atomic if for any e' such that e reduces to e' we have that e' is a value.

These two definition differ (the new version is strictly weaker) in cases where we are reasoning about facts that unlike WP do not guarantee safety, e.g., IC (if convergent predicates).

Edited Oct 28, 2017 by Ralf Jung
Assignee
Assign to
Iris 3.1
Milestone
Iris 3.1
Assign milestone
Time tracking
None
Due date
None
Reference: iris/iris#107