mirror of https://lore.kernel.org/lkml/
 help / color / mirror / Atom feed
* [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors
@ 2026-09-11 12:34 Tobias Schaffner
  2026-09-11 12:34 ` [PATCH v2 1/3] rv: add per-edge dwell-time statistics primitive Tobias Schaffner
                   ` (3 more replies)
  0 siblings, 4 replies; 13+ messages in thread
From: Tobias Schaffner @ 2026-09-11 12:34 UTC (permalink / raw)
  To: Steven Rostedt, Gabriele Monaco
  Cc: Jonathan Corbet, Shuah Khan, Masami Hiramatsu, Mathieu Desnoyers,
	linux-trace-kernel, linux-doc, linux-kselftest, linux-kernel,
	rpm, jan.kiszka, Tobias Schaffner

Hi Steven, Gabriele,

I am using the RV system for a downstream project called EVL (aka Xenomai4).
It is a small co-kernel system, small enough that I can model the whole
co-kernel with RV instead of just a fragment of it.

The patches in this series add a per-monitor "stats" file that exposes how
often an edge has been visited and the dwell time in the prior state for
per-cpu monitors.

This allows me to not only check if the model is correct but also to see if
all paths are exercised by my stress tooling and to decompose the latency of
the co-kernel's wakeup path.

I think that some of the upstream monitors like e.g. the sts monitor could also
profit from this.

As an example, here is the sts monitor on a StarFive VisionFive2 running an rt
kernel (isolcpus=2-3), after enabling it and generating some scheduler load.
Only the edges the automaton actually takes are non-zero:

  # cat monitors/sched/sts/stats
  # cpu edge label count max_ns sum_ns
  0 0 can_sched:irq_disable 367732 3998500 14773091250
  0 4 can_sched:schedule_entry 40282 398750 45510750
  0 7 cant_sched:irq_enable 367732 32500 532791750
  0 8 cant_sched:irq_entry 26188 6250 38357250
  0 13 disable_to_switch:irq_enable 4933 12500 12275000
  0 14 disable_to_switch:irq_entry 31 2250 35250
  0 15 disable_to_switch:sched_switch 35373 26750 111615750
  0 18 enable_to_exit:irq_disable 373 3250 649750
  0 19 enable_to_exit:irq_enable 373 20000 1676250
  0 20 enable_to_exit:irq_entry 309 4750 420000
  0 23 enable_to_exit:schedule_exit 40298 3000 37335000
  0 25 in_irq:irq_enable 31 12250 140750
  0 30 scheduling:irq_disable 40337 18000 45449500
  0 37 switching:irq_enable 35373 9250 72471000
  [ cpus 1-2 omitted ]
  3 0 can_sched:irq_disable 567 3983750 300860250
  3 4 can_sched:schedule_entry 150 1500 171000
  3 7 cant_sched:irq_enable 567 21500 1777500
  3 8 cant_sched:irq_entry 76 6500 164750
  3 15 disable_to_switch:sched_switch 150 4250 413750
  3 23 enable_to_exit:schedule_exit 150 1500 147750
  3 30 scheduling:irq_disable 150 1500 166000
  3 37 switching:irq_enable 150 3750 277000

The sts model splits the schedule->switch path into separate states, so the
per-edge dwell decomposes the scheduler's interrupts-off window: on cpu0 the
prep phase (disable_to_switch, irqs off until the switch) tops out at 26.8us
and the switch itself (switching:irq_enable) at 9.3us, over 35k switches. The
counts also line up with the model, e.g. every irq_disable in can_sched has a
matching irq_enable in cant_sched (367732 == 367732). The isolated cpus 2-3
take almost no switches (150 on cpu3, versus 35k on cpu0) and their worst case
is tighter still (~4us), so the same file also makes the effect of cpu
isolation visible per cpu.

The changes are gated by CONFIG_RV_EDGE_STAT and dormant until a monitor is
enabled, so existing setups are unaffected. When enabled, each accepted
transition adds one local_clock() and a few lock-free local64_t updates. With
the config off there is no code on the hot path at all.

I focused on per-cpu monitors as a first step. Per-task and per-object
monitors would have to aggregate entities that share a cpu, which is harder
to get right, so I left them out for now.

What is your opinion on this? Do you think this is worth getting upstreamed?

Thanks for taking a look,
Tobias

---

Changes since v1:
 - Packed the state and its entry timestamp into one word, so one cmpxchg
   commits both and a nested IRQ can no longer charge a dwell to the
   wrong edge. Hope this approach is fine.
 - Moved the header to include/rv/edge_stat.h (Gabriele).
 - Implemented it all in the da_monitor layer so that rv.c is untouched
   and the file is created from da_monitor_init() (Gabriele). I did not
   create a matrix living in struct da_monitor though. I think that this
   would need a fixed upper bound as rv.h does not know how many states
   and events the monitor will have. But this would lead to a large array
   in any monitor including per-task monitors.
 - Used local64_try_cmpxchg(), bound the loop at
   MAX_DA_RETRY_RACING_EVENTS and warn now if it is hit (Gabriele).
 - Static per-cpu matrix instead of alloc_percpu() (sashiko).
 - depend on 64BIT, so GENERIC_ATOMIC64 is unreachable and the 32-bit
   NMI deadlock cannot happen at all (sashiko).
 - Reset and report for_each_possible_cpu(), and reset before the
   tracepoints are registered (sashiko).
 - stats file is 0440 now, and a failed create is propagated.
 - Columns are now count sum_ns max_ns.

Tobias Schaffner (3):
  rv: add per-edge dwell-time statistics primitive
  rv: add per-monitor edge-stat facility and stats file
  rv: collect per-edge dwell time for per-cpu DA/HA monitors

 .../trace/rv/runtime-verification.rst         |  26 +++
 include/linux/rv.h                            |   9 +-
 include/rv/da_monitor.h                       |  16 +-
 include/rv/edge_stat.h                        | 204 ++++++++++++++++++
 include/rv/ha_monitor.h                       |   2 +-
 kernel/trace/rv/Kconfig                       |  12 ++
 tools/testing/selftests/verification/config   |   3 +
 .../verification/test.d/rv_edge_stats.tc      |  33 +++
 8 files changed, 300 insertions(+), 5 deletions(-)
 create mode 100644 include/rv/edge_stat.h
 create mode 100644 tools/testing/selftests/verification/test.d/rv_edge_stats.tc

-- 
2.43.0


^ permalink raw reply	[flat|nested] 13+ messages in thread

* [PATCH v2 1/3] rv: add per-edge dwell-time statistics primitive
  2026-09-11 12:34 [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors Tobias Schaffner
@ 2026-09-11 12:34 ` Tobias Schaffner
  2026-09-24  7:21   ` Gabriele Monaco
  2026-09-11 12:34 ` [PATCH v2 2/3] rv: add per-monitor edge-stat facility and stats file Tobias Schaffner
                   ` (2 subsequent siblings)
  3 siblings, 1 reply; 13+ messages in thread
From: Tobias Schaffner @ 2026-09-11 12:34 UTC (permalink / raw)
  To: Steven Rostedt, Gabriele Monaco
  Cc: Jonathan Corbet, Shuah Khan, Masami Hiramatsu, Mathieu Desnoyers,
	linux-trace-kernel, linux-doc, linux-kselftest, linux-kernel,
	rpm, jan.kiszka, Tobias Schaffner

Add a small primitive that records, per automaton edge, how long the
monitor dwelled before taking it with a count, a sum and a maximum.

The counters are per-CPU and lock-free, so a monitor's hot path can
update them without disabling interrupts and without perturbing the latency
being measured. Keep the state and its entry timestamp in one word so
nested transitions cannot charge a dwell to the wrong edge.

Signed-off-by: Tobias Schaffner <tobias.schaffner@siemens.com>
---
 include/rv/edge_stat.h | 69 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)
 create mode 100644 include/rv/edge_stat.h

diff --git a/include/rv/edge_stat.h b/include/rv/edge_stat.h
new file mode 100644
index 000000000000..c5f04fd34aee
--- /dev/null
+++ b/include/rv/edge_stat.h
@@ -0,0 +1,69 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Per-edge dwell-time statistics for RV monitors.
+ *
+ * Copyright (C) 2026 Siemens AG
+ * Author: Tobias Schaffner <tobias.schaffner@siemens.com>
+ */
+#ifndef _RV_EDGE_STAT_H
+#define _RV_EDGE_STAT_H
+
+#include <linux/atomic.h>
+#include <linux/bug.h>
+#include <linux/compiler.h>
+#include <linux/rv.h>
+#include <linux/types.h>
+#include <asm/local64.h>
+
+#ifdef CONFIG_RV_EDGE_STAT
+
+/*
+ * Per-CPU counters kept in local64_t so accounting is safe against interrupt
+ * and NMI nesting on the owning CPU without disabling interrupts. Only the
+ * owning CPU writes.
+ */
+struct rv_edge_stat {
+	local64_t	count;
+	local64_t	sum_ns;
+	local64_t	max_ns;
+};
+
+/*
+ * State and entry timestamp share one word so a transition commits both with
+ * one cmpxchg. Comparing the timestamp also detects nested transitions that
+ * return to the same state.
+ */
+#define RV_STATE_BITS		8
+#define RV_STATE_MASK		GENMASK(RV_STATE_BITS - 1, 0)
+#define RV_TS_MASK		GENMASK(BITS_PER_LONG - RV_STATE_BITS - 1, 0)
+
+#define da_state_of(w)		((unsigned int)((w) & RV_STATE_MASK))
+#define da_ts_of(w)		((u64)(w) >> RV_STATE_BITS)
+#define da_state_pack(s, ts)	(((((da_state_t)(ts)) & RV_TS_MASK) << RV_STATE_BITS) | \
+				 ((da_state_t)(s) & RV_STATE_MASK))
+
+static __always_inline
+void rv_edge_stat_account(struct rv_edge_stat *s, u64 dwell_ns)
+{
+	s64 max;
+	int i;
+
+	local64_inc(&s->count);
+	local64_add(dwell_ns, &s->sum_ns);
+
+	/* Keep the largest dwell; bound retries if a nested update races us. */
+	max = local64_read(&s->max_ns);
+	for (i = 0; dwell_ns > (u64)max; i++) {
+		if (i == MAX_DA_RETRY_RACING_EVENTS) {
+			WARN_ONCE(1, "rv: edge-stat max update exceeded %d retries\n",
+				  MAX_DA_RETRY_RACING_EVENTS);
+			break;
+		}
+		if (local64_try_cmpxchg(&s->max_ns, &max, dwell_ns))
+			break;
+	}
+}
+
+#endif /* CONFIG_RV_EDGE_STAT */
+
+#endif /* _RV_EDGE_STAT_H */
-- 
2.43.0


