flock.v 7.79 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 4 5
From iris.heap_lang Require Import spin_lock.
From iris.base_logic.lib Require Import cancelable_invariants.
From iris.algebra Require Import auth excl frac.
Léon Gondelman's avatar
Léon Gondelman committed
6 7
From iris.base_logic.lib Require Import fractional.

8 9 10 11 12 13 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 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
Inductive lockstate :=
  | Locked : frac  lockstate
  | Unlocked.
Canonical Structure lockstateC := leibnizC lockstate.

Record flock_name := {
  flock_lock_name : gname;
  flock_cinv_name : gname;
  flock_state_name : gname;
}.

Class flockG Σ :=
  FlockG {
    flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
    flock_cinvG :> cinvG Σ;
    flock_lockG :> lockG Σ
  }.


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
58
Section flock.
59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
  Context `{heapG Σ, flockG Σ}.

  Variable N : namespace.

  Definition flock_inv (γ : flock_name) (R : iProp Σ) : iProp Σ :=
    ( s : lockstate,
       own (flock_state_name γ) ( (Excl' s)) 
       match s with
       | Locked q =>
         cinv_own (flock_cinv_name γ) (q/2) 
         locked (flock_lock_name γ)
       | Unlocked => R
       end)%I.

  Local Instance flock_inv_timeless γ R `{Timeless _ R} : Timeless (flock_inv γ R).
  Proof.
    rewrite /flock_inv.
    apply uPred.exist_timeless => s.
    destruct s; apply _.
  Qed.

  Definition is_flock (γ : flock_name) (lk : val) (R : iProp Σ) : iProp Σ :=
    (cinv (N .@ "inv") (flock_cinv_name γ) (flock_inv γ R) 
     is_lock (N .@ "lock") (flock_lock_name γ) lk
         (own (flock_state_name γ) ( (Excl' Unlocked))))%I.

  Global Instance is_flock_persistent γ lk R : Persistent (is_flock γ lk R).
  Proof. apply _. Qed.

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

  Definition flocked (γ : flock_name) (q : frac) : iProp Σ :=
    (own (flock_state_name γ) ( (Excl' (Locked q)))
      cinv_own (flock_cinv_name γ) (q/2))%I.

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

  Global Instance unflocked_fractional γ :
    Fractional (unflocked γ).
  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
105 106 107
  Proof. split. done. apply _. Qed.

  Lemma newlock_cancel_spec (R : iProp Σ):
108 109 110 111 112 113 114 115 116 117 118 119 120 121 122
    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk R  unflocked γ 1 }}}.
  Proof.
    iIntros (Φ) "HR HΦ". rewrite -wp_fupd.
    iMod (own_alloc ( (Excl' Unlocked)   (Excl' Unlocked)))
      as (γ_state) "[Hauth Hfrag]"; first done.
    iApply (newlock_spec (N.@"lock") (own γ_state ( (Excl' Unlocked))) with "Hfrag").
    iNext. iIntros (lk γ_lock) "#Hlock".
    iMod (cinv_alloc_strong  _ (N.@"inv")
       (fun γ => flock_inv (Build_flock_name γ_lock γ γ_state) R) with "[-HΦ]") as (γ_cinv) "(_ & #Hcinv & Hown)".
    { iNext. rewrite /flock_inv /=. iIntros (γ _).
      iExists Unlocked. by iFrame. }
    pose (γ := (Build_flock_name γ_lock γ_cinv γ_state)).
    iModIntro. iApply ("HΦ" $! lk γ). iFrame "Hown".
    rewrite /is_flock. by iFrame "Hlock".
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
123

124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152
  Lemma acquire_cancel_spec γ π lk (R : iProp Σ) `{Timeless _ R} :
    {{{ is_flock γ lk R  unflocked γ π }}}
      acquire lk
    {{{ RET #(); flocked γ π  R }}}.
  Proof.
    iIntros (Φ) "[Hl Hunfl] 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.
    (* TODO: why doesn't this work?
       iDestruct "Hstate" as (s) "Hstate". *)
    iDestruct "Hstate" as ">Hstate".
    iDestruct "Hstate" as (s) "Hstate".
    destruct s as [q|].
    - iDestruct "Hstate" as "(Hstate & Hcown & Hlocked2)".
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
    - iDestruct "Hstate" as "[Hstate HR]".
      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]".
      iMod ("Hcl" with "[Hstate Hcown Hlocked]").
      { iNext. iExists (Locked π). iFrame. }
      iApply "HΦ". by iFrame.
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
153

154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193
  Lemma release_cancel_spec γ π lk R `{Timeless _ R} :
    {{{ is_flock γ lk R  flocked γ π  R }}}
      release lk
    {{{ RET #(); unflocked γ π }}}.
  Proof.
    iIntros (Φ) "(Hl & (Hstate' & Hflkd) & HR) HΦ". rewrite -fupd_wp.
    rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iMod (cinv_open with "Hcinv Hflkd") as "(Hstate & Hunfl & Hcl)"; first done.
    rewrite {2}/flock_inv.
    (* TODO: why doesn't this work?
       iDestruct "Hstate" as (s) "Hstate". *)
    iDestruct "Hstate" as ">Hstate".
    iDestruct "Hstate" as (s) "Hstate".
    destruct s as [q|]; last first.
    - iDestruct "Hstate" as "[Hstate HR']".
      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.
    - iDestruct "Hstate" as "(Hstate & Hcown & Hlocked)".
      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']".
      iMod ("Hcl" with "[Hstate HR]").
      { iNext. iExists Unlocked. iFrame. }
      iApply (release_spec with "[$Hlk $Hlocked $Hstate']").
      iModIntro. iNext. iIntros "_". iApply "HΦ".
      by iSplitL "Hcown".
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
194

195 196 197 198 199 200 201 202 203 204 205 206 207 208
  Lemma cancel_lock γ lk R `{Timeless _ R} :
    is_flock γ lk R - unflocked γ 1 ={}= R.
  Proof.
    rewrite /is_flock /unflocked.
    iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "Hcown".
    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as ">$"; eauto.
    iIntros "[Hcown Hstate]".
    iDestruct "Hstate" as ">Hstate".
    iDestruct "Hstate" as (s) "(Hstate & HR)".
    destruct s as [q|].
    - iDestruct "HR" as "(Hcown2 & Hlocked)".
      iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
    - by iFrame.
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
209 210

End flock.