This series contains several related changes, the main areas are:
* hybrid automata
Hybrid automata are an extension of deterministic automata where each
state transition is validating a constraint on a finite number of
environment variables.
Hybrid automata can be used to implement timed automata, where the
environment variables are clocks.
* per-object monitors
Define the generic per-object monitor allow RV monitors on any kind
of object where the user can specify how to get an id (e.g. pid for
tasks) and the data type for the monitor_target (e.g. struct
task_struct * for tasks).
The monitor storage (e.g. the rv monitor, pointer to the target, etc.)
is stored in a hash table indexed by id.
* deadline monitors collection
Add the throttle and nomiss monitors to validate timing aspects of
the deadline scheduler, as they work for tasks and servers, their
inclusion requires also per-object monitors (for dl entities).
Also add the boost and laxity monitors specific to servers.
The entire series can also be found on:
git.kernel.org/pub/scm/linux/kernel/git/gmonaco/linux.git rv_hybrid_automata
Changes since V5 [1]:
* Export task_is_scx_enabled() for monitors code to determine if tasks are ext
* tracepoints:
- Add dl_se type to differentiate between fair and ext servers
- Add event to track dl_update_curr not firing other events
* monitors:
- Add support for ext server
- Remove mostly unused dl_server_start from nomiss
- Allow to skip runtime constraint on throttle monitor
- Consider also BATCH and IDLE as fair policies
- Handle events only for supported deadline entities (future proof)
- Add missing transition running -> zero_laxity_wait
- Handle dl_update event in laxity to cover missing update without
enqueue nor replenish when multiple server types are active
- Cleanup and sort constraints as generated
* rvgen:
- Use f-strings in newly added code and cleanup
- Sort constraints for predictable generated code
Changes since V4 [2]:
* Do not fire enqueue tracepoint for delayed enqueues
* Do not use boosted dl_se in monitors
* Add enqueue/dequeue validation on snroc model
* Do not export pi_of to deadline.h
* Remove useless variable reset when resetting Hybrid Automata
Changes since V3 [3]:
* Improve ns to jiffy rounding in HA timers
* Use da_handle_start_run_event not to lose the first event in opid
* Sort self_loop_reset_events in rvgen to avoid unpredictable order
* Add enqueue/dequeue tracepoints (Nam Cao)
* Rename handle_syscall as it collides with some UM function
* Simplify idle handling on nomiss and throttle from sleeping
* Improve switch_out for servers in throttle
* Rely on enqueue/dequeue tracepoints instead of syscalls
* Improve timing conditions in laxity and handle resume action
* Remove fragile Stopping state from boost
[1] - https://lore.kernel.org/lkml/[email protected]
[2] - https://lore.kernel.org/lkml/[email protected]
[3] - https://lore.kernel.org/lkml/[email protected]
To: Steven Rostedt <[email protected]>
To: Nam Cao <[email protected]>
To: Juri Lelli <[email protected]>
Cc: Tomas Glozar <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: John Kacur <[email protected]>
Cc: [email protected]
Gabriele Monaco (15):
rv: Unify DA event handling functions across monitor types
rv: Add Hybrid Automata monitor type
verification/rvgen: Allow spaces in and events strings
verification/rvgen: Add support for Hybrid Automata
Documentation/rv: Add documentation about hybrid automata
rv: Add sample hybrid monitors stall
rv: Convert the opid monitor to a hybrid automaton
rv: Add enqueue/dequeue to snroc monitor
rv: Add support for per-object monitors in DA/HA
verification/rvgen: Add support for per-obj monitors
sched: Add deadline tracepoints
sched/deadline: Move some utility functions to deadline.h
sched_ext: Export task_is_scx_enabled() for verification
rv: Add deadline monitors
rv: Add dl_server specific monitors
Nam Cao (1):
sched: Add task enqueue/dequeue trace points
Documentation/tools/rv/index.rst | 1 +
Documentation/tools/rv/rv-mon-stall.rst | 44 ++
.../trace/rv/deterministic_automata.rst | 2 +-
Documentation/trace/rv/hybrid_automata.rst | 341 ++++++++++
Documentation/trace/rv/index.rst | 3 +
Documentation/trace/rv/monitor_deadline.rst | 278 ++++++++
Documentation/trace/rv/monitor_sched.rst | 101 ++-
Documentation/trace/rv/monitor_stall.rst | 43 ++
Documentation/trace/rv/monitor_synthesis.rst | 117 +++-
include/linux/rv.h | 39 ++
include/linux/sched/deadline.h | 29 +
include/linux/sched/ext.h | 2 +
include/rv/da_monitor.h | 644 +++++++++++++-----
include/rv/ha_monitor.h | 478 +++++++++++++
include/trace/events/sched.h | 34 +
kernel/sched/core.c | 16 +-
kernel/sched/deadline.c | 53 +-
kernel/sched/ext.c | 8 +
kernel/sched/sched.h | 2 +
kernel/trace/rv/Kconfig | 21 +
kernel/trace/rv/Makefile | 6 +
kernel/trace/rv/monitors/boost/Kconfig | 15 +
kernel/trace/rv/monitors/boost/boost.c | 258 +++++++
kernel/trace/rv/monitors/boost/boost.h | 146 ++++
kernel/trace/rv/monitors/boost/boost_trace.h | 19 +
kernel/trace/rv/monitors/deadline/Kconfig | 10 +
kernel/trace/rv/monitors/deadline/deadline.c | 35 +
kernel/trace/rv/monitors/deadline/deadline.h | 206 ++++++
kernel/trace/rv/monitors/laxity/Kconfig | 14 +
kernel/trace/rv/monitors/laxity/laxity.c | 279 ++++++++
kernel/trace/rv/monitors/laxity/laxity.h | 140 ++++
.../trace/rv/monitors/laxity/laxity_trace.h | 19 +
kernel/trace/rv/monitors/nomiss/Kconfig | 15 +
kernel/trace/rv/monitors/nomiss/nomiss.c | 287 ++++++++
kernel/trace/rv/monitors/nomiss/nomiss.h | 123 ++++
.../trace/rv/monitors/nomiss/nomiss_trace.h | 19 +
kernel/trace/rv/monitors/opid/Kconfig | 11 +-
kernel/trace/rv/monitors/opid/opid.c | 111 +--
kernel/trace/rv/monitors/opid/opid.h | 86 +--
kernel/trace/rv/monitors/opid/opid_trace.h | 4 +
kernel/trace/rv/monitors/snroc/snroc.c | 18 +-
kernel/trace/rv/monitors/snroc/snroc.h | 46 +-
kernel/trace/rv/monitors/stall/Kconfig | 13 +
kernel/trace/rv/monitors/stall/stall.c | 150 ++++
kernel/trace/rv/monitors/stall/stall.h | 81 +++
kernel/trace/rv/monitors/stall/stall_trace.h | 19 +
kernel/trace/rv/monitors/throttle/Kconfig | 15 +
kernel/trace/rv/monitors/throttle/throttle.c | 279 ++++++++
kernel/trace/rv/monitors/throttle/throttle.h | 116 ++++
.../rv/monitors/throttle/throttle_trace.h | 19 +
kernel/trace/rv/rv_trace.h | 70 +-
tools/verification/models/deadline/boost.dot | 48 ++
tools/verification/models/deadline/laxity.dot | 37 +
tools/verification/models/deadline/nomiss.dot | 41 ++
.../verification/models/deadline/throttle.dot | 44 ++
tools/verification/models/sched/opid.dot | 36 +-
tools/verification/models/sched/snroc.dot | 30 +-
tools/verification/models/stall.dot | 22 +
tools/verification/rvgen/__main__.py | 8 +-
tools/verification/rvgen/rvgen/automata.py | 151 +++-
tools/verification/rvgen/rvgen/dot2c.py | 47 ++
tools/verification/rvgen/rvgen/dot2k.py | 489 ++++++++++++-
tools/verification/rvgen/rvgen/generator.py | 4 +-
.../rvgen/rvgen/templates/dot2k/main.c | 2 +-
.../rvgen/templates/dot2k/trace_hybrid.h | 16 +
65 files changed, 5379 insertions(+), 481 deletions(-)
create mode 100644 Documentation/tools/rv/rv-mon-stall.rst
create mode 100644 Documentation/trace/rv/hybrid_automata.rst
create mode 100644 Documentation/trace/rv/monitor_deadline.rst
create mode 100644 Documentation/trace/rv/monitor_stall.rst
create mode 100644 include/rv/ha_monitor.h
create mode 100644 kernel/trace/rv/monitors/boost/Kconfig
create mode 100644 kernel/trace/rv/monitors/boost/boost.c
create mode 100644 kernel/trace/rv/monitors/boost/boost.h
create mode 100644 kernel/trace/rv/monitors/boost/boost_trace.h
create mode 100644 kernel/trace/rv/monitors/deadline/Kconfig
create mode 100644 kernel/trace/rv/monitors/deadline/deadline.c
create mode 100644 kernel/trace/rv/monitors/deadline/deadline.h
create mode 100644 kernel/trace/rv/monitors/laxity/Kconfig
create mode 100644 kernel/trace/rv/monitors/laxity/laxity.c
create mode 100644 kernel/trace/rv/monitors/laxity/laxity.h
create mode 100644 kernel/trace/rv/monitors/laxity/laxity_trace.h
create mode 100644 kernel/trace/rv/monitors/nomiss/Kconfig
create mode 100644 kernel/trace/rv/monitors/nomiss/nomiss.c
create mode 100644 kernel/trace/rv/monitors/nomiss/nomiss.h
create mode 100644 kernel/trace/rv/monitors/nomiss/nomiss_trace.h
create mode 100644 kernel/trace/rv/monitors/stall/Kconfig
create mode 100644 kernel/trace/rv/monitors/stall/stall.c
create mode 100644 kernel/trace/rv/monitors/stall/stall.h
create mode 100644 kernel/trace/rv/monitors/stall/stall_trace.h
create mode 100644 kernel/trace/rv/monitors/throttle/Kconfig
create mode 100644 kernel/trace/rv/monitors/throttle/throttle.c
create mode 100644 kernel/trace/rv/monitors/throttle/throttle.h
create mode 100644 kernel/trace/rv/monitors/throttle/throttle_trace.h
create mode 100644 tools/verification/models/deadline/boost.dot
create mode 100644 tools/verification/models/deadline/laxity.dot
create mode 100644 tools/verification/models/deadline/nomiss.dot
create mode 100644 tools/verification/models/deadline/throttle.dot
create mode 100644 tools/verification/models/stall.dot
create mode 100644
tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h
base-commit: 6de23f81a5e08be8fbf5e8d7e9febc72a5b5f27f
--
2.53.0