^ permalink raw reply	[flat|nested] 13+ messages in thread

* [PATCH v2 2/3] rv: add per-monitor edge-stat facility and stats file
  2026-09-11 12:34 [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors Tobias Schaffner
  2026-09-11 12:34 ` [PATCH v2 1/3] rv: add per-edge dwell-time statistics primitive Tobias Schaffner
@ 2026-09-11 12:34 ` Tobias Schaffner
  2026-09-24  7:47   ` Gabriele Monaco
  2026-10-13 11:43   ` Gabriele Monaco
  2026-09-11 12:34 ` [PATCH v2 3/3] rv: collect per-edge dwell time for per-cpu DA/HA monitors Tobias Schaffner
  2026-10-12 11:47 ` [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors Gabriele Monaco
  3 siblings, 2 replies; 13+ messages in thread
From: Tobias Schaffner @ 2026-09-11 12:34 UTC (permalink / raw)
  To: Steven Rostedt, Gabriele Monaco
  Cc: Jonathan Corbet, Shuah Khan, Masami Hiramatsu, Mathieu Desnoyers,
	linux-trace-kernel, linux-doc, linux-kselftest, linux-kernel,
	rpm, jan.kiszka, Tobias Schaffner

Add CONFIG_RV_EDGE_STAT, an optional feature that records how long a
monitor's automaton dwells in a state and exposes it per edge through a
per-monitor "stats" tracefs file.

The facility uses a static per-CPU matrix and reports, per edge and per
CPU, the count, summed dwell time and maximum dwell time. Only the owning
CPU writes the counters, so a reader snapshots them with local64_read()
with no IPI and no locking on the accounting path.

Signed-off-by: Tobias Schaffner <tobias.schaffner@siemens.com>
---
 .../trace/rv/runtime-verification.rst         |  26 ++++
 include/rv/edge_stat.h                        | 135 ++++++++++++++++++
 kernel/trace/rv/Kconfig                       |  12 ++
 3 files changed, 173 insertions(+)

diff --git a/Documentation/trace/rv/runtime-verification.rst b/Documentation/trace/rv/runtime-verification.rst
index c700dde9259c..88ea04ff64be 100644
--- a/Documentation/trace/rv/runtime-verification.rst
+++ b/Documentation/trace/rv/runtime-verification.rst
@@ -229,3 +229,29 @@ For example::
    nop
    [panic]
    printk
+
+**monitors/MONITOR/stats**
+
+Present only when the kernel is built with CONFIG_RV_EDGE_STAT=y and *MONITOR*
+is a per-cpu deterministic or hybrid automaton monitor. The file exists while
+the monitor is enabled and reports how long the automaton dwells in each state
+before leaving it, timed with local_clock() and accounted per outgoing edge and
+per CPU.
+
+- The first line is a header naming the columns.
+- Each following line describes one edge on on one CPU::
+
+   cpu edge label count sum_ns max_ns
+
+   *count* is the number of times the transition was committed, *sum_ns* and
+   *max_ns* are the total and worst dwell in nanoseconds, and *label* is
+   "state:event".
+
+The counters are reset each time the monitor is enabled.
+
+For example::
+
+   # cat monitors/wip/stats
+   # cpu edge label count sum_ns max_ns
+   0 0 preemptive:preempt_disable 4210 95501200 183200
+   0 4 non_preemptive:preempt_enable 4208 3812900 42600
diff --git a/include/rv/edge_stat.h b/include/rv/edge_stat.h
index c5f04fd34aee..aff00c6fbb39 100644
--- a/include/rv/edge_stat.h
+++ b/include/rv/edge_stat.h
@@ -8,12 +8,18 @@
 #ifndef _RV_EDGE_STAT_H
 #define _RV_EDGE_STAT_H
 
+#include <linux/args.h>
 #include <linux/atomic.h>
 #include <linux/bug.h>
 #include <linux/compiler.h>
+#include <linux/percpu.h>
 #include <linux/rv.h>
+#include <linux/sched/clock.h>
+#include <linux/seq_file.h>
+#include <linux/tracefs.h>
 #include <linux/types.h>
 #include <asm/local64.h>
+#include <rv/automata.h>
 
 #ifdef CONFIG_RV_EDGE_STAT
 
@@ -64,6 +70,135 @@ void rv_edge_stat_account(struct rv_edge_stat *s, u64 dwell_ns)
 	}
 }
 
