On 5/19/21 4:36 AM, Daniel Bristot de Oliveira wrote: > diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig > new file mode 100644 > index 000000000000..e8e65cfc7959 > --- /dev/null > +++ b/kernel/trace/rv/Kconfig > @@ -0,0 +1,13 @@ > +# SPDX-License-Identifier: GPL-2.0-only > +# > +menuconfig RV > + bool "Runtime Verification" > + depends on TRACING > + default y if DEBUG_KERNEL No need for default y. There are other reasons to use DEBUG_KERNEL without wanting RV turned on. > + 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. And in the cover/patch 00: tlrd: should be tl;dr: or at least tldr: :) -- ~Randy
