-
Notifications
You must be signed in to change notification settings - Fork 0
/
JSMM_m_scdrf.v
176 lines (168 loc) · 5.87 KB
/
JSMM_m_scdrf.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
(******************************************************************************)
(** * Definition of the JSMM memory model *)
(******************************************************************************)
From hahn Require Import Hahn.
Require Import Arith.
Require Import List.
Require Import Bool.
From imm Require Import Events.
Require Import Execution_m.
Require Import JSMM_m.
Set Implicit Arguments.
Section JSMM_m_scdrf.
Variable G : execution_m.
Variable tot : relation actid.
Variable tearfree : actid -> Prop.
Hypothesis WF : Wf_m G.
Hypothesis CNST : jsmm_m_consistent G tot tearfree.
Hypothesis DRF : data_race_free G.
Notation "'E'" := G.(acts_set).
Notation "'acts'" := G.(acts).
Notation "'lab'" := G.(lab).
Notation "'range_value'" := G.(range_value).
Notation "'rf_on'" := G.(rf_on).
Notation "'overlap_on'" := G.(overlap_on).
Notation "'no_overlap'" := G.(no_overlap).
Notation "'is_overlap'" := G.(is_overlap).
Notation "'rfb'" := G.(rfb).
Notation "'cob'" := G.(cob).
Notation "'sb'" := G.(sb).
Notation "'rf'" := G.(rf).
Notation "'co'" := G.(co).
Notation "'rmw'" := G.(rmw).
(* Notation "'fr'" := G.(fr). *)
(* Notation "'eco'" := G.(eco). *)
Notation "'same_range'" := G.(same_range).
Notation "'same_loc'" := (same_loc lab).
Notation "'R'" := (fun a => is_true (is_r lab a)).
Notation "'W'" := (fun a => is_true (is_w lab a)).
Notation "'F'" := (fun a => is_true (is_f lab a)).
Notation "'Pln'" := (fun a => is_true (is_only_pln lab a)).
Notation "'Rlx'" := (fun a => is_true (is_rlx lab a)).
Notation "'Rel'" := (fun a => is_true (is_rel lab a)).
Notation "'Acq'" := (fun a => is_true (is_acq lab a)).
Notation "'Acqrel'" := (fun a => is_true (is_acqrel lab a)).
Notation "'Acq/Rel'" := (fun a => is_true (is_ra lab a)).
Notation "'Sc'" := (fun a => is_true (is_sc lab a)).
Notation sw := G.(sw).
Notation hb := G.(hb).
Theorem sc_drf :
seqcst G tot.
Proof.
unfold seqcst.
split.
- intro x.
intro H.
destruct H as [y [Hrf Htot]].
assert (hb y x \/ (same_range y x /\ Sc y /\ Sc x)). {
eapply (drf_tot__hb_sc DRF).
- apply CNST.
- apply CNST.
- assumption.
- apply overlap_sym; apply (rf_overlap WF Hrf).
- pose (rf_w_r WF Hrf). intuition.
}
destruct CNST as [CNST1 [CNST2 [CNST3 _]]].
apply (CNST3 y).
exists x.
split; try assumption.
destruct H.
+ assumption.
+ assert (sw x y). { unfold sw. exists x. split. { intuition. } unfold inter_rel. exists y. intuition. }
assert (hb x y). { unfold hb. intuition. }
exfalso. eapply (hb_tot_inconsist CNST1 CNST2 Htot H1).
- intros n x.
unfolder.
intros [x_ [[H11 H12] [y [[H211 H212] [z [H221 H222]]]]]].
destruct CNST as [CNST1 [CNST2 [CNST3 [CNST4 [CNST5 [CNST6 CNST7]]]]]].
rewrite <- H11 in H211, H212.
assert (tot z y). { eapply CNST1. apply H222. apply H211. }
assert (hb z y \/ (same_range z y /\ Sc z /\ Sc y)) as Hzy. {
eapply (drf_tot__hb_sc DRF).
- apply CNST.
- apply CNST.
- apply H.
- apply (rf_overlap WF).
unfold Execution_m.rf_on in H221.
unfold Execution_m.rf.
intros is_nil.
eapply in_nil.
rewrite <- is_nil in H221.
apply H221.
- pose (rf_w_r WF (rf_on_rf _ _ _ _ H221)). left. intuition.
}
assert (hb z y) as Hzy_. {
destruct Hzy as [Hzy1 | Hzy2].
assumption.
apply sw_hb.
apply rf_sw.
apply (rf_on_rf _ _ _ _ H221).
intuition. intuition. intuition.
}
assert (hb x y \/ (same_range x y /\ Sc x /\ Sc y)) as Hxy. {
apply overlap_on_is_overlap in H212.
eapply (drf_tot__hb_sc DRF); try assumption.
- apply CNST.
- apply CNST.
- assumption.
- left. assumption.
}
assert (hb z x \/ (same_range z x /\ Sc z /\ Sc x)) as Hzx. {
eapply (drf_tot__hb_sc DRF). apply CNST. apply CNST. assumption. eapply overlap_on_is_overlap.
eapply overlap_on_trans. apply rf_on_overlap_on. apply WF. apply H221.
apply overlap_on_sym. apply H212. right. assumption.
}
destruct Hxy as [hbxy | [srxy [scx scy]]].
+ destruct Hzx as [hbzx | [srzx [scz scx]]].
* apply (CNST4 n x).
econstructor.
split. apply hbxy.
econstructor.
split. apply H221.
econstructor.
split. {
econstructor.
apply hbzx.
eapply overlap_on_trans.
apply (rf_on_overlap_on _ _ _ WF H221).
apply overlap_on_sym.
apply H212.
}
econstructor. reflexivity. assumption.
* apply CNST6 with x.
econstructor.
split. { econstructor. reflexivity. econstructor; assumption. }
econstructor.
split. apply hbxy.
econstructor.
split. { econstructor. apply Hzy_. eapply rf_on_rf. apply H221. }
repeat econstructor; try assumption.
apply rf_on_rf in H221.
apply rf_w_r in H221.
easy. assumption.
+ destruct Hzx as [hbzx | [srzx [scz scx_]]].
* apply CNST7 with x.
econstructor.
split. { repeat econstructor; assumption. }
econstructor.
split. { econstructor. apply H211. assumption. }
econstructor.
split. { econstructor. reflexivity. repeat econstructor.
apply rf_on_rf in H221. apply rf_w_r in H221. easy. assumption. assumption. }
econstructor.
split. { econstructor. apply Hzy_. eapply rf_on_rf. apply H221. }
assumption.
* apply CNST5 with x.
econstructor.
split. { repeat econstructor; assumption. }
econstructor.
split. { apply H211. }
econstructor.
split. { econstructor. split. repeat econstructor. apply scz.
econstructor. split. econstructor. eapply rf_on_rf. apply H221.
apply same_range_trans with x; assumption. econstructor. reflexivity.
assumption.
}
econstructor. easy. easy.
Qed.
End JSMM_m_scdrf.