| 1 | # SPDX-License-Identifier: GPL-2.0-only |
| 2 | # |
| 3 | config RV_MON_EVENTS |
| 4 | bool |
| 5 | |
| 6 | config RV_MON_MAINTENANCE_EVENTS |
| 7 | bool |
| 8 | |
| 9 | config DA_MON_EVENTS_IMPLICIT |
| 10 | select RV_MON_EVENTS |
| 11 | select RV_MON_MAINTENANCE_EVENTS |
| 12 | bool |
| 13 | |
| 14 | config DA_MON_EVENTS_ID |
| 15 | select RV_MON_EVENTS |
| 16 | select RV_MON_MAINTENANCE_EVENTS |
| 17 | bool |
| 18 | |
| 19 | config LTL_MON_EVENTS_ID |
| 20 | select RV_MON_EVENTS |
| 21 | bool |
| 22 | |
| 23 | config RV_LTL_MONITOR |
| 24 | bool |
| 25 | |
| 26 | config RV_HA_MONITOR |
| 27 | bool |
| 28 | |
| 29 | config HA_MON_EVENTS_IMPLICIT |
| 30 | select DA_MON_EVENTS_IMPLICIT |
| 31 | select RV_HA_MONITOR |
| 32 | bool |
| 33 | |
| 34 | config HA_MON_EVENTS_ID |
| 35 | select DA_MON_EVENTS_ID |
| 36 | select RV_HA_MONITOR |
| 37 | bool |
| 38 | |
| 39 | menuconfig RV |
| 40 | bool "Runtime Verification" |
| 41 | select TRACING |
| 42 | help |
| 43 | Enable the kernel runtime verification infrastructure. RV is a |
| 44 | lightweight (yet rigorous) method that complements classical |
| 45 | exhaustive verification techniques (such as model checking and |
| 46 | theorem proving). RV works by analyzing the trace of the system's |
| 47 | actual execution, comparing it against a formal specification of |
| 48 | the system behavior. |
| 49 | |
| 50 | For further information, see: |
| 51 | Documentation/trace/rv/runtime-verification.rst |
| 52 | |
| 53 | config RV_PER_TASK_MONITORS |
| 54 | int "Maximum number of per-task monitor" |
| 55 | depends on RV |
| 56 | range 1 8 |
| 57 | default 2 |
| 58 | help |
| 59 | This option configures the maximum number of per-task RV monitors that can run |
| 60 | simultaneously. |
| 61 | |
| 62 | source "kernel/trace/rv/monitors/wip/Kconfig" |
| 63 | source "kernel/trace/rv/monitors/wwnr/Kconfig" |
| 64 | |
| 65 | source "kernel/trace/rv/monitors/sched/Kconfig" |
| 66 | source "kernel/trace/rv/monitors/sco/Kconfig" |
| 67 | source "kernel/trace/rv/monitors/snroc/Kconfig" |
| 68 | source "kernel/trace/rv/monitors/scpd/Kconfig" |
| 69 | source "kernel/trace/rv/monitors/snep/Kconfig" |
| 70 | source "kernel/trace/rv/monitors/sts/Kconfig" |
| 71 | source "kernel/trace/rv/monitors/nrp/Kconfig" |
| 72 | source "kernel/trace/rv/monitors/sssw/Kconfig" |
| 73 | source "kernel/trace/rv/monitors/opid/Kconfig" |
| 74 | # Add new sched monitors here |
| 75 | |
| 76 | source "kernel/trace/rv/monitors/rtapp/Kconfig" |
| 77 | source "kernel/trace/rv/monitors/pagefault/Kconfig" |
| 78 | source "kernel/trace/rv/monitors/sleep/Kconfig" |
| 79 | source "kernel/trace/rv/monitors/wakeup/Kconfig" |
| 80 | # Add new rtapp monitors here |
| 81 | |
| 82 | source "kernel/trace/rv/monitors/stall/Kconfig" |
| 83 | source "kernel/trace/rv/monitors/deadline/Kconfig" |
| 84 | source "kernel/trace/rv/monitors/nomiss/Kconfig" |
| 85 | # Add new deadline monitors here |
| 86 | |
| 87 | # Add new monitors here |
| 88 | |
| 89 | config RV_REACTORS |
| 90 | bool "Runtime verification reactors" |
| 91 | default y |
| 92 | depends on RV |
| 93 | help |
| 94 | Enables the online runtime verification reactors. A runtime |
| 95 | monitor can cause a reaction to the detection of an exception |
| 96 | on the model's execution. By default, the monitors have |
| 97 | tracing reactions, printing the monitor output via tracepoints, |
| 98 | but other reactions can be added (on-demand) via this interface. |
| 99 | |
| 100 | config RV_REACT_PRINTK |
| 101 | bool "Printk reactor" |
| 102 | depends on RV_REACTORS |
| 103 | default y |
| 104 | help |
| 105 | Enables the printk reactor. The printk reactor emits a printk() |
| 106 | message if an exception is found. |
| 107 | |
| 108 | config RV_REACT_PANIC |
| 109 | bool "Panic reactor" |
| 110 | depends on RV_REACTORS |
| 111 | default y |
| 112 | help |
| 113 | Enables the panic reactor. The panic reactor emits a printk() |
| 114 | message if an exception is found and panic()s the system. |
| 115 | |
| 116 | config RV_MONITORS_KUNIT_TEST |
| 117 | tristate "KUnit tests for RV monitors" if !KUNIT_ALL_TESTS |
| 118 | depends on KUNIT && RV && RV_REACTORS |
| 119 | default KUNIT_ALL_TESTS |
| 120 | help |
| 121 | Enable KUnit tests for the RV (Runtime Verification) monitors. |
| 122 | These tests verify that monitors correctly detect violations by |
| 123 | triggering fake events and validating the expected reactions. |
| 124 | |
| 125 | Enabling this may slightly increase overhead of some monitors if any |
| 126 | unrelated KUnit test is running. |
| 127 | |
| 128 | If unsure, say N. |