| lists.openwall.net | lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC | |
|
Open Source and information security mailing list archives
| ||
|
Message-Id: <3c7900721428d9091f70302ea9b6c4577c749f63.1753879295.git.namcao@linutronix.de>
Date: Wed, 30 Jul 2025 14:45:41 +0200
From: Nam Cao <namcao@...utronix.de>
To: Steven Rostedt <rostedt@...dmis.org>,
Masami Hiramatsu <mhiramat@...nel.org>,
Mathieu Desnoyers <mathieu.desnoyers@...icios.com>,
Gabriele Monaco <gmonaco@...hat.com>,
linux-trace-kernel@...r.kernel.org,
linux-kernel@...r.kernel.org
Cc: Nam Cao <namcao@...utronix.de>
Subject: [PATCH 3/5] verification/rvgen/ltl: Support per-cpu monitor generation
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@...utronix.de>
---
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..0fd3f9963a87 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 LTL_TASK_MONITOR"
+ if self.monitor_type == "per_cpu":
+ return "#define LTL_MONITOR_TYPE LTL_CPU_MONITOR"
+ 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_IMPLICIT"
+ 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"
+ 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
Powered by blists - more mailing lists