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