Hi, This series adds support for linear temporal logic per-cpu monitor type, analogous to deterministic automaton per-cpu monitor. Then a new per-cpu monitor is added which validates real-time scheduling.
Nam Cao (5): rv/ltl: Prepare for other monitor types rv/ltl: Support per-cpu monitors verification/rvgen/ltl: Support per-cpu monitor generation sched: Add rt task enqueue/dequeue trace points rv: Add rts monitor Documentation/trace/rv/monitor_sched.rst | 19 +++ include/linux/rv.h | 2 + include/rv/ltl_monitor.h | 117 +++++++++++----- include/trace/events/sched.h | 8 ++ kernel/sched/rt.c | 4 + kernel/trace/rv/Kconfig | 5 + kernel/trace/rv/Makefile | 1 + .../trace/rv/monitors/pagefault/pagefault.h | 2 + kernel/trace/rv/monitors/rts/Kconfig | 17 +++ kernel/trace/rv/monitors/rts/rts.c | 131 ++++++++++++++++++ kernel/trace/rv/monitors/rts/rts.h | 126 +++++++++++++++++ kernel/trace/rv/monitors/rts/rts_trace.h | 15 ++ kernel/trace/rv/monitors/sleep/sleep.h | 2 + kernel/trace/rv/rv_trace.h | 47 +++++++ tools/verification/models/sched/rts.ltl | 5 + tools/verification/rvgen/rvgen/ltl2k.py | 48 ++++++- .../rvgen/rvgen/templates/ltl2k/main.c | 9 +- .../rvgen/rvgen/templates/ltl2k/trace.h | 7 +- 18 files changed, 516 insertions(+), 49 deletions(-) create mode 100644 kernel/trace/rv/monitors/rts/Kconfig create mode 100644 kernel/trace/rv/monitors/rts/rts.c create mode 100644 kernel/trace/rv/monitors/rts/rts.h create mode 100644 kernel/trace/rv/monitors/rts/rts_trace.h create mode 100644 tools/verification/models/sched/rts.ltl -- 2.39.5
