From: Gabriele Monaco <gmonaco@redhat.com>
To: linux-kernel@vger.kernel.org,
Steven Rostedt <rostedt@goodmis.org>,
Nam Cao <namcao@linutronix.de>, Juri Lelli <jlelli@redhat.com>
Cc: Gabriele Monaco <gmonaco@redhat.com>,
Tomas Glozar <tglozar@redhat.com>,
Clark Williams <williams@redhat.com>,
John Kacur <jkacur@redhat.com>,
linux-trace-kernel@vger.kernel.org
Subject: [PATCH v5 00/15] rv: Add Hybrid Automata monitor type, per-object and deadline monitors
Date: Thu, 22 Jan 2026 16:54:45 +0100 [thread overview]
Message-ID: <20260122155500.362683-1-gmonaco@redhat.com> (raw)
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.
This series is based on the previously sent [1] that includes
preliminary patches present in V2 [2] and already reviewed. As such this
series is simplified and includes only relevant new changes.
These models were found stable during testing if 63be0c9e5489
("sched/deadline: Fix server stopping with runnable tasks") is applied.
The entire series can also be found on:
git.kernel.org/pub/scm/linux/kernel/git/gmonaco/linux.git rv_hybrid_automata
Changes since V4:
* 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:
* 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
Changes since V2 [2]:
* Adapt models to new dl server behaviour
* Rearrange start/handle helpers to share more code
* Improve documentation clarity after review
* Extend stall model to handle preemption
* Improve functions naming for HA helpers
* Use kmalloc_nolock for per-obj storage allocation
* Add boost and laxity monitors for deadline servers
* Add _is_id_monitor() in dot2k to handle per-obj together with per-task
* Rename dl argument to dl_se in tracepoints
* Use __COUNTER__ in dl monitor syscall helpers
* Fix conflicts after rebase (cond_react -> rv_react)
* General cleanup
Changes since V1 [3]:
* Cleanup unused trace events definitions
* Improve hybrid automata description about use of timers
* Unify event handler internals across DA monitor types
* Implement timer wheel alternative for invariants
* Extend models to consider timing of task switches (in before deadline,
out after throttle)
* Refactor tracepoints and per-object monitors to allow server events
from remote CPUs
* Changed clock representation in case of invariants (time to expire vs
time since reset) and allow conversion without reset
* Extend dot2k to understand the graph relations and suggest where
invariant conversions are needed
* General cleanup of rvgen scripts
[1] - https://lore.kernel.org/lkml/20251126104241.291258-1-gmonaco@redhat.com
[2] - https://lore.kernel.org/lkml/20250919140954.104920-1-gmonaco@redhat.com
[3] - https://lore.kernel.org/lkml/20250814150809.140739-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
sched: Add deadline tracepoints
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/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 | 270 ++++++++
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/rv/da_monitor.h | 654 +++++++++++++-----
include/rv/ha_monitor.h | 478 +++++++++++++
include/trace/events/sched.h | 29 +
kernel/sched/core.c | 14 +-
kernel/sched/deadline.c | 35 +-
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 | 232 +++++++
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 | 168 +++++
kernel/trace/rv/monitors/laxity/Kconfig | 14 +
kernel/trace/rv/monitors/laxity/laxity.c | 248 +++++++
kernel/trace/rv/monitors/laxity/laxity.h | 133 ++++
.../trace/rv/monitors/laxity/laxity_trace.h | 19 +
kernel/trace/rv/monitors/nomiss/Kconfig | 15 +
kernel/trace/rv/monitors/nomiss/nomiss.c | 279 ++++++++
kernel/trace/rv/monitors/nomiss/nomiss.h | 130 ++++
.../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 | 250 +++++++
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 | 49 ++
tools/verification/rvgen/rvgen/dot2k.py | 488 ++++++++++++-
tools/verification/rvgen/rvgen/generator.py | 4 +-
.../rvgen/rvgen/templates/dot2k/main.c | 2 +-
.../rvgen/templates/dot2k/trace_hybrid.h | 16 +
63 files changed, 5211 insertions(+), 485 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: 924400c1c29006d835408ea0962446d4a481e774
--
2.52.0
next reply other threads:[~2026-01-22 15:55 UTC|newest]
Thread overview: 21+ messages / expand[flat|nested] mbox.gz Atom feed top
2026-01-22 15:54 Gabriele Monaco [this message]
2026-01-22 15:54 ` [PATCH v5 01/15] rv: Unify DA event handling functions across monitor types Gabriele Monaco
2026-01-22 15:54 ` [PATCH v5 02/15] rv: Add Hybrid Automata monitor type Gabriele Monaco
2026-01-22 15:54 ` [PATCH v5 03/15] verification/rvgen: Allow spaces in and events strings Gabriele Monaco
2026-01-22 15:54 ` [PATCH v5 04/15] verification/rvgen: Add support for Hybrid Automata Gabriele Monaco
2026-01-22 15:54 ` [PATCH v5 05/15] Documentation/rv: Add documentation about hybrid automata Gabriele Monaco
2026-01-22 15:54 ` [PATCH v5 06/15] rv: Add sample hybrid monitors stall Gabriele Monaco
2026-01-22 15:54 ` [PATCH v5 07/15] rv: Convert the opid monitor to a hybrid automaton Gabriele Monaco
2026-01-22 15:54 ` [PATCH v5 08/15] sched: Add deadline tracepoints Gabriele Monaco
2026-01-22 15:54 ` [PATCH v5 09/15] sched: Add task enqueue/dequeue trace points Gabriele Monaco
2026-01-27 9:10 ` Gabriele Monaco
2026-02-03 11:06 ` Gabriele Monaco
2026-01-22 15:54 ` [PATCH v5 10/15] rv: Add enqueue/dequeue to snroc monitor Gabriele Monaco
2026-01-22 15:54 ` [PATCH v5 11/15] rv: Add support for per-object monitors in DA/HA Gabriele Monaco
2026-01-22 15:54 ` [PATCH v5 12/15] verification/rvgen: Add support for per-obj monitors Gabriele Monaco
2026-01-22 15:54 ` [PATCH v5 13/15] sched/deadline: Move some utility functions to deadline.h Gabriele Monaco
2026-01-23 13:00 ` Juri Lelli
2026-01-22 15:54 ` [PATCH v5 14/15] rv: Add deadline monitors Gabriele Monaco
2026-01-23 13:03 ` Juri Lelli
2026-01-22 15:55 ` [PATCH v5 15/15] rv: Add dl_server specific monitors Gabriele Monaco
2026-01-23 13:04 ` Juri Lelli
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20260122155500.362683-1-gmonaco@redhat.com \
--to=gmonaco@redhat.com \
--cc=jkacur@redhat.com \
--cc=jlelli@redhat.com \
--cc=linux-kernel@vger.kernel.org \
--cc=linux-trace-kernel@vger.kernel.org \
--cc=namcao@linutronix.de \
--cc=rostedt@goodmis.org \
--cc=tglozar@redhat.com \
--cc=williams@redhat.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox