flock.v 16.7 KB
Newer Older
1
(** Cancellable locks *)
Léon Gondelman's avatar
Léon Gondelman committed
2
From iris.heap_lang Require Export proofmode notation.
3
From iris.heap_lang Require Import spin_lock.
4 5
From iris.base_logic.lib Require Import cancelable_invariants auth saved_prop.
From iris.algebra Require Import auth agree excl frac gmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
From iris.bi.lib Require Import fractional.
Léon Gondelman's avatar
Léon Gondelman committed
7

8 9 10 11 12
Inductive lockstate :=
  | Locked : frac  lockstate
  | Unlocked.
Canonical Structure lockstateC := leibnizC lockstate.

13 14
Instance lockstate_inhabited : Inhabited lockstate := populate Unlocked.

15 16 17 18
Record flock_name := {
  flock_lock_name : gname;
  flock_cinv_name : gname;
  flock_state_name : gname;
19 20
  flock_props_name : gname;
  flock_props_active_name : gname
21 22
}.

23 24 25
(* positive so that we have a `Fresh` instance for `gset positive` *)
Definition prop_id := positive.

26 27 28
Class flockG Σ :=
  FlockG {
    flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
29 30 31 32
    flock_cinvG  :> cinvG Σ;
    flock_lockG  :> lockG Σ;
    flock_props :> authG Σ (optionUR (exclR (gmapC prop_id (iProp Σ))));
    flock_props_activeG :> authG Σ (gmapUR prop_id (agreeR (iProp Σ)))
33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
  }.

Section cinv_lemmas.
  Context `{invG Σ, cinvG Σ}.

  Lemma cinv_alloc_strong (G : gset gname) E N (Φ : gname  iProp Σ) :
     ( γ, ⌜γ  G  Φ γ) ={E}=  γ, ⌜γ  G  cinv N γ (Φ γ)  cinv_own γ 1.
  Proof.
    iIntros "HP".
    iMod (own_alloc_strong 1%Qp G) as (γ) "[% H1]"; first done.
    iMod (inv_alloc N _ (Φ γ  own γ 1%Qp)%I with "[HP]") as "#Hinv".
    - iNext. iLeft. by iApply "HP".
    - iExists γ. iModIntro. rewrite /cinv /cinv_own. iFrame "H1".
      iSplit; eauto. iExists _. iFrame "Hinv".
      iIntros "!# !>". iSplit; by iIntros "?".
  Qed.

  Lemma cinv_cancel_vs (P Q : iProp Σ) E N γ :
    N  E  cinv N γ P
    - (cinv_own γ 1   P ={E∖↑N}= cinv_own γ 1   Q)
    - cinv_own γ 1 ={E}=  Q.
  Proof.
    iIntros (?) "#Hinv Hvs Hγ". rewrite /cinv.
    iDestruct "Hinv" as (P') "[#HP' Hinv]".
    iInv N as "[HP|>Hγ']" "Hclose"; last first.
    - iDestruct (cinv_own_1_l with "Hγ Hγ'") as %[].
    - iMod ("Hvs" with "[$Hγ HP]") as "[Hγ HQ]".
      { by iApply "HP'". }
      iFrame. iApply "Hclose". iNext. by iRight.
  Qed.

End cinv_lemmas.

Léon Gondelman's avatar
Léon Gondelman committed
66
Section flock.
67 68 69
  Context `{heapG Σ, flockG Σ}.

  Variable N : namespace.
