Changes in Kconfig

fbe6c09b - rv: Add scpd, snep and sncid per-cpu monitors

Wed, 05 Mar 2025 14:03:58 +0000

rv: Add scpd, snep and sncid per-cpu monitorsAdd 3 per-cpu monitors as part of the sched model:* scpd: schedule called with preemption disabled Monitor to ensure schedule is called with preemption disabled* snep: schedule does not enable preempt Monitor to ensure schedule does not enable preempt* sncid: schedule not called with interrupt disabled Monitor to ensure schedule is not called with interrupt disabledTo: Ingo Molnar To: Peter Zijlstra Cc: Juri Lelli Cc: Ingo Molnar Cc: Peter Zijlstra Cc: John Kacur Cc: Clark Williams Link: https://lore.kernel.org/20250305140406.350227-6-gmonaco@redhat.comSigned-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

93bac9cf - rv: Add snroc per-task monitor

Wed, 05 Mar 2025 14:03:57 +0000

rv: Add snroc per-task monitorAdd a per-task monitor as part of the sched model:* snroc: set non runnable on its own context Monitor to ensure set_state happens only in the respective task's contextTo: Ingo Molnar To: Peter Zijlstra Cc: Juri Lelli Cc: Ingo Molnar Cc: Peter Zijlstra Cc: John Kacur Cc: Clark Williams Link: https://lore.kernel.org/20250305140406.350227-5-gmonaco@redhat.comSigned-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

9fd420ab - rv: Add sco and tss per-cpu monitors

Wed, 05 Mar 2025 14:03:56 +0000

rv: Add sco and tss per-cpu monitorsAdd 2 per-cpu monitors as part of the sched model:* sco: scheduling context operations Monitor to ensure sched_set_state happens only in thread context* tss: task switch while scheduling Monitor to ensure sched_switch happens only in scheduling contextTo: Ingo Molnar To: Peter Zijlstra Cc: Juri Lelli Cc: Ingo Molnar Cc: Peter Zijlstra Cc: John Kacur Cc: Clark Williams Link: https://lore.kernel.org/20250305140406.350227-4-gmonaco@redhat.comSigned-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

cb85c660 - rv: Add option for nested monitors and include sched

Wed, 05 Mar 2025 14:03:55 +0000

rv: Add option for nested monitors and include schedMonitors describing complex systems, such as the scheduler, can easilygrow to the point where they are just hard to understand because of themany possible state transitions.Often it is possible to break such descriptions into smaller monitors,sharing some or all events. Enabling those smaller monitors concurrentlyis, in fact, testing the system as if we had one single larger monitor.Splitting models into multiple specification is not only easier tounderstand, but gives some more clues when we see errors.Add the possibility to create container monitors, whose only purpose isto host other nested monitors. Enabling a container monitor enables allnested ones, but it's still possible to enable nested monitorsindependently.Add the sched monitor as first container, for now empty.Cc: Ingo Molnar Cc: Peter Zijlstra Cc: Juri Lelli Link: https://lore.kernel.org/20250305140406.350227-3-gmonaco@redhat.comSigned-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

de6f45c2 - verification/dot2k: Auto patch current kernel source

Fri, 27 Dec 2024 14:47:51 +0000

verification/dot2k: Auto patch current kernel sourcedot2k suggests a list of changes to the kernel tree while adding amonitor: edit tracepoints header, Makefile, Kconfig and moving themonitor folder. Those changes can be easily run automatically.Add a flag to dot2k to alter the kernel source.The kernel source directory can be either assumed from the PWD, or fromthe running kernel, if installed.This feature works best if the kernel tree is a git repository, so thatits easier to make sure there are no unintended changes.The main RV files (e.g. Makefile) have now a comment placeholder thatcan be useful for manual editing (e.g. to know where to add newmonitors) and it is used by the script to append the required lines.We also slightly adapt the file handling functions in dot2k: __open_fileis now called __read_file and also closes the file before returning thecontent; __create_file is now a more general __write_file, we no longerreturn on FileExistsError (not thrown while opening), a new__create_file simply calls __write_file specifying the monitor folder inthe path.Cc: Juri Lelli Cc: Thomas Gleixner Cc: John Kacur Link: https://lore.kernel.org/20241227144752.362911-8-gmonaco@redhat.comSigned-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

bc3d482d - rv: Simplify manual steps in monitor creation

Fri, 27 Dec 2024 14:47:49 +0000

rv: Simplify manual steps in monitor creationWhile creating a new monitor in RV, besides generating code from dot2k,there are a few manual steps which can be tedious and error prone, likeadding the tracepoints, makefile lines and kconfig.This patch restructures the existing monitors to keep some files in themonitor's folder itself, which can be automatically generated by futureversions of dot2k.Monitors have now their own Kconfig and tracepoint snippets. Forsimplicity, the main tracepoint definition, is moved to the RVdirectory, it defines only the tracepoint classes and includes themonitor-specific tracepoints, which reside in the monitor directory.Tracepoints and Kconfig no longer need to be copied and adapted fromexisting ones but only need to be included in the main files.The Makefile remains untouched since there's little advantage in havinga separated Makefile for each monitor with a single line and includingit in the main RV Makefile.Cc: Juri Lelli Cc: Thomas Gleixner Cc: John Kacur Link: https://lore.kernel.org/20241227144752.362911-6-gmonaco@redhat.comSigned-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

