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
