Skip to content

GitLab

Commit 45a38169 authored by Zhen Zhang's avatar Zhen Zhang
Browse files

improve

parent 9cd90a1a
Hide whitespace changes
Inline Side-by-side
Showing with 165 additions and 73 deletions
misc.v
View file @ 45a38169
......@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.tests Require Import atomic.
From iris.algebra Require Import dec_agree frac.
From iris.algebra Require Import dec_agree frac gmap upred_big_op.
From iris.program_logic Require Import auth.
Import uPred.
......@@ -32,5 +32,54 @@ Section lemmas.
Lemma pair_l_frac_op_1' (g g': val):
(1%Qp, DecAgree g') ~~> (((1/2)%Qp, DecAgree g') ⋅ ((1/2)%Qp, DecAgree g')).
Proof. by rewrite pair_op dec_agree_idemp frac_op' Qp_div_2. Qed.
Lemma split_mapk
{Σ} {K: Type} `{Countable K} {V: cmraT}
(m: gmapUR K V) (k: K) (v: V) (R: K → iProp Σ) :
m !! k = Some v → ([★ map] k ↦ v ∈ m, R k) ⊢ R k ★ ([★ map] k ↦ v ∈ delete k m, R k).
Proof. iIntros (?) "HRm". by iApply (big_sepM_delete (fun k _ => R k)). Qed.
Lemma split_mapv
{Σ} {K: Type} `{Countable K} {V: cmraT}
(m: gmapUR K V) (k: K) (v: V) (R: V → iProp Σ) :
m !! k = Some v → ([★ map] k ↦ v ∈ m, R v) ⊢ R v ★ ([★ map] k ↦ v ∈ delete k m, R v).
Proof. iIntros (?) "HRm". by iApply (big_sepM_delete (fun _ v => R v)). Qed.
Lemma map_agree {A: cmraT} m m' (hd: loc) (p q: A) x y:
m !! hd = Some (p, DecAgree y) →
x ≠ y → m = {[hd := (q, DecAgree x)]} ⋅ m' → False.
Proof.
intros H1 H2 H3.
subst. rewrite lookup_op lookup_singleton in H1.
destruct (m' !! hd) as [[b [c|]]|] eqn:Heqn; rewrite Heqn in H1; inversion H1=>//.
destruct (decide (x = c)) as [->|Hneq3]=>//.
- rewrite dec_agree_idemp in H3. by inversion H3.
- rewrite dec_agree_ne in H3=>//.
Qed.
Lemma map_agree_none {A: cmraT} m m' (hd: loc) (q: A) x:
m !! hd = None → m = {[hd := (q, DecAgree x)]} ⋅ m' → False.
Proof.
intros H1 H2. subst. rewrite lookup_op lookup_singleton in H1.
destruct (m' !! hd)=>//.
Qed.
End lemmas.
Section heap_extra.
Context `{heapG Σ}.
Lemma bogus_heap p (q1 q2: Qp) a b:
~((q1 + q2)%Qp ≤ 1%Qp)%Qc →
heap_ctx ★ p ↦{q1} a ★ p ↦{q2} b ⊢ False.
Proof.
iIntros (?) "(#Hh & Hp1 & Hp2)".
iCombine "Hp1" "Hp2" as "Hp".
iDestruct (heap_mapsto_op_1 with "Hp") as "[_ Hp]".
rewrite heap_mapsto_eq. iDestruct (auth_own_valid with "Hp") as %H'.
apply singleton_valid in H'. destruct H' as [H' _].
auto.
Qed.
End heap_extra.
srv.v
View file @ 45a38169
......@@ -3,7 +3,7 @@ From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import upred frac excl dec_agree upred_big_op gset gmap.
From iris.algebra Require Import upred frac agree excl dec_agree upred_big_op gset gmap.
From iris.tests Require Import atomic treiber_stack.
From flatcomb Require Import misc.
......@@ -77,7 +77,7 @@ Section proof.
Definition srv_stack_inv (γ γm γ2: gname) (s: loc) (Q: val → val → Prop) : iProp Σ :=
(∃ xs, is_stack' (p_inv_R γm γ2 Q) xs s γ)%I.
Definition srv_m_inv γm := (∃ m, own γm (● m) ★ [★ map] p ↦ _ ∈ m, ∃ v, p ↦{1/2} v)%I.
Definition srv_m_inv γm := (∃ m : tokR, own γm (● m) ★ [★ map] p ↦ _ ∈ m, ∃ v, p ↦{1/2} v)%I.
Lemma install_push_spec
(Φ: val → iProp Σ) (Q: val → val → Prop)
......@@ -114,7 +114,6 @@ Section proof.
Proof.
iIntros (HN) "(#Hh & #? & #? & HΦ)".
wp_seq. wp_let. wp_alloc p as "Hl".
iDestruct "Hl" as "[Hl1 Hl2]".
iApply pvs_wp.
iVs (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
iVs (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
......@@ -122,66 +121,118 @@ Section proof.
iVs (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
iInv N as ">Hm" "Hclose".
iDestruct "Hm" as (m) "[Hm HRm]".
destruct (decide (m !! p = None)).
destruct (m !! p) eqn:Heqn.
- (* old name *)
iDestruct (split_mapk m with "[HRm]") as "[Hp HRm]"=>//.
iDestruct "Hp" as (?) "Hp". iExFalso. iApply bogus_heap; last by iFrame "Hh Hl Hp". auto.
- (* fresh name *)
iAssert (|=r=> own γm (● ({[p := (1%Qp, DecAgree (γx, γ1, γ3, γ4))]} ⋅ m) ⋅
◯ {[p := (1%Qp, DecAgree (γx, γ1, γ3, γ4))]}))%I with "[Hm]" as "==>[Hm1 Hm2]".
{ iDestruct (own_update with "Hm") as "?"; last by iAssumption.
apply auth_update_no_frag. apply alloc_unit_singleton_local_update=>//. }
iDestruct "Hl" as "[Hl1 Hl2]".
iVs ("Hclose" with "[HRm Hm1 Hl1]").
{ iNext. rewrite /srv_m_inv. iExists ({[p := (1%Qp, DecAgree (γx, γ1, γ3, γ4))]} ⋅ m).
iFrame. replace ({[p := (1%Qp, DecAgree (γx, γ1, γ3, γ4))]} ⋅ m) with (<[p := (1%Qp, DecAgree (γx, γ1, γ3, γ4))]> m); last admit.
iDestruct (big_sepM_insert _ m with "[-]") as "?".
- exact e.
- iSplitR "HRm"; last done. simpl. eauto.
- eauto. }
iAssert (|=r=>own γm (◯ {[p := ((1/2)%Qp, DecAgree (γx, γ1, γ3, γ4))]} ⋅
◯ {[p := ((1/2)%Qp, DecAgree (γx, γ1, γ3, γ4))]}))%I
with "[Hm2]" as "==>[Hfrag1 Hfrag2]".
{ iDestruct (own_update with "Hm2") as "?"; last by iAssumption.
rewrite <- auth_frag_op.
by rewrite op_singleton pair_op dec_agree_idemp frac_op' Qp_div_2. }
iDestruct (own_update with "Hx") as "==>[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
iVsIntro. wp_let. wp_bind ((push _) _).
iApply install_push_spec=>//.
iFrame "#". iFrame "Hx1 Hfrag1 Hl2 Ho1 Ho4". iIntros "_". wp_seq. iVsIntro.
iSpecialize ("HΦ" $! p γx γ1 γ2 γ3 γ4 with "[-Hx2 Hfrag2]")=>//.
iApply ("HΦ" with "Hfrag2 Hx2").
- iExFalso. (* XXX: used name *)
(* iAssert (([★ map] _↦v ∈ delete p m, ∃ v' : val, v = (1%Qp, DecAgree v') ★ p_inv_R γm γ2 Q v') ★ *)
(* (∃ v, v = (1%Qp, DecAgree #p) ★ p_inv_R γm γ2 Q #p))%I *)
(* with "[HRs]" as "[HRs Hp]". *)
admit.
Admitted.
+ iNext. rewrite /srv_m_inv. iExists ({[p := (1%Qp, DecAgree (γx, γ1, γ3, γ4))]} ⋅ m).
iFrame.
replace ({[p := (1%Qp, DecAgree (γx, γ1, γ3, γ4))]} ⋅ m) with
(<[p := (1%Qp, DecAgree (γx, γ1, γ3, γ4))]> m); last by apply insert_singleton_op.
iDestruct (big_sepM_insert _ m with "[-]") as "H"=>//.
iSplitL "Hl1"; last by iAssumption. simpl. auto.
+ iAssert (|=r=>own γm (◯ {[p := ((1/2)%Qp, DecAgree (γx, γ1, γ3, γ4))]} ⋅
◯ {[p := ((1/2)%Qp, DecAgree (γx, γ1, γ3, γ4))]}))%I
with "[Hm2]" as "==>[Hfrag1 Hfrag2]".
{ iDestruct (own_update with "Hm2") as "?"; last by iAssumption.
rewrite <- auth_frag_op.
by rewrite op_singleton pair_op dec_agree_idemp frac_op' Qp_div_2. }
iDestruct (own_update with "Hx") as "==>[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
iVsIntro. wp_let. wp_bind ((push _) _).
iApply install_push_spec=>//.
iFrame "#". iFrame "Hx1 Hfrag1 Hl2 Ho1 Ho4". iIntros "_". wp_seq. iVsIntro.
iSpecialize ("HΦ" $! p γx γ1 γ2 γ3 γ4 with "[-Hx2 Hfrag2]")=>//.
iApply ("HΦ" with "Hfrag2 Hx2").
Qed.
Lemma access x xs m Q (γ γm γ2: gname):
∀ hd: loc,
heapN ⊥ N → x ∈ xs →
heap_ctx ★ ([★ map] _↦v ∈ m, ∃ v' : val,
v = (1%Qp, DecAgree v') ★ p_inv_R γm γ2 Q v') ★ own γ (● m) ★
is_list' γ hd xs
⊢ ∃ hd', (([★ map] _↦v ∈ delete hd' m, ∃ v' : val,
v = (1%Qp, DecAgree v') ★ p_inv_R γm γ2 Q v') ★
∃ v, v = (1%Qp, DecAgree x) ★ p_inv_R γm γ2 Q x) ★ own γ (● m).
Proof.
induction xs as [|x' xs' IHxs'].
- iIntros (? _ Habsurd). inversion Habsurd.
- destruct (decide (x = x')) as [->|Hneq].
+ iIntros (hd HN _) "(#Hh & HR & Hom & Hxs)".
simpl. iDestruct "Hxs" as (hd' q p) "[Hhd [Hev Hxs']]".
rewrite /ev. destruct (m !! hd) eqn:Heqn.
* iDestruct (split_mapv m with "[HR]") as "[Hp HRm]"=>//.
iDestruct "Hp" as (v') "[% ?]".
subst.
destruct (decide (x' = v')) as [->|Hneq].
{ iFrame. eauto. }
{ iExFalso.
iCombine "Hom" "Hev" as "Hauth".
iDestruct (own_valid γ (● m ⋅ ◯ {[hd := (p, DecAgree x')]}) with "[Hauth]") as %H=>//.
iPureIntro.
apply auth_valid_discrete_2 in H as [[af Compose%leibniz_equiv_iff] Valid].
eapply map_agree=>//. }
* iExFalso.
iCombine "Hom" "Hev" as "Hauth".
iDestruct (own_valid γ (● m ⋅ ◯ {[hd := (p, DecAgree x')]}) with "[Hauth]") as %H=>//.
iPureIntro.
apply auth_valid_discrete_2 in H as [[af Compose%leibniz_equiv_iff] Valid].
eapply map_agree_none=>//. rewrite Compose in Heqn. exact Heqn.
+ iIntros (hd HN ?).
assert (x ∈ xs').
{ set_solver. }
iIntros "(#Hh & HRs & Hom & Hxs')".
simpl. iDestruct "Hxs'" as (hd' q p) "[Hhd [Hev Hxs']]".
iApply IHxs'=>//.
iFrame "#". iFrame.
Qed.
Lemma loop_iter_list_spec Φ (f: val) (s hd: loc) Q (γ γm γ2: gname) xs:
heapN ⊥ N →
heap_ctx ★ inv N (srv_stack_inv γ γm γ2 s Q) ★ □ (∀ x:val, WP f x {{ v, ■ Q x v }})%I ★ own γ2 (Excl ()) ★
heapN ⊥ N → (∀ x:val, True ⊢ WP f x {{ v, ■ Q x v }}) →
heap_ctx ★ inv N (srv_stack_inv γ γm γ2 s Q) ★ own γ2 (Excl ()) ★
is_list' γ hd xs ★ (own γ2 (Excl ()) -★ Φ #())
⊢ WP iter' #hd (doOp f) {{ Φ }}.
Proof.
iIntros (HN) "(#Hh & #? & #Hf & Ho2 & Hlist' & HΦ)".
rewrite /doOp.
iIntros (HN Hf) "(#Hh & #? & Ho2 & Hlist' & HΦ)".
iApply pvs_wp.
iDestruct (dup_is_list' with "[Hlist']") as "==>[Hl1 Hl2]"; first by iFrame.
iDestruct (dup_is_list' with "[Hl2]") as "==>[Hl2 Hl3]"; first by iFrame.
iDestruct (iter'_spec _ (p_inv_R γm γ2 Q) _ γ s (is_list' γ hd xs ★ own γ2 (Excl ()))%I xs hd (λ: "p",
match: ! "p" with InjL "x" => "p" <- SOME (f "x") | InjR "_" => #() end)%V (λ: "p",
match: ! "p" with InjL "x" => "p" <- SOME (f "x") | InjR "_" => #() end) with "[-Hl1]") as "Hiter'"=>//.
iDestruct (iter'_spec _ (p_inv_R γm γ2 Q) _ γ s (is_list' γ hd xs ★ own γ2 (Excl ()))%I xs hd
(doOp f) (doOp f)
with "[-Hl1]") as "Hiter'"=>//.
- rewrite /f_spec.
iIntros (Φ' x _ Hin) "(#Hh & #? & (Hls & Ho2) & HΦ')".
iIntros (Φ' p _ Hin) "(#Hh & #? & (Hls & Ho2) & HΦ')".
wp_let. wp_bind (! _)%E. iInv N as (xs') ">Hs" "Hclose".
iDestruct "Hs" as (hd') "[Hhd [Hxs HRs]]".
iDestruct (dup_is_list' with "[Hls]") as "==>[Hls1 Hls2]"; first by iFrame.
iDestruct "HRs" as (m) "[Hom HRs]".
(* now I know x conforms to p_inv:
since is_list' γ hd xs, so for any x ∈ xs,
we can attain its fragment as evidence that it is
mapped to by some k in m; and since "HRs", so we know (tmeporarily)
that x conforms to R.
XXX: I suppose that this part can be further simplified and split out
*)
(* iAssert (p_inv_R γm γ2 Q x) as "Hx". *)
admit.
iDestruct (access with "[Hom HRs Hls1]") as "[Hop Hom]"=>//.
{ iFrame "#". iFrame. }
iDestruct "Hop" as (p') "[Hos Ho]".
iDestruct "Ho" as (v) "[% Hv']". subst.
iDestruct "Hv'" as (γx γ1 γ3 γ4) "H".
iDestruct "H" as (p'' q'') "[% [Ho [Hp | [Hp | [Hp | Hp]]]]]"; subst.
+ iDestruct "Hp" as (y) "(Hp'' & Ho1 & Ho3)".
wp_load. iVs ("Hclose" with "[-HΦ' Ho2 Hls2]").
{ iNext. iExists xs', hd'. iFrame.
iAssert (p_inv_R γm γ2 Q #p'') with "[-Hom Hos]" as "HIp''".
{ iExists γx, γ1, γ3, γ4, p'', q''.
iSplitR; first done. iFrame.
iLeft. iExists y. by iFrame. }
iExists m. iFrame. admit. }
iVsIntro. wp_match. iApply "HΦ'". iFrame.
+ (* major part of proof ... *)
admit.
+ iExFalso. admit.
+ (* same as the first one *)
admit.
- apply to_of_val.
- iFrame "#". iFrame "Hl2 Hl3 Ho2".
iIntros "[_ H]". by iApply "HΦ".
......@@ -190,38 +241,33 @@ Section proof.
Lemma loop_spec Φ (p s: loc) (lk: val) (f: val)
Q (γ2 γm γ γlk: gname) (γx γ1 γ3 γ4: gname):
heapN ⊥ N →
heapN ⊥ N → (∀ x:val, True ⊢ WP f x {{ v, ■ Q x v }}) →
heap_ctx ★ inv N (srv_stack_inv γ γm γ2 s Q) ★ is_lock N γlk lk (own γ2 (Excl ())) ★
own γ3 (Excl ()) ★ (∃ q: Qp, own γm (◯ {[ p := (q, DecAgree (γx, γ1, γ3, γ4)) ]})) ★
□ (∀ x:val, WP f x {{ v, ■ Q x v }})%I ★ (∀ x y, own γx ((1 / 2)%Qp, DecAgree x) -★ ■ Q x y -★ Φ y)
(∀ x y, own γx ((1 / 2)%Qp, DecAgree x) -★ ■ Q x y -★ Φ y)
⊢ WP loop f #p #s lk {{ Φ }}.
Proof.
iIntros (HN) "(#Hh & #? & #? & Ho3 & Hγs & #? & HΦ)".
iIntros (HN Hf) "(#Hh & #? & #? & Ho3 & Hγs & HΦ)".
iLöb as "IH". wp_rec. repeat wp_let.
iDestruct "Hγs" as (q) "Hγs".
wp_bind (! _)%E. iInv N as ">Hinv" "Hclose".
iDestruct "Hinv" as (xs hd) "[Hs [Hxs HRs]]".
(* iAssert (|=r=>own γm (◯ {[p := ((q/2)%Qp, DecAgree (γx, γ1, γ3, γ4))]} ⋅ *)
(* ◯ {[p := ((q/2)%Qp, DecAgree (γx, γ1, γ3, γ4))]}))%I *)
(* with "[Hγs]" as "==>[Hfrag1 Hfrag2]". *)
(* { iDestruct (own_update with "Hγs") as "?"; last by iAssumption. *)
(* rewrite <- auth_frag_op. *)
(* by rewrite op_singleton pair_op dec_agree_idemp frac_op' Qp_div_2. } *)
iDestruct "HRs" as (m) "[Hom HRs]".
destruct (decide (m !! p = None)).
- admit.
(* impossible -- because of the fragment *)
(* There is also problem regarding destruct the cases of lookup ... *)
- admit. (* impossible -- because of the fragment *)
- iAssert (([★ map] _↦v ∈ delete p m, ∃ v' : val, v = (1%Qp, DecAgree v') ★ p_inv_R γm γ2 Q v') ★
(∃ v, v = (1%Qp, DecAgree #p) ★ p_inv_R γm γ2 Q #p))%I
with "[HRs]" as "[HRs Hp]".
{ admit. }
{ admit. (* lookup case analysis problem *)
(* iDestruct (big_sepM_delete with "[HRs]") as "H". *) }
iDestruct "Hp" as (?) "[% Hpr]"; subst.
iDestruct "Hpr" as (γx' γ1' γ3' γ4' p' q') "(% & Hp' & Hp)".
inversion H. subst.
destruct (decide (γ1 = γ1' ∧ γx = γx' ∧ γ3 = γ3' ∧ γ4 = γ4')) as [[? [? [? ?]]]|Hneq].
+ subst.
iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]".
* admit.
* (* trivial *) admit.
* iDestruct "Hp" as (x) "(Hp & Hx & Ho1 & Ho4)".
wp_load.
iVs ("Hclose" with "[-Hp' Ho3 HΦ]").
......@@ -239,11 +285,9 @@ Section proof.
iVs ("Hclose" with "[Hs Hxs1 HRs]").
{ iNext. iExists xs', hd'. by iFrame. }
iVsIntro. iApply loop_iter_list_spec=>//.
iFrame "#". iSplitR; first eauto.
iFrame. iIntros "Ho2".
iFrame "#". iFrame. iIntros "Ho2".
wp_seq. wp_bind (release _). iApply release_spec.
iFrame "~ Hlocked Ho2". wp_seq.
(* maybe q q' should be equal? or we just need any kind of q? *)
iAssert ((∃ q0 : Qp,
own γm (◯ {[p' := (q0, DecAgree (γx', γ1', γ3', γ4'))]})))%I with "[Hp']" as "Hp'".
{ eauto. }
......@@ -257,7 +301,7 @@ Section proof.
wp_load.
iVs ("Hclose" with "[-Hp' Ho3 HΦ]").
{ iNext. iExists xs, hd. iFrame. iExists m. iFrame. (* merge *) admit. }
iVsIntro. wp_match. (* we should close it as it is in this case *)
iVsIntro. wp_match.
wp_bind (try_acquire _). iApply try_acquire_spec.
iFrame "#". iSplit.
{ (* impossible *) admit. }
......@@ -277,11 +321,10 @@ Section proof.
Admitted.
Lemma flat_spec (f: val) Q:
heapN ⊥ N →
heap_ctx ★ □ (∀ x: val, WP f x {{ v, ■ Q x v }})%I
⊢ WP flat f #() {{ f', □ (∀ x: val, WP f' x {{ v, ■ Q x v }}) }}.
heapN ⊥ N → (∀ x:val, True ⊢ WP f x {{ v, ■ Q x v }}) →
heap_ctx ⊢ WP flat f #() {{ f', □ (∀ x: val, WP f' x {{ v, ■ Q x v }}) }}.
Proof.
iIntros (HN) "(#Hh & #?)".
iIntros (HN Hf) "#Hh".
iVs (own_alloc (Excl ())) as (γ2) "Ho2"; first done.
iVs (own_alloc (● (∅: tokR) ⋅ ◯ ∅)) as (γm) "[Hm _]".
{ by rewrite -auth_both_op. }
......@@ -302,11 +345,11 @@ Section proof.
wp_let. iApply loop_spec=>//.
iFrame "Hh Hss Hlk". iFrame.
iSplitL "Hpx"; first eauto.
iSplitR; first eauto. iIntros (? ?) "Hox %".
iIntros (? ?) "Hox %".
destruct (decide (x = a)) as [->|Hneq]; first done.
iExFalso. iCombine "Hx" "Hox" as "Hx".
iDestruct (own_valid with "Hx") as "%".
rewrite pair_op in H0. destruct H0 as [_ ?]. simpl in H0.
rewrite dec_agree_ne in H0=>//.
{ iExFalso. iCombine "Hx" "Hox" as "Hx".
iDestruct (own_valid with "Hx") as "%".
rewrite pair_op in H0. destruct H0 as [_ ?]. simpl in H0.
rewrite dec_agree_ne in H0=>//. }
Qed.
End proof.
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