On 5/19/21 8:10 PM, Randy Dunlap wrote: > 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. yes, you are right, I will remove it. >> + 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: > :) Ack! Thanks! -- Daniel
