0001 # SPDX-License-Identifier: GPL-2.0-only
0002 #
0003 config DA_MON_EVENTS
0004 bool
0005
0006 config DA_MON_EVENTS_IMPLICIT
0007 select DA_MON_EVENTS
0008 bool
0009
0010 config DA_MON_EVENTS_ID
0011 select DA_MON_EVENTS
0012 bool
0013
0014 menuconfig RV
0015 bool "Runtime Verification"
0016 depends on TRACING
0017 help
0018 Enable the kernel runtime verification infrastructure. RV is a
0019 lightweight (yet rigorous) method that complements classical
0020 exhaustive verification techniques (such as model checking and
0021 theorem proving). RV works by analyzing the trace of the system's
0022 actual execution, comparing it against a formal specification of
0023 the system behavior.
0024
0025 For further information, see:
0026 Documentation/trace/rv/runtime-verification.rst
0027
0028 config RV_MON_WIP
0029 depends on RV
0030 depends on PREEMPT_TRACER
0031 select DA_MON_EVENTS_IMPLICIT
0032 bool "wip monitor"
0033 help
0034 Enable wip (wakeup in preemptive) sample monitor that illustrates
0035 the usage of per-cpu monitors, and one limitation of the
0036 preempt_disable/enable events.
0037
0038 For further information, see:
0039 Documentation/trace/rv/monitor_wip.rst
0040
0041 config RV_MON_WWNR
0042 depends on RV
0043 select DA_MON_EVENTS_ID
0044 bool "wwnr monitor"
0045 help
0046 Enable wwnr (wakeup while not running) sample monitor, this is a
0047 sample monitor that illustrates the usage of per-task monitor.
0048 The model is borken on purpose: it serves to test reactors.
0049
0050 For further information, see:
0051 Documentation/trace/rv/monitor_wwnr.rst
0052
0053 config RV_REACTORS
0054 bool "Runtime verification reactors"
0055 default y
0056 depends on RV
0057 help
0058 Enables the online runtime verification reactors. A runtime
0059 monitor can cause a reaction to the detection of an exception
0060 on the model's execution. By default, the monitors have
0061 tracing reactions, printing the monitor output via tracepoints,
0062 but other reactions can be added (on-demand) via this interface.
0063
0064 config RV_REACT_PRINTK
0065 bool "Printk reactor"
0066 depends on RV_REACTORS
0067 default y
0068 help
0069 Enables the printk reactor. The printk reactor emits a printk()
0070 message if an exception is found.
0071
0072 config RV_REACT_PANIC
0073 bool "Panic reactor"
0074 depends on RV_REACTORS
0075 default y
0076 help
0077 Enables the panic reactor. The panic reactor emits a printk()
0078 message if an exception is found and panic()s the system.
