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 (* Generate coherence orders and handle lock operations *)
   8 (*
   9  * Warning, crashes with herd7 versions strictly before 7.48.
  10  * spin_islocked is functional from version 7.49.
  11  *
  12  *)
  13 include "cross.cat"
  14
  15 (* From lock reads to their partner lock writes *)
  16 let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po)
  17 let rmw = rmw | lk-rmw
  18
  19 (*
  20  * A paired LKR must always see an unlocked value; spin_lock() calls nested
  21  * inside a critical section (for the same lock) always deadlock.
  22  *)
  23 empty ([LKW] ; po-loc ; [domain(lk-rmw)]) \ (po-loc ; [UL] ; po-loc)
  24         as lock-nest
  25
  26 (* The litmus test is invalid if an LKW event is not part of an RMW pair *)
  27 flag ~empty LKW \ range(lk-rmw) as unpaired-LKW
  28
  29 (* This will be allowed if we implement spin_is_locked() *)
  30 flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
  31
  32 (* There should be no R or W accesses to spinlocks *)
  33 let ALL-LOCKS = LKR | LKW | UL | LF
  34 flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
  35
  36 (* The final value of a spinlock should not be tested *)
  37 flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
  38
  39 (*
  40  * Backward compatibility
  41  *)
  42 let RL = try RL with emptyset (* defined herd7 >= 7.49 *)
  43 let RU = try RU with emptyset (* defined herd7 >= 7.49 *)
  44 (*
  45  * Put lock operations in their appropriate classes, but leave UL out of W
  46  * until after the co relation has been generated.
  47  *)
  48 let R = R | LKR | LF | RL | RU
  49 let W = W | LKW
  50
  51 let Release = Release | UL
  52 let Acquire = Acquire | LKR
  53
  54
  55 (* Match LKW events to their corresponding UL events *)
  56 let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
  57
  58 flag ~empty UL \ range(critical) as unmatched-unlock
  59
  60 (* Allow up to one unmatched LKW per location; more must deadlock *)
  61 let UNMATCHED-LKW = LKW \ domain(critical)
  62 empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks
  63
  64
  65 (* rfi for LF events: link each LKW to the LF events in its critical section *)
  66 let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
  67
  68 (* rfe for LF events *)
  69 let all-possible-rfe-lf =
  70   (*
  71    * Given an LF event r, compute the possible rfe edges for that event
  72    * (all those starting from LKW events in other threads),
  73    * and then convert that relation to a set of single-edge relations.
  74    *)
  75   let possible-rfe-lf r =
  76     let pair-to-relation p = p ++ 0
  77     in map pair-to-relation ((LKW * {r}) & loc & ext)
  78   (* Do this for each LF event r that isn't in rfi-lf *)
  79   in map possible-rfe-lf (LF \ range(rfi-lf))
  80
  81 (* Generate all rf relations for LF events *)
  82 with rfe-lf from cross(all-possible-rfe-lf)
  83
  84 let rf-lf = rfe-lf | rfi-lf
  85
  86 (* rf for RL events, ie islocked returning true, similar to LF above *)
  87
  88 (* islocked returning true inside a critical section
  89  * must read from the opening lock
  90  *)
  91 let rfi-rl = ([LKW] ; po-loc ; [RL]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
  92
  93 (* islocked returning true outside critical sections can match any
  94  * external lock.
  95  *)
  96 let all-possible-rfe-rl =
  97   let possible-rfe-lf r =
  98     let pair-to-relation p = p ++ 0
  99     in map pair-to-relation ((LKW * {r}) & loc & ext)
 100   in map possible-rfe-lf (RL \ range(rfi-rl))
 101
 102 with rfe-rl from cross(all-possible-rfe-rl)
 103 let rf-rl = rfe-rl | rfi-rl
 104
 105 (* Read from unlock, ie islocked returning false, slightly different *)
 106
 107 (* islocked returning false can read from the last po-previous unlock *)
 108 let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
 109
 110 (* any islocked returning false can read from any external unlock *)
 111 let all-possible-rfe-ru =
 112    let possible-rfe-ru r =
 113      let pair-to-relation p = p ++ 0
 114      in map pair-to-relation (((UL|IW) * {r}) & loc & ext)
 115   in map possible-rfe-ru RU
 116
 117 with rfe-ru from cross(all-possible-rfe-ru)
 118 let rf-ru = rfe-ru | rfi-ru
 119
 120 (* Final rf relation *)
 121 let rf = rf | rf-lf | rf-rl | rf-ru
 122
 123 (* Generate all co relations, including LKW events but not UL *)
 124 let co0 = co0 | ([IW] ; loc ; [LKW]) |
 125         (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW])
 126 include "cos-opt.cat"
 127 let W = W | UL
 128 let M = R | W
 129
 130 (* Merge UL events into co *)
 131 let co = (co | critical | (critical^-1 ; co))+
 132 let coe = co & ext
 133 let coi = co & int
 134
 135 (* Merge LKR events into rf *)
 136 let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)
 137 let rfe = rf & ext
 138 let rfi = rf & int
 139
 140 let fr = rf^-1 ; co
 141 let fre = fr & ext
 142 let fri = fr & int
 143
 144 show co,rf,fr