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