Commit cbef0e78 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

WIP: generalization to arbirary A locations, one admit

Made a gc access lemma stronger (old one was too weak for the proof)
parent 2491d164
Pipeline #17784 canceled with stage
......@@ -202,26 +202,29 @@ Section gc.
iMod ("Hclose" with "[H● HsepM]"); [ iExists _; by iFrame | by iModIntro].
Qed.
Lemma is_gc_access l E: gcN E gc_inv - is_gc_loc l ={E, E gcN}= v, l v (l v ={E gcN, E}= True).
Lemma is_gc_access l E: gcN E gc_inv - is_gc_loc l ={E, E gcN}=
v, l v
( (b: bool) w, (if b then gc_mapsto l w else True) -
(if b then v = w gc_mapsto l w else True) (l v ={E gcN, E}= True)).
Proof.
iIntros (HN) "#Hinv Hgc_l".
iIntros (HN) "#Hinv #Hgc_l".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iModIntro.
iDestruct "P" as (gcm) "[H● HsepM]".
iDestruct (is_gc_lookup_Some with "Hgc_l H●") as %Hsome.
destruct Hsome as [v Hsome].
iDestruct (is_gc_lookup_Some with "Hgc_l H●") as %HSome.
destruct HSome as [v HSome].
iDestruct (big_sepM_lookup_acc with "HsepM") as "[Hl HsepM]"=>//.
iExists _. iFrame.
iIntros "Hl".
iMod ("Hclose" with "[H● HsepM Hl]"); last done.
iExists _. iFrame.
by (iApply ("HsepM" with "Hl")).
iIntros (b w) "Hgc_l'".
destruct b;
[iDestruct (gc_mapsto_lookup_Some with "Hgc_l' H●") as %?;
simplify_eq;
iSplitL "Hgc_l'"; first by iFrame | iSplit; first done
];
iIntros "Hl";
iMod ("Hclose" with "[H● HsepM Hl]"); try done;
iExists _; iFrame;
by (iApply ("HsepM" with "Hl")).
Qed.
End gc.
This diff is collapsed.
From stdpp Require Import namespaces.
From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic.
From iris_examples.logatom.rdcss Require Export gc.
Set Default Proof Using "Type".
(** A general logically atomic interface for conditional increment. *)
Record atomic_rdcss {Σ} `{!heapG Σ} := AtomicRdcss {
Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
(* -- operations -- *)
new_rdcss : val;
rdcss: val;
set_value: val;
get : val;
(* -- other data -- *)
name : Type;
name_eqdec : EqDecision name;
name_countable : Countable name;
(* -- predicates -- *)
is_rdcss (N : namespace) (γs : name) (v : val) : iProp Σ;
rdcss_content (γs : name) (m n : Z) : iProp Σ;
is_rdcss (N : namespace) (γ : name) (v : val) : iProp Σ;
rdcss_content (γ : name) (n : Z) : iProp Σ;
(* -- predicate properties -- *)
is_rdcss_persistent N γs v : Persistent (is_rdcss N γs v);
rdcss_content_timeless γs f c : Timeless (rdcss_content γs f c);
rdcss_content_exclusive γs f1 c1 f2 c2 : rdcss_content γs f1 c1 - rdcss_content γs f2 c2 - False;
is_rdcss_persistent N γ v : Persistent (is_rdcss N γ v);
rdcss_content_timeless γ lln : Timeless (rdcss_content γ lln);
rdcss_content_exclusive γ lln1 lln2 : rdcss_content γ lln1 - rdcss_content γ lln2 - False;
(* -- operation specs -- *)
new_rdcss_spec N :
{{{ True }}}
new_rdcss #()
{{{ ctr γs, RET ctr ; is_rdcss N γs ctr rdcss_content γs 0 0 }}};
rdcss_spec N γs v (m1 n1 n2 : Z):
is_rdcss N γs v -
<<< (m n: Z), rdcss_content γs m n >>>
rdcss v #m1 #n1 #n2 @∖↑N
<<< rdcss_content γs m (if decide (m = m1 n = n1) then n2 else n), RET #(bool_decide (n = n1)) >>>;
set_value_spec N γs v (new_m: Z) :
is_rdcss N γs v -
<<< (m n : Z), rdcss_content γs m n >>>
set_value v #new_m @∖↑N
<<< rdcss_content γs new_m n, RET #() >>>;
get_spec N γs v:
is_rdcss N γs v -
<<< (m n : Z), rdcss_content γs m n >>>
get v @∖↑N
<<< rdcss_content γs m n, RET #n >>>;
{{{ lln γ, RET lln ; is_rdcss N γ lln rdcss_content γ 0 }}};
rdcss_spec N γ v lm (m1 n1 n2 : Z):
N ## gcN is_rdcss N γ v - is_gc_loc lm - gc_inv -
<<< (m n: Z), gc_mapsto lm #m rdcss_content γ n >>>
rdcss v #lm #m1 #n1 #n2 @((∖↑N)∖↑gcN)
<<< gc_mapsto lm #m rdcss_content γ (if decide (m = m1 n = n1) then n2 else n), RET #(bool_decide (n = n1)) >>>;
get_spec N γ v:
N ## gcN gc_inv - is_rdcss N γ v -
<<< (n : Z), rdcss_content γ n >>>
get v @(∖↑N)
<<< rdcss_content γ n, RET #n >>>;
}.
Arguments atomic_rdcss _ {_}.
Arguments atomic_rdcss _ {_} {_}.
Existing Instances
is_rdcss_persistent rdcss_content_timeless
name_countable name_eqdec.
name_countable name_eqdec.
\ No newline at end of file
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