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