[GIT PULL] rv changes for v7.1 (for-next)

[Gabriele Monaco]

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 <rostedt@xxxxxxxxxxx>
Cc: Gabriele Monaco <gmonaco@xxxxxxxxxx>
Cc: Nam Cao <namcao@xxxxxxxxxxxxx>
Cc: Wander Lairson Costa <wander@xxxxxxxxxx>