flock.v 24.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
  Definition flockN := N.@"flock".

  Definition to_props_map (f : gmap prop_id (iProp Σ))
    : gmapUR prop_id (agreeR (iProp Σ)) := to_agree <$> f.
Dan Frumin's avatar
Dan Frumin committed
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
  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.
Dan Frumin's avatar
Dan Frumin committed
161 162 163 164 165

  Definition flock_res (γ : flock_name) (R : iProp Σ) : iProp Σ :=
    ( f, R  all_props f  own (flock_props_name γ) ( to_props_map f))%I.

  Definition flock_res_single (γ : flock_name) (s : prop_id) (R : iProp Σ) : iProp Σ :=
166
    (own (flock_props_name γ) ( {[ s := to_agree R ]}))%I.
167

168 169 170
  Global Instance is_flock_persistent γ lk : Persistent (is_flock γ lk).
  Proof. apply _. Qed.

Dan Frumin's avatar
Dan Frumin committed
171
  Global Instance flock_res_persistent γ R : Persistent (flock_res γ R).
172 173
  Proof. apply _. Qed.

Dan Frumin's avatar
Dan Frumin committed
174 175 176 177 178 179 180 181 182
  Global Instance flock_res_single_persistent γ s R : Persistent (flock_res_single γ s R).
  Proof. apply _. Qed.

  Global Instance flock_res_proper : Proper ((=) ==> () ==> ()) flock_res.
  Proof.
    intros ? γ -> P R HPR. rewrite /flock_res.
    apply bi.exist_proper=>f. by rewrite HPR.
  Qed.

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

186 187
  Definition flocked
    (γ : flock_name) (q : frac) (f : gmap prop_id (iProp Σ)) : iProp Σ :=
188
    (own (flock_state_name γ) ( (Excl' (Locked q)))
189 190 191
      cinv_own (flock_cinv_name γ) (q/2)
      own (flock_props_active_name γ) ( Excl' f)
       all_props f)%I.
192 193

  Lemma unflocked_op (γ : flock_name) (π1 π2 : frac) :
194
    unflocked γ (π1+π2)  unflocked γ π1  unflocked γ π2.
195 196
  Proof. by rewrite /unflocked fractional. Qed.

197
  Global Instance unflocked_fractional γ : Fractional (unflocked γ).
198 199 200
  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
201 202
  Proof. split. done. apply _. Qed.

Dan Frumin's avatar
Dan Frumin committed
203 204 205
  Lemma flock_res_single_alloc_unflocked (X : gset prop_id) γ lk π R :
    is_flock γ lk - unflocked γ π -  R
    ={}=  s, s  X  flock_res_single γ s R  unflocked γ π.
206
  Proof.
207 208 209 210 211
    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)".
Dan Frumin's avatar
Dan Frumin committed
212 213 214 215 216
      pose (s := (fresh ((dom (gset prop_id) (fp  fa))  X))).
      assert (s  (dom (gset prop_id) (fp  fa))) as Hs.
      { intros Hs.
        apply (elem_of_union_l s (dom (gset prop_id) (fp  fa)) X) in Hs.
        revert Hs. apply is_fresh. }
217 218 219 220 221 222 223
      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)).
Dan Frumin's avatar
Dan Frumin committed
224
        rewrite to_props_map_dom. done. }
225 226
      iDestruct "Hauth" as "[Hauth Hres]".
      iExists s. iFrame "Hres Hunfl".
Dan Frumin's avatar
Dan Frumin committed
227 228 229 230 231 232 233 234 235
      iMod ("Hcl" with "[-]") as "_".
      { iNext. iExists _,_,_. iFrame. iFrame "Hcown Hlocked2".
        rewrite /all_props bi.big_sepM_insert. iFrame.
        apply (not_elem_of_dom _ s (D:=gset prop_id)).
        revert Hs. rewrite dom_union_L not_elem_of_union. set_solver. }
      iModIntro. iPureIntro.
      clear Hs. intros Hs.
      apply (elem_of_union_r s (dom (gset prop_id) (fp  fa)) X) in Hs.
      revert Hs. apply is_fresh.
236 237
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. rewrite left_id.
Dan Frumin's avatar
Dan Frumin committed
238 239 240 241 242
      pose (s := (fresh (dom (gset prop_id) fa  X))).
      assert (s  (dom (gset prop_id) fa)) as Hs.
      { intros Hs.
        apply (elem_of_union_l s _ X) in Hs.
        revert Hs. apply is_fresh. }
243 244 245 246 247 248
      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)).
Dan Frumin's avatar
Dan Frumin committed
249
        rewrite to_props_map_dom. done. }
250 251 252 253 254
      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. }
Dan Frumin's avatar
Dan Frumin committed
255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305
      iMod ("Hcl" with "[-]") as "_".
      { iNext. iExists _,,_. rewrite left_id. iFrame. iFrame "Hactive".
        iSplit; auto.
        rewrite /all_props bi.big_sepM_insert. iFrame.
        by apply (not_elem_of_dom _ s (D:=gset prop_id)). }
      iModIntro. iPureIntro.
      clear Hs. intros Hs.
      apply (elem_of_union_r s (dom (gset prop_id) fa) X) in Hs.
      revert Hs. apply is_fresh.
  Qed.

  Lemma flock_res_alloc_unflocked γ lk π R :
    is_flock γ lk - unflocked γ π -  R ={}= flock_res γ R  unflocked γ π.
  Proof.
    iIntros "#Hlk Hunfl HR".
    iMod (flock_res_single_alloc_unflocked  with "Hlk Hunfl HR") as (s ?) "[HR $]".
    iModIntro. iExists {[s := R]}.
    rewrite /flock_res_single /to_props_map map_fmap_singleton. iFrame "HR".
    iPureIntro. by rewrite /all_props bi.big_sepM_singleton.
  Qed.

  Lemma flock_res_insert_unflocked γ lk π P R :
    is_flock γ lk - flock_res γ P - unflocked γ π -  R
    ={}= flock_res γ (PR)  unflocked γ π.
  Proof.
    iIntros "#Hlk #Hres Hunfl HR".
    iDestruct "Hres" as (f Hfeq) "Hf".
    iMod (flock_res_single_alloc_unflocked (dom (gset prop_id) f)
            with "Hlk Hunfl HR") as (s Hs) "[HR $]".
    iModIntro. iExists (<[s := R]>f).
    rewrite to_props_map_insert /flock_res_single.
    iCombine "HR Hf" as "HR".
    (* TODO this should be a lemma, somewhere in std++ *)
    rewrite /op /cmra_op /= /ucmra_op /= /gmap_op /=.
    assert ((merge op {[s := to_agree R]} (to_props_map f))
            = <[s:=to_agree R]> (to_props_map f)) as Hmerge.
    { apply map_eq=>i. rewrite lookup_merge.
      destruct (decide (s = i)) as [->|?].
      - rewrite lookup_singleton lookup_insert.
        rewrite /to_props_map lookup_fmap.
        assert (f !! i = None) as ->.
        + by rewrite -(not_elem_of_dom (D:=(gset prop_id))).
        + simpl. done.
      - rewrite lookup_singleton_ne; auto.
        rewrite lookup_insert_ne; auto.
        remember (to_props_map f !! i) as o. rewrite -Heqo.
        by destruct o. }
    rewrite Hmerge. iFrame "HR".
    iPureIntro. rewrite /all_props bi.big_sepM_insert; last first.
    - by apply (not_elem_of_dom (D:=gset prop_id)).
    - rewrite comm Hfeq /all_props. reflexivity.
306 307 308 309 310 311
  Qed.

  Lemma newlock_cancel_spec :
    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk  unflocked γ 1 }}}.
  Proof.
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
312 313
    iMod (own_alloc ( (Excl' Unlocked)   (Excl' Unlocked)))
      as (γ_state) "[Hauth Hfrag]"; first done.
314 315 316 317 318 319 320
    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").
321
    iNext. iIntros (lk γ_lock) "#Hlock".
322 323
    iMod (cinv_alloc_strong  _ (flockN.@"inv")
       (fun γ => flock_inv (Build_flock_name γ_lock γ γ_state γ_props γ_ac_props)) with "[-HΦ]") as (γ_cinv) "(_ & #Hcinv & Hown)".
324
    { iNext. rewrite /flock_inv /=. iIntros (γ _).
325 326 327 328
      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".
329 330
    rewrite /is_flock. by iFrame "Hlock".
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
331

Dan Frumin's avatar
Dan Frumin committed
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425
  Lemma flock_res_auth γ R fp :
    flock_res γ R -
    own (flock_props_name γ) ( to_props_map fp) -
     f', all_props fp  R  all_props f'.
  Proof.
    rewrite /flock_res. iDestruct 1 as (f Heq) "#Hf".
    iIntros "Hauth".
    iDestruct (own_valid_2 with "Hauth Hf")
      as %[Hfoo _]%auth_valid_discrete.
    iPureIntro. revert Hfoo. simpl. rewrite left_id.
    rewrite lookup_included. intros Hffp.
    exists (fp  f). rewrite Heq /all_props. revert Hffp.
    simple refine (map_ind (fun f => ( i, _)  _  _) _ _ f); simpl.
    - (* TODO: this should be somewhere in std++ *)
      assert (fp   = fp) as ->.
      { apply map_eq=>i. remember (fp !! i) as XX. destruct XX.
        - apply lookup_difference_Some. eauto.
        - apply lookup_difference_None. eauto. }
      by rewrite bi.big_sepM_empty left_id.
    - intros i P f' Hi IH Hffp. rewrite IH; last first.
      { intros j. specialize (Hffp j).
        destruct (decide (i = j)) as [->|?].
        - rewrite /to_props_map !lookup_fmap Hi. simpl.
          apply option_included. eauto.
        - revert Hffp.
          rewrite /to_props_map !lookup_fmap lookup_insert_ne; auto. }
      rewrite bi.big_sepM_insert; last assumption.
      specialize (Hffp i). revert Hffp.
      rewrite /to_props_map !lookup_fmap lookup_insert; auto. simpl.
      rewrite option_included.
      intros [Hffp | [? [Q' [HP [HQ HeqQ]]]]]; first by inversion Hffp.
      simplify_eq/=. remember (fp !! i) as XX.
      destruct XX as [Q|]; simpl in HQ; last first.
      { inversion HQ. }
      simplify_eq/=.
      assert (P  Q) as HPQ.
      { by destruct HeqQ as [?%to_agree_inj |?%to_agree_included]. }
      clear HeqQ.
      assert (fp = <[i:=Q]>(delete i fp)) as ->.
      { by rewrite insert_delete insert_id. }
      assert (<[i:=Q]> (delete i fp)  f' = <[i:=Q]>((delete i fp)  f')) as ->.
      { apply map_eq=>j. destruct (decide (i = j)) as [->|?].
        - by rewrite lookup_insert lookup_difference_Some lookup_insert.
        - rewrite lookup_insert_ne; auto.
          unfold difference, map_difference; rewrite !lookup_difference_with.
          rewrite lookup_insert_ne; auto. }
      rewrite bi.big_sepM_insert; last first.
      { apply lookup_difference_None. left. apply lookup_delete. }
      assert ((<[i:=Q]> (delete i fp)  <[i:=P]> f') = (delete i fp  f')) as ->.
      { apply map_eq=>j. destruct (decide (i = j)) as [->|?].
        - unfold difference, map_difference; rewrite !lookup_difference_with.
            by rewrite !lookup_insert lookup_delete Hi.
        - unfold difference, map_difference; rewrite !lookup_difference_with.
          rewrite !lookup_insert_ne; auto. }
      iSplit; rewrite {1}HPQ. iIntros "($ & $ & $)".
      iIntros "[[$ $] $]".
  Qed.

  Lemma acquire_cancel_spec γ π lk R :
    {{{ is_flock γ lk  unflocked γ π  flock_res γ R }}}
      acquire lk
    {{{ f, RET #();  R  ( R - flocked γ π f) }}}.
  Proof.
    iIntros (Φ) "(Hl & Hunfl & #HRres) HΦ". rewrite -wp_fupd.
    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.
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown & >Hlocked2 & Hfp)".
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. rewrite left_id.
      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]".
      iDestruct (flock_res_auth with "HRres Hauth") as %Hfoo.
      destruct Hfoo as [f' Hf'].
      iMod ("Hcl" with "[Hstate Hcown Hlocked Hauth Hfactive]") as "_".
      { iNext. iExists (Locked π),,fa. rewrite left_id. iFrame.
        by rewrite /all_props bi.big_sepM_empty. }
      iModIntro. rewrite Hf'. iDestruct "Hfa" as "[HR Hf']".
      iApply ("HΦ" $! fa). iFrame.
      iApply bi.later_wand. iNext. iIntros "HR".
      rewrite Hf'. iFrame.
  Qed.

  (* TODO: derive this from acquire_cancel_spec *)
  Lemma acquire_single_cancel_spec γ π lk s R :
    {{{ is_flock γ lk  unflocked γ π  flock_res_single γ s R }}}
426
      acquire lk
427
    {{{ f, RET #();  R  ( R - flocked γ π f) }}}.
428
  Proof.
429
    iIntros (Φ) "(Hl & Hunfl & #HRres) HΦ". rewrite -wp_fupd.
430 431 432 433 434
    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.
435 436
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown & >Hlocked2 & Hfp)".
437
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
438 439
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. rewrite left_id.
440 441 442 443 444 445
      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]".
446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461
      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. }
Dan Frumin's avatar
Dan Frumin committed
462
      iModIntro.
463 464
      iApply ("HΦ" $! fa). rewrite -HReq. iFrame.
      by iApply bi.later_wand.
465
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
466

467 468
  Lemma release_cancel_spec γ π lk f :
    {{{ is_flock γ lk  flocked γ π f }}}
469 470 471
      release lk
    {{{ RET #(); unflocked γ π }}}.
  Proof.
472
    iIntros (Φ) "(Hl & (Hstate' & Hflkd & Hactive & Hf)) HΦ". rewrite -fupd_wp.
473 474 475
    rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iMod (cinv_open with "Hcinv Hflkd") as "(Hstate & Hunfl & Hcl)"; first done.
    rewrite {2}/flock_inv.
476 477
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)"; last first.
    - iDestruct "Hrest" as "(>Hactive2 & Hfa & >%)".
478 479 480 481 482 483
      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.
484
    - iDestruct "Hrest" as "(>Hcown & >Hlocked & Hfp)".
485 486 487 488 489 490 491 492 493 494 495 496
      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']".
497 498 499 500 501 502 503 504 505 506 507 508 509 510
      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. }
511 512
      iApply (release_spec with "[$Hlk $Hlocked $Hstate']").
      iModIntro. iNext. iIntros "_". iApply "HΦ".
513
      rewrite /unflocked. by iSplitL "Hcown".
514
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
515

Dan Frumin's avatar
Dan Frumin committed
516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535
  Lemma cancel_lock γ lk R :
    is_flock γ lk - flock_res γ R - unflocked γ 1 ={}=  R.
  Proof.
    rewrite /is_flock /unflocked.
    iDestruct 1 as "(#Hcinv & #Hislock)".
    iIntros "#Hres Hcown".
    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; eauto.
    iIntros "[Hcown Hstate]".
    iDestruct "Hstate" as ([q|] fp fa) "(Hstate & >Hauth & Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown2 & >Hlocked & Hfp)".
      iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. iFrame. rewrite left_id.
      iDestruct (flock_res_auth with "Hres Hauth") as %Hfoo.
      destruct Hfoo as [f' Hf'].
      iModIntro. rewrite Hf'. iDestruct "Hfa" as "[$ ?]".
  Qed.

  Lemma cancel_lock_single γ lk s R :
    is_flock γ lk - flock_res_single γ s R - unflocked γ 1 ={}=  R.
536 537
  Proof.
    rewrite /is_flock /unflocked.
538 539
    iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "#Hres Hcown".
    rewrite /flock_res.
540
    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; eauto.
541
    iIntros "[Hcown Hstate]".
542 543
    iDestruct "Hstate" as ([q|] fp fa) "(Hstate & >Hauth & Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown2 & >Hlocked & Hfp)".
544
      iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561
    - 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.
562
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
563
End flock.