diff options
| author | Steven Rostedt <rostedt@goodmis.org> | 2026-09-02 09:55:01 -0400 |
|---|---|---|
| committer | Steven Rostedt <rostedt@goodmis.org> | 2026-09-02 11:08:21 -0400 |
| commit | 4617721c502b2ddaa4e324e86da4997edf738fa5 (patch) | |
| tree | 350aa83b47da0b574a814795392b20b0bed83cbc /tools/memory-model/lock.cat | |
| download | linux-stable-4617721c502b2ddaa4e324e86da4997edf738fa5.tar.gz linux-stable-4617721c502b2ddaa4e324e86da4997edf738fa5.zip | |
ftrace: Synchronize the initialization of ftrace_opsgrafted
There's some internal state that ftrace_ops needs to have set, but since
it can be declared outside of the ftrace.c code, it calls
ftrace_ops_init() on the ops in every global function. The issue is that
if two tasks call it on the same ops at the same time it is possible to
have the initialization of one corrupt the initialization of the other
call.
Create a ops_mutex to use to synchronize every initialization of the
ftrace_ops. The mutex is taken within checking the ftrace_ops flag that
states it was initializied but the flag is checked again after the mutex
has been taken. Checking first outside the mutex allows it to shortcut
having to take the mutex. But then the check needs to be done again after
the mute is taken in case of races.
Cc: stable@vger.kernel.org
Link: https://patch.msgid.link/20260902095501.6b59af20@gandalf.local.home
Fixes: f04f24fb7e48d ("ftrace, kprobes: Fix a deadlock on ftrace_regex_lock")
Reported-by: sashiko-bot@kernel.org
Close: https://lore.kernel.org/all/20260829025528.49A831F000E9@smtp.kernel.org/
Signed-off-by: Steven Rostedt <rostedt@goodmis.org>
Diffstat (limited to 'tools/memory-model/lock.cat')
| -rw-r--r-- | tools/memory-model/lock.cat | 157 |
1 files changed, 157 insertions, 0 deletions
diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat new file mode 100644 index 000000000..03c12efed --- /dev/null +++ b/tools/memory-model/lock.cat @@ -0,0 +1,157 @@ +// SPDX-License-Identifier: GPL-2.0+ +(* + * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria + * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu> + *) + +(* + * Generate coherence orders and handle lock operations + *) + +include "cross.cat" + +(* + * The lock-related events generated by herd7 are as follows: + * + * LKR Lock-Read: the read part of a spin_lock() or successful + * spin_trylock() read-modify-write event pair + * LKW Lock-Write: the write part of a spin_lock() or successful + * spin_trylock() RMW event pair + * UL Unlock: a spin_unlock() event + * LF Lock-Fail: a failed spin_trylock() event + * RL Read-Locked: a spin_is_locked() event which returns True + * RU Read-Unlocked: a spin_is_locked() event which returns False + * + * LKR and LKW events always come paired, like all RMW event sequences. + * + * LKR, LF, RL, and RU are read events; LKR has Acquire ordering. + * LKW and UL are write events; UL has Release ordering. + * LKW, LF, RL, and RU have no ordering properties. + *) + +(* Backward compatibility *) +let RL = try RL with emptyset +let RU = try RU with emptyset + +(* Treat RL as a kind of LF: a read with no ordering properties *) +let LF = LF | RL + +(* There should be no ordinary R or W accesses to spinlocks or SRCU structs *) +let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Sync-srcu +flag ~empty [M \ IW \ ALL-LOCKS] ; loc ; [ALL-LOCKS] as mixed-lock-accesses + +(* Link Lock-Reads to their RMW-partner Lock-Writes *) +let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po) +let rmw = rmw | lk-rmw + +(* The litmus test is invalid if an LKR/LKW event is not part of an RMW pair *) +flag ~empty LKW \ range(lk-rmw) as unpaired-LKW +flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR + +(* + * An LKR must always see an unlocked value; spin_lock() calls nested + * inside a critical section (for the same lock) always deadlock. + *) +empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest + +(* + * In the same way, spin_is_locked() inside a critical section must always + * return True (no RU events can be in a critical section for the same lock). + *) +empty ([LKW] ; po-loc ; [RU]) \ (po-loc ; [UL] ; po-loc) as nested-is-locked + +(* The final value of a spinlock should not be tested *) +flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final + +(* + * Put lock operations in their appropriate classes, but leave UL out of W + * until after the co relation has been generated. + *) +let R = R | LKR | LF | RU +let W = W | LKW + +let Release = Release | UL +let Acquire = Acquire | LKR + +(* Match LKW events to their corresponding UL events *) +let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc) + +flag ~empty UL \ range(critical) as unmatched-unlock + +(* Allow up to one unmatched LKW per location; more must deadlock *) +let UNMATCHED-LKW = LKW \ domain(critical) +empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks + +(* rfi for LF events: link each LKW to the LF events in its critical section *) +let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc) + +(* Utility macro to convert a single pair to a single-edge relation *) +let pair-to-relation p = p ++ 0 + +(* + * If a given LF event e is outside a critical section, it cannot read + * internally but it may read from an LKW event in another thread. + * Compute the relation containing these possible edges. + *) +let possible-rfe-noncrit-lf e = (LKW * {e}) & loc & ext + +(* Compute set of sets of possible rfe edges for LF events *) +let all-possible-rfe-lf = + (* + * Convert the possible-rfe-noncrit-lf relation for e + * to a set of single edges + *) + let set-of-singleton-rfe-lf e = + map pair-to-relation (possible-rfe-noncrit-lf e) + (* Do this for each LF event e that isn't in rfi-lf *) + in map set-of-singleton-rfe-lf (LF \ range(rfi-lf)) + +(* Generate all rf relations for LF events *) +with rfe-lf from cross(all-possible-rfe-lf) +let rf-lf = rfe-lf | rfi-lf + +(* + * A given RU event e may read internally from the last po-previous UL, + * or it may read from a UL event in another thread or the initial write. + * Compute the relation containing these possible edges. + *) +let possible-rf-ru e = (((UL * {e}) & po-loc) \ + ([UL] ; po-loc ; [UL] ; po-loc)) | + (((UL | IW) * {e}) & loc & ext) + +(* Compute set of sets of possible rf edges for RU events *) +let all-possible-rf-ru = + (* Convert the possible-rf-ru relation for e to a set of single edges *) + let set-of-singleton-rf-ru e = + map pair-to-relation (possible-rf-ru e) + (* Do this for each RU event e *) + in map set-of-singleton-rf-ru RU + +(* Generate all rf relations for RU events *) +with rf-ru from cross(all-possible-rf-ru) + +(* Final rf relation *) +let rf = rf | rf-lf | rf-ru + +(* Generate all co relations, including LKW events but not UL *) +let co0 = co0 | ([IW] ; loc ; [LKW]) | + (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW]) +include "cos-opt.cat" +let W = W | UL +let M = R | W + +(* Merge UL events into co *) +let co = (co | critical | (critical^-1 ; co))+ +let coe = co & ext +let coi = co & int + +(* Merge LKR events into rf *) +let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1) +let rfe = rf & ext +let rfi = rf & int + +let fr = rf^-1 ; co +let fre = fr & ext +let fri = fr & int + +show co,rf,fr |
