flock.v 31.1 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 60 61
(** The data about pending and active propositions will be stored in
the maps `prop_id -> _` *)
(* `prop_id` is fefined as `positive` so that we have a `Fresh` instance for `gset positive`.
Dan Frumin's avatar
Dan Frumin committed
62
   Doubles as an invariant name. *)
63
Definition prop_id := positive.
Dan Frumin's avatar
Dan Frumin committed
64
Canonical Structure gnameC := leibnizC gname.
65

66 67 68 69
(** 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
70 71 72 73
Record lock_res_name := {
  flock_cinv_name : gname;
  flock_token1_name : gname;
  flock_token2_name : gname;
Dan Frumin's avatar
Dan Frumin committed
74
}.
Dan Frumin's avatar
Dan Frumin committed
75
Canonical Structure lock_res_nameC := leibnizC lock_res_name.
76

77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92

(** 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:

   `prop_id → frac * ag (flock_res_name)`,

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

   `excl (prop_id → frac * ag (flock_res_name))`.

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

 *)
93 94 95
Class flockG Σ :=
  FlockG {
    flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
96
    flock_lockG  :> lockG Σ;
Dan Frumin's avatar
Dan Frumin committed
97 98 99 100 101
    flock_cinvG  :> cinvG Σ;
    (* note the difference between the two RAs here ! *)
    flock_props_active :> inG Σ (authR (optionUR (exclR (gmapC prop_id (prodC fracC lock_res_nameC)))));
    flock_props :> inG Σ (authR (gmapUR prop_id (prodR fracR (agreeR lock_res_nameC))));
    flock_tokens :> inG Σ (exclR unitC);
102 103
  }.

104 105 106 107 108 109 110 111 112 113
Definition flockΣ : gFunctors :=
  #[GFunctor (authR (optionUR (exclR lockstateC)))
   ;lockΣ
   ;cinvΣ
   ;GFunctor (authR (optionUR (exclR (gmapC prop_id (prodC fracC lock_res_nameC)))))
   ;GFunctor (authR (gmapUR prop_id (prodR fracR (agreeR lock_res_nameC))))%CF].

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

Dan Frumin's avatar
Dan Frumin committed
114 115 116 117 118 119
Record lock_res `{flockG Σ} := {
  res_prop : iProp Σ;
  res_frac : frac;
  res_name : lock_res_name;
}.

120
(** A "smart constructor" for `lock_res` *)
Dan Frumin's avatar
Dan Frumin committed
121 122
Definition LockRes `{flockG Σ} (R : iProp Σ) (π : frac) (ρ : lock_res_name) :=
  {| res_prop := R; res_frac := π; res_name := ρ |}.
123