+#define DA_MON_EDGES CONCATENATE(da_mon_edges_, MONITOR_NAME)
+
+static_assert(STATE_MAX <= (1U << RV_STATE_BITS),
+	      "automaton has more states than the packed state word can hold");
+
+#if RV_MON_TYPE == RV_MON_PER_CPU
+
+/*
+ * Static storage avoids allocation lifetime races. Only the owning CPU writes,
+ * so readers can snapshot counters with local64_read().
+ */
+#define RV_THIS_NR_EDGES	(STATE_MAX * EVENT_MAX)
+
+struct rv_this_edges {
+	struct rv_edge_stat	edge[RV_THIS_NR_EDGES];
+};
+
+static DEFINE_PER_CPU(struct rv_this_edges, DA_MON_EDGES);
+static struct dentry *rv_this_stats_file;
+
+/* Called before tracepoints are registered, so memset cannot race an update. */
+static void rv_edge_stats_reset(void)
+{
+	int cpu;
+
+	for_each_possible_cpu(cpu)
+		memset(per_cpu_ptr(&DA_MON_EDGES, cpu), 0,
+		       sizeof(struct rv_this_edges));
+}
+
+static int rv_edge_stats_show(struct seq_file *seq, void *v)
+{
+	unsigned int e;
+	int cpu;
+
+	seq_puts(seq, "# cpu edge label count sum_ns max_ns\n");
+	/* Include offline CPUs and keep output stable across CPU hotplug. */
+	for_each_possible_cpu(cpu) {
+		struct rv_this_edges *m = per_cpu_ptr(&DA_MON_EDGES, cpu);
+
+		for (e = 0; e < RV_THIS_NR_EDGES; e++)
+			seq_printf(seq, "%d %u %s:%s %llu %llu %llu\n",
+				   cpu, e,
+				   model_get_state_name(e / EVENT_MAX),
+				   model_get_event_name(e % EVENT_MAX),
+				   (u64)local64_read(&m->edge[e].count),
+				   (u64)local64_read(&m->edge[e].sum_ns),
+				   (u64)local64_read(&m->edge[e].max_ns));
+	}
+	return 0;
+}
+DEFINE_SHOW_ATTRIBUTE(rv_edge_stats);
+
+static int rv_edge_stats_create(struct dentry *parent)
+{
+	rv_edge_stats_reset();
+	/* RV_MODE_READ is private to kernel/trace/rv/. */
+	rv_this_stats_file = tracefs_create_file("stats", 0440, parent,
+						 NULL, &rv_edge_stats_fops);
+	return rv_this_stats_file ? 0 : -ENOMEM;
+}
+
+static void rv_edge_stats_remove(void)
+{
+	tracefs_remove(rv_this_stats_file);
+	rv_this_stats_file = NULL;
+}
+
+/* A zero timestamp marks resets, which can run on a different CPU. */
+#define da_state_entered(s)	da_state_pack((s), local_clock() & RV_TS_MASK)
+
+static __always_inline void
+rv_edge_account(da_state_t old, da_state_t new, enum states curr, enum events ev)
+{
+	struct rv_this_edges *m;
+	u64 prev = da_ts_of(old);
+
+	if (!prev)
+		return;
+
+	m = this_cpu_ptr(&DA_MON_EDGES);
+	rv_edge_stat_account(&m->edge[curr * EVENT_MAX + ev],
+			     (da_ts_of(new) - prev) & RV_TS_MASK);
+}
+
+#else /* per-cpu accounting off for this monitor type */
+
+#define da_state_entered(s)	((da_state_t)(s))
+
+static __always_inline void
+rv_edge_account(da_state_t old, da_state_t new, enum states curr, enum events ev) { }
+
+#endif /* RV_MON_TYPE == RV_MON_PER_CPU */
+
+static __always_inline bool
+da_state_try_commit(da_state_t *word, da_state_t *old, enum states next,
+		    enum events event)
+{
+	da_state_t prev = *old;
+	da_state_t new = da_state_entered(next);
+
+	if (!try_cmpxchg(word, old, new))
+		return false;
+
+	rv_edge_account(prev, new, da_state_of(prev), event);
+	return true;
+}
+
+#else /* !CONFIG_RV_EDGE_STAT */
+
+/*
+ * Feature off: only the hooks the DA/HA layer calls are provided, as trivial
+ * pass-throughs. da_state_t is a plain state word with no packed timestamp.
+ */
+#define da_state_of(w)		((unsigned int)(w))
+#define da_state_entered(s)	(s)
+
+static __always_inline bool
+da_state_try_commit(da_state_t *word, da_state_t *old, enum states next,
+		    enum events event)
+{
+	return try_cmpxchg(word, old, next);
+}
+
+#if RV_MON_TYPE == RV_MON_PER_CPU
+static inline int rv_edge_stats_create(struct dentry *parent) { return 0; }
+static inline void rv_edge_stats_remove(void) { }
+#endif
+
 #endif /* CONFIG_RV_EDGE_STAT */
 
 #endif /* _RV_EDGE_STAT_H */
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 3884b14df375..3045037fb36a 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -59,6 +59,18 @@ config RV_PER_TASK_MONITORS
 	  This option configures the maximum number of per-task RV monitors that can run
 	  simultaneously.
 
+config RV_EDGE_STAT
+	bool "Per-edge dwell-time statistics"
+	depends on RV && 64BIT && DA_MON_EVENTS_IMPLICIT
+	help
+	  Record per-edge dwell-time statistics for per-cpu deterministic and
+	  hybrid automaton monitors and expose them through a per-monitor
+	  "stats" tracefs file. This times each monitored automaton transition
+	  with local_clock(), so leave it off if you do not need the
+	  statistics.
+
+	  If unsure, say N.
+
 source "kernel/trace/rv/monitors/wip/Kconfig"
 source "kernel/trace/rv/monitors/wwnr/Kconfig"
 
-- 
2.43.0


^ permalink raw reply	[flat|nested] 13+ messages in thread

