Commit 8f5c5363 authored by Dan Frumin's avatar Dan Frumin

[flock2] flock_res is fractional

parent c4d5aec7
......@@ -69,10 +69,10 @@ Section a_wp.
Definition awp (e : expr)
(R : iProp Σ) (Φ : val iProp Σ) : iProp Σ :=
tc_opaque (WP e {{ ev, (γ : flock_name) (π : frac) (env : val) (l : val),
tc_opaque (WP e {{ ev, (γ : flock_name) (π : frac) (i : prop_id) (env : val) (l : val),
is_flock amonadN γ l -
flock_res γ (env_inv env R) π -
WP ev env l {{ v, Φ v flock_res γ (env_inv env R) π }}
flock_res γ i (env_inv env R) π -
WP ev env l {{ v, Φ v flock_res γ i (env_inv env R) π }}
}})%I.
Global Instance elim_bupd_awp p e Φ :
......@@ -113,7 +113,7 @@ Section a_wp_rules.
iIntros "HR1 Hawp". rewrite /awp /=.
iApply (wp_wand with "Hawp").
iIntros (v) "HΦ".
iIntros (γ π env l) "#Hflock Hres".
iIntros (γ π i env l) "#Hflock Hres".
(* iMod (flock_res_insert_unflocked with "Hflock Hres Hunfl HR1") *)
(* as "(#Hres & Hunfl)"; first done. *)
(* iApply ("HΦ" with "Hflock [Hres] Hunfl"). *)
......@@ -131,7 +131,7 @@ Section a_wp_rules.
iIntros "HAWP Hv". rewrite /awp /=.
iApply (wp_wand with "HAWP").
iIntros (v) "HΦ".
iIntros (γ π env l) "#Hflock Hres".
iIntros (γ π i env l) "#Hflock Hres".
iApply (wp_wand with "[HΦ Hres]"); first by iApply "HΦ".
iIntros (w) "[HΦ $]". by iApply "Hv".
Qed.
......@@ -151,7 +151,7 @@ Section a_wp_rules.
Proof.
iIntros "Hwp". rewrite /awp /a_ret /=. wp_apply (wp_wand with "Hwp").
iIntros (v) "HΦ". wp_lam.
iIntros (γ π env l) "#Hlock Hres". do 2 wp_lam. iFrame.
iIntros (γ π i env l) "#Hlock Hres". do 2 wp_lam. iFrame.
Qed.
Lemma awp_bind (f e : expr) R Φ :
......@@ -161,7 +161,7 @@ Section a_wp_rules.
Proof.
iIntros ([fv <-%of_to_val]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e.
iApply (wp_wand with "Hwp"). iIntros (ev) "Hwp". wp_lam.
iIntros (γ π env l) "#Hlock Hres". do 2 wp_lam. wp_bind (ev env l).
iIntros (γ π i env l) "#Hlock Hres". do 2 wp_lam. wp_bind (ev env l).
iApply (wp_wand with "[Hwp Hres]"); first by iApply "Hwp".
iIntros (w) "[Hwp Hres]". wp_let. wp_apply (wp_wand with "Hwp").
iIntros (v) "H". by iApply ("H" with "[$]").
......@@ -173,7 +173,7 @@ Section a_wp_rules.
awp (a_atomic e) R Φ.
Proof.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic /=. wp_lam.
iIntros (γ π env l) "#Hlock1 Hres". do 2 wp_let.
iIntros (γ π i env l) "#Hlock1 Hres". do 2 wp_let.
wp_apply (acquire_cancel_spec with "[$]").
iDestruct 1 as (R') "(HR' & #Heq & Hcl)". wp_seq.
iAssert ( (env_inv env R))%I with "[HR']" as "[Henv HR]".
......@@ -182,7 +182,7 @@ Section a_wp_rules.
wp_apply (newlock_cancel_spec amonadN); first done.
iIntros (k γ') "#Hlock2".
iMod (flock_res_single_alloc _ _ _ (env_inv env Q)%I
with "Hlock2 [$Henv $HQ]") as "Hres"; first done.
with "Hlock2 [$Henv $HQ]") as (i') "Hres"; first done.
wp_let.
wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
iApply (wp_wand with "[Hwp Hres]"); first by iApply "Hwp".
......@@ -206,7 +206,7 @@ Section a_wp_rules.
awp (a_atomic_env e) R Φ.
Proof.
iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam.
iIntros (γ π env l) "#Hlock Hres". do 2 wp_lam.
iIntros (γ π i env l) "#Hlock Hres". do 2 wp_lam.
wp_apply (acquire_cancel_spec with "[$]").
iDestruct 1 as (R') "(HR' & #Heq & Hcl)". wp_seq.
iAssert ( (env_inv env R))%I with "[HR']" as "[Henv HR]".
......@@ -231,9 +231,9 @@ Section a_wp_rules.
iIntros (ev1) "Hwp1". wp_lam.
wp_bind e2. iApply (wp_wand with "Hwp2").
iIntros (ev2) "Hwp2". wp_lam.
iIntros (γ π env l) "#Hlock [Hres1 Hres2]". do 2 wp_lam.
iApply (par_spec (λ v, Ψ1 v flock_res _ _ (π/2))%I
(λ v, Ψ2 v flock_res _ _ (π/2))%I
iIntros (γ π i env l) "#Hlock [Hres1 Hres2]". do 2 wp_lam.
iApply (par_spec (λ v, Ψ1 v flock_res _ _ _ (π/2))%I
(λ v, Ψ2 v flock_res _ _ _ (π/2))%I
with "[Hwp1 Hres1] [Hwp2 Hres2]").
- wp_lam. iApply ("Hwp1" with "Hlock Hres1").
- wp_lam. iApply ("Hwp2" with "Hlock Hres2").
......@@ -258,7 +258,7 @@ Section a_wp_run.
wp_apply (newlock_cancel_spec amonadN); first done.
iIntros (k γ') "#Hlock". rewrite- wp_fupd.
iMod (flock_res_single_alloc _ _ _ (env_inv env R)%I
with "Hlock [Henv Hσ $HR]") as "Hres"; first done.
with "Hlock [Henv Hσ $HR]") as (i) "Hres"; first done.
{ iNext. iExists , . iFrame. eauto. }
iSpecialize ("Hwp" $! amg).
iMod (wp_value_inv with "Hwp") as "Hwp".
......
......@@ -46,23 +46,6 @@ Proof. solve_inG. Qed.
Section flock.
Context `{heapG Σ, flockG Σ}.
(* because flock_res_op is admitted, it has to go before the Variable N part *)
Definition flock_res (γ : flock_name) (R : iProp Σ) (π : Qp) : iProp Σ :=
( s ρ, saved_prop_own ρ.1 R own ρ.2 π
own (flock_props_name γ) ( {[s := (π, to_agree ρ)]}))%I.
Lemma flock_res_op (γ : flock_name) (R : iProp Σ) (π1 π2 : frac) :
flock_res γ R (π1+π2) flock_res γ R π1 flock_res γ R π2.
Proof. rewrite /flock_res. admit. Admitted.
Global Instance flock_res_fractional γ R : Fractional (flock_res γ R).
Proof. intros p q. apply flock_res_op. Qed.
Global Instance flock_res_as_fractional γ R π :
AsFractional (flock_res γ R π) (flock_res γ R) π.
Proof. split. done. apply _. Qed.
Variable N : namespace.
Definition flockN := N.@"flock".
......@@ -119,11 +102,43 @@ Section flock.
own (flock_props_active_name γ) ( Excl' f)
all_props (from_active f))%I.
Definition flock_res (γ : flock_name) (s : prop_id) (R : iProp Σ) (π : Qp) : iProp Σ :=
( ρ, saved_prop_own ρ.1 R own ρ.2 π
own (flock_props_name γ) ( {[s := (π, to_agree ρ)]}))%I.
Lemma flock_res_op (γ : flock_name) (s : prop_id) (R : iProp Σ) (π1 π2 : frac) :
flock_res γ s R (π1+π2) flock_res γ s R π1 flock_res γ s R π2.
Proof.
rewrite /flock_res. iSplit.
- iDestruct 1 as (ρ) "(#Hsaved & Hρ & Hs)".
iDestruct "Hρ" as "[Hρ1 Hρ2]".
iDestruct "Hs" as "[Hs1 Hs2]".
iSplitL "Hρ1 Hs1"; iExists _; by iFrame.
- iIntros "[H1 H2]".
iDestruct "H1" as (ρ) "(#Hsaved & Hρ1 & Hs1)".
iDestruct "H2" as (ρ') "(_ & Hρ2 & Hs2)".
iCombine "Hs1 Hs2" as "Hs".
iDestruct (own_valid with "Hs")
as %Hfoo%auth_valid_discrete.
simpl in Hfoo. apply singleton_valid in Hfoo.
destruct Hfoo as [_ Hfoo%agree_op_inv'].
fold_leibniz. rewrite -!Hfoo.
iCombine "Hρ1 Hρ2" as "Hρ".
rewrite !frac_op' agree_idemp.
iExists ρ. by iFrame.
Qed.
Global Instance flock_res_fractional γ s R : Fractional (flock_res γ s R).
Proof. intros p q. apply flock_res_op. Qed.
Global Instance flock_res_as_fractional γ s R π :
AsFractional (flock_res γ s R π) (flock_res γ s R) π.
Proof. split. done. apply _. Qed.
Lemma flock_res_single_alloc γ lk R E :
flockN E
is_flock γ lk - R
={E}= flock_res γ R 1.
={E}= s, flock_res γ s R 1.
Proof.
iIntros (?) "Hl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
iMod (saved_prop_alloc R) as (ρ1) "#Hρ1".
......@@ -151,15 +166,15 @@ Section flock.
iPureIntro. admit. (* TODO: map disjoint *)
Admitted.
Lemma flock_res_single_dealloc γ lk R E :
Lemma flock_res_single_dealloc γ lk i R E :
flockN E
is_flock γ lk - flock_res γ R 1
is_flock γ lk - flock_res γ i R 1
={E}= R', R' (R R').
Proof.
iIntros (?) "Hl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
iInv (flockN.@"inv") as ([|] fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl".
- iDestruct "Hrest" as ">[Hlocked Htokens]".
iDestruct "HR" as (i [ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
iDestruct "HR" as ([ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
iDestruct (own_valid_2 with "Hauth HR")
as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
iAssert (fa !! i = None)%I with "[-]" as %Hbar.
......@@ -204,7 +219,7 @@ Section flock.
as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
iPureIntro. by unfold_leibniz. }
rewrite from_active_empty right_id.
iDestruct "HR" as (i [ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
iDestruct "HR" as ([ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
iDestruct (own_valid_2 with "Hauth HR")
as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hauth HR") as "Hauth".
......@@ -243,10 +258,10 @@ Section flock.
rewrite /is_flock. by iFrame "Hlock".
Qed.
Lemma acquire_cancel_spec γ π lk R :
{{{ is_flock γ lk flock_res γ R π }}}
Lemma acquire_cancel_spec γ π lk i R :
{{{ is_flock γ lk flock_res γ i R π }}}
acquire lk
{{{ RET #(); R', R' (R R') ( R' ={}= flocked γ flock_res γ R π) }}}.
{{{ RET #(); R', R' (R R') ( R' ={}= flocked γ flock_res γ i R π) }}}.
Proof.
iIntros (Φ) "(Hl & HRres) HΦ".
rewrite /is_flock. iDestruct "Hl" as "(#Hinv & #Hlk)".
......@@ -261,7 +276,7 @@ Section flock.
as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
iPureIntro. by unfold_leibniz. }
rewrite from_active_empty right_id.
iDestruct "HRres" as (i [ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
iDestruct "HRres" as ([ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
(* Unlocked ~~> Locked *)
iMod (own_update_2 with "Hstate Hunlk") as "Hstate".
......@@ -346,7 +361,7 @@ Section flock.
iModIntro. iFrame. rewrite /all_props from_active_empty big_sepM_empty.
iSplitR; first done.
rewrite /all_tokens big_sepM_singleton. simpl.
iExists i, (ρ1, ρ2). by iFrame.
iExists (ρ1, ρ2). by iFrame.
Admitted.
Lemma release_cancel_spec γ lk :
......
......@@ -120,20 +120,20 @@ Section test.
iIntros "$". iSplit; eauto.
Qed.
Lemma invoke_test (l : loc) (z0 z1 z2: Z) R :
l U #z0 -
awp (a_bin_op PlusOp
(a_invoke assignF (a_par (a_ret #l) (a_ret #z1)))
(a_invoke assignF (a_par (a_ret #l) (a_ret #z2)))) R
(λ v, v = #(z1 + z2))%I.
Proof.
iIntros "Hl".
iApply (awp_insert_res _ _ (l U -)%I with "[Hl]").
{ iNext. by iExists #z0. }
iApply a_bin_op_spec.
- iApply invoke_assignF_2.
- iApply invoke_assignF_2.
- iIntros (? ? -> ->). iExists #(z1+z2). eauto.
Qed.
(* Lemma invoke_test (l : loc) (z0 z1 z2: Z) R : *)
(* l ↦U #z0 -∗ *)
(* awp (a_bin_op PlusOp *)
(* (a_invoke assignF (a_par (a_ret #l) (a_ret #z1))) *)
(* (a_invoke assignF (a_par (a_ret #l) (a_ret #z2)))) R *)
(* (λ v, ⌜v = #(z1 + z2)⌝)%I. *)
(* Proof. *)
(* iIntros "Hl". *)
(* iApply (awp_insert_res _ _ (l ↦U -)%I with "[Hl]"). *)
(* { iNext. by iExists #z0. } *)
(* iApply a_bin_op_spec. *)
(* - iApply invoke_assignF_2. *)
(* - iApply invoke_assignF_2. *)
(* - iIntros (? ? -> ->). iExists #(z1+z2). eauto. *)
(* Qed. *)
End test.
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