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