| 1 | // SPDX-License-Identifier: GPL-2.0+ |
| 2 | (* |
| 3 | * Copyright (C) 2016 Luc Maranget <[email protected]> for Inria |
| 4 | * Copyright (C) 2017 Alan Stern <[email protected]> |
| 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 |