158 lines · plain
1// SPDX-License-Identifier: GPL-2.0+2(*3 * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria4 * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>5 *)6 7(*8 * Generate coherence orders and handle lock operations9 *)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 successful17 * spin_trylock() read-modify-write event pair18 * LKW Lock-Write: the write part of a spin_lock() or successful19 * spin_trylock() RMW event pair20 * UL Unlock: a spin_unlock() event21 * LF Lock-Fail: a failed spin_trylock() event22 * RL Read-Locked: a spin_is_locked() event which returns True23 * RU Read-Unlocked: a spin_is_locked() event which returns False24 *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 emptyset34let RU = try RU with emptyset35 36(* Treat RL as a kind of LF: a read with no ordering properties *)37let LF = LF | RL38 39(* There should be no ordinary R or W accesses to spinlocks or SRCU structs *)40let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Sync-srcu41flag ~empty [M \ IW \ ALL-LOCKS] ; loc ; [ALL-LOCKS] as mixed-lock-accesses42 43(* Link Lock-Reads to their RMW-partner Lock-Writes *)44let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po)45let rmw = rmw | lk-rmw46 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-LKW49flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR50 51(*52 * An LKR must always see an unlocked value; spin_lock() calls nested53 * inside a critical section (for the same lock) always deadlock.54 *)55empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest56 57(*58 * In the same way, spin_is_locked() inside a critical section must always59 * return True (no RU events can be in a critical section for the same lock).60 *)61empty ([LKW] ; po-loc ; [RU]) \ (po-loc ; [UL] ; po-loc) as nested-is-locked62 63(* The final value of a spinlock should not be tested *)64flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final65 66(*67 * Put lock operations in their appropriate classes, but leave UL out of W68 * until after the co relation has been generated.69 *)70let R = R | LKR | LF | RU71let W = W | LKW72 73let Release = Release | UL74let Acquire = Acquire | LKR75 76(* Match LKW events to their corresponding UL events *)77let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)78 79flag ~empty UL \ range(critical) as unmatched-unlock80 81(* Allow up to one unmatched LKW per location; more must deadlock *)82let UNMATCHED-LKW = LKW \ domain(critical)83empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks84 85(* rfi for LF events: link each LKW to the LF events in its critical section *)86let 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 *)89let pair-to-relation p = p ++ 090 91(*92 * If a given LF event e is outside a critical section, it cannot read93 * internally but it may read from an LKW event in another thread.94 * Compute the relation containing these possible edges.95 *)96let possible-rfe-noncrit-lf e = (LKW * {e}) & loc & ext97 98(* Compute set of sets of possible rfe edges for LF events *)99let all-possible-rfe-lf =100 (*101 * Convert the possible-rfe-noncrit-lf relation for e102 * to a set of single edges103 *)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 *)110with rfe-lf from cross(all-possible-rfe-lf)111let rf-lf = rfe-lf | rfi-lf112 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 *)118let 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 *)123let 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 RU129 130(* Generate all rf relations for RU events *)131with rf-ru from cross(all-possible-rf-ru)132 133(* Final rf relation *)134let rf = rf | rf-lf | rf-ru135 136(* Generate all co relations, including LKW events but not UL *)137let co0 = co0 | ([IW] ; loc ; [LKW]) |138 (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW])139include "cos-opt.cat"140let W = W | UL141let M = R | W142 143(* Merge UL events into co *)144let co = (co | critical | (critical^-1 ; co))+145let coe = co & ext146let coi = co & int147 148(* Merge LKR events into rf *)149let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)150let rfe = rf & ext151let rfi = rf & int152 153let fr = rf^-1 ; co154let fre = fr & ext155let fri = fr & int156 157show co,rf,fr158