Commit c0dd63f2 authored by Hai Dang's avatar Hai Dang
Browse files

Use meta for stack history proof

parent ce0dc131
......@@ -51,19 +51,19 @@ Section Stack.
Qed.
(* Stack Invariant *)
Definition StackInv1 γs γh γg s: vProp :=
E, stk.(StackInv) γs γh s E own γg (E (GSet (to_set E))).
Definition StackInv1 γh γg s: vProp :=
E, stk.(StackInv) γh s E own γg (E (GSet (to_set E))).
Local Existing Instances
StackInv_Objective StackInv_Timeless StackLocal_Persistent
queue_persistent.
Instance StackInv_obj γs γh γg s : Objective (StackInv1 γs γh γg s) := _.
Instance StackInv_obj γh γg s : Objective (StackInv1 γh γg s) := _.
Definition QueueInv s γs γh γg (v : Z) : vProp :=
Definition QueueInv s γh γg (v : Z) : vProp :=
( if decide (v = 2)
then E i e k, E !! i = Some e /\ e.(ge_event) = Push 1 /\ i k
stk.(StackLocal) (mpN .@ "stk") γs γh s E k
stk.(StackLocal) (mpN .@ "stk") γh s E k
own γg (E (GSet {[i]}))
else True)%I.
......@@ -75,15 +75,15 @@ Section Stack.
iIntros (Φ) "_ Post".
rewrite /prog.
wp_apply (new_stack_spec _ (mpN .@ "stk") with "[//]").
iIntros (γs γh s) "[#S SI]".
iIntros (γh s) "[#S SI]".
iMod (Ghost_alloc ) as (γg) "[SA nodes]".
wp_let.
wp_apply (new_queue_spec _ (QueueInv s γs γh γg) with "[//]").
wp_apply (new_queue_spec _ (QueueInv s γh γg) with "[//]").
iIntros (q) "#Q".
wp_let.
(* allocate invariants *)
iMod (inv_alloc (mpN .@ "inv") _ (StackInv1 γs γh γg s) with "[SI SA]") as "#I".
iMod (inv_alloc (mpN .@ "inv") _ (StackInv1 γh γg s) with "[SI SA]") as "#I".
{ iModIntro. rewrite / StackInv1. iExists []. iFrame. }
(*forking *)
......
......@@ -3,6 +3,7 @@ From gpfsl.examples Require Import sflib.
From iris.algebra Require Import auth gset gmap agree.
From iris.proofmode Require Import tactics.
From gpfsl.base_logic Require Import meta_data.
From gpfsl.algebra Require Import mono_list mono_list_list.
From gpfsl.logic Require Import logatom atomics invariants.
......@@ -1123,8 +1124,9 @@ Definition seen_logview_all (E : history) : Prop :=
(** ** Top-level predicates & invariant *)
Definition StackInv γs γg s E : vProp := γh γe ti esi emo stk (ont : option loc) Vt Vi,
γs = encode (γh,γe,ti)
Definition StackInv γg s E : vProp :=
(γh γe : gname) ti esi emo stk (ont : option loc) Vt Vi,
meta s nroot (γh,γe,ti)
(* Logical states *)
history_master γg 1 E
......@@ -1149,11 +1151,12 @@ Definition StackInv γs γg s E : vProp := ∃ γh γe ti esi emo stk (ont : opt
« XO_INTERP : stack_interp E (write_xo E) [] stk »
.
#[global] Instance StackInv_objective γs γg s E : Objective (StackInv γs γg s E) := _.
#[global] Instance StackInv_timeless γs γg s E : Timeless (StackInv γs γg s E) := _.
#[global] Instance StackInv_objective γg s E : Objective (StackInv γg s E) := _.
#[global] Instance StackInv_timeless γg s E : Timeless (StackInv γg s E) := _.
Definition StackLocal (_ : namespace) γs γg s E M : vProp := γh γe ti esi emo,
⌜γs = encode (γh,γe,ti)
Definition StackLocal (_ : namespace) γg s E M : vProp :=
(γh γe : gname) ti esi emo,
meta s nroot (γh,γe,ti)
(* Local snapshot of the history *)
history_snap γg E M
......@@ -1166,8 +1169,8 @@ Definition StackLocal (_ : namespace) γs γg s E M : vProp := ∃ γh γe ti es
lin_of_emo esi emo seq 0 (length E)
.
#[global] Instance StackLocal_persistent N γs γg s E M :
Persistent (StackLocal N γs γg s E M) := _.
#[global] Instance StackLocal_persistent N γg s E M :
Persistent (StackLocal N γg s E M) := _.
(** ** The main linearization lemma *)
Lemma interp_lin_induction E emo stk i
......@@ -1435,31 +1438,31 @@ Local Existing Instances tstk_graphG tstk_emoG.
#[local] Notation vProp := (vProp Σ).
Lemma StackInv_StackLinearizability_instance :
γs γg s E, StackInv γs γg s E StackLinearizability E .
γg s E, StackInv γg s E StackLinearizability E .
Proof.
intros. iDestruct 1 as (??????????) "(_ & _ & _ & _ & _ & _ & %Props)".
intros. iDestruct 1 as (?????????) "(_ & _ & _ & _ & _ & _ & _ & %Props)".
des. iPureIntro. by eapply stack_linearization.
Qed.
Lemma StackInv_history_master_acc_instance :
γs γg s E, StackInv γs γg s E
γg s E, StackInv γg s E
history_master γg 1 E
(history_master γg 1 E - StackInv γs γg s E).
(history_master γg 1 E - StackInv γg s E).
Proof.
intros. iDestruct 1 as (??????????) "[$ ?]". iIntros "$". eauto 11 with iFrame.
intros. iDestruct 1 as (?????????) "(? & $ & ?)". iIntros "$". eauto 11 with iFrame.
Qed.
Lemma StackInv_history_snap_instance :
γs γg s E E' M',
StackInv γs γg s E - history_snap γg E' M' - E' E .
γg s E E' M',
StackInv γg s E - history_snap γg E' M' - E' E .
Proof.
intros. iDestruct 1 as (??????????) "[E ?]". iIntros "E'".
intros. iDestruct 1 as (?????????) "(? & E & ?)". iIntros "E'".
by iDestruct (history_master_snap_included with "E E'") as %?.
Qed.
Lemma StackLocal_history_snap_instance :
N γs γg s E M, StackLocal N γs γg s E M history_snap γg E M.
Proof. intros. iDestruct 1 as (??????) "[$ _]". Qed.
N γg s E M, StackLocal N γg s E M history_snap γg E M.
Proof. intros. iDestruct 1 as (?????) "(_ & $ & _)". Qed.
Lemma new_stack_spec :
new_stack_spec' new_tstack StackLocal StackInv.
......@@ -1468,7 +1471,7 @@ Proof.
wp_lam.
(* allocate head *)
wp_apply wp_new; [done..|].
iIntros (s) "([H†|%] & Hs & Hms)"; [|done].
iIntros (s) "([H†|%] & Hs & Hms & _)"; [|done].
wp_let.
(* initialize head as null, and create protocol *)
rewrite own_loc_na_vec_singleton.
......@@ -1478,18 +1481,16 @@ Proof.
iMod history_master_alloc_empty as (γg) "[E● #E◯]".
iMod (emo_own_alloc [] []) as (γe) "[M● #M◯]".
set γs : gname := encode (γh,γe,ti).
iApply ("Post" $! γs γg). iModIntro.
iMod (meta_set _ _ (γh,γe,ti) nroot with "Hms") as "#Hms"; [done|].
iApply ("Post" $! γg). iModIntro.
iSplitL "".
- iExists γh,γe,ti,[],[]. iFrame "E◯ M◯". iSplit; last iSplit; last iSplit.
+ done.
- iExists γh,γe,ti,[],[]. rewrite shift_0.
iFrame "Hms E◯ M◯". iSplit; last iSplit.
+ iApply SeenLogview_empty.
+ iExists _. iFrame "sn⊒". done.
+ done.
- iExists γh,γe,ti. iExists [],[],[],None,V0,V0. iFrame "E● M●".
iSplit; last iSplit; last iSplit; last iSplit; last iSplit.
+ done.
- iExists γh,γe,ti. iExists [],[],[],None,V0,V0. rewrite shift_0.
iFrame "Hms E● M●". iSplit; last iSplit; last iSplit; last iSplit.
+ iDestruct (view_at_intro with "at↦") as (Vb) "[? ?]". by iExists Vb.
+ done.
+ rewrite /AllLinks //=.
......@@ -1497,25 +1498,21 @@ Proof.
+ iPureIntro. unnw. split_and!; [done..|constructor].
Qed.
(* Prefer the names that appear first... Is it robust? *)
Ltac simplify_encode :=
match goal with
| H1 : ?γ = encode _, H2 : ?γ = encode _ |- _ =>
rewrite H1 in H2; apply (inj encode) in H2 as [= <- <- <-]
end.
Local Tactic Notation "simplify_meta" "with" constr(Hs) :=
iDestruct (meta_agree with Hs) as %[[-> ->]%pair_inj ->]%pair_inj.
Lemma atom_try_push_internal :
N (DISJ: N ## histN) s tid γs γg E0 M V (v : Z) (Posv: 0 < v) (n : loc),
N (DISJ: N ## histN) s tid γg E0 M V (v : Z) (Posv: 0 < v) (n : loc),
(* E1 is a snapshot of the history, locally observed by M *)
V - StackLocal N γs γg s E0 M -
V - StackLocal N γg s E0 M -
(n >> next) - - (n >> data) #v -
(* PUBLIC PRE *)
<<< E, StackInv γs γg s E >>>
<<< E, StackInv γg s E >>>
try_push_internal [ #s ; #n] @ tid; N
<<< (b : bool) V' E' (psId : event_id) ps Vpush M',
(* PUBLIC POST *)
StackInv γs γg s E'
V' @{V'} StackLocal N γs γg s E' M'
StackInv γg s E'
V' @{V'} StackLocal N γg s E' M'
( (* FAIL_RACE case *)
b = false E' = E M' = M
(n >> next) - (n >> data) #v
......@@ -1533,15 +1530,15 @@ Lemma atom_try_push_internal :
.
Proof.
intros. iIntros "#⊒V #StackLocal n↦ d↦" (Φ) "AU".
iDestruct "StackLocal" as (?? ti esi0 emo0 Hγs) "(E◯0 & M◯0 & (%ζh0 & sn⊒0 & %SM0) & %LIN_PERM0)".
iDestruct "StackLocal" as (?? ti esi0 emo0) "(MS & E◯0 & M◯0 & (%ζh0 & sn⊒0 & %SM0) & %LIN_PERM0)".
wp_lam. wp_bind (!ʳˡˣ _)%E.
(* Inv access #1 *)
iMod "AU" as (E1) "[>StackInv [Abort1 _]]".
iDestruct "StackInv" as (??? esi1 emo1 stk1 ont1 Vt1 Vi1 ?)
"(E●1 & M●1 & (%Vb1 & at↦1) & StackNodes1 & AllLinks1 & #SeenMsgsAll1 & %Props1)".
simplify_encode.
iDestruct "StackInv" as (??? esi1 emo1 stk1 ont1 Vt1 Vi1)
"(MS' & E●1 & M●1 & (%Vb1 & at↦1) & StackNodes1 & AllLinks1 & #SeenMsgsAll1 & %Props1)".
simplify_meta with "MS' MS".
(* get snapshot of E1 *)
iDestruct (history_master_snap with "E●1") as "#E◯1".
iDestruct (history_master_snap_included with "E●1 E◯0") as %SubE01.
......@@ -1554,29 +1551,27 @@ Proof.
(* Close Inv #1 *)
iMod ("Abort1" with "[- n↦ d↦]") as "AU".
{ unfold StackInv. iExists _,_,_. iExists esi1,emo1,stk1,ont1,Vt1,Vi1. eauto 10 with iFrame. }
clear Props1.
{ iExists _,_,_. iExists esi1,emo1,stk1,ont1,Vt1,Vi1.
iNext. iFrame "∗"; eauto with iFrame. } clear Props1.
(* check what we just read *)
move: (lookup_weaken _ _ _ _ Eqth1 Subζh1emo1) => /toHeadHist_lookup_Some.
intros (Letith1 & on1 & -> & Eqemo1).
iPoseProof "E◯0" as "E◯0'".
iDestruct "E◯0'" as "[_ PSV]".
iPoseProof "E◯0" as "[_ PSV]".
iDestruct (SeenLogview_closed with "PSV") as %SubME0.
have SubMemo0 : set_Forall (λ e, eidx, lookup_emo esi0 emo0 eidx = Some e) M.
{ intros ??. eapply event_in_esi_emo; [done|]. by apply SubME0. }
(* set n's link to what we read from Head *)
iModIntro. wp_let. wp_op.
iDestruct "n↦" as (vn) "n↦". wp_write. clear vn.
iDestruct "n↦" as (vn) "n↦". wp_write. clear vn Vb1.
clear Vb1.
(* Inv access #2 *)
iMod "AU" as (E2) "[>StackInv [_ Commit2]]".
iDestruct "StackInv" as (??? esi2 emo2 stk2 ont2 Vt2 Vi2 ?)
"(E●2 & M●2 & (%Vb2 & at↦2) & StackNodes2 & AllLinks2 & #SeenMsgsAll2 & %Props2)".
simplify_encode.
iDestruct "StackInv" as (??? esi2 emo2 stk2 ont2 Vt2 Vi2)
"(MS' & E●2 & M●2 & (%Vb2 & at↦2) & StackNodes2 & AllLinks2 & #SeenMsgsAll2 & %Props2)".
simplify_meta with "MS' MS".
have Injemo2 : emo_inj esi2 emo2.
{ apply (lin_perm_emo_inj E2). des. by destruct ESI_EMO_GOOD. }
......@@ -1628,9 +1623,10 @@ Proof.
set Vps := mkDView V V V bLeVV.
iMod ("Commit2" $! false V2 E2 dummy_eid dummy_sevt Vps M with "[-]") as "HΦ".
{ iSplitR "n↦d↦"; last iSplitR; last iSplitR.
- unfold StackInv. iExists _,_,_. iExists esi2,emo2,stk2,ont2,Vt2,Vi2. eauto 10 with iFrame.
- iExists _,_,_. iExists esi2,emo2,stk2,ont2,Vt2,Vi2.
iNext. iFrame "∗"; eauto with iFrame.
- done.
- unfold StackLocal. iExists _,_,_,esi2,emo2. iFrame (Hγs) "M◯2". iSplit; last iSplit.
- iExists _,_,_,esi2,emo2. iFrame "MS M◯2". iSplit; last iSplit.
+ iDestruct "E◯2" as "[$ ?]".
iApply (view_at_mono with "PSVA"); [done|].
by apply SeenLogview_map_mono.
......@@ -1734,13 +1730,13 @@ Proof.
iMod ("Commit2" $! true V2 E2' psId (Push v) Vps M' with "[-]") as "HΦ".
{ des. destruct ESI_EMO_GOOD.
iSplitL; last iSplitL; last iSplitL.
- unfold StackInv. iExists _,_,_. iExists esi2,emo2',stk2',(Some n),Vw2,Vi2.
iFrame (Hγs) "∗". iSplitL; last iSplitL.
- iExists _,_,_. iExists esi2,emo2',stk2',(Some n),Vw2,Vi2.
iFrame "∗". iNext. iSplitL; last iSplitL.
{ (* at↦ *) subst ζn2. rewrite (toHeadHist_insert _ _ _ (Some n)).
- subst emo2'. rewrite !fmap_app /=. eauto with iFrame.
- clear -Letitr2 EqL. rewrite cons_length /=. lia.
- clear. rewrite cons_length /=. lia. }
{ (* SeenMsgsAll γh s E2' esi2 emo2' ti *) iNext. iIntros (???? EMO_LOOKUP).
{ (* SeenMsgsAll γh s E2' esi2 emo2' ti *) iIntros (???? EMO_LOOKUP).
(* TODO: Suspicious repetition of the same case analysis in SM2' proof. *)
case (decide (eidx = emo_ne (length emo2.*1.*1))) as [->|NEeidx].
- subst emo2'. rewrite /= !fmap_app /= in EMO_LOOKUP.
......@@ -1790,7 +1786,7 @@ Proof.
* apply lookup_app_1_eq.
* by constructor.
- done.
- unfold StackLocal. iExists _,_,_,esi2,emo2'. iFrame (Hγs LIN_PERM2') "E◯2' M◯2' PSV2'".
- iExists _,_,_,esi2,emo2'. iFrame (LIN_PERM2') "MS E◯2' M◯2' PSV2'".
iExists ζh2. iFrame "sn⊒2". done.
- by iRight. }
......@@ -1800,7 +1796,7 @@ Qed.
Lemma atom_try_push :
try_push_spec' try_push StackLocal StackInv.
Proof.
intros N DISJ s tid γs γg E0 M V v Posv. iIntros "#⊒V #Es" (Φ) "AU".
intros N DISJ s tid γg E0 M V v Posv. iIntros "#⊒V #Es" (Φ) "AU".
wp_lam.
(* allocate node *)
......@@ -1834,17 +1830,17 @@ Proof.
Qed.
Lemma atom_push_internal :
N (DISJ: N ## histN) s tid γs γg E0 M V (v : Z) (Posv: 0 < v) (n : loc),
N (DISJ: N ## histN) s tid γg E0 M V (v : Z) (Posv: 0 < v) (n : loc),
(* E1 is a snapshot of the history, locally observed by M *)
V - StackLocal N γs γg s E0 M -
V - StackLocal N γg s E0 M -
(n >> next) - - (n >> data) #v -
(* PUBLIC PRE *)
<<< E, StackInv γs γg s E >>>
<<< E, StackInv γg s E >>>
push_internal [ #s ; #n] @ tid; N
<<< V' E' (psId : event_id) ps Vpush M',
(* PUBLIC POST *)
StackInv γs γg s E'
V' @{V'} StackLocal N γs γg s E' M'
StackInv γg s E'
V' @{V'} StackLocal N γg s E' M'
Vpush.(dv_in) = V Vpush.(dv_comm) = V'
(* Vpush ⊑ V' ∧ *) (* << only works if push is also acquiring *)
(* ps is a new push event with which G' strictly extends G *)
......@@ -1878,7 +1874,7 @@ Qed.
Lemma atom_push :
push_spec' push StackLocal StackInv.
Proof.
intros N DISJ s tid γs γg E0 M V v Posv. iIntros "⊒V Es" (Φ) "AU".
intros N DISJ s tid γg E0 M V v Posv. iIntros "⊒V Es" (Φ) "AU".
wp_lam.
(* allocate node *)
wp_apply wp_new; [done..|].
......@@ -1896,16 +1892,16 @@ Qed.
Lemma atom_try_pop :
try_pop_spec' try_pop StackLocal StackInv.
Proof.
intros N DISJ s tid γs γg E0 M V. iIntros "#⊒V #StackLocal" (Φ) "AU".
iDestruct "StackLocal" as (?? ti esi0 emo0 Hγs) "(E◯0 & M◯0 & (%ζh0 & sn⊒0 & %SM0) & %LIN_PERM0)".
intros N DISJ s tid γg E0 M V. iIntros "#⊒V #StackLocal" (Φ) "AU".
iDestruct "StackLocal" as (?? ti esi0 emo0) "(MS & E◯0 & M◯0 & (%ζh0 & sn⊒0 & %SM0) & %LIN_PERM0)".
wp_lam. wp_bind (!ᵃᶜ _)%E.
(* Inv access #1 *)
iMod "AU" as (E1) "[>StackInv Acc1]".
iDestruct "StackInv" as (??? esi1 emo1 stk1 ont1 Vt1 Vi1 ?)
"(E●1 & M●1 & (%Vb1 & at↦1) & StackNodes1 & AllLinks1 & #SeenMsgsAll1 & %Props1)".
simplify_encode.
iDestruct "StackInv" as (??? esi1 emo1 stk1 ont1 Vt1 Vi1)
"(MS' & E●1 & M●1 & (%Vb1 & at↦1) & StackNodes1 & AllLinks1 & #SeenMsgsAll1 & %Props1)".
simplify_meta with "MS' MS".
(* get snapshot of E1 *)
iDestruct (history_master_snap with "E●1") as "#E◯1".
(* initial snapshot is included in E1 *)
......@@ -2013,12 +2009,12 @@ Proof.
iMod ("Commit1" $! EMPTY V1 E1' dummy_eid ppId dummy_sevt EmpPop Vpp M' with "[-]") as "HΦ"; last first.
{ iModIntro. wp_let. wp_op. wp_if. by iApply "HΦ". }
iFrame "⊒V1". rewrite (bi.sep_assoc ( StackInv _ _ _ _)%I).
iFrame "⊒V1". rewrite (bi.sep_assoc ( StackInv _ _ _)%I).
iSplitL; last iSplitL; [|done|by iRight; iLeft].
iSplitL.
+ unfold StackInv. iExists _,_,_. iExists esi1',emo1,stk1',ont1,Vt1,Vi1.
iFrame (Hγs) "∗". iSplitL; last iSplitL; first by eauto with iFrame.
+ iExists _,_,_. iExists esi1',emo1,stk1',ont1,Vt1,Vi1.
iFrame "∗". iSplitL; last iSplitL; first by eauto with iFrame.
{ (* SeenMsgsAll γh s E1' esi1' emo1 ti. *)
iNext. iIntros (???? EMO_LOOKUP).
case (decide (eidx = emo_e O (length esi1))) as [->|NEeidx].
......@@ -2079,7 +2075,7 @@ Proof.
by eapply (HB_EMO eidx1 eidx2).
-- (* LIN_PERM *) done.
* (* XO_INTERP *) done.
+ unfold StackLocal. iExists _,_,_,esi1',emo1. iFrame (Hγs LIN_PERM1') "E◯1' M◯1' PSV1'".
+ iExists _,_,_,esi1',emo1. iFrame (LIN_PERM1') "MS E◯1' M◯1' PSV1'".
iExists ζh1. iFrame (SM1') "sn⊒1".
- subst gen. rewrite ->Egen in *.
des. destruct ESI_EMO_GOOD.
......@@ -2121,13 +2117,13 @@ Proof.
iMod ("Commit1" $! EMPTY V1 E1' dummy_eid ppId dummy_sevt EmpPop Vpp M' with "[-]") as "HΦ"; last first.
{ iModIntro. wp_let. wp_op. wp_if. by iApply "HΦ". }
iFrame "⊒V1". rewrite (bi.sep_assoc ( StackInv _ _ _ _)%I).
iFrame "⊒V1". rewrite (bi.sep_assoc ( StackInv _ _ _)%I).
iSplitL; last iSplitL; [|done|by iRight; iLeft].
iSplitL.
+ unfold StackInv. iExists _,_,_. iExists esi1,emo1',stk1',ont1,Vt1,Vi1.
+ iExists _,_,_. iExists esi1,emo1',stk1',ont1,Vt1,Vi1.
rewrite (_ : emo1.*2 = emo1'.*2); last by rewrite emo_insert_e_2.
iFrame (Hγs) "∗". iSplitL; last iSplitL; first by eauto with iFrame.
iFrame "∗". iSplitL; last iSplitL; first by eauto with iFrame.
{ (* SeenMsgsAll γh s E1' esi1 emo1' ti *)
iNext. iIntros (???? EMO_LOOKUP).
case (decide (eidx = emo_e (S gen') (length es))) as [->|NEeidx].
......@@ -2208,7 +2204,7 @@ Proof.
by eapply (HB_EMO eidx1 eidx2).
-- (* LIN_PERM *) done.
* (* XO_INTERP *) done.
+ unfold StackLocal. iExists _,_,_,esi1,emo1'. iFrame (Hγs LIN_PERM1') "E◯1' M◯1' PSV1'".
+ iExists _,_,_,esi1,emo1'. iFrame (LIN_PERM1') "MS E◯1' M◯1' PSV1'".
iExists ζh1. iFrame (SM1') "sn⊒1". }
(* Possibly non-empty, do not commit yet. *)
......@@ -2222,8 +2218,8 @@ Proof.
(* Close Inv #1 *)
iDestruct "Acc1" as "[Abort1 _]".
iMod ("Abort1" with "[-n1↦]") as "AU".
{ unfold StackInv. iExists _,_,_. iExists esi1,emo1,stk1,ont1,Vt1,Vi1. eauto 10 with iFrame. }
clear Props1.
{ iExists _,_,_. iExists esi1,emo1,stk1,ont1,Vt1,Vi1.
iNext. iFrame "∗"; eauto with iFrame. } clear Props1.
iModIntro. simpl. wp_let. wp_op. wp_if. wp_op.
......@@ -2237,9 +2233,9 @@ Proof.
clear Vb1.
(* Inv access #2 *)
iMod "AU" as (E2) "[>StackInv [_ Commit2]]".
iDestruct "StackInv" as (??? esi2 emo2 stk2 ont2 Vt2 Vi2 ?)
"(E●2 & M●2 & (%Vb2 & at↦2) & StackNodes2 & AllLinks2 & #SeenMsgsAll2 & %Props2)".
simplify_encode.
iDestruct "StackInv" as (??? esi2 emo2 stk2 ont2 Vt2 Vi2)
"(MS' & E●2 & M●2 & (%Vb2 & at↦2) & StackNodes2 & AllLinks2 & #SeenMsgsAll2 & %Props2)".
simplify_meta with "MS' MS".
have Injemo2 : emo_inj esi2 emo2.
{ apply (lin_perm_emo_inj E2). des. by destruct ESI_EMO_GOOD. }
......@@ -2284,9 +2280,9 @@ Proof.
iMod ("Commit2" $! FAIL_RACE V2 E2 dummy_eid dummy_eid
dummy_sevt dummy_sevt Vpp M with "[-]") as "HΦ".
{ iSplitL; last iSplitL; last iSplitL.
- unfold StackInv. iExists _,_,_. iExists esi2,emo2,stk2,ont2,Vt2,Vi2. eauto 10 with iFrame.
- iExists _,_,_. iExists esi2,emo2,stk2,ont2,Vt2,Vi2. eauto 10 with iFrame.
- done.
- unfold StackLocal. iExists _,_,_,esi2,emo2. iFrame (Hγs) "M◯2". iSplit; last iSplit.
- iExists _,_,_,esi2,emo2. iFrame "MS M◯2". iSplit; last iSplit.
+ (* history_snap γg E2 M *)
iDestruct "E◯2" as "[$ ?]".
iApply (view_at_mono with "PSV0"); [solve_lat|].
......@@ -2487,8 +2483,8 @@ Proof.
have ORD_NODUP : NoDup (filter (not_empty_pop E2) (seq 0 (length E2)))
by apply NoDup_filter, NoDup_seq.
iSplitL; last iSplitL; last iSplitL; last iSplitL.
- unfold StackInv. iExists _,_,_. iExists esi2,emo2',stk2',onn,Vw2,Vi2.
iFrame (Hγs) "∗". iSplitL; last iSplitL.
- iExists _,_,_. iExists esi2,emo2',stk2',onn,Vw2,Vi2.
iFrame "∗". iSplitL; last iSplitL.
{ (* at↦ *) subst ζn2. rewrite (toHeadHist_insert _ _ _ onn).
- subst emo2'. rewrite !fmap_app /=. eauto with iFrame.
- clear -Letitr2 EqL. rewrite cons_length /=. lia.
......@@ -2549,7 +2545,7 @@ Proof.
* apply lookup_app_1_eq.
* done.
- done.
- unfold StackLocal. iExists _,_,_,esi2,emo2'. iFrame (Hγs LIN_PERM2') "E◯2' M◯2' PSV2' SM2'".
- iExists _,_,_,esi2,emo2'. iFrame (LIN_PERM2') "MS E◯2' M◯2' PSV2' SM2'".
- done.
- iPureIntro. right; right. subst. split_and!; try done.
+ by apply lookup_lt_is_Some.
......@@ -2565,7 +2561,7 @@ Qed.
Lemma atom_pop :
pop_spec' pop StackLocal StackInv.
Proof.
intros N DISJ s tid γs γg E1 M V. iIntros "#⊒V #Es" (Φ) "AU".
intros N DISJ s tid γg E1 M V. iIntros "#⊒V #Es" (Φ) "AU".
iLöb as "IH" forall "#".
wp_rec.
......
......@@ -66,32 +66,32 @@ Local Notation EMPTY := 0 (only parsing).
Local Notation FAIL_RACE := (-1) (only parsing).
Definition StackLocalT Σ : Type :=
(γs γg : gname) (s : loc) (E : history) (M : logView), vProp Σ.
(γg : gname) (s : loc) (E : history) (M : logView), vProp Σ.
Definition StackLocalNT Σ : Type :=
(N : namespace), StackLocalT Σ.
Definition StackInvT Σ : Type :=
(γs γg : gname) (s : loc) (E : history), vProp Σ.
(γg : gname) (s : loc) (E : history), vProp Σ.
Definition new_stack_spec' {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)}
(new_stack : val) (StackLocal : StackLocalNT Σ) (StackInv : StackInvT Σ) : Prop :=
N tid,
{{{ True }}}
new_stack [] @ tid;
{{{ γs γg (s: loc), RET #s; StackLocal N γs γg s [] StackInv γs γg s [] }}}.
{{{ γg (s: loc), RET #s; StackLocal N γg s [] StackInv γg s [] }}}.
Definition try_push_spec' {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)}
(try_push : val) (StackLocal : StackLocalNT Σ) (StackInv : StackInvT Σ) : Prop :=
N (DISJ: N ## histN) (s: loc) tid γs γg E1 M (V : view) (v : Z) (Posx: 0 < v),
N (DISJ: N ## histN) (s: loc) tid γg E1 M (V : view) (v : Z) (Posx: 0 < v),
(* PRIVATE PRE *)
(* E1 is a snapshot of the history, locally observed by M *)
V - StackLocal N γs γg s E1 M -
V - StackLocal N γg s E1 M -
(* PUBLIC PRE *)
<<< E, StackInv γs γg s E >>>
<<< E, StackInv γg s E >>>
try_push [ #s ; #v] @ tid; N
<<< (b: bool) V' E' (psId : event_id) ps Vpush M',
(* PUBLIC POST *)
StackInv γs γg s E'
V' @{V'} StackLocal N γs γg s E' M'
StackInv γg s E'
V' @{V'} StackLocal N γg s E' M'
(* FAIL_RACE case *)
(b = false E' = E M' = M)
(* successful case *)
......@@ -106,17 +106,17 @@ Definition try_push_spec' {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)}
Definition push_spec' {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)}
(push : val) (StackLocal : StackLocalNT Σ) (StackInv : StackInvT Σ) : Prop :=
N (DISJ: N ## histN) (s: loc) tid γs γg E1 M (V : view) (v : Z) (Posx: 0 < v),
N (DISJ: N ## histN) (s: loc) tid γg E1 M (V : view) (v : Z) (Posx: 0 < v),
(* PRIVATE PRE *)
(* E1 is a snapshot of the history, locally observed by M *)