lock.v 6.15 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2
From iris_logrel.F_mu_ref_conc Require Import tactics rel_tactics.
3
From iris_logrel.F_mu_ref_conc Require Export rules_binary typing fundamental_binary relational_properties notation.
4
From iris.base_logic Require Import namespaces.
5

Dan Frumin's avatar
Dan Frumin committed
6
(** [newlock = alloc false] *)
7
Definition newlock : expr := Alloc (# false).
Dan Frumin's avatar
Dan Frumin committed
8
(** [acquire = λ x. if cas(x, false, true) then #() else acquire(x) ] *)
9 10 11 12 13
Definition acquire : val :=
  RecV "acquire" "x"
       (If (CAS "x" (# false) (# true))
           (Unit)
           (App "acquire" "x")).
14

15 16 17 18 19 20 21
(** [release = λ x. x <- false] *)
Definition release : val := LamV "x" (Store "x" (# false)).
(** [with_lock e l = λ x. (acquire l) ;; e x ;; (release l)] *)
Definition with_lock : val := λ: "e" "l" "x",
  acquire "l";;
  Let "v" ("e" "x")
    (release "l";; "v").
22

23 24
Instance newlock_closed: Closed  newlock.
Proof. rewrite /newlock. solve_closed. Qed.
25 26 27

Definition LockType := Tref TBool.

Dan Frumin's avatar
Dan Frumin committed
28 29
Hint Unfold LockType : typeable.

30
Lemma newlock_type Γ : typed Γ newlock LockType.
Dan Frumin's avatar
Dan Frumin committed
31
Proof. eauto with typeable. Qed.
32 33

Lemma acquire_type Γ : typed Γ acquire (TArrow LockType TUnit).
Dan Frumin's avatar
Dan Frumin committed
34
Proof. unfold acquire. eauto 10 with typeable. Qed.
35 36

Lemma release_type Γ : typed Γ release (TArrow LockType TUnit).
Dan Frumin's avatar
Dan Frumin committed
37
Proof. unfold release. eauto with typeable. Qed.
38

39 40 41
Opaque acquire.
Opaque release.

Dan Frumin's avatar
Dan Frumin committed
42 43 44
Hint Resolve newlock_type : typeable.
Hint Resolve release_type : typeable.
Hint Resolve acquire_type : typeable.
45 46 47 48

Lemma with_lock_type Γ τ τ' :
  typed Γ with_lock (TArrow (TArrow τ τ') (TArrow LockType (TArrow τ τ'))).
Proof.
Dan Frumin's avatar
Dan Frumin committed
49
  unfold with_lock. unlock. eauto 25 with typeable.
50 51
Qed.

Dan Frumin's avatar
Dan Frumin committed
52 53
Hint Resolve with_lock_type : typeable.

54
Section proof.
55
  Context `{logrelG Σ}.
56 57 58 59
  Variable (E1 E2 : coPset).

  Lemma steps_newlock ρ j K
    (Hcl : nclose specN  E1) :
60
    spec_ctx ρ - j  fill K newlock
61
    ={E1}=  l, j  fill K (Loc l)  l ↦ₛ (#v false).
62
  Proof.
63
    iIntros "#Hspec Hj".
64 65
    tp_alloc j as l "Hl". tp_normalise j.
    by iExists _; iFrame.
66 67
  Qed.

68 69 70 71
  Lemma bin_log_related_newlock_r Γ K t τ 
    (Hcl : nclose specN  E1) :
    ( l : loc, l ↦ₛ (#v false) - {E1,E2;Γ}  t log fill K (Loc l) : τ)%I
    - {E1,E2;Γ}  t log fill K newlock : τ.
72 73
  Proof.
    iIntros "Hlog".
74
    unfold newlock.
75 76
    rel_alloc_r as l "Hl".
    iApply ("Hlog" with "Hl").
77 78
  Qed.

79
  Global Opaque newlock.
80 81
  
  Transparent acquire. 
82 83
  Lemma steps_acquire ρ j K l
    (Hcl : nclose specN  E1) :
84
    spec_ctx ρ - l ↦ₛ (#v false) - j  fill K (App acquire (Loc l))
85
    ={E1}= j  fill K (Lit Unit)  l ↦ₛ (#v true).
86
  Proof.
87
    iIntros "#Hspec Hl Hj". 
88
    unfold acquire.
89
    tp_rec j.
90
    tp_cas_suc j. 
91
    tp_if_true j.
92
    by iFrame.
93
  Qed.
94
  
95 96
  Lemma bin_log_related_acquire_r Γ K l t τ
    (Hcl : nclose specN  E1) :
97
    l ↦ₛ (#v false) -
98
    (l ↦ₛ (#v true) - {E1,E2;Γ}  t log fill K (Lit Unit) : τ)%I
99
    - {E1,E2;Γ}  t log fill K (App acquire (Loc l)) : τ.
100 101
  Proof.
    iIntros "Hl Hlog".
102
    rel_rec_r.
103
    rel_cas_suc_r. simpl.
104
    rel_if_r.
105
    by iApply "Hlog".
106 107
  Qed.
  
108 109
  Global Opaque acquire.

110
  Transparent release.
111 112
  Lemma steps_release ρ j K l b
    (Hcl : nclose specN  E1) :
113
    spec_ctx ρ - l ↦ₛ (#v b) - j  fill K (App release (Loc l))
114
    ={E1}= j  fill K (Lit Unit)  l ↦ₛ (#v false).
115
  Proof.
116
    iIntros "#Hspec Hl Hj". unfold release.
117 118 119
    tp_rec j.
    tp_store j. tp_normalise j.
    by iFrame.
120 121
  Qed.

122 123
  Lemma bin_log_related_release_r Γ K l t τ b
    (Hcl : nclose specN  E1) :
124
    l ↦ₛ (#v b) -
125
    (l ↦ₛ (#v false) - {E1,E2;Γ}  t log fill K (Lit Unit) : τ)%I
126
    - {E1,E2;Γ}  t log fill K (App release (Loc l)) : τ.
127 128
  Proof.
    iIntros "Hl Hlog".
129
    unfold release.
130 131 132
    rel_rec_r.
    rel_store_r.
    by iApply "Hlog".
133 134
  Qed.

135
  Global Opaque release.
136

137
  Lemma steps_with_lock ρ j K e ev l P Q v w:
138
    to_val e = Some ev 
139
    ( K', spec_ctx ρ - P - j  fill K' (App e (of_val w))
140 141
            ={E1}= j  fill K' (of_val v)  Q) 
    (nclose specN  E1) 
142 143
    spec_ctx ρ - P - l ↦ₛ (#v false)
    - j  fill K (App (with_lock e (Loc l)) (of_val w))
144
    ={E1}= j  fill K (of_val v)  Q  l ↦ₛ (#v false).
145
  Proof.
146
    iIntros (Hev Hpf ?) "#Hspec HP Hl Hj".
147
    unfold with_lock. unlock. (* TODO :( *)
148 149 150
    tp_rec j.
    tp_rec j.
    tp_rec j; eauto using to_of_val.
151
    tp_bind j (App acquire (Loc l)).
Dan Frumin's avatar
Dan Frumin committed
152
    tp_apply j steps_acquire with "Hl" as "Hl".
153
    tp_rec j.
154
    tp_bind j (App e _).
155
    iMod (Hpf with "Hspec HP Hj") as "[Hj HQ]". 
156
    tp_normalise j.
157
    tp_rec j; eauto using to_of_val.
158
    tp_bind j (App release _).    
Dan Frumin's avatar
Dan Frumin committed
159
    tp_apply j steps_release with "Hl" as "Hl".
160
    tp_normalise j.
161
    tp_rec j.
162
    by iFrame.
163
  Qed.
164
  
165
  Lemma bin_log_related_with_lock_r Γ K Q e ev ew cl v w l t τ :
166
    (to_val e = Some cl) 
167 168
    (to_val ev = Some v) 
    (to_val ew = Some w) 
169
    (nclose specN  E1) 
170 171 172 173
    ( K, (Q - {E1,E2;Γ}  t log fill K ev : τ) -
        {E1,E2;Γ}  t log fill K (App e ew) : τ) -
    l ↦ₛ (#v false) -
    (Q - l ↦ₛ (#v false) - {E1,E2;Γ}  t log fill K ev : τ)%I
174
    - {E1,E2;Γ}  t log fill K (with_lock e (Loc l) ew) : τ.
175
  Proof.
176 177 178
    iIntros (????) "HA Hl Hlog".
    rel_bind_r (with_lock e).
    unfold with_lock. unlock. (*TODO: unlock here needed *)
179
    iApply (bin_log_related_rec_r); eauto. simpl_subst.
180
    rel_bind_r (App _ (#l)%E).
181 182
    iApply (bin_log_related_rec_r); eauto. simpl_subst.
    iApply (bin_log_related_rec_r); eauto. simpl_subst.
183
    rel_bind_r (App acquire (Loc l)).
184
    iApply (bin_log_related_acquire_r Γ (_ :: K) l with "Hl"); auto.
185
    iIntros "Hl". simpl.
186
    iApply (bin_log_related_rec_r); eauto. simpl_subst/=.
187
    rel_bind_r (App e ew).
188
    iApply "HA". iIntros "HQ". simpl.
189
    iApply (bin_log_related_rec_r); eauto. simpl_subst.
190 191
    rel_bind_r (App release _).
    iApply (bin_log_related_release_r with "Hl"); eauto.
192
    iIntros "Hl". simpl.
193
    iApply (bin_log_related_rec_r); eauto. simpl_subst.
194 195 196
    iApply ("Hlog" with "HQ Hl").
  Qed.

197
End proof.