| 123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778 |
- # SPDX-License-Identifier: GPL-2.0-only
- #
- config DA_MON_EVENTS
- bool
- config DA_MON_EVENTS_IMPLICIT
- select DA_MON_EVENTS
- bool
- config DA_MON_EVENTS_ID
- select DA_MON_EVENTS
- bool
- menuconfig RV
- bool "Runtime Verification"
- depends on TRACING
- help
- Enable the kernel runtime verification infrastructure. RV is a
- lightweight (yet rigorous) method that complements classical
- exhaustive verification techniques (such as model checking and
- theorem proving). RV works by analyzing the trace of the system's
- actual execution, comparing it against a formal specification of
- the system behavior.
- For further information, see:
- Documentation/trace/rv/runtime-verification.rst
- config RV_MON_WIP
- depends on RV
- depends on PREEMPT_TRACER
- select DA_MON_EVENTS_IMPLICIT
- bool "wip monitor"
- help
- Enable wip (wakeup in preemptive) sample monitor that illustrates
- the usage of per-cpu monitors, and one limitation of the
- preempt_disable/enable events.
- For further information, see:
- Documentation/trace/rv/monitor_wip.rst
- config RV_MON_WWNR
- depends on RV
- select DA_MON_EVENTS_ID
- bool "wwnr monitor"
- help
- Enable wwnr (wakeup while not running) sample monitor, this is a
- sample monitor that illustrates the usage of per-task monitor.
- The model is borken on purpose: it serves to test reactors.
- For further information, see:
- Documentation/trace/rv/monitor_wwnr.rst
- config RV_REACTORS
- bool "Runtime verification reactors"
- default y
- depends on RV
- help
- Enables the online runtime verification reactors. A runtime
- monitor can cause a reaction to the detection of an exception
- on the model's execution. By default, the monitors have
- tracing reactions, printing the monitor output via tracepoints,
- but other reactions can be added (on-demand) via this interface.
- config RV_REACT_PRINTK
- bool "Printk reactor"
- depends on RV_REACTORS
- default y
- help
- Enables the printk reactor. The printk reactor emits a printk()
- message if an exception is found.
- config RV_REACT_PANIC
- bool "Panic reactor"
- depends on RV_REACTORS
- default y
- help
- Enables the panic reactor. The panic reactor emits a printk()
- message if an exception is found and panic()s the system.
|
