github-mirror/linux
1
0
Fork 0
mirror of https://github.com/torvalds/linux.git synced 2026-05-30 18:13:41 +02:00
Code Issues Actions Packages Projects Releases Wiki Activity Graph

Documentation/rv: Prepare monitor synthesis document for LTL inclusion

Browse Source 
Monitor synthesis from deterministic automaton and linear temporal logic
have a lot in common. Therefore a single document should describe both.

Change da_monitor_synthesis.rst to monitor_synthesis.rst. LTL monitor
synthesis will be added to this file by a follow-up commit.

This makes the diff far easier to read. If renaming and adding LTL info is
done in a single commit, git wouldn't recognize it as a rename, but a file
removal and a file addition.

While at it, correct the old dot2k commands to the new rvgen commands.

Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/d91c6e4600287f4732d68a014219e576a75ce6dc.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
This commit is contained in:
Nam Cao 2025-07-04 15:20:02 +02:00 committed by Steven Rostedt (Google)
parent b6c62aa791
commit f40a7c0602
2 changed files with 11 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Documentation/trace/rv/index.rst
View File

@ -8,7 +8,7 @@ Runtime Verification
runtime-verification.rst runtime-verification.rst
deterministic_automata.rst deterministic_automata.rst
da_monitor_synthesis.rst monitor_synthesis.rst
da_monitor_instrumentation.rst da_monitor_instrumentation.rst
monitor_wip.rst monitor_wip.rst
monitor_wwnr.rst monitor_wwnr.rst

20
Documentation/trace/rv/da_monitor_synthesis.rst → Documentation/trace/rv/monitor_synthesis.rst
View File

@ -1,5 +1,5 @@
Deterministic Automata Monitor Synthesis Runtime Verification Monitor Synthesis
======================================== ======================================
The starting point for the application of runtime verification (RV) techniques The starting point for the application of runtime verification (RV) techniques
is the *specification* or *modeling* of the desired (or undesired) behavior is the *specification* or *modeling* of the desired (or undesired) behavior
@ -36,24 +36,24 @@ below::
| +----> panic ? | +----> panic ?
+-------> <user-specified> +-------> <user-specified>
DA monitor synthesis RV monitor synthesis
-------------------- --------------------
The synthesis of automata-based models into the Linux *RV monitor* abstraction The synthesis of automata-based models into the Linux *RV monitor* abstraction
is automated by the dot2k tool and the rv/da_monitor.h header file that is automated by the rvgen tool and the rv/da_monitor.h header file that
contains a set of macros that automatically generate the monitor's code. contains a set of macros that automatically generate the monitor's code.
dot2k rvgen
----- -----
The dot2k utility leverages dot2c by converting an automaton model in The rvgen utility leverages dot2c by converting an automaton model in
the DOT format into the C representation [1] and creating the skeleton of the DOT format into the C representation [1] and creating the skeleton of
a kernel monitor in C. a kernel monitor in C.
For example, it is possible to transform the wip.dot model present in For example, it is possible to transform the wip.dot model present in
[1] into a per-cpu monitor with the following command:: [1] into a per-cpu monitor with the following command::
$ dot2k -d wip.dot -t per_cpu $ rvgen monitor -c da -s wip.dot -t per_cpu
This will create a directory named wip/ with the following files: This will create a directory named wip/ with the following files:
@ -87,7 +87,7 @@ the second for monitors with per-cpu instances, and the third with per-task
instances. instances.
In all cases, the 'name' argument is a string that identifies the monitor, and In all cases, the 'name' argument is a string that identifies the monitor, and
the 'type' argument is the data type used by dot2k on the representation of the 'type' argument is the data type used by rvgen on the representation of
the model in C. the model in C.
For example, the wip model with two states and three events can be For example, the wip model with two states and three events can be
@ -134,7 +134,7 @@ Final remarks
------------- -------------
With the monitor synthesis in place using the rv/da_monitor.h and With the monitor synthesis in place using the rv/da_monitor.h and
dot2k, the developer's work should be limited to the instrumentation rvgen, the developer's work should be limited to the instrumentation
of the system, increasing the confidence in the overall approach. of the system, increasing the confidence in the overall approach.
[1] For details about deterministic automata format and the translation [1] For details about deterministic automata format and the translation
@ -142,6 +142,6 @@ from one representation to another, see::
Documentation/trace/rv/deterministic_automata.rst Documentation/trace/rv/deterministic_automata.rst
[2] dot2k appends the monitor's name suffix to the events enums to [2] rvgen appends the monitor's name suffix to the events enums to
avoid conflicting variables when exporting the global vmlinux.h avoid conflicting variables when exporting the global vmlinux.h
use by BPF programs. use by BPF programs.