kernel/trace/rv/Kconfig
Source file repositories/reference/linux-study-clean/kernel/trace/rv/Kconfig
File Facts
- System
- Linux kernel
- Corpus path
kernel/trace/rv/Kconfig- Extension
[no extension]- Size
- 3042 bytes
- Lines
- 114
- Domain
- Core OS
- Bucket
- Scheduler, Processes, Timers, Sync, And Syscalls
- Inferred role
- Core OS: build/configuration rule
- Status
- atlas-only
Why This File Exists
Core operating-system implementation surface: boot, tasks, memory, VFS, syscall-facing interfaces, synchronization, credentials, and isolation.
- Core operating-system implementation surface: boot, tasks, memory, VFS, syscall-facing interfaces, synchronization, credentials, and isolation.
Dependency Surface
- No C-style include directives detected by the generator.
Detected Declarations
- No top-level syscall, struct, function, initcall, or export declaration detected by the generator.
Annotated Snippet
# SPDX-License-Identifier: GPL-2.0-only
#
config RV_MON_EVENTS
bool
config RV_MON_MAINTENANCE_EVENTS
bool
config DA_MON_EVENTS_IMPLICIT
select RV_MON_EVENTS
select RV_MON_MAINTENANCE_EVENTS
bool
config DA_MON_EVENTS_ID
select RV_MON_EVENTS
select RV_MON_MAINTENANCE_EVENTS
bool
config LTL_MON_EVENTS_ID
select RV_MON_EVENTS
bool
config RV_LTL_MONITOR
bool
config RV_HA_MONITOR
bool
config HA_MON_EVENTS_IMPLICIT
select DA_MON_EVENTS_IMPLICIT
select RV_HA_MONITOR
bool
config HA_MON_EVENTS_ID
select DA_MON_EVENTS_ID
select RV_HA_MONITOR
bool
menuconfig RV
bool "Runtime Verification"
select 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_PER_TASK_MONITORS
int "Maximum number of per-task monitor"
depends on RV
range 1 8
default 2
help
This option configures the maximum number of per-task RV monitors that can run
simultaneously.
source "kernel/trace/rv/monitors/wip/Kconfig"
source "kernel/trace/rv/monitors/wwnr/Kconfig"
source "kernel/trace/rv/monitors/sched/Kconfig"
source "kernel/trace/rv/monitors/sco/Kconfig"
source "kernel/trace/rv/monitors/snroc/Kconfig"
source "kernel/trace/rv/monitors/scpd/Kconfig"
source "kernel/trace/rv/monitors/snep/Kconfig"
source "kernel/trace/rv/monitors/sts/Kconfig"
Annotation
- Atlas domain: Core OS / Scheduler, Processes, Timers, Sync, And Syscalls.
- Implementation status: atlas-only.
Implementation Notes
- This generated page is the file-by-file coverage layer; curated subsystem chapters should link here when they synthesize a multi-file control flow.
- Core OS pages should be promoted from atlas-only to deep-reviewed when they explain data structures, invariants, locking, lifecycle, and C implementation snippets.
- Driver-family pages are intentionally pattern-oriented unless they are part of the selected PCIe/NVMe representative device path.