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" 23f74f8bb2SNam Cao select 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 35fac54932SNam Caoconfig RV_PER_TASK_MONITORS 36fac54932SNam Cao int "Maximum number of per-task monitor" 37fac54932SNam Cao depends on RV 38fac54932SNam Cao range 1 8 39fac54932SNam Cao default 2 40fac54932SNam Cao help 41fac54932SNam Cao This option configures the maximum number of per-task RV monitors that can run 42fac54932SNam Cao simultaneously. 43fac54932SNam Cao 44bc3d482dSGabriele Monacosource "kernel/trace/rv/monitors/wip/Kconfig" 45bc3d482dSGabriele Monacosource "kernel/trace/rv/monitors/wwnr/Kconfig" 46*560473f2SGabriele Monaco 47cb85c660SGabriele Monacosource "kernel/trace/rv/monitors/sched/Kconfig" 489fd420abSGabriele Monacosource "kernel/trace/rv/monitors/tss/Kconfig" 499fd420abSGabriele Monacosource "kernel/trace/rv/monitors/sco/Kconfig" 5093bac9cfSGabriele Monacosource "kernel/trace/rv/monitors/snroc/Kconfig" 51fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/scpd/Kconfig" 52fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/snep/Kconfig" 53fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/sncid/Kconfig" 54*560473f2SGabriele Monaco# Add new sched monitors here 55*560473f2SGabriele Monaco 56886fc86eSNam Caosource "kernel/trace/rv/monitors/rtapp/Kconfig" 579162620eSNam Caosource "kernel/trace/rv/monitors/pagefault/Kconfig" 58f74f8bb2SNam Caosource "kernel/trace/rv/monitors/sleep/Kconfig" 59*560473f2SGabriele Monaco# Add new rtapp monitors here 60*560473f2SGabriele Monaco 61de6f45c2SGabriele Monaco# Add new monitors here 62ccc319dcSDaniel Bristot de Oliveira 6304acadcbSDaniel Bristot de Oliveiraconfig RV_REACTORS 6404acadcbSDaniel Bristot de Oliveira bool "Runtime verification reactors" 6504acadcbSDaniel Bristot de Oliveira default y 6604acadcbSDaniel Bristot de Oliveira depends on RV 6704acadcbSDaniel Bristot de Oliveira help 6804acadcbSDaniel Bristot de Oliveira Enables the online runtime verification reactors. A runtime 6904acadcbSDaniel Bristot de Oliveira monitor can cause a reaction to the detection of an exception 7004acadcbSDaniel Bristot de Oliveira on the model's execution. By default, the monitors have 7104acadcbSDaniel Bristot de Oliveira tracing reactions, printing the monitor output via tracepoints, 7204acadcbSDaniel Bristot de Oliveira but other reactions can be added (on-demand) via this interface. 73135b881eSDaniel Bristot de Oliveira 74135b881eSDaniel Bristot de Oliveiraconfig RV_REACT_PRINTK 75135b881eSDaniel Bristot de Oliveira bool "Printk reactor" 76135b881eSDaniel Bristot de Oliveira depends on RV_REACTORS 77135b881eSDaniel Bristot de Oliveira default y 78135b881eSDaniel Bristot de Oliveira help 79135b881eSDaniel Bristot de Oliveira Enables the printk reactor. The printk reactor emits a printk() 80135b881eSDaniel Bristot de Oliveira message if an exception is found. 81e88043c0SDaniel Bristot de Oliveira 82e88043c0SDaniel Bristot de Oliveiraconfig RV_REACT_PANIC 83e88043c0SDaniel Bristot de Oliveira bool "Panic reactor" 84e88043c0SDaniel Bristot de Oliveira depends on RV_REACTORS 85e88043c0SDaniel Bristot de Oliveira default y 86e88043c0SDaniel Bristot de Oliveira help 87e88043c0SDaniel Bristot de Oliveira Enables the panic reactor. The panic reactor emits a printk() 88e88043c0SDaniel Bristot de Oliveira message if an exception is found and panic()s the system. 89