1102227b9SDaniel Bristot de Oliveira# SPDX-License-Identifier: GPL-2.0-only 2102227b9SDaniel Bristot de Oliveira# 379257534SDaniel Bristot de Oliveiraconfig DA_MON_EVENTS 479257534SDaniel Bristot de Oliveira bool 579257534SDaniel Bristot de Oliveira 679257534SDaniel Bristot de Oliveiraconfig DA_MON_EVENTS_IMPLICIT 779257534SDaniel Bristot de Oliveira select DA_MON_EVENTS 879257534SDaniel Bristot de Oliveira bool 979257534SDaniel Bristot de Oliveira 1079257534SDaniel Bristot de Oliveiraconfig DA_MON_EVENTS_ID 1179257534SDaniel Bristot de Oliveira select DA_MON_EVENTS 1279257534SDaniel Bristot de Oliveira bool 1379257534SDaniel Bristot de Oliveira 14102227b9SDaniel Bristot de Oliveiramenuconfig RV 15102227b9SDaniel Bristot de Oliveira bool "Runtime Verification" 16102227b9SDaniel Bristot de Oliveira depends on TRACING 17102227b9SDaniel Bristot de Oliveira help 18102227b9SDaniel Bristot de Oliveira Enable the kernel runtime verification infrastructure. RV is a 19102227b9SDaniel Bristot de Oliveira lightweight (yet rigorous) method that complements classical 20102227b9SDaniel Bristot de Oliveira exhaustive verification techniques (such as model checking and 21102227b9SDaniel Bristot de Oliveira theorem proving). RV works by analyzing the trace of the system's 22102227b9SDaniel Bristot de Oliveira actual execution, comparing it against a formal specification of 23102227b9SDaniel Bristot de Oliveira the system behavior. 2404acadcbSDaniel Bristot de Oliveira 25ff0aaf67SDaniel Bristot de Oliveira For further information, see: 26ff0aaf67SDaniel Bristot de Oliveira Documentation/trace/rv/runtime-verification.rst 27ff0aaf67SDaniel Bristot de Oliveira 28bc3d482dSGabriele Monacosource "kernel/trace/rv/monitors/wip/Kconfig" 29bc3d482dSGabriele Monacosource "kernel/trace/rv/monitors/wwnr/Kconfig" 30cb85c660SGabriele Monacosource "kernel/trace/rv/monitors/sched/Kconfig" 319fd420abSGabriele Monacosource "kernel/trace/rv/monitors/tss/Kconfig" 329fd420abSGabriele Monacosource "kernel/trace/rv/monitors/sco/Kconfig" 3393bac9cfSGabriele Monacosource "kernel/trace/rv/monitors/snroc/Kconfig" 34*fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/scpd/Kconfig" 35*fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/snep/Kconfig" 36*fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/sncid/Kconfig" 37de6f45c2SGabriele Monaco# Add new monitors here 38ccc319dcSDaniel Bristot de Oliveira 3904acadcbSDaniel Bristot de Oliveiraconfig RV_REACTORS 4004acadcbSDaniel Bristot de Oliveira bool "Runtime verification reactors" 4104acadcbSDaniel Bristot de Oliveira default y 4204acadcbSDaniel Bristot de Oliveira depends on RV 4304acadcbSDaniel Bristot de Oliveira help 4404acadcbSDaniel Bristot de Oliveira Enables the online runtime verification reactors. A runtime 4504acadcbSDaniel Bristot de Oliveira monitor can cause a reaction to the detection of an exception 4604acadcbSDaniel Bristot de Oliveira on the model's execution. By default, the monitors have 4704acadcbSDaniel Bristot de Oliveira tracing reactions, printing the monitor output via tracepoints, 4804acadcbSDaniel Bristot de Oliveira but other reactions can be added (on-demand) via this interface. 49135b881eSDaniel Bristot de Oliveira 50135b881eSDaniel Bristot de Oliveiraconfig RV_REACT_PRINTK 51135b881eSDaniel Bristot de Oliveira bool "Printk reactor" 52135b881eSDaniel Bristot de Oliveira depends on RV_REACTORS 53135b881eSDaniel Bristot de Oliveira default y 54135b881eSDaniel Bristot de Oliveira help 55135b881eSDaniel Bristot de Oliveira Enables the printk reactor. The printk reactor emits a printk() 56135b881eSDaniel Bristot de Oliveira message if an exception is found. 57e88043c0SDaniel Bristot de Oliveira 58e88043c0SDaniel Bristot de Oliveiraconfig RV_REACT_PANIC 59e88043c0SDaniel Bristot de Oliveira bool "Panic reactor" 60e88043c0SDaniel Bristot de Oliveira depends on RV_REACTORS 61e88043c0SDaniel Bristot de Oliveira default y 62e88043c0SDaniel Bristot de Oliveira help 63e88043c0SDaniel Bristot de Oliveira Enables the panic reactor. The panic reactor emits a printk() 64e88043c0SDaniel Bristot de Oliveira message if an exception is found and panic()s the system. 65