Re: [PATCH v2 10/22] Documentation/rv: Prepare monitor synthesis document for LTL inclusion

[Gabriele Monaco]

On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> 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.
> 
> Signed-off-by: Nam Cao <namcao@xxxxxxxxxxxxx>
> ---
>  Documentation/trace/rv/index.rst              |  2 +-
>  ...or_synthesis.rst => monitor_synthesis.rst} | 20 +++++++++--------
> --
>  2 files changed, 11 insertions(+), 11 deletions(-)
>  rename Documentation/trace/rv/{da_monitor_synthesis.rst =>
> monitor_synthesis.rst} (92%)
> 
> diff --git a/Documentation/trace/rv/index.rst
> b/Documentation/trace/rv/index.rst
> index e80e0057feb4..8e411b76ec82 100644
> --- a/Documentation/trace/rv/index.rst
> +++ b/Documentation/trace/rv/index.rst
> @@ -8,7 +8,7 @@ Runtime Verification
>  
>     runtime-verification.rst
>     deterministic_automata.rst
> -   da_monitor_synthesis.rst
> +   monitor_synthesis.rst
>     da_monitor_instrumentation.rst
>     monitor_wip.rst
>     monitor_wwnr.rst
> diff --git a/Documentation/trace/rv/da_monitor_synthesis.rst
> b/Documentation/trace/rv/monitor_synthesis.rst
> similarity index 92%
> rename from Documentation/trace/rv/da_monitor_synthesis.rst
> rename to Documentation/trace/rv/monitor_synthesis.rst
> index 0a92729c8a9b..7d848e204687 100644
> --- a/Documentation/trace/rv/da_monitor_synthesis.rst
> +++ b/Documentation/trace/rv/monitor_synthesis.rst
> @@ -1,5 +1,5 @@
> -Deterministic Automata Monitor Synthesis
> -========================================
> +Runtime verification Monitor Synthesis
> +======================================

+Runtime Verification Monitor Synthesis

The title is capitalised here.

The rest looks good, thanks.

Reviewed-by: Gabriele Monaco <gmonaco@xxxxxxxxxx>

>  
>  The starting point for the application of runtime verification (RV)
> techniques
>  is the *specification* or *modeling* of the desired (or undesired)
> behavior
> @@ -36,24 +36,24 @@ below::
>                                    |  +----> panic ?
>                                    +-------> <user-specified>
>  
> -DA monitor synthesis
> +RV monitor synthesis
>  --------------------
>  
>  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.
>  
> -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
>  a kernel monitor in C.
>  
>  For example, it is possible to transform the wip.dot model present
> in
>  [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:
>  
> @@ -87,7 +87,7 @@ the second for monitors with per-cpu instances, and
> the third with per-task
>  instances.
>  
>  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.
>  
>  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
> -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.
>  
>  [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
>  
> -[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
>  use by BPF programs.