From 954d43aabbfe8a122f7c52e944e413c862fed27a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Mar 2021 10:07:47 +0100
Subject: [PATCH] changelog and improve docs
---
CHANGELOG.md | 10 ++++++++++
iris/algebra/dyn_reservation_map.v | 11 ++++++-----
2 files changed, 16 insertions(+), 5 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 72b73b157..4987007c8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,6 +12,16 @@ lemma.
(`dfrac`) instead of a fraction (`frac`). Normal fractions are now denoted
`â—{#q} a` and `â—V{#q} a`. Lemmas affected by this have been renamed such that
the "frac" in their name has been changed into "dfrac".
+* Generalize `namespace_map` to `reservation_map` which enhances `gmap positive
+ A` with a notion of 'tokens' that enable allocating a particular name in the
+ map. See [algebra.reservation_map](iris/algebra/reservation_map.v) for further
+ information.
+* Add `dyn_reservation_map` which further extends `reservation_map` with the
+ ability to dynamically allocate an infinite set of tokens. This is useful to
+ perform synchronized allocation of the same name in two maps/APIs without
+ dedicated support from one of the involved maps/APIs. See
+ [algebra.dyn_reservation_map](iris/algebra/dyn_reservation_map.v) for further
+ information.
**Changes in `base_logic`:**
diff --git a/iris/algebra/dyn_reservation_map.v b/iris/algebra/dyn_reservation_map.v
index ae73315a0..c6077426c 100644
--- a/iris/algebra/dyn_reservation_map.v
+++ b/iris/algebra/dyn_reservation_map.v
@@ -8,11 +8,12 @@ coPset] which represent the right to allocate a map entry at any position [k ∈
E]. Unlike [reservation_map], [dyn_reservation_map] supports dynamically
allocating these tokens, including infinite sets of them. This is useful when
syncing the keys of this map with another API that dynamically allocates names:
-we can first reserve a fresh infinite set of tokens here, then allocate a new
-*in that set* with the other API, and then use our tokens to allocate the same
-name here. In effect, we have performed synchronized allocation of the same
-name across two maps, without the other API having to have dedicated support for
-this.
+we can first reserve a fresh infinite set [E] of tokens here, then allocate a
+new name *in [E]* with the other API (assuming it offers the usual "allocate a
+fresh name in an infinite set" API), and then use our tokens to allocate the
+same name here. In effect, we have performed synchronized allocation of the
+same name across two maps, without the other API having to have dedicated
+support for this.
The key connectives are [dyn_reservation_map_data k a] (the "points-to"
assertion of this map), which associates data [a : A] with a key [k : positive],
--
GitLab