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 <nam...@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.5
