1# SPDX-License-Identifier: GPL-2.0-only 2# 3config DA_MON_EVENTS 4 bool 5 6config DA_MON_EVENTS_IMPLICIT 7 select DA_MON_EVENTS 8 bool 9 10config DA_MON_EVENTS_ID 11 select DA_MON_EVENTS 12 bool 13 14menuconfig RV 15 bool "Runtime Verification" 16 depends on TRACING 17 help 18 Enable the kernel runtime verification infrastructure. RV is a 19 lightweight (yet rigorous) method that complements classical 20 exhaustive verification techniques (such as model checking and 21 theorem proving). RV works by analyzing the trace of the system's 22 actual execution, comparing it against a formal specification of 23 the system behavior. 24 25 For further information, see: 26 Documentation/trace/rv/runtime-verification.rst 27 28config RV_MON_WIP 29 depends on RV 30 depends on PREEMPT_TRACER 31 select DA_MON_EVENTS_IMPLICIT 32 bool "wip monitor" 33 help 34 Enable wip (wakeup in preemptive) sample monitor that illustrates 35 the usage of per-cpu monitors, and one limitation of the 36 preempt_disable/enable events. 37 38 For further information, see: 39 Documentation/trace/rv/monitor_wip.rst 40 41config RV_MON_WWNR 42 depends on RV 43 select DA_MON_EVENTS_ID 44 bool "wwnr monitor" 45 help 46 Enable wwnr (wakeup while not running) sample monitor, this is a 47 sample monitor that illustrates the usage of per-task monitor. 48 The model is borken on purpose: it serves to test reactors. 49 50 For further information, see: 51 Documentation/trace/rv/monitor_wwnr.rst 52 53config RV_REACTORS 54 bool "Runtime verification reactors" 55 default y 56 depends on RV 57 help 58 Enables the online runtime verification reactors. A runtime 59 monitor can cause a reaction to the detection of an exception 60 on the model's execution. By default, the monitors have 61 tracing reactions, printing the monitor output via tracepoints, 62 but other reactions can be added (on-demand) via this interface. 63 64config RV_REACT_PRINTK 65 bool "Printk reactor" 66 depends on RV_REACTORS 67 default y 68 help 69 Enables the printk reactor. The printk reactor emits a printk() 70 message if an exception is found. 71 72config RV_REACT_PANIC 73 bool "Panic reactor" 74 depends on RV_REACTORS 75 default y 76 help 77 Enables the panic reactor. The panic reactor emits a printk() 78 message if an exception is found and panic()s the system. 79