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