lock_unary_spec.v 7.7 KB
Newer Older
1 2 3 4 5 6 7 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 58 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 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 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 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245
(* This file contains the specification of a lock module discussed
   in the section on the Fancy update modality and weakest precondition
   in the Iris Lecture Notes. 
     Recall from loc. cit. that the point of this 
   alternative lock specification is that it allows ones
   to allocate the lock before one knows what the resource
   of the invariant it is going to protect is.
*)

(* Contains definitions of the weakest precondition assertion, and its basic rules. *)
From iris.program_logic Require Export weakestpre.

(* Instantiation of Iris with the particular language. The notation file
   contains many shorthand notations for the programming language constructs, and
   the lang file contains the actual language syntax. *)
From iris.heap_lang Require Export notation lang.

(* Files related to the interactive proof mode. The first import includes the 
   general tactics of the proof mode. The second provides some more specialized 
   tactics particular to the instantiation of Iris to a particular programming 
   language. *)
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode.

(* Definition of invariants and their rules (expressed using the fancy update
   modality). *)
From iris.base_logic.lib Require Export invariants.

(* The exclusive resource algebra *)
From iris.algebra Require Import excl.


Section lock_model. 
(* In order to do the proof we need to assume certain things about the
   instantiation of Iris. The particular, even the heap is handled in an
   analogous way as other ghost state. This line states that we assume the Iris
   instantiation has sufficient structure to manipulate the heap, e.g., it
   allows us to use the points-to predicate, and that the ghost state includes
   the exclusive resource algebra over the singleton set (represented using the
   unitR type). *)  

  Context `{heapG Σ}.
  Context `{inG Σ (exclR unitR)}.
 
  (* We use a ghost name with a token to model whether the lock is locked or not.
     The the token is just exclusive ownerwhip of unit value. *)
  Definition locked γ := own γ (Excl ()).

  (* The name of a lock. *)
  Definition lockN (l : loc) := nroot .@ "lock" .@ l.

  (* The lock invariant *)
  Definition is_lock γ l P :=
    inv (lockN l) ((l  (#false)  P  locked γ) 
                                l  (#true))%I.

  (* The is_lock predicate is persistent *)
  Global Instance is_lock_persistent γ l Φ : Persistent (is_lock γ l Φ).
  Proof. apply _. Qed.
  
End lock_model.

Section lock_code.

  (* Here is the standard spin lock code *)
  
  Definition newlock : val := λ: <>, ref #false.
  Definition acquire : val :=
    rec: "acquire" "l" :=
      if: CAS "l" #false #true then #() else "acquire" "l".
  Definition release : val := λ: "l", "l" <- #false.

End lock_code.

Section lock_spec.
  Context `{heapG Σ}.
  Context `{inG Σ (exclR unitR)}.
  
  (* Here is the interesting part of this example, namely the new specification 
     for newlock, which allows one to get a post-condition which can be instantiated 
     with the lock invariant at some point later, when it is known. 
     See the discussion in Iris Lecture Notes. 
     First we show the specs using triples, and afterwards using weakest preconditions.
  *)

  Lemma wp_newlock_t :
    {{{ True }}} newlock #() {{{v, RET v;  (l: loc) γ, v = #l  ( P E, P ={E}= is_lock γ l P) }}}.
  Proof.
    iIntros (φ) "Hi Hcont".
    rewrite -wp_fupd /newlock.
    wp_lam.
    wp_alloc l as "HPt".
    iApply "Hcont".
    iExists l.
    iMod (own_alloc (Excl ())) as (γ) "Hld"; first done.
    iExists γ.
    iModIntro. iSplit; first done.
    iIntros (P E) "HP".
    iMod (inv_alloc _ _
           ((l  (#false)  P  locked γ)  l  (#true))%I with "[-]")
      as "Hinv"; last eauto.
    { iNext; iLeft; iFrame. }
  Qed.

  Lemma wp_acquire_t E γ l P :
    nclose (lockN l)  E 
    {{{ is_lock γ l P }}} acquire (#l) @ E {{{v, RET #v; P  locked γ}}}.
  Proof.
    iIntros (HE φ) "#Hi Hcont"; rewrite /acquire.
    iLöb as "IH".
    wp_rec.
    wp_bind (CAS _ _ _).
    iInv (lockN l) as "[(Hl & HP & Ht)|Hl]" "Hcl".
    - wp_cas_suc. 
      iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
      iModIntro.
      wp_if.
      iApply "Hcont".
      iFrame.
    - wp_cas_fail.
      iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
      iModIntro.
      wp_if.
      iApply ("IH" with "[$Hcont]").
  Qed.


  Lemma wp_release_t E γ l P :
    nclose (lockN l)  E 
    {{{ is_lock γ l P  locked γ  P }}} release (#l) @ E {{{RET #(); True}}}.
  Proof.
    iIntros (HE φ) "(#Hi & Hld & HP) Hcont"; rewrite /release.
    wp_lam.
    iInv (lockN l) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
    - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done. 
    - wp_store.
      iMod ("Hcl" with "[-Hcont]") as "_"; first by iNext; iLeft; iFrame.
      iApply "Hcont".
      done.
  Qed.

  (* Here are the specifications again, just written using weakest preconditions *)
  
  Lemma wp_newlock :
    True  WP newlock #() {{v,  (l: loc) γ, v = #l  ( P E, P ={E}= is_lock γ l P) }}.
  Proof.
    iIntros "_".
    rewrite -wp_fupd /newlock.
    wp_lam.
    wp_alloc l as "HPt". 
    iExists l.
    iMod (own_alloc (Excl ())) as (γ) "Hld"; first done.
    iExists γ.
    iModIntro. iSplit; first done.
    iIntros (P E) "HP".
    iMod (inv_alloc _ _
           ((l  (#false)  P  locked γ)  l  (#true))%I with "[-]")
      as "Hinv"; last eauto.
    { iNext; iLeft; iFrame. }
  Qed.

  
  Lemma wp_acquire E γ l P :
    nclose (lockN l)  E 
    is_lock γ l P  WP acquire (#l) @ E {{v, P  locked γ}}.
  Proof.
    iIntros (HE) "#Hi"; rewrite /acquire.
    iLöb as "IH".
    wp_rec.
    wp_bind (CAS _ _ _).
    iInv (lockN l) as "[(Hl & HP & Ht)|Hl]" "Hcl".
    - wp_cas_suc. 
      iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
      iModIntro.
      wp_if.
      iFrame.
    - wp_cas_fail.
      iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
      iModIntro.
      wp_if.
      iApply "IH".
  Qed.


  Lemma wp_release E γ l P :
    nclose (lockN l)  E 
    is_lock γ l P  locked γ  P  WP release (#l) @ E {{v, True}}.
  Proof.
    iIntros (HE) "(#Hi & Hld & HP)"; rewrite /release.
    wp_lam.
    iInv (lockN l) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
    - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done. 
    - wp_store.
      iMod ("Hcl" with "[-]") as "_"; first by iNext; iLeft; iFrame.
      done.
  Qed.


  Global Opaque newlock release acquire.

  (* We now present a simple client of the lock which cannot be verified with the
     lock specification described in the Chapter on Invariants and Ghost State in the
     Iris Lecture Notes, but which can be specifed and verified with the current 
     specification.  
  *)
  Definition test : expr :=
    let: "l" := newlock #() in
    let: "r" := ref #0 in
    (λ: <>, acquire "l";; "r" <- !"r" + #1;; release "l").

  Lemma test_spec :
    {{{ True }}} test #() {{{ v, RET v; True }}}.
  Proof.
    iIntros (φ) "Hi HCont"; rewrite /test.
    wp_bind (newlock #())%E.
    iApply (wp_newlock_t); auto.
    iNext.
    iIntros (v) "Hs".
    wp_lam.
    wp_bind (ref #0)%E.
    wp_alloc l as "Hl".
    wp_lam.
    wp_lam.
    wp_bind (acquire v)%E.
    iDestruct "Hs" as (l' γ) "[% H2]".
    subst.
    iMod ("H2" $! ( (n : Z), l  #n)%I with "[Hl]") as "#H3".
    { iExists 0; iFrame. }
    wp_apply (wp_acquire_t with "H3"); auto.
    iIntros (v) "(Hpt & Hlocked)".
    iDestruct "Hpt" as (u) "Hpt".
    wp_lam.
    wp_load.
    wp_op.
    wp_store.
    wp_apply (wp_release_t with "[-HCont]"); auto.
    iFrame "H3 Hlocked".
    iExists _; iFrame.
  Qed.
End lock_spec.

Typeclasses Opaque locked.
Global Opaque locked.
Typeclasses Opaque is_lock.
Global Opaque is_lock.