70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
  Definition flockN := N.@"flock".

  Definition to_props_map (f : gmap prop_id (iProp Σ))
    : gmapUR prop_id (agreeR (iProp Σ)) := to_agree <$> f.
  
  Lemma to_props_map_insert f i P :
    to_props_map (<[i:=P]>f) = <[i:=to_agree P]>(to_props_map f).
  Proof. by rewrite /to_props_map fmap_insert. Qed.

  Lemma to_props_map_dom f :
    dom (gset prop_id) (to_props_map f) = dom (gset prop_id) f.
  Proof. by rewrite /to_props_map dom_fmap_L. Qed.

  Definition all_props (f : gmap prop_id (iProp Σ)) : iProp Σ :=
    ([ map] i  R  f, R)%I.

  Lemma all_props_union f g :
    all_props f  all_props g  all_props (f  g).
  Proof.
    revert g.
    simple refine (map_ind (fun f =>  g, all_props f  all_props g - all_props (f  g)) _ _ f); simpl; rewrite /all_props.
    - intros g. by rewrite bi.big_sepM_empty !left_id.
    - intros i P f' Hi IH.
      intros g. rewrite bi.big_sepM_insert; last done.
      iIntros "[[HP Hf] Hg]".
      rewrite -insert_union_l.
      remember (g !! i) as Z. destruct Z as [R|].
      + assert (g = <[i:=R]>(delete i g)) as Hfoo.
        { rewrite insert_delete insert_id; eauto. }
        rewrite {1}Hfoo.
        rewrite bi.big_sepM_insert; last first.
        { apply lookup_delete. }
        iDestruct "Hg" as "[HR Hg]".
        iApply (bi.big_sepM_insert_override_2 _ _ i R P with "[-HP] [HP]"); simpl.
        { apply lookup_union_Some_raw. right. eauto. }
        * iApply (IH g).
          rewrite Hfoo bi.big_sepM_insert; last by apply lookup_delete.
          rewrite delete_insert; last by apply lookup_delete. iFrame.
        * eauto.
      + rewrite bi.big_sepM_insert; last first.
        { apply lookup_union_None. eauto. }
        iFrame. iApply (IH g). iFrame.
  Qed.

  Global Instance all_props_proper : Proper (() ==> ())
    (all_props : gmapC prop_id (iProp Σ)  iProp Σ).
  Proof.
    intros f. rewrite /all_props. (* rewrite /all_props /big_opM. *)
    simple refine (map_ind (fun f =>  g, f  g  _  _) _ _ f); simpl.
    - intros g. rewrite bi.big_sepM_empty.
      simple refine (map_ind (fun g =>   g  _  _) _ _ g); simpl.
      + by rewrite bi.big_sepM_empty.
      + intros j R g' Hj IH Hg'.
        exfalso. specialize (Hg' j). revert Hg'.
        rewrite lookup_insert lookup_empty. inversion 1.
    - intros i P f' Hi IH g Hf'.
      rewrite bi.big_sepM_insert; last done.
      specialize (IH (delete i g)).
      assert (f'  delete i g) as Hf'g.
      { by rewrite -Hf' delete_insert. }
      specialize (IH Hf'g). rewrite IH.
      assert ( R, g !! i = Some R  P  R) as [R [Hg HR]].
      { specialize (Hf' i).
        destruct (g !! i) as [R|]; last first.
        - exfalso. revert Hf'. rewrite lookup_insert. inversion 1.
        - exists R. split; auto.
          revert Hf'. rewrite lookup_insert. by inversion 1. }
      rewrite (bi.big_sepM_delete _ g i R); eauto.
      by apply bi.sep_proper.
  Qed.
140

141 142 143
  Definition flock_inv (γ : flock_name) : iProp Σ :=
    ( (s : lockstate) (fp fa : gmap prop_id (iProp Σ)),
       (** fa -- active propositions, fp -- inactive propositions *)
144
       own (flock_state_name γ) ( (Excl' s)) 
145 146
       own (flock_props_name γ) ( to_props_map (fp  fa)) 
       own (flock_props_active_name γ) ( Excl' fa) 
147 148 149
       match s with
       | Locked q =>
         cinv_own (flock_cinv_name γ) (q/2) 
150 151 152 153 154
         locked (flock_lock_name γ) 
         all_props fp
       | Unlocked => own (flock_props_active_name γ) ( Excl' fa) 
                     all_props fa 
                     fp = ∅⌝
155 156
       end)%I.

157 158 159
  Definition is_flock (γ : flock_name) (lk : val) : iProp Σ :=
    (cinv (flockN .@ "inv") (flock_cinv_name γ) (flock_inv γ) 
     is_lock (flockN .@ "lock") (flock_lock_name γ) lk
160
         (own (flock_state_name γ) ( (Excl' Unlocked))))%I.
161 162 163
  
  Definition flock_res (γ : flock_name) (s : prop_id) (R : iProp Σ) : iProp Σ :=
    (own (flock_props_name γ) ( {[ s := to_agree R ]}))%I.
164

165 166 167 168
  Global Instance is_flock_persistent γ lk : Persistent (is_flock γ lk).
  Proof. apply _. Qed.

  Global Instance flock_res_persistent γ s R : Persistent (flock_res γ s R).
169 170 171 172 173
  Proof. apply _. Qed.

  Definition unflocked (γ : flock_name) (q : frac) : iProp Σ :=
    cinv_own (flock_cinv_name γ) q.

174 175
  Definition flocked
    (γ : flock_name) (q : frac) (f : gmap prop_id (iProp Σ)) : iProp Σ :=
176
    (own (flock_state_name γ) ( (Excl' (Locked q)))
177 178 179
      cinv_own (flock_cinv_name γ) (q/2)
      own (flock_props_active_name γ) ( Excl' f)
       all_props f)%I.
180 181

  Lemma unflocked_op (γ : flock_name) (π1 π2 : frac) :
182
    unflocked γ (π1+π2)  unflocked γ π1  unflocked γ π2.
183 184
  Proof. by rewrite /unflocked fractional. Qed.

185
  Global Instance unflocked_fractional γ : Fractional (unflocked γ).
186 187 188
  Proof. intros p q. apply unflocked_op. Qed.
  Global Instance unflocked_as_fractional γ π :
    AsFractional (unflocked γ π) (unflocked γ) π.
Léon Gondelman's avatar
Léon Gondelman committed
189 190
  Proof. split. done. apply _. Qed.

191 192
  Lemma flock_res_alloc_unflocked γ lk π R :
    is_flock γ lk - unflocked γ π -  R ={}=  s, flock_res γ s R  unflocked γ π.
193
  Proof.
194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245
    iIntros "Hl Hunfl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first done.
    rewrite {2}/flock_inv.
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown & >Hlocked2 & Hfp)".
      pose (s := (fresh (dom (gset prop_id) (fp  fa)))).
      iMod (own_update  with "Hauth") as "Hauth".
      { apply (auth_update_alloc _ (to_props_map (<[s := R]> fp  fa))
                                 {[ s := to_agree R ]}).
        rewrite -insert_union_l.
        rewrite to_props_map_insert.
        apply alloc_local_update; last done.
        apply (not_elem_of_dom (to_props_map (fp  fa)) s (D:=gset prop_id)).
        rewrite to_props_map_dom.
        apply is_fresh. }
      iDestruct "Hauth" as "[Hauth Hres]".
      iExists s. iFrame "Hres Hunfl".
      iApply ("Hcl" with "[-]").
      iNext. iExists _,_,_. iFrame. iFrame "Hcown Hlocked2".
      rewrite /all_props bi.big_sepM_insert. iFrame.
      apply (not_elem_of_dom _ s (D:=gset prop_id)).
      assert (s  (dom (gset prop_id) (fp  fa))) as Hs.
      { apply is_fresh. }
      revert Hs. rewrite dom_union_L not_elem_of_union. set_solver.
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. rewrite left_id.
      pose (s := (fresh (dom (gset prop_id) fa))).
      iMod (own_update  with "Hauth") as "Hauth".
      { apply (auth_update_alloc _ (to_props_map (<[s := R]> fa))
                                 {[ s := to_agree R ]}).
        rewrite to_props_map_insert.
        apply alloc_local_update; last done.
        apply (not_elem_of_dom (to_props_map fa) s (D:=gset prop_id)).
        rewrite to_props_map_dom.
        apply is_fresh. }
      iDestruct "Hauth" as "[Hauth Hres]".
      iExists s. iFrame "Hres Hunfl".
      iMod (own_update_2 _ _ _ (( Excl' (<[s:=R]>fa))  ( Excl' (<[s:=R]>fa)))
              with "Hactive Hfactive") as "[Hactive Hfactive]".
      { by apply auth_update, option_local_update, exclusive_local_update. }
      iApply ("Hcl" with "[-]").
      iNext. iExists _,,_. rewrite left_id. iFrame. iFrame "Hactive".
      iSplit; auto.
      rewrite /all_props bi.big_sepM_insert. iFrame.
      apply (not_elem_of_dom _ s (D:=gset prop_id)).
      apply is_fresh.
  Qed.

  Lemma newlock_cancel_spec :
    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk  unflocked γ 1 }}}.
  Proof.
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
246 247
    iMod (own_alloc ( (Excl' Unlocked)   (Excl' Unlocked)))
      as (γ_state) "[Hauth Hfrag]"; first done.
248 249 250 251 252 253 254
    iMod (own_alloc ( to_props_map )) as (γ_props) "Hprops".
    { apply auth_valid_discrete. simpl.
      split; last done. apply ucmra_unit_least. }
    iMod (own_alloc (( Excl' )  ( Excl' ))) as (γ_ac_props) "[Hacprops1 Hacprops2]".
    { apply auth_valid_discrete. simpl.
      split; last done. by rewrite left_id. }
    iApply (newlock_spec (flockN.@"lock") (own γ_state ( (Excl' Unlocked))) with "Hfrag").
255
    iNext. iIntros (lk γ_lock) "#Hlock".
256 257
    iMod (cinv_alloc_strong  _ (flockN.@"inv")
       (fun γ => flock_inv (Build_flock_name γ_lock γ γ_state γ_props γ_ac_props)) with "[-HΦ]") as (γ_cinv) "(_ & #Hcinv & Hown)".
258
    { iNext. rewrite /flock_inv /=. iIntros (γ _).
259 260 261 262
      iExists Unlocked, , . rewrite left_id. iFrame.
      by rewrite /all_props !bi.big_sepM_empty. }
    pose (γ := (Build_flock_name γ_lock γ_cinv γ_state γ_props γ_ac_props)).
    iModIntro. iApply ("HΦ" $! lk γ with "[-]"). iFrame "Hown".
263 264
    rewrite /is_flock. by iFrame "Hlock".
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
265

266 267
  Lemma acquire_cancel_spec γ π lk s R :
    {{{ is_flock γ lk  unflocked γ π   flock_res γ s R }}}
268
      acquire lk
269
    {{{ f, RET #();  R  ( R - flocked γ π f) }}}.
270
  Proof.
271
    iIntros (Φ) "(Hl & Hunfl & #HRres) HΦ". rewrite -wp_fupd.
272 273 274 275 276
    rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iApply (acquire_spec with "Hlk"). iNext.
    iIntros "[Hlocked Hunlk]".
    iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first done.
    rewrite {2}/flock_inv.
277 278
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown & >Hlocked2 & Hfp)".
279
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
280 281
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. rewrite left_id.
282 283 284 285 286 287
      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 "Hunfl" as "[Hunfl Hcown]".
288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306
      iAssert ( R', R  R'  fa !! s = Some R')%I
        with "[HRres Hauth]" as %Hfoo.
      { iDestruct (own_valid_2 with "Hauth HRres")
          as %[Hfoo _]%auth_valid_discrete.
        iPureIntro. revert Hfoo.
        rewrite /= left_id singleton_included=> -[R' [Hf HR]].
        revert Hf HR.
        rewrite /to_props_map lookup_fmap fmap_Some_equiv=>-[R'' [/= Hf ->]].
        intros [?%to_agree_inj | ?%to_agree_included]%Some_included;
          simplify_eq/=; exists R''; eauto. }
      destruct Hfoo as [R' [HReq Hf]].
      rewrite /all_props {1}(bi.big_sepM_lookup_acc _ fa s R'); last done.
      iDestruct "Hfa" as "[HR' Hfa]".
      iMod ("Hcl" with "[Hstate Hcown Hlocked Hauth Hfactive]").
      { iNext. iExists (Locked π),,fa. rewrite left_id. iFrame.
        by rewrite /all_props bi.big_sepM_empty. }
      iModIntro. 
      iApply ("HΦ" $! fa). rewrite -HReq. iFrame.
      by iApply bi.later_wand.
307
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
308

309 310
  Lemma release_cancel_spec γ π lk f :
    {{{ is_flock γ lk  flocked γ π f }}}
311 312 313
      release lk
    {{{ RET #(); unflocked γ π }}}.
  Proof.
314
    iIntros (Φ) "(Hl & (Hstate' & Hflkd & Hactive & Hf)) HΦ". rewrite -fupd_wp.
315 316 317
    rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iMod (cinv_open with "Hcinv Hflkd") as "(Hstate & Hunfl & Hcl)"; first done.
    rewrite {2}/flock_inv.
318 319
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)"; last first.
    - iDestruct "Hrest" as "(>Hactive2 & Hfa & >%)".
320 321 322 323 324 325
      iExFalso. iDestruct (own_valid_2 with "Hstate Hstate'") as %Hfoo.
      iPureIntro. revert Hfoo.
      rewrite auth_valid_discrete /= left_id.
      intros [Hexcl _].
      apply Some_included_exclusive in Hexcl; try (done || apply _).
      simplify_eq.
326
    - iDestruct "Hrest" as "(>Hcown & >Hlocked & Hfp)".
327 328 329 330 331 332 333 334 335 336 337 338
      iAssert (q = π⌝)%I with "[Hstate Hstate']" as  %->.
      { iDestruct (own_valid_2 with "Hstate Hstate'") as %Hfoo.
        iPureIntro. revert Hfoo.
        rewrite auth_valid_discrete /= left_id.
        intros [Hexcl _].
        apply Some_included_exclusive in Hexcl; try (done || apply _).
        by simplify_eq. }
      iMod (own_update_2 with "Hstate Hstate'") as "Hstate".
      { apply (auth_update _ _ (Excl' Unlocked) (Excl' Unlocked)).
        apply option_local_update.
        by apply exclusive_local_update. }
      iDestruct "Hstate" as "[Hstate Hstate']".
339 340 341 342 343 344 345 346 347 348 349 350 351 352
      iAssert ((f : gmapC prop_id (iProp Σ))  fa%I) with "[Hactive Hfactive]" as %Hfoo.
      { iDestruct (own_valid_2 with "Hactive Hfactive") as %Hfoo.
        iPureIntro. apply auth_valid_discrete_2 in Hfoo.
        destruct Hfoo as [Hfoo _].
        apply Some_included_exclusive in Hfoo; [|apply _|done].
        by apply Excl_inj. }
      rewrite {1}Hfoo.
      iMod (own_update_2 _ _ _ ( Excl' (fp  fa)   Excl' (fp  fa))
              with "Hactive Hfactive") as "[Hactive Hfactive]".
      { by apply auth_update, option_local_update, exclusive_local_update. }
      iMod ("Hcl" with "[Hstate Hauth Hfp Hf Hactive Hfactive]").
      { iNext. iExists Unlocked,,(fpfa). rewrite left_id. iFrame.
        rewrite Hfoo. iSplit; eauto.
        iApply all_props_union; iFrame. }
353 354
      iApply (release_spec with "[$Hlk $Hlocked $Hstate']").
      iModIntro. iNext. iIntros "_". iApply "HΦ".
355
      rewrite /unflocked. by iSplitL "Hcown".
356
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
357

358 359
  Lemma cancel_lock γ lk s R :
    is_flock γ lk - flock_res γ s R - unflocked γ 1 ={}=  R.
360 361
  Proof.
    rewrite /is_flock /unflocked.
362 363
    iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "#Hres Hcown".
    rewrite /flock_res.
364
    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; eauto.
365
    iIntros "[Hcown Hstate]".
366 367
    iDestruct "Hstate" as ([q|] fp fa) "(Hstate & >Hauth & Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown2 & >Hlocked & Hfp)".
368
      iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. iFrame. rewrite left_id.
      iAssert ( R', R  R'  fa !! s = Some R')%I
        with "[Hres Hauth]" as %Hfoo.
      { iDestruct (own_valid_2 with "Hauth Hres")
          as %[Hfoo _]%auth_valid_discrete.
        iPureIntro. revert Hfoo.
        rewrite /= left_id singleton_included=> -[R' [Hf HR]].
        revert Hf HR.
        rewrite /to_props_map lookup_fmap fmap_Some_equiv=>-[R'' [/= Hf ->]].
        intros [?%to_agree_inj | ?%to_agree_included]%Some_included;
          simplify_eq/=; exists R''; eauto. }
      destruct Hfoo as [R' [HReq Hf]].
      rewrite /all_props {1}(bi.big_sepM_lookup_acc _ fa s R'); last done.
      iDestruct "Hfa" as "[HR' Hfa]".
      assert (( R)%I  ( R')%I) as ->. by apply bi.later_proper.
      by iFrame.
386
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
387
End flock.