Re: [RFC PATCH 0/9] rv: Verify generic IRQ context transitions

On Fri, Oct 23, 2026 at 06:05:30PM +0100, Gabriele Monaco wrote:

On Thu, 2026-10-22 at 07:07 +0200, Karl Mehltretter wrote:

quoted

This RFC adds events at the generic hardirq and serving-softirq
boundaries. The irqstate RV monitor checks their order and agreement with
live kernel state. irqexit follows the owner of a preempt_schedule_irq()
invocation across task switches and CPU migration.

Hi Karl,

thanks for your contribution!
I'm probably not going to have much time to look at this soon as I have a few
holidays planned and other series to review first. But it looks interesting.

What points my eyes is that you didn't include any schematic graph in the
documentation.
Some folks don't like RST, but I find having a textual representation of the
model there easy to understand what you're trying to do without having to build
the models.
We use graph-easy for that (and adapt things if the model is too complex).

Do not send a V2 just for this, but please keep that in mind for next time.

Hi Gabriele,

thanks for the encouragment! Yes I continue working on this RFC and use
it to check for my related early irq cleanup series. I will use your doc
suggestion.

I will wait for further input and liekly post a v2 in a week or two.

Any broad strategic direction for me and my LLM are always welcome.

Regards,
Karl