Speaker
Gabriele Monaco
(Red Hat Inc.)
Description
With the ongoing work on RV and the deadline scheduler, coupled with timed automata, we introduced a practical way to validate timing properties in the kernel.
Now we can have models guaranteeing that tasks are throttled when consuming their runtime and don't miss their deadline.
The few models for the deadline scheduler are barely scratching the surface of what could be done to validate it.
A few questions come to mind:
- What timing properties are interesting to model in other schedulers?
- Can we validate more subsystems without affecting their behaviour?
- Timed automata don't allow concurrency: do we need other model types?
- How much of this can be general enough not to break at the next iteration of a scheduler?
Primary author
Gabriele Monaco
(Red Hat Inc.)