Hi Steve, gentle ping: could you have a look at this pull request?
Thanks, Gabriele On Wed, 2026-04-01 at 17:17 +0200, Gabriele Monaco wrote: > Steve, > > The following changes since commit 7aaa8047eafd0bd628065b15757d9b48c5f9c07d: > > Linux 7.0-rc6 (2026-03-29 15:40:00 -0700) > > are available in the Git repository at: > > git://git.kernel.org/pub/scm/linux/kernel/git/gmonaco/linux.git rv-7.1-next > > for you to fetch changes up to 00f0dadde8c5036fe6462621a6920549036dce70: > > rv: Allow epoll in rtapp-sleep monitor (2026-04-01 15:18:30 +0200) > > ---------------------------------------------------------------- > rv changes for v7.1 (for-next) > > Summary of changes: > > - 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. > > ---------------------------------------------------------------- > 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 > > To: Steven Rostedt <[email protected]> > Cc: Gabriele Monaco <[email protected]> > Cc: Nam Cao <[email protected]> > Cc: Wander Lairson Costa <[email protected]>