e88043c0 - rv/reactor: Add the panic reactor

Fri, 29 Jul 2022 09:38:55 +0000

rv/reactor: Add the panic reactorSample reactor that panics the system when an exception is found. Thisis useful both to capture a vmcore, or to fail-safe a critical system.Link: https://lkml.kernel.org/r/729aae3aba95f35738b8f8180e626d747d1d9da2.1659052063.git.bristot@kernel.orgCc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap Cc: linux-doc@vger.kernel.orgCc: linux-kernel@vger.kernel.orgCc: linux-trace-devel@vger.kernel.orgSigned-off-by: Daniel Bristot de Oliveira Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

135b881e - rv/reactor: Add the printk reactor

Fri, 29 Jul 2022 09:38:54 +0000

rv/reactor: Add the printk reactorA reactor that printks the reaction message.Link: https://lkml.kernel.org/r/b65f18a7fd6dc6659a3008fd7b7392de3465d47b.1659052063.git.bristot@kernel.orgCc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap Cc: linux-doc@vger.kernel.orgCc: linux-kernel@vger.kernel.orgCc: linux-trace-devel@vger.kernel.orgSigned-off-by: Daniel Bristot de Oliveira Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

ccc319dc - rv/monitor: Add the wwnr monitor

Fri, 29 Jul 2022 09:38:53 +0000

rv/monitor: Add the wwnr monitorPer task wakeup while not running (wwnr) monitor.This model is broken, the reason is that a task can be running in theprocessor without being set as RUNNABLE. Think about a task about tosleep:1: set_current_state(TASK_UNINTERRUPTIBLE);2: schedule();And then imagine an IRQ happening in between the lines one and two,waking the task up. BOOM, the wakeup will happen while the task isrunning.Q: Why do we need this model, so?A: To test the reactors.Link: https://lkml.kernel.org/r/473c0fc39967250fdebcff8b620311c11dccad30.1659052063.git.bristot@kernel.orgCc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap Cc: linux-doc@vger.kernel.orgCc: linux-kernel@vger.kernel.orgCc: linux-trace-devel@vger.kernel.orgSigned-off-by: Daniel Bristot de Oliveira Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

10bde81c - rv/monitor: Add the wip monitor

Fri, 29 Jul 2022 09:38:52 +0000

rv/monitor: Add the wip monitorThe wakeup in preemptive (wip) monitor verifies if thewakeup events always take place with preemption disabled: | | v #==================# H preemptive H <+ #==================# | | | | preempt_disable | preempt_enable v | sched_waking +------------------+ | +--------------- | | | | | non_preemptive | | +--------------> | | -+ +------------------+The wakeup event always takes place with preemption disabled becauseof the scheduler synchronization. However, because the preempt_countand its trace event are not atomic with regard to interrupts, someinconsistencies might happen.The documentation illustrates one of these cases.Link: https://lkml.kernel.org/r/c98ca678df81115fddc04921b3c79720c836b18f.1659052063.git.bristot@kernel.orgCc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap Cc: linux-doc@vger.kernel.orgCc: linux-kernel@vger.kernel.orgCc: linux-trace-devel@vger.kernel.orgSigned-off-by: Daniel Bristot de Oliveira Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

ff0aaf67 - Documentation/rv: Add a basic documentation

Fri, 29 Jul 2022 09:38:45 +0000

Documentation/rv: Add a basic documentationAdd the runtime-verification.rst document, explaining the basics of RVand how to use the interface.Link: https://lkml.kernel.org/r/4be7d1a88ab1e2eb0767521e1ab52a149a154bc4.1659052063.git.bristot@kernel.orgCc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap Cc: linux-doc@vger.kernel.orgCc: linux-kernel@vger.kernel.orgCc: linux-trace-devel@vger.kernel.orgSigned-off-by: Daniel Bristot de Oliveira Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

79257534 - rv/include: Add deterministic automata monitor definition via C macros

Fri, 29 Jul 2022 09:38:43 +0000

