verification/dot2k: Add support for nested monitors

RV now supports nested monitors, this functionality requires a container
monitor, which has virtually no functionality besides holding other
monit

verification/dot2k: Add support for nested monitors

RV now supports nested monitors, this functionality requires a container
monitor, which has virtually no functionality besides holding other
monitors, and nested monitors, that have a container as parent.

Add the -p flag to pass a parent to a monitor, this sets it up while
registering the monitor and adds necessary includes and configurations.
Add the -c flag to create a container, since containers are empty, we
don't allow supplying a dot model or a monitor type, the template is
also different since functions to enable and disable the monitor are not
defined, nor any tracepoint. The generated header file only allows to
include the rv_monitor structure in children monitors.

Cc: Ingo Molnar <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Juri Lelli <[email protected]>
Link: https://lore.kernel.org/[email protected]
Signed-off-by: Gabriele Monaco <[email protected]>
Signed-off-by: Steven Rostedt (Google) <[email protected]>

show more ...

verification/dot2k: Auto patch current kernel source

dot2k suggests a list of changes to the kernel tree while adding a
monitor: edit tracepoints header, Makefile, Kconfig and moving the
monitor fol

verification/dot2k: Auto patch current kernel source

dot2k suggests a list of changes to the kernel tree while adding a
monitor: edit tracepoints header, Makefile, Kconfig and moving the
monitor 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 from
the running kernel, if installed.
This feature works best if the kernel tree is a git repository, so that
its easier to make sure there are no unintended changes.

The main RV files (e.g. Makefile) have now a comment placeholder that
can be useful for manual editing (e.g. to know where to add new
monitors) and it is used by the script to append the required lines.

We also slightly adapt the file handling functions in dot2k: __open_file
is now called __read_file and also closes the file before returning the
content; __create_file is now a more general __write_file, we no longer
return on FileExistsError (not thrown while opening), a new
__create_file simply calls __write_file specifying the monitor folder in
the path.

Cc: Juri Lelli <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: John Kacur <[email protected]>
Link: https://lore.kernel.org/[email protected]
Signed-off-by: Gabriele Monaco <[email protected]>
Signed-off-by: Steven Rostedt (Google) <[email protected]>

show more ...

verification/dot2k: Simplify manual steps in monitor creation

This patch reduces and simplifies the manual steps still needed in
creating a new RV monitor.

It extends the dot2k script to create a t

verification/dot2k: Simplify manual steps in monitor creation

This patch reduces and simplifies the manual steps still needed in
creating a new RV monitor.

It extends the dot2k script to create a tracepoint snippet and a
Kconfig file for the newly generated monitor. Those files can be kept
in the monitor's directory but shall be included in the main tracepoint
header and Kconfig.
Together with the checklist, dot2k now suggests the lines to add to
those files for inclusion and the Makefile line to compile the new
monitor:

Writing the monitor into the directory monitor_name
Almost done, checklist
- Edit the monitor_name/monitor_name.c to add the instrumentation
- Edit kernel/trace/rv/rv_trace.h:
Add this line where other tracepoints are included and DA_MON_EVENTS_ID is defined:
#include <monitors/monitor_name/monitor_name_trace.h>

- Edit kernel/trace/rv/Makefile:
Add this line where other monitors are included:
obj-$(CONFIG_RV_MON_MONITOR_NAME) += monitors/monitor_name/monitor_name.o

- Edit kernel/trace/rv/Kconfig:
Add this line where other monitors are included:
source "kernel/trace/rv/monitors/monitor_name/Kconfig"

- Move monitor_name/ to the kernel's monitor directory (kernel/trace/rv/monitors)

Cc: Juri Lelli <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: John Kacur <[email protected]>
Link: https://lore.kernel.org/[email protected]
Signed-off-by: Gabriele Monaco <[email protected]>
Signed-off-by: Steven Rostedt (Google) <[email protected]>

show more ...

verification/dot2k: Add support for name and description options

The dot2k command includes options to set a model name with -n and a
description with -D, however those are not used in practice.

Th

verification/dot2k: Add support for name and description options

The dot2k command includes options to set a model name with -n and a
description with -D, however those are not used in practice.

This patch allows to specify a custom model name (by default the name of
the dot file without extension) and a description which overrides the
one in the C file.

Cc: Juri Lelli <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: John Kacur <[email protected]>
Link: https://lore.kernel.org/[email protected]
Signed-off-by: Gabriele Monaco <[email protected]>
Signed-off-by: Steven Rostedt (Google) <[email protected]>

show more ...

verification/dot2k: Delete duplicate imports

The presence of duplicate import lines appears to be a typo.
Removing them.

Link: https://lore.kernel.org/r/20230906155703.3917918-1-alessandro.carminat

verification/dot2k: Delete duplicate imports

The presence of duplicate import lines appears to be a typo.
Removing them.

Link: https://lore.kernel.org/r/[email protected]

Fixes: 24bce201d798 ("tools/rv: Add dot2k")
Signed-off-by: Alessandro Carminati (Red Hat) <[email protected]>
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>

show more ...

Documentation/rv: Add deterministic automata monitor synthesis documentation

Add the da_monitor_synthesis.rst introduces some concepts behind the
Deterministic Automata (DA) monitor synthesis and in

Documentation/rv: Add deterministic automata monitor synthesis documentation

Add the da_monitor_synthesis.rst introduces some concepts behind the
Deterministic Automata (DA) monitor synthesis and interface.

Link: https://lkml.kernel.org/r/7873bdb7b2e5d2bc0b2eb6ca0b324af9a0ba27a0.1659052063.git.bristot@kernel.org

Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: Tao Zhou <[email protected]>
Cc: Randy Dunlap <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
Signed-off-by: Steven Rostedt (Google) <[email protected]>

show more ...

tools/rv: Add dot2k

transform .dot file into kernel rv monitor

usage: dot2k [-h] -d DOT_FILE -t MONITOR_TYPE [-n MODEL_NAME] [-D DESCRIPTION]

optional arguments:
-h, --help show this

tools/rv: Add dot2k

transform .dot file into kernel rv monitor

usage: dot2k [-h] -d DOT_FILE -t MONITOR_TYPE [-n MODEL_NAME] [-D DESCRIPTION]

optional arguments:
-h, --help show this help message and exit
-d DOT_FILE, --dot DOT_FILE
-t MONITOR_TYPE, --monitor_type MONITOR_TYPE
-n MODEL_NAME, --model_name MODEL_NAME
-D DESCRIPTION, --description DESCRIPTION

Link: https://lkml.kernel.org/r/083b3ae61e5a62c1e2e5d08009baa91f82181618.1659052063.git.bristot@kernel.org

Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: Tao Zhou <[email protected]>
Cc: Randy Dunlap <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
Signed-off-by: Steven Rostedt (Google) <[email protected]>

show more ...