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
|
[[sec:herd]]
== Formal Axiomatic Specification in Herd
The tool [.sans-serif]#herd# takes a memory model and a litmus test as
input and simulates the execution of the test on top of the memory
model. Memory models are written in the domain specific language Cat.
This section provides two Cat memory model of RVWMO. The first model,
Figure #fig:herd2[[fig:herd2]], follows the _global memory order_,
Chapter #ch:memorymodel[[ch:memorymodel]], definition of RVWMO, as much
as is possible for a Cat model. The second model,
Figure #fig:herd3[[fig:herd3]], is an equivalent, more efficient,
partial order based RVWMO model.
The simulator [.sans-serif]#herd# is part of the [.sans-serif]#diy# tool
suite — see http://diy.inria.fr for software and documentation. The
models and more are available online
at http://diy.inria.fr/cats7/riscv/.
` `
....
(*************)
(* Utilities *)
(*************)
(* All fence relations *)
let fence.r.r = [R];fencerel(Fence.r.r);[R]
let fence.r.w = [R];fencerel(Fence.r.w);[W]
let fence.r.rw = [R];fencerel(Fence.r.rw);[M]
let fence.w.r = [W];fencerel(Fence.w.r);[R]
let fence.w.w = [W];fencerel(Fence.w.w);[W]
let fence.w.rw = [W];fencerel(Fence.w.rw);[M]
let fence.rw.r = [M];fencerel(Fence.rw.r);[R]
let fence.rw.w = [M];fencerel(Fence.rw.w);[W]
let fence.rw.rw = [M];fencerel(Fence.rw.rw);[M]
let fence.tso =
let f = fencerel(Fence.tso) in
([W];f;[W]) | ([R];f;[M])
let fence =
fence.r.r | fence.r.w | fence.r.rw |
fence.w.r | fence.w.w | fence.w.rw |
fence.rw.r | fence.rw.w | fence.rw.rw |
fence.tso
(* Same address, no W to the same address in-between *)
let po-loc-no-w = po-loc \ (po-loc?;[W];po-loc)
(* Read same write *)
let rsw = rf^-1;rf
(* Acquire, or stronger *)
let AQ = Acq|AcqRel
(* Release or stronger *)
and RL = RelAcqRel
(* All RCsc *)
let RCsc = Acq|Rel|AcqRel
(* Amo events are both R and W, relation rmw relates paired lr/sc *)
let AMO = R & W
let StCond = range(rmw)
(*************)
(* ppo rules *)
(*************)
(* Overlapping-Address Orderings *)
let r1 = [M];po-loc;[W]
and r2 = ([R];po-loc-no-w;[R]) \ rsw
and r3 = [AMO|StCond];rfi;[R]
(* Explicit Synchronization *)
and r4 = fence
and r5 = [AQ];po;[M]
and r6 = [M];po;[RL]
and r7 = [RCsc];po;[RCsc]
and r8 = rmw
(* Syntactic Dependencies *)
and r9 = [M];addr;[M]
and r10 = [M];data;[W]
and r11 = [M];ctrl;[W]
(* Pipeline Dependencies *)
and r12 = [R];(addr|data);[W];rfi;[R]
and r13 = [R];addr;[M];po;[W]
let ppo = r1 | r2 | r3 | r4 | r5 | r6 | r7 | r8 | r9 | r10 | r11 | r12 | r13
....
` `
....
Total
(* Notice that herd has defined its own rf relation *)
(* Define ppo *)
include "riscv-defs.cat"
(********************************)
(* Generate global memory order *)
(********************************)
let gmo0 = (* precursor: ie build gmo as an total order that include gmo0 *)
loc & (W\FW) * FW | # Final write after any write to the same location
ppo | # ppo compatible
rfe # includes herd external rf (optimization)
(* Walk over all linear extensions of gmo0 *)
with gmo from linearizations(M\IW,gmo0)
(* Add initial writes upfront -- convenient for computing rfGMO *)
let gmo = gmo | loc & IW * (M\IW)
(**********)
(* Axioms *)
(**********)
(* Compute rf according to the load value axiom, aka rfGMO *)
let WR = loc & ([W];(gmo|po);[R])
let rfGMO = WR \ (loc&([W];gmo);WR)
(* Check equality of herd rf and of rfGMO *)
empty (rf\rfGMO)|(rfGMO\rf) as RfCons
(* Atomicity axiom *)
let infloc = (gmo & loc)^-1
let inflocext = infloc & ext
let winside = (infloc;rmw;inflocext) & (infloc;rf;rmw;inflocext) & [W]
empty winside as Atomic
....
` `
....
Partial
(***************)
(* Definitions *)
(***************)
(* Define ppo *)
include "riscv-defs.cat"
(* Compute coherence relation *)
include "cos-opt.cat"
(**********)
(* Axioms *)
(**********)
(* Sc per location *)
acyclic co|rf|fr|po-loc as Coherence
(* Main model axiom *)
acyclic co|rfe|fr|ppo as Model
(* Atomicity axiom *)
empty rmw & (fre;coe) as Atomic
....
|
