Skip to content
GitLab
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 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 14
    • Merge requests 14
  • 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
  • Merge requests
  • !646

New Camera dyn_reservation_map and generalize namespace_map → reservation_map

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Ralf Jung requested to merge ralf/reservation-map into master Mar 08, 2021
  • Overview 24
  • Commits 6
  • Pipelines 0
  • Changes 6

This MR first renames and generalizes the existing namespace_map to reservation_map that works for arbitrary positive keys -- basically this is now a general gmap positive A with support for owning a set of tokens E that can be used to perform allocation at some specific key k ∈ E. The lemma namespace_map_alloc_update further changes to reservation_map_alloc

Then I also add dyn_reservation_map, which is very similar but has the additional constraint that the set of unused tokens must be infinite. This permits a new frame-preserving update that allocates a fresh infinite set of tokens E. The intended use is to then take that infinite set and allocate some fresh name inside it in some other place, and have a guarantee that the newly allocated name can be associated with some data in the dyn_reservation_map. This is a form of "synchronized allocation" where the "other place" does not have to cooperate beyond offering an API to allocate a fresh name in any given infinite set.

dyn_reservation_map is a reimplementation of gsingleton (part of the GhostCell work) by Joshua Yanowski, which in turn is based on ideas by Joshua and me.

Both of these could be generalized to arbitrary countable key types instead of just positive, but I leave that to future work.

Edited Mar 08, 2021 by Ralf Jung
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: ralf/reservation-map