| # SPDX-License-Identifier: GPL-2.0-only | |
| # | |
| config DA_MON_EVENTS | |
| bool | |
| config DA_MON_EVENTS_IMPLICIT | |
| select DA_MON_EVENTS | |
| bool | |
| config DA_MON_EVENTS_ID | |
| select DA_MON_EVENTS | |
| bool | |
| menuconfig RV | |
| bool "Runtime Verification" | |
| depends on 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_MON_WIP | |
| depends on RV | |
| depends on PREEMPT_TRACER | |
| select DA_MON_EVENTS_IMPLICIT | |
| bool "wip monitor" | |
| help | |
| Enable wip (wakeup in preemptive) sample monitor that illustrates | |
| the usage of per-cpu monitors, and one limitation of the | |
| preempt_disable/enable events. | |
| For further information, see: | |
| Documentation/trace/rv/monitor_wip.rst | |
| config RV_MON_WWNR | |
| depends on RV | |
| select DA_MON_EVENTS_ID | |
| bool "wwnr monitor" | |
| help | |
| Enable wwnr (wakeup while not running) sample monitor, this is a | |
| sample monitor that illustrates the usage of per-task monitor. | |
| The model is borken on purpose: it serves to test reactors. | |
| For further information, see: | |
| Documentation/trace/rv/monitor_wwnr.rst | |
| 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. |