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
