From 34ff636f322c6d5e4f0a52338fa63a7dff09a495 Mon Sep 17 00:00:00 2001 From: Joel Fernandes Date: Sat, 18 Jul 2026 13:15:36 -0400 Subject: scftorture: Count single_rpc offline failures in statistics output scf_torture_stats_print() aggregates each invoker thread's counters into a local scf_statistics structure before printing, but the n_single_rpc_ofl field is missing from the aggregation loop. As a result, the "single_rpc_ofl" value printed in the statistics line is always zero, even when smp_call_function_single() invocations for the RPC test have failed due to offline CPUs and been counted by the invoker threads. Add the missing accumulation so that the printed value reflects the actual counts. Signed-off-by: Joel Fernandes Signed-off-by: Paul E. McKenney --- tools/memory-model/lock.cat | 157 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 157 insertions(+) create mode 100644 tools/memory-model/lock.cat (limited to 'tools/memory-model/lock.cat') 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 for Inria + * Copyright (C) 2017 Alan Stern + *) + +(* + * 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 -- cgit v1.3.1