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
|
// SPDX-License-Identifier: GPL-2.0+
(*
* Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
* Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>
*)
(*
* Generate coherence orders and handle lock operations
*)
include "cross.cat"
(*
* The lock-related events generated by herd7 are as follows:
*
* LKR Lock-Read: the read part of a spin_lock() or successful
* spin_trylock() read-modify-write event pair
* LKW Lock-Write: the write part of a spin_lock() or successful
* spin_trylock() RMW event pair
* UL Unlock: a spin_unlock() event
* LF Lock-Fail: a failed spin_trylock() event
* RL Read-Locked: a spin_is_locked() event which returns True
* RU Read-Unlocked: a spin_is_locked() event which returns False
*
* LKR and LKW events always come paired, like all RMW event sequences.
*
* LKR, LF, RL, and RU are read events; LKR has Acquire ordering.
* LKW and UL are write events; UL has Release ordering.
* LKW, LF, RL, and RU have no ordering properties.
*)
(* Backward compatibility *)
let RL = try RL with emptyset
let RU = try RU with emptyset
(* Treat RL as a kind of LF: a read with no ordering properties *)
let LF = LF | RL
(* There should be no ordinary R or W accesses to spinlocks or SRCU structs *)
let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Sync-srcu
flag ~empty [M \ IW \ ALL-LOCKS] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
(* Link Lock-Reads to their RMW-partner Lock-Writes *)
let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po)
let rmw = rmw | lk-rmw
(* The litmus test is invalid if an LKR/LKW event is not part of an RMW pair *)
flag ~empty LKW \ range(lk-rmw) as unpaired-LKW
flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
(*
* An LKR must always see an unlocked value; spin_lock() calls nested
* inside a critical section (for the same lock) always deadlock.
*)
empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
(*
* In the same way, spin_is_locked() inside a critical section must always
* return True (no RU events can be in a critical section for the same lock).
*)
empty ([LKW] ; po-loc ; [RU]) \ (po-loc ; [UL] ; po-loc) as nested-is-locked
(* The final value of a spinlock should not be tested *)
flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
(*
* Put lock operations in their appropriate classes, but leave UL out of W
* until after the co relation has been generated.
*)
let R = R | LKR | LF | RU
let W = W | LKW
let Release = Release | UL
let Acquire = Acquire | LKR
(* Match LKW events to their corresponding UL events *)
let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
flag ~empty UL \ range(critical) as unmatched-unlock
(* Allow up to one unmatched LKW per location; more must deadlock *)
let UNMATCHED-LKW = LKW \ domain(critical)
empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks
(* rfi for LF events: link each LKW to the LF events in its critical section *)
let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
(* Utility macro to convert a single pair to a single-edge relation *)
let pair-to-relation p = p ++ 0
(*
* If a given LF event e is outside a critical section, it cannot read
* internally but it may read from an LKW event in another thread.
* Compute the relation containing these possible edges.
*)
let possible-rfe-noncrit-lf e = (LKW * {e}) & loc & ext
(* Compute set of sets of possible rfe edges for LF events *)
let all-possible-rfe-lf =
(*
* Convert the possible-rfe-noncrit-lf relation for e
* to a set of single edges
*)
let set-of-singleton-rfe-lf e =
map pair-to-relation (possible-rfe-noncrit-lf e)
(* Do this for each LF event e that isn't in rfi-lf *)
in map set-of-singleton-rfe-lf (LF \ range(rfi-lf))
(* Generate all rf relations for LF events *)
with rfe-lf from cross(all-possible-rfe-lf)
let rf-lf = rfe-lf | rfi-lf
(*
* A given RU event e may read internally from the last po-previous UL,
* or it may read from a UL event in another thread or the initial write.
* Compute the relation containing these possible edges.
*)
let possible-rf-ru e = (((UL * {e}) & po-loc) \
([UL] ; po-loc ; [UL] ; po-loc)) |
(((UL | IW) * {e}) & loc & ext)
(* Compute set of sets of possible rf edges for RU events *)
let all-possible-rf-ru =
(* Convert the possible-rf-ru relation for e to a set of single edges *)
let set-of-singleton-rf-ru e =
map pair-to-relation (possible-rf-ru e)
(* Do this for each RU event e *)
in map set-of-singleton-rf-ru RU
(* Generate all rf relations for RU events *)
with rf-ru from cross(all-possible-rf-ru)
(* Final rf relation *)
let rf = rf | rf-lf | rf-ru
(* Generate all co relations, including LKW events but not UL *)
let co0 = co0 | ([IW] ; loc ; [LKW]) |
(([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW])
include "cos-opt.cat"
let W = W | UL
let M = R | W
(* Merge UL events into co *)
let co = (co | critical | (critical^-1 ; co))+
let coe = co & ext
let coi = co & int
(* Merge LKR events into rf *)
let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)
let rfe = rf & ext
let rfi = rf & int
let fr = rf^-1 ; co
let fre = fr & ext
let fri = fr & int
show co,rf,fr
|
