From: Steven Rostedt <rostedt@goodmis.org>
To: Linus Torvalds <torvalds@linux-foundation.org>
Cc: LKML <linux-kernel@vger.kernel.org>,
"Gabriele Monaco" <gmonaco@redhat.com>,
"Nam Cao" <namcao@linutronix.de>,
"Wander Lairson Costa" <wander@redhat.com>,
"Thomas Weißschuh" <thomas.weissschuh@linutronix.de>
Subject: [GIT PULL] rv: Updates for v7.1
Date: Tue, 14 Apr 2026 07:32:12 -0400 [thread overview]
Message-ID: <20260414073212.1b7174dd@robin> (raw)
Linus,
Runtime Verification updates for 7.1:
- Refactor da_monitor header to share handlers across monitor types
No functional changes, only less code duplication.
- Add Hybrid Automata model class
Add a new model class that extends deterministic automata by adding
constraints on transitions and states. Those constraints can take into
account wall-clock time and as such allow RV monitor to make
assertions on real time. Add documentation and code generation
scripts.
- Add stall monitor as hybrid automaton example
Add a monitor that triggers a violation when a task is stalling as an
example of automaton working with real time variables.
- Convert the opid monitor to a hybrid automaton
The opid monitor can be heavily simplified if written as a hybrid
automaton: instead of tracking preempt and interrupt enable/disable
events, it can just run constraints on the preemption/interrupt
states when events like wakeup and need_resched verify.
- Add support for per-object monitors in DA/HA
Allow writing deterministic and hybrid automata monitors for generic
objects (e.g. any struct), by exploiting a hash table where objects
are saved. This allows to track more than just tasks in RV. For
instance it will be used to track deadline entities in deadline
monitors.
- Add deadline tracepoints and move some deadline utilities
Prepare the ground for deadline monitors by defining events and
exporting helpers.
- Add nomiss deadline monitor
Add first example of deadline monitor asserting all entities complete
before their deadline.
- Improve rvgen error handling
Introduce AutomataError exception class and better handle expected
exceptions while showing a backtrace for unexpected ones.
- Improve python code quality in rvgen
Refactor the rvgen generation scripts to align with python best
practices: use f-strings instead of %, use len() instead of __len__(),
remove semicolons, use context managers for file operations, fix
whitespace violations, extract magic strings into constants, remove
unused imports and methods.
- Fix small bugs in rvgen
The generator scripts presented some corner case bugs: logical error in
validating what a correct dot file looks like, fix an isinstance()
check, enforce a dot file has an initial state, fix type annotations
and typos in comments.
- rvgen refactoring
Refactor automata.py to use iterator-based parsing and handle required
arguments directly in argparse.
- Allow epoll in rtapp-sleep monitor
The epoll_wait call is now rt-friendly so it should be allowed in the
sleep monitor as a valid sleep method.
Please pull the latest trace-rv-v7.1 tree, which can be found at:
git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace.git
trace-rv-v7.1
Tag SHA1: a6d8b3e4af26a6d177bbd9cab0e2e0228441209c
Head SHA1: 00f0dadde8c5036fe6462621a6920549036dce70
Gabriele Monaco (12):
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 monitor stall
rv: Convert the opid monitor to a hybrid automaton
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 nomiss deadline monitor
Nam Cao (1):
rv: Allow epoll in rtapp-sleep monitor
Wander Lairson Costa (19):
rv/rvgen: introduce AutomataError exception class
rv/rvgen: remove bare except clauses in generator
rv/rvgen: replace % string formatting with f-strings
rv/rvgen: replace __len__() calls with len()
rv/rvgen: remove unnecessary semicolons
rv/rvgen: use context managers for file operations
rv/rvgen: fix typos in automata and generator docstring and comments
rv/rvgen: fix PEP 8 whitespace violations
rv/rvgen: fix DOT file validation logic error
rv/rvgen: use class constant for init marker
rv/rvgen: refactor automata.py to use iterator-based parsing
rv/rvgen: remove unused sys import from dot2c
rv/rvgen: remove unused __get_main_name method
rv/rvgen: make monitor arguments required in rvgen
rv/rvgen: fix isinstance check in Variable.expand()
rv/rvgen: extract node marker string to class constant
rv/rvgen: enforce presence of initial state
rv/rvgen: fix unbound loop variable warning
rv/rvgen: fix _fill_states() return type annotation
----
Documentation/tools/rv/index.rst | 1 +
Documentation/tools/rv/rv-mon-stall.rst | 44 ++
Documentation/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 | 84 +++
Documentation/trace/rv/monitor_sched.rst | 62 +-
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 | 26 +
kernel/sched/core.c | 5 +
kernel/sched/deadline.c | 51 +-
kernel/trace/rv/Kconfig | 18 +
kernel/trace/rv/Makefile | 3 +
kernel/trace/rv/monitors/deadline/Kconfig | 10 +
kernel/trace/rv/monitors/deadline/deadline.c | 44 ++
kernel/trace/rv/monitors/deadline/deadline.h | 202 +++++++
kernel/trace/rv/monitors/nomiss/Kconfig | 15 +
kernel/trace/rv/monitors/nomiss/nomiss.c | 293 ++++++++++
kernel/trace/rv/monitors/nomiss/nomiss.h | 123 ++++
kernel/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/sleep/sleep.c | 8 +
kernel/trace/rv/monitors/sleep/sleep.h | 98 ++--
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/rv_trace.h | 67 ++-
tools/verification/models/deadline/nomiss.dot | 41 ++
tools/verification/models/rtapp/sleep.ltl | 1 +
tools/verification/models/sched/opid.dot | 36 +-
tools/verification/models/stall.dot | 22 +
tools/verification/rvgen/__main__.py | 27 +-
tools/verification/rvgen/dot2c | 1 -
tools/verification/rvgen/rvgen/automata.py | 294 +++++++---
tools/verification/rvgen/rvgen/dot2c.py | 105 +++-
tools/verification/rvgen/rvgen/dot2k.py | 524 ++++++++++++++++-
tools/verification/rvgen/rvgen/generator.py | 93 ++-
tools/verification/rvgen/rvgen/ltl2ba.py | 11 +-
tools/verification/rvgen/rvgen/ltl2k.py | 54 +-
.../rvgen/rvgen/templates/dot2k/main.c | 2 +-
.../rvgen/rvgen/templates/dot2k/trace_hybrid.h | 16 +
50 files changed, 3883 insertions(+), 686 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/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/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 tools/verification/models/deadline/nomiss.dot
create mode 100644 tools/verification/models/stall.dot
create mode 100644 tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h
---------------------------
next reply other threads:[~2026-04-14 11:32 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2026-04-14 11:32 Steven Rostedt [this message]
2026-04-16 0:51 ` [GIT PULL] rv: Updates for v7.1 pr-tracker-bot
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=20260414073212.1b7174dd@robin \
--to=rostedt@goodmis.org \
--cc=gmonaco@redhat.com \
--cc=linux-kernel@vger.kernel.org \
--cc=namcao@linutronix.de \
--cc=thomas.weissschuh@linutronix.de \
--cc=torvalds@linux-foundation.org \
--cc=wander@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