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 122
    • Issues 122
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 18
    • Merge Requests 18
  • 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
  • #257

Closed
Open
Opened Aug 01, 2019 by Ralf Jung@jungOwner0 of 2 tasks completed0/2 tasks

Auth as Views

Gregory suggested a generalization of "Auth" that, in hindsight, seems blatantly obvious: make the authoritative and the fragment not the same type, and let the user pick some relation between them. I think it can truly be any (Coq-level) relation for discrete types; for the CMRA variant we likely need a step-indexed relation. The existing "auth" is then the special case of using the same type, and equality as the relation.

This subsumes !91 (closed) by making the relation also require bijectivity. And this also could be useful for situations where we have a very right CMRA for the fragments, which often means lots of "junk" data (such as to_agree, of ExclBot). So instead of the pattern where we do exists heap, own (● to_auth heap), we could have this to_auth in the relation.

An open question is what would happen with all our theory about local updates.

Things to do:

  • Implement a generalized "auth as view" library
  • Implement monotone partial bijections (!91 (closed)) in terms of that.
Edited Nov 01, 2019 by Ralf Jung
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: iris/iris#257