rv/include: Add deterministic automata monitor definition via C macrosIn Linux terms, the runtime verification monitors are encapsulatedinside the "RV monitor" abstraction. The "RV monitor" includes a setof instances of the monitor (per-cpu monitor, per-task monitor, andso on), the helper functions that glue the monitor to the systemreference model, and the trace output as a reaction for event parsingand exceptions, as depicted below:Linux +----- RV Monitor ----------------------------------+ Formal Realm | | Realm +-------------------+ +----------------+ +-----------------+ | Linux kernel | | Monitor | | Reference | | Tracing | -> | Instance(s) | <- | Model | | (instrumentation) | | (verification) | | (specification) | +-------------------+ +----------------+ +-----------------+ | | | | V | | +----------+ | | | Reaction | | | +--+--+--+-+ | | | | | | | | | +-> trace output ? | +------------------------|--|----------------------+ | +----> panic ? +-------> Add the rv/da_monitor.h, enabling automatic code generation for the*Monitor Instance(s)* using C macros, and code to support it.The benefits of the usage of macro for monitor synthesis are 3-fold as it:- Reduces the code duplication;- Facilitates the bug fix/improvement;- Avoids the case of developers changing the core of the monitor code to manipulate the model in a (let's say) non-standard way.This initial implementation presents three different types of monitorinstances:- DECLARE_DA_MON_GLOBAL(name, type)- DECLARE_DA_MON_PER_CPU(name, type)- DECLARE_DA_MON_PER_TASK(name, type)The first declares the functions for a global deterministic automata monitor,the second for monitors with per-cpu instances, and the third with per-taskinstances.Link: https://lkml.kernel.org/r/51b0bf425a281e226dfeba7401d2115d6091f84e.1659052063.git.bristot@kernel.orgCc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap Cc: linux-doc@vger.kernel.orgCc: linux-kernel@vger.kernel.orgCc: linux-trace-devel@vger.kernel.orgSigned-off-by: Daniel Bristot de Oliveira Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

04acadcb - rv: Add runtime reactors interface

Fri, 29 Jul 2022 09:38:41 +0000

rv: Add runtime reactors interfaceA runtime monitor can cause a reaction to the detection of anexception on the model's execution. By default, the monitors havetracing reactions, printing the monitor output via tracepoints.But other reactions can be added (on-demand) via this interface.The user interface resembles the kernel tracing interface andpresents these files:"available_reactors" - Reading shows the available reactors, one per line. For example: # cat available_reactors nop panic printk "reacting_on" - It is an on/off general switch for reactors, disabling all reactions. "monitors/MONITOR/reactors" - List available reactors, with the select reaction for the given MONITOR inside []. The default one is the nop (no operation) reactor. - Writing the name of a reactor enables it to the given MONITOR. For example: # cat monitors/wip/reactors [nop] panic printk # echo panic > monitors/wip/reactors # cat monitors/wip/reactors nop [panic] printkLink: https://lkml.kernel.org/r/1794eb994637457bdeaa6bad0b8263d2f7eece0c.1659052063.git.bristot@kernel.orgCc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap Cc: linux-doc@vger.kernel.orgCc: linux-kernel@vger.kernel.orgCc: linux-trace-devel@vger.kernel.orgSigned-off-by: Daniel Bristot de Oliveira Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig

102227b9 - rv: Add Runtime Verification (RV) interface

Fri, 29 Jul 2022 09:38:40 +0000

rv: Add Runtime Verification (RV) interfaceRV is a lightweight (yet rigorous) method that complements classicalexhaustive verification techniques (such as model checking andtheorem proving) with a more practical approach to complex systems.RV works by analyzing the trace of the system's actual execution,comparing it against a formal specification of the system behavior.RV can give precise information on the runtime behavior of themonitored system while enabling the reaction for unexpectedevents, avoiding, for example, the propagation of a failure onsafety-critical systems.The development of this interface roots in the development of thepaper:De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, RomuloSilva. Efficient formal verification for the Linux kernel. In:International Conference on Software Engineering and Formal Methods.Springer, Cham, 2019. p. 315-332.And:De Oliveira, Daniel Bristot. Automata-based formal analysisand verification of the real-time Linux kernel. PhD Thesis, 2020.The RV interface resembles the tracing/ interface on purpose. The currentpath for the RV interface is /sys/kernel/tracing/rv/.It presents these files: "available_monitors" - List the available monitors, one per line. For example: # cat available_monitors wip wwnr "enabled_monitors" - Lists the enabled monitors, one per line; - Writing to it enables a given monitor; - Writing a monitor name with a '!' prefix disables it; - Truncating the file disables all enabled monitors. For example: # cat enabled_monitors # echo wip > enabled_monitors # echo wwnr >> enabled_monitors # cat enabled_monitors wip wwnr # echo '!wip' >> enabled_monitors # cat enabled_monitors wwnr # echo > enabled_monitors # cat enabled_monitors # Note that more than one monitor can be enabled concurrently. "monitoring_on" - It is an on/off general switcher for monitoring. Note that it does not disable enabled monitors or detach events, but stop the per-entity monitors of monitoring the events received from the system. It resembles the "tracing_on" switcher. "monitors/" Each monitor will have its one directory inside "monitors/". There the monitor specific files will be presented. The "monitors/" directory resembles the "events" directory on tracefs. For example: # cd monitors/wip/ # ls desc enable # cat desc wakeup in preemptive per-cpu testing monitor. # cat enable 0For further information, see the comments in the header ofkernel/trace/rv/rv.c from this patch.Link: https://lkml.kernel.org/r/a4bfe038f50cb047bfb343ad0e12b0e646ab308b.1659052063.git.bristot@kernel.orgCc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap Cc: linux-doc@vger.kernel.orgCc: linux-kernel@vger.kernel.orgCc: linux-trace-devel@vger.kernel.orgSigned-off-by: Daniel Bristot de Oliveira Signed-off-by: Steven Rostedt (Google) List of files: /linux-6.15/kernel/trace/rv/Kconfig