From 92e9852f0c2dcb34ae6b8561ea6aeace6fee6c19 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Fri, 15 Jun 2018 14:03:40 +0200 Subject: [PATCH] WIP: multi-flock-res acquire --- theories/c_translation/monad.v | 145 ++++++++++------- theories/lib/flock.v | 290 +++++++++++++++++++++++++++++---- 2 files changed, 345 insertions(+), 90 deletions(-) diff --git a/theories/c_translation/monad.v b/theories/c_translation/monad.v index 9cff966..95ef879 100644 --- a/theories/c_translation/monad.v +++ b/theories/c_translation/monad.v @@ -67,12 +67,16 @@ Section a_wp. ∗ ([∗ map] l ↦ _ ∈ σ, ∃ v', l ↦{1/2} v') ∗ ⌜correct_locks X (locked_locs σ)⌝)%I. + Definition flock_resources (γ : flock_name) (I : gmap prop_id (iProp Σ * frac)) := + ([∗ map] i ↦ p ∈ I, flock_res γ i p.1 p.2)%I. + Definition awp (e : expr) (R : iProp Σ) (Φ : val → iProp Σ) : iProp Σ := - tc_opaque (WP e {{ ev, ∀ (γ : flock_name) (π : frac) (i : prop_id) (env : val) (l : val), + tc_opaque (WP e {{ ev, ∀ (γ : flock_name) (env : val) (l : val) (I : gmap prop_id (iProp Σ * frac)), is_flock amonadN γ l -∗ - flock_res γ i (env_inv env ∗ R) π -∗ - WP ev env l {{ v, Φ v ∗ flock_res γ i (env_inv env ∗ R) π }} + flock_resources γ I -∗ + (([∗ map] p ∈ I, p.1) ≡ (env_inv env ∗ R)) -∗ + WP ev env l {{ v, Φ v ∗ flock_resources γ I }} }})%I. Global Instance elim_bupd_awp p e Φ : @@ -107,21 +111,30 @@ Section a_wp_rules. Lemma awp_insert_res e Φ R1 R2 : ▷ R1 -∗ - awp e (R1 ∗ R2) (λ v, R1 -∗ Φ v) -∗ + awp e (R1 ∗ R2) (λ v, ▷ ▷ R1 -∗ Φ v) -∗ awp e R2 Φ. Proof. iIntros "HR1 Hawp". rewrite /awp /=. iApply (wp_wand with "Hawp"). iIntros (v) "HΦ". - 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"). *) - (* rewrite (comm (∗)%I R1 R2). *) - (* rewrite (assoc (∗)%I _ R2 R1). *) - (* by iFrame "Hres". *) - (* Qed. *) - Abort. + iIntros (γ env l I) "#Hflock Hres #Heq". + iMod (flock_res_single_alloc _ (dom (gset prop_id) I) with "Hflock HR1") as (j) "[% Hres']"; first done. + pose (I' := <[j:= (R1,1%Qp)]>I). + assert (I !! j = None) by by eapply not_elem_of_dom. + iSpecialize ("HΦ" $! _ env l I' with "Hflock [Hres Hres'] []"). + { rewrite /flock_resources /I'. + rewrite big_sepM_insert; last done. iFrame. } + { rewrite big_sepM_insert; last done. simpl. iRewrite "Heq". + rewrite (assoc _ R1 _ R2). + rewrite (comm _ R1 (env_inv env)). + rewrite -(assoc _ _ R1 R2). done. } + iApply wp_fupd. + iApply (wp_wand with "HΦ"). + iIntros (w) "[HΦ HI]". rewrite /flock_resources /I'. + rewrite big_sepM_insert /=; last done. iDestruct "HI" as "[HR1 $]". + iMod (flock_res_single_dealloc with "Hflock HR1") as (R') "[HR' Heq']"; first done. + iApply "HΦ". iModIntro. do 2 iNext. by iRewrite "Heq'". + Qed. Lemma awp_wand e (Φ Ψ : val → iProp Σ) R : awp e R Φ -∗ @@ -131,8 +144,8 @@ Section a_wp_rules. iIntros "HAWP Hv". rewrite /awp /=. iApply (wp_wand with "HAWP"). iIntros (v) "HΦ". - iIntros (γ π i env l) "#Hflock Hres". - iApply (wp_wand with "[HΦ Hres]"); first by iApply "HΦ". + iIntros (γ env l I) "#Hflock Hres #Heq". + iApply (wp_wand with "[HΦ Hres]"). iApply ("HΦ" with "Hflock Hres Heq"). iIntros (w) "[HΦ $]". by iApply "Hv". Qed. @@ -151,7 +164,7 @@ Section a_wp_rules. Proof. iIntros "Hwp". rewrite /awp /a_ret /=. wp_apply (wp_wand with "Hwp"). iIntros (v) "HΦ". wp_lam. - iIntros (γ π i env l) "#Hlock Hres". do 2 wp_lam. iFrame. + iIntros (γ env l I) "#Hlock Hres #Heq". do 2 wp_lam. iFrame. Qed. Lemma awp_bind (f e : expr) R Φ : @@ -161,10 +174,10 @@ 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 (γ π 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 (γ env l I) "#Hflock Hres #Heq". do 2 wp_lam. wp_bind (ev env l). + iApply (wp_wand with "[Hwp Hres]"). iApply ("Hwp" with "Hflock Hres Heq"). iIntros (w) "[Hwp Hres]". wp_let. wp_apply (wp_wand with "Hwp"). - iIntros (v) "H". by iApply ("H" with "[$]"). + iIntros (v) "H". iApply ("H" with "Hflock Hres Heq"). Qed. Lemma awp_atomic (e : expr) (ev : val) R Φ : @@ -173,48 +186,50 @@ Section a_wp_rules. awp (a_atomic e) R Φ. Proof. iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic /=. wp_lam. - iIntros (γ π i env l) "#Hlock1 Hres". do 2 wp_let. + iIntros (γ env l I) "#Hlock1 Hres #Heq1". 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]". - { iNext. iRewrite "Heq". done. } + iIntros "[HI Hcl]". iRewrite "Heq1" in "HI". + iDestruct "HI" as "[Henv HR]". iDestruct ("Hwp" with "HR") as (Q) "[HQ Hwp]". + wp_seq. 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 (i') "Hres"; first done. + iMod (flock_res_single_alloc _ (dom (gset prop_id) I) _ _ (env_inv env ∗ Q)%I + 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". - iIntros (w) "[HR Hres]". - iMod (flock_res_single_dealloc with "Hlock2 Hres") as (Q') "[HQ' #HeqQ]"; first done. - wp_let. - iAssert (▷ (env_inv env ∗ Q))%I with "[HQ']" as "[Henv HQ]". - { iNext. by iRewrite "HeqQ". } - iDestruct ("HR" with "HQ") as "[HR HΦ]". - iAssert (▷ R')%I with "[HR Henv]" as "HR'". - { iNext. iRewrite -"Heq". iFrame. } - iMod ("Hcl" with "HR'") as "[Hflocked Hres]". - wp_apply (release_cancel_spec with "[$Hlock1 $Hflocked]"). - iIntros "_". wp_seq. iFrame. + iApply (wp_wand with "[Hwp Hres]"). + - iApply ("Hwp" $! _ _ _ {[i' := ((env_inv env ∗ Q)%I,1%Qp)]} with "Hlock2 [Hres] []"). + + rewrite /flock_resources big_sepM_singleton //. + + rewrite big_sepM_singleton //. + - iIntros (w) "[HR Hres]". + rewrite /flock_resources big_sepM_singleton /=. + iMod (flock_res_single_dealloc with "Hlock2 Hres") as (Q') "[HQ' #Heq2]"; first done. + wp_let. + iAssert (▷ (env_inv env ∗ Q))%I with "[HQ']" as "[Henv HQ]". + { iNext. by iRewrite "Heq2". } + iDestruct ("HR" with "HQ") as "[HR HΦ]". + iMod ("Hcl" with "[HR Henv]") as "[Hflocked Hres]". + { iNext. iRewrite "Heq1". iFrame. } + wp_apply (release_cancel_spec with "[$Hlock1 $Hflocked]"). + iIntros "_". wp_seq. iFrame. Qed. Lemma awp_atomic_env (e : expr) (ev : val) R Φ : IntoVal e ev → - (∀ env, ▷ env_inv env -∗ ▷ R -∗ - WP ev env {{ w, env_inv env ∗ R ∗ Φ w }}) -∗ + (∀ env, env_inv env -∗ R -∗ + WP ev env {{ w, ▷ env_inv env ∗ ▷ R ∗ ▷ Φ w }}) -∗ awp (a_atomic_env e) R Φ. Proof. iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam. - iIntros (γ π i env l) "#Hlock Hres". do 2 wp_lam. + iIntros (γ env l I) "#Hlock Hres #Heq". 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]". - { iNext. iRewrite "Heq". done. } + iIntros "[HI Hcl]". iRewrite "Heq" in "HI". + iDestruct "HI" as "[Henv HR]". iDestruct ("Hwp" with "Henv HR") as "Hwp". - wp_apply (wp_wand with "Hwp"). + wp_seq. wp_apply (wp_wand with "Hwp"). iIntros (w) "[Henv [HR HΦ]]". wp_let. - iRewrite -"Heq" in "Hcl". + iRewrite "Heq" in "Hcl". iMod ("Hcl" with "[$HR $Henv]") as "[Hflocked Hres]". wp_apply (release_cancel_spec with "[$Hlock $Hflocked]"). iIntros "_". wp_seq. iFrame. @@ -231,13 +246,27 @@ Section a_wp_rules. iIntros (ev1) "Hwp1". wp_lam. wp_bind e2. iApply (wp_wand with "Hwp2"). iIntros (ev2) "Hwp2". wp_lam. - 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 + iIntros (γ env l I) "#Hlock Hres #Heq". do 2 wp_lam. + pose (I' := fmap (λ x, (x.1, (x.2/2)%Qp)) I). + iAssert (flock_resources γ I' ∗ flock_resources γ I')%I with "[Hres]" as "[Hres1 Hres2]". + { rewrite /flock_resources -big_sepM_sepM. + rewrite /I' big_sepM_fmap /=. + iApply (big_sepM_mono with "Hres"). iIntros (k x Hk). simpl. + by rewrite -flock_res_op Qp_div_2. } + iApply (par_spec (λ v, Ψ1 v ∗ flock_resources γ I')%I + (λ v, Ψ2 v ∗ flock_resources γ I')%I with "[Hwp1 Hres1] [Hwp2 Hres2]"). - wp_lam. iApply ("Hwp1" with "Hlock Hres1"). + by rewrite /I' big_sepM_fmap /=. - wp_lam. iApply ("Hwp2" with "Hlock Hres2"). - - iNext. iIntros (w1 w2) "[[HΨ1 $] [HΨ2 $]]". + by rewrite /I' big_sepM_fmap /=. + - iNext. iIntros (w1 w2) "[[HΨ1 Hres1] [HΨ2 Hres2]]". + iAssert (flock_resources γ I)%I with "[Hres1 Hres2]" as "$". + { iCombine "Hres1 Hres2" as "Hres". + rewrite /flock_resources -big_sepM_sepM. + rewrite /I' big_sepM_fmap /=. + iApply (big_sepM_mono with "Hres"). iIntros (k x Hk). simpl. + by rewrite -flock_res_op Qp_div_2. } iApply ("HΦ" with "[$] [$]"). Qed. End a_wp_rules. @@ -257,17 +286,21 @@ Section a_wp_run. pose (amg := AMonadG Σ _ _ _ _). 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 (i) "Hres"; first done. + iMod (flock_res_single_alloc _ ∅ _ _ (env_inv env ∗ R)%I + 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". wp_let. wp_bind (ev env k). - iApply (wp_wand with "[Hwp Hres]"); first by iApply "Hwp". - iIntros (w) "[HΦ Hres]". - iMod (flock_res_single_dealloc with "Hlock Hres") as (R') "[HR' #Heq]"; first done. - wp_let. - iApply "HΦ". iNext. iRewrite -"Heq" in "HR'". iDestruct "HR'" as "[_ $]". + iApply (wp_wand with "[Hwp Hres]"). + - iApply ("Hwp" $! _ _ _ {[i := ((env_inv env ∗ R)%I,1%Qp)]} with "Hlock [Hres] []"). + + rewrite /flock_resources big_sepM_singleton //. + + rewrite big_sepM_singleton //. + - iIntros (w) "[HΦ Hres]". + rewrite /flock_resources big_sepM_singleton /=. + iMod (flock_res_single_dealloc with "Hlock Hres") as (R') "[HR' #Heq]"; first done. + wp_let. + iApply "HΦ". iNext. iRewrite -"Heq" in "HR'". iDestruct "HR'" as "[_ $]". Qed. End a_wp_run. diff --git a/theories/lib/flock.v b/theories/lib/flock.v index cb485c1..4c5808e 100644 --- a/theories/lib/flock.v +++ b/theories/lib/flock.v @@ -23,13 +23,20 @@ Record flock_name := { Definition prop_id := positive. Canonical Structure gnameC := leibnizC gname. +Record PropPerm := { + prop_perm : frac; + prop_saved_name : gname; + prop_perm_name : gname +}. +Canonical Structure PropPermC := leibnizC PropPerm. + Class flockG Σ := FlockG { flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC))); flock_lockG :> lockG Σ; flock_savedProp :> savedPropG Σ; flock_tokens :> inG Σ fracR; - flock_props_active :> inG Σ (authR (optionUR (exclR (gmapC prop_id (prodC fracC (prodC gnameC gnameC)))))); + flock_props_active :> inG Σ (authR (optionUR (exclR (gmapC prop_id PropPermC)))); flock_props :> inG Σ (authR (gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC))))) }. @@ -38,7 +45,7 @@ Definition flockΣ : gFunctors := ;lockΣ ;savedPropΣ ;GFunctor fracR - ;GFunctor (authR (optionUR (exclR (gmapC prop_id (prodC fracC (prodC gnameC gnameC)))))) + ;GFunctor (authR (optionUR (exclR (gmapC prop_id PropPermC)))) ;GFunctor (authR (gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC)))))%CF]. Instance subG_flockΣ Σ : subG flockΣ Σ → flockG Σ. @@ -48,11 +55,15 @@ Section flock. Context `{heapG Σ, flockG Σ}. Variable N : namespace. Definition flockN := N.@"flock". - + Definition to_props_map (f : gmap prop_id (gname * gname)) : gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC))) := (λ x, (1%Qp, to_agree (x.1, x.2))) <$> f. + Definition to_props_map_ (f : gmap prop_id PropPerm) + : gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC))) := + (λ x, (prop_perm x, to_agree (prop_saved_name x, prop_perm_name x))) <$> f. + Lemma to_props_map_singleton_included fp i q ρ: {[i := (q, to_agree ρ)]} ≼ to_props_map fp → fp !! i = Some ρ. Proof. @@ -62,8 +73,9 @@ Section flock. rewrite Hi. by destruct v'. Qed. - Definition from_active (f : gmap prop_id (frac * (gname * gname))) - : gmap prop_id (gname * gname) := fmap snd f. + Definition from_active (f : gmap prop_id PropPerm) + : gmap prop_id (gname * gname) := + (λ x, (prop_saved_name x, prop_perm_name x)) <$> f. Lemma from_active_empty : from_active ∅ = ∅. Proof. by rewrite /from_active fmap_empty. Qed. @@ -71,13 +83,18 @@ Section flock. Definition all_props (f : gmap prop_id (gname*gname)) : iProp Σ := ([∗ map] i ↦ ρ ∈ f, ∃ R, saved_prop_own ρ.1 R ∗ R)%I. - Definition all_tokens (f : gmap prop_id (frac * (gname*gname))) : iProp Σ := - ([∗ map] i ↦ ρ ∈ f, own ρ.2.2 ρ.1)%I. + Lemma all_props_to_props_map_ f f1 f2 : + to_props_map f = to_props_map_ f1 ⋅ to_props_map_ f2 → + all_props f ⊣⊢ all_props (from_active f1) ∗ all_props (from_active f2). + Proof. Admitted. + + Definition all_tokens (f : gmap prop_id PropPerm) : iProp Σ := + ([∗ map] i ↦ ρ ∈ f, own (prop_perm_name ρ) (prop_perm ρ))%I. Definition flock_inv (γ : flock_name) : iProp Σ := (∃ (s : lockstate) (fp : gmap prop_id (gname * gname)) - (fa : gmap prop_id (frac * (gname * gname))), + (fa : gmap prop_id PropPerm), (** fa -- active propositions, fp -- pending propositions *) ⌜fp ##ₘ from_active fa⌝ ∗ own (flock_state_name γ) (● (Excl' s)) ∗ @@ -97,7 +114,7 @@ Section flock. (own (flock_state_name γ) (◯ (Excl' Unlocked))))%I. Definition flocked - (γ : flock_name) (f : gmap prop_id (frac * (gname * gname))) : iProp Σ := + (γ : flock_name) (f : gmap prop_id PropPerm) : iProp Σ := (own (flock_state_name γ) (◯ (Excl' Locked)) ∗ own (flock_props_active_name γ) (● Excl' f) ∗ all_props (from_active f))%I. @@ -135,18 +152,19 @@ Section flock. AsFractional (flock_res γ s R π) (flock_res γ s R) π. Proof. split. done. apply _. Qed. - Lemma flock_res_single_alloc γ lk R E : + Lemma flock_res_single_alloc (X : gset prop_id) γ lk R E : ↑flockN ⊆ E → is_flock γ lk -∗ ▷ R - ={E}=∗ ∃ s, flock_res γ s R 1. + ={E}=∗ ∃ s, ⌜s ∉ X⌝ ∧ 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". iMod (own_alloc 1%Qp) as (ρ2) "Hρ2"; first done. iInv (flockN.@"inv") as (s fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl". - pose (i := (fresh ((dom (gset prop_id) (fp ∪ from_active fa))))). - assert (i ∉ (dom (gset prop_id) (fp ∪ from_active fa))) as Hs. + pose (i := (fresh ((dom (gset prop_id) (fp ∪ from_active fa)) ∪ X))). + assert (i ∉ (dom (gset prop_id) (fp ∪ from_active fa)) ∪ X) as Hs. { apply is_fresh. } + apply not_elem_of_union in Hs. destruct Hs as [Hi1 Hi2]. iMod (own_update with "Hauth") as "Hauth". { apply (auth_update_alloc _ (to_props_map (<[i := (ρ1,ρ2)]> fp ∪ from_active fa)) {[ i := (1%Qp, to_agree (ρ1, ρ2)) ]}). @@ -156,17 +174,18 @@ Section flock. apply (not_elem_of_dom (to_props_map (fp ∪ from_active fa)) i (D:=gset prop_id)). by rewrite /to_props_map dom_fmap. } iDestruct "Hauth" as "[Hauth Hres]". - iExists i, (ρ1,ρ2). iFrame "Hres Hρ1 Hρ2". - iApply ("Hcl" with "[-]"). - iNext. iExists _,_,_. iFrame. iFrame "Hrest". - rewrite /all_props big_sepM_insert; last first. - + apply (not_elem_of_dom _ i (D:=gset prop_id)). - revert Hs. rewrite dom_union_L not_elem_of_union. set_solver. - + iFrame "Hfp". iSplitR; last by eauto. - iPureIntro. apply map_disjoint_insert_l_2; eauto. - eapply (not_elem_of_dom (D:=gset prop_id)). - intros Hi; apply Hs. rewrite dom_union_L elem_of_union. - eauto. + iExists i. iMod ("Hcl" with "[-Hres Hρ1 Hρ2]") as "_". + { iNext. iExists _,_,_. iFrame. iFrame "Hrest". + rewrite /all_props big_sepM_insert; last first. + + apply (not_elem_of_dom _ i (D:=gset prop_id)). + revert Hi1. rewrite dom_union_L not_elem_of_union. set_solver. + + iFrame "Hfp". iSplitR; last by eauto. + iPureIntro. apply map_disjoint_insert_l_2; eauto. + eapply (not_elem_of_dom (D:=gset prop_id)). + intros Hi; apply Hi1. rewrite dom_union_L elem_of_union. + eauto. } + iModIntro; iSplit; eauto. + iExists (ρ1,ρ2). iFrame "Hres Hρ1 Hρ2". Qed. Lemma flock_res_single_dealloc γ lk i R E : @@ -181,7 +200,7 @@ Section flock. 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. - { remember (fa !! i) as fai. destruct fai as [[π [ρ'1 ρ'2]]|]; last done. + { remember (fa !! i) as fai. destruct fai as [[π ρ'1 ρ'2]|]; last done. iExFalso. assert (fp !! i = None) as Hbar. { apply lookup_union_Some_raw in Hfoo. @@ -271,10 +290,206 @@ Section flock. (* (▷ ([∗ list] (i, R, π) ∈ I, R) *) (* ={⊤}=∗ flocked γ ∅ ∗ ([∗ list] (i, R, π) ∈ I, flock_res γ i R π) }}}. *) - Lemma acquire_cancel_spec γ π lk i R : + Lemma extract_existential {A B C : Type} `{EqDecision A, Countable A} (I : gmap A B) (P : A -> B -> C -> iProp Σ) : + (([∗ map] a ↦ b ∈ I, ∃ c : C, P a b c) ⊢ + ∃ J : gmap A (B*C), ⌜fmap fst J = I⌝ ∗ [∗ map] a ↦ bc ∈ J, P a bc.1 bc.2)%I. + Proof. + simple refine (map_ind (λ I, (([∗ map] a ↦ b ∈ I, ∃ c : C, P a b c) ⊢ + ∃ J : gmap A (B*C), ⌜fmap fst J = I⌝ ∗ [∗ map] a ↦ bc ∈ J, P a bc.1 bc.2)) _ _ I); simpl. + - rewrite big_sepM_empty. + iIntros "_". iExists ∅. iSplit; eauto. by rewrite fmap_empty. + - iIntros (a b I' Ha HI') "H". + rewrite big_sepM_insert; auto. + iDestruct "H" as "[HC H]". + iDestruct "HC" as (c) "Habc". + rewrite HI'. iDestruct "H" as (J' HJ') "H". + iExists (<[a:=(b,c)]>J'). iSplit. + + iPureIntro. by rewrite fmap_insert /=HJ'. + + rewrite big_sepM_insert; eauto with iFrame. + cut (fst <$> J' !! a = None). + { destruct (J' !! a); eauto; inversion 1. } + rewrite -lookup_fmap HJ' //. + Qed. + + Lemma big_sepM_own_frag {A B : Type} `{EqDecision A, Countable A} + `{inG Σ (authR (gmapUR A C))} (f : B → C) (m : gmap A B) (γ : gname) : + own γ (◯ ∅) -∗ + own γ (◯ (f <$> m)) ∗-∗ [∗ map] i↦x ∈ m, own γ (◯ {[ i := f x ]}). + Proof. + simple refine (map_ind (λ m, _)%I _ _ m); simpl. + - iIntros "He". rewrite fmap_empty big_sepM_empty. iSplit; eauto. + - iIntros (i x m' Hi IH) "He". + rewrite fmap_insert insert_union_singleton_l. + assert (({[i := f x]} ∪ (f <$> m')) = {[i := f x]} ⋅ (f <$> m')) as ->. + { rewrite /op /cmra_op /= /gmap_op. + apply map_eq. intros j. destruct (decide (i = j)) as [->|?]. + - etransitivity. eapply lookup_union_Some_l. apply lookup_insert. + symmetry. rewrite lookup_merge lookup_insert. + rewrite lookup_fmap Hi /=. done. + - remember (m' !! j) as mj. + destruct mj; simplify_eq/=. + + etransitivity. apply lookup_union_Some_raw. + right. split; first by rewrite lookup_insert_ne. + by rewrite lookup_fmap -Heqmj. + symmetry. rewrite lookup_merge lookup_singleton_ne; eauto. + rewrite lookup_fmap -Heqmj. done. + + etransitivity. apply lookup_union_None. + split; first by rewrite lookup_singleton_ne. + rewrite lookup_fmap -Heqmj //. + symmetry. + rewrite lookup_merge lookup_singleton_ne // lookup_fmap -Heqmj //. } + rewrite auth_frag_op own_op IH big_sepM_insert; last eauto. + iSplit; iIntros "[$ Hm']"; by iApply "He". + Qed. + +(* here it is crucial that we use a gmap: + that way there is at most one flock_res associated with a prop_id *) + Lemma acquire_cancel_spec γ lk (I : gmap prop_id (iProp Σ * frac)) : + {{{ is_flock γ lk ∗ [∗ map] i ↦ p ∈ I, flock_res γ i p.1 p.2 }}} + acquire lk + {{{ RET #(); + (▷ [∗ map] p ∈ I, p.1) + ∗ ((▷ [∗ map] p ∈ I, p.1) ={⊤}=∗ flocked γ ∅ + ∗ [∗ map] i ↦ p ∈ I, flock_res γ i p.1 p.2) }}}. + Proof. + iIntros (Φ) "(Hl & HRres) HΦ". + rewrite /is_flock. iDestruct "Hl" as "(#Hinv & #Hlk)". + iApply (acquire_spec with "Hlk"). + iNext. iIntros "[Hlocked Hunlk]". + iInv (flockN.@"inv") as ([|] fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl". + - iDestruct "Hrest" as "(>Hlocked2 & Htokens)". + iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2"). + - iDestruct "Hrest" as ">Haactive". + iAssert (⌜fa = ∅⌝)%I with "[-]" as %->. + { iDestruct (own_valid_2 with "Haactive Hfactive") + as %[Hfoo%Excl_included _]%auth_valid_discrete_2. + iPureIntro. by unfold_leibniz. } + rewrite from_active_empty right_id. + + (* Unlocked ~~> Locked *) + iMod (own_update_2 with "Hstate Hunlk") as "Hstate". + { apply (auth_update _ _ (Excl' Locked) (Excl' Locked)). + apply option_local_update. + by apply exclusive_local_update. } + iDestruct "Hstate" as "[Hstate Hflkd]". + + iDestruct (extract_existential with "HRres") as (J HJ) "HRres". + + iAssert (([∗ map] a↦bc ∈ J, own (flock_props_name γ) (◯ {[a := (bc.1.2, to_agree bc.2)]})) ∗ ([∗ map] a↦bc ∈ J, saved_prop_own bc.2.1 bc.1.1 ∗ own bc.2.2 bc.1.2))%I with "[HRres]" as "[Hfs HJ]". + { rewrite -big_sepM_sepM. iApply (big_sepM_mono with "HRres"). + iIntros (k x Hk) "(? & ? & ?)". eauto with iFrame. } + pose (fs := fmap (λ bc, {| prop_perm := bc.1.2; prop_saved_name := bc.2.1; prop_perm_name := bc.2.2 |}) J). + + iMod (own_update _ _ (● to_props_map fp ⋅ ◯ ∅) with "Hauth") as "[Hauth He]". + { by apply auth_update_alloc. } + iAssert (own (flock_props_name γ) (◯ to_props_map_ fs))%I with "[Hfs He]" as "Hfs". + { unfold fs. iApply (big_sepM_own_frag with "He"). + rewrite big_sepM_fmap /=. iApply (big_sepM_mono with "Hfs"). + iIntros (k x Hk) "H /=". by destruct (x.2). } + + (* fs ≤ fp *) + iDestruct (own_valid_2 with "Hauth Hfs") + as %[Hfoo _]%auth_valid_discrete_2. + + assert (∃ fo : gmap prop_id PropPerm, + to_props_map fp = to_props_map_ fs ⋅ to_props_map_ fo) + as [fo Hfo]. + { admit. } + + rewrite (all_props_to_props_map_ fp fs fo); last done. + iDestruct "Hfp" as "[Hfs_props Hfo]". + + iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]". + { apply (auth_update _ _ (Excl' fs) + (Excl' fs)). + by apply option_local_update, exclusive_local_update. } + + rewrite (big_sepM_sepM _ _ J). + iDestruct "HJ" as "[#HJ Htokens]". + + iMod ("Hcl" with "[-HΦ Haactive Hflkd Hfs_props Hfs HJ]") as "_". + { iNext. iExists Locked,(from_active fo),fs. + iFrame. iSplitR. admit. (* TODO: map_disjoint *) + iSplitL "Hauth". + - admit. (* fp = from_active fo ∪ from_active fs *) + - rewrite /all_tokens /fs big_sepM_fmap /= //. } + + iAssert (▷▷ [∗ map] p ∈ I, p.1)%I with "[Hfs_props]" as "Hfs_props". + { iNext. rewrite /all_props /fs -HJ !big_sepM_fmap big_sepM_later /=. + (* TODO: why is big_sepM_mono not formulated with the persistence modality? *) + iCombine "HJ Hfs_props" as "Hfs". + rewrite -big_sepM_sepM. + iApply (big_sepM_mono with "Hfs"). + iIntros (k ρ Hk) "[#Hsaved HR]". + iDestruct "HR" as (R') "[Hsaved' HR']". + iDestruct (saved_prop_agree with "Hsaved Hsaved'") as "#Hfoo". + iNext. iRewrite -"Hfoo" in "HR'". done. + (* TODO: iRewrite "Hfoo" didn't work *) } + + iModIntro. iApply "HΦ". + iNext. iFrame "Hfs_props". iIntros "Hfs_props". + clear Hfoo H1 Hfo fp. rewrite /flocked /flock_res. + iInv (flockN.@"inv") as ([|] fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl"; last first. + + iDestruct (own_valid_2 with "Hstate Hflkd") + as %[Hfoo%Excl_included _]%auth_valid_discrete_2. + fold_leibniz. inversion Hfoo. + + iDestruct "Hrest" as ">[Hlocked Htokens]". + + iDestruct (own_valid_2 with "Haactive Hfactive") + as %[Hfoo%Excl_included _]%auth_valid_discrete_2. + fold_leibniz. simplify_eq/=. + + iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]". + { apply (auth_update _ _ (Excl' ∅) (Excl' ∅)). + by apply option_local_update, exclusive_local_update. } + + (* fs ≤ fp *) + iDestruct (own_valid_2 with "Hauth Hfs") + as %[Hfoo _]%auth_valid_discrete_2. + + iMod (own_update _ _ (● to_props_map _ ⋅ ◯ ∅) with "Hauth") as "[Hauth He]". + { by apply auth_update_alloc. } + + iMod ("Hcl" with "[Hlocked Hstate Hauth Hfactive Hfp Hfs_props]") as "_". + { iNext. iExists Locked,(fp ∪ from_active fs),∅. iFrame. + iSplitR. + { rewrite from_active_empty. iPureIntro. apply map_disjoint_empty_r. } + iSplitL "Hauth". + - by rewrite from_active_empty right_id. + - iSplitL; last first. + { by rewrite /all_tokens big_sepM_empty. } + rewrite big_sepM_fmap. + rewrite /fs /from_active. + (* TODO: need all_props union lemma *) + admit. } + iModIntro. iFrame. rewrite /all_props from_active_empty big_sepM_empty. + iSplitR; first done. rewrite /all_tokens big_sepM_fmap. + rewrite {1}/fs /to_props_map_ -map_fmap_compose /=. + iAssert ([∗ map] k↦y ∈ J, own (flock_props_name γ) (◯ {[k := (y.1.2, to_agree y.2)]}))%I with "[Hfs He]" as "Hfs". + { iApply (big_sepM_own_frag with "He"); simpl. + assert (((λ y, (y.1.2, to_agree y.2)) <$> J) = ((λ x : PropPerm, (prop_perm x, + to_agree (prop_saved_name x, prop_perm_name x))) + ∘ (λ bc : iProp Σ * Qp * (gname * gname), + {| + prop_perm := bc.1.2; + prop_saved_name := bc.2.1; + prop_perm_name := bc.2.2 |}) <$> J)) as Hh. + { apply map_eq=>i /=. rewrite !lookup_fmap /=. + destruct (J !! i);eauto. simpl. by destruct (p.2). } + rewrite Hh. done. } + iCombine "Hfs Htokens" as "Hm". + rewrite /fs big_sepM_fmap -big_sepM_sepM. + iCombine "HJ Hm" as "Hm". rewrite -big_sepM_sepM. + iApply (big_sepM_mono with "Hm"). + iIntros (k x Hk) "(Hsaved & Hx & Hperm)". simpl. + iExists x.2. iFrame. + Admitted. + + + Lemma acquire_single_cancel_spec γ π lk i R : {{{ is_flock γ lk ∗ flock_res γ i R π }}} acquire lk - {{{ RET #(); ∃ R', R' ∗ ▷ (R ≡ R') ∗ (▷ R' ={⊤}=∗ flocked γ ∅ ∗ flock_res γ i R π) }}}. + {{{ RET #(); ▷ R ∗ (▷ R ={⊤}=∗ flocked γ ∅ ∗ flock_res γ i R π) }}}. Proof. iIntros (Φ) "(Hl & HRres) HΦ". rewrite /is_flock. iDestruct "Hl" as "(#Hinv & #Hlk)". @@ -309,13 +524,18 @@ Section flock. (* move (i,ρ) to the set of active propositions *) iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]". - { apply (auth_update _ _ (Excl' {[ i := (π, (ρ1, ρ2)) ]}) - (Excl' {[ i := (π, (ρ1, ρ2)) ]})). - apply option_local_update. - by apply exclusive_local_update. } + { apply (auth_update _ _ (Excl' {[ i := {| prop_perm := π; + prop_saved_name := ρ1; + prop_perm_name := ρ2 |} ]}) + (Excl' {[ i := {| prop_perm := π; + prop_saved_name := ρ1; + prop_perm_name := ρ2 |} ]})). + by apply option_local_update, exclusive_local_update. } iMod ("Hcl" with "[-HΦ HR' Hfoo Haactive Hflkd HR]") as "_". - { iNext. iExists Locked,(delete i fp),{[i := (π, (ρ1, ρ2))]}. + { iNext. iExists Locked,(delete i fp),{[i := {| prop_perm := π; + prop_saved_name := ρ1; + prop_perm_name := ρ2 |}]}. iFrame. iSplitR. admit. (* TODO: map_disjoint *) iSplitL "Hauth". - rewrite /from_active map_fmap_singleton /=. @@ -337,7 +557,9 @@ Section flock. - rewrite /all_tokens big_sepM_singleton //. } iModIntro. (* iApply ("HΦ" $! {[ i := (π, (ρ1, ρ2)) ]}). *) iApply "HΦ". - iNext. iExists R'. iFrame "HR' Hfoo". iIntros "HR'". + iNext. iAssert (▷ R)%I with "[HR']" as "HR'". + { iNext. by iRewrite "Hfoo". } + iFrame "HR'". iIntros "HR'". clear Hfoo H1 fp. rewrite /flocked /flock_res. iInv (flockN.@"inv") as ([|] fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl"; last first. + iDestruct (own_valid_2 with "Hstate Hflkd") @@ -370,7 +592,7 @@ Section flock. - rewrite /all_tokens /all_props big_sepM_empty. iSplitL; last done. rewrite big_sepM_insert; last done. iFrame "Hfp". iExists R'. iFrame. simpl. - iRewrite "Hfoo" in "Hρ1". by iFrame. } + iRewrite "Hfoo" in "Hρ1". iRewrite "Hfoo" in "HR'". by iFrame. } iModIntro. iFrame. rewrite /all_props from_active_empty big_sepM_empty. iSplitR; first done. rewrite /all_tokens big_sepM_singleton. simpl. -- GitLab