1# SPDX-License-Identifier: GPL-2.0-only 2# 3config RV_MON_EVENTS 4 bool 5 6config DA_MON_EVENTS_IMPLICIT 7 select RV_MON_EVENTS 8 bool 9 10config DA_MON_EVENTS_ID 11 select RV_MON_EVENTS 12 bool 13 14config LTL_MON_EVENTS_ID 15 select RV_MON_EVENTS 16 bool 17 18config RV_LTL_MONITOR 19 bool 20 21menuconfig RV 22 bool "Runtime Verification" 23 select TRACING 24 help 25 Enable the kernel runtime verification infrastructure. RV is a 26 lightweight (yet rigorous) method that complements classical 27 exhaustive verification techniques (such as model checking and 28 theorem proving). RV works by analyzing the trace of the system's 29 actual execution, comparing it against a formal specification of 30 the system behavior. 31 32 For further information, see: 33 Documentation/trace/rv/runtime-verification.rst 34 35config RV_PER_TASK_MONITORS 36 int "Maximum number of per-task monitor" 37 depends on RV 38 range 1 8 39 default 2 40 help 41 This option configures the maximum number of per-task RV monitors that can run 42 simultaneously. 43 44source "kernel/trace/rv/monitors/wip/Kconfig" 45source "kernel/trace/rv/monitors/wwnr/Kconfig" 46 47source "kernel/trace/rv/monitors/sched/Kconfig" 48source "kernel/trace/rv/monitors/tss/Kconfig" 49source "kernel/trace/rv/monitors/sco/Kconfig" 50source "kernel/trace/rv/monitors/snroc/Kconfig" 51source "kernel/trace/rv/monitors/scpd/Kconfig" 52source "kernel/trace/rv/monitors/snep/Kconfig" 53source "kernel/trace/rv/monitors/sncid/Kconfig" 54# Add new sched monitors here 55 56source "kernel/trace/rv/monitors/rtapp/Kconfig" 57source "kernel/trace/rv/monitors/pagefault/Kconfig" 58source "kernel/trace/rv/monitors/sleep/Kconfig" 59# Add new rtapp monitors here 60 61# Add new monitors here 62 63config RV_REACTORS 64 bool "Runtime verification reactors" 65 default y 66 depends on RV 67 help 68 Enables the online runtime verification reactors. A runtime 69 monitor can cause a reaction to the detection of an exception 70 on the model's execution. By default, the monitors have 71 tracing reactions, printing the monitor output via tracepoints, 72 but other reactions can be added (on-demand) via this interface. 73 74config RV_REACT_PRINTK 75 bool "Printk reactor" 76 depends on RV_REACTORS 77 default y 78 help 79 Enables the printk reactor. The printk reactor emits a printk() 80 message if an exception is found. 81 82config RV_REACT_PANIC 83 bool "Panic reactor" 84 depends on RV_REACTORS 85 default y 86 help 87 Enables the panic reactor. The panic reactor emits a printk() 88 message if an exception is found and panic()s the system. 89