1102227b9SDaniel Bristot de Oliveira# SPDX-License-Identifier: GPL-2.0-only 2102227b9SDaniel Bristot de Oliveira# 3c94d27c0SNam Caoconfig RV_MON_EVENTS 479257534SDaniel Bristot de Oliveira bool 579257534SDaniel Bristot de Oliveira 679257534SDaniel Bristot de Oliveiraconfig DA_MON_EVENTS_IMPLICIT 7c94d27c0SNam Cao select RV_MON_EVENTS 879257534SDaniel Bristot de Oliveira bool 979257534SDaniel Bristot de Oliveira 1079257534SDaniel Bristot de Oliveiraconfig DA_MON_EVENTS_ID 11c94d27c0SNam Cao select RV_MON_EVENTS 1279257534SDaniel Bristot de Oliveira bool 1379257534SDaniel Bristot de Oliveira 14a9769a5bSNam Caoconfig LTL_MON_EVENTS_ID 15a9769a5bSNam Cao select RV_MON_EVENTS 16a9769a5bSNam Cao bool 17a9769a5bSNam Cao 18a9769a5bSNam Caoconfig RV_LTL_MONITOR 19a9769a5bSNam Cao bool 20a9769a5bSNam Cao 21102227b9SDaniel Bristot de Oliveiramenuconfig RV 22102227b9SDaniel Bristot de Oliveira bool "Runtime Verification" 23102227b9SDaniel Bristot de Oliveira depends on TRACING 24102227b9SDaniel Bristot de Oliveira help 25102227b9SDaniel Bristot de Oliveira Enable the kernel runtime verification infrastructure. RV is a 26102227b9SDaniel Bristot de Oliveira lightweight (yet rigorous) method that complements classical 27102227b9SDaniel Bristot de Oliveira exhaustive verification techniques (such as model checking and 28102227b9SDaniel Bristot de Oliveira theorem proving). RV works by analyzing the trace of the system's 29102227b9SDaniel Bristot de Oliveira actual execution, comparing it against a formal specification of 30102227b9SDaniel Bristot de Oliveira the system behavior. 3104acadcbSDaniel Bristot de Oliveira 32ff0aaf67SDaniel Bristot de Oliveira For further information, see: 33ff0aaf67SDaniel Bristot de Oliveira Documentation/trace/rv/runtime-verification.rst 34ff0aaf67SDaniel Bristot de Oliveira 35bc3d482dSGabriele Monacosource "kernel/trace/rv/monitors/wip/Kconfig" 36bc3d482dSGabriele Monacosource "kernel/trace/rv/monitors/wwnr/Kconfig" 37cb85c660SGabriele Monacosource "kernel/trace/rv/monitors/sched/Kconfig" 389fd420abSGabriele Monacosource "kernel/trace/rv/monitors/tss/Kconfig" 399fd420abSGabriele Monacosource "kernel/trace/rv/monitors/sco/Kconfig" 4093bac9cfSGabriele Monacosource "kernel/trace/rv/monitors/snroc/Kconfig" 41fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/scpd/Kconfig" 42fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/snep/Kconfig" 43fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/sncid/Kconfig" 44886fc86eSNam Caosource "kernel/trace/rv/monitors/rtapp/Kconfig" 45*9162620eSNam Caosource "kernel/trace/rv/monitors/pagefault/Kconfig" 46de6f45c2SGabriele Monaco# Add new monitors here 47ccc319dcSDaniel Bristot de Oliveira 4804acadcbSDaniel Bristot de Oliveiraconfig RV_REACTORS 4904acadcbSDaniel Bristot de Oliveira bool "Runtime verification reactors" 5004acadcbSDaniel Bristot de Oliveira default y 5104acadcbSDaniel Bristot de Oliveira depends on RV 5204acadcbSDaniel Bristot de Oliveira help 5304acadcbSDaniel Bristot de Oliveira Enables the online runtime verification reactors. A runtime 5404acadcbSDaniel Bristot de Oliveira monitor can cause a reaction to the detection of an exception 5504acadcbSDaniel Bristot de Oliveira on the model's execution. By default, the monitors have 5604acadcbSDaniel Bristot de Oliveira tracing reactions, printing the monitor output via tracepoints, 5704acadcbSDaniel Bristot de Oliveira but other reactions can be added (on-demand) via this interface. 58135b881eSDaniel Bristot de Oliveira 59135b881eSDaniel Bristot de Oliveiraconfig RV_REACT_PRINTK 60135b881eSDaniel Bristot de Oliveira bool "Printk reactor" 61135b881eSDaniel Bristot de Oliveira depends on RV_REACTORS 62135b881eSDaniel Bristot de Oliveira default y 63135b881eSDaniel Bristot de Oliveira help 64135b881eSDaniel Bristot de Oliveira Enables the printk reactor. The printk reactor emits a printk() 65135b881eSDaniel Bristot de Oliveira message if an exception is found. 66e88043c0SDaniel Bristot de Oliveira 67e88043c0SDaniel Bristot de Oliveiraconfig RV_REACT_PANIC 68e88043c0SDaniel Bristot de Oliveira bool "Panic reactor" 69e88043c0SDaniel Bristot de Oliveira depends on RV_REACTORS 70e88043c0SDaniel Bristot de Oliveira default y 71e88043c0SDaniel Bristot de Oliveira help 72e88043c0SDaniel Bristot de Oliveira Enables the panic reactor. The panic reactor emits a printk() 73e88043c0SDaniel Bristot de Oliveira message if an exception is found and panic()s the system. 74