Léon Gondelman's avatar
Léon Gondelman committed
124
Section flock.
125 126
  Context `{heapG Σ, flockG Σ}.
  Variable N : namespace.
Dan Frumin's avatar
Dan Frumin committed
127 128 129 130 131 132 133 134 135 136 137 138 139
  Definition invN := N.@"flock_inv".
  Definition lockN := N.@"flock_lock".
  Definition resN := N.@"flock_res".

  (** * Definitions **)
  Definition token (ρ : lock_res_name) : iProp Σ :=
    own (flock_token1_name ρ) (Excl ()).
  Definition token (ρ : lock_res_name) : iProp Σ :=
    own (flock_token2_name ρ) (Excl ()).

  Definition C (R : iProp Σ) (ρ : lock_res_name) : iProp Σ :=
    (R  token ρ  token ρ)%I.

140
  (** Tokens that allow you to get all the propositions from `A` out of the invariants *)
Dan Frumin's avatar
Dan Frumin committed
141 142
  Definition all_tokens (P : gmap prop_id lock_res_name) : iProp Σ :=
    ([ map] i  X  P, token X)%I.
Dan Frumin's avatar
Dan Frumin committed
143

Dan Frumin's avatar
Dan Frumin committed
144 145 146
  (** For active propositions we also need to know the fraction which was used to access it *)
  Definition from_active (A : gmap prop_id (frac * lock_res_name))
    := fmap snd A.
Dan Frumin's avatar
Dan Frumin committed
147

148 149 150 151 152 153

  (** A flock resource `s ↦ X,π,γ` contains:
      - Knowledge that the `s ↦{π} γ` is in the set of propositions managed by the flock;
      - There is a cancellable invariant `C X γ`;
      - We have π- permissiones to access that invariant.
   *)
Dan Frumin's avatar
Dan Frumin committed
154 155 156 157
  Definition flock_res (γ : flock_name) (s : prop_id) (X : lock_res) : iProp Σ :=
    (own (flock_props_name γ) ( {[s := (res_frac X, to_agree (res_name X))]})
     cinv (resN.@s) (flock_cinv_name (res_name X)) (C (res_prop X) (res_name X))
     cinv_own (flock_cinv_name (res_name X)) (res_frac X))%I.
158

159 160 161 162 163
  (** 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
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
  Definition flocked
    (γ : flock_name) (A : gmap prop_id lock_res) : iProp Σ :=
    ( fa : gmap prop_id (frac * lock_res_name),
         fa = fmap (λ X, (res_frac X, res_name X)) A
       (* Information we retain: the flock is locked .. *)
        own (flock_state_name γ) ( (Excl' Locked))
       (* What are the exact propositions that we have activated.. *)
        own (flock_props_active_name γ) ( (Excl' fa))
       (* Tokens and permissions for closing the active propositions .. *)
        ([ map] i  X  A, token (res_name X)
                   cinv (resN.@i) (flock_cinv_name (res_name X)) (C (res_prop X) (res_name X))
                   cinv_own (flock_cinv_name (res_name X)) (res_frac X)))%I.

  Definition to_props_map (f : gmap prop_id lock_res_name)
    : gmapUR prop_id (prodR fracR (agreeR lock_res_nameC)) :=
    fmap (λ X, (1%Qp, to_agree X)) f.
Dan Frumin's avatar
Dan Frumin committed
180

181
  (** TODO: can we actually get rid of the `to_props_map` here? *)
Dan Frumin's avatar
Dan Frumin committed
182
  Definition flock_inv (γ : flock_name) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
183 184
    ( (s : lockstate)
       (** fa -- active propositions, fp -- pending propositions *)
Dan Frumin's avatar
Dan Frumin committed
185 186
       (fa : gmap prop_id (frac * lock_res_name))
       (fp : gmap prop_id lock_res_name),
187
       (** ... and those sets are disjoint *)
Dan Frumin's avatar
Dan Frumin committed
188
       fp ## from_active fa 
Dan Frumin's avatar
Dan Frumin committed
189
       own (flock_state_name γ) ( (Excl' s)) 
190
       (** the totality of resources: fp ∪ fa *)
Dan Frumin's avatar
Dan Frumin committed
191
       own (flock_props_name γ) ( to_props_map (fp  from_active fa)) 
192
       (** but we also need to know the exact contents of fa *)
Dan Frumin's avatar
Dan Frumin committed
193
       own (flock_props_active_name γ) ( Excl' fa) 
194 195 196 197
       (** 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
198
       all_tokens fp 
Dan Frumin's avatar
Dan Frumin committed
199
       match s with
Dan Frumin's avatar
Dan Frumin committed
200
       | Locked =>
201
         (** If the lock is acuired, then we hold on to the token from the "old" specification *)
Dan Frumin's avatar
Dan Frumin committed
202
         locked (flock_lock_name γ) 
203 204 205 206 207 208 209
         (** .. and we take hold of all the ghost pointsto `s ↦{π} ρ`.

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

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

Dan Frumin's avatar
Dan Frumin committed
221 222 223
  (** * Lemmata **)

  (** ** Basic properties of the CAPs *)
224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263
  (* TODO, we only have this for the "smart constructor" *)
  Lemma flock_res_agree (γ : flock_name) (s : prop_id) (R1 R2 : iProp Σ) ρ1 ρ2 (π1 π2 : frac) :
    flock_res γ s (LockRes R1 π1 ρ1) -
    flock_res γ s (LockRes R2 π2 ρ2) ==
    ⌜ρ1 = ρ2.
  Proof.
    rewrite /flock_res.
    iDestruct 1 as "(Hs1 & #Hinv1 & Hρ1)".
    iDestruct 1 as "(Hs2 & #Hinv2 & Hρ2)".
    iCombine "Hs1 Hs2" as "Hs".
    iDestruct (own_valid with "Hs")
      as %Hfoo%auth_valid_discrete.
    simpl in Hfoo. apply singleton_valid in Hfoo.
    destruct Hfoo as [_ Hfoo%agree_op_inv']. eauto.
  Qed.

  Lemma flock_res_op (γ : flock_name) (s : prop_id) (R : iProp Σ) ρ (π1 π2 : frac) :
    flock_res γ s (LockRes R (π1+π2) ρ)
  flock_res γ s (LockRes R π1 ρ)  flock_res γ s (LockRes R π2 ρ).
  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.

  Global Instance flock_res_fractional γ s R ρ :
    Fractional (λ π, flock_res γ s (LockRes R π ρ)).
  Proof. intros p q. apply flock_res_op. Qed.

  Global Instance flock_res_as_fractional γ s R π ρ :
    AsFractional (flock_res γ s (LockRes R π ρ))
                 (λ π, flock_res γ s (LockRes R π ρ)) π.
  Proof. split. done. apply _. Qed.
Dan Frumin's avatar
Dan Frumin committed
264

Dan Frumin's avatar
Dan Frumin committed
265 266
  Lemma to_props_map_singleton_included fp i q ρ:
    {[i := (q, to_agree ρ)]}  to_props_map fp  fp !! i = Some ρ.
267
  Proof.
Dan Frumin's avatar
Dan Frumin committed
268 269 270
    rewrite singleton_included=> -[[q' av] []].
    rewrite /to_props_map lookup_fmap fmap_Some_equiv => -[v' [Hi [/= -> ->]]].
    move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
271 272
  Qed.

Dan Frumin's avatar
Dan Frumin committed
273 274 275
  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
276
    by rewrite /to_props_map fmap_delete.
Dan Frumin's avatar
Dan Frumin committed
277
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
278

Dan Frumin's avatar
Dan Frumin committed
279 280
  (** ** Spectral operations *)

Dan Frumin's avatar
Dan Frumin committed
281 282 283 284
  Lemma flock_res_alloc_strong (X : gset prop_id) γ lk R E :
    N  E 
    is_flock γ lk -
     R ={E}=  s ρ, s  X  flock_res γ s (LockRes R 1 ρ).
285
  Proof.
Dan Frumin's avatar
Dan Frumin committed
286 287 288 289 290 291
    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".
Dan Frumin's avatar
Dan Frumin committed
292 293
    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.
Dan Frumin's avatar
Dan Frumin committed
294
    { apply is_fresh. }
Dan Frumin's avatar
Dan Frumin committed
295
    apply not_elem_of_union in Hs. destruct Hs as [Hi1 Hi2].
Dan Frumin's avatar
Dan Frumin committed
296 297 298 299 300 301 302 303 304 305

    (* Alloc all the data for the resource *)
    iMod (own_alloc (Excl ())) as (γt) "T1"; first done.
    iMod (own_alloc (Excl ())) as (γt) "T2"; first done.
    iMod (cinv_alloc _ (resN.@i) (R  own γt (Excl ())  own γt (Excl ()))%I with "[HR T1]") as (γc) "[#HR Hρ]".
    { iNext. iLeft. by iFrame. }
    pose (ρ :=
            {| flock_cinv_name := γc;
               flock_token1_name := γt;
               flock_token2_name := γt |}).
Dan Frumin's avatar
Dan Frumin committed
306

Dan Frumin's avatar
Dan Frumin committed
307 308 309 310
    (* Put it in the map of flock resources *)
    iMod (own_update  with "Haprops") as "Haprops".
    { apply (auth_update_alloc _ (to_props_map (<[i := ρ]> fp  from_active fa))
                               {[ i := (1%Qp, to_agree ρ) ]}).
Dan Frumin's avatar
Dan Frumin committed
311 312 313 314 315
      rewrite -insert_union_l.
      rewrite /to_props_map /= fmap_insert.
      apply alloc_local_update; last done.
      apply (not_elem_of_dom (to_props_map (fp  from_active fa)) i (D:=gset prop_id)).
      by rewrite /to_props_map dom_fmap. }
Dan Frumin's avatar
Dan Frumin committed
316 317 318 319 320 321 322 323 324
    iDestruct "Haprops" as "[Haprops Hi]".
    iMod ("Hcl" with "[-Hi Hρ]") as "_".
    { iNext. iExists s, fa,(<[i:=ρ]>fp).
      iFrame. rewrite /all_tokens 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. iPureIntro.
      apply map_disjoint_insert_l_2; eauto.
Dan Frumin's avatar
Dan Frumin committed
325
      eapply (not_elem_of_dom (D:=gset prop_id)).
Dan Frumin's avatar
Dan Frumin committed
326 327 328 329
      intros Hi; apply Hi1. rewrite dom_union_L elem_of_union. eauto.
    }
    iModIntro; iExists i, ρ; iSplit; eauto.
    by iFrame.
Dan Frumin's avatar
Dan Frumin committed
330 331
  Qed.

Dan Frumin's avatar
Dan Frumin committed
332 333 334 335 336
  Lemma flock_res_dealloc γ lk i X E :
    N  E 
    res_frac X = 1%Qp 
    is_flock γ lk -
    flock_res γ i X ={E}=  (res_prop X).
Dan Frumin's avatar
Dan Frumin committed
337
  Proof.
Dan Frumin's avatar
Dan Frumin committed
338 339 340 341 342 343 344 345 346 347 348
    iIntros (? HX) "Hl HR". rewrite /is_flock.
    iDestruct "Hl" as "(#Hfl & #Hlk)".
    destruct X as [R ? ρ]. simpl in HX. rewrite HX; clear HX.
    iDestruct "HR" as "(Hi & #Hiinv & Hρ)".

    iInv invN as ([|] fa fp)
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl".
    (* Locked *)
    - iDestruct "Hst" as ">[Hlocked Hactives]".
      (* We can now show that the proposition `i` is *not* active *)
      iDestruct (own_valid_2 with "Haprops Hi")
Dan Frumin's avatar
Dan Frumin committed
349
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
350
      iAssert (fa !! i = None)%I with "[-]" as %Hbar.
Dan Frumin's avatar
Dan Frumin committed
351 352 353
      { remember (fa !! i) as fai. destruct fai as [[π ρ']|]; last done.
        symmetry in Heqfai.
        rewrite (big_sepM_lookup _ fa i (π, ρ')) //.
Dan Frumin's avatar
Dan Frumin committed
354
        (* TODO: RK, please look at this! *)
Dan Frumin's avatar
Dan Frumin committed
355
        iDestruct (own_valid_2 with "Hi Hactives") as %Hbaz.
Dan Frumin's avatar
Dan Frumin committed
356 357 358 359 360
        exfalso. revert Hbaz.
        rewrite -auth_frag_op /=. intros Hbaz%auth_own_valid.
        revert Hbaz. simpl. rewrite op_singleton pair_op /=.
        rewrite singleton_valid. intros [Hlol _]. simpl in *.
        eapply exclusive_l ; eauto. apply _. }
Dan Frumin's avatar
Dan Frumin committed
361
      assert (fp !! i = Some ρ) as Hbaz.
Dan Frumin's avatar
Dan Frumin committed
362 363
      { apply lookup_union_Some in Hfoo; last done.
        destruct Hfoo as [? | Hfoo]; first done.
Dan Frumin's avatar
Dan Frumin committed
364
        exfalso. revert Hfoo. by rewrite /from_active lookup_fmap Hbar.
Dan Frumin's avatar
Dan Frumin committed
365 366
      }

Dan Frumin's avatar
Dan Frumin committed
367
      iMod (own_update_2 with "Haprops Hi") as "Haprops".
Dan Frumin's avatar
Dan Frumin committed
368
      { apply auth_update_dealloc, (delete_singleton_local_update _ i _). }
Dan Frumin's avatar
Dan Frumin committed
369 370 371 372 373 374
      rewrite /all_tokens (big_sepM_delete _ fp i ρ) //.
      iDestruct "Htokens" as "[T2 Htokens]".
      iMod (cinv_cancel with "Hiinv Hρ") as "HC". solve_ndisj.
      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
375

Dan Frumin's avatar
Dan Frumin committed
376 377 378 379
      (* Now that the resource is cancelled we close the flock invariant *)
      iApply "Hcl". iNext.
      iExists Locked,fa,(delete i fp). iFrame.
      iSplit.
380
      + iPureIntro. solve_map_disjoint.
Dan Frumin's avatar
Dan Frumin committed
381 382 383 384 385
      + 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
386 387 388 389
      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
390 391
      rewrite /from_active fmap_empty /= right_id.
      iDestruct (own_valid_2 with "Haprops Hi")
Dan Frumin's avatar
Dan Frumin committed
392
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
393
      iMod (own_update_2 with "Haprops Hi") as "Haprops".
Dan Frumin's avatar
Dan Frumin committed
394
      { apply auth_update_dealloc, (delete_singleton_local_update _ i _). }
Dan Frumin's avatar
Dan Frumin committed
395 396 397 398 399 400 401 402 403 404 405
      rewrite /all_tokens (big_sepM_delete _ fp i ρ) //.
      iDestruct "Htokens" as "[T2 Htokens]".
      iMod (cinv_cancel with "Hiinv Hρ") as "HC". solve_ndisj.
      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.
      iExists Unlocked,,(delete i fp). iFrame.
      iSplit.
406
      + iPureIntro. solve_map_disjoint.
Dan Frumin's avatar
Dan Frumin committed
407 408
      + rewrite /from_active fmap_empty /= right_id.
        by rewrite to_props_map_delete.
Dan Frumin's avatar
Dan Frumin committed
409
  Qed.
410

Dan Frumin's avatar
Dan Frumin committed
411
  (** `flocked` supports invariant access just like regular invariants *)
Dan Frumin's avatar
Dan Frumin committed
412
  Lemma flocked_inv_open_single E i X γ I :
Dan Frumin's avatar
Dan Frumin committed
413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437
    resN  E 
    I !! i = Some X 
    flocked γ I ={E}=
     (res_prop X)  ( (res_prop X) ={E}= flocked γ I).
  Proof.
    iIntros (? Hi). rewrite {1}/flocked.
    iDestruct 1 as (fa ?) "(Hst & Hfa & Htokens)".
    rewrite (big_sepM_lookup_acc _ I i X) //.
    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. }
    iModIntro. rewrite /flocked. iExists fa.
    iFrame "Hst Hfa". iSplit; first eauto.
    iApply "Htokens". by iFrame.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
438 439 440 441 442 443 444 445 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 471 472 473 474 475 476 477
  Lemma flocked_inv_open E γ I :
    resN  E 
    flocked γ I ={E}=
     ([ map] s  X  I, res_prop X) 
   ( ([ map] s  X  I, res_prop X) ={E}= flocked γ I).
  Proof.
    iIntros (?). rewrite {1}/flocked.
    iDestruct 1 as (fa ?) "(Hst & Hfa & Htokens)".
    rewrite !big_sepM_sepM.
    iDestruct "Htokens" as "(T2s & Hinvs & Hρs)".
    rewrite /flocked -(bi.exist_intro fa).
    iAssert (fa = (λ X, (res_frac X, res_name X)) <$> I)%I as "$".
    { eauto. }
    iFrame "Hst Hfa". subst fa.
    iInduction I as [|s X I Hs] "IH" using map_ind.
    - 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
478
  (** ** Physical operations *)
Dan Frumin's avatar
Dan Frumin committed
479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500
  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
501 502
  Lemma release_cancel_spec γ lk I :
    {{{ is_flock γ lk  flocked γ I }}}
503
      release lk
Dan Frumin's avatar
Dan Frumin committed
504
    {{{ RET #(); [ map] i  X  I, flock_res γ i X }}}.
505
  Proof.
Dan Frumin's avatar
Dan Frumin committed
506
    iIntros (Φ) "(#Hl & H) HΦ". rewrite -fupd_wp.
Dan Frumin's avatar
Dan Frumin committed
507
    rewrite /is_flock. iDestruct "Hl" as "(#Hinv & #Hlk)".
Dan Frumin's avatar
Dan Frumin committed
508

Dan Frumin's avatar
Dan Frumin committed
509
    rewrite {1}/flocked /=.
Dan Frumin's avatar
Dan Frumin committed
510
    iDestruct "H" as (fa' Hfa) "(Hflkd & Hfactive & Hfa)".
Dan Frumin's avatar
Dan Frumin committed
511 512 513
    do 2 rewrite big_sepM_sepM.
    iDestruct "Hfa" as "(HT2s & #Hinvs & Hρs)".

Dan Frumin's avatar
Dan Frumin committed
514 515 516
    iInv invN as ([|] fa fp)
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl";
      last first.
Dan Frumin's avatar
Dan Frumin committed
517 518 519
    - 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
520
    - iDestruct "Hst" as ">[Hlocked Hactives]".
Dan Frumin's avatar
Dan Frumin committed
521 522 523 524 525 526
      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".
527 528 529
      { apply (auth_update _ _ (Excl' Unlocked) (Excl' Unlocked)).
        apply option_local_update.
        by apply exclusive_local_update. }
Dan Frumin's avatar
Dan Frumin committed
530
      iDestruct "Hstate" as "[Hstate Hunflkd]".
Léon Gondelman's avatar
Léon Gondelman committed
531

Dan Frumin's avatar
Dan Frumin committed
532 533 534 535 536 537 538
      (* 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
539 540 541
      pose (fa := ((λ X : lock_res, (res_frac X, res_name X)) <$> I)).
      iMod ("Hcl" with "[-HΦ Hlocked Hactives Hunflkd Hρs]") as "_".
      { iNext. iExists Unlocked,,(fp  from_active fa).
Dan Frumin's avatar
Dan Frumin committed
542 543
        iSplitR; eauto.
        - rewrite /from_active fmap_empty. iPureIntro.
544
          solve_map_disjoint.
Dan Frumin's avatar
Dan Frumin committed
545
        - iFrame. rewrite /from_active fmap_empty right_id /=.
Dan Frumin's avatar
Dan Frumin committed
546 547 548 549
          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
550
      iApply (release_spec with "[$Hlk $Hlocked $Hunflkd]").
Dan Frumin's avatar
Dan Frumin committed
551
      iModIntro. iNext. iIntros "_". iApply "HΦ".
Dan Frumin's avatar
Dan Frumin committed
552 553 554
      rewrite /flock_res !big_sepM_sepM.
      iFrame "Hρs Hinvs".
      rewrite big_sepM_fmap. iFrame.
Dan Frumin's avatar
Dan Frumin committed
555 556
  Qed.

Dan Frumin's avatar
Dan Frumin committed
557
  (** For the acquire we need two additional lemmas, and they are annoying! *)
Dan Frumin's avatar
Dan Frumin committed
558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587
  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.
Dan Frumin's avatar
Dan Frumin committed
588

Dan Frumin's avatar
Dan Frumin committed
589 590 591 592 593 594 595 596 597
  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
598 599 600
  Lemma acquire_flock_spec γ lk (I : gmap prop_id lock_res) :
    {{{ is_flock γ lk  [ map] i  X  I, flock_res γ i X }}}
      acquire lk
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 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648
    {{{ 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 *)
      pose (fa := fmap (λ X, (res_frac X, res_name X)) I).
      iExists fa.
      iAssert (fa = (λ X, (res_frac X, res_name X)) <$> I)%I as "$".
      { eauto. }

      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
649 650
      iMod (own_frag_empty with "Haprops") as "[Haprops #Hemp]".

651 652 653 654 655 656 657 658 659
      pose (I' := (fmap (λ X, (res_frac X, to_agree (res_name X))) I)).
      iAssert (own (flock_props_name γ) ( I'))
        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
660 661
      (* TODO: RK, please take a look at this horrific script *)
      (* We are going to separate the active resources I out of the fp map *)
662
      pose (I'' := fmap res_name I).
Dan Frumin's avatar
Dan Frumin committed
663
      assert ( P', P' ## I''  fp  P'  I'') as [P' HP'].
664
      { subst I'' I' fa. clear H1.
Dan Frumin's avatar
Dan Frumin committed
665 666 667 668 669 670 671 672 673
        unfold to_props_map in *.
        pose (f := (λ X, (res_frac X, to_agree (res_name X)))).
        pose (g := (λ X:lock_res_name, (1%Qp, to_agree X))).
        (* Proof idea:
          f <$> I ≼ g <$> fp
             implies
          snd <$> f <$> I ≼ snd <$> g <$> fp
          =  to_agree o res_name <$> I ≼ to_agree <$> fp *)
        assert (((snd <$> (f <$> I)) : gmapUR prop_id (agreeR lock_res_nameC))  (snd <$> (g <$> fp))) as Hbar.
Dan Frumin's avatar
Dan Frumin committed
674 675 676
        { apply gmap_fmap_mono; eauto.
          - move=> [? ?] [? ?] [? ?] //.
          - intros [? ?] [? ?] [? ?]%prod_included. done. }
Dan Frumin's avatar
Dan Frumin committed
677 678 679 680 681 682 683 684 685 686
        rewrite -!map_fmap_compose in Hbar.
        assert ((to_agree  res_name <$> I)  to_agree <$> fp) as Hbaz by exact: Hbar.
        rewrite map_fmap_compose in Hbaz.

        (* which implies the following *)
        assert ( i, to_agree <$> (res_name <$> (I !! i))  to_agree <$> (fp !! i)) as Hbork.
        { intros i. rewrite -!lookup_fmap. revert i.
          apply lookup_included. exact: Hbaz. }
        clear Hbaz Hbar Hfoo.

687
        generalize dependent fp.
Dan Frumin's avatar
Dan Frumin committed
688
        induction I as [|i X I HI IHI] using map_ind; intros fp.
689
        + rewrite fmap_empty.
Dan Frumin's avatar
Dan Frumin committed
690 691
          exists fp. rewrite right_id.
          split; first solve_map_disjoint; auto.
692 693
        + rewrite fmap_insert=>Hfp.
          specialize (IHI (delete i fp)).
Dan Frumin's avatar
Dan Frumin committed
694 695 696 697 698 699 700 701 702
          assert ( j, to_agree <$> (res_name <$> I !! j)
                          (to_agree <$> delete i fp !! j)) as goodboi.
          { intros j.
            destruct (decide (i = j)) as [<-|?].
            - by rewrite HI lookup_delete.
            - specialize (Hfp j).
              rewrite lookup_insert_ne in Hfp; last done.
              rewrite lookup_delete_ne //. }
          specialize (IHI goodboi). clear goodboi.
703 704
          destruct IHI as [P [HP HU]].
          assert (P !! i = None) as HPi.
Dan Frumin's avatar
Dan Frumin committed
705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724
          { destruct (P !! i) as [Y|] eqn:HPi; auto; simplify_eq/=.
            exfalso. unfold_leibniz.
            specialize (HU i). fold_leibniz.
            rewrite (lookup_union_Some_l _ _ _ _ HPi) in HU.
            rewrite lookup_delete in HU. done. }
          exists P. split; first solve_map_disjoint.
          rewrite -insert_union_r // -HU.
          rewrite insert_delete=> j.
          specialize (Hfp j).
          destruct (decide (i = j)) as [<-|?].
          * revert Hfp. rewrite !lookup_insert.
            intros Hfp.
            destruct (proj1( option_included _ _) Hfp)
              as [?|(a&?&Ha&Hj&Heq)]; simplify_eq/=.
            destruct (fp !! i) as [Y|] eqn:HY; simplify_eq/=.
            revert Heq. rewrite to_agree_included HY.
            intros [->%to_agree_inj | ->]; reflexivity.
          * rewrite lookup_insert_ne //. }
      fold_leibniz.

725
      destruct HP' as [HP' ->].
Dan Frumin's avatar
Dan Frumin committed
726

727 728 729 730 731 732 733 734 735 736
      rewrite /all_tokens big_sepM_union //.
      iDestruct "Htokens" as "[Htokens H]".
      rewrite /I'' big_sepM_fmap. iFrame.
      iApply "Hcl".
      iNext. iExists Locked, fa, P'.
      assert (res_name <$> I = from_active fa) as <-.
      { rewrite /from_active -map_fmap_compose.
        apply map_eq=> k. by rewrite lookup_fmap. }
      iFrame. iSplit; eauto.
      rewrite big_sepM_fmap.
Dan Frumin's avatar
Dan Frumin committed
737
      iApply (big_sepM_own_frag with "Hemp HI").
Dan Frumin's avatar
Dan Frumin committed
738
  Qed.
739

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