Commit 954d43aa authored by Ralf Jung's avatar Ralf Jung
Browse files

changelog and improve docs

parent aba3bee9
......@@ -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`:**
......
......@@ -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],
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment