New Camera dyn_reservation_map and generalize namespace_map → reservation_map
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.
Merge request reports
Activity
added 6 commits
-
5fc8dd22...5380a1d7 - 5 commits from branch
master - 49f290a4 - rename namespace_map → reservation_map and generalize it to `positive` keys
-
5fc8dd22...5380a1d7 - 5 commits from branch
added 1 commit
- 250a4b8b - rename reservation_map_alloc_update → reservation_map_alloc
mentioned in commit 7cfeca1f
