1 # SPDX-License-Identifier: GPL-2.0-only 1 # SPDX-License-Identifier: GPL-2.0-only
2 # 2 #
3 config DA_MON_EVENTS 3 config DA_MON_EVENTS
4 bool 4 bool
5 5
6 config DA_MON_EVENTS_IMPLICIT 6 config DA_MON_EVENTS_IMPLICIT
7 select DA_MON_EVENTS 7 select DA_MON_EVENTS
8 bool 8 bool
9 9
10 config DA_MON_EVENTS_ID 10 config DA_MON_EVENTS_ID
11 select DA_MON_EVENTS 11 select DA_MON_EVENTS
12 bool 12 bool
13 13
14 menuconfig RV 14 menuconfig RV
15 bool "Runtime Verification" 15 bool "Runtime Verification"
16 depends on TRACING 16 depends on TRACING
17 help 17 help
18 Enable the kernel runtime verificati 18 Enable the kernel runtime verification infrastructure. RV is a
19 lightweight (yet rigorous) method th 19 lightweight (yet rigorous) method that complements classical
20 exhaustive verification techniques ( 20 exhaustive verification techniques (such as model checking and
21 theorem proving). RV works by analyz 21 theorem proving). RV works by analyzing the trace of the system's
22 actual execution, comparing it again 22 actual execution, comparing it against a formal specification of
23 the system behavior. 23 the system behavior.
24 24
25 For further information, see: 25 For further information, see:
26 Documentation/trace/rv/runtime-ver 26 Documentation/trace/rv/runtime-verification.rst
27 27
28 config RV_MON_WIP 28 config RV_MON_WIP
29 depends on RV 29 depends on RV
30 depends on PREEMPT_TRACER 30 depends on PREEMPT_TRACER
31 select DA_MON_EVENTS_IMPLICIT 31 select DA_MON_EVENTS_IMPLICIT
32 bool "wip monitor" 32 bool "wip monitor"
33 help 33 help
34 Enable wip (wakeup in preemptive) sa 34 Enable wip (wakeup in preemptive) sample monitor that illustrates
35 the usage of per-cpu monitors, and o 35 the usage of per-cpu monitors, and one limitation of the
36 preempt_disable/enable events. 36 preempt_disable/enable events.
37 37
38 For further information, see: 38 For further information, see:
39 Documentation/trace/rv/monitor_wip 39 Documentation/trace/rv/monitor_wip.rst
40 40
41 config RV_MON_WWNR 41 config RV_MON_WWNR
42 depends on RV 42 depends on RV
43 select DA_MON_EVENTS_ID 43 select DA_MON_EVENTS_ID
44 bool "wwnr monitor" 44 bool "wwnr monitor"
45 help 45 help
46 Enable wwnr (wakeup while not runnin 46 Enable wwnr (wakeup while not running) sample monitor, this is a
47 sample monitor that illustrates the 47 sample monitor that illustrates the usage of per-task monitor.
48 The model is borken on purpose: it s 48 The model is borken on purpose: it serves to test reactors.
49 49
50 For further information, see: 50 For further information, see:
51 Documentation/trace/rv/monitor_wwn 51 Documentation/trace/rv/monitor_wwnr.rst
52 52
53 config RV_REACTORS 53 config RV_REACTORS
54 bool "Runtime verification reactors" 54 bool "Runtime verification reactors"
55 default y 55 default y
56 depends on RV 56 depends on RV
57 help 57 help
58 Enables the online runtime verificat 58 Enables the online runtime verification reactors. A runtime
59 monitor can cause a reaction to the 59 monitor can cause a reaction to the detection of an exception
60 on the model's execution. By default 60 on the model's execution. By default, the monitors have
61 tracing reactions, printing the moni 61 tracing reactions, printing the monitor output via tracepoints,
62 but other reactions can be added (on 62 but other reactions can be added (on-demand) via this interface.
63 63
64 config RV_REACT_PRINTK 64 config RV_REACT_PRINTK
65 bool "Printk reactor" 65 bool "Printk reactor"
66 depends on RV_REACTORS 66 depends on RV_REACTORS
67 default y 67 default y
68 help 68 help
69 Enables the printk reactor. The prin 69 Enables the printk reactor. The printk reactor emits a printk()
70 message if an exception is found. 70 message if an exception is found.
71 71
72 config RV_REACT_PANIC 72 config RV_REACT_PANIC
73 bool "Panic reactor" 73 bool "Panic reactor"
74 depends on RV_REACTORS 74 depends on RV_REACTORS
75 default y 75 default y
76 help 76 help
77 Enables the panic reactor. The panic 77 Enables the panic reactor. The panic reactor emits a printk()
78 message if an exception is found and 78 message if an exception is found and panic()s the system.
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.