Re: [PATCH v2 3/5] verification/rvgen/ltl: Support per-cpu monitor generation

[Gabriele Monaco <gmonaco@redhat.com>]

On Wed, 2025-08-06 at 10:01 +0200, Nam Cao wrote:
> Add support to generate per-cpu LTL monitors. Similar to generating
> per-cpu monitors from .dot files, the "-t per_cpu" parameter can be
> used to generate per-cpu monitors from .ltl files.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
> v2: Rename "implicit" to "cpu"
> ---
>  
> -static void ltl_atoms_init(struct task_struct *task, struct
> ltl_monitor *mon, bool task_creation)
> +static void ltl_atoms_init(%%TARGET_ARG%%, struct ltl_monitor *mon,
> bool target_creation)
>  {
>  	/*
>  	 * This should initialize as many atomic propositions as
> possible.
>  	 *
> -	 * @task_creation indicates whether the task is being
> created. This is
> -	 * false if the task is already running before the monitor
> is enabled.
> +	 * @target_creation indicates whether the monitored target
> is being
> +	 * created. This is false if the monitor target is already
> online before
> +	 * the monitor is enabled.

I get you're trying to be more type-agnostic, but I believe this
/online/ is a bit imprecise, unless you register a hotplug handler and
just initialise the online CPUs (much of an overkill I'd say).
What about something like "this is false if the monitor exists already
before the monitor is enabled"

Other than that it looks good to me.

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

Thanks,
Gabriele

>  	 */
>  %%ATOMS_INIT%%
>  }
> diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h
> b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h
> index 49394c4b0f1c..87d3a1308926 100644
> --- a/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h
> +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h
> @@ -6,9 +6,8 @@
>  
>  #ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%%
>  DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%,
> -	     TP_PROTO(struct task_struct *task, char *states, char
> *atoms, char *next),
> -	     TP_ARGS(task, states, atoms, next));
> +%%TRACEPOINT_ARGS_SKEL_EVENT%%);
> +
>  DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%,
> -	     TP_PROTO(struct task_struct *task),
> -	     TP_ARGS(task));
> +%%TRACEPOINT_ARGS_SKEL_ERROR%%);
>  #endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */