flock.v 28.7 KB
Newer Older
Léon Gondelman's avatar
Léon Gondelman committed
1
From iris.heap_lang Require Export proofmode notation.
Dan Frumin's avatar
Dan Frumin committed
2
From iris.heap_lang Require Import spin_lock.
3
From iris.base_logic.lib Require Import cancelable_invariants auth saved_prop.
Dan Frumin's avatar
Dan Frumin committed
4
From iris.algebra Require Import auth agree excl frac gmap gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
From iris.bi.lib Require Import fractional.
Léon Gondelman's avatar
Léon Gondelman committed
6

7
Inductive lockstate :=
Dan Frumin's avatar
Dan Frumin committed
8
  | Locked
9 10 11
  | Unlocked.
Canonical Structure lockstateC := leibnizC lockstate.

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

Dan Frumin's avatar
Dan Frumin committed
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
(** We need to be able to allocate resources into the lock even when
    it is in use -- for that we need to have /active/ and /pending/
    propositions. If the lock is unlocked (not acquired), then all the
    propositions are active (can be acquired); if the lock is locked
    (acquired), then some thread has the ownership of the active
    propositions, but any other thread can add a pending proposition.
    Pending propositions are thus always held by the lock.

    When a thread acquires the lock, it gets all the active
    propositions. For the whole construction to make sense, the thread
    should return exactly the same propositions once it releases the
    lock. For this to work we need to ensure that the set of active
    proposition has not changed since the lock has been acquired.
    Thus, we use ghost state to track the exact content of the set of
    active propositions.

    If we have a full access to the resource (with fraction 1), we may
    want to cancel it and get the proposition back. In order to do
    that we need to make sure that if we have the full fraction for
    accessing the resource, then this resource cannot be active. For
    that purpose we also need to store the information about the
    fractional permissions for the active propositions.

    Finally, the actual propositional content of the resources is
    shared via cancellable invariants. Each proposition (active or
    pending) is stored in a cancellable invariant associated with it:
Dan Frumin's avatar
Dan Frumin committed
40

Dan Frumin's avatar
Dan Frumin committed
41 42 43 44 45
        C(X) = X.prop ∗ X.token₁ ∨ X.token₂

    The exclusive tokens allow the thread to take out the proposition
    for the whole duration of the critical section. *)

46
Record flock_name := {
Dan Frumin's avatar
Dan Frumin committed
47
  (** ghost name for the actual spin lock invariant *)
Dan Frumin's avatar
Dan Frumin committed
48
  flock_lock_name : gname;
Dan Frumin's avatar
Dan Frumin committed
49
  (** -//- for keeping the track of the state of the flock *)
50
  flock_state_name : gname;
Dan Frumin's avatar
Dan Frumin committed
51
  (** -//- for keeping track of all propositions in the flock *)
52
  flock_props_name : gname;
53 54
  (** -//- for keeping track of the "active" propositions.
      Once you relase the lock you need to know that the set of the active propositions
Dan Frumin's avatar
Dan Frumin committed
55
      has not changed since you have acquired it *)
56
  flock_props_active_name : gname
57 58
}.

59
(** The data about pending and active propositions will be stored in
Dan Frumin's avatar
Dan Frumin committed
60
the maps `lock_res_gname -> frac` *)
61

62 63 64 65
(** One of the tricks in this lock is to store only ghost names associated with a 'flock resource' in the flock invariant.
    If we start storing propositions, then we end up in the LATER HELL.
    The `lock_res_name` datastructure contains all the ghosts names needed to manage an individual proposition.
 *)
Dan Frumin's avatar
Dan Frumin committed
66
Record lock_res_gname := {
Dan Frumin's avatar
Dan Frumin committed
67 68 69
  flock_cinv_name : gname;
  flock_token1_name : gname;
  flock_token2_name : gname;
Dan Frumin's avatar
Dan Frumin committed
70
}.
Dan Frumin's avatar
Dan Frumin committed
71 72 73 74 75 76 77 78 79 80 81
Canonical Structure lock_res_gnameC := leibnizC lock_res_gname.

Instance lock_res_gname_eq_dec : EqDecision lock_res_gname.
Proof. solve_decision. Defined.
Instance lock_res_gname_countable : Countable lock_res_gname.
Proof.
  apply inj_countable' with
      (f:=(λ x, (flock_cinv_name x, flock_token1_name x, flock_token2_name x)))
      (g:=(λ '(γ1,γ2,γ3), Build_lock_res_gname γ1 γ2 γ3)).
  intros []. reflexivity.
Defined.
82 83 84 85 86 87 88

(** Before we define the type of flock resources, we need to have
    access to the appropriate CMRAs.

   The totality of propositions , and the pending propositions will be
   represented as a map:

Dan Frumin's avatar
Dan Frumin committed
89
   `lock_res_gname → frac`,
90 91 92

   so a standart ghost heap. Active propositions will be modelled by a map

Dan Frumin's avatar
Dan Frumin committed
93
   `excl (lock_res_name → frac)`.
94 95 96 97

   In other words, this map will contain *exact* information of which propositions are active and with what fractions were they activated.

 *)
98 99 100
Class flockG Σ :=
  FlockG {
    flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
101
    flock_lockG  :> lockG Σ;
Dan Frumin's avatar
Dan Frumin committed
102 103
    flock_cinvG  :> cinvG Σ;
    (* note the difference between the two RAs here ! *)
Dan Frumin's avatar
Dan Frumin committed
104 105 106 107
    flock_props_active :> inG Σ (authR
        (optionUR (exclR (gmapC lock_res_gname fracR))));
    flock_props :> inG Σ (authR
        (gmapUR lock_res_gname fracR));
Dan Frumin's avatar
Dan Frumin committed
108
    flock_tokens :> inG Σ (exclR unitC);
109 110
  }.

111 112 113 114
Definition flockΣ : gFunctors :=
  #[GFunctor (authR (optionUR (exclR lockstateC)))
   ;lockΣ
   ;cinvΣ
Dan Frumin's avatar
Dan Frumin committed
115 116
   ;GFunctor (authR (optionUR (exclR (gmapC lock_res_gname fracC))))
   ;GFunctor (authR (gmapUR lock_res_gname fracR))%CF].
117 118 119 120

Instance subG_flockΣ Σ : subG flockΣ Σ  flockG Σ.
Proof. solve_inG. Qed.

Léon Gondelman's avatar
Léon Gondelman committed
121
Section flock.
122 123
  Context `{heapG Σ, flockG Σ}.
  Variable N : namespace.
Dan Frumin's avatar
Dan Frumin committed
124 125 126 127 128
  Definition invN := N.@"flock_inv".
  Definition lockN := N.@"flock_lock".
  Definition resN := N.@"flock_res".

  (** * Definitions **)
Dan Frumin's avatar
Dan Frumin committed
129 130 131 132
  Definition token (γ : lock_res_gname) : iProp Σ :=
    own (flock_token1_name γ) (Excl ()).
  Definition token (γ : lock_res_gname) : iProp Σ :=
    own (flock_token2_name γ) (Excl ()).
Dan Frumin's avatar
Dan Frumin committed
133

Dan Frumin's avatar
Dan Frumin committed
134
  Definition C (R : iProp Σ) (ρ : lock_res_gname) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
135 136
    (R  token ρ  token ρ)%I.

137
  (** Tokens that allow you to get all the propositions from `A` out of the invariants *)
Dan Frumin's avatar
Dan Frumin committed
138 139
  Definition all_tokens (P : gmap lock_res_gname ()) : iProp Σ :=
    ([ map] ρ  _  P, token ρ)%I.
Dan Frumin's avatar
Dan Frumin committed
140

Dan Frumin's avatar
Dan Frumin committed
141
  (** For active propositions we also need to know the fraction which was used to access it *)
Dan Frumin's avatar
Dan Frumin committed
142 143
  Definition from_active (A : gmap lock_res_gname frac)
    := fmap (const ()) A.
Dan Frumin's avatar
Dan Frumin committed
144

145

Dan Frumin's avatar
Dan Frumin committed
146 147 148
  (** A flock resource `(ρ,X,π)` contains:
      - Knowledge that the `ρ ↦ π` is in the set of propositions managed by the flock;
      - There is a cancellable invariant `C X ρ`;
149 150
      - We have π- permissiones to access that invariant.
   *)
Dan Frumin's avatar
Dan Frumin committed
151 152 153 154 155 156 157 158 159 160 161 162
  Definition N_of_ρ (ρ : lock_res_gname) :=
    (flock_token1_name ρ, flock_token2_name ρ).
  (* When creating a new invariant we need to pick a name that depends
  _only_ on the ghost names of the tokens. We cannot depend on the
  ghost name for the cancellable invariant, because that would be
  circular. I mean we potentially can but that would be annoying. *)
  Definition flock_res (γ : flock_name) (ρ : lock_res_gname)
             (π : frac)
             (P : iProp Σ) : iProp Σ :=
    (own (flock_props_name γ) ( {[ρ := π]})
     cinv (resN.@(N_of_ρ ρ)) (flock_cinv_name ρ) (C P ρ)
     cinv_own (flock_cinv_name ρ) π)%I.
163

164 165 166 167 168
  (** Basically says that the propositions from the map `A` are active.
      This predicate is designed to contain enough information to deactivate those propositions.

      When we are deactivating the propositions we need to make sure that the set of the active propositions has not changed. That's why we need a CMRA to keep track of the exact contents of that set.
 *)
Dan Frumin's avatar
Dan Frumin committed
169
  Definition flocked
Dan Frumin's avatar
Dan Frumin committed
170 171
    (γ : flock_name) (A : gmap lock_res_gname (frac*iProp Σ)) : iProp Σ :=
    (let fa := fmap fst A : gmap lock_res_gname frac in
Dan Frumin's avatar
Dan Frumin committed
172
       (* Information we retain: the flock is locked .. *)
Dan Frumin's avatar
Dan Frumin committed
173
         own (flock_state_name γ) ( (Excl' Locked))
Dan Frumin's avatar
Dan Frumin committed
174 175 176
       (* What are the exact propositions that we have activated.. *)
        own (flock_props_active_name γ) ( (Excl' fa))
       (* Tokens and permissions for closing the active propositions .. *)
Dan Frumin's avatar
Dan Frumin committed
177 178 179
        ([ map] ρ  πR  A, token ρ
                   cinv (resN.@(N_of_ρ ρ)) (flock_cinv_name ρ) (C πR.2 ρ)
                   cinv_own (flock_cinv_name ρ) πR.1))%I.
Dan Frumin's avatar
Dan Frumin committed
180

Dan Frumin's avatar
Dan Frumin committed
181 182 183
  Definition to_props_map (f : gmap lock_res_gname ())
    : gmapUR lock_res_gname fracR :=
    fmap (const 1%Qp) f.
Dan Frumin's avatar
Dan Frumin committed
184 185

  Definition flock_inv (γ : flock_name) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
186 187
    ( (s : lockstate)
       (** fa -- active propositions, fp -- pending propositions *)
Dan Frumin's avatar
Dan Frumin committed
188 189
       (fa : gmap lock_res_gname frac)
       (fp : gmap lock_res_gname unit), (** aka mapset lock_res_name *)
190
       (** ... and those sets are disjoint *)
Dan Frumin's avatar
Dan Frumin committed
191
       fp ## from_active fa 
Dan Frumin's avatar
Dan Frumin committed
192
       own (flock_state_name γ) ( (Excl' s)) 
193
       (** the totality of resources: fp ∪ fa *)
Dan Frumin's avatar
Dan Frumin committed
194
       own (flock_props_name γ) ( to_props_map (fp  from_active fa)) 
195
       (** but we also need to know the exact contents of fa *)
Dan Frumin's avatar
Dan Frumin committed
196
       own (flock_props_active_name γ) ( Excl' fa) 
197 198 199 200
       (** the invariant keeps track of the tokens (token₂) for the
           pending resource; when we activate a resource, we transfer
           this token to the client, which uses it to open the
           cinvariant and get the actual proposition. *)
Dan Frumin's avatar
Dan Frumin committed
201
       all_tokens fp 
Dan Frumin's avatar
Dan Frumin committed
202
       match s with
Dan Frumin's avatar
Dan Frumin committed
203
       | Locked =>
204
         (** If the lock is acuired, then we hold on to the token from the "old" specification *)
Dan Frumin's avatar
Dan Frumin committed
205
         locked (flock_lock_name γ) 
206 207 208
         (** .. and we take hold of all the ghost pointsto `s ↦{π} ρ`.

             This is necessary to have if we want to free the
Dan Frumin's avatar
Dan Frumin committed
209
             resources. If we wish to free the resource `ρ ↦ 1`,
210 211
             then we need to know that it is not currently active (has
             not been acquired). The predicate below ensures that. *)
Dan Frumin's avatar
Dan Frumin committed
212
         own (flock_props_name γ) ( fa)
Dan Frumin's avatar
Dan Frumin committed
213
       | Unlocked =>
214 215
         (** If the lock is NOT acquired, then there are no active
         proposition *)
Dan Frumin's avatar
Dan Frumin committed
216
         own (flock_props_active_name γ) ( Excl' )
Dan Frumin's avatar
Dan Frumin committed
217 218 219
       end)%I.

  Definition is_flock (γ : flock_name) (lk : val) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
220 221
    (inv invN (flock_inv γ) 
     is_lock lockN (flock_lock_name γ) lk
Dan Frumin's avatar
Dan Frumin committed
222 223
         (own (flock_state_name γ) ( (Excl' Unlocked))))%I.

Dan Frumin's avatar
Dan Frumin committed
224 225 226
  (** * Lemmata **)

  (** ** Basic properties of the CAPs *)
Dan Frumin's avatar
Dan Frumin committed
227 228 229
  Lemma flock_res_op (γ : flock_name) (ρ : lock_res_gname) (R : iProp Σ) (π1 π2 : frac) :
    flock_res γ ρ (π1+π2) R
  flock_res γ ρ π1 R  flock_res γ ρ π2 R.
230 231 232 233 234 235 236 237 238 239 240 241 242
  Proof.
    rewrite /flock_res. iSplit.
    - iDestruct 1 as "(Hs & #Hinv & Hρ)".
      iDestruct "Hρ" as "[Hρ1 Hρ2]".
      iDestruct "Hs" as "[Hs1 Hs2]".
      iSplitL "Hρ1 Hs1"; by iFrame.
    - iIntros "[H1 H2]".
      iDestruct "H1" as "(Hs1 & #Hinv1 & Hρ1)".
      iDestruct "H2" as "(Hs2 & #Hinv2 & Hρ2)".
      iCombine "Hs1 Hs2" as "Hs". iFrame.
      rewrite /C /=. iFrame "Hinv1".
  Qed.

Dan Frumin's avatar
Dan Frumin committed
243 244
  Global Instance flock_res_fractional γ i R :
    Fractional (λ π, flock_res γ i π R).
245 246
  Proof. intros p q. apply flock_res_op. Qed.

Dan Frumin's avatar
Dan Frumin committed
247 248 249
  Global Instance flock_res_as_fractional γ i R π :
    AsFractional (flock_res γ i π R)
                 (λ π, flock_res γ i π R) π.
250
  Proof. split. done. apply _. Qed.
Dan Frumin's avatar
Dan Frumin committed
251

Dan Frumin's avatar
Dan Frumin committed
252 253
  Lemma to_props_map_singleton_included fp q ρ:
    {[ρ := q]}  to_props_map fp  fp !! ρ = Some ().
254
  Proof.
Dan Frumin's avatar
Dan Frumin committed
255
    rewrite singleton_included=> -[[q' av] []].
Dan Frumin's avatar
Dan Frumin committed
256 257
    rewrite /to_props_map lookup_fmap fmap_Some_equiv.
    move=> -[[] [Hρ _]]//.
258 259
  Qed.

Dan Frumin's avatar
Dan Frumin committed
260 261 262
  Lemma to_props_map_delete fp i:
    delete i (to_props_map fp) = to_props_map (delete i fp).
  Proof.
Dan Frumin's avatar
Dan Frumin committed
263
    by rewrite /to_props_map fmap_delete.
Dan Frumin's avatar
Dan Frumin committed
264
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
265

Dan Frumin's avatar
Dan Frumin committed
266 267
  (** ** Spectral operations *)

Dan Frumin's avatar
Dan Frumin committed
268
  Lemma flock_res_alloc_strong (X : gset lock_res_gname) γ lk R E :
Dan Frumin's avatar
Dan Frumin committed
269 270
    N  E 
    is_flock γ lk -
Dan Frumin's avatar
Dan Frumin committed
271
     R ={E}=  ρ, ⌜ρ  X  flock_res γ ρ 1 R.
272
  Proof.
Dan Frumin's avatar
Dan Frumin committed
273 274 275 276 277 278 279 280
    iIntros (?) "Hl HR". rewrite /is_flock.
    iDestruct "Hl" as "(#Hfl & #Hlk)".

    (* Pick a fresh name *)
    iInv invN as (s fa fp)
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl".

    (* Alloc all the data for the resource *)
Dan Frumin's avatar
Dan Frumin committed
281 282 283 284 285 286 287 288 289 290 291
    (* We need to guarantee that the new name
       - is not in the set X,
       - does not clash with the existing names in the invariant *)
    set (X := collection_map flock_token1_name
                              X : gset gname).
    set (X := collection_map flock_token2_name
                              (dom (gset lock_res_gname) (fp  from_active fa)) : gset gname).

    iMod (own_alloc_strong (Excl ()) X) as (γt Ht) "T1"; first done.
    iMod (own_alloc_strong (Excl ()) X) as (γt Ht) "T2"; first done.
    iMod (cinv_alloc _ (resN.@(γt,γt)) (R  own γt (Excl ())  own γt (Excl ()))%I with "[HR T1]") as (γc) "[#HR Hρ]".
Dan Frumin's avatar
Dan Frumin committed
292
    { iNext. iLeft. by iFrame. }
Dan Frumin's avatar
Dan Frumin committed
293
    set (ρ :=
Dan Frumin's avatar
Dan Frumin committed
294 295 296 297 298
            {| flock_cinv_name := γc;
               flock_token1_name := γt;
               flock_token2_name := γt |}).
    (* Put it in the map of flock resources *)
    iMod (own_update  with "Haprops") as "Haprops".
Dan Frumin's avatar
Dan Frumin committed
299 300 301
    { eapply (auth_update_alloc _
              (to_props_map (<[ρ := ()]> fp  from_active fa))
              {[ ρ := 1%Qp ]}).
Dan Frumin's avatar
Dan Frumin committed
302 303 304
      rewrite -insert_union_l.
      rewrite /to_props_map /= fmap_insert.
      apply alloc_local_update; last done.
Dan Frumin's avatar
Dan Frumin committed
305 306 307 308 309
      apply (not_elem_of_dom (to_props_map (fp  from_active fa)) _ (D:=gset lock_res_gname)).
      rewrite /to_props_map dom_fmap.
      intros Hρ. apply Ht.
      by apply (elem_of_map_2 flock_token2_name _ ρ).
    }
Dan Frumin's avatar
Dan Frumin committed
310 311
    iDestruct "Haprops" as "[Haprops Hi]".
    iMod ("Hcl" with "[-Hi Hρ]") as "_".
Dan Frumin's avatar
Dan Frumin committed
312
    { iNext. iExists s, fa,(<[ρ:=()]>fp).
Dan Frumin's avatar
Dan Frumin committed
313
      iFrame. rewrite /all_tokens big_sepM_insert; last first.
Dan Frumin's avatar
Dan Frumin committed
314 315 316 317
      { apply (not_elem_of_dom _ ρ (D:=gset lock_res_gname)).
        intros Hρ. apply Ht.
        apply (elem_of_map_2 flock_token2_name _ ρ).
        rewrite dom_union_L elem_of_union //. eauto. }
Dan Frumin's avatar
Dan Frumin committed
318 319
      iFrame. iPureIntro.
      apply map_disjoint_insert_l_2; eauto.
Dan Frumin's avatar
Dan Frumin committed
320 321 322 323 324 325 326 327
      eapply (not_elem_of_dom (D:=gset lock_res_gname)).
      intros Hi. apply Ht.
      apply (elem_of_map_2 flock_token2_name _ ρ).
      rewrite dom_union_L elem_of_union. eauto. }
    iModIntro; iExists ρ; iSplit; last by iFrame.
    iPureIntro.
    intros Hρ. apply Ht. unfold X.
    by apply (elem_of_map_2 flock_token1_name X ρ).
Dan Frumin's avatar
Dan Frumin committed
328 329
  Qed.

Dan Frumin's avatar
Dan Frumin committed
330
  Lemma flock_res_dealloc γ lk ρ R E :
Dan Frumin's avatar
Dan Frumin committed
331 332
    N  E 
    is_flock γ lk -
Dan Frumin's avatar
Dan Frumin committed
333
    flock_res γ ρ 1 R ={E}=  R.
Dan Frumin's avatar
Dan Frumin committed
334
  Proof.
Dan Frumin's avatar
Dan Frumin committed
335
    iIntros (?) "Hl HR". rewrite /is_flock.
Dan Frumin's avatar
Dan Frumin committed
336
    iDestruct "Hl" as "(#Hfl & #Hlk)".
Dan Frumin's avatar
Dan Frumin committed
337
    iDestruct "HR" as "(Hρ & #Hiinv & Hcinv)".
Dan Frumin's avatar
Dan Frumin committed
338 339 340 341 342

    iInv invN as ([|] fa fp)
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl".
    (* Locked *)
    - iDestruct "Hst" as ">[Hlocked Hactives]".
Dan Frumin's avatar
Dan Frumin committed
343 344
      (* We can now show that the proposition `ρ` is *not* active *)
      iDestruct (own_valid_2 with "Haprops Hρ")
Dan Frumin's avatar
Dan Frumin committed
345
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
346 347 348 349 350 351 352 353 354 355 356
      iAssert (fa !! ρ = None)%I with "[-]" as %Hbar.
      { remember (fa !! ρ) as faρ. destruct faρ as [π|]; last done.
        symmetry in Heqfaρ.
        iCombine "Hactives Hρ" as "H".
        iDestruct (own_valid with "H") as %Hbaz.
        exfalso. apply auth_own_valid in Hbaz. simpl in *.
        specialize (Hbaz ρ). revert Hbaz.
        rewrite lookup_op Heqfaρ lookup_singleton.
        rewrite -Some_op Some_valid.
        eapply exclusive_r ; eauto. apply _. }
      assert (fp !! ρ = Some ()) as Hbaz.
Dan Frumin's avatar
Dan Frumin committed
357 358
      { apply lookup_union_Some in Hfoo; last done.
        destruct Hfoo as [? | Hfoo]; first done.
Dan Frumin's avatar
Dan Frumin committed
359
        exfalso. revert Hfoo. by rewrite /from_active lookup_fmap Hbar.
Dan Frumin's avatar
Dan Frumin committed
360 361
      }

Dan Frumin's avatar
Dan Frumin committed
362 363 364
      iMod (own_update_2 with "Haprops Hρ") as "Haprops".
      { apply auth_update_dealloc, (delete_singleton_local_update _ ρ _). }
      rewrite /all_tokens (big_sepM_delete _ fp ρ) //.
Dan Frumin's avatar
Dan Frumin committed
365
      iDestruct "Htokens" as "[T2 Htokens]".
Dan Frumin's avatar
Dan Frumin committed
366
      iMod (cinv_cancel with "Hiinv Hcinv") as "HC". solve_ndisj.
Dan Frumin's avatar
Dan Frumin committed
367 368 369
      rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
      { iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
      iFrame "HR".
Dan Frumin's avatar
Dan Frumin committed
370

Dan Frumin's avatar
Dan Frumin committed
371 372
      (* Now that the resource is cancelled we close the flock invariant *)
      iApply "Hcl". iNext.
Dan Frumin's avatar
Dan Frumin committed
373
      iExists Locked,fa,(delete ρ fp). iFrame.
Dan Frumin's avatar
Dan Frumin committed
374
      iSplit.
375
      + iPureIntro. solve_map_disjoint.
Dan Frumin's avatar
Dan Frumin committed
376 377 378 379 380
      + rewrite to_props_map_delete delete_union.
        rewrite (delete_notin (from_active fa)) //.
        rewrite /from_active lookup_fmap Hbar //.
    (* Unlocked *)
    - iDestruct "Hst" as ">Hfactive".
Dan Frumin's avatar
Dan Frumin committed
381 382 383 384
      iAssert (fa = ∅⌝)%I with "[-]" as %->.
      { iDestruct (own_valid_2 with "Haactive Hfactive")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
        iPureIntro. by unfold_leibniz. }
Dan Frumin's avatar
Dan Frumin committed
385
      rewrite /from_active fmap_empty /= right_id.
Dan Frumin's avatar
Dan Frumin committed
386
      iDestruct (own_valid_2 with "Haprops Hρ")
Dan Frumin's avatar
Dan Frumin committed
387
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
388 389 390
      iMod (own_update_2 with "Haprops Hρ") as "Haprops".
      { apply auth_update_dealloc, (delete_singleton_local_update _ ρ _). }
      rewrite /all_tokens (big_sepM_delete _ fp ρ _) //.
Dan Frumin's avatar
Dan Frumin committed
391
      iDestruct "Htokens" as "[T2 Htokens]".
Dan Frumin's avatar
Dan Frumin committed
392
      iMod (cinv_cancel with "Hiinv Hcinv") as "HC". solve_ndisj.
Dan Frumin's avatar
Dan Frumin committed
393 394 395 396 397 398
      rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
      { iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
      iFrame "HR".

      (* Now that the resource is cancelled we close the flock invariant *)
      iApply "Hcl". iNext.
Dan Frumin's avatar
Dan Frumin committed
399
      iExists Unlocked,,(delete ρ fp). iFrame.
Dan Frumin's avatar
Dan Frumin committed
400
      iSplit.
401
      + iPureIntro. solve_map_disjoint.
Dan Frumin's avatar
Dan Frumin committed
402 403
      + rewrite /from_active fmap_empty /= right_id.
        by rewrite to_props_map_delete.
Dan Frumin's avatar
Dan Frumin committed
404
  Qed.
405

Dan Frumin's avatar
Dan Frumin committed
406
  (** `flocked` supports invariant access just like regular invariants *)
Dan Frumin's avatar
Dan Frumin committed
407
  Lemma flocked_inv_open_single E γ ρ πR I :
Dan Frumin's avatar
Dan Frumin committed
408
    resN  E 
Dan Frumin's avatar
Dan Frumin committed
409
    I !! ρ = Some πR 
Dan Frumin's avatar
Dan Frumin committed
410
    flocked γ I ={E}=
Dan Frumin's avatar
Dan Frumin committed
411
     πR.2  ( πR.2 ={E}= flocked γ I).
Dan Frumin's avatar
Dan Frumin committed
412
  Proof.
Dan Frumin's avatar
Dan Frumin committed
413 414 415 416
    destruct πR as [π R].
    iIntros (? Hρ). rewrite {1}/flocked.
    iIntros "(Hst & Hfa & Htokens)".
    rewrite (big_sepM_lookup_acc _ I ρ (π,R)) //.
Dan Frumin's avatar
Dan Frumin committed
417 418 419 420 421 422 423 424 425 426 427 428
    iDestruct "Htokens" as "[(T2 & #Hinv & Hρ) Htokens]".
    iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
    rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
    { iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
    iMod ("Hcl" with "[T2]") as "_".
    { iNext. iRight. done. }
    iModIntro. iFrame "HR". iIntros "HR".
    iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
    iDestruct "HC" as "[[? >T1'] | >T2]".
    { iDestruct (own_valid_2 with "T1 T1'") as %?. done. }
    iMod ("Hcl" with "[T1 HR]") as "_".
    { iNext. iLeft. iFrame. }
Dan Frumin's avatar
Dan Frumin committed
429 430
    iModIntro. rewrite /flocked.
    iFrame "Hst Hfa". iApply "Htokens". by iFrame.
Dan Frumin's avatar
Dan Frumin committed
431 432
  Qed.

Dan Frumin's avatar
Dan Frumin committed
433 434 435
  Lemma flocked_inv_open E γ I :
    resN  E 
    flocked γ I ={E}=
Dan Frumin's avatar
Dan Frumin committed
436 437
     ([ map] ρ  πR  I, πR.2) 
   ( ([ map] ρ  πR  I, πR.2) ={E}= flocked γ I).
Dan Frumin's avatar
Dan Frumin committed
438 439
  Proof.
    iIntros (?). rewrite {1}/flocked.
Dan Frumin's avatar
Dan Frumin committed
440
    iIntros "(Hst & Hfa & Htokens)".
Dan Frumin's avatar
Dan Frumin committed
441 442
    rewrite !big_sepM_sepM.
    iDestruct "Htokens" as "(T2s & Hinvs & Hρs)".
Dan Frumin's avatar
Dan Frumin committed
443 444 445
    rewrite /flocked.
    iFrame "Hst Hfa".
    iInduction I as [|ρ πR I Hs] "IH" using map_ind.
Dan Frumin's avatar
Dan Frumin committed
446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470
    - rewrite /flocked !big_sepM_empty. eauto with iFrame.
    - rewrite !big_sepM_insert //.
      iDestruct "T2s"   as "[T2 T2s]".
      iDestruct "Hinvs" as "[#Hinv Hinvs]".
      iDestruct "Hρs"   as "[Hρ Hρs]".
      iMod ("IH" with "T2s Hinvs Hρs") as "[$ IH']".
      iClear "IH".

      (* The main induction step *)
      iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
      rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
      { iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
      iMod ("Hcl" with "[T2]") as "_".
      { iNext. iRight. done. }
      iModIntro. iFrame "HR". iIntros "[HR HRs]".
      iMod ("IH'" with "HRs") as "$".

      iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
      iDestruct "HC" as "[[? >T1'] | >$]".
      { iDestruct (own_valid_2 with "T1 T1'") as %?. done. }
      iMod ("Hcl" with "[T1 HR]") as "_".
      { iNext. iLeft. iFrame. }
      iModIntro. by iFrame.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
471
  (** ** Physical operations *)
Dan Frumin's avatar
Dan Frumin committed
472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493
  Lemma newflock_spec :
    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
  Proof.
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
    iMod (own_alloc ( (Excl' Unlocked)   (Excl' Unlocked)))
      as (γ_state) "[Hauth Hfrag]"; first done.
    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 lockN (own γ_state ( (Excl' Unlocked))) with "Hfrag").
    iNext. iIntros (lk γ_lock) "#Hlock".
    pose (γ := (Build_flock_name γ_lock γ_state γ_props γ_ac_props)).
    iMod (inv_alloc invN _ (flock_inv γ) with "[-HΦ]") as "#Hinv".
    { iNext. iExists Unlocked, , . rewrite /from_active fmap_empty right_id. iFrame.
      iSplit; eauto. by rewrite /all_tokens big_sepM_empty. }
    iModIntro. iApply ("HΦ" $! lk γ with "[-]").
    rewrite /is_flock. by iFrame "Hlock".
  Qed.

Dan Frumin's avatar
Dan Frumin committed
494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535
  (** We need two additional lemmas, and they are annoying! *)
  Lemma big_sepM_own_frag {A B : Type} {C} `{EqDecision A, Countable A}
        `{inG Σ (authR (gmapUR A C))} (f : B  C) (m : gmap A B) (γ : gname) :
    own γ ( ) -
    own γ ( (f <$> m)) - [ map] ix  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.

  Lemma own_frag_empty γ X :
    own (flock_props_name γ) ( X) ==
    own (flock_props_name γ) ( X)  own (flock_props_name γ) ( ).
  Proof.
    iIntros "H". rewrite -own_op.
    iApply (own_update with "H").
    by apply auth_update_alloc.
  Qed.


Dan Frumin's avatar
Dan Frumin committed
536 537
  Lemma release_cancel_spec γ lk I :
    {{{ is_flock γ lk  flocked γ I }}}
538
      release lk
Dan Frumin's avatar
Dan Frumin committed
539
    {{{ RET #(); [ map] ρ  πR  I, flock_res γ ρ πR.1 πR.2 }}}.
540
  Proof.
Dan Frumin's avatar
Dan Frumin committed
541
    iIntros (Φ) "(#Hl & H) HΦ". rewrite -fupd_wp.
Dan Frumin's avatar
Dan Frumin committed
542
    rewrite /is_flock. iDestruct "Hl" as "(#Hinv & #Hlk)".
Dan Frumin's avatar
Dan Frumin committed
543

Dan Frumin's avatar
Dan Frumin committed
544
    rewrite {1}/flocked /=.
Dan Frumin's avatar
Dan Frumin committed
545
    iDestruct "H" as "(Hflkd & Hfactive & Hfa)".
Dan Frumin's avatar
Dan Frumin committed
546 547 548
    do 2 rewrite big_sepM_sepM.
    iDestruct "Hfa" as "(HT2s & #Hinvs & Hρs)".

Dan Frumin's avatar
Dan Frumin committed
549 550 551
    iInv invN as ([|] fa fp)
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl";
      last first.
Dan Frumin's avatar
Dan Frumin committed
552 553 554
    - iDestruct (own_valid_2 with "Hstate Hflkd")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
      fold_leibniz. inversion Hfoo.
Dan Frumin's avatar
Dan Frumin committed
555
    - iDestruct "Hst" as ">[Hlocked Hactives]".
Dan Frumin's avatar
Dan Frumin committed
556 557 558 559 560 561
      iDestruct (own_valid_2 with "Haactive Hfactive")
        as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
      fold_leibniz. simplify_eq/=.

      (* Locked ~~> Unlocked *)
      iMod (own_update_2 with "Hstate Hflkd") as "Hstate".
562 563 564
      { apply (auth_update _ _ (Excl' Unlocked) (Excl' Unlocked)).
        apply option_local_update.
        by apply exclusive_local_update. }
Dan Frumin's avatar
Dan Frumin committed
565
      iDestruct "Hstate" as "[Hstate Hunflkd]".
Léon Gondelman's avatar
Léon Gondelman committed
566

Dan Frumin's avatar
Dan Frumin committed
567 568 569 570 571 572 573
      (* Empty up the set of active propositions *)
      iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
      { apply (auth_update _ _ (Excl' )
                               (Excl' )).
        by apply option_local_update, exclusive_local_update. }


Dan Frumin's avatar
Dan Frumin committed
574 575 576 577
      pose (fa := fst <$> I).
      iMod (own_frag_empty with "Haprops") as "[Haprops Hemp]".
      (* You may wonder, why the hell do we need this useless Hemp proposition? .. Well you will find out towards the end of the proof *)
      iMod ("Hcl" with "[-HΦ Hlocked Hactives Hunflkd Hρs Hemp]") as "_".
Dan Frumin's avatar
Dan Frumin committed
578
      { iNext. iExists Unlocked,,(fp  from_active fa).
Dan Frumin's avatar
Dan Frumin committed
579 580
        iSplitR; eauto.
        - rewrite /from_active fmap_empty. iPureIntro.
581
          solve_map_disjoint.
Dan Frumin's avatar
Dan Frumin committed
582
        - iFrame. rewrite /from_active fmap_empty right_id /=.
Dan Frumin's avatar
Dan Frumin committed
583 584 585 586
          iFrame "Haprops".
          rewrite /all_tokens.
          rewrite big_sepM_union // -map_fmap_compose.
          rewrite big_sepM_fmap. by iFrame. }
Dan Frumin's avatar
Dan Frumin committed
587
      iApply (release_spec with "[$Hlk $Hlocked $Hunflkd]").
Dan Frumin's avatar
Dan Frumin committed
588
      iModIntro. iNext. iIntros "_". iApply "HΦ".
Dan Frumin's avatar
Dan Frumin committed
589 590
      rewrite /flock_res !big_sepM_sepM.
      iFrame "Hρs Hinvs".
Dan Frumin's avatar
Dan Frumin committed
591
      by iApply (big_sepM_own_frag with "Hemp").
Dan Frumin's avatar
Dan Frumin committed
592
  Qed.
Dan Frumin's avatar
Dan Frumin committed
593

Dan Frumin's avatar
Dan Frumin committed
594

Dan Frumin's avatar
Dan Frumin committed
595 596 597
  Lemma acquire_flock_spec γ lk
        (I : gmap lock_res_gname (frac*iProp Σ)) :
    {{{ is_flock γ lk  [ map] ρ  πR  I, flock_res γ ρ πR.1 πR.2 }}}
Dan Frumin's avatar
Dan Frumin committed
598
      acquire lk
599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627
    {{{ RET #(); flocked γ I }}}.
  Proof.
    iIntros (Φ) "(Hl & HRres) HΦ".
    rewrite /is_flock. iDestruct "Hl" as "(#Hfl & #Hlk)".
    iApply wp_fupd.
    iApply (acquire_spec with "Hlk").
    iNext. iIntros "[Hlocked Hunlk]".
    iInv invN as ([|] fa fp)
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl".
    - iDestruct "Hst" as "(>Hlocked2 & ?)".
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
    - iDestruct "Hst" as ">Hfactive".
      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 fmap_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]".

      iApply "HΦ". rewrite /flocked.
      iFrame "Hflkd".

      (* Designate the propositions from I as active *)
Dan Frumin's avatar
Dan Frumin committed
628
      pose (fa := fst <$> I).
629 630 631 632 633 634 635 636 637 638 639 640 641 642
      iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
      { apply (auth_update _ _ (Excl' fa)
                               (Excl' fa)).
        by apply option_local_update, exclusive_local_update. }
      iFrame "Hfactive".

      rewrite /flock_res. rewrite !big_sepM_sepM.
      iDestruct "HRres" as "(HI & #Hinvs & Hρs)".
      iFrame "Hinvs Hρs".

      (* this is going to be annoying .. *)
      (* show that I ⊆ fp, or, better fp = fp' ∪ I *)

      (* first obtain the empty fragment for big_sepM_own_frag *)
Dan Frumin's avatar
Dan Frumin committed
643 644
      iMod (own_frag_empty with "Haprops") as "[Haprops #Hemp]".

Dan Frumin's avatar
Dan Frumin committed
645
      iAssert (own (flock_props_name γ) ( fa))
646 647 648 649 650 651 652
        with "[HI Hemp]" as "HI".
      { by iApply (big_sepM_own_frag with "Hemp"). }

      (* I' ≼ fp *)
      iDestruct (own_valid_2 with "Haprops HI")
        as %[Hfoo _]%auth_valid_discrete_2.

Dan Frumin's avatar
Dan Frumin committed
653
      (* TODO: RK, can this proof script be simplified? The idea is not complicated. *)
Dan Frumin's avatar
Dan Frumin committed
654
      (* We are going to separate the active resources I out of the fp map *)
Dan Frumin's avatar
Dan Frumin committed
655 656 657
      pose (I'' := fmap (const ()) I).
      assert (I''  fp).
      { subst I'' fa.
Dan Frumin's avatar
Dan Frumin committed
658
        unfold to_props_map in *.
Dan Frumin's avatar
Dan Frumin committed
659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688
        pose (f := fst : frac*(iProp Σ)  frac).
        pose (g := const 1%Qp : ()  frac).
        assert (const () <$> (f <$> I) 
                (const () <$> (g <$> fp) : gmapUR lock_res_gname unitR)) as Hbar.
        { by apply gmap_fmap_mono. }

        move: Hbar. rewrite -!map_fmap_compose=>Hbar.
        (* TODO: WHY can't I do
           apply (lookup_included (fst <$> I) (const 1%Qp <$> fp))
           in Hbar *)
        assert ( x, (const ()  f <$> I) !! x  (const ()  g <$> fp) !! x) as Hbaz.
        { by apply lookup_included. }
        apply map_subseteq_spec.
        intros ρ []. specialize (Hbaz ρ).
        revert Hbaz. rewrite !lookup_fmap.
        intros Hbaz Hρ. rewrite Hρ in Hbaz.
        destruct (fp !! ρ) as [[]|] eqn:Hfp; auto.
        simpl in Hbaz. exfalso.
        destruct Hbaz as [[[]|] Hbaz];
          fold_leibniz; inversion Hbaz. }

      pose (P' := fp  I'').

      assert (I'' ## P').
      { by apply map_disjoint_difference_r. }

      assert (fp = P'  I'') as HP'.
      { symmetry. rewrite map_union_comm//.
        by apply map_difference_union. }
      rewrite HP'.
Dan Frumin's avatar
Dan Frumin committed
689

690 691 692 693 694
      rewrite /all_tokens big_sepM_union //.
      iDestruct "Htokens" as "[Htokens H]".
      rewrite /I'' big_sepM_fmap. iFrame.
      iApply "Hcl".
      iNext. iExists Locked, fa, P'.
Dan Frumin's avatar
Dan Frumin committed
695 696 697
      assert (I'' = from_active fa) as <-.
      { by rewrite /from_active -map_fmap_compose. }
      eauto with iFrame.
Dan Frumin's avatar
Dan Frumin committed
698
  Qed.
699

Léon Gondelman's avatar
Léon Gondelman committed
700
End flock.