LXR linux/tools/memory-model/lock.cat

   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 *)
  40let ALL-LOCKS = LKR | LKW | UL | LF | RU
  41flag ~empty [M \ IW] ; 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(* The final value of a spinlock should not be tested *)
  58flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
  59
  60(*
  61 * Put lock operations in their appropriate classes, but leave UL out of W
  62 * until after the co relation has been generated.
  63 *)
  64let R = R | LKR | LF | RU
  65let W = W | LKW
  66
  67let Release = Release | UL
  68let Acquire = Acquire | LKR
  69
  70(* Match LKW events to their corresponding UL events *)
  71let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
  72
  73flag ~empty UL \ range(critical) as unmatched-unlock
  74
  75(* Allow up to one unmatched LKW per location; more must deadlock *)
  76let UNMATCHED-LKW = LKW \ domain(critical)
  77empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks
  78
  79(* rfi for LF events: link each LKW to the LF events in its critical section *)
  80let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
  81
  82(* rfe for LF events *)
  83let all-possible-rfe-lf =
  84        (*
  85         * Given an LF event r, compute the possible rfe edges for that event
  86         * (all those starting from LKW events in other threads),
  87         * and then convert that relation to a set of single-edge relations.
  88         *)
  89        let possible-rfe-lf r =
  90                let pair-to-relation p = p ++ 0
  91                in map pair-to-relation ((LKW * {r}) & loc & ext)
  92        (* Do this for each LF event r that isn't in rfi-lf *)
  93        in map possible-rfe-lf (LF \ range(rfi-lf))
  94
  95(* Generate all rf relations for LF events *)
  96with rfe-lf from cross(all-possible-rfe-lf)
  97let rf-lf = rfe-lf | rfi-lf
  98
  99(*
 100 * RU, i.e., spin_is_locked() returning False, is slightly different.
 101 * We rely on the memory model to rule out cases where spin_is_locked()
 102 * within one of the lock's critical sections returns False.
 103 *)
 104
 105(* rfi for RU events: an RU may read from the last po-previous UL *)
 106let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
 107
 108(* rfe for RU events: an RU may read from an external UL or the initial write *)
 109let all-possible-rfe-ru =
 110        let possible-rfe-ru r =
 111                let pair-to-relation p = p ++ 0
 112                in map pair-to-relation (((UL | IW) * {r}) & loc & ext)
 113        in map possible-rfe-ru RU
 114
 115(* Generate all rf relations for RU events *)
 116with rfe-ru from cross(all-possible-rfe-ru)
 117let rf-ru = rfe-ru | rfi-ru
 118
 119(* Final rf relation *)
 120let rf = rf | rf-lf | rf-ru
 121
 122(* Generate all co relations, including LKW events but not UL *)
 123let co0 = co0 | ([IW] ; loc ; [LKW]) |
 124        (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW])
 125include "cos-opt.cat"
 126let W = W | UL
 127let M = R | W
 128
 129(* Merge UL events into co *)
 130let co = (co | critical | (critical^-1 ; co))+
 131let coe = co & ext
 132let coi = co & int
 133
 134(* Merge LKR events into rf *)
 135let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)
 136let rfe = rf & ext
 137let rfi = rf & int
 138
 139let fr = rf^-1 ; co
 140let fre = fr & ext
 141let fri = fr & int
 142
 143show co,rf,fr
 144