mirror of
https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
synced 2026-07-22 02:17:36 -04:00
560473f2e2
The current behaviour of rvgen when running with the -a option is to append the necessary lines at the end of the configuration for Kconfig, Makefile and tracepoints. This is not always the desired behaviour in case of nested monitors: while tracepoints are not affected by nesting and the Makefile's only requirement is that the parent monitor is built before its children, in the Kconfig it is better to have children defined right after their parent, otherwise the result has wrong indentation: [*] foo_parent monitor [*] foo_child1 monitor [*] foo_child2 monitor [*] bar_parent monitor [*] bar_child1 monitor [*] bar_child2 monitor [*] foo_child3 monitor [*] foo_child4 monitor Adapt rvgen to look for a different marker for nested monitors in the Kconfig file and append the line right after the last sibling, instead of the last monitor. Also add the marker when creating a new parent monitor. Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Tomas Glozar <tglozar@redhat.com> Cc: Juri Lelli <jlelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: John Kacur <jkacur@redhat.com> Link: https://lore.kernel.org/20250723161240.194860-5-gmonaco@redhat.com Reviewed-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
89 lines
2.4 KiB
Plaintext
89 lines
2.4 KiB
Plaintext
# SPDX-License-Identifier: GPL-2.0-only
|
|
#
|
|
config RV_MON_EVENTS
|
|
bool
|
|
|
|
config DA_MON_EVENTS_IMPLICIT
|
|
select RV_MON_EVENTS
|
|
bool
|
|
|
|
config DA_MON_EVENTS_ID
|
|
select RV_MON_EVENTS
|
|
bool
|
|
|
|
config LTL_MON_EVENTS_ID
|
|
select RV_MON_EVENTS
|
|
bool
|
|
|
|
config RV_LTL_MONITOR
|
|
bool
|
|
|
|
menuconfig RV
|
|
bool "Runtime Verification"
|
|
select TRACING
|
|
help
|
|
Enable the kernel runtime verification infrastructure. RV is a
|
|
lightweight (yet rigorous) method that complements classical
|
|
exhaustive verification techniques (such as model checking and
|
|
theorem proving). RV works by analyzing the trace of the system's
|
|
actual execution, comparing it against a formal specification of
|
|
the system behavior.
|
|
|
|
For further information, see:
|
|
Documentation/trace/rv/runtime-verification.rst
|
|
|
|
config RV_PER_TASK_MONITORS
|
|
int "Maximum number of per-task monitor"
|
|
depends on RV
|
|
range 1 8
|
|
default 2
|
|
help
|
|
This option configures the maximum number of per-task RV monitors that can run
|
|
simultaneously.
|
|
|
|
source "kernel/trace/rv/monitors/wip/Kconfig"
|
|
source "kernel/trace/rv/monitors/wwnr/Kconfig"
|
|
|
|
source "kernel/trace/rv/monitors/sched/Kconfig"
|
|
source "kernel/trace/rv/monitors/tss/Kconfig"
|
|
source "kernel/trace/rv/monitors/sco/Kconfig"
|
|
source "kernel/trace/rv/monitors/snroc/Kconfig"
|
|
source "kernel/trace/rv/monitors/scpd/Kconfig"
|
|
source "kernel/trace/rv/monitors/snep/Kconfig"
|
|
source "kernel/trace/rv/monitors/sncid/Kconfig"
|
|
# Add new sched monitors here
|
|
|
|
source "kernel/trace/rv/monitors/rtapp/Kconfig"
|
|
source "kernel/trace/rv/monitors/pagefault/Kconfig"
|
|
source "kernel/trace/rv/monitors/sleep/Kconfig"
|
|
# Add new rtapp monitors here
|
|
|
|
# Add new monitors here
|
|
|
|
config RV_REACTORS
|
|
bool "Runtime verification reactors"
|
|
default y
|
|
depends on RV
|
|
help
|
|
Enables the online runtime verification reactors. A runtime
|
|
monitor can cause a reaction to the detection of an exception
|
|
on the model's execution. By default, the monitors have
|
|
tracing reactions, printing the monitor output via tracepoints,
|
|
but other reactions can be added (on-demand) via this interface.
|
|
|
|
config RV_REACT_PRINTK
|
|
bool "Printk reactor"
|
|
depends on RV_REACTORS
|
|
default y
|
|
help
|
|
Enables the printk reactor. The printk reactor emits a printk()
|
|
message if an exception is found.
|
|
|
|
config RV_REACT_PANIC
|
|
bool "Panic reactor"
|
|
depends on RV_REACTORS
|
|
default y
|
|
help
|
|
Enables the panic reactor. The panic reactor emits a printk()
|
|
message if an exception is found and panic()s the system.
|