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