lock.v 5.53 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2
From iris_logrel.F_mu_ref_conc Require Export rules_binary typing.
3
From iris.base_logic Require Import namespaces.
Amin Timany's avatar
Amin Timany committed
4

Amin Timany's avatar
Amin Timany committed
5
Definition newlock : expr := Alloc (# false).
Amin Timany's avatar
Amin Timany committed
6
Definition acquire : expr :=
Amin Timany's avatar
Amin Timany committed
7 8
  Rec (If (CAS (Var 1) (# false) (# true)) (Unit) (App (Var 0) (Var 1))).
Definition release : expr := Rec (Store (Var 1) (# false)).
Amin Timany's avatar
Amin Timany committed
9 10

Definition with_lock (e : expr) (l : expr) : expr :=
11 12
  Rec
    (App (Rec (App (Rec (App (Rec (Var 3)) (App release l.[ren (+6)])))
13 14
                   (App e.[ren (+4)] (Var 3))))
         (App acquire l.[ren (+2)])
Amin Timany's avatar
Amin Timany committed
15 16 17
    ).

Definition with_lockV (e l : expr) : val :=
18 19
  RecV
    (App (Rec (App (Rec (App (Rec (Var 3)) (App release l.[ren (+6)])))
20 21
                   (App e.[ren (+4)] (Var 3))))
         (App acquire l.[ren (+2)])
Amin Timany's avatar
Amin Timany committed
22 23
    ).

Robbert Krebbers's avatar
Robbert Krebbers committed
24
Lemma with_lock_to_val e l : to_val (with_lock e l) = Some (with_lockV e l).
Amin Timany's avatar
Amin Timany committed
25 26
Proof. trivial. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
27
Lemma with_lock_of_val e l : of_val (with_lockV e l) = with_lock e l.
Amin Timany's avatar
Amin Timany committed
28 29 30
Proof. trivial. Qed.

Global Opaque with_lockV.
Amin Timany's avatar
Amin Timany committed
31

32 33
Lemma newlock_closed f : newlock.[f] = newlock.
Proof. by asimpl. Qed.
34
Hint Rewrite newlock_closed : autosubst.
35 36 37

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
44
Lemma with_lock_subst (e l : expr) f :  (with_lock e l).[f] = with_lock e.[f] l.[f].
45 46
Proof. unfold with_lock; asimpl; trivial. Qed.

47 48 49 50
Lemma with_lock_closed e l:
  ( f : var  expr, e.[f] = e) 
  ( f : var  expr, l.[f] = l) 
   f, (with_lock e l).[f] = with_lock e l.
51
Proof. asimpl => H1 H2 f. unfold with_lock. by rewrite ?H1 ?H2. Qed.
52 53 54 55 56 57 58 59 60 61 62 63

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.

Amin Timany's avatar
Amin Timany committed
64 65
Lemma with_lock_type e l Γ τ τ' :
  typed Γ e (TArrow τ τ') 
66
  typed Γ l LockType 
Amin Timany's avatar
Amin Timany committed
67
  typed Γ (with_lock e l) (TArrow τ τ').
68
Proof.
69 70 71 72 73
  intros H1 H2. do 3 econstructor; eauto.
  - repeat (econstructor; eauto using release_type).
    + eapply (context_weakening [_; _; _; _; _; _]); eauto.
    + eapply (context_weakening [_; _; _; _]); eauto.
  - eapply acquire_type.
Amin Timany's avatar
Amin Timany committed
74
  - eapply (context_weakening [_; _]); eauto.
75 76
Qed.

Amin Timany's avatar
Amin Timany committed
77
Section proof.
78
  Context `{cfgSG Σ}.
79

80 81
  Lemma steps_newlock E ρ j K :
    nclose specN  E 
82 83
    spec_ctx ρ  j  fill K newlock
       |={E}=>  l, j  fill K (Loc l)  l ↦ₛ (#v false).
84
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
    iIntros (HNE) "[#Hspec Hj]".
86
    by iMod (step_alloc _ _ j K with "[Hj]") as "Hj"; eauto.
87 88 89 90
  Qed.

  Global Opaque newlock.

91 92
  Lemma steps_acquire E ρ j K l :
    nclose specN  E 
93 94
    spec_ctx ρ  l ↦ₛ (#v false)  j  fill K (App acquire (Loc l))
       |={E}=> j  fill K Unit  l ↦ₛ (#v true).
95
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
    iIntros (HNE) "[#Hspec [Hl Hj]]". unfold acquire.
97 98
    iMod (step_rec _ _ j K with "[Hj]") as "Hj"; eauto. done.
    iMod (step_cas_suc _ _ j (K ++ [IfCtx _ _])
99
                       _ _ _ _ _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; trivial.
Robbert Krebbers's avatar
Robbert Krebbers committed
100 101
    { rewrite fill_app /=. iFrame "Hspec Hj Hl"; eauto. }
    rewrite fill_app /=.
102
    iMod (step_if_true _ _ j K _ _ _ with "[Hj]") as "Hj"; trivial.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
    { by iFrame. }
104
    by iIntros "!> {$Hj $Hl}".
105 106 107 108 109
    Unshelve. all:trivial.
  Qed.

  Global Opaque acquire.

110 111
  Lemma steps_release E ρ j K l b:
    nclose specN  E 
112 113
    spec_ctx ρ  l ↦ₛ (#v b)  j  fill K (App release (Loc l))
       |={E}=> j  fill K Unit  l ↦ₛ (#v false).
114
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
115
    iIntros (HNE) "[#Hspec [Hl Hj]]". unfold release.
116 117
    iMod (step_rec _ _ j K with "[Hj]") as "Hj"; eauto; try done.
    iMod (step_store _ _ j K _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
    { by iFrame. }
119
    by iIntros "!> {$Hj $Hl}".
120 121 122 123
    Unshelve. all: trivial.
  Qed.

  Global Opaque release.
Amin Timany's avatar
Amin Timany committed
124

125 126
  Lemma steps_with_lock E ρ j K e l P Q v w:
    nclose specN  E 
127
    ( f, e.[f] = e) (* e is a closed term *) 
128 129 130 131 132
    ( 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).
Amin Timany's avatar
Amin Timany committed
133
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
    iIntros (HNE H1 H2) "[#Hspec [HP [Hl Hj]]]".
135
    iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
136
    asimpl. rewrite H1.
137
    iMod (steps_acquire _ _ j (K ++ [AppRCtx (RecV _)])
138
                   _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
    { rewrite fill_app /=. iFrame "Hspec Hj Hl"; eauto. }
140
    rewrite fill_app; simpl.
141
    iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
142
    asimpl. rewrite H1.
143
    iMod (H2 (K ++ [AppRCtx (RecV _)]) with "[Hj HP]") as "[Hj HQ]"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
    { rewrite fill_app /=. iFrame "Hspec Hj HP"; eauto. }
145
    rewrite ?fill_app /=.
146
    iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
147
    asimpl.
148
    iMod (steps_release _ _ j (K ++ [AppRCtx (RecV _)]) _ _ with "[Hj Hl]")
Amin Timany's avatar
Amin Timany committed
149
      as "[Hj Hl]"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
    { rewrite fill_app /=. by iFrame. }
151
    rewrite ?fill_app /=.
152 153
    iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
    asimpl. iModIntro; by iFrame.
154 155 156
    Unshelve.
    all: try match goal with |- to_val _ = _ => auto using to_of_val end.
    trivial.
Amin Timany's avatar
Amin Timany committed
157 158
  Qed.

159
  Global Opaque with_lock.
160
End proof.