This MR first renames and generalizes the existing
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
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.