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 or SRCU structs *)
  40 let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Sync-srcu
  41 flag ~empty [M \ IW \ ALL-LOCKS] ; 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 (*
  58  * In the same way, spin_is_locked() inside a critical section must always
  59  * return True (no RU events can be in a critical section for the same lock).
  60  *)
  61 empty ([LKW] ; po-loc ; [RU]) \ (po-loc ; [UL] ; po-loc) as nested-is-locked
  62
  63 (* The final value of a spinlock should not be tested *)
  64 flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
  65
  66 (*
  67  * Put lock operations in their appropriate classes, but leave UL out of W
  68  * until after the co relation has been generated.
  69  *)
  70 let R = R | LKR | LF | RU
  71 let W = W | LKW
  72
  73 let Release = Release | UL
  74 let Acquire = Acquire | LKR
  75
  76 (* Match LKW events to their corresponding UL events *)
  77 let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
  78
  79 flag ~empty UL \ range(critical) as unmatched-unlock
  80
  81 (* Allow up to one unmatched LKW per location; more must deadlock *)
  82 let UNMATCHED-LKW = LKW \ domain(critical)
  83 empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks
  84
  85 (* rfi for LF events: link each LKW to the LF events in its critical section *)
  86 let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
  87
  88 (* Utility macro to convert a single pair to a single-edge relation *)
  89 let pair-to-relation p = p ++ 0
  90
  91 (*
  92  * If a given LF event e is outside a critical section, it cannot read
  93  * internally but it may read from an LKW event in another thread.
  94  * Compute the relation containing these possible edges.
  95  *)
  96 let possible-rfe-noncrit-lf e = (LKW * {e}) & loc & ext
  97
  98 (* Compute set of sets of possible rfe edges for LF events *)
  99 let all-possible-rfe-lf =
 100         (*
 101          * Convert the possible-rfe-noncrit-lf relation for e
 102          * to a set of single edges
 103          *)
 104         let set-of-singleton-rfe-lf e =
 105                         map pair-to-relation (possible-rfe-noncrit-lf e)
 106         (* Do this for each LF event e that isn't in rfi-lf *)
 107         in map set-of-singleton-rfe-lf (LF \ range(rfi-lf))
 108
 109 (* Generate all rf relations for LF events *)
 110 with rfe-lf from cross(all-possible-rfe-lf)
 111 let rf-lf = rfe-lf | rfi-lf
 112
 113 (*
 114  * A given RU event e may read internally from the last po-previous UL,
 115  * or it may read from a UL event in another thread or the initial write.
 116  * Compute the relation containing these possible edges.
 117  *)
 118 let possible-rf-ru e = (((UL * {e}) & po-loc) \
 119                         ([UL] ; po-loc ; [UL] ; po-loc)) |
 120                 (((UL | IW) * {e}) & loc & ext)
 121
 122 (* Compute set of sets of possible rf edges for RU events *)
 123 let all-possible-rf-ru =
 124         (* Convert the possible-rf-ru relation for e to a set of single edges *)
 125         let set-of-singleton-rf-ru e =
 126                 map pair-to-relation (possible-rf-ru e)
 127         (* Do this for each RU event e *)
 128         in map set-of-singleton-rf-ru RU
 129
 130 (* Generate all rf relations for RU events *)
 131 with rf-ru from cross(all-possible-rf-ru)
 132
 133 (* Final rf relation *)
 134 let rf = rf | rf-lf | rf-ru
 135
 136 (* Generate all co relations, including LKW events but not UL *)
 137 let co0 = co0 | ([IW] ; loc ; [LKW]) |
 138         (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW])
 139 include "cos-opt.cat"
 140 let W = W | UL
 141 let M = R | W
 142
 143 (* Merge UL events into co *)
 144 let co = (co | critical | (critical^-1 ; co))+
 145 let coe = co & ext
 146 let coi = co & int
 147
 148 (* Merge LKR events into rf *)
 149 let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)
 150 let rfe = rf & ext
 151 let rfi = rf & int
 152
 153 let fr = rf^-1 ; co
 154 let fre = fr & ext
 155 let fri = fr & int
 156
 157 show co,rf,fr