Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 148
    • Issues 148
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 8
    • Merge requests 8
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !25

Merged
Created Nov 18, 2016 by Robbert Krebbers@robbertkrebbersMaintainer

State invariants in WP and the dead of heap_ctx.

  • Overview 34
  • Commits 8
  • Pipelines 6
  • Changes 33

This merge request changes the WP construction so that it takes state interpretation as its parameter (part of the irisG type class), instead of building in the authoritative ownership of the entire state. When instantiating WP with a concrete language, one can choose the state interpretation. For example, for heap_lang we directly use auth (gmap loc (frac * dec_agree val)), and avoid the indirection through an invariant managing ownership of the entire state.

As a result, we no longer have to carry around heap_ctx.

Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: state_inv