[<prev] [next>] [thread-next>] [day] [month] [year] [list]
Message-Id: <cover.1753879295.git.namcao@linutronix.de>
Date: Wed, 30 Jul 2025 14:45:38 +0200
From: Nam Cao <namcao@...utronix.de>
To: Steven Rostedt <rostedt@...dmis.org>,
Masami Hiramatsu <mhiramat@...nel.org>,
Mathieu Desnoyers <mathieu.desnoyers@...icios.com>,
Gabriele Monaco <gmonaco@...hat.com>,
linux-trace-kernel@...r.kernel.org,
linux-kernel@...r.kernel.org
Cc: Nam Cao <namcao@...utronix.de>
Subject: [PATCH 0/5] rv: LTL per-cpu monitor type and real-time scheduling monitor
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
Powered by blists - more mailing lists