* [PATCH v2 3/3] rv: collect per-edge dwell time for per-cpu DA/HA monitors
  2026-09-11 12:34 [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors Tobias Schaffner
  2026-09-11 12:34 ` [PATCH v2 1/3] rv: add per-edge dwell-time statistics primitive Tobias Schaffner
  2026-09-11 12:34 ` [PATCH v2 2/3] rv: add per-monitor edge-stat facility and stats file Tobias Schaffner
@ 2026-09-11 12:34 ` Tobias Schaffner
  2026-09-24  7:18   ` Gabriele Monaco
  2026-10-12 11:47 ` [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors Gabriele Monaco
  3 siblings, 1 reply; 13+ messages in thread
From: Tobias Schaffner @ 2026-09-11 12:34 UTC (permalink / raw)
  To: Steven Rostedt, Gabriele Monaco
  Cc: Jonathan Corbet, Shuah Khan, Masami Hiramatsu, Mathieu Desnoyers,
	linux-trace-kernel, linux-doc, linux-kselftest, linux-kernel,
	rpm, jan.kiszka, Tobias Schaffner

With the core facility in place, hook it into the DA/HA layer so that any
per-CPU automaton monitor also reports how long it lingers in each state.

Pack the automaton state and its entry timestamp into one word so the
transition cmpxchg updates both atomically. This prevents nested events
from attributing dwell time to the wrong edge and requires a native
64-bit cmpxchg.

Account a transition as soon as its state change is committed. An HA
constraint that rejects the transition can therefore reset the monitor
without leaving an accounting window for nested events.

Add a selftest that enables a per-CPU monitor, checks the stats file
appears and is populated under load, and skips cleanly otherwise.

Signed-off-by: Tobias Schaffner <tobias.schaffner@siemens.com>
---
 include/linux/rv.h                            |  9 ++++-
 include/rv/da_monitor.h                       | 16 +++++++--
 include/rv/ha_monitor.h                       |  2 +-
 tools/testing/selftests/verification/config   |  3 ++
 .../verification/test.d/rv_edge_stats.tc      | 33 +++++++++++++++++++
 5 files changed, 58 insertions(+), 5 deletions(-)
 create mode 100644 tools/testing/selftests/verification/test.d/rv_edge_stats.tc

diff --git a/include/linux/rv.h b/include/linux/rv.h
index 541ba404926a..6c5c2fa7dd68 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -21,12 +21,19 @@
 #include <linux/list.h>
 #include <linux/types.h>
 
+/* Edge statistics pack the state and its entry timestamp into one word. */
+#ifdef CONFIG_RV_EDGE_STAT
+#define da_state_t	unsigned long
+#else
+#define da_state_t	unsigned int
+#endif
+
 /*
  * Deterministic automaton per-object variables.
  */
 struct da_monitor {
 	bool		monitoring;
-	unsigned int	curr_state;
+	da_state_t	curr_state;
 };
 
 #ifdef CONFIG_RV_LTL_MONITOR
diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
index 34b8fba9ecd4..bd7bd422b39a 100644
--- a/include/rv/da_monitor.h
+++ b/include/rv/da_monitor.h
@@ -16,6 +16,7 @@
 
 #include <rv/automata.h>
 #include <linux/rv.h>
+#include <rv/edge_stat.h>
 #include <linux/stringify.h>
 #include <linux/bug.h>
 #include <linux/sched.h>
@@ -112,7 +113,7 @@ static inline void da_monitor_reset(struct da_monitor *da_mon)
  */
 static inline void da_monitor_start(struct da_monitor *da_mon)
 {
-	da_mon->curr_state = model_get_initial_state();
+	da_mon->curr_state = da_state_entered(model_get_initial_state());
 	da_monitor_init_hook(da_mon);
 	/* Pairs with smp_load_acquire in da_monitoring(). */
 	smp_store_release(&da_mon->monitoring, 1);
@@ -275,6 +276,11 @@ static inline void da_monitor_reset_state_all(void)
  */
 static inline int da_monitor_init(void)
 {
+	int retval = rv_edge_stats_create(rv_this.root_d);
+
+	if (retval)
+		return retval;
+
 	da_monitor_reset_state_all();
 	return 0;
 }
@@ -286,6 +292,7 @@ static inline void da_monitor_destroy(void)
 {
 	da_monitor_reset_all();
 	da_monitor_sync_hook();
+	rv_edge_stats_remove();
 }
 
 #ifndef da_implicit_guard
@@ -683,9 +690,11 @@ static inline void da_trace_error(struct da_monitor *da_mon,
 static inline bool da_event(struct da_monitor *da_mon, enum events event, da_id_type id)
 {
 	enum states curr_state, next_state;
+	da_state_t old;
 
-	curr_state = READ_ONCE(da_mon->curr_state);
+	old = READ_ONCE(da_mon->curr_state);
 	for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) {
+		curr_state = da_state_of(old);
 		next_state = model_get_next_state(curr_state, event);
 		if (next_state == INVALID_STATE) {
 			react(curr_state, event);
@@ -693,7 +702,8 @@ static inline bool da_event(struct da_monitor *da_mon, enum events event, da_id_
 				       model_get_event_name(event), id);
 			return false;
 		}
-		if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) {
+		if (likely(da_state_try_commit(&da_mon->curr_state, &old,
+					       next_state, event))) {
 			if (!da_monitor_event_hook(da_mon, curr_state, event, next_state, id))
 				return false;
 			da_trace_event(da_mon, model_get_state_name(curr_state),
diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h
index 28d3c74cabfc..4def2aac92de 100644
--- a/include/rv/ha_monitor.h
+++ b/include/rv/ha_monitor.h
@@ -312,7 +312,7 @@ static inline void __ha_monitor_timer_callback(struct ha_monitor *ha_mon)
 	if (unlikely(READ_ONCE(ha_mon_destroying)))
 		return;
 	/* Ensure consistent curr_state if we race with da_monitor_reset */
-	curr_state = smp_load_acquire(&ha_mon->da_mon.curr_state);
+	curr_state = da_state_of(smp_load_acquire(&ha_mon->da_mon.curr_state));
 	if (unlikely(!da_monitor_handling_event(&ha_mon->da_mon)))
 		return;
 
diff --git a/tools/testing/selftests/verification/config b/tools/testing/selftests/verification/config
index 43072c1c38f4..caf3a96ac8b4 100644
--- a/tools/testing/selftests/verification/config
+++ b/tools/testing/selftests/verification/config
@@ -1 +1,4 @@
 CONFIG_RV=y
+CONFIG_PREEMPT_TRACER=y
+CONFIG_RV_MON_WIP=y
+CONFIG_RV_EDGE_STAT=y
diff --git a/tools/testing/selftests/verification/test.d/rv_edge_stats.tc b/tools/testing/selftests/verification/test.d/rv_edge_stats.tc
new file mode 100644
index 000000000000..616bb0b5166e
--- /dev/null
+++ b/tools/testing/selftests/verification/test.d/rv_edge_stats.tc
@@ -0,0 +1,33 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0-or-later
+# description: Test per-edge dwell-time statistics (stats)
+
+MON=wip
+
+check_requires "$MON:monitor"
+
+# The "stats" file is created on enable; if it is still missing the kernel was
+# built without CONFIG_RV_EDGE_STAT, so skip.
+echo 1 > "monitors/$MON/enable"
+if [ ! -e "monitors/$MON/stats" ]; then
+	echo 0 > "monitors/$MON/enable"
+	echo "CONFIG_RV_EDGE_STAT is not enabled."
+	exit_unsupported
+fi
+
+# The first line is the column header; the body has one line per (cpu, edge).
+head -n1 "monitors/$MON/stats" | grep -q "^# cpu edge label count sum_ns max_ns"
+[ "$(grep -cvE '^#' "monitors/$MON/stats")" -gt 0 ]
+
+# Drive some scheduler activity so the automaton records transitions.
+for _ in 1 2 3 4 5 6 7 8 9 10; do
+	(true) &
+	wait
+done
+
+# At least one edge must now show a non-zero count. Do not require a non-zero
+# dwell: a coarse local_clock() may legitimately return the same value twice.
+grep -vE '^#' "monitors/$MON/stats" | \
+	awk '$4 > 0 && $5 >= $6 { hit = 1 } END { exit !hit }'
+
+echo 0 > "monitors/$MON/enable"
-- 
2.43.0


^ permalink raw reply	[flat|nested] 13+ messages in thread

* Re: [PATCH v2 3/3] rv: collect per-edge dwell time for per-cpu DA/HA monitors
  2026-09-11 12:34 ` [PATCH v2 3/3] rv: collect per-edge dwell time for per-cpu DA/HA monitors Tobias Schaffner
@ 2026-09-24  7:18   ` Gabriele Monaco
  0 siblings, 0 replies; 13+ messages in thread
From: Gabriele Monaco @ 2026-09-24  7:18 UTC (permalink / raw)
  To: Tobias Schaffner, Steven Rostedt
  Cc: Jonathan Corbet, Shuah Khan, Masami Hiramatsu, Mathieu Desnoyers,
	linux-trace-kernel, linux-doc, linux-kselftest, linux-kernel,
	rpm, jan.kiszka

On Fri, 2026-09-11 at 14:34 +0200, Tobias Schaffner wrote:
> With the core facility in place, hook it into the DA/HA layer so that any
> per-CPU automaton monitor also reports how long it lingers in each state.
> 
> Pack the automaton state and its entry timestamp into one word so the
> transition cmpxchg updates both atomically. This prevents nested events
> from attributing dwell time to the wrong edge and requires a native
> 64-bit cmpxchg.
> 
> Account a transition as soon as its state change is committed. An HA
> constraint that rejects the transition can therefore reset the monitor
> without leaving an accounting window for nested events.
> 
> Add a selftest that enables a per-CPU monitor, checks the stats file
> appears and is populated under load, and skips cleanly otherwise.
> 
> Signed-off-by: Tobias Schaffner <tobias.schaffner@siemens.com>
> ---

Sorry for taking that long, I could just have a quick look at your patches, the
approach looks fine but I'm going to need more time to check them carefully,
likely after the LPC conference.

I'm not too fond of how you split into patches. What's the reason for splitting
1/3 and 2/3 ? It seems they both add the new functionality, one step at a time.

...
> +/* Edge statistics pack the state and its entry timestamp into one word. */
> +#ifdef CONFIG_RV_EDGE_STAT
> +#define da_state_t	unsigned long
> +#else
> +#define da_state_t	unsigned int
> +#endif

Also try to define things in order, da_state_t is used in 2/3 but not defined
until 3/3. This doesn't break builds (the header is unused until 3/3) but is
just harder to review.

I find it more natural to split it into 1 add new functionality, 2 wire it, 3
test it. What do you think?

Thanks,
Gabriele


^ permalink raw reply	[flat|nested] 13+ messages in thread

* Re: [PATCH v2 1/3] rv: add per-edge dwell-time statistics primitive
  2026-09-11 12:34 ` [PATCH v2 1/3] rv: add per-edge dwell-time statistics primitive Tobias Schaffner
@ 2026-09-24  7:21   ` Gabriele Monaco
  0 siblings, 0 replies; 13+ messages in thread
From: Gabriele Monaco @ 2026-09-24  7:21 UTC (permalink / raw)
  To: Tobias Schaffner, Steven Rostedt
  Cc: Jonathan Corbet, Shuah Khan, Masami Hiramatsu, Mathieu Desnoyers,
	linux-trace-kernel, linux-doc, linux-kselftest, linux-kernel,
	rpm, jan.kiszka

On Fri, 2026-09-11 at 14:34 +0200, Tobias Schaffner wrote:
> Add a small primitive that records, per automaton edge, how long the
> monitor dwelled before taking it with a count, a sum and a maximum.
> 
> The counters are per-CPU and lock-free, so a monitor's hot path can
> update them without disabling interrupts and without perturbing the latency
> being measured. Keep the state and its entry timestamp in one word so
> nested transitions cannot charge a dwell to the wrong edge.
> 
> Signed-off-by: Tobias Schaffner <tobias.schaffner@siemens.com>
> ---
>  include/rv/edge_stat.h | 69 ++++++++++++++++++++++++++++++++++++++++++
>  1 file changed, 69 insertions(+)
>  create mode 100644 include/rv/edge_stat.h
> 
> diff --git a/include/rv/edge_stat.h b/include/rv/edge_stat.h

...
> +#define RV_STATE_BITS		8
> +#define RV_STATE_MASK		GENMASK(RV_STATE_BITS - 1, 0)
> +#define RV_TS_MASK		GENMASK(BITS_PER_LONG - RV_STATE_BITS - 1, 0)
> +
> +#define da_state_of(w)		((unsigned int)((w) & RV_STATE_MASK))
> +#define da_ts_of(w)		((u64)(w) >> RV_STATE_BITS)
> +#define da_state_pack(s, ts)	(((((da_state_t)(ts)) & RV_TS_MASK) <<
> RV_STATE_BITS) | \
> +				 ((da_state_t)(s) & RV_STATE_MASK))

These are barely readable and error prone, can you use FIELD_GET()/FIELD_PREP()?

Thanks,
Gabriele

> +
> +static __always_inline
> +void rv_edge_stat_account(struct rv_edge_stat *s, u64 dwell_ns)
> +{
> +	s64 max;
> +	int i;
> +
> +	local64_inc(&s->count);
> +	local64_add(dwell_ns, &s->sum_ns);
> +
> +	/* Keep the largest dwell; bound retries if a nested update races us.
> */
> +	max = local64_read(&s->max_ns);
> +	for (i = 0; dwell_ns > (u64)max; i++) {
> +		if (i == MAX_DA_RETRY_RACING_EVENTS) {
> +			WARN_ONCE(1, "rv: edge-stat max update exceeded %d
> retries\n",
> +				  MAX_DA_RETRY_RACING_EVENTS);
> +			break;
> +		}
> +		if (local64_try_cmpxchg(&s->max_ns, &max, dwell_ns))
> +			break;
> +	}
> +}
> +
> +#endif /* CONFIG_RV_EDGE_STAT */
> +
> +#endif /* _RV_EDGE_STAT_H */


^ permalink raw reply	[flat|nested] 13+ messages in thread

* Re: [PATCH v2 2/3] rv: add per-monitor edge-stat facility and stats file
  2026-09-11 12:34 ` [PATCH v2 2/3] rv: add per-monitor edge-stat facility and stats file Tobias Schaffner
@ 2026-09-24  7:47   ` Gabriele Monaco
  2026-10-13 11:43   ` Gabriele Monaco
  1 sibling, 0 replies; 13+ messages in thread
From: Gabriele Monaco @ 2026-09-24  7:47 UTC (permalink / raw)
  To: Tobias Schaffner, Steven Rostedt
  Cc: Jonathan Corbet, Shuah Khan, Masami Hiramatsu, Mathieu Desnoyers,
	linux-trace-kernel, linux-doc, linux-kselftest, linux-kernel,
	rpm, jan.kiszka

On Fri, 2026-09-11 at 14:34 +0200, Tobias Schaffner wrote:
> +static int rv_edge_stats_create(struct dentry *parent)
> +{
> +	rv_edge_stats_reset();
> +	/* RV_MODE_READ is private to kernel/trace/rv/. */
> +	rv_this_stats_file = tracefs_create_file("stats", 0440, parent,
> +						 NULL, &rv_edge_stats_fops);
> +	return rv_this_stats_file ? 0 : -ENOMEM;
> +}
> +
> +static void rv_edge_stats_remove(void)
> +{
> +	tracefs_remove(rv_this_stats_file);
> +	rv_this_stats_file = NULL;
> +}

Very minor nit, just for consistency you may want to use the macros
rv_create_file() / rv_remove(). You also probably don't need to include
tracefs.
You can also just include "rv.h" instead of <linux/rv.h> and
<linux/tracefs.h>.

> +
> +/* A zero timestamp marks resets, which can run on a different CPU. */
> +#define da_state_entered(s)	da_state_pack((s), local_clock() &
> RV_TS_MASK)

