-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathUniqueInits.v
More file actions
293 lines (268 loc) · 10 KB
/
Copy pathUniqueInits.v
File metadata and controls
293 lines (268 loc) · 10 KB
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
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
From Coq Require Import Lia.
From Elo Require Import Core.
From Elo Require Import NoRef.
From Elo Require Import NoInit.
From Elo Require Import ValidTerm.
From Elo Require Import OneInit.
From Elo Require Import NoUninitRefs.
(* ------------------------------------------------------------------------- *)
(* unique-initializers *)
(* ------------------------------------------------------------------------- *)
Definition unique_initializers (m : mem) (ths : threads) := forall ad,
ad < #m ->
(m[ad].t <> None -> forall_threads ths (no_init ad)) /\
(m[ad].t = None -> forone_thread ths (one_init ad) (no_init ad)).
(* lemmas ------------------------------------------------------------------ *)
Corollary noinit_or_oneinit_from_ui : forall ad m ths tid,
forall_threads ths (valid_term m) ->
(* --- *)
unique_initializers m ths ->
no_init ad ths[tid] \/ one_init ad ths[tid].
Proof.
intros * ? Hui. lt_eq_gt ad (#m);
eauto using noinit_from_vtm1, noinit_from_vtm2.
specialize (Hui ad). spec. specialize Hui as [? Hnone].
opt_dec (m[ad].t); spec; auto.
specialize Hnone as [tid' [? ?]]. nat_eq_dec tid' tid; auto.
Qed.
Corollary ui_oneinit_contradiction : forall ad m ths tid1 tid2,
unique_initializers m ths ->
(* --- *)
ad < #m ->
tid1 <> tid2 ->
one_init ad ths[tid1] ->
one_init ad ths[tid2] ->
False.
Proof.
intros * Hui Had **. specialize (Hui ad Had) as [? Hnone].
opt_dec (m[ad].t); spec;
eauto using noinit_oneinit_contradiction.
specialize Hnone as [tid [? ?]].
nat_eq_dec tid1 tid; nat_eq_dec tid2 tid;
eauto using noinit_oneinit_contradiction.
Qed.
Corollary ui_oneinit_equality : forall ad m ths tid1 tid2,
unique_initializers m ths ->
(* --- *)
ad < #m ->
one_init ad ths[tid1] ->
one_init ad ths[tid2] ->
tid1 = tid2.
Proof.
intros. nat_eq_dec tid1 tid2; trivial. exfalso.
eauto using ui_oneinit_contradiction.
Qed.
(* preservation lemmas ----------------------------------------------------- *)
Lemma ui_mem_region : forall m ths ad R,
unique_initializers m ths ->
unique_initializers m[ad.R <- R] ths.
Proof.
intros * H. intros ad' ?. specialize (H ad').
repeat omicron; upsilon; destruct H; trivial;
split; repeat intro; repeat omicron; upsilon; spec; eauto.
Qed.
(* preservation ------------------------------------------------------------ *)
Local Lemma ui_preservation_none : forall m ths tid t,
forall_threads ths (valid_term m) ->
(* --- *)
tid < #ths ->
unique_initializers m ths ->
ths[tid] --[e_none]--> t ->
unique_initializers m ths[tid <- t].
Proof.
intros until 1.
intros ? Hui ? ad Had. specialize (Hui ad Had) as [Hfall Hfone].
split; intros; spec.
- intros ?. omicron; eauto using noinit_preservation_none.
- specialize Hfone as [tid' [? ?]]. exists tid'. split; intros; omicron;
eauto using noinit_preservation_none, oneinit_preservation_none.
Qed.
Local Lemma ui_preservation_alloc : forall m ths tid t T R,
forall_threads ths (valid_term m) ->
(* --- *)
tid < #ths ->
unique_initializers m ths ->
ths[tid] --[e_alloc (#m) T]--> t ->
unique_initializers (m +++ new_cell T R) ths[tid <- t].
Proof.
intros until 1.
intros ? Hui ? ad Had. omicron.
- specialize (Hui ad) as [Hfall Hfone]; trivial.
split; intros; upsilon; spec.
+ intros ?. omicron; eauto using noinit_preservation_alloc.
+ specialize Hfone as [tid' [? ?]]. exists tid'.
assert (ad < #m) by eauto using oneinit_ad_bound.
split; intros; omicron;
eauto using noinit_preservation_alloc, oneinit_preservation_alloc.
- split; intros; upsilon; auto. exists tid. split; intros; sigma;
eauto using noinit_from_vtm1, noinit_to_oneinit.
- lia.
Qed.
Local Lemma ui_preservation_init : forall m ths tid t ad' t',
forall_threads ths (valid_term m) ->
(* --- *)
tid < #ths ->
unique_initializers m ths ->
ths[tid] --[e_init ad' t']--> t ->
unique_initializers m[ad'.t <- t'] ths[tid <- t].
Proof.
intros until 1.
intros ? Hui ? ad Had. sigma. specialize (Hui ad Had) as [Hfall Hfone].
assert (ad < #m) by eauto using vtm_init_address.
opt_dec (m[ad].t); spec; split; intros.
- specialize Hfone as [tid'' [? ?]].
intros tid'. repeat omicron; nat_eq_dec tid'' tid';
auto; eauto using oneinit_to_noinit;
exfalso; eauto using noinit_init_contradiction.
- specialize Hfone as [tid'' [? ?]].
repeat omicron; try discriminate.
exists tid''. split; intros; omicron;
eauto using noinit_preservation_init, oneinit_preservation_init.
- intros tid'. repeat omicron; eauto using noinit_preservation_init.
- omicron; eauto. discriminate.
Qed.
Local Lemma ui_preservation_read : forall m ths tid t ad te,
no_inits te ->
(* --- *)
tid < #ths ->
unique_initializers m ths ->
ths[tid] --[e_read ad te]--> t ->
unique_initializers m ths[tid <- t].
Proof.
intros until 1.
intros ? Hui ? ad' Had'. specialize (Hui ad' Had') as [Hfall Hfone].
split; intros; upsilon; spec.
- intros ?. omicron; eauto using noinit_preservation_read.
- specialize Hfone as [tid' [? ?]]. exists tid'.
split; intros; omicron;
eauto using noinit_preservation_read, oneinit_preservation_read.
Qed.
Local Lemma ui_preservation_write : forall m ths tid t ad te,
forall_threads ths (valid_term m) ->
no_uninitialized_references m ths ->
(* --- *)
tid < #ths ->
unique_initializers m ths ->
ths[tid] --[e_write ad te]--> t ->
unique_initializers m[ad.t <- te] ths[tid <- t].
Proof.
intros until 1. intros Hnur.
intros ? Hui ? ad' Had'. sigma. specialize (Hui ad' Had') as [Hfall Hfone].
assert (ad < #m) by eauto using vtm_write_address.
split; intros; repeat omicron; try discriminate; try spec.
- destruct (_opt_dec m[ad'].t) as [Hmad' | Hmad']; spec.
+ destruct (Hnur ad' Hmad').
exfalso. eauto using noref_write_contradiction.
+ intros ?. omicron; eauto using noinit_preservation_write.
- intros ?. omicron; eauto using noinit_preservation_write.
- specialize Hfone as [tid' [? ?]]. exists tid'; split; intros;
omicron; eauto using noinit_preservation_write, oneinit_preservation_write.
Qed.
Local Lemma ui_preservation_acq : forall m ths tid ad t te,
no_inits te ->
(* --- *)
tid < #ths ->
unique_initializers m ths ->
ths[tid] --[e_acq ad te]--> t ->
unique_initializers m[ad.X <- true] ths[tid <- t].
Proof.
intros until 1.
intros ? Hui ? ad' Had'. sigma. specialize (Hui ad' Had') as [Hfall Hfone].
split; intros; upsilon; spec.
- intros ?. omicron; eauto using noinit_preservation_acq.
- specialize Hfone as [tid' [? ?]]. exists tid'.
split; intros; omicron;
eauto using noinit_preservation_acq, oneinit_preservation_acq.
Qed.
Local Lemma ui_preservation_rel : forall m ths tid ad t,
tid < #ths ->
unique_initializers m ths ->
ths[tid] --[e_rel ad]--> t ->
unique_initializers m[ad.X <- false] ths[tid <- t].
Proof.
intros *.
intros ? Hui ? ad' Had'. sigma. specialize (Hui ad' Had') as [Hfall Hfone].
split; intros; upsilon; spec.
- intros ?. omicron; eauto using noinit_preservation_rel.
- specialize Hfone as [tid' [? ?]]. exists tid'.
split; intros; omicron;
eauto using noinit_preservation_rel, oneinit_preservation_rel.
Qed.
Local Lemma ui_preservation_wacq : forall m ths tid t ad',
tid < #ths ->
unique_initializers m ths ->
ths[tid] --[e_wacq ad']--> t ->
unique_initializers m[ad'.X <- true] ths[tid <- t].
Proof.
intros *.
intros ? Hui ? ad Had. sigma. specialize (Hui ad Had) as [Hfall Hfone].
split; intros; upsilon; spec.
- intros ?. omicron; eauto using noinit_preservation_wacq.
- specialize Hfone as [tid' [? ?]]. exists tid'.
split; intros; omicron;
eauto using noinit_preservation_wacq, oneinit_preservation_wacq.
Qed.
Local Lemma ui_preservation_wrel : forall m ths tid t ad,
tid < #ths ->
unique_initializers m ths ->
ths[tid] --[e_wrel ad]--> t ->
unique_initializers m[ad.X <- false] ths[tid <- t].
Proof.
intros *.
intros ? Hui ? ad' Had'. sigma. specialize (Hui ad' Had') as [Hfall Hfone].
split; intros; upsilon; spec.
- intros ?. omicron; eauto using noinit_preservation_wrel.
- specialize Hfone as [tid' [? ?]]. exists tid'.
split; intros; omicron;
eauto using noinit_preservation_wrel, oneinit_preservation_wrel.
Qed.
Local Lemma ui_preservation_spawn : forall m ths tid t t',
forall_threads ths (valid_term m) ->
(* --- *)
tid < #ths ->
unique_initializers m ths ->
ths[tid] --[e_spawn t']--> t ->
unique_initializers m (ths[tid <- t] +++ t').
Proof.
intros until 1.
intros ? Hui ? ad' Had'. specialize (Hui ad' Had') as [Hfall Hfone].
split; intros; upsilon; spec.
- intros ?. omicron; try constructor;
eauto using noinit_preservation_spawn, noinit_preservation_spawned.
- specialize Hfone as [tid' [? ?]]. exists tid'.
split; intros; omicron; try constructor;
eauto using noinit_preservation_spawn, oneinit_preservation_spawn.
+ invc_oneinit.
+ eauto using noinit_spawn_term.
Qed.
(* ------------------------------------------------------------------------- *)
Theorem ui_preservation_cstep : forall m1 m2 ths1 ths2 tid e,
forall_memory m1 value ->
forall_program m1 ths1 (valid_term m1) ->
no_uninitialized_references m1 ths1 ->
(* --- *)
unique_initializers m1 ths1 ->
m1 \ ths1 ~~[tid, e]~~> m2 \ ths2 ->
unique_initializers m2 ths2.
Proof.
intros * ? [? ?] **. invc_cstep; try invc_mstep.
- eauto using ui_preservation_none.
- sigma. upsilon. eauto using ui_preservation_alloc.
- eauto using ui_preservation_init.
- eauto using noinits_from_value, ui_preservation_read.
- eauto using ui_preservation_write.
- eauto using noinits_from_value, ui_preservation_acq.
- eauto using ui_preservation_rel.
- eauto using ui_preservation_wacq.
- eauto using ui_preservation_wrel.
- eauto using ui_preservation_spawn.
Qed.
Theorem ui_preservation_base : forall t,
no_inits t ->
(* --- *)
unique_initializers nil (base t).
Proof.
unfold base. intros ** ? ?. split; intros Hnil.
- intros ad'. simpl in Hnil. destruct ad; upsilon; auto.
- simpl in Hnil. destruct ad; upsilon; simpl in *; lia.
Qed.