public inbox for linux-kernel@vger.kernel.org
 help / color / mirror / Atom feed
* [PATCH v7 00/15] rv: Add Hybrid Automata monitor type, per-object and deadline monitors
@ 2026-03-10 10:56 Gabriele Monaco
  2026-03-10 10:56 ` [PATCH v7 01/15] rv: Unify DA event handling functions across monitor types Gabriele Monaco
                   ` (14 more replies)
  0 siblings, 15 replies; 25+ messages in thread
From: Gabriele Monaco @ 2026-03-10 10:56 UTC (permalink / raw)
  To: linux-kernel, Steven Rostedt, Nam Cao, Juri Lelli
  Cc: Gabriele Monaco, Tomas Glozar, Clark Williams, John Kacur,
	linux-trace-kernel

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 V6 [1]:
* Drop general task_is_scx_enabled() to use the kallsyms-based version
* Search for task and lock RCU in extract_params() callers
* Use offsetofend when copying sched_attr for better clarity
* Export sched_dl_update to modules and fix style
* Use consistent events in examples in docs
* Use cpu_of(rq) helper in tracepoint calls

Changes since V5 [2]:
* 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 [3]:
* 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 [4]:
* 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/20260225095122.80683-1-gmonaco@redhat.com
[2] - https://lore.kernel.org/lkml/20260122155500.362683-1-gmonaco@redhat.com
[3] - https://lore.kernel.org/lkml/20260116123911.130300-1-gmonaco@redhat.com
[4] - https://lore.kernel.org/lkml/20251205131621.135513-1-gmonaco@redhat.com

To: Steven Rostedt <rostedt@goodmis.org>
To: Nam Cao <namcao@linutronix.de>
To: Juri Lelli <jlelli@redhat.com>
Cc: Tomas Glozar <tglozar@redhat.com>
Cc: Clark Williams <williams@redhat.com>
Cc: John Kacur <jkacur@redhat.com>
Cc: linux-trace-kernel@vger.kernel.org

Gabriele Monaco (14):
  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
  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                |  27 +
 include/rv/da_monitor.h                       | 644 +++++++++++++-----
 include/rv/ha_monitor.h                       | 478 +++++++++++++
 include/trace/events/sched.h                  |  34 +
 kernel/sched/core.c                           |  17 +-
 kernel/sched/deadline.c                       |  52 +-
 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  |  41 ++
 kernel/trace/rv/monitors/deadline/deadline.h  | 202 ++++++
 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      | 293 ++++++++
 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  | 285 ++++++++
 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 +
 63 files changed, 5382 insertions(+), 480 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: 1f318b96cc84d7c2ab792fcc0bfd42a7ca890681
-- 
2.53.0


^ permalink raw reply	[flat|nested] 25+ messages in thread

end of thread, other threads:[~2026-03-23  9:06 UTC | newest]

Thread overview: 25+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2026-03-10 10:56 [PATCH v7 00/15] rv: Add Hybrid Automata monitor type, per-object and deadline monitors Gabriele Monaco
2026-03-10 10:56 ` [PATCH v7 01/15] rv: Unify DA event handling functions across monitor types Gabriele Monaco
2026-03-10 10:56 ` [PATCH v7 02/15] rv: Add Hybrid Automata monitor type Gabriele Monaco
2026-03-10 10:56 ` [PATCH v7 03/15] verification/rvgen: Allow spaces in and events strings Gabriele Monaco
2026-03-10 10:56 ` [PATCH v7 04/15] verification/rvgen: Add support for Hybrid Automata Gabriele Monaco
2026-03-10 10:56 ` [PATCH v7 05/15] Documentation/rv: Add documentation about hybrid automata Gabriele Monaco
2026-03-12 10:39   ` Juri Lelli
2026-03-13 13:05     ` gmonaco
2026-03-13 13:23       ` Juri Lelli
2026-03-10 10:56 ` [PATCH v7 06/15] rv: Add sample hybrid monitors stall Gabriele Monaco
2026-03-10 10:56 ` [PATCH v7 07/15] rv: Convert the opid monitor to a hybrid automaton Gabriele Monaco
2026-03-10 10:56 ` [PATCH v7 08/15] sched: Add task enqueue/dequeue trace points Gabriele Monaco
2026-03-18 15:44   ` gmonaco
2026-03-10 10:56 ` [PATCH v7 09/15] rv: Add enqueue/dequeue to snroc monitor Gabriele Monaco
2026-03-23  9:06   ` Nam Cao
2026-03-10 10:56 ` [PATCH v7 10/15] rv: Add support for per-object monitors in DA/HA Gabriele Monaco
2026-03-10 10:56 ` [PATCH v7 11/15] verification/rvgen: Add support for per-obj monitors Gabriele Monaco
2026-03-10 10:56 ` [PATCH v7 12/15] sched: Add deadline tracepoints Gabriele Monaco
2026-03-12 13:07   ` Juri Lelli
2026-03-10 10:56 ` [PATCH v7 13/15] sched/deadline: Move some utility functions to deadline.h Gabriele Monaco
2026-03-10 10:56 ` [PATCH v7 14/15] rv: Add deadline monitors Gabriele Monaco
2026-03-12 13:37   ` Juri Lelli
2026-03-18 12:00     ` gmonaco
2026-03-10 10:56 ` [PATCH v7 15/15] rv: Add dl_server specific monitors Gabriele Monaco
2026-03-12 13:55   ` Juri Lelli

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox