<feed xmlns='http://www.w3.org/2005/Atom'>
<title>linux/tools/verification/dot2, branch master</title>
<subtitle>Mirror of https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/
</subtitle>
<id>https://git.shady.money/linux/atom?h=master</id>
<link rel='self' href='https://git.shady.money/linux/atom?h=master'/>
<link rel='alternate' type='text/html' href='https://git.shady.money/linux/'/>
<updated>2025-07-24T14:42:46Z</updated>
<entry>
<title>verification/dot2k: Prepare the frontend for LTL inclusion</title>
<updated>2025-07-24T14:42:46Z</updated>
<author>
<name>Nam Cao</name>
<email>namcao@linutronix.de</email>
</author>
<published>2025-07-04T13:20:01Z</published>
<link rel='alternate' type='text/html' href='https://git.shady.money/linux/commit/?id=b6c62aa7914b386c4a8983ec3a537399f523cf18'/>
<id>urn:sha1:b6c62aa7914b386c4a8983ec3a537399f523cf18</id>
<content type='text'>
The dot2k tool has some code that can be reused for linear temporal logic
monitor. Prepare its frontend for LTL inclusion:

  1. Rename to be generic: rvgen

  2. Replace the parameter --dot with 2 parameters:
     --class: to specific the monitor class, can be 'da' or 'ltl'
     --spec: the monitor specification file, .dot file for DA, and .ltl
             file for LTL

The old command:

  python3 dot2/dot2k monitor -d wip.dot -t per_cpu

is equivalent to the new commands:

  python3 rvgen monitor -c da -s wip.dot -t per_cpu

Cc: Masami Hiramatsu &lt;mhiramat@kernel.org&gt;
Cc: Mathieu Desnoyers &lt;mathieu.desnoyers@efficios.com&gt;
Link: https://lore.kernel.org/dea18f7a44374e4db8df5c7e785604bc3062ffc9.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco &lt;gmonaco@redhat.com&gt;
Signed-off-by: Nam Cao &lt;namcao@linutronix.de&gt;
Signed-off-by: Steven Rostedt (Google) &lt;rostedt@goodmis.org&gt;
</content>
</entry>
<entry>
<title>verification/dot2k: Replace is_container() hack with subparsers</title>
<updated>2025-07-24T14:42:46Z</updated>
<author>
<name>Nam Cao</name>
<email>namcao@linutronix.de</email>
</author>
<published>2025-07-04T13:19:59Z</published>
<link rel='alternate' type='text/html' href='https://git.shady.money/linux/commit/?id=5270a0e3041cba8aef76aaf62408313b9cd4ad9f'/>
<id>urn:sha1:5270a0e3041cba8aef76aaf62408313b9cd4ad9f</id>
<content type='text'>
dot2k is used for both generating deterministic automaton (DA) monitor and
generating container monitor.

Generating DA monitor and generating container requires different
parameters. This is implemented by peeking at sys.argv and check whether
"--container" is specified, and use that information to make some
parameters optional or required.

This works, but is quite hacky and ugly.

Replace this hack with Python's built-in subparsers.

The old commands:

  python3 dot2/dot2k -d wip.dot -t per_cpu
  python3 dot2/dot2k -n sched --container

are equivalent to the new commands:

  python3 dot2/dot2k monitor -d wip.dot -t per_cpu
  python3 dot2/dot2k container -n sched

Cc: Masami Hiramatsu &lt;mhiramat@kernel.org&gt;
Cc: Mathieu Desnoyers &lt;mathieu.desnoyers@efficios.com&gt;
Link: https://lore.kernel.org/23c4e3c6e10c39e86d8e6a289208dde407efc4a8.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco &lt;gmonaco@redhat.com&gt;
Signed-off-by: Nam Cao &lt;namcao@linutronix.de&gt;
Signed-off-by: Steven Rostedt (Google) &lt;rostedt@goodmis.org&gt;
</content>
</entry>
<entry>
<title>verification/dot2k: Remove __buff_to_string()</title>
<updated>2025-07-24T14:42:46Z</updated>
<author>
<name>Nam Cao</name>
<email>namcao@linutronix.de</email>
</author>
<published>2025-07-04T13:19:58Z</published>
<link rel='alternate' type='text/html' href='https://git.shady.money/linux/commit/?id=612934e99b562c959ea5fc4c3adc75248b17b818'/>
<id>urn:sha1:612934e99b562c959ea5fc4c3adc75248b17b818</id>
<content type='text'>
str.join() can do what __buff_to_string() does. Therefore replace
__buff_to_string() to make the scripts more pythonic.

Cc: Masami Hiramatsu &lt;mhiramat@kernel.org&gt;
Cc: Mathieu Desnoyers &lt;mathieu.desnoyers@efficios.com&gt;
Link: https://lore.kernel.org/860d6002659f604c743e0f23d5cf3c99ea6a82d8.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco &lt;gmonaco@redhat.com&gt;
Signed-off-by: Nam Cao &lt;namcao@linutronix.de&gt;
Signed-off-by: Steven Rostedt (Google) &lt;rostedt@goodmis.org&gt;
</content>
</entry>
<entry>
<title>verification/dot2k: Make a separate dot2k_templates/Kconfig_container</title>
<updated>2025-07-24T14:42:46Z</updated>
<author>
<name>Nam Cao</name>
<email>namcao@linutronix.de</email>
</author>
<published>2025-07-04T13:19:57Z</published>
<link rel='alternate' type='text/html' href='https://git.shady.money/linux/commit/?id=214459699fd202c28b7b9f787e674acbd3af724a'/>
<id>urn:sha1:214459699fd202c28b7b9f787e674acbd3af724a</id>
<content type='text'>
A generated container's Kconfig has an incorrect line:

    select DA_MON_EVENTS_IMPLICIT

This is due to container generation uses the same template Kconfig file as
deterministic automaton monitor.

Therefore, make a separate Kconfig template for container which has only
the necessaries for container.

Cc: Masami Hiramatsu &lt;mhiramat@kernel.org&gt;
Cc: Mathieu Desnoyers &lt;mathieu.desnoyers@efficios.com&gt;
Link: https://lore.kernel.org/d54fd7ee120785bec5695220e837dbbd6efb30e5.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco &lt;gmonaco@redhat.com&gt;
Signed-off-by: Nam Cao &lt;namcao@linutronix.de&gt;
Signed-off-by: Steven Rostedt (Google) &lt;rostedt@goodmis.org&gt;
</content>
</entry>
<entry>
<title>verification/dot2k: Add support for nested monitors</title>
<updated>2025-03-24T21:27:40Z</updated>
<author>
<name>Gabriele Monaco</name>
<email>gmonaco@redhat.com</email>
</author>
<published>2025-03-05T14:04:00Z</published>
<link rel='alternate' type='text/html' href='https://git.shady.money/linux/commit/?id=2334cf7d0963882a2247e06ef26776f9f98c730c'/>
<id>urn:sha1:2334cf7d0963882a2247e06ef26776f9f98c730c</id>
<content type='text'>
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 &lt;mingo@redhat.com&gt;
Cc: Peter Zijlstra &lt;peterz@infradead.org&gt;
Cc: Juri Lelli &lt;juri.lelli@redhat.com&gt;
Link: https://lore.kernel.org/20250305140406.350227-8-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco &lt;gmonaco@redhat.com&gt;
Signed-off-by: Steven Rostedt (Google) &lt;rostedt@goodmis.org&gt;
</content>
</entry>
<entry>
<title>rv: Add license identifiers to monitor files</title>
<updated>2025-03-04T17:11:08Z</updated>
<author>
<name>Gabriele Monaco</name>
<email>gmonaco@redhat.com</email>
</author>
<published>2025-02-18T12:31:07Z</published>
<link rel='alternate' type='text/html' href='https://git.shady.money/linux/commit/?id=41a4d2d3e3b6fe86bd54cc4c3b731378290a0d00'/>
<id>urn:sha1:41a4d2d3e3b6fe86bd54cc4c3b731378290a0d00</id>
<content type='text'>
Some monitor files like the main header and the Kconfig are missing the
license identifier.

Add it to those and make sure the automatic generation script includes
the line in newly created monitors.

Cc: Masami Hiramatsu &lt;mhiramat@kernel.org&gt;
Cc: Ingo Molnar &lt;mingo@redhat.com&gt;
Cc: Peter Zijlstra &lt;peterz@infradead.org&gt;
Cc: Juri Lelli &lt;juri.lelli@redhat.com&gt;
Link: https://lore.kernel.org/20250218123121.253551-3-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco &lt;gmonaco@redhat.com&gt;
Signed-off-by: Steven Rostedt (Google) &lt;rostedt@goodmis.org&gt;
</content>
</entry>
<entry>
<title>verification/dot2k: Implement event type detection</title>
<updated>2024-12-27T19:41:01Z</updated>
<author>
<name>Gabriele Monaco</name>
<email>gmonaco@redhat.com</email>
</author>
<published>2024-12-27T14:47:52Z</published>
<link rel='alternate' type='text/html' href='https://git.shady.money/linux/commit/?id=87c5d7f5e5938f713bde4e7435e6b207372a7f8e'/>
<id>urn:sha1:87c5d7f5e5938f713bde4e7435e6b207372a7f8e</id>
<content type='text'>
Currently dot2k treats all events equally and registers them with a
general da_handle_event. This is however just part of the work because
some events are necessary to understand when the monitor is entering the
initial state.

Specifically, the da_handle_start_event takes care of setting the
monitor in the initial state and da_handle_start_run_event also
registers the current event in the newly enabled monitor.
da_handle_start_event can be used on events that only lead to the
initial state (as it is currently done in the example monitors), while
da_handle_start_run_event could be used on events that are only valid
from the initial one.
Failing to set at least one of those functions to handle events makes
the monitor useless, since it will never be activated.

This patch adapts dot2k to parse the events that surely lead to the
initial state and set da_handle_start_event for those, if no such event
is found but some events are only valid in the initial event, we instead
set da_handle_start_run_event (it isn't necessary to set both).
We still add a comment to warn the user to make sure this change is
matching the model definition.

Cc: Juri Lelli &lt;juri.lelli@redhat.com&gt;
Cc: Thomas Gleixner &lt;tglx@linutronix.de&gt;
Cc: John Kacur &lt;jkacur@redhat.com&gt;
Link: https://lore.kernel.org/20241227144752.362911-9-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco &lt;gmonaco@redhat.com&gt;
Signed-off-by: Steven Rostedt (Google) &lt;rostedt@goodmis.org&gt;
</content>
</entry>
<entry>
<title>verification/dot2k: Auto patch current kernel source</title>
<updated>2024-12-27T19:39:35Z</updated>
<author>
<name>Gabriele Monaco</name>
<email>gmonaco@redhat.com</email>
</author>
<published>2024-12-27T14:47:51Z</published>
<link rel='alternate' type='text/html' href='https://git.shady.money/linux/commit/?id=de6f45c2dd226269fe9886290a139533c817c5bc'/>
<id>urn:sha1:de6f45c2dd226269fe9886290a139533c817c5bc</id>
<content type='text'>
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 &lt;juri.lelli@redhat.com&gt;
Cc: Thomas Gleixner &lt;tglx@linutronix.de&gt;
Cc: John Kacur &lt;jkacur@redhat.com&gt;
Link: https://lore.kernel.org/20241227144752.362911-8-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco &lt;gmonaco@redhat.com&gt;
Signed-off-by: Steven Rostedt (Google) &lt;rostedt@goodmis.org&gt;
</content>
</entry>
<entry>
<title>verification/dot2k: Simplify manual steps in monitor creation</title>
<updated>2024-12-27T19:21:28Z</updated>
<author>
<name>Gabriele Monaco</name>
<email>gmonaco@redhat.com</email>
</author>
<published>2024-12-27T14:47:50Z</published>
<link rel='alternate' type='text/html' href='https://git.shady.money/linux/commit/?id=9c6cfe80980056042f1f80d65c74806021708989'/>
<id>urn:sha1:9c6cfe80980056042f1f80d65c74806021708989</id>
<content type='text'>
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 &lt;monitors/monitor_name/monitor_name_trace.h&gt;

   - 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 &lt;juri.lelli@redhat.com&gt;
Cc: Thomas Gleixner &lt;tglx@linutronix.de&gt;
Cc: John Kacur &lt;jkacur@redhat.com&gt;
Link: https://lore.kernel.org/20241227144752.362911-7-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco &lt;gmonaco@redhat.com&gt;
Signed-off-by: Steven Rostedt (Google) &lt;rostedt@goodmis.org&gt;
</content>
</entry>
<entry>
<title>verification/dot2k: Add support for name and description options</title>
<updated>2024-12-27T19:19:34Z</updated>
<author>
<name>Gabriele Monaco</name>
<email>gmonaco@redhat.com</email>
</author>
<published>2024-12-27T14:47:48Z</published>
<link rel='alternate' type='text/html' href='https://git.shady.money/linux/commit/?id=64b3e5f0d45329bc593e13b64dcdcf836da006cd'/>
<id>urn:sha1:64b3e5f0d45329bc593e13b64dcdcf836da006cd</id>
<content type='text'>
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 &lt;juri.lelli@redhat.com&gt;
Cc: Thomas Gleixner &lt;tglx@linutronix.de&gt;
Cc: John Kacur &lt;jkacur@redhat.com&gt;
Link: https://lore.kernel.org/20241227144752.362911-5-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco &lt;gmonaco@redhat.com&gt;
Signed-off-by: Steven Rostedt (Google) &lt;rostedt@goodmis.org&gt;
</content>
</entry>
</feed>
