Commit 36f30c73 authored by Ralf Jung's avatar Ralf Jung

adjust inv_heap users to heap_lang changes

parent 9137bb10
......@@ -102,7 +102,7 @@ Instance subG_cincΣ {Σ} : subG cincΣ Σ → cincG Σ.
Proof. solve_inG. Qed.
Section conditional_counter.
Context {Σ} `{!heapG Σ, !inv_heapG loc val Σ, !cincG Σ}.
Context {Σ} `{!heapG Σ, !cincG Σ}.
Context (N : namespace).
Local Definition stateN := N .@ "state".
......@@ -208,7 +208,7 @@ Section conditional_counter.
Local Hint Extern 0 (environments.envs_entails _ (counter_inv _ _)) => unfold counter_inv : core.
Definition is_counter (γ_n : gname) (ctr : val) :=
( (c : loc), ctr = #c N ## inv_heapN inv_heap_inv loc val inv counterN (counter_inv γ_n c))%I.
( (c : loc), ctr = #c N ## inv_heapN inv_heap_inv inv counterN (counter_inv γ_n c))%I.
Global Instance is_counter_persistent γs ctr : Persistent (is_counter γs ctr) := _.
......@@ -355,7 +355,7 @@ Section conditional_counter.
as a precondition. *)
Lemma complete_spec (c f l : loc) (n : Z) (p : proph_id) γ_n γ_t γ_s l_ghost_inv P Q :
N ## inv_heapN
inv_heap_inv loc val -
inv_heap_inv -
inv counterN (counter_inv γ_n c) -
inv stateN (state_inv P Q p n c l l_ghost_inv γ_n γ_t γ_s) -
pau P Q γ_n f -
......@@ -491,7 +491,7 @@ Section conditional_counter.
Lemma new_counter_spec :
N ## inv_heapN
inv_heap_inv loc val -
inv_heap_inv -
{{{ True }}}
new_counter #()
{{{ ctr γs, RET ctr ; is_counter γs ctr counter_content γs 0 }}}.
......@@ -541,7 +541,7 @@ Section conditional_counter.
End conditional_counter.
Definition atomic_cinc `{!heapG Σ, !cincG Σ, !inv_heapG loc val Σ} :
Definition atomic_cinc `{!heapG Σ, !cincG Σ} :
spec.atomic_cinc Σ :=
{| spec.new_counter_spec := new_counter_spec;
spec.cinc_spec := cinc_spec;
......
......@@ -5,7 +5,7 @@ From iris.heap_lang Require Export lifting notation.
Set Default Proof Using "Type".
(** A general logically atomic interface for conditional increment. *)
Record atomic_cinc {Σ} `{!heapG Σ, !inv_heapG loc val Σ} := AtomicCinc {
Record atomic_cinc {Σ} `{!heapG Σ} := AtomicCinc {
(* -- operations -- *)
new_counter : val;
cinc : val;
......@@ -25,7 +25,7 @@ Record atomic_cinc {Σ} `{!heapG Σ, !inv_heapG loc val Σ} := AtomicCinc {
(* -- operation specs -- *)
new_counter_spec N :
N ## inv_heapN
inv_heap_inv loc val -
inv_heap_inv -
{{{ True }}}
new_counter #()
{{{ ctr γs, RET ctr ; is_counter N γs ctr counter_content γs 0 }}};
......@@ -40,7 +40,7 @@ Record atomic_cinc {Σ} `{!heapG Σ, !inv_heapG loc val Σ} := AtomicCinc {
get v @∖↑N∖↑inv_heapN
<<< counter_content γs n, RET #n >>>;
}.
Arguments atomic_cinc _ {_ _}.
Arguments atomic_cinc _ {_}.
Existing Instances
is_counter_persistent counter_content_timeless
......
......@@ -172,7 +172,7 @@ Instance subG_rdcssΣ {Σ} : subG rdcssΣ Σ → rdcssG Σ.
Proof. solve_inG. Qed.
Section rdcss.
Context {Σ} `{!heapG Σ, !rdcssG Σ, !inv_heapG loc val Σ }.
Context {Σ} `{!heapG Σ, !rdcssG Σ}.
Context (N : namespace).
Implicit Types γ_n γ_a γ_t γ_s : gname.
......@@ -320,7 +320,7 @@ Section rdcss.
Local Hint Extern 0 (environments.envs_entails _ (rdcss_inv _)) => unfold rdcss_inv : core.
Definition is_rdcss (l_n : loc) :=
(inv rdcssN (rdcss_inv l_n) inv_heap_inv loc val N ## inv_heapN)%I.
(inv rdcssN (rdcss_inv l_n) inv_heap_inv N ## inv_heapN)%I.
Global Instance is_rdcss_persistent l_n : Persistent (is_rdcss l_n) := _.
......@@ -486,7 +486,7 @@ Section rdcss.
inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost_inv γ_t γ_s γ_a) -
pau P Q l_n l_m m1 n1 n2 -
l_m ↦□ (λ _, True) -
inv_heap_inv loc val -
inv_heap_inv -
{{{ l_descr {q} (#l_m, m1, n1, n2, #p) }}}
complete #l_descr #l_n
{{{ RET #(); (own_token γ_t ={}= (Q n1)) }}}.
......@@ -638,7 +638,7 @@ Section rdcss.
(** ** Proof of [new_rdcss] *)
Lemma new_rdcss_spec (n : val) :
N ## inv_heapN inv_heap_inv loc val -
N ## inv_heapN inv_heap_inv -
{{{ True }}}
new_rdcss n
{{{ l_n, RET #l_n ; is_rdcss l_n rdcss_state l_n n }}}.
......@@ -685,7 +685,7 @@ Section rdcss.
End rdcss.
Definition atomic_rdcss `{!heapG Σ, !rdcssG Σ, !inv_heapG loc val Σ} :
Definition atomic_rdcss `{!heapG Σ, !rdcssG Σ} :
spec.atomic_rdcss Σ :=
{| spec.new_rdcss_spec := new_rdcss_spec;
spec.rdcss_spec := rdcss_spec;
......
......@@ -12,7 +12,7 @@ as given by [rdcss_spec] relies on the [gc_mapsto l_m m] assertion. It roughly
corresponds to the usual [l_m ↦ m] but with an additional guarantee that [l_m]
will not be deallocated. This guarantees that unique immutable descriptors can
be associated to each operation, and that they cannot be "reused". *)
Record atomic_rdcss {Σ} `{!heapG Σ, !inv_heapG loc val Σ} := AtomicRdcss {
Record atomic_rdcss {Σ} `{!heapG Σ} := AtomicRdcss {
(* -- operations -- *)
new_rdcss : val;
rdcss: val;
......@@ -27,7 +27,7 @@ Record atomic_rdcss {Σ} `{!heapG Σ, !inv_heapG loc val Σ} := AtomicRdcss {
rdcss_state N l_n n1 - rdcss_state N l_n n2 - False;
(* -- operation specs -- *)
new_rdcss_spec N (n : val):
N ## inv_heapN inv_heap_inv loc val -
N ## inv_heapN inv_heap_inv -
{{{ True }}}
new_rdcss n
{{{ l_n, RET #l_n ; is_rdcss N l_n rdcss_state N l_n n }}};
......@@ -44,6 +44,6 @@ Record atomic_rdcss {Σ} `{!heapG Σ, !inv_heapG loc val Σ} := AtomicRdcss {
get #l_n @(∖↑N)
<<< rdcss_state N l_n n, RET n >>>;
}.
Arguments atomic_rdcss _ {_} {_}.
Arguments atomic_rdcss _ {_}.
Existing Instances is_rdcss_persistent rdcss_state_timeless.
Markdown is supported
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