flock.v 7.31 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
Inductive lockstate :=
  | Locked : frac  lockstate
  | Unlocked.
Canonical Structure lockstateC := leibnizC lockstate.

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

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 58
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
59
Section flock.
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
  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.

  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) :
90
    unflocked γ (π1+π2)  unflocked γ π1  unflocked γ π2.
91 92
  Proof. by rewrite /unflocked fractional. Qed.

93
  Global Instance unflocked_fractional γ : Fractional (unflocked γ).
94 95 96
  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
97 98 99
  Proof. split. done. apply _. Qed.

  Lemma newlock_cancel_spec (R : iProp Σ):
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
    {{{ 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
115

116
  Lemma acquire_cancel_spec γ π lk (R : iProp Σ) :
117 118
    {{{ is_flock γ lk R  unflocked γ π }}}
      acquire lk
119
    {{{ RET #(); flocked γ π   R }}}.
120 121 122 123 124 125 126
  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.
127 128
    iDestruct "Hstate" as ([q|]) "Hstate".
    - iDestruct "Hstate" as ">(Hstate & Hcown & Hlocked2)".
129
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
130
    - iDestruct "Hstate" as "[>Hstate HR]".
131 132 133 134 135 136 137 138 139 140
      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
141

142 143
  Lemma release_cancel_spec γ π lk R :
    {{{ is_flock γ lk R  flocked γ π   R }}}
144 145 146 147 148 149 150
      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.
151 152
    iDestruct "Hstate" as ([q|]) "Hstate"; last first.
    - iDestruct "Hstate" as "[>Hstate HR']".
153 154 155 156 157 158
      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.
159
    - iDestruct "Hstate" as ">(Hstate & Hcown & Hlocked)".
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
      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
178

179 180
  Lemma cancel_lock γ lk R :
    is_flock γ lk R - unflocked γ 1 ={}=  R.
181 182 183
  Proof.
    rewrite /is_flock /unflocked.
    iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "Hcown".
184
    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; eauto.
185
    iIntros "[Hcown Hstate]".
186 187
    iDestruct "Hstate" as ([q|]) "(Hstate & HR)".
    - iDestruct "HR" as ">(Hcown2 & Hlocked)".
188 189 190
      iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
    - by iFrame.
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
191
End flock.