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 include "cross.cat"
  10
  11 (* From lock reads to their partner lock writes *)
  12 let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po)
  13 let rmw = rmw | lk-rmw
  14
  15 (*
  16  * A paired LKR must always see an unlocked value; spin_lock() calls nested
  17  * inside a critical section (for the same lock) always deadlock.
  18  *)
  19 empty ([LKW] ; po-loc ; [domain(lk-rmw)]) \ (po-loc ; [UL] ; po-loc)
  20         as lock-nest
  21
  22 (* The litmus test is invalid if an LKW event is not part of an RMW pair *)
  23 flag ~empty LKW \ range(lk-rmw) as unpaired-LKW
  24
  25 (* This will be allowed if we implement spin_is_locked() *)
  26 flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
  27
  28 (* There should be no R or W accesses to spinlocks *)
  29 let ALL-LOCKS = LKR | LKW | UL | LF
  30 flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
  31
  32 (* The final value of a spinlock should not be tested *)
  33 flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
  34
  35
  36 (*
  37  * Put lock operations in their appropriate classes, but leave UL out of W
  38  * until after the co relation has been generated.
  39  *)
  40 let R = R | LKR | LF
  41 let W = W | LKW
  42
  43 let Release = Release | UL
  44 let Acquire = Acquire | LKR
  45
  46
  47 (* Match LKW events to their corresponding UL events *)
  48 let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
  49
  50 flag ~empty UL \ range(critical) as unmatched-unlock
  51
  52 (* Allow up to one unmatched LKW per location; more must deadlock *)
  53 let UNMATCHED-LKW = LKW \ domain(critical)
  54 empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks
  55
  56
  57 (* rfi for LF events: link each LKW to the LF events in its critical section *)
  58 let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
  59
  60 (* rfe for LF events *)
  61 let all-possible-rfe-lf =
  62   (*
  63    * Given an LF event r, compute the possible rfe edges for that event
  64    * (all those starting from LKW events in other threads),
  65    * and then convert that relation to a set of single-edge relations.
  66    *)
  67   let possible-rfe-lf r =
  68     let pair-to-relation p = p ++ 0
  69     in map pair-to-relation ((LKW * {r}) & loc & ext)
  70   (* Do this for each LF event r that isn't in rfi-lf *)
  71   in map possible-rfe-lf (LF \ range(rfi-lf))
  72
  73 (* Generate all rf relations for LF events *)
  74 with rfe-lf from cross(all-possible-rfe-lf)
  75 let rf = rf | rfi-lf | rfe-lf
  76
  77
  78 (* Generate all co relations, including LKW events but not UL *)
  79 let co0 = co0 | ([IW] ; loc ; [LKW]) |
  80         (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW])
  81 include "cos-opt.cat"
  82 let W = W | UL
  83 let M = R | W
  84
  85 (* Merge UL events into co *)
  86 let co = (co | critical | (critical^-1 ; co))+
  87 let coe = co & ext
  88 let coi = co & int
  89
  90 (* Merge LKR events into rf *)
  91 let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)
  92 let rfe = rf & ext
  93 let rfi = rf & int
  94
  95 let fr = rf^-1 ; co
  96 let fre = fr & ext
  97 let fri = fr & int
  98
  99 show co,rf,fr