1 // SPDX-License-Identifier: GPL-2.0+
2 (*
3 * Copyright (C) 2016 Luc Maranget <luc.marange
4 * Copyright (C) 2017 Alan Stern <stern@rowland
5 *)
6
7 (*
8 * Generate coherence orders and handle lock o
9 *)
10
11 include "cross.cat"
12
13 (*
14 * The lock-related events generated by herd7
15 *
16 * LKR Lock-Read: the read part of a
17 * spin_trylock() read-mo
18 * LKW Lock-Write: the write part of
19 * spin_trylock() RMW eve
20 * UL Unlock: a spin_unlock() event
21 * LF Lock-Fail: a failed spin_trylo
22 * RL Read-Locked: a spin_is_locked(
23 * RU Read-Unlocked: a spin_is_locke
24 *
25 * LKR and LKW events always come paired, like
26 *
27 * LKR, LF, RL, and RU are read events; LKR ha
28 * LKW and UL are write events; UL has Release
29 * LKW, LF, RL, and RU have no ordering proper
30 *)
31
32 (* Backward compatibility *)
33 let RL = try RL with emptyset
34 let RU = try RU with emptyset
35
36 (* Treat RL as a kind of LF: a read with no or
37 let LF = LF | RL
38
39 (* There should be no ordinary R or W accesses
40 let ALL-LOCKS = LKR | LKW | UL | LF | RU | Src
41 flag ~empty [M \ IW \ ALL-LOCKS] ; loc ; [ALL-
42
43 (* Link Lock-Reads to their RMW-partner Lock-W
44 let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ;
45 let rmw = rmw | lk-rmw
46
47 (* The litmus test is invalid if an LKR/LKW ev
48 flag ~empty LKW \ range(lk-rmw) as unpaired-LK
49 flag ~empty LKR \ domain(lk-rmw) as unpaired-L
50
51 (*
52 * An LKR must always see an unlocked value; s
53 * inside a critical section (for the same loc
54 *)
55 empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL
56
57 (*
58 * In the same way, spin_is_locked() inside a
59 * return True (no RU events can be in a criti
60 *)
61 empty ([LKW] ; po-loc ; [RU]) \ (po-loc ; [UL]
62
63 (* The final value of a spinlock should not be
64 flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-f
65
66 (*
67 * Put lock operations in their appropriate cl
68 * until after the co relation has been genera
69 *)
70 let R = R | LKR | LF | RU
71 let W = W | LKW
72
73 let Release = Release | UL
74 let Acquire = Acquire | LKR
75
76 (* Match LKW events to their corresponding UL
77 let critical = ([LKW] ; po-loc ; [UL]) \ (po-l
78
79 flag ~empty UL \ range(critical) as unmatched-
80
81 (* Allow up to one unmatched LKW per location;
82 let UNMATCHED-LKW = LKW \ domain(critical)
83 empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]
84
85 (* rfi for LF events: link each LKW to the LF
86 let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW]
87
88 (* Utility macro to convert a single pair to a
89 let pair-to-relation p = p ++ 0
90
91 (*
92 * If a given LF event e is outside a critical
93 * internally but it may read from an LKW even
94 * Compute the relation containing these possi
95 *)
96 let possible-rfe-noncrit-lf e = (LKW * {e}) &
97
98 (* Compute set of sets of possible rfe edges f
99 let all-possible-rfe-lf =
100 (*
101 * Convert the possible-rfe-noncrit-lf
102 * to a set of single edges
103 *)
104 let set-of-singleton-rfe-lf e =
105 map pair-to-relation (
106 (* Do this for each LF event e that is
107 in map set-of-singleton-rfe-lf (LF \ r
108
109 (* Generate all rf relations for LF events *)
110 with rfe-lf from cross(all-possible-rfe-lf)
111 let rf-lf = rfe-lf | rfi-lf
112
113 (*
114 * A given RU event e may read internally from
115 * or it may read from a UL event in another t
116 * Compute the relation containing these possi
117 *)
118 let possible-rf-ru e = (((UL * {e}) & po-loc)
119 ([UL] ; po-loc ; [UL]
120 (((UL | IW) * {e}) & loc & ext
121
122 (* Compute set of sets of possible rf edges fo
123 let all-possible-rf-ru =
124 (* Convert the possible-rf-ru relation
125 let set-of-singleton-rf-ru e =
126 map pair-to-relation (possible
127 (* Do this for each RU event e *)
128 in map set-of-singleton-rf-ru RU
129
130 (* Generate all rf relations for RU events *)
131 with rf-ru from cross(all-possible-rf-ru)
132
133 (* Final rf relation *)
134 let rf = rf | rf-lf | rf-ru
135
136 (* Generate all co relations, including LKW ev
137 let co0 = co0 | ([IW] ; loc ; [LKW]) |
138 (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UN
139 include "cos-opt.cat"
140 let W = W | UL
141 let M = R | W
142
143 (* Merge UL events into co *)
144 let co = (co | critical | (critical^-1 ; co))+
145 let coe = co & ext
146 let coi = co & int
147
148 (* Merge LKR events into rf *)
149 let rf = rf | ([IW | UL] ; singlestep(co) ; lk
150 let rfe = rf & ext
151 let rfi = rf & int
152
153 let fr = rf^-1 ; co
154 let fre = fr & ext
155 let fri = fr & int
156
157 show co,rf,fr
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.