-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathincsum.v
executable file
·270 lines (243 loc) · 7.03 KB
/
incsum.v
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
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
(*
Project - Proving spec for list sum with concurrent modification
Course: CS 472, Spring 2024, UIC
Author: Himanshu Dongre
*)
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import par.
Section proof.
Context `{!heapGS Σ, !spawnG Σ}.
(**
is_list
Representation predicate in separation logic for a list of integers.
*)
Fixpoint is_list (l : list Z) (v : val) : iProp Σ :=
match l with
| [] => ⌜ v = NONEV ⌝ (* null pointer *)
| x :: l' => ∃ (p : loc), ⌜ v = SOMEV #p ⌝ ∗
∃ v' : val, p ↦ (#x, v') ∗ is_list l' v'
end.
Notation NULL := (InjLV #()).
(* list sum *)
(**
sum_list_coq
Coq-level list sum function
*)
Fixpoint sum_list_coq (l : list Z) :=
match l with
| [] => 0%Z
| h :: t => (h + sum_list_coq t)%Z
end.
(**
sum_list
HeapLang list sum function.
*)
Definition sum_list : val :=
rec: "sum_list" "l" :=
match: "l" with
NONE => #0
| SOME "p" =>
let: "h" := Fst !"p" in
let: "t" := Snd !"p" in
"h" + "sum_list" "t"
end.
(**
sum_list_spec
*)
Lemma sum_list_spec l v :
{{{ is_list l v }}} sum_list v
{{{ RET #(sum_list_coq l); is_list l v }}}.
Proof.
iIntros (Φ) "Hl Post".
iLöb as "IH" forall (l v Φ).
destruct l as [|x l]; simpl; wp_rec.
+ iDestruct "Hl" as %->. wp_match. by iApply "Post".
+ iDestruct "Hl" as (p -> v) "[Hp Hl]". wp_match.
do 2 (wp_load; wp_proj; wp_let).
wp_apply ("IH" with "Hl"). iIntros "Hl". wp_op.
iApply "Post". eauto with iFrame.
Qed.
(* list increase *)
(**
inc_list
A function that increases all elements of a list in-place.
*)
Definition inc_list : val :=
rec: "inc_list" "n" "l" :=
match: "l" with
NONE => #()
| SOME "p" =>
let: "x" := Fst !"p" in
let: "next" := Snd !"p" in
"p" <- ("n" + "x", "next");;
"inc_list" "n" "next"
end.
(**
inc_list_spec
*)
Lemma inc_list_spec n l v :
{{{ is_list l v }}}
inc_list #n v
{{{ RET #(); is_list (map (Z.add n) l) v }}}.
Proof.
iIntros (Ø) "Hl Hpost".
iLöb as "IH" forall (n l v Ø).
unfold inc_list. wp_rec. fold inc_list.
destruct l as [| h t]; simpl.
+ iDestruct "Hl" as %->.
wp_let. wp_match.
iApply "Hpost". auto.
+ iDestruct "Hl" as (p -> v') "(Hp & Hv')".
wp_let. wp_match.
do 2 (wp_load; wp_proj; wp_let).
wp_store.
wp_apply ("IH" with "[$Hv']").
iIntros "H". iApply "Hpost". iFrame. auto.
Qed.
(* spinlock *)
Definition try_acquire : val := λ: "l",
CAS "l" #false #true.
Definition acquire : val :=
rec: "acquire" "l" :=
if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l",
"l" <- #false.
Definition newlock : val := λ: <>,
ref #false.
(**
lock_inv
*)
Definition lock_inv (l : loc) (R : iProp Σ) : iProp Σ :=
(∃ b : bool, l ↦ #b ∗ if b then True else R)%I.
Definition lockN : namespace := nroot .@ "lock".
(**
is_lock
*)
Definition is_lock (lk : val) (R : iProp Σ) : iProp Σ :=
(∃ l: loc, ⌜ lk = #l ⌝ ∧ inv lockN (lock_inv l R))%I.
(**
newlock_spec
*)
Lemma newlock_spec R:
{{{ R }}} newlock #() {{{ lk, RET lk; is_lock lk R }}}.
Proof.
iIntros (Φ) "HR HΦ".
wp_lam. wp_alloc l as "Hl".
iMod (inv_alloc lockN _ (lock_inv l R) with "[HR Hl]") as "#Hinv".
{ iNext. unfold lock_inv. iExists false. iFrame. }
iModIntro. iApply "HΦ". unfold is_lock. iExists l. eauto.
Qed.
(**
try_acquire_spec
*)
Lemma try_acquire_spec lk R :
{{{ is_lock lk R }}} try_acquire lk
{{{ b, RET #b; if b is true then R else True }}}.
Proof.
iIntros (Φ) "#Hl HΦ".
unfold is_lock.
iDestruct "Hl" as (l ->) "#Hinv".
wp_rec.
wp_bind (CmpXchg _ _ _).
iInv lockN as (b) "[Hl HR]" "Hclose".
destruct b.
+ wp_cmpxchg_fail. iMod ("Hclose" with "[Hl]") as "_".
- iNext. iExists true. iFrame.
- iModIntro. wp_proj.
iApply "HΦ". done.
+ wp_cmpxchg_suc.
iMod ("Hclose" with "[$Hl]") as "_".
iModIntro. wp_proj.
iApply "HΦ". done.
Qed.
(**
acquire_spec
*)
Lemma acquire_spec lk R :
{{{ is_lock lk R }}} acquire lk {{{ RET #(); R }}}.
Proof.
iIntros (Φ) "#Hl Hpost".
iLöb as "IH".
wp_rec.
wp_apply (try_acquire_spec with "Hl").
iIntros (b) "HR".
destruct b.
- wp_if_true.
iApply "Hpost"; auto.
- wp_if_false.
wp_apply "IH".
auto.
Qed.
(**
release_spec
*)
Lemma release_spec lk R :
{{{ is_lock lk R ∗ R }}} release lk {{{ RET #(); True }}}.
Proof.
iIntros (Ø) "(#Hpre & HR) Hpost".
unfold is_lock.
iDestruct "Hpre" as (l ->) "#Hinv".
unfold release. wp_lam. Fail wp_store.
iInv lockN as (b) "[H1 H2]" "Hclose".
wp_store.
iMod ("Hclose" with "[$H1 HR]"); auto.
iApply "Hpost". done.
Qed.
(* parallel inc sum *)
Definition parallel_inc_sum_locked (lock : val) : val := λ: "n" "v",
let: "sum" := ref #0 in
((acquire lock;; inc_list "n" "v";; release lock) |||
(acquire lock;; "sum" <- (sum_list "v");; release lock));;
!"sum".
Definition inc_sum_inv (n : Z) (l : list Z) (v : val) :=
(∃ (l' : list Z), ⌜(sum_list_coq l ≤ sum_list_coq l')%Z⌝ ∗ is_list l' v)%I.
Definition incsumN : namespace := nroot .@ "incsum".
Lemma sum_inc_eq_n_len : forall (l : list Z) n,
(sum_list_coq (map (Z.add n) l) = (n * length l) + sum_list_coq l)%Z.
Proof.
intros l n. induction l as [| h t IH]; simpl; lia.
Qed.
Theorem parallel_inc_sum_locked_spec lock l v (n : Z) :
{{{ is_lock lock (inc_sum_inv n l v) ∗ ⌜(0 ≤ n)%Z⌝ }}}
parallel_inc_sum_locked lock #n v
{{{ m, RET #m; ⌜(sum_list_coq l ≤ m)%Z⌝ }}}.
Proof.
iIntros (Ø) "(#Hlock & %Hn) Hpost".
unfold parallel_inc_sum_locked. wp_lam. wp_let.
wp_alloc sum as "Hsum". wp_let.
wp_bind ((acquire lock;; inc_list #n v;; release lock) ||| (acquire lock;; #sum <- sum_list v;; release lock))%E.
wp_smart_apply ((wp_par (fun _ => True)%I (fun _ => (∃ (m : Z), ⌜(sum_list_coq l ≤ m)%Z⌝ ∗ sum ↦ #m))%I) with "[] [Hsum]").
+ wp_apply (acquire_spec with "[Hlock]").
- unfold is_lock. iDestruct "Hlock" as (l0 ->) "Hinv".
iExists l0. iSplit.
{ iPureIntro. done. }
{ done. }
- iIntros "HR". wp_seq.
unfold inc_sum_inv.
iDestruct "HR" as (l') "(%Hl & Hv)".
wp_apply (inc_list_spec with "Hv").
iIntros "Hv". wp_seq.
wp_apply (release_spec with "[$Hlock Hv]").
{ iExists (map (Z.add n) l'). iSplit.
{ iPureIntro.
rewrite sum_inc_eq_n_len.
lia. }
{ done. }}
{ done. }
+ wp_apply (acquire_spec with "[Hlock]"). done.
iIntros "Hv". wp_seq.
unfold is_lock. iDestruct "Hlock" as (l0 ->) "Hinv".
unfold inc_sum_inv. iDestruct "Hv" as (l') "(%Hl & Hv)".
wp_apply (sum_list_spec with "[Hv]"). done.
iIntros "Hv". wp_store.
wp_apply (release_spec with "[Hv]").
- iSplitR.
{ unfold is_lock. iExists l0. iSplit; done. }
{ iExists l'. iFrame. done. }
- iIntros "_". iExists (sum_list_coq l'). iFrame. done.
+ iIntros (v1 v2) "[_ Hm]".
iDestruct "Hm" as (m) "[%Hl Hm]".
iNext. wp_pure _. wp_lam. wp_load.
iApply "Hpost". done.
Qed.