| # SPDX-License-Identifier: GPL-2.0-only | |
| # | |
| config RV_MON_EVENTS | |
| bool | |
| config RV_MON_MAINTENANCE_EVENTS | |
| bool | |
| config DA_MON_EVENTS_IMPLICIT | |
| select RV_MON_EVENTS | |
| select RV_MON_MAINTENANCE_EVENTS | |
| bool | |
| config DA_MON_EVENTS_ID | |
| select RV_MON_EVENTS | |
| select RV_MON_MAINTENANCE_EVENTS | |
| bool | |
| config LTL_MON_EVENTS_ID | |
| select RV_MON_EVENTS | |
| bool | |
| config RV_LTL_MONITOR | |
| bool | |
| config RV_HA_MONITOR | |
| bool | |
| config HA_MON_EVENTS_IMPLICIT | |
| select DA_MON_EVENTS_IMPLICIT | |
| select RV_HA_MONITOR | |
| bool | |
| config HA_MON_EVENTS_ID | |
| select DA_MON_EVENTS_ID | |
| select RV_HA_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/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/sts/Kconfig" | |
| source "kernel/trace/rv/monitors/nrp/Kconfig" | |
| source "kernel/trace/rv/monitors/sssw/Kconfig" | |
| source "kernel/trace/rv/monitors/opid/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" | |
| source "kernel/trace/rv/monitors/wakeup/Kconfig" | |
| # Add new rtapp monitors here | |
| source "kernel/trace/rv/monitors/stall/Kconfig" | |
| source "kernel/trace/rv/monitors/deadline/Kconfig" | |
| source "kernel/trace/rv/monitors/nomiss/Kconfig" | |
| # Add new deadline 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. | |
| config RV_REACTORS_KUNIT | |
| tristate "KUnit tests for RV reactors" if !KUNIT_ALL_TESTS | |
| depends on KUNIT | |
| depends on RV_REACTORS | |
| default KUNIT_ALL_TESTS | |
| help | |
| Enable KUnit tests for RV reactor registration and dispatch. | |
| These tests verify the register/unregister lifecycle, duplicate | |
| rejection, and that rv_react() correctly invokes callbacks. | |
| If unsure, say N. | |
| config RV_MONITORS_KUNIT_TEST | |
| tristate "KUnit tests for RV monitors" if !KUNIT_ALL_TESTS | |
| depends on KUNIT && RV && RV_REACTORS | |
| default KUNIT_ALL_TESTS | |
| help | |
| Enable KUnit tests for the RV (Runtime Verification) monitors. | |
| These tests verify that monitors correctly detect violations by | |
| triggering fake events and validating the expected reactions. | |
| Enabling this may slightly increase overhead of some monitors if any | |
| unrelated KUnit test is running. | |
| If unsure, say N. |