Commit f9e04141 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

changed gc library with Ralf's change and adjusted proofs

parent f96d6cb7
......@@ -112,7 +112,9 @@ Section to_gc_map.
End to_gc_map.
Section gc.
Context `{!invG Σ, !heapG Σ, gG: gcG Σ}.
Context `{!invG Σ, !heapG Σ, !gcG Σ}.
(* FIXME: still needs a constructor. *)
Global Instance is_gc_loc_persistent (l: loc): Persistent (is_gc_loc l).
Proof. rewrite /is_gc_loc. apply _. Qed.
......@@ -158,7 +160,7 @@ Section gc.
iFrame.
Qed.
Lemma is_gc_lookup_Some l gcm: is_gc_loc l - own (gc_name gG) ( to_gc_map gcm) - v, gcm !! l = Some v.
Lemma is_gc_lookup_Some l gcm: is_gc_loc l - own (gc_name _) ( to_gc_map gcm) - v, gcm !! l = Some v.
iIntros "Hgc_l H◯".
iCombine "H◯ Hgc_l" as "Hcomb".
iDestruct (own_valid with "Hcomb") as %Hvalid.
......@@ -170,7 +172,7 @@ Section gc.
by apply leibniz_equiv_iff in Hsome.
Qed.
Lemma gc_mapsto_lookup_Some l v gcm: gc_mapsto l v - own (gc_name gG) ( to_gc_map gcm) - gcm !! l = Some v .
Lemma gc_mapsto_lookup_Some l v gcm: gc_mapsto l v - own (gc_name _) ( to_gc_map gcm) - gcm !! l = Some v .
Proof.
iIntros "Hgc_l H●".
iCombine "H● Hgc_l" as "Hcomb".
......@@ -180,12 +182,17 @@ Section gc.
by apply gc_map_singleton_included.
Qed.
Lemma gc_access l v E:
gcN E gc_inv - gc_mapsto l v ={E, E gcN}= (l v ( w, l w ={E gcN, E}= gc_mapsto l w)).
(** An accessor to make use of [gc_mapsto].
This opens the invariant *before* consuming [gc_mapsto] so that you can use
this before opening an atomic update that provides [gc_mapsto]!. *)
Lemma gc_access E:
gcN E
gc_inv ={E, E gcN}= l v, gc_mapsto l v -
(l v ( w, l w == gc_mapsto l w |={E gcN, E}=> True)).
Proof.
iIntros (HN) "#Hinv Hgc_l".
iIntros (HN) "#Hinv".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iModIntro.
iIntros "!>" (l v) "Hgc_l".
iDestruct "P" as (gcm) "[H● HsepM]".
iDestruct (gc_mapsto_lookup_Some with "Hgc_l H●") as %Hsome.
iDestruct (big_sepM_delete with "HsepM") as "[Hl HsepM]"=>//.
......@@ -199,32 +206,24 @@ Section gc.
iDestruct (big_sepM_insert with "[Hl HsepM]") as "HsepM"; [ | iFrame | ].
{ apply lookup_delete. }
rewrite insert_delete. rewrite <- to_gc_map_insert.
iModIntro. iFrame.
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
( (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)).
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).
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 (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")).
iIntros "Hl".
iMod ("Hclose" with "[H● HsepM Hl]"); last done.
iExists _. iFrame.
by (iApply ("HsepM" with "Hl")).
Qed.
End gc.
......@@ -407,15 +407,12 @@ Section rdcss.
complete #l_n #l_m #l_descr #m1 #n1 #n2 #p
{{{ RET #(); (own_token γ_t ={}= (Q #true)) }}}.
Proof.
iIntros (Hdisj) "#InvC #InvS #PAU #GC #InvGC".
iIntros (Hdisj) "#InvC #InvS #PAU #isGC #InvGC".
iModIntro. iIntros (Φ) "_ HQ". wp_lam. wp_pures.
wp_alloc l_ghost as "[Hl_ghost' Hl_ghost'2]". wp_pures.
wp_bind (! _)%E.
(* read lm *)
iMod (is_gc_access with "InvGC GC") as (v) "[Hlm HcloseGC]"=>//.
(* open outer invariant *)
iInv rdcssN as (s) "(>Hln & Hrest)"=>//.
wp_load.
(* two different proofs depending on whether we are succeeding thread *)
destruct (decide (l_ghost_inv = l_ghost)) as [-> | Hnl].
- (* we are the succeeding thread *)
......@@ -424,26 +421,32 @@ Section rdcss.
+ (* Pending: update to accepted *)
iDestruct "Pending" as "[P >[Hvs Hn●]]".
iDestruct ("PAU" with "P") as ">AU".
(* open and *COMMIT* AU, sync flag and counter *)
iMod (gc_access with "InvGC") as "Hgc"; first solve_ndisj.
(* open and *COMMIT* AU, sync B location l_n and A location l_m *)
iMod "AU" as (m' n') "[CC [_ Hclose]]".
{ admit. }
iDestruct "CC" as "[Hgc_lm Hn◯]".
(* sync B location and update it if required *)
iDestruct (sync_num_values with "Hn● Hn◯") as %->.
iDestruct ("HcloseGC" $! true with "Hgc_lm") as "((Heq & Hgc_lm) & HcloseGC)".
iDestruct "Heq" as %->.
iMod (update_num_value _ _ _ (if decide (m' = m1 n' = n') then n2 else n') with "Hn● Hn◯")
as "[Hn● Hn◯]".
(* get access to A location *)
iDestruct ("Hgc" with "Hgc_lm") as "[Hl Hgc_close]".
(* read A location *)
wp_load.
(* sync A location *)
iMod ("Hgc_close" with "Hl") as "[Hgc_lm Hgc_close]".
(* give back access to A location *)
iMod ("Hclose" with "[Hn◯ Hgc_lm]") as "Q"; first by iFrame.
iModIntro. iMod "Hgc_close" as "_".
(* close state inv *)
iModIntro. iSplitL "Q Hl_ghost' Hp Hvs Hs Hln'".
{ iNext. iExists _. iFrame "Hp". iLeft. iFrame.
{ iModIntro. iNext. iExists _. iFrame "Hp". iLeft. iFrame.
iRight. iSplitL "Hl_ghost'"; first by iExists _.
case_bool_decide; simplify_eq;
destruct (val_to_some_loc l_descr vs) eqn:Hvts; iFrame. }
(* close outer inv *)
iModIntro. iSplitR "Hl_ghost'2 HQ Hn● Hlm HcloseGC".
{ iNext. iExists _. iFrame. eauto. }
iMod ("HcloseGC" with "Hlm").
iModIntro. iSplitR "Hl_ghost'2 HQ Hn●".
{ iModIntro. iExists _. iFrame. eauto. }
iModIntro.
destruct (decide (m' = m1)) as [-> | ?];
wp_op;
......@@ -463,20 +466,19 @@ Section rdcss.
by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %?.
- (* we are the failing thread *)
(* close invariant *)
iMod (is_gc_access with "InvGC isGC") as (v) "[Hlm Hclose]"; first solve_ndisj.
wp_load.
iMod ("Hclose" with "Hlm") as "_". iModIntro.
iModIntro.
iSplitL "Hln Hrest".
{ iNext. iExists _. iFrame. iFrame. }
iDestruct ("HcloseGC" $! false #0) as "HcloseGC".
iDestruct (wand_elim_l with "[HcloseGC]") as "HcloseGC"; first iFrame.
iDestruct "HcloseGC" as "(_ & HcloseGC)".
iMod ("HcloseGC" with "Hlm"). iModIntro.
{ iExists _. iFrame. iFrame. }
(* two equal proofs depending on value of m1 *)
wp_op.
destruct (decide (v = #m1)) as [-> | ];
case_bool_decide; simplify_eq; wp_if; wp_pures;
iApply (complete_failing_thread
with "InvC InvS PAU HQ"); done.
Admitted.
Qed.
(** ** Proof of [rdcss] *)
Lemma rdcss_spec γ_n v (l_m: loc) (m1 n1 n2: Z) :
......
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