blob: 3b1439edc81864e2a3966cfe7a7d2f91b299451a (
plain)
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
|
// 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 *)
(*
* Warning, crashes with herd7 versions strictly before 7.48.
* spin_islocked is functional from version 7.49.
*
*)
include "cross.cat"
(* From lock reads to their partner lock writes *)
let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po)
let rmw = rmw | lk-rmw
(*
* A paired 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 ; [domain(lk-rmw)]) \ (po-loc ; [UL] ; po-loc)
as lock-nest
(* The litmus test is invalid if an LKW event is not part of an RMW pair *)
flag ~empty LKW \ range(lk-rmw) as unpaired-LKW
(* This will be allowed if we implement spin_is_locked() *)
flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
(* There should be no R or W accesses to spinlocks *)
let ALL-LOCKS = LKR | LKW | UL | LF
flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
(* The final value of a spinlock should not be tested *)
flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
(*
* Backward compatibility
*)
let RL = try RL with emptyset (* defined herd7 >= 7.49 *)
let RU = try RU with emptyset (* defined herd7 >= 7.49 *)
(*
* 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 | RL | 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)
(* rfe for LF events *)
let all-possible-rfe-lf =
(*
* Given an LF event r, compute the possible rfe edges for that event
* (all those starting from LKW events in other threads),
* and then convert that relation to a set of single-edge relations.
*)
let possible-rfe-lf r =
let pair-to-relation p = p ++ 0
in map pair-to-relation ((LKW * {r}) & loc & ext)
(* Do this for each LF event r that isn't in rfi-lf *)
in map possible-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
(* rf for RL events, ie islocked returning true, similar to LF above *)
(* islocked returning true inside a critical section
* must read from the opening lock
*)
let rfi-rl = ([LKW] ; po-loc ; [RL]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
(* islocked returning true outside critical sections can match any
* external lock.
*)
let all-possible-rfe-rl =
let possible-rfe-lf r =
let pair-to-relation p = p ++ 0
in map pair-to-relation ((LKW * {r}) & loc & ext)
in map possible-rfe-lf (RL \ range(rfi-rl))
with rfe-rl from cross(all-possible-rfe-rl)
let rf-rl = rfe-rl | rfi-rl
(* Read from unlock, ie islocked returning false, slightly different *)
(* islocked returning false can read from the last po-previous unlock *)
let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
(* any islocked returning false can read from any external unlock *)
let all-possible-rfe-ru =
let possible-rfe-ru r =
let pair-to-relation p = p ++ 0
in map pair-to-relation (((UL|IW) * {r}) & loc & ext)
in map possible-rfe-ru RU
with rfe-ru from cross(all-possible-rfe-ru)
let rf-ru = rfe-ru | rfi-ru
(* Final rf relation *)
let rf = rf | rf-lf | rf-rl | 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
|
