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 2810bde81cSDaniel Bristot de Oliveiraconfig RV_MON_WIP 2910bde81cSDaniel Bristot de Oliveira depends on RV 3010bde81cSDaniel Bristot de Oliveira depends on PREEMPT_TRACER 3110bde81cSDaniel Bristot de Oliveira select DA_MON_EVENTS_IMPLICIT 3210bde81cSDaniel Bristot de Oliveira bool "wip monitor" 3310bde81cSDaniel Bristot de Oliveira help 3410bde81cSDaniel Bristot de Oliveira Enable wip (wakeup in preemptive) sample monitor that illustrates 3510bde81cSDaniel Bristot de Oliveira the usage of per-cpu monitors, and one limitation of the 3610bde81cSDaniel Bristot de Oliveira preempt_disable/enable events. 3710bde81cSDaniel Bristot de Oliveira 3810bde81cSDaniel Bristot de Oliveira For further information, see: 3910bde81cSDaniel Bristot de Oliveira Documentation/trace/rv/monitor_wip.rst 4010bde81cSDaniel Bristot de Oliveira 41*ccc319dcSDaniel Bristot de Oliveiraconfig RV_MON_WWNR 42*ccc319dcSDaniel Bristot de Oliveira depends on RV 43*ccc319dcSDaniel Bristot de Oliveira select DA_MON_EVENTS_ID 44*ccc319dcSDaniel Bristot de Oliveira bool "wwnr monitor" 45*ccc319dcSDaniel Bristot de Oliveira help 46*ccc319dcSDaniel Bristot de Oliveira Enable wwnr (wakeup while not running) sample monitor, this is a 47*ccc319dcSDaniel Bristot de Oliveira sample monitor that illustrates the usage of per-task monitor. 48*ccc319dcSDaniel Bristot de Oliveira The model is borken on purpose: it serves to test reactors. 49*ccc319dcSDaniel Bristot de Oliveira 50*ccc319dcSDaniel Bristot de Oliveira For further information, see: 51*ccc319dcSDaniel Bristot de Oliveira Documentation/trace/rv/monitor_wwnr.rst 52*ccc319dcSDaniel Bristot de Oliveira 5304acadcbSDaniel Bristot de Oliveiraconfig RV_REACTORS 5404acadcbSDaniel Bristot de Oliveira bool "Runtime verification reactors" 5504acadcbSDaniel Bristot de Oliveira default y 5604acadcbSDaniel Bristot de Oliveira depends on RV 5704acadcbSDaniel Bristot de Oliveira help 5804acadcbSDaniel Bristot de Oliveira Enables the online runtime verification reactors. A runtime 5904acadcbSDaniel Bristot de Oliveira monitor can cause a reaction to the detection of an exception 6004acadcbSDaniel Bristot de Oliveira on the model's execution. By default, the monitors have 6104acadcbSDaniel Bristot de Oliveira tracing reactions, printing the monitor output via tracepoints, 6204acadcbSDaniel Bristot de Oliveira but other reactions can be added (on-demand) via this interface. 63