Isn't this masking already happening in da_state_pack() ?

Thanks,
Gabriele


^ permalink raw reply	[flat|nested] 13+ messages in thread

* Re: [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors
  2026-09-11 12:34 [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors Tobias Schaffner
                   ` (2 preceding siblings ...)
  2026-09-11 12:34 ` [PATCH v2 3/3] rv: collect per-edge dwell time for per-cpu DA/HA monitors Tobias Schaffner
@ 2026-10-12 11:47 ` Gabriele Monaco
  2026-10-12 16:18   ` Tobias Schaffner
  3 siblings, 1 reply; 13+ messages in thread
From: Gabriele Monaco @ 2026-10-12 11:47 UTC (permalink / raw)
  To: Tobias Schaffner, Steven Rostedt
  Cc: Jonathan Corbet, Shuah Khan, Masami Hiramatsu, Mathieu Desnoyers,
	linux-trace-kernel, linux-doc, linux-kselftest, linux-kernel,
	rpm, jan.kiszka

On Fri, 2026-09-11 at 14:34 +0200, Tobias Schaffner wrote:
> Hi Steven, Gabriele,
> 
> I am using the RV system for a downstream project called EVL (aka Xenomai4).
> It is a small co-kernel system, small enough that I can model the whole
> co-kernel with RV instead of just a fragment of it.
> 
> The patches in this series add a per-monitor "stats" file that exposes how
> often an edge has been visited and the dwell time in the prior state for
> per-cpu monitors.
> 
> This allows me to not only check if the model is correct but also to see if
> all paths are exercised by my stress tooling and to decompose the latency of
> the co-kernel's wakeup path.
> 
> I think that some of the upstream monitors like e.g. the sts monitor could
> also profit from this.

Hi Tobias,

there's been a conversation at LPC about completely migrating RV to BPF.
While we aren't sure of its feasibility yet, and it will take time, it's
something to keep in mind for new contributions.

First of all, would dropping RV in-kernel support negatively affect your current
workflow?

About this series, I believe we could implement the same using BPF maps without
too much effort, then the rv userspace tool could display them nicely.

What do you think?

Thanks,
Gabriele


^ permalink raw reply	[flat|nested] 13+ messages in thread

* Re: [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors
  2026-10-12 11:47 ` [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors Gabriele Monaco
@ 2026-10-12 16:18   ` Tobias Schaffner
  2026-10-12 19:21     ` Steven Rostedt
  2026-10-13  7:26     ` Gabriele Monaco
  0 siblings, 2 replies; 13+ messages in thread
From: Tobias Schaffner @ 2026-10-12 16:18 UTC (permalink / raw)
  To: Gabriele Monaco, Steven Rostedt
  Cc: Jonathan Corbet, Shuah Khan, Masami Hiramatsu, Mathieu Desnoyers,
	linux-trace-kernel, linux-doc, linux-kselftest, linux-kernel,
	rpm, jan.kiszka

On 10/12/26 13:47, Gabriele Monaco wrote:
> On Fri, 2026-09-11 at 14:34 +0200, Tobias Schaffner wrote:
>> Hi Steven, Gabriele,
>>
>> I am using the RV system for a downstream project called EVL (aka Xenomai4).
>> It is a small co-kernel system, small enough that I can model the whole
>> co-kernel with RV instead of just a fragment of it.
>>
>> The patches in this series add a per-monitor "stats" file that exposes how
>> often an edge has been visited and the dwell time in the prior state for
>> per-cpu monitors.
>>
>> This allows me to not only check if the model is correct but also to see if
>> all paths are exercised by my stress tooling and to decompose the latency of
>> the co-kernel's wakeup path.
>>
>> I think that some of the upstream monitors like e.g. the sts monitor could
>> also profit from this.
> 
> Hi Tobias,
> 
> there's been a conversation at LPC about completely migrating RV to BPF.
> While we aren't sure of its feasibility yet, and it will take time, it's
> something to keep in mind for new contributions.

Hi Gabriele,

first thanks for the reviews and for keeping me in the loop, I really
appreciate it. I unfortunately was not able to attend LPC this year, but
I followed the discussions and watched your presentation.

> First of all, would dropping RV in-kernel support negatively affect your current
> workflow?

I am afraid it would, but first mine is a niche use case, and
second I am not very experienced with BPF, so please weigh that in.

> About this series, I believe we could implement the same using BPF maps without
> too much effort, then the rv userspace tool could display them nicely.
> 
> What do you think?

 From an implementation perspective there may be a few pieces missing,
both in EVL and in BPF, to make this work. But I guess most of them can
use the patterns the kernel already has for NMIs, so I expect we would
find a way.

I have two more fundamental concerns though. One about verification and
one about recording dwell times.

Regarding verification:
The path I verify is deliberately kept short and simple. RV fits well
because the probe is a plain function call and the state update is a
try_cmpxchg that cannot fail, so it adds very little. A BPF program
brings more machinery into the probe path doesn't it? I fear that adding
this would force me to verify that the new RV system does not change the
behavior of the system we are trying to verify, and I suspect that could
be harder than verifying the system itself.

Regarding dwell timings:
The numbers you presented look very good. But wouldn't we lose
determinism by using BPF? If I want to use this as a measurement tool, I
need it either not to add latency or to add a constant amount. The mean
wake-up latency of EVL on my system is around 10 us, so an observer does
not have to be very variable before I can no longer tell its jitter from
the timings I am trying to measure.

Really looking forward to your opinion on this.

Thanks and all the best,
Tobias

> 
> Thanks,
> Gabriele
> 


^ permalink raw reply	[flat|nested] 13+ messages in thread

* Re: [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors
  2026-10-12 16:18   ` Tobias Schaffner
@ 2026-10-12 19:21     ` Steven Rostedt
  2026-10-13  7:53       ` Gabriele Monaco
  2026-10-13  7:26     ` Gabriele Monaco
  1 sibling, 1 reply; 13+ messages in thread
From: Steven Rostedt @ 2026-10-12 19:21 UTC (permalink / raw)
  To: Tobias Schaffner
  Cc: Gabriele Monaco, Jonathan Corbet, Shuah Khan, Masami Hiramatsu,
	Mathieu Desnoyers, linux-trace-kernel, linux-doc,
	linux-kselftest, linux-kernel, rpm, jan.kiszka

On Mon, 12 Oct 2026 18:18:52 +0200
Tobias Schaffner <tobias.schaffner@siemens.com> wrote:

> Regarding verification:
> The path I verify is deliberately kept short and simple. RV fits well
> because the probe is a plain function call and the state update is a
> try_cmpxchg that cannot fail, so it adds very little. A BPF program
> brings more machinery into the probe path doesn't it? I fear that adding
> this would force me to verify that the new RV system does not change the
> behavior of the system we are trying to verify, and I suspect that could
> be harder than verifying the system itself.

This brings back memories of conversations I had with Daniel. When asked
about how this is being used in formal verification of safety critical
systems, he told me that only the RV verifier itself needed to be verified
and to show what it is verifying can be verified via it. For example,
running Linux in autonomous vehicles handling critical systems the watchdog
had to be verified that it could catch lockups. As the watchdog would
trigger fail-safe mode if something went wrong. RV would be monitoring the
watchdog and if RV detected something it would panic the machine, which
would immediately force the vehicle into fail-safe mode (stop lots of
features and only keep those that can stop the vehicle safely).

Can using BPF as the RV verifier be formally verified? As verification for
RV monitors did look at the binary. Is BPF optimized to machine language
before it enters the kernel? If not, can we formally verify the BPF
verifier created the correct binary? Maybe, I don't know.

Maybe the safety-critical project was canceled and this is no longer needed.

-- Steve

^ permalink raw reply	[flat|nested] 13+ messages in thread

* Re: [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors
  2026-10-12 16:18   ` Tobias Schaffner
  2026-10-12 19:21     ` Steven Rostedt
@ 2026-10-13  7:26     ` Gabriele Monaco
  1 sibling, 0 replies; 13+ messages in thread
From: Gabriele Monaco @ 2026-10-13  7:26 UTC (permalink / raw)
  To: Tobias Schaffner, Steven Rostedt
  Cc: Jonathan Corbet, Shuah Khan, Masami Hiramatsu, Mathieu Desnoyers,
	linux-trace-kernel, linux-doc, linux-kselftest, linux-kernel,
	rpm, jan.kiszka

On Mon, 2026-10-12 at 18:18 +0200, Tobias Schaffner wrote:
> > First of all, would dropping RV in-kernel support negatively affect your
> > current workflow?
> 
> I am afraid it would, but first mine is a niche use case, and
> second I am not very experienced with BPF, so please weigh that in.

Thanks for sharing, I'm asking this question precisely to find out all use
cases. RV is itself a niche tool, so I'd rather not squash use-cases away!

> > About this series, I believe we could implement the same using BPF maps
> > without too much effort, then the rv userspace tool could display them
> > nicely.
> > 
> > What do you think?
> 
>  From an implementation perspective there may be a few pieces missing,
> both in EVL and in BPF, to make this work. But I guess most of them can
> use the patterns the kernel already has for NMIs, so I expect we would
> find a way.

I'm curious to know how exactly you're tracing EVL right now. Are you having it
generate NMIs to linux and catch their tracepoints?

RV attaches to tracepoints and BPF would do exactly the same.

> I have two more fundamental concerns though. One about verification and
> one about recording dwell times.
> 
> Regarding verification:
> The path I verify is deliberately kept short and simple. RV fits well
> because the probe is a plain function call and the state update is a
> try_cmpxchg that cannot fail, so it adds very little. A BPF program
> brings more machinery into the probe path doesn't it? I fear that adding
> this would force me to verify that the new RV system does not change the
> behavior of the system we are trying to verify, and I suspect that could
> be harder than verifying the system itself.

I had a few conversation with some Functional Safety folks over the past weeks
(the same people Daniel used to talk to), I now understand the problem better.

Their use-case was even stricter, that's why RV didn't take off for them,
essentially they're trying to prove some more isolation from interference RV
doesn't really have out of the box.

But back to the RV vs BPF case, I'm trying to reuse the exact same code in
handlers, so the verification step should be mostly equivalent.

Assuming you'd use tracepoints (BPF can have more probes but vanilla RV does
not), I guess you'd need to validate also the ftrace code that ends up calling
your handler. BPF adds a bit more on top of that too, not much though.

Then obviously there's the data representation: we use BPF maps that can be
quite complex, though simple arrays (in per-cpu/global monitors) shouldn't be.
That would probably add more to the verification you need to make..

> Regarding dwell timings:
> The numbers you presented look very good. But wouldn't we lose
> determinism by using BPF? If I want to use this as a measurement tool, I
> need it either not to add latency or to add a constant amount. The mean
> wake-up latency of EVL on my system is around 10 us, so an observer does
> not have to be very variable before I can no longer tell its jitter from
> the timings I am trying to measure.

Ok that's a good point I'd like to investigate more. BPF shows great performance
in the average case, though I fear it could have worst case spikes my quick
tests didn't show.

I'd need to run more numbers to be absolutely sure of that, I'm not aware of any
internal locks in the simple maps we are using (though I only quickly checked).
BPF maps are clearly heavier (memory indirection and/or function calls,
sometimes mitigated by the JIT). But if we properly set them up we shouldn't
expect big determinism issues.
Nevertheless, this is definitely something I need to look into.

The whole JIT thing shouldn't bring big problems either, once handlers are
compiled, they should run almost natively, but again, I am not too familiar with
everything that happens under the hood so take this with a grain of salt.

Thanks,
Gabriele


^ permalink raw reply	[flat|nested] 13+ messages in thread

* Re: [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors
  2026-10-12 19:21     ` Steven Rostedt
@ 2026-10-13  7:53       ` Gabriele Monaco
  0 siblings, 0 replies; 13+ messages in thread
From: Gabriele Monaco @ 2026-10-13  7:53 UTC (permalink / raw)
  To: Steven Rostedt, Tobias Schaffner
  Cc: Jonathan Corbet, Shuah Khan, Masami Hiramatsu, Mathieu Desnoyers,
	linux-trace-kernel, linux-doc, linux-kselftest, linux-kernel,
	rpm, jan.kiszka

On Mon, 2026-10-12 at 15:21 -0400, Steven Rostedt wrote:
> This brings back memories of conversations I had with Daniel. When asked
> about how this is being used in formal verification of safety critical
> systems, he told me that only the RV verifier itself needed to be verified
> and to show what it is verifying can be verified via it. For example,
> running Linux in autonomous vehicles handling critical systems the watchdog
> had to be verified that it could catch lockups. As the watchdog would
> trigger fail-safe mode if something went wrong. RV would be monitoring the
> watchdog and if RV detected something it would panic the machine, which
> would immediately force the vehicle into fail-safe mode (stop lots of
> features and only keep those that can stop the vehicle safely).

Yeah I talked to the same people working on that project, eventually there were
more problems like verifying RV can't be affected by the code it's verifying.
This is still an open problem though.

> Can using BPF as the RV verifier be formally verified? As verification for
> RV monitors did look at the binary. Is BPF optimized to machine language
> before it enters the kernel? If not, can we formally verify the BPF
> verifier created the correct binary? Maybe, I don't know.

As far as I understand, verifying the BPF verifier would take an insane amount
of work, the go-to approach is manually validating only the code you know you
are running. Let's say up to a point where you can realistically say it behaves
like you want it to.
In short, having a verifier doesn't add much value here, at least until someone
verifies that too.

Then there are the levels of indirection, BPF C code gets compiled to BPF
bytecode and that gets JIT compiled inside the kernel. Now it's machine code.

If people are normally not validating clang/gcc produce machine code consistent
to the verified source code, this case should be equivalent, but I'm just
speculating here.

Gabriele


^ permalink raw reply	[flat|nested] 13+ messages in thread

* Re: [PATCH v2 2/3] rv: add per-monitor edge-stat facility and stats file
  2026-09-11 12:34 ` [PATCH v2 2/3] rv: add per-monitor edge-stat facility and stats file Tobias Schaffner
  2026-09-24  7:47   ` Gabriele Monaco
@ 2026-10-13 11:43   ` Gabriele Monaco
  1 sibling, 0 replies; 13+ messages in thread
From: Gabriele Monaco @ 2026-10-13 11:43 UTC (permalink / raw)
  To: Tobias Schaffner, Steven Rostedt
  Cc: Jonathan Corbet, Shuah Khan, Masami Hiramatsu, Mathieu Desnoyers,
	linux-trace-kernel, linux-doc, linux-kselftest, linux-kernel,
	rpm, jan.kiszka

On Fri, 2026-09-11 at 14:34 +0200, Tobias Schaffner wrote:
> Add CONFIG_RV_EDGE_STAT, an optional feature that records how long a
> monitor's automaton dwells in a state and exposes it per edge through a
> per-monitor "stats" tracefs file.
> 
> The facility uses a static per-CPU matrix and reports, per edge and per
> CPU, the count, summed dwell time and maximum dwell time. Only the owning
> CPU writes the counters, so a reader snapshots them with local64_read()
> with no IPI and no locking on the accounting path.
> 
> Signed-off-by: Tobias Schaffner <tobias.schaffner@siemens.com>
> ---
...

> +
> +/*
> + * Static storage avoids allocation lifetime races. Only the owning CPU
> writes,
> + * so readers can snapshot counters with local64_read().
> + */
> +#define RV_THIS_NR_EDGES	(STATE_MAX * EVENT_MAX)
> +
> +struct rv_this_edges {
> +	struct rv_edge_stat	edge[RV_THIS_NR_EDGES];
> +};

Does this really need to be a new struct? Cannot you just define it as:

DEFINE_PER_CPU(struct rv_edge_stat[RV_THIS_NR_EDGES], DA_MON_EDGES);

Then use it as:

per_cpu_ptr(DA_MON_EDGES, cpu), sizeof(DA_MON_EDGES)

struct rv_edge_stat *edges = per_cpu_ptr(DA_MON_EDGES, cpu);
&edges[e].count

> +
> +static DEFINE_PER_CPU(struct rv_this_edges, DA_MON_EDGES);
> +static struct dentry *rv_this_stats_file;
> +
> +/* Called before tracepoints are registered, so memset cannot race an update.
> */
> +static void rv_edge_stats_reset(void)
> +{
> +	int cpu;
> +
> +	for_each_possible_cpu(cpu)
> +		memset(per_cpu_ptr(&DA_MON_EDGES, cpu), 0,
> +		       sizeof(struct rv_this_edges));
> +}
> +
> +static int rv_edge_stats_show(struct seq_file *seq, void *v)
> +{
> +	unsigned int e;
> +	int cpu;
> +
> +	seq_puts(seq, "# cpu edge label count sum_ns max_ns\n");
> +	/* Include offline CPUs and keep output stable across CPU hotplug. */
> +	for_each_possible_cpu(cpu) {
> +		struct rv_this_edges *m = per_cpu_ptr(&DA_MON_EDGES, cpu);
> +
> +		for (e = 0; e < RV_THIS_NR_EDGES; e++)
> +			seq_printf(seq, "%d %u %s:%s %llu %llu %llu\n",
> +				   cpu, e,
> +				   model_get_state_name(e / EVENT_MAX),
> +				   model_get_event_name(e % EVENT_MAX),

Perhaps you could have macros like DA_EDGE(s, e) or DA_EDGE_TO_EVENT(e)
DA_EDGE_TO_STATE(s) to make the matrix selection a bit more readable,
but that's a matter of taste.

> +				   (u64)local64_read(&m->edge[e].count),
> +				   (u64)local64_read(&m->edge[e].sum_ns),
> +				   (u64)local64_read(&m->edge[e].max_ns));
> +	}

I would like to see a way to tell if an edge is invalid or not, we
expect zero on invalid edges.
Perhaps that can be a new column so you also show the count in case they
are not 0.

You can just use model_get_next_state() == INVALID_STATE

> +	return 0;
> +}
> +DEFINE_SHOW_ATTRIBUTE(rv_edge_stats);
> +
> +static int rv_edge_stats_create(struct dentry *parent)
> +{
> +	rv_edge_stats_reset();
> +	/* RV_MODE_READ is private to kernel/trace/rv/. */

I suggested you to use the rv helpers for this, you can obviously also
use RV_MODE_READ. Now monitors are in kernel/trace/rv/, so it won't be
an issue.

If we add support for modular monitors, moving the definitions to
linux/rv.h is the easiest thing to do anyway (you can do it too if you
really want and/or your agents complain, in a separate commit).

> +	rv_this_stats_file = tracefs_create_file("stats", 0440, parent,
> +						 NULL, &rv_edge_stats_fops);
> +	return rv_this_stats_file ? 0 : -ENOMEM;
> +}
> +
> +static void rv_edge_stats_remove(void)
> +{
> +	tracefs_remove(rv_this_stats_file);
> +	rv_this_stats_file = NULL;
> +}
> +
> +/* A zero timestamp marks resets, which can run on a different CPU. */
> +#define da_state_entered(s)	da_state_pack((s), local_clock() &
> RV_TS_MASK)
> +
> +static __always_inline void
> +rv_edge_account(da_state_t old, da_state_t new, enum states curr, enum events
> ev)
> +{
> +	struct rv_this_edges *m;
> +	u64 prev = da_ts_of(old);
> +
> +	if (!prev)
> +		return;

This happens only the first time after reset, isn't it unlikely()?

> +
> +	m = this_cpu_ptr(&DA_MON_EDGES);
> +	rv_edge_stat_account(&m->edge[curr * EVENT_MAX + ev],
> +			     (da_ts_of(new) - prev) & RV_TS_MASK);

If you decide to go for the macro, this would be DA_EDGE(s, e) or whatever
looks clear to you.

> +}
> +
> +#else /* per-cpu accounting off for this monitor type */
> +
> +#define da_state_entered(s)	((da_state_t)(s))
> +
> +static __always_inline void
> +rv_edge_account(da_state_t old, da_state_t new, enum states curr, enum events
> ev) { }
> +
> +#endif /* RV_MON_TYPE == RV_MON_PER_CPU */
> +
> +static __always_inline bool
> +da_state_try_commit(da_state_t *word, da_state_t *old, enum states next,
> +		    enum events event)
> +{
> +	da_state_t prev = *old;
> +	da_state_t new = da_state_entered(next);
> +
> +	if (!try_cmpxchg(word, old, new))
> +		return false;
> +
> +	rv_edge_account(prev, new, da_state_of(prev), event);
> +	return true;
> +}
> +
> +#else /* !CONFIG_RV_EDGE_STAT */
> +
> +/*
> + * Feature off: only the hooks the DA/HA layer calls are provided, as trivial
> + * pass-throughs. da_state_t is a plain state word with no packed timestamp.
> + */
> +#define da_state_of(w)		((unsigned int)(w))

Is this cast necessary? We assign it to an enum, the sign isn't really
important. I guess it's the same for the other implementation of
da_state_of() (which is now in another patch).

Thanks,
Gabriele


> +#define da_state_entered(s)	(s)
> +
> +static __always_inline bool
> +da_state_try_commit(da_state_t *word, da_state_t *old, enum states next,
> +		    enum events event)
> +{
> +	return try_cmpxchg(word, old, next);
> +}
> +
> +#if RV_MON_TYPE == RV_MON_PER_CPU
> +static inline int rv_edge_stats_create(struct dentry *parent) { return 0; }
> +static inline void rv_edge_stats_remove(void) { }
> +#endif
> +
>  #endif /* CONFIG_RV_EDGE_STAT */
>  
>  #endif /* _RV_EDGE_STAT_H */
> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
> index 3884b14df375..3045037fb36a 100644
> --- a/kernel/trace/rv/Kconfig
> +++ b/kernel/trace/rv/Kconfig
> @@ -59,6 +59,18 @@ config RV_PER_TASK_MONITORS
>  	  This option configures the maximum number of per-task RV monitors
> that can run
>  	  simultaneously.
>  
> +config RV_EDGE_STAT
> +	bool "Per-edge dwell-time statistics"
> +	depends on RV && 64BIT && DA_MON_EVENTS_IMPLICIT
> +	help
> +	  Record per-edge dwell-time statistics for per-cpu deterministic and
> +	  hybrid automaton monitors and expose them through a per-monitor
> +	  "stats" tracefs file. This times each monitored automaton
> transition
> +	  with local_clock(), so leave it off if you do not need the
> +	  statistics.
> +
> +	  If unsure, say N.
> +
>  source "kernel/trace/rv/monitors/wip/Kconfig"
>  source "kernel/trace/rv/monitors/wwnr/Kconfig"
> 


^ permalink raw reply	[flat|nested] 13+ messages in thread

end of thread, other threads:[~2026-10-13 11:44 UTC | newest]

Thread overview: 13+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2026-09-11 12:34 [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors Tobias Schaffner
2026-09-11 12:34 ` [PATCH v2 1/3] rv: add per-edge dwell-time statistics primitive Tobias Schaffner
2026-09-24  7:21   ` Gabriele Monaco
2026-09-11 12:34 ` [PATCH v2 2/3] rv: add per-monitor edge-stat facility and stats file Tobias Schaffner
2026-09-24  7:47   ` Gabriele Monaco
2026-10-13 11:43   ` Gabriele Monaco
2026-09-11 12:34 ` [PATCH v2 3/3] rv: collect per-edge dwell time for per-cpu DA/HA monitors Tobias Schaffner
2026-09-24  7:18   ` Gabriele Monaco
2026-10-12 11:47 ` [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors Gabriele Monaco
2026-10-12 16:18   ` Tobias Schaffner
2026-10-12 19:21     ` Steven Rostedt
2026-10-13  7:53       ` Gabriele Monaco
2026-10-13  7:26     ` Gabriele Monaco

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox

all inboxes | Powered by JetHome®