Commit 4f7546c5 authored by Hai Dang's avatar Hai Dang
Browse files

Minor cleanup of Treiber stack graph proof

parent e048a414
......@@ -270,7 +270,7 @@ Definition in_sloc E T n (on' : option loc) : vProp :=
Definition in_slocs E T S : vProp :=
[ list] n ; on' S ; (next_nodes S), in_sloc E T n on'.
Definition all_slocs T (LVs : list (option loc * view)) : vProp :=
Definition all_slocs (LVs : list (option loc * view)) : vProp :=
(* TODO: use read-only atomic points-to [ROPtsTo] here instead of fractions. *)
[ list] onV LVs,
if onV is (Some n, V)
......@@ -279,9 +279,9 @@ Definition all_slocs T (LVs : list (option loc * view)) : vProp :=
else emp%I
.
#[global] Instance all_slocs_objective T LVs : Objective (all_slocs T LVs).
#[global] Instance all_slocs_objective LVs : Objective (all_slocs LVs).
Proof. apply big_sepL_objective => _ [[n|] V]; apply _. Qed.
#[global] Instance all_slocs_timeless T LVs : Timeless (all_slocs T LVs).
#[global] Instance all_slocs_timeless LVs : Timeless (all_slocs LVs).
Proof. apply big_sepL_timeless => _ [[n|] V]; apply _. Qed.
(* Locs of the Stack: Head, popped nodes, and nodes *)
......@@ -296,7 +296,7 @@ Definition StackLocs_no_exist s (E : event_list) γh T S t0 LVs Vh : vProp :=
HeadValues T LVs' HeadUnpopped S ζh
PushHistory E LVs' StackTopView LVs' Vh
(* anything that is ever in the stack nodes *)
all_slocs T LVs'
all_slocs LVs'
(* the actual stack: all resources are at the top's write view *)
@{Vh} in_slocs E T S
.
......@@ -619,11 +619,9 @@ Proof.
iIntros "(H & #Hs & As & Is)". eauto with iFrame.
Qed.
Lemma all_slocs_node_next_access T LVs n Vn :
Lemma all_slocs_node_next_access LVs n Vn :
(Some n, Vn) LVs
all_slocs T LVs -
all_slocs T LVs
q on, @{Vn} (n >> 0) {q} #(oloc_to_lit on).
all_slocs LVs - all_slocs LVs q on, @{Vn} (n >> 0) {q} #(oloc_to_lit on).
Proof.
iIntros ([i Inn]%elem_of_list_lookup) "As".
rewrite {1}/all_slocs (big_sepL_lookup_acc _ _ _ _ Inn).
......@@ -633,17 +631,10 @@ Proof.
- eauto with iFrame.
Qed.
Lemma all_slocs_app T LVs LVs' :
all_slocs T (LVs ++ LVs') all_slocs T LVs all_slocs T LVs'.
Lemma all_slocs_app LVs LVs' :
all_slocs (LVs ++ LVs') all_slocs LVs all_slocs LVs'.
Proof. by rewrite /all_slocs -big_sepL_app. Qed.
Lemma all_slocs_mono T T' LVs :
T T' all_slocs T LVs all_slocs T' LVs.
Proof.
intros SUB. apply big_sepL_mono => i [[n|] V] Eqon; [|done].
iDestruct 1 as (q on) "Hn". iExists q, on. iFrame.
Qed.
Lemma in_slocs_node_access E T S i n :
S !! i = Some n
in_slocs E T S -
......@@ -1022,7 +1013,7 @@ Proof.
iDestruct (view_at_elim with "sV1 sH1") as "sH1'".
iDestruct (AtomicPtsTo_AtomicSeen_latest_1 with "H sH1'") as %Subζ0.
set Pr : vProp := (@{Vb} all_slocs T2 (LVs2 ++ [(hd_error S2, Vh2)]))%I.
set Pr : vProp := (@{Vb} all_slocs (LVs2 ++ [(hd_error S2, Vh2)]))%I.
(* CAS with possible pointer comparison *)
wp_apply (AtomicSeen_CON_CAS _ _ _ _ _ _ _ (oloc_to_lit on') #n _ Pr
......@@ -1032,7 +1023,7 @@ Proof.
{ iSplit; [done|]. iIntros "!>". destruct on' as [n'|]; [|done].
simpl. iIntros "As !>".
(* acquire a fraction of n' *)
rewrite /Pr (all_slocs_node_next_access _ _ n' V0); last first.
rewrite /Pr (all_slocs_node_next_access _ n' V0); last first.
{ eapply lookup_weaken in Eqth1; [|apply Subζ0]. simpl in Eqth1.
clear -Eqth1. apply toHeadHist_lookup_Some in Eqth1 as (_ & on' & Eq & Eq1).
destruct on' as [n''|]; [|done]. inversion Eq. subst n''.
......@@ -1049,7 +1040,7 @@ Proof.
assert (on = Some l') as ->.
{ clear -Eq. destruct on; by inversion Eq. } clear Eq.
apply elem_of_list_lookup_2 in Eq2.
rewrite (all_slocs_node_next_access _ _ _ _ Eq2).
rewrite (all_slocs_node_next_access _ _ _ Eq2).
iDestruct "As" as "[As En]". iDestruct "En" as (q' on) "En".
rewrite view_at_view_at (shift_0 l') (own_loc_na_own_loc_prim l').
iDestruct (view_at_subjectively with "En") as (C) "En".
......@@ -1134,7 +1125,7 @@ Proof.
{ iIntros "{#}" (InT2). destruct (HV2 n) as [_ In2].
specialize (In2 InT2). apply elem_of_list_fmap in In2 as ([n' Vn] & Eq & In2).
simpl in Eq. subst n'.
rewrite (all_slocs_node_next_access _ _ _ _ In2). clear.
rewrite (all_slocs_node_next_access _ _ _ In2). clear.
iDestruct "As" as "[_ Hn']". iDestruct "Hn'" as (q' on) "Hn'".
iDestruct (view_at_intro with "Hn") as (V') "[_ Hn]".
rewrite !view_at_view_at.
......@@ -1265,16 +1256,14 @@ Proof.
iCombine "Hn Hd" as "Hnd".
set LVs' := (LVs2 ++ [(hd_error S2,Vr)]) ++ [(Some n, Vw)].
iAssert (@{Vb V2} (all_slocs T' LVs' @{Vw} in_slocs E' T' S'))%I
iAssert (@{Vb V2} (all_slocs LVs' @{Vw} in_slocs E' T' S'))%I
with "[As Is Hnd SYE]" as "[As Is]".
{ iDestruct (view_at_mono _ Vw with "Hnd") as "Hnd"; [solve_lat|eauto|].
iDestruct "Hnd" as "[[Hn1 Hn2] Hd]". iSplitL "As Hn1".
- rewrite (all_slocs_app T'). iSplitL "As".
{ iClear "#". rewrite (all_slocs_mono _ _ _ LeT2). by iFrame. }
iDestruct "Hnd" as "[[Hn1 Hn2] Hd]". iClear "#". iSplitL "As Hn1".
- rewrite(all_slocs_app (_ ++ _)). iSplitL "As"; [by iFrame "As"|].
rewrite /all_slocs /=. iSplitL; [|done]. iExists _, (hd_error S2).
rewrite view_at_view_at /=. iFrame "Hn1".
- iClear "#".
rewrite 2!view_at_view_at (in_sloc_cons E'). iSplitR "Is".
- rewrite 2!view_at_view_at (in_sloc_cons E'). iSplitR "Is".
+ iExists v, psId. rewrite /= /in_sloc.
iSplit. { iPureIntro. by rewrite lookup_insert. }
iSplitL "Hn2". { iExists _. by iFrame "Hn2". }
......@@ -1720,7 +1709,7 @@ Proof.
iDestruct (view_at_elim with "sV1 sH1") as "sH1'".
set Pr : vProp :=
((n >> next) {q} #(oloc_to_lit on')
@{Vb} all_slocs T2 (LVs2 ++ [(hd_error S2, Vh2)]))%I.
@{Vb} all_slocs (LVs2 ++ [(hd_error S2, Vh2)]))%I.
wp_apply (AtomicSeen_CON_CAS_live_loc _ _ _ _ _ _ _ n #(oloc_to_lit on') Pr _
with "[$sH1' $H $sV1 HRE $oN $As]"); [done|done|done|solve_ndisj|..].
{ intros t v NE. rewrite lookup_fmap_Some'.
......@@ -1737,7 +1726,7 @@ Proof.
assert (on = Some l') as ->.
{ clear -Eq. destruct on; by inversion Eq. } clear Eq.
apply elem_of_list_lookup_2 in Eq2.
rewrite (all_slocs_node_next_access _ _ _ _ Eq2).
rewrite (all_slocs_node_next_access _ _ _ Eq2).
iDestruct "As" as "[As En]". iDestruct "En" as (q' on) "En".
rewrite view_at_view_at shift_0 own_loc_na_own_loc_prim.
iDestruct (view_at_subjectively with "En") as (C) "En".
......@@ -1820,7 +1809,7 @@ Proof.
iDestruct (own_loc_na_agree with "oN Hnn") as %Eq. iPureIntro.
inversion Eq as [Eq']. by apply oloc_to_lit_inj in Eq'. }
iAssert (@{Vb} all_slocs T2 ((LVs2 ++ [(Some n, V2)]) ++ [(hd_error S2', Vw)]))%I
iAssert (@{Vb} all_slocs ((LVs2 ++ [(Some n, V2)]) ++ [(hd_error S2', Vw)]))%I
with "[Hnn HSh As]" as "As".
{ rewrite {2}/all_slocs big_sepL_app big_sepL_singleton.
iSplitL "As"; [by iFrame|].
......
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