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 69d475d80SGabriele Monacoconfig RV_MON_MAINTENANCE_EVENTS 79d475d80SGabriele Monaco bool 89d475d80SGabriele Monaco 979257534SDaniel Bristot de Oliveiraconfig DA_MON_EVENTS_IMPLICIT 10c94d27c0SNam Cao select RV_MON_EVENTS 119d475d80SGabriele Monaco select RV_MON_MAINTENANCE_EVENTS 1279257534SDaniel Bristot de Oliveira bool 1379257534SDaniel Bristot de Oliveira 1479257534SDaniel Bristot de Oliveiraconfig DA_MON_EVENTS_ID 15c94d27c0SNam Cao select RV_MON_EVENTS 169d475d80SGabriele Monaco select RV_MON_MAINTENANCE_EVENTS 1779257534SDaniel Bristot de Oliveira bool 1879257534SDaniel Bristot de Oliveira 19a9769a5bSNam Caoconfig LTL_MON_EVENTS_ID 20a9769a5bSNam Cao select RV_MON_EVENTS 21a9769a5bSNam Cao bool 22a9769a5bSNam Cao 23a9769a5bSNam Caoconfig RV_LTL_MONITOR 24a9769a5bSNam Cao bool 25a9769a5bSNam Cao 26102227b9SDaniel Bristot de Oliveiramenuconfig RV 27102227b9SDaniel Bristot de Oliveira bool "Runtime Verification" 28f74f8bb2SNam Cao select TRACING 29102227b9SDaniel Bristot de Oliveira help 30102227b9SDaniel Bristot de Oliveira Enable the kernel runtime verification infrastructure. RV is a 31102227b9SDaniel Bristot de Oliveira lightweight (yet rigorous) method that complements classical 32102227b9SDaniel Bristot de Oliveira exhaustive verification techniques (such as model checking and 33102227b9SDaniel Bristot de Oliveira theorem proving). RV works by analyzing the trace of the system's 34102227b9SDaniel Bristot de Oliveira actual execution, comparing it against a formal specification of 35102227b9SDaniel Bristot de Oliveira the system behavior. 3604acadcbSDaniel Bristot de Oliveira 37ff0aaf67SDaniel Bristot de Oliveira For further information, see: 38ff0aaf67SDaniel Bristot de Oliveira Documentation/trace/rv/runtime-verification.rst 39ff0aaf67SDaniel Bristot de Oliveira 40fac54932SNam Caoconfig RV_PER_TASK_MONITORS 41fac54932SNam Cao int "Maximum number of per-task monitor" 42fac54932SNam Cao depends on RV 43fac54932SNam Cao range 1 8 44fac54932SNam Cao default 2 45fac54932SNam Cao help 46fac54932SNam Cao This option configures the maximum number of per-task RV monitors that can run 47fac54932SNam Cao simultaneously. 48fac54932SNam Cao 49bc3d482dSGabriele Monacosource "kernel/trace/rv/monitors/wip/Kconfig" 50bc3d482dSGabriele Monacosource "kernel/trace/rv/monitors/wwnr/Kconfig" 51560473f2SGabriele Monaco 52cb85c660SGabriele Monacosource "kernel/trace/rv/monitors/sched/Kconfig" 539fd420abSGabriele Monacosource "kernel/trace/rv/monitors/sco/Kconfig" 5493bac9cfSGabriele Monacosource "kernel/trace/rv/monitors/snroc/Kconfig" 55fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/scpd/Kconfig" 56fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/snep/Kconfig" 57d0096c2fSGabriele Monacosource "kernel/trace/rv/monitors/sts/Kconfig" 58*e8440a88SGabriele Monacosource "kernel/trace/rv/monitors/nrp/Kconfig" 59*e8440a88SGabriele Monacosource "kernel/trace/rv/monitors/sssw/Kconfig" 60560473f2SGabriele Monaco# Add new sched monitors here 61560473f2SGabriele Monaco 62886fc86eSNam Caosource "kernel/trace/rv/monitors/rtapp/Kconfig" 639162620eSNam Caosource "kernel/trace/rv/monitors/pagefault/Kconfig" 64f74f8bb2SNam Caosource "kernel/trace/rv/monitors/sleep/Kconfig" 65560473f2SGabriele Monaco# Add new rtapp monitors here 66560473f2SGabriele Monaco 67de6f45c2SGabriele Monaco# Add new monitors here 68ccc319dcSDaniel Bristot de Oliveira 6904acadcbSDaniel Bristot de Oliveiraconfig RV_REACTORS 7004acadcbSDaniel Bristot de Oliveira bool "Runtime verification reactors" 7104acadcbSDaniel Bristot de Oliveira default y 7204acadcbSDaniel Bristot de Oliveira depends on RV 7304acadcbSDaniel Bristot de Oliveira help 7404acadcbSDaniel Bristot de Oliveira Enables the online runtime verification reactors. A runtime 7504acadcbSDaniel Bristot de Oliveira monitor can cause a reaction to the detection of an exception 7604acadcbSDaniel Bristot de Oliveira on the model's execution. By default, the monitors have 7704acadcbSDaniel Bristot de Oliveira tracing reactions, printing the monitor output via tracepoints, 7804acadcbSDaniel Bristot de Oliveira but other reactions can be added (on-demand) via this interface. 79135b881eSDaniel Bristot de Oliveira 80135b881eSDaniel Bristot de Oliveiraconfig RV_REACT_PRINTK 81135b881eSDaniel Bristot de Oliveira bool "Printk reactor" 82135b881eSDaniel Bristot de Oliveira depends on RV_REACTORS 83135b881eSDaniel Bristot de Oliveira default y 84135b881eSDaniel Bristot de Oliveira help 85135b881eSDaniel Bristot de Oliveira Enables the printk reactor. The printk reactor emits a printk() 86135b881eSDaniel Bristot de Oliveira message if an exception is found. 87e88043c0SDaniel Bristot de Oliveira 88e88043c0SDaniel Bristot de Oliveiraconfig RV_REACT_PANIC 89e88043c0SDaniel Bristot de Oliveira bool "Panic reactor" 90e88043c0SDaniel Bristot de Oliveira depends on RV_REACTORS 91e88043c0SDaniel Bristot de Oliveira default y 92e88043c0SDaniel Bristot de Oliveira help 93e88043c0SDaniel Bristot de Oliveira Enables the panic reactor. The panic reactor emits a printk() 94e88043c0SDaniel Bristot de Oliveira message if an exception is found and panic()s the system. 95