Commit 3bb9aedd authored by Zhen Zhang's avatar Zhen Zhang
Browse files

rewrite: hope i got things right this time

parent 889d57f1
...@@ -7,20 +7,20 @@ From iris.algebra Require Import upred frac excl dec_agree upred_big_op gset gma ...@@ -7,20 +7,20 @@ From iris.algebra Require Import upred frac excl dec_agree upred_big_op gset gma
From iris.tests Require Import atomic treiber_stack. From iris.tests Require Import atomic treiber_stack.
From flatcomb Require Import misc. From flatcomb Require Import misc.
Definition doOp : val := Definition doOp (f: val) : val :=
λ: "f" "p", λ: "p",
match: !"p" with match: !"p" with
InjL "x" => "p" <- InjR ("f" "x") InjL "x" => "p" <- InjR (f "x")
| InjR "_" => #() | InjR "_" => #()
end. end.
Definition loop : val := Definition loop (f: val): val :=
rec: "loop" "p" "f" "s" "lk" := rec: "loop" "p" "s" "lk" :=
match: !"p" with match: !"p" with
InjL "_" => InjL "_" =>
if: CAS "lk" #false #true if: CAS "lk" #false #true
then iter (doOp "f") "s" then iter (doOp f) "s"
else "loop" "p" "f" "s" "lk" else "loop" "p" "s" "lk"
| InjR "r" => "r" | InjR "r" => "r"
end. end.
...@@ -31,240 +31,127 @@ Definition install : val := ...@@ -31,240 +31,127 @@ Definition install : val :=
push "s" "p";; push "s" "p";;
"p". "p".
Definition flat : val := Definition flat (f: val) : val :=
λ: "f", λ: "f",
let: "lk" := ref (#false) in let: "lk" := ref (#false) in
let: "s" := new_stack #() in let: "s" := new_stack #() in
λ: "x", λ: "x",
let: "p" := install "x" "s" in let: "p" := install "x" "s" in
loop "p" "f" "s" "lk". loop f "p" "s" "lk".
Global Opaque doOp install loop flat. Global Opaque doOp install loop flat.
Definition srvR := prodR fracR (dec_agreeR val). Definition srvR := prodR fracR (dec_agreeR val).
Class srvG Σ := SrvG { srv_G :> inG Σ srvR }. Definition tokR := evmapR loc (gname * gname * gname * gname).
Definition srvΣ : gFunctors := #[GFunctor (constRF srvR)]. Class srvG Σ := SrvG {
srv_G :> inG Σ srvR;
tok_G :> inG Σ (authR tokR);
}.
Definition srvΣ : gFunctors :=
#[ GFunctor (constRF srvR);
GFunctor (constRF (authR tokR))
].
Instance subG_srvΣ {Σ} : subG srvΣ Σ srvG Σ. Instance subG_srvΣ {Σ} : subG srvΣ Σ srvG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed. Proof. intros [?%subG_inG [?%subG_inG _]%subG_inv]%subG_inv. split; apply _. Qed.
Section proof. Section proof.
Context `{!heapG Σ, !lockG Σ, !evidenceG loc val Σ, !srvG Σ} (N : namespace). Context `{!heapG Σ, !lockG Σ, !evidenceG loc val Σ, !srvG Σ} (N : namespace).
Definition p_inv Definition p_inv
(γx γ1 γ2 γ3 γ4: gname) (γm γx γ1 γ2 γ3 γ4: gname)
(Q: val val Prop) (Q: val val Prop)
(v: val): iProp Σ := (v: val): iProp Σ :=
(( (y: val), v = InjRV y own γ1 (Excl ()) own γ3 (Excl ())) ( (p : loc) (q: Qp), v = #p own γm ( ({[ p := (q, DecAgree (γx, γ1, γ3, γ4)) ]} : tokR))
( (x: val), v = InjLV x own γx ((1/2)%Qp, DecAgree x) own γ1 (Excl ()) own γ4 (Excl ())) (( (y: val), p InjRV y own γ1 (Excl ()) own γ3 (Excl ()))
( (x: val), v = InjLV x own γx ((1/4)%Qp, DecAgree x) own γ2 (Excl ()) own γ4 (Excl ())) ( (x: val), p InjLV x own γx ((1/2)%Qp, DecAgree x) own γ1 (Excl ()) own γ4 (Excl ()))
( (x y: val), v = InjRV y own γx ((1/2)%Qp, DecAgree x) Q x y own γ1 (Excl ()) own γ4 (Excl ())))%I. ( (x: val), p InjLV x own γx ((1/4)%Qp, DecAgree x) own γ2 (Excl ()) own γ4 (Excl ()))
( (x y: val), p InjRV y own γx ((1/2)%Qp, DecAgree x) Q x y own γ1 (Excl ()) own γ4 (Excl ()))))%I.
Definition p_inv_R γ2 Q v : iProp Σ := ( γx γ1 γ3 γ4: gname, p_inv γx γ1 γ2 γ3 γ4 Q v)%I. Definition p_inv_R γm γ2 Q v : iProp Σ :=
( γx γ1 γ3 γ4: gname, p_inv γm γx γ1 γ2 γ3 γ4 Q v)%I.
Definition srv_inv (γ γ2: gname) (s: loc) (Q: val val Prop) : iProp Σ := Definition srv_stack_inv (γ γm γ2: gname) (s: loc) (Q: val val Prop) : iProp Σ :=
( xs, is_stack' (p_inv_R γ2 Q) xs s γ)%I. ( xs, is_stack' (p_inv_R γm γ2 Q) xs s γ)%I.
Instance p_inv_timeless γx γ1 γ2 γ3 γ4 p Q: TimelessP (p_inv γx γ1 γ2 γ3 γ4 p Q). Definition srv_m_inv γm := ( m, own γm ( m))%I.
Proof. apply _. Qed.
Instance srv_inv_timeless γ γ2 s Q: TimelessP (srv_inv γ γ2 s Q). Lemma install_push_spec
(Φ: val iProp Σ) (Q: val val Prop)
(p: loc) (γ γm γx γ1 γ2 γ3 γ4: gname)
(s: loc) (x: val) :
heapN N
heap_ctx inv N (srv_stack_inv γ γm γ2 s Q) own γx ((1/2)%Qp, DecAgree x)
own γm ( ({[ p := ((1 / 2)%Qp, DecAgree (γx, γ1, γ3, γ4)) ]}))
p InjLV x own γ1 (Excl ()) own γ4 (Excl ()) (True - Φ #())
WP push #s #p {{ Φ }}.
Proof. Proof.
apply uPred.exist_timeless. iIntros (HN) "(#Hh & #? & Hx & Hpm & Hp & Ho1 & Ho2 & HΦ)".
move=>x. apply is_stack'_timeless. rewrite /srv_stack_inv.
move=>v. apply _. iDestruct (push_spec N (p_inv_R γm γ2 Q) with "[-HΦ]") as "Hpush"=>//.
- iFrame "Hh". iSplitL "Hx Hp Hpm Ho1 Ho2"; last eauto.
iExists γx, γ1, γ3, γ4. iExists p, (1/2)%Qp. iSplit=>//. iFrame "Hpm".
iRight. iLeft.
iExists x. iFrame.
- iApply wp_wand_r.
iSplitL "Hpush"; first done.
iIntros (?). iIntros "%".
inversion H. by iApply "HΦ".
Qed. Qed.
(* Lemma push_spec *) Lemma install_spec
(* (Φ: val iProp Σ) (Q: val val Prop) *) (Φ: val iProp Σ) (Q: val val Prop)
(* (p: loc) (γx γ1 γ2 γ3 γ4: gname) *) (x: val) (γ2 γm γ: gname) (s: loc):
(* (γhd γgn: gname) (s: loc) (x: val) : *) heapN N
(* heapN N *) heap_ctx inv N (srv_stack_inv γ γm γ2 s Q) inv N (srv_m_inv γm)
(* heap_ctx inv N (srv_inv γhd γgn s Q) own γx ((1/2)%Qp, DecAgree x) *) ( (p: loc) (γx γ1 γ2 γ3 γ4: gname),
(* p InjLV x own γ1 (Excl ()) own γ4 (Excl ()) (True - Φ #()) *) own γ3 (Excl ()) - own γm ( {[ p := ((1 / 2)%Qp, DecAgree (γx, γ1, γ3, γ4)) ]}) -
(* WP push #s #p {{ Φ }}. *) own γx ((1/2)%Qp, DecAgree x) - Φ #p)
(* Proof. *) WP install x #s {{ Φ }}.
(* iIntros (HN) "(#Hh & #Hsrv & Hp & Hx & Ho1 & Ho4 & HΦ)". *) Proof.
(* iDestruct (push_atomic_spec N s #p with "Hh") as "Hpush"=>//. *) iIntros (HN) "(#Hh & #? & #? & HΦ)".
(* rewrite /push_triple /atomic_triple. *) wp_seq. wp_let. wp_alloc p as "Hl".
(* iSpecialize ("Hpush" $! (p InjLV x own γ1 (Excl ()) own γ4 (Excl ()) *) iVs (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
(* own γx ((1/2)%Qp, DecAgree x))%I *) iVs (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
(* (fun _ ret => ret = #())%I with "[]"). *) iVs (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
(* - iIntros "!#". iIntros "(Hp & Hx & Ho1 & Ho4)". *) iVs (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
(* (* open the invariant *) *) iDestruct (own_update with "Hx") as "==>[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
(* iInv N as (hds gnm) ">(Hohd & Hogn & Hxs & Hhd & Hps)" "Hclose". *) wp_let. wp_bind ((push _) _).
(* iDestruct "Hxs" as (xs) "(Hs & Hgn)". *) iApply install_push_spec=>//.
(* (* mask magic *) *) iFrame "#".
(* iApply pvs_intro'. *) iAssert (own γm ( {[p := ((1/2)%Qp, DecAgree (γx, γ1, γ3, γ4))]}
(* { apply ndisj_subseteq_difference; auto. } *) {[p := ((1/2)%Qp, DecAgree (γx, γ1, γ3, γ4))]})) as "[Hfrag1 Hfrag2]".
(* iIntros "Hvs". *) { admit. }
(* iExists (map (λ x : loc, #x) xs). *) iFrame "Hx1 Hfrag1 Hl Ho1 Ho4". iIntros "_". wp_seq. iVsIntro.
(* iFrame "Hs". iSplit. *) iSpecialize ("HΦ" $! p γx γ1 γ2 γ3 γ4 with "[-Hx2 Hfrag2]")=>//.
(* + (* provide a way to rollback *) *) iApply ("HΦ" with "Hfrag2 Hx2").
(* iIntros "Hl'". *) Admitted.
(* iVs "Hvs". iVs ("Hclose" with "[-Hp Hx Ho1 Ho4]"); last by iFrame. *)
(* iNext. rewrite /srv_inv. iExists hds, gnm. *)
(* iFrame. iExists xs. by iFrame. *)
(* + (* provide a way to commit *) *)
(* iIntros (?) "[% Hs]". subst. *)
(* iVs "Hvs". iVs ("Hclose" with "[-]"); last done. *)
(* iNext. rewrite /srv_inv. iExists hds, (gnm {[ p := DecAgree (γx, γ1, γ2, γ3, γ4) ]}). *)
(* iFrame. *)
(* iClear "Hogn". *)
(* iAssert (own γgn ( (gnm {[p := DecAgree (γx, γ1, γ2, γ3, γ4)]})) *)
(* own γgn ( {[ p := DecAgree (γx, γ1, γ2, γ3, γ4) ]}))%I as "[Hogn' Hfrag]". *)
(* { admit. } *)
(* iFrame. iSplitL "Hs Hgn". *)
(* { iExists (p::xs). *)
(* iFrame. admit. } *)
(* iSplitL "Hhd". *)
(* { admit. } *)
(* iAssert (p_inv' (DecAgree (γx, γ1, γ2, γ3, γ4)) p Q) with "[Hp Hx Ho1 Ho4]" as "Hinvp". *)
(* { rewrite /p_inv' /p_inv. iRight. iLeft. iExists x. by iFrame. } *)
(* admit. *)
(* - iApply wp_wand_r. iSplitR "HΦ". *)
(* + iApply "Hpush". by iFrame. *)
(* + iIntros (?) "H". iDestruct "H" as (?) "%". subst. by iApply "HΦ". *)
(* Admitted. *)
(* Lemma install_spec *)
(* (Φ: val iProp Σ) (Q: val val Prop) *)
(* (x: val) (γhd γgn: gname) (s: loc): *)
(* heapN N *)
(* heap_ctx inv N (srv_inv γhd γgn s Q) *)
(* ( (p: loc) (γx γ1 γ2 γ3 γ4: gname), *)
(* own γ2 (Excl ()) - own γ3 (Excl ()) - own γgn ( {[ p := DecAgree (γx, γ1, γ2, γ3, γ4) ]}) - *)
(* own γx ((1/2)%Qp, DecAgree x) - Φ #p) *)
(* WP install x #s {{ Φ }}. *)
(* Proof. *)
(* iIntros (HN) "(#Hh & #Hsrv & HΦ)". *)
(* wp_seq. wp_let. wp_alloc p as "Hl". *)
(* iVs (own_alloc (Excl ())) as (γ1) "Ho1"; first done. *)
(* iVs (own_alloc (Excl ())) as (γ2) "Ho2"; first done. *)
(* iVs (own_alloc (Excl ())) as (γ3) "Ho3"; first done. *)
(* iVs (own_alloc (Excl ())) as (γ4) "Ho4"; first done. *)
(* iVs (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done. *)
(* iDestruct (own_update with "Hx") as "==>[Hx1 Hx2]". *)
(* { by apply pair_l_frac_op_1'. } *)
(* wp_let. wp_bind ((push _) _). *)
(* iApply push_spec=>//. *)
(* iFrame "Hh Hsrv Hx1 Hl Ho1 Ho4". *)
(* iIntros "_". wp_seq. iVsIntro. *)
(* iSpecialize ("HΦ" $! p γx γ1 γ2 γ3 γ4). *)
(* iAssert (own γgn ( {[p := DecAgree (γx, γ1, γ2, γ3, γ4)]})) as "Hfrag". *)
(* { admit. } *)
(* iApply ("HΦ" with "Ho2 Ho3 Hfrag Hx2"). *)
(* Admitted. *)
(* Definition pinv_sub RI γx γ1 γ2 γ3 γ4 p Q := (RI ⊣⊢ Rf, Rf p_inv γx γ1 γ2 γ3 γ4 p Q)%I. *)
(* Lemma doOp_spec Φ (f: val) (RI: iProp Σ) γx γ1 γ2 γ3 γ4 p Q `{TimelessP _ RI}: *)
(* heapN N pinv_sub RI γx γ1 γ2 γ3 γ4 p Q *)
(* heap_ctx inv N RI own γ2 (Excl ()) *)
(* ( x:val, WP f x {{ v, Q x v }})%I (own γ2 (Excl ()) - Φ #()) *)
(* WP doOp f #p {{ Φ }}. *)
(* Proof. *)
(* iIntros (HN Hsub) "(#Hh & #HRI & Ho2 & #Hf & HΦ)". *)
(* wp_seq. wp_let. wp_bind (! _)%E. *)
(* iInv N as ">H" "Hclose". *)
(* iDestruct (Hsub with "H") as (Rf) "[HRf [Hp | [Hp | [Hp | Hp]]]]". *)
(* - iDestruct "Hp" as (y) "(Hp & Ho1 & Ho3)". *)
(* wp_load. iVs ("Hclose" with "[HRf Hp Ho1 Ho3]"). *)
(* { iNext. iApply Hsub. iExists Rf. iFrame "HRf". *)
(* iLeft. iExists y. by iFrame. } *)
(* iVsIntro. wp_match. by iApply "HΦ". *)
(* - iDestruct "Hp" as (x) "(Hp & Hx & Ho1 & Ho4)". *)
(* wp_load. *)
(* iAssert (|=r=> own γx (((1 / 4)%Qp, DecAgree x) ((1 / 4)%Qp, DecAgree x)))%I with "[Hx]" as "==>[Hx1 Hx2]". *)
(* { iDestruct (own_update with "Hx") as "Hx"; last by iAssumption. *)
(* replace ((1 / 2)%Qp) with (1/4 + 1/4)%Qp; last by apply Qp_div_S. *)
(* by apply pair_l_frac_op'. } *)
(* iVs ("Hclose" with "[HRf Hp Hx1 Ho2 Ho4]"). *)
(* { iNext. iApply Hsub. iExists Rf. iFrame "HRf". *)
(* iRight. iRight. iLeft. iExists x. by iFrame. } *)
(* iVsIntro. wp_match. *)
(* wp_bind (f _). iApply wp_wand_r. *)
(* iSplitR; first by iApply "Hf". *)
(* iIntros (y) "%". *)
(* iInv N as ">H" "Hclose". *)
(* iDestruct (Hsub with "H") as (Rf') "[HRf [Hp | [Hp | [Hp | Hp]]]]". *)
(* + admit. *)
(* + admit. *)
(* + iDestruct "Hp" as (x') "(Hp & Hx & Ho2 & Ho4)". *)
(* destruct (decide (x = x')) as [->|Hneq]; last by admit. *)
(* iCombine "Hx2" "Hx" as "Hx". *)
(* iDestruct (own_update with "Hx") as "==>Hx"; first by apply pair_l_frac_op. *)
(* rewrite Qp_div_S. *)
(* wp_store. iVs ("Hclose" with "[HRf Hp Hx Ho1 Ho4]"). *)
(* { iNext. iApply Hsub. iExists Rf'. iFrame "HRf". *)
(* iRight. iRight. iRight. iExists x', y. *)
(* by iFrame. } *)
(* iVsIntro. by iApply "HΦ". *)
(* + admit. *)
(* - admit. *)
(* - admit. *)
(* Admitted. *)
Lemma loop_iter_list_spec Φ (f: val) (s hd: loc) Q (γhd γgn γ2: gname) xs: Lemma loop_iter_list_spec Φ (f: val) (s hd: loc) Q (γ γm γ2: gname) xs:
heapN N heapN N
heap_ctx inv N (srv_inv γhd γgn γ2 s Q) ( x:val, WP f x {{ v, Q x v }})%I own γ2 (Excl ()) heap_ctx inv N (srv_stack_inv γ γm γ2 s Q) ( x:val, WP f x {{ v, Q x v }})%I own γ2 (Excl ())
is_list hd xs own γhd ( ({[ hd ]} : hdsetR)) (own γ2 (Excl ()) - Φ #()) is_list' γ hd xs (own γ2 (Excl ()) - Φ #())
WP doOp f {{ f', WP iter' #hd f' {{ Φ }} }}. WP iter' #hd (doOp f) {{ Φ }}.
Proof. Proof.
iIntros (HN) "(#Hh & #? & #Hf & Hxs & Hhd & Ho2 & HΦ)". iIntros (HN) "(#Hh & #? & #Hf & Ho2 & Hlist' & HΦ)".
rewrite /doOp. wp_let. rewrite /doOp.
iLöb as "IH". iApply pvs_wp.
wp_rec. wp_let. wp_bind (! _)%E. iDestruct (dup_is_list' with "[Hlist']") as "==>[Hl1 Hl2]"; first by iFrame.
destruct xs as [|x xs']. iDestruct (dup_is_list' with "[Hl2]") as "==>[Hl2 Hl3]"; first by iFrame.
- simpl. iDestruct "Hhd" as (q) "Hhd". iDestruct (iter'_spec _ (p_inv_R γm γ2 Q) _ γ s (is_list' γ hd xs own γ2 (Excl ()))%I xs hd (λ: "p",
wp_load. wp_match. by iApply "HΦ". match: ! "p" with InjL "x" => "p" <- SOME (f "x") | InjR "_" => #() end)%V (λ: "p",
- simpl. iDestruct "Hhd" as (hd' q) "[[Hhd1 Hhd2] Hhd']". match: ! "p" with InjL "x" => "p" <- SOME (f "x") | InjR "_" => #() end) with "[-Hl1]") as "Hiter'"=>//.
wp_load. wp_match. wp_proj. wp_let. - rewrite /f_spec.
wp_bind (! _)%E. iIntros (Φ' x _ Hin) "(#Hh & #? & (Hls & Ho2) & HΦ')".
iInv N as (hds gnm) ">(Hohd & Hogn & Hxse & Hhds & Hps)" "Hclose". wp_let. wp_bind (! _)%E. iInv N as (xs') ">Hs" "Hclose".
iAssert ( (p: loc) γs, x = #p p_inv' γ2 γs p Q)%I as "Hx". iDestruct "Hs" as (hd') "[Hhd [Hxs HRs]]".
{ admit. } (* now I know x conforms to p_inv_R *)
iDestruct "Hx" as (p γs) "[% Hp]". subst. admit.
rewrite /p_inv'. destruct γs as [[[[γx γ1] γ3] γ4]|]. - apply to_of_val.
iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]"=>//. - iFrame "#". iFrame "Hl2 Hl3 Ho2".
+ admit. iIntros "[_ H]". by iApply "HΦ".
+ iDestruct "Hp" as (x) "(Hp & Hx & Ho1 & Ho4)". - done.
iAssert (|=r=> own γx (((1 / 4)%Qp, DecAgree x) ((1 / 4)%Qp, DecAgree x)))%I with "[Hx]" as "==>[Hx1 Hx2]".
{ iDestruct (own_update with "Hx") as "Hx"; last by iAssumption.
replace ((1 / 2)%Qp) with (1/4 + 1/4)%Qp; last by apply Qp_div_S.
by apply pair_l_frac_op'. }
wp_load. iVs ("Hclose" with "[-Ho1 Hx2 Hhd2 HΦ]").
{ iNext. iExists hds, gnm. by iFrame. }
iVsIntro. wp_match.
wp_bind (f _). iApply wp_wand_r. iSplitR; first by iApply "Hf".
iIntros (y) "Q".
iInv N as (hds' gnm') ">(Hohd & Hogn & Hxse & Hhds & Hps)" "Hclose".
iAssert (p_inv' γ2 (DecAgree (γx, γ1, γ3, γ4)) p Q)%I as "Hp".
{ admit. }
rewrite /p_inv'.
iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]".
* admit.
* admit.
* iDestruct "Hp" as (x') "(Hp & Hx' & Ho2 & Ho4)".
destruct (decide (x = x')) as [->|Hneq]; last by admit.
iCombine "Hx2" "Hx'" as "Hx".
iDestruct (own_update with "Hx") as "==>Hx"; first by apply pair_l_frac_op.
rewrite Qp_div_S.
wp_store. iVs ("Hclose" with "[-Ho2 HΦ Hhd2]").
{ iNext. iExists hds', gnm'. by iFrame. }
iVsIntro. wp_seq. wp_proj. rewrite /doOp.
iAssert (is_list hd' xs') as "Hl".
{ admit. }
iAssert ( (hd'0 : loc) (q0 : Qp),
hd {q0} SOMEV (#p, #hd'0) is_list hd'0 xs')%I with "[Hhd2 Hl]" as "He".
{ iExists hd', (q / 2)%Qp. by iFrame. }
iAssert (own γhd ( {[hd]})) as "Hfrag".
{ admit. }
iSpecialize ("IH" with "Ho2 He Hfrag HΦ").
admit.
* admit.
+ admit.
+ admit.
+ by iExFalso.
Admitted. Admitted.
Lemma loop_iter_spec Φ (f: val) (s: loc) Q (γhd γgn γ2: gname): Lemma loop_iter_spec Φ (f: val) (s: loc) Q (γhd γgn γ2: gname):
......
Supports Markdown
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