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 26f5587d1bSGabriele Monacoconfig RV_HA_MONITOR 27f5587d1bSGabriele Monaco bool 28f5587d1bSGabriele Monaco 29f5587d1bSGabriele Monacoconfig HA_MON_EVENTS_IMPLICIT 30f5587d1bSGabriele Monaco select DA_MON_EVENTS_IMPLICIT 31f5587d1bSGabriele Monaco select RV_HA_MONITOR 32f5587d1bSGabriele Monaco bool 33f5587d1bSGabriele Monaco 34f5587d1bSGabriele Monacoconfig HA_MON_EVENTS_ID 35f5587d1bSGabriele Monaco select DA_MON_EVENTS_ID 36f5587d1bSGabriele Monaco select RV_HA_MONITOR 37f5587d1bSGabriele Monaco bool 38f5587d1bSGabriele Monaco 39102227b9SDaniel Bristot de Oliveiramenuconfig RV 40102227b9SDaniel Bristot de Oliveira bool "Runtime Verification" 41f74f8bb2SNam Cao select TRACING 42102227b9SDaniel Bristot de Oliveira help 43102227b9SDaniel Bristot de Oliveira Enable the kernel runtime verification infrastructure. RV is a 44102227b9SDaniel Bristot de Oliveira lightweight (yet rigorous) method that complements classical 45102227b9SDaniel Bristot de Oliveira exhaustive verification techniques (such as model checking and 46102227b9SDaniel Bristot de Oliveira theorem proving). RV works by analyzing the trace of the system's 47102227b9SDaniel Bristot de Oliveira actual execution, comparing it against a formal specification of 48102227b9SDaniel Bristot de Oliveira the system behavior. 4904acadcbSDaniel Bristot de Oliveira 50ff0aaf67SDaniel Bristot de Oliveira For further information, see: 51ff0aaf67SDaniel Bristot de Oliveira Documentation/trace/rv/runtime-verification.rst 52ff0aaf67SDaniel Bristot de Oliveira 53fac54932SNam Caoconfig RV_PER_TASK_MONITORS 54fac54932SNam Cao int "Maximum number of per-task monitor" 55fac54932SNam Cao depends on RV 56fac54932SNam Cao range 1 8 57fac54932SNam Cao default 2 58fac54932SNam Cao help 59fac54932SNam Cao This option configures the maximum number of per-task RV monitors that can run 60fac54932SNam Cao simultaneously. 61fac54932SNam Cao 62bc3d482dSGabriele Monacosource "kernel/trace/rv/monitors/wip/Kconfig" 63bc3d482dSGabriele Monacosource "kernel/trace/rv/monitors/wwnr/Kconfig" 64560473f2SGabriele Monaco 65cb85c660SGabriele Monacosource "kernel/trace/rv/monitors/sched/Kconfig" 669fd420abSGabriele Monacosource "kernel/trace/rv/monitors/sco/Kconfig" 6793bac9cfSGabriele Monacosource "kernel/trace/rv/monitors/snroc/Kconfig" 68fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/scpd/Kconfig" 69fbe6c09bSGabriele Monacosource "kernel/trace/rv/monitors/snep/Kconfig" 70d0096c2fSGabriele Monacosource "kernel/trace/rv/monitors/sts/Kconfig" 71e8440a88SGabriele Monacosource "kernel/trace/rv/monitors/nrp/Kconfig" 72e8440a88SGabriele Monacosource "kernel/trace/rv/monitors/sssw/Kconfig" 7361438453SGabriele Monacosource "kernel/trace/rv/monitors/opid/Kconfig" 74560473f2SGabriele Monaco# Add new sched monitors here 75560473f2SGabriele Monaco 76886fc86eSNam Caosource "kernel/trace/rv/monitors/rtapp/Kconfig" 779162620eSNam Caosource "kernel/trace/rv/monitors/pagefault/Kconfig" 78f74f8bb2SNam Caosource "kernel/trace/rv/monitors/sleep/Kconfig" 79560473f2SGabriele Monaco# Add new rtapp monitors here 80560473f2SGabriele Monaco 8113578a08SGabriele Monacosource "kernel/trace/rv/monitors/stall/Kconfig" 82*b133207dSGabriele Monacosource "kernel/trace/rv/monitors/deadline/Kconfig" 83*b133207dSGabriele Monacosource "kernel/trace/rv/monitors/nomiss/Kconfig" 84*b133207dSGabriele Monaco# Add new deadline monitors here 85*b133207dSGabriele Monaco 86de6f45c2SGabriele Monaco# Add new monitors here 87ccc319dcSDaniel Bristot de Oliveira 8804acadcbSDaniel Bristot de Oliveiraconfig RV_REACTORS 8904acadcbSDaniel Bristot de Oliveira bool "Runtime verification reactors" 9004acadcbSDaniel Bristot de Oliveira default y 9104acadcbSDaniel Bristot de Oliveira depends on RV 9204acadcbSDaniel Bristot de Oliveira help 9304acadcbSDaniel Bristot de Oliveira Enables the online runtime verification reactors. A runtime 9404acadcbSDaniel Bristot de Oliveira monitor can cause a reaction to the detection of an exception 9504acadcbSDaniel Bristot de Oliveira on the model's execution. By default, the monitors have 9604acadcbSDaniel Bristot de Oliveira tracing reactions, printing the monitor output via tracepoints, 9704acadcbSDaniel Bristot de Oliveira but other reactions can be added (on-demand) via this interface. 98135b881eSDaniel Bristot de Oliveira 99135b881eSDaniel Bristot de Oliveiraconfig RV_REACT_PRINTK 100135b881eSDaniel Bristot de Oliveira bool "Printk reactor" 101135b881eSDaniel Bristot de Oliveira depends on RV_REACTORS 102135b881eSDaniel Bristot de Oliveira default y 103135b881eSDaniel Bristot de Oliveira help 104135b881eSDaniel Bristot de Oliveira Enables the printk reactor. The printk reactor emits a printk() 105135b881eSDaniel Bristot de Oliveira message if an exception is found. 106e88043c0SDaniel Bristot de Oliveira 107e88043c0SDaniel Bristot de Oliveiraconfig RV_REACT_PANIC 108e88043c0SDaniel Bristot de Oliveira bool "Panic reactor" 109e88043c0SDaniel Bristot de Oliveira depends on RV_REACTORS 110e88043c0SDaniel Bristot de Oliveira default y 111e88043c0SDaniel Bristot de Oliveira help 112e88043c0SDaniel Bristot de Oliveira Enables the panic reactor. The panic reactor emits a printk() 113e88043c0SDaniel Bristot de Oliveira message if an exception is found and panic()s the system. 114