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
  • #391

Closed
Open
Opened Dec 08, 2020 by Ralf Jung@jungOwner

Add append-only list RA to Iris

Append-only lists are probably the most often requested RA that is not available in Iris. This is a special case of #244, that (a) can be landed without having to figure out how to formalize lattices in general, and (b) would probably be a useful dedicated abstraction even if we get general lattices one day.

@haidang wrote a version of this, which was forked at some point by @jtassaro for Perennial while also adding a logic-level wrapper for auth (mlist T) with the following three core assertions:

  • authoritative ownership of the full trace
  • persistent ownership that some list is a prefix of the trace
  • persistent ownership that index i in the trace has some particular value

Perennial also has another version of this by @tchajed that is based on (the Perennial version of) gmap_view. And finally, @msammler has his own implementation that is based on the list RA.

I do not have a strong preference for which approach to use for the version in Iris, but we should probably look at all of them to figure out what kinds of lemmas people need for this.

Edited Dec 08, 2020 by Ralf Jung
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: iris/iris#391