-
Notifications
You must be signed in to change notification settings - Fork 9
/
ppo.v
355 lines (320 loc) · 11.6 KB
/
ppo.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
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
(******************************************************************************)
(* PipeCheck: Specifying and Verifying Microarchitectural *)
(* Enforcement of Memory Consistency Models *)
(* *)
(* Copyright (c) 2014 Daniel Lustig, Princeton University *)
(* All rights reserved. *)
(* *)
(* This library is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public *)
(* License as published by the Free Software Foundation; either *)
(* version 2.1 of the License, or (at your option) any later version. *)
(* *)
(* This library is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU *)
(* Lesser General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this library; if not, write to the Free Software *)
(* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 *)
(* USA *)
(******************************************************************************)
Require Import Arith.
Require Import Compare_dec.
Require Import util2.
Require Import adjacency.
Require Import topsort.
Require Import wmm.
Require Import bell.
Require Import dot.
Require Import tree.
Require Import stages.
Require Import globalgraph.
Require Import musthappenbefore.
Require Import Bool.
Require Import List.
Import ListNotations.
Require Import Ascii.
Require Import String.
Fixpoint PerfWRTiAtStage
(l : list PerformStages)
(c : nat)
: option location :=
match l with
| mkPerformStages stg cores vis cli imm :: t =>
if Inb_nat c cores
then Some stg
else PerfWRTiAtStage t c
| [] => None
end.
Fixpoint PerfWRTiBeforePerfWRTj
(po1 po2 : PathOption)
(local_core : nat)
(cores : list nat)
: list (GlobalEvent * GlobalEvent * string) :=
let ps1 := performStages po1 in
let ps2 := performStages po2 in
match cores with
| h::t =>
match (PerfWRTiAtStage ps1 h, PerfWRTiAtStage ps2 local_core) with
| (Some l1, Some l2) =>
((l1, eiid (evt po1)), (l2, eiid (evt po2)), "PPO")
:: PerfWRTiBeforePerfWRTj po1 po2 local_core t
| _ => PerfWRTiBeforePerfWRTj po1 po2 local_core t
end
| [] => []
end.
Definition PPOMustHappenBeforeGlobalEvents
(s : Scenario)
(e1 e2 : nat)
: GraphTree GlobalEvent :=
match (nth_error s e1, nth_error s e2) with
| (Some po1, Some po2) =>
let local_core := proc (iiid (evt po1)) in
let ps1 := performStages po1 in
let all_cores := match last_error ps1 with
| Some (mkPerformStages _ cores _ _ _) => cores
| _ => []
end in
let remote_cores := remove_nat local_core all_cores in
GraphTreeLeaf _ "PPO" (PerfWRTiBeforePerfWRTj po1 po2 local_core remote_cores)
| _ => GraphTreeEmptyLeaf
end.
Definition PPOMustHappenBeforeLocalEvents
(s : Scenario)
(e1 e2 : nat)
: GraphTree GlobalEvent :=
match (nth_error s e1, nth_error s e2) with
| (Some po1, Some po2) =>
let local_core := proc (iiid (evt po1)) in
let ps1 := performStages po1 in
GraphTreeLeaf _ "PPO" (PerfWRTiBeforePerfWRTj po1 po2 local_core [local_core])
| _ => GraphTreeEmptyLeaf
end.
Definition PPOGlobalEvents
(s : Scenario)
(p : Pipeline)
(e1 e2 : nat)
: GraphTree GlobalEvent :=
let dirs := map dirn (map evt s) in
match (nth e1 dirs W, nth e2 dirs W) with
| (R, R) =>
GraphTreeOr _
[PPOMustHappenBeforeGlobalEvents s e1 e2 (*;
PPOSpeculativeLoadReorderEvents s p e1 e2 *)]
| _ => PPOMustHappenBeforeGlobalEvents s e1 e2
end.
Definition PPOLocalEvents
(s : Scenario)
(p : Pipeline)
(e1 e2 : nat)
: GraphTree GlobalEvent :=
let dirs := map dirn (map evt s) in
match (nth e1 dirs W, nth e2 dirs W) with
| (R, R) =>
GraphTreeOr _
[PPOMustHappenBeforeLocalEvents s e1 e2 (*;
PPOSpeculativeLoadReorderEvents s p e1 e2 *)]
| _ => PPOMustHappenBeforeLocalEvents s e1 e2
end.
(** * Verification Scenarios *)
Definition GraphToVerifyPPOGlobalScenario
(p : Pipeline)
(s : Scenario)
(e1 e2 : nat)
: GraphTree GlobalEvent * GraphTree GlobalEvent :=
let g := ScenarioEdges "PPO " p s in
let v := PPOGlobalEvents s p e1 e2 in
(g, v).
Definition GraphToVerifyPPOLocalScenario
(p : Pipeline)
(s : Scenario)
(e1 e2 : nat)
: GraphTree GlobalEvent * GraphTree GlobalEvent :=
let g := ScenarioEdges "PPOLocal " p s in
let v := PPOLocalEvents s p e1 e2 in
(g, v).
Definition VerifyPPOScenario
(g v : GraphTree GlobalEvent)
(p : Pipeline)
: list (string * MHBResult) :=
TreeMustHappenBeforeInAllGraphs (getid p g) (getid p v).
Definition AddTitle
(t : string)
(r : string * MHBResult)
: string * MHBResult :=
let (rn, rr) := r in
(* (append t (append ":" rn), rr) *)
(t, rr).
Fixpoint VerifyPPOGlobalScenarios
(l : list (string * Scenario))
(p : Pipeline)
(e1 e2 : nat)
: list (string * MHBResult) :=
match l with
| (title, h)::t =>
let (g, v) := GraphToVerifyPPOGlobalScenario p h e1 e2 in
let g' := g (* AddCacheEdgesToGraphTree p g e1 e2 *) in
map (AddTitle title) (VerifyPPOScenario g v p)
++ VerifyPPOGlobalScenarios t p e1 e2
| [] => []
end.
Fixpoint VerifyPPOLocalScenarios
(l : list (string * Scenario))
(p : Pipeline)
(e1 e2 : nat)
: list (string * MHBResult) :=
match l with
| (title, h)::t =>
let (g, v) := GraphToVerifyPPOLocalScenario p h e1 e2 in
let g' := g (* AddCacheEdgesToGraphTree p g e1 e2 *) in
map (AddTitle title) (VerifyPPOScenario g v p)
++ VerifyPPOLocalScenarios t p e1 e2
| [] => []
end.
(** * Verification Scenarios *)
Fixpoint GenerateEventsFromDirns'
(l : list Dirn)
(n : nat)
: list Event :=
match l with
| h::t =>
(** Address will be adjusted by [ReplaceLocs] later *)
(** Value will be ignored *)
mkev n (mkiiid 0 n) (Access h 0 0)
:: GenerateEventsFromDirns' t (S n)
| [] => []
end.
Fixpoint GenerateEventsFromDirns
(l : list Dirn)
: list Event :=
GenerateEventsFromDirns' l 0.
(** Replace the [Location] accessed by each [Event] in [le] with the [Location]
in the corresponding position in [ll]. *)
Fixpoint ReplaceLocs
(le : list Event)
(ll : list Location)
: list Event :=
match (le, ll) with
| (mkev eeiid eiiid (Access d _ v) :: et, lh::lt) =>
mkev eeiid eiiid (Access d lh v) :: ReplaceLocs et lt
| _ => []
end.
(** Given a list of [Event]s, return a list of lists of [Event]s in which
the [Location]s accessed by the [Event]s are replaced by each possible
assignment of overlapping vs. non-overlapping [Location]s.
For example, given a list of two [Event]s of directions [R] and [R], return
the the pair of lists (R 0, R 0) and (R 0, R 1), i.e., the overlapping case
and the non-overlapping case. Scenarios with more than two events will have
more than two possibilities. *)
Definition AllLocationCombos
(l : list Event)
: list (list Event) :=
let b := Bell (List.length l) in
map (ReplaceLocs l) b.
Fixpoint ScenarioTitle
(l : list PathOption)
: string :=
match l with
| h::t =>
let h_name := optionName h in
match t with
| _::_ =>
append h_name (append " -> " (ScenarioTitle t))
| [] => h_name
end
| [] => ""
end.
(** [AllScenariosForPO'] calculates the set of all possible [Scenario]s for
a given [Pipeline] and given [dirn]s of [Event]s in program order. *)
Definition AllScenariosForPO'
(pipeline : Pipeline)
(events : list Event)
: list (string * Scenario) :=
let all_paths := map (fun e => pathsFor pipeline e) events in
let f s := (ScenarioTitle s, s) in
map f (CartesianProduct all_paths).
(** [AllScenariosForPOWithAnyAddress] calculates the set of all possible [Scenario]s for
a given [Pipeline] and given [dirn]s of [Event]s in program order. *)
Definition AllScenariosForPOWithAnyAddress
(pipeline : Pipeline)
(program_order : list Dirn)
: list (string * Scenario) :=
let program_order' := GenerateEventsFromDirns program_order in
let program_orders := AllLocationCombos program_order' in
let f po := AllScenariosForPO' pipeline po in
fold_left (app (A:=_)) (map f program_orders) [].
Definition AllScenariosForPOWithSameAddress
(pipeline : Pipeline)
(program_order : list Dirn)
: list (string * Scenario) :=
let program_order' := GenerateEventsFromDirns program_order in
AllScenariosForPO' pipeline program_order'.
Definition VerifyPPOWithAnyAddresses
(pipeline : Pipeline)
(program_order : list Dirn)
(e1 e2 : nat)
: list (string * MHBResult) :=
let scenarios := AllScenariosForPOWithAnyAddress pipeline program_order in
VerifyPPOGlobalScenarios scenarios pipeline e1 e2.
Definition VerifyPPOWithSameAddress
(pipeline : Pipeline)
(program_order : list Dirn)
(e1 e2 : nat)
: list (string * MHBResult) :=
let scenarios := AllScenariosForPOWithSameAddress pipeline program_order in
VerifyPPOLocalScenarios scenarios pipeline e1 e2.
Definition GraphOfPPOVerificationResult
(pipeline : Pipeline)
(e1 e2 : nat)
(tr : string * MHBResult)
: string * string :=
let (t, r) := tr in
let f x := GlobalEventString pipeline (ungeid pipeline x) in
(fold_left append [pipename pipeline; ": PPO: "; t] "",
match r with
| MustHappenBefore g p =>
dot_graph
(fold_left append ["PPO Verified: "; pipename pipeline; ": "; t] "") g
(ungeid pipeline) f p (PairConsecutive p) (List.length (stages pipeline))
| Unverified g s d =>
dot_graph
(fold_left append ["PPO Unverified! "; pipename pipeline; ": "; t] "") g
(ungeid pipeline) f [s; d] [] (List.length (stages pipeline))
| Cyclic g p =>
dot_graph
(fold_left append ["PPO Ruled out (cyclic): "; pipename pipeline; ": "; t] "") g
(ungeid pipeline) f p (PairConsecutive p) (List.length (stages pipeline))
end).
Definition GraphsToVerifyPPOWithAnyAddresses
(pipeline : Pipeline)
(program_order : list Dirn)
(e1 e2 : nat)
: list (string * string) :=
let lv := VerifyPPOWithAnyAddresses pipeline program_order e1 e2 in
map (GraphOfPPOVerificationResult pipeline e1 e2) lv.
Definition GraphsToVerifyPPOWithSameAddress
(pipeline : Pipeline)
(program_order : list Dirn)
(e1 e2 : nat)
: list (string * string) :=
let lv := VerifyPPOWithSameAddress pipeline program_order e1 e2 in
map (GraphOfPPOVerificationResult pipeline e1 e2) lv.
Module EdgesExample5.
Import EdgesExample.
Import EdgesExample2.
Import EdgesExample3.
Definition SampleValidation :=
GraphsToVerifyPPOWithAnyAddresses my_pipeline [W; R; R; W] 0 3.
End EdgesExample5.
Definition GraphsToVerifyTSOPPO
(pipeline : Pipeline)
: list (string * string) :=
GraphsToVerifyPPOWithAnyAddresses pipeline [R; R] 0 1 ++
GraphsToVerifyPPOWithAnyAddresses pipeline [R; W] 0 1 ++
GraphsToVerifyPPOWithAnyAddresses pipeline [W; W] 0 1 ++
GraphsToVerifyPPOWithSameAddress pipeline [R; R] 0 1 ++
GraphsToVerifyPPOWithSameAddress pipeline [R; W] 0 1 ++
GraphsToVerifyPPOWithSameAddress pipeline [W; R] 0 1 ++
GraphsToVerifyPPOWithSameAddress pipeline [W; W] 0 1.