xref: /linux/kernel/trace/rv/Kconfig (revision 0fc8f6200d2313278fbf4539bbab74677c685531)
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