Re: [PATCH v2 0/3] rv: per-edge dwell-time statistics for per-cpu monitors

[Steven Rostedt <rostedt@goodmis.org>]

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