]> git.ipfire.org Git - thirdparty/kernel/stable.git/commit
rv: Add support for LTL monitors
authorNam Cao <namcao@linutronix.de>
Wed, 9 Jul 2025 19:21:17 +0000 (21:21 +0200)
committerSteven Rostedt (Google) <rostedt@goodmis.org>
Wed, 9 Jul 2025 19:27:01 +0000 (15:27 -0400)
commita9769a5b987838f03f3dd57b097794cd4c691098
tree0708cc71905bfb9143214666b7b84c8bd71665ae
parentc94d27c01b1ff2e26ca347524b3527534e285a39
rv: Add support for LTL monitors

While attempting to implement DA monitors for some complex specifications,
deterministic automaton is found to be inappropriate as the specification
language. The automaton is complicated, hard to understand, and
error-prone.

For these cases, linear temporal logic is more suitable as the
specification language.

Add support for linear temporal logic runtime verification monitor.

Cc: John Ogness <john.ogness@linutronix.de>
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Cc: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/d366c1fed60ed4e8f6451f3c15a99755f2740b5f.1752088709.git.namcao@linutronix.de
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
include/linux/rv.h
include/rv/ltl_monitor.h [new file with mode: 0644]
kernel/fork.c
kernel/trace/rv/Kconfig
kernel/trace/rv/rv_trace.h