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
  11 include "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 *)
  33 let RL = try RL with emptyset
  34 let RU = try RU with emptyset
  35
  36 (* Treat RL as a kind of LF: a read with no ordering properties *)
  37 let LF = LF | RL
  38
  39 (* There should be no ordinary R or W accesses to spinlocks *)
  40 let ALL-LOCKS = LKR | LKW | UL | LF | RU
  41 flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
  42
  43 (* Link Lock-Reads to their RMW-partner Lock-Writes *)
  44 let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po)
  45 let rmw = rmw | lk-rmw
  46
  47 (* The litmus test is invalid if an LKR/LKW event is not part of an RMW pair *)
  48 flag ~empty LKW \ range(lk-rmw) as unpaired-LKW
  49 flag ~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  *)
  55 empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
  56
  57 (* The final value of a spinlock should not be tested *)
  58 flag ~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  *)
  64 let R = R | LKR | LF | RU
  65 let W = W | LKW
  66
  67 let Release = Release | UL
  68 let Acquire = Acquire | LKR
  69
  70 (* Match LKW events to their corresponding UL events *)
  71 let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
  72
  73 flag ~empty UL \ range(critical) as unmatched-unlock
  74
  75 (* Allow up to one unmatched LKW per location; more must deadlock *)
  76 let UNMATCHED-LKW = LKW \ domain(critical)
  77 empty ([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 *)
  80 let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
  81
  82 (* rfe for LF events *)
  83 let 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 *)
  96 with rfe-lf from cross(all-possible-rfe-lf)
  97 let 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 *)
 106 let 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 *)
 109 let 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 *)
 116 with rfe-ru from cross(all-possible-rfe-ru)
 117 let rf-ru = rfe-ru | rfi-ru
 118
 119 (* Final rf relation *)
 120 let rf = rf | rf-lf | rf-ru
 121
 122 (* Generate all co relations, including LKW events but not UL *)
 123 let co0 = co0 | ([IW] ; loc ; [LKW]) |
 124         (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW])
 125 include "cos-opt.cat"
 126 let W = W | UL
 127 let M = R | W
 128
 129 (* Merge UL events into co *)
 130 let co = (co | critical | (critical^-1 ; co))+
 131 let coe = co & ext
 132 let coi = co & int
 133
 134 (* Merge LKR events into rf *)
 135 let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)
 136 let rfe = rf & ext
 137 let rfi = rf & int
 138
 139 let fr = rf^-1 ; co
 140 let fre = fr & ext
 141 let fri = fr & int
 142
 143 show co,rf,fr