Re: [RFC PATCH 00/11] rv: Add scheduler specification monitors

[Juri Lelli]

Hi Gabriele,

On 06/02/25 09:09, Gabriele Monaco wrote:
> This patchset starts including adapted scheduler specifications from
> Daniel's task model [1].

Thanks a lot for working on this. Apart from being cool stuff per-se, it
means a lot personally to see Daniel's work continuing to be developed.

> As the model is fairly complicated, it is split in several generators
> and specifications. The tool used to create the model can output a
> unified model, but that would be hardly readable (9k states).
> 
> RV allows monitors to run and react concurrently. Running the cumulative
> model is equivalent to running single components using the same
> reactors, with the advantage that it's easier to point out which
> specification failed in case of error.
> 
> We allow this by introducing nested monitors, in short, the sysfs
> monitor folder will contain a monitor named sched, which is nothing but
> an empty container for other monitors. Controlling the sched monitor
> (enable, disable, set reactors) controls all nested monitors.
> 
> The task model proposed by Daniel includes 12 generators and 33
> specifications. The generators are good for documentation but are
> usually implied in some specifications.
> Not all monitors work out of the box, mainly because of those reasons:
> * need to distinguish if preempt disable leads to schedule
> * need to distinguish if irq disable comes from an actual irq
> * assumptions not always true on SMP
> 
> The original task model was designed for PREEMPT_RT and this patchset is
> only tested on an upstream kernel with full preemption enabled.

I played with your additions a bit and I was able to enable/disable
monitors, switch reactors, etc., w/o noticing any issue.

I wonder if you also had ways to test that the monitors actually react
properly in case of erroneous conditions (so that we can see a reactor
actually react :).

Thanks,
Juri