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 task enqueue/dequeue trace points rv: Add rts monitor Documentation/trace/rv/monitor_rtapp.rst | 19 +++ include/linux/rv.h | 4 + include/rv/ltl_monitor.h | 115 +++++++++----- include/trace/events/sched.h | 13 ++ kernel/sched/core.c | 8 +- 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 | 144 ++++++++++++++++++ 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/rtapp/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, 538 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/rtapp/rts.ltl -- 2.39.5