lock.v 5.3 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris.proofmode Require Import tactics.
Amin Timany's avatar
Amin Timany committed
2
From iris_examples.logrel.F_mu_ref_conc Require Export rules_binary typing.
Amin Timany's avatar
Amin Timany committed
3 4 5 6 7 8 9

(** [newlock = alloc false] *)
Definition newlock : expr := Alloc (# false).
(** [acquire = λ x. if cas(x, false, true) then #() else acquire(x) ] *)
Definition acquire : expr :=
  Rec (If (CAS (Var 1) (# false) (# true)) (Unit) (App (Var 0) (Var 1))).
(** [release = λ x. x <- false] *)
Amin Timany's avatar
Amin Timany committed
10
Definition release : expr := Lam (Store (Var 0) (# false)).
Amin Timany's avatar
Amin Timany committed
11 12
(** [with_lock e l = λ x. (acquire l) ;; e x ;; (release l)] *)
Definition with_lock (e : expr) (l : expr) : expr :=
Amin Timany's avatar
Amin Timany committed
13 14 15 16 17 18 19
  Lam
    (Seq
       (App acquire l.[ren (+1)])
       (LetIn
          (App e.[ren (+1)] (Var 0))
          (Seq (App release l.[ren (+2)]) (Var 0))
       )
Amin Timany's avatar
Amin Timany committed
20 21 22
    ).

Definition with_lockV (e l : expr) : val :=
Amin Timany's avatar
Amin Timany committed
23 24 25 26 27 28 29
  LamV
    (Seq
       (App acquire l.[ren (+1)])
       (LetIn
          (App e.[ren (+1)] (Var 0))
          (Seq (App release l.[ren (+2)]) (Var 0))
       )
Amin Timany's avatar
Amin Timany committed
30 31 32 33 34 35 36 37
    ).

Lemma with_lock_to_val e l : to_val (with_lock e l) = Some (with_lockV e l).
Proof. trivial. Qed.

Lemma with_lock_of_val e l : of_val (with_lockV e l) = with_lock e l.
Proof. trivial. Qed.

38
Typeclasses Opaque with_lockV.
Amin Timany's avatar
Amin Timany committed
39 40 41 42 43 44 45 46 47 48 49 50 51 52
Global Opaque with_lockV.

Lemma newlock_closed f : newlock.[f] = newlock.
Proof. by asimpl. Qed.
Hint Rewrite newlock_closed : autosubst.

Lemma acquire_closed f : acquire.[f] = acquire.
Proof. by asimpl. Qed.
Hint Rewrite acquire_closed : autosubst.

Lemma release_closed f : release.[f] = release.
Proof. by asimpl. Qed.
Hint Rewrite release_closed : autosubst.

Amin Timany's avatar
Amin Timany committed
53 54
Lemma with_lock_subst (e l : expr) f :
  (with_lock e l).[f] = with_lock e.[f] l.[f].
Amin Timany's avatar
Amin Timany committed
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
Proof. unfold with_lock; asimpl; trivial. Qed.

Definition LockType := Tref TBool.

Lemma newlock_type Γ : typed Γ newlock LockType.
Proof. repeat constructor. Qed.

Lemma acquire_type Γ : typed Γ acquire (TArrow LockType TUnit).
Proof. do 3 econstructor; eauto using EqTBool; repeat constructor. Qed.

Lemma release_type Γ : typed Γ release (TArrow LockType TUnit).
Proof. repeat econstructor. Qed.

Lemma with_lock_type e l Γ τ τ' :
  typed Γ e (TArrow τ τ') 
  typed Γ l LockType 
  typed Γ (with_lock e l) (TArrow τ τ').
Proof.
Amin Timany's avatar
Amin Timany committed
73 74 75 76 77 78 79 80
  intros ??.
  do 3 econstructor; eauto using acquire_type.
  - eapply (context_weakening [_]); eauto.
  - econstructor; eauto using typed.
    eapply (context_weakening [_]); eauto.
  - econstructor; eauto using typed.
    econstructor; eauto using release_type.
    eapply (context_weakening [_;_]); eauto.
Amin Timany's avatar
Amin Timany committed
81 82 83 84 85
Qed.

Section proof.
  Context `{cfgSG Σ}.
  Context `{heapIG Σ}.
Amin Timany's avatar
Amin Timany committed
86

Amin Timany's avatar
Amin Timany committed
87 88 89 90 91 92 93 94 95
  Lemma steps_newlock E ρ j K :
    nclose specN  E 
    spec_ctx ρ  j  fill K newlock
       |={E}=>  l, j  fill K (Loc l)  l ↦ₛ (#v false).
  Proof.
    iIntros (HNE) "[#Hspec Hj]".
    by iMod (step_alloc _ _ j K with "[Hj]") as "Hj"; eauto.
  Qed.

96
  Typeclasses Opaque newlock.
Amin Timany's avatar
Amin Timany committed
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
  Global Opaque newlock.

  Lemma steps_acquire E ρ j K l :
    nclose specN  E 
    spec_ctx ρ  l ↦ₛ (#v false)  j  fill K (App acquire (Loc l))
       |={E}=> j  fill K Unit  l ↦ₛ (#v true).
  Proof.
    iIntros (HNE) "[#Hspec [Hl Hj]]". unfold acquire.
    iMod (step_rec _ _ j K with "[Hj]") as "Hj"; eauto. done.
    iMod (step_cas_suc _ _ j ((IfCtx _ _) :: K)
                       _ _ _ _ _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; trivial.
    { simpl. iFrame "Hspec Hj Hl"; eauto. }
    iMod (step_if_true _ _ j K _ _ _ with "[Hj]") as "Hj"; trivial.
    { by iFrame. }
    by iIntros "!> {$Hj $Hl}".
    Unshelve. all:trivial.
  Qed.

115
  Typeclasses Opaque acquire.
Amin Timany's avatar
Amin Timany committed
116 117 118 119 120 121 122 123
  Global Opaque acquire.

  Lemma steps_release E ρ j K l b:
    nclose specN  E 
    spec_ctx ρ  l ↦ₛ (#v b)  j  fill K (App release (Loc l))
       |={E}=> j  fill K Unit  l ↦ₛ (#v false).
  Proof.
    iIntros (HNE) "[#Hspec [Hl Hj]]". unfold release.
Amin Timany's avatar
Amin Timany committed
124 125
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto; try done.
    iMod (step_store with "[$Hj $Hl]") as "[Hj Hl]"; eauto.
Amin Timany's avatar
Amin Timany committed
126 127 128
    by iIntros "!> {$Hj $Hl}".
  Qed.

129
  Typeclasses Opaque release.
Amin Timany's avatar
Amin Timany committed
130 131 132 133
  Global Opaque release.

  Lemma steps_with_lock E ρ j K e l P Q v w:
    nclose specN  E 
Amin Timany's avatar
Amin Timany committed
134
    (* (∀ f, e.[f] = e) (* e is a closed term *) → *)
Amin Timany's avatar
Amin Timany committed
135 136 137 138 139 140
    ( K', spec_ctx ρ  P  j  fill K' (App e (of_val w))
             |={E}=> j  fill K' (of_val v)  Q) 
    spec_ctx ρ  P  l ↦ₛ (#v false)
                 j  fill K (App (with_lock e (Loc l)) (of_val w))
       |={E}=> j  fill K (of_val v)  Q  l ↦ₛ (#v false).
  Proof.
Amin Timany's avatar
Amin Timany committed
141 142 143 144 145 146 147
    iIntros (HNE He) "[#Hspec [HP [Hl Hj]]]".
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
    iMod (steps_acquire _ _ j (SeqCtx _ :: K) with "[$Hj Hl]") as "[Hj Hl]";
      auto. simpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iMod (He (LetInCtx _ :: K) with "[$Hj HP]") as "[Hj HQ]"; eauto.
Amin Timany's avatar
Amin Timany committed
148
    simpl.
Amin Timany's avatar
Amin Timany committed
149
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
    iAsimpl.
Amin Timany's avatar
Amin Timany committed
151
    iMod (steps_release _ _ j (SeqCtx _ :: K) _ _ with "[$Hj $Hl]")
Amin Timany's avatar
Amin Timany committed
152
      as "[Hj Hl]"; eauto.
Amin Timany's avatar
Amin Timany committed
153 154 155
    simpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iModIntro; by iFrame.
Amin Timany's avatar
Amin Timany committed
156 157
  Qed.

158
  Typeclasses Opaque with_lock.
Amin Timany's avatar
Amin Timany committed
159 160
  Global Opaque with_lock.
End proof.
Amin Timany's avatar
Amin Timany committed
161

Ralf Jung's avatar
Ralf Jung committed
162 163 164 165
Hint Rewrite newlock_closed : autosubst.
Hint Rewrite acquire_closed : autosubst.
Hint Rewrite release_closed : autosubst.
Hint Rewrite with_lock_subst : autosubst.