lock.v 5.26 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

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

96
  Typeclasses Opaque newlock.
Amin Timany's avatar
Amin Timany committed
97 98
  Global Opaque newlock.

99
  Lemma steps_acquire E j K l :
Amin Timany's avatar
Amin Timany committed
100
    nclose specN  E 
101
    spec_ctx  l ↦ₛ (#v false)  j  fill K (App acquire (Loc l))
Amin Timany's avatar
Amin Timany committed
102 103 104
       |={E}=> j  fill K Unit  l ↦ₛ (#v true).
  Proof.
    iIntros (HNE) "[#Hspec [Hl Hj]]". unfold acquire.
105 106
    iMod (step_rec _ j K with "[Hj]") as "Hj"; eauto. done.
    iMod (step_cas_suc _ j ((IfCtx _ _) :: K)
Amin Timany's avatar
Amin Timany committed
107 108
                       _ _ _ _ _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; trivial.
    { simpl. iFrame "Hspec Hj Hl"; eauto. }
109
    iMod (step_if_true _ j K _ _ _ with "[Hj]") as "Hj"; trivial.
Amin Timany's avatar
Amin Timany committed
110 111 112 113 114
    { by iFrame. }
    by iIntros "!> {$Hj $Hl}".
    Unshelve. all:trivial.
  Qed.

115
  Typeclasses Opaque acquire.
Amin Timany's avatar
Amin Timany committed
116 117
  Global Opaque acquire.

118
  Lemma steps_release E j K l b:
Amin Timany's avatar
Amin Timany committed
119
    nclose specN  E 
120
    spec_ctx  l ↦ₛ (#v b)  j  fill K (App release (Loc l))
Amin Timany's avatar
Amin Timany committed
121 122 123
       |={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
  Global Opaque release.

132
  Lemma steps_with_lock E j K e l P Q v w:
Amin Timany's avatar
Amin Timany committed
133
    nclose specN  E 
Amin Timany's avatar
Amin Timany committed
134
    (* (∀ f, e.[f] = e) (* e is a closed term *) → *)
135
    ( K', spec_ctx  P  j  fill K' (App e (of_val w))
Amin Timany's avatar
Amin Timany committed
136
             |={E}=> j  fill K' (of_val v)  Q) 
137
    spec_ctx  P  l ↦ₛ (#v false)
Amin Timany's avatar
Amin Timany committed
138 139 140
                 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
    iIntros (HNE He) "[#Hspec [HP [Hl Hj]]]".
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
144
    iMod (steps_acquire _ j (SeqCtx _ :: K) with "[$Hj Hl]") as "[Hj Hl]";
Amin Timany's avatar
Amin Timany committed
145 146 147
      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.
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.