0001 // SPDX-License-Identifier: GPL-2.0+
0002 (*
0003 * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
0004 * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>
0005 *)
0006
0007 (*
0008 * Generate coherence orders and handle lock operations
0009 *)
0010
0011 include "cross.cat"
0012
0013 (*
0014 * The lock-related events generated by herd7 are as follows:
0015 *
0016 * LKR Lock-Read: the read part of a spin_lock() or successful
0017 * spin_trylock() read-modify-write event pair
0018 * LKW Lock-Write: the write part of a spin_lock() or successful
0019 * spin_trylock() RMW event pair
0020 * UL Unlock: a spin_unlock() event
0021 * LF Lock-Fail: a failed spin_trylock() event
0022 * RL Read-Locked: a spin_is_locked() event which returns True
0023 * RU Read-Unlocked: a spin_is_locked() event which returns False
0024 *
0025 * LKR and LKW events always come paired, like all RMW event sequences.
0026 *
0027 * LKR, LF, RL, and RU are read events; LKR has Acquire ordering.
0028 * LKW and UL are write events; UL has Release ordering.
0029 * LKW, LF, RL, and RU have no ordering properties.
0030 *)
0031
0032 (* Backward compatibility *)
0033 let RL = try RL with emptyset
0034 let RU = try RU with emptyset
0035
0036 (* Treat RL as a kind of LF: a read with no ordering properties *)
0037 let LF = LF | RL
0038
0039 (* There should be no ordinary R or W accesses to spinlocks *)
0040 let ALL-LOCKS = LKR | LKW | UL | LF | RU
0041 flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
0042
0043 (* Link Lock-Reads to their RMW-partner Lock-Writes *)
0044 let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po)
0045 let rmw = rmw | lk-rmw
0046
0047 (* The litmus test is invalid if an LKR/LKW event is not part of an RMW pair *)
0048 flag ~empty LKW \ range(lk-rmw) as unpaired-LKW
0049 flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
0050
0051 (*
0052 * An LKR must always see an unlocked value; spin_lock() calls nested
0053 * inside a critical section (for the same lock) always deadlock.
0054 *)
0055 empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
0056
0057 (* The final value of a spinlock should not be tested *)
0058 flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
0059
0060 (*
0061 * Put lock operations in their appropriate classes, but leave UL out of W
0062 * until after the co relation has been generated.
0063 *)
0064 let R = R | LKR | LF | RU
0065 let W = W | LKW
0066
0067 let Release = Release | UL
0068 let Acquire = Acquire | LKR
0069
0070 (* Match LKW events to their corresponding UL events *)
0071 let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
0072
0073 flag ~empty UL \ range(critical) as unmatched-unlock
0074
0075 (* Allow up to one unmatched LKW per location; more must deadlock *)
0076 let UNMATCHED-LKW = LKW \ domain(critical)
0077 empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks
0078
0079 (* rfi for LF events: link each LKW to the LF events in its critical section *)
0080 let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
0081
0082 (* rfe for LF events *)
0083 let all-possible-rfe-lf =
0084 (*
0085 * Given an LF event r, compute the possible rfe edges for that event
0086 * (all those starting from LKW events in other threads),
0087 * and then convert that relation to a set of single-edge relations.
0088 *)
0089 let possible-rfe-lf r =
0090 let pair-to-relation p = p ++ 0
0091 in map pair-to-relation ((LKW * {r}) & loc & ext)
0092 (* Do this for each LF event r that isn't in rfi-lf *)
0093 in map possible-rfe-lf (LF \ range(rfi-lf))
0094
0095 (* Generate all rf relations for LF events *)
0096 with rfe-lf from cross(all-possible-rfe-lf)
0097 let rf-lf = rfe-lf | rfi-lf
0098
0099 (*
0100 * RU, i.e., spin_is_locked() returning False, is slightly different.
0101 * We rely on the memory model to rule out cases where spin_is_locked()
0102 * within one of the lock's critical sections returns False.
0103 *)
0104
0105 (* rfi for RU events: an RU may read from the last po-previous UL *)
0106 let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
0107
0108 (* rfe for RU events: an RU may read from an external UL or the initial write *)
0109 let all-possible-rfe-ru =
0110 let possible-rfe-ru r =
0111 let pair-to-relation p = p ++ 0
0112 in map pair-to-relation (((UL | IW) * {r}) & loc & ext)
0113 in map possible-rfe-ru RU
0114
0115 (* Generate all rf relations for RU events *)
0116 with rfe-ru from cross(all-possible-rfe-ru)
0117 let rf-ru = rfe-ru | rfi-ru
0118
0119 (* Final rf relation *)
0120 let rf = rf | rf-lf | rf-ru
0121
0122 (* Generate all co relations, including LKW events but not UL *)
0123 let co0 = co0 | ([IW] ; loc ; [LKW]) |
0124 (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW])
0125 include "cos-opt.cat"
0126 let W = W | UL
0127 let M = R | W
0128
0129 (* Merge UL events into co *)
0130 let co = (co | critical | (critical^-1 ; co))+
0131 let coe = co & ext
0132 let coi = co & int
0133
0134 (* Merge LKR events into rf *)
0135 let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)
0136 let rfe = rf & ext
0137 let rfi = rf & int
0138
0139 let fr = rf^-1 ; co
0140 let fre = fr & ext
0141 let fri = fr & int
0142
0143 show co,rf,fr
