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"
---
tools/verification/rvgen/rvgen/ltl2k.py | 48 ++++++++++++++++---
.../rvgen/rvgen/templates/ltl2k/main.c | 9 ++--
.../rvgen/rvgen/templates/ltl2k/trace.h | 7 ++-
3 files changed, 50 insertions(+), 14 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index b075f98d50c4..f291d1f03d05 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -57,9 +57,16 @@ class ltl2k(generator.Monitor):
template_dir = "ltl2k"
def __init__(self, file_path, MonitorType, extra_params={}):
- if MonitorType != "per_task":
- raise NotImplementedError("Only per_task monitor is supported for LTL")
+ if MonitorType == "per_task":
+ self._target_arg = "struct task_struct *task"
+ self._target = "task"
+ elif MonitorType == "per_cpu":
+ self._target_arg = "unsigned int cpu"
+ self._target = "cpu"
+ else:
+ raise NotImplementedError(f"LTL does not support monitor type {MonitorType}")
super().__init__(extra_params)
+ self.monitor_type = MonitorType
with open(file_path) as f:
self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read())
self.atoms_abbr = abbreviate_atoms(self.atoms)
@@ -67,6 +74,13 @@ class ltl2k(generator.Monitor):
if not self.name:
self.name = Path(file_path).stem
+ def _fill_monitor_type(self) -> str:
+ if self.monitor_type == "per_task":
+ return "#define LTL_MONITOR_TYPE RV_MON_PER_TASK"
+ if self.monitor_type == "per_cpu":
+ return "#define LTL_MONITOR_TYPE RV_MON_PER_CPU"
+ assert False
+
def _fill_states(self) -> str:
buf = [
"enum ltl_buchi_state {",
@@ -174,7 +188,7 @@ class ltl2k(generator.Monitor):
def _fill_start(self):
buf = [
- "static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)",
+ "static void ltl_start(%s, struct ltl_monitor *mon)" % self._target_arg,
"{"
]
@@ -205,7 +219,7 @@ class ltl2k(generator.Monitor):
buff = []
buff.append("static void handle_example_event(void *data, /* XXX: fill header */)")
buff.append("{")
- buff.append("\tltl_atom_update(task, LTL_%s, true/false);" % self.atoms[0])
+ buff.append("\tltl_atom_update(%s, LTL_%s, true/false);" % (self._target, self.atoms[0]))
buff.append("}")
buff.append("")
return '\n'.join(buff)
@@ -241,6 +255,9 @@ class ltl2k(generator.Monitor):
""
]
+ buf.append(self._fill_monitor_type())
+ buf.append('')
+
buf.extend(self._fill_atoms())
buf.append('')
@@ -259,13 +276,32 @@ class ltl2k(generator.Monitor):
return '\n'.join(buf)
def fill_monitor_class_type(self):
- return "LTL_MON_EVENTS_ID"
+ if self.monitor_type == "per_task":
+ return "LTL_MON_EVENTS_ID"
+ if self.monitor_type == "per_cpu":
+ return "LTL_MON_EVENTS_CPU"
+ assert False
def fill_monitor_class(self):
- return "ltl_monitor_id"
+ if self.monitor_type == "per_task":
+ return "ltl_monitor_id"
+ if self.monitor_type == "per_cpu":
+ return "ltl_monitor_cpu"
+ assert False
+
+ def fill_tracepoint_args_skel(self, tp_type):
+ if tp_type == "event":
+ return \
+ ("\tTP_PROTO(%s, char *states, char *atoms, char *next),\n" % self._target_arg) + \
+ ("\tTP_ARGS(%s, states, atoms, next)" % self._target)
+ if tp_type == "error":
+ return \
+ ("\tTP_PROTO(%s),\n" % self._target_arg) + \
+ ("\tTP_ARGS(%s)" % self._target)
def fill_main_c(self):
main_c = super().fill_main_c()
main_c = main_c.replace("%%ATOMS_INIT%%", self.fill_atoms_init())
+ main_c = main_c.replace("%%TARGET_ARG%%", self._target_arg)
return main_c
diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c
index f85d076fbf78..09167efbfbf0 100644
--- a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c
+++ b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c
@@ -23,7 +23,7 @@
#include "%%MODEL_NAME%%.h"
#include <rv/ltl_monitor.h>
-static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+static void ltl_atoms_fetch(%%TARGET_ARG%%, struct ltl_monitor *mon)
{
/*
* This is called everytime the Buchi automaton is triggered.
@@ -36,13 +36,14 @@ static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
*/
}
-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.
*/
%%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%% */
--
2.39.5On 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%% */
Gabriele Monaco <gmonaco@redhat.com> writes: > 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" Sorry, after re-reading this one day later, I am still not sure why you says "online" is imprecise. Due to hotplug, CPUs can become online and offline. The current implementation ignore hotplug and initialize all possible CPUs as if they are all oneline. But if hotplug becomes important in the future, I may add a CPU hotplug handler. > Other than that it looks good to me. > > Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Thanks! Nam
On Fri, 2025-08-08 at 07:12 +0200, Nam Cao wrote: > Gabriele Monaco <gmonaco@redhat.com> writes: > > 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" > > Sorry, after re-reading this one day later, I am still not sure why > you says "online" is imprecise. Due to hotplug, CPUs can become > online and offline. > > The current implementation ignore hotplug and initialize all possible > CPUs as if they are all oneline. But if hotplug becomes important in > the future, I may add a CPU hotplug handler. Alright, I was probably a bit unclear with that, I don't mean the implementation needs changes, only the wording. > This is false if the monitor target is already online before the > monitor is enabled. becomes > This is false if the CPU is already online before the monitor is > enabled. which is not always true, when starting the monitor, you initialise all possible CPUs, also offline ones, which are still initialised with @target_creation as false. Mind I don't say you should change the value passed to ltl_target_init nor change your logic, I only mean /online/ isn't the right word here. Does this make more sense? Thanks, Gabriele
Gabriele Monaco <gmonaco@redhat.com> writes: > Mind I don't say you should change the value passed to ltl_target_init > nor change your logic, I only mean /online/ isn't the right word here. > > Does this make more sense? Yes, thanks for the elaboration! Nam
© 2016 - 2025 Red Hat, Inc.