-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathSafetyLemmas.v
223 lines (209 loc) · 8.91 KB
/
SafetyLemmas.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
From Elo Require Import Core.
From Elo Require Import SyntacticProperties.
From Elo Require Import TypeProperties.
From Elo Require Import Multistep.
(*
(* ------------------------------------------------------------------------- *)
(* one-cr inheritance *)
(* ------------------------------------------------------------------------- *)
Lemma onecr_inheritance_cstep :
forall ad m1 m2 ths1 ths2 tid tid' e,
invariants m1 ths1 ->
invariants m2 ths2 ->
(* --- *)
one_cr ad ths2[tid] ->
m1 \ ths1 ~~[tid', e]~~> m2 \ ths2 ->
exists t, (e <> e_acq ad t /\ one_cr ad ths1[tid]) \/
(e = e_acq ad t /\ tid' = tid).
Proof.
intros.
assert (forall_memory m1 value) by eauto with inva.
assert (forall_memory m1 (valid_term m1)) by eauto with inva.
assert (forall_threads ths1 (valid_term m1)) by eauto with inva.
assert (unique_holding m1 ths1) by eauto with inva.
assert (Huh : unique_holding m2 ths2) by eauto with inva.
assert (forall_threads ths1 term_init_cr_exc) by eauto with inva.
assert (H' : forall_threads ths2 term_init_cr_exc) by eauto with inva.
invc_cstep; try invc_mstep.
- exists <{unit}>. left. split. 1: intros F; invc F.
omicron; eauto using onecr_inheritance_none.
- exists <{unit}>. left. split. 1: intros F; invc F.
omicron; eauto using onecr_inheritance_alloc.
- exists <{unit}>. left. split. 1: intros F; invc F.
omicron; eauto using onecr_inheritance_init.
- exists <{unit}>. left. split. 1: intros F; invc F.
omicron; eauto using nocr_from_value, onecr_inheritance_read.
- exists <{unit}>. left. split. 1: intros F; invc F.
omicron; eauto using onecr_inheritance_write.
- exists t'. omicron.
+ left. split.
* intros F. invc F. auto.
* omicron; eauto using nocrs_from_value, onecr_inheritance_acq.
+
+ nat_eq_dec ad' ad; eauto.
assert (term_init_cr_exc t) by (specialize (H' tid); sigma; trivial).
assert (no_cr ad' ths1[tid]) by eauto using nocr_from_acq with inva.
assert (one_cr ad ths1[tid <- t][tid']) by (sigma; trivial).
assert (one_cr ad ths1[tid <- t][tid]) by (sigma; trivial).
match goal with _ : _ --[_]--> ?t |- _ =>
(* assert (one_cr ad t) by eauto using nocr_to_onecr, nocrs_from_value; *)
assert (one_cr ad ths1[tid' <- t][tid']) by (sigma; trivial);
assert (one_cr ad ths1[tid' <- t][tid]) by (sigma; trivial)
end.
exfalso. eauto using uh_onecr_contradiction.
+ left. split.
* intros F. invc F. auto.
* omicron; eauto using nocrs_from_value, onecr_inheritance_acq.
- exists <{unit}>. left. split. 1: intros F; invc F.
match goal with _ : _ --[e_rel ?ad']--> _ |- _ => nat_eq_dec ad' ad end;
omicron; eauto using onecr_inheritance_rel.
exfalso.
eauto using onecr_from_rel, onecr_to_nocr, nocr_onecr_contradiction.
- exists <{unit}>. left. split. 1: intros F; invc F.
omicron; eauto using onecr_inheritance_spawn.
exfalso. eauto using nocr_spawn_term, nocr_onecr_contradiction.
Qed.
*)
(* ------------------------------------------------------------------------- *)
(* initialized preservation *)
(* ------------------------------------------------------------------------- *)
Lemma initialized_preservation_cstep : forall m1 m2 ths1 ths2 tid e ad t,
m1[ad].t = Some t ->
m1 \ ths1 ~~[tid, e]~~> m2 \ ths2 ->
exists t', m2 [ad].t = Some t'.
Proof.
intros.
assert (ad < #m1) by (lt_eq_gt ad (#m1); sigma; upsilon; eauto).
invc_cstep; try invc_mstep; sigma; eauto;
omicron; upsilon; eauto.
Qed.
Lemma initialized_preservation_ustep : forall m1 m2 ths1 ths2 tc ad t,
m1[ad].t = Some t ->
m1 \ ths1 ~~[tc]~~>* m2 \ ths2 ->
exists t', m2 [ad].t = Some t'.
Proof.
intros. ind_ustep; eauto.
destruct IHmultistep; trivial.
eauto using initialized_preservation_cstep.
Qed.
(* ------------------------------------------------------------------------- *)
(* one-init preservation *)
(* ------------------------------------------------------------------------- *)
Lemma oneinit_preservation_cstep :
forall ad m1 m2 ths1 ths2 tid tid' e,
invariants m1 ths1 ->
invariants m2 ths2 ->
(* --- *)
one_init ad ths1[tid] ->
m1 \ ths1 ~~[tid', e]~~> m2 \ ths2 ->
(forall t, e <> e_init ad t /\ one_init ad ths2[tid]) \/
(exists t, e = e_init ad t /\ tid' = tid /\ m2[ad].t = Some t).
Proof.
intros.
assert (forall_memory m1 value) by eauto with inva.
assert (forall_memory m1 (valid_term m1)) by eauto with inva.
assert (forall_threads ths1 (valid_term m1)) by eauto with inva.
assert (forall_threads ths1 (consistent_term m1)) by eauto with inva.
assert (unique_initializers m1 ths1) by eauto with inva.
invc_cstep; try invc_mstep.
- left. intros. split; eauto.
omicron; eauto using oneinit_preservation_none.
- left. split; try omicron; auto; try congruence.
assert (ad < #m1) by eauto using oneinit_ad_bound.
eauto using oneinit_preservation_alloc.
- match goal with _ : _ --[e_init ?x _]--> _ |- _ => rename x into ad' end.
nat_eq_dec ad' ad.
+ assert (ad < #m1) by eauto using vtm_init_address.
right. repeat eexists; sigma; upsilon; trivial.
eauto using oneinit_from_init, ui_oneinit_equality.
+ left. intros. split; auto.
omicron; eauto using oneinit_preservation_init.
- left. split; auto; try congruence.
omicron; eauto using noinits_from_value, oneinit_preservation_read.
- left. split; auto; try congruence.
omicron; eauto using oneinit_preservation_write.
- left. split; auto.
omicron; eauto using noinits_from_value, oneinit_preservation_acq.
- left. split; auto.
omicron; eauto using oneinit_preservation_rel.
- left. split; auto; try congruence.
omicron; eauto using oneinit_preservation_wacq.
- left. split; auto; try congruence.
omicron; eauto using oneinit_preservation_wrel.
- left. split; auto; try congruence.
omicron; eauto using oneinit_preservation_spawn.
invc_oneinit.
Qed.
Lemma oneinit_preservation_ustep :
forall tc m1 m2 ths1 ths2 ad tid,
invariants m1 ths1 ->
invariants m2 ths2 ->
(* --- *)
one_init ad ths1[tid] ->
m1 \ ths1 ~~[tc]~~>* m2 \ ths2 ->
one_init ad ths2[tid] \/ exists t, m2[ad].t = Some t.
Proof.
intros. ind_ustep; auto.
match goal with _ : ?m \ ?ths ~~[?tid, _]~~> ?m' \ ?ths' |- _ =>
rename tid into tid';
rename m' into m3; rename ths' into ths3;
rename m into m2; rename ths into ths2
end.
assert (invariants m2 ths2) by eauto using invariants_preservation_ustep.
destruct IHmultistep as [? | [? ?]]; trivial.
- assert (
(forall t, e <> e_init ad t /\ one_init ad ths3[tid]) \/
(exists t, e = e_init ad t /\ tid' = tid /\ m3[ad].t = Some t)
) as [H' | [t' [? [? ?]]]]
by eauto using oneinit_preservation_cstep.
+ specialize (H' <{unit}>) as [? ?]. eauto.
+ subst. eauto.
- right. eauto using initialized_preservation_cstep.
Qed.
(*
(* ------------------------------------------------------------------------- *)
(* one-cr preservation *)
(* ------------------------------------------------------------------------- *)
Lemma onecr_preservation_rstep :
forall ad m1 m2 ths1 ths2 tid tid' e,
invariants m1 ths1 ->
invariants m2 ths2 ->
(* --- *)
one_cr ad ths1[tid] ->
m1 \ ths1 ~~~[tid', e]~~> m2 \ ths2 ->
(e <> e_rel ad /\ one_cr ad ths2[tid]) \/
(e = e_rel ad /\ tid' = tid).
Proof.
intros.
assert (forall_memory m1 value) by eauto with inva.
assert (forall_memory m1 (valid_term m1)) by eauto with inva.
assert (forall_threads ths1 (valid_term m1)) by eauto with inva.
assert (unique_critical_regions m1 ths1) by eauto with inva.
invc_rstep; invc_cstep; try invc_mstep.
- left. split; auto.
omicron; eauto using onecr_preservation_none.
- left. split; auto.
omicron; eauto using onecr_preservation_alloc.
- left. split; auto.
omicron; eauto using onecr_preservation_init.
- left. split; auto.
omicron; eauto using nocrs_from_value, onecr_preservation_read.
- left. split; auto.
omicron; eauto using onecr_preservation_write.
- left. split; auto.
match goal with _ : _ --[e_acq ?ad ?t]--> _ |- _ =>
rename ad into ad'; rename t into t'
end.
nat_eq_dec ad ad'; omicron; auto.
+ assert (Htrue : m1[ad'].X = true) by eauto using locked_from_onecr.
rewrite Htrue in *. auto.
+ eauto 6 using nocr_from_nocrs, nocrs_from_value, onecr_preservation_acq.
- match goal with _ : _ --[e_rel ?ad]--> _ |- _ => rename ad into ad' end.
nat_eq_dec ad ad'.
+ right. split; eauto using onecr_from_rel, ucr_onecr_equality.
+ left; split; try omicron; eauto using onecr_preservation_rel.
- left. split; auto.
omicron; eauto using onecr_preservation_spawn.
invc_onecr.
Qed.
*)