On Thu, 2026-08-27 at 09:23 +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.
Hi Tobias, Haven't heard about Xenomai in a while.. That sounds very interesting. Since it's something out-of-tree you likely don't want to submit monitors upstream, but if you can trigger BPF events from your co-kernel you may want to have a look at RV BPF monitors, which I'm likely going to submit in a couple of days. Otherwise we can always get out-of-tree monitors as modules, currently not supported just out of a missing use-case. > 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. The idea crossed my mind a few times, good you came up with an implementation! > 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. Your first need (see if all paths are exercised) doesn't really require the stat to be per-monitor-instance (i.e. per-cpu) right? You could have a global accumulator matrix, at least for count and sum where you can be atomic. This could extend the feature to other types of monitors. Just brainstorming here though. > 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. As said before, I haven't really played with an implementation but I think atomic types may help here. > What is your opinion on this? Do you think this is worth getting upstreamed? I will have a look at your patches but it's definitely something I'd want. Thanks, Gabriele > > Thanks for taking a look, > Tobias > > 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 | 24 ++++ > MAINTAINERS | 1 + > include/linux/rv.h | 18 +++ > include/linux/rv_edge_stat.h | 60 +++++++++ > include/rv/da_monitor.h | 53 ++++++++ > kernel/trace/rv/Kconfig | 11 ++ > kernel/trace/rv/rv.c | 116 +++++++++++++++++- > tools/testing/selftests/verification/config | 1 + > .../verification/test.d/rv_edge_stats.tc | 32 +++++ > 9 files changed, 315 insertions(+), 1 deletion(-) > create mode 100644 include/linux/rv_edge_stat.h > create mode 100644 > tools/testing/selftests/verification/test.d/rv_edge_stats.tc
