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
|
\section{Formal Axiomatic Specification in Herd}
\label{sec:herd}
The tool \textsf{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 \textsc{Cat}. This section provides two \textsc{Cat} memory model of RVWMO. The first model, Figure~\ref{fig:herd2}, follows the \emph{global memory order}, Chapter~\ref{ch:memorymodel}, definition of~RVWMO, as much as is possible for a \textsc{Cat} model. The second model, Figure~\ref{fig:herd3}, is an equivalent, more efficient, partial order based RVWMO model.
The simulator~\textsf{herd} is part of the \textsf{diy} tool suite --- see \url{http://diy.inria.fr} for software and documentation. The models and more are available online at~\url{http://diy.inria.fr/cats7/riscv/}.
\begin{figure}[h!]
{
\tt\bfseries\centering\footnotesize
\begin{lstlisting}
(*************)
(* 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
\end{lstlisting}
}
\caption{{\tt riscv-defs.cat}, a herd definition of preserved program order (1/3)}
\label{fig:herd1}
\end{figure}
\begin{figure}[ht!]
{
\tt\bfseries\centering\footnotesize
\begin{lstlisting}
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
\end{lstlisting}
}
\caption{{\tt riscv.cat}, a herd version of the RVWMO memory model (2/3)}
\label{fig:herd2}
\end{figure}
\begin{figure}[h!]
{
\tt\bfseries\centering\footnotesize
\begin{lstlisting}
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
\end{lstlisting}
}
\caption{{\tt riscv.cat}, an alternative herd presentation of the RVWMO memory model (3/3)}
\label{fig:herd3}
\end{figure}
|
