Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 16
    • Merge requests 16
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #107
Closed
Open
Issue created 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
Time tracking