* [for-next][PATCH 1/9] verification/dot2k: Make a separate dot2k_templates/Kconfig_container
2025-07-10 0:34 [for-next][PATCH 0/9] tracing/tools: rv: Updates for v6.17 Steven Rostedt
@ 2025-07-10 0:34 ` Steven Rostedt
2025-07-10 0:34 ` [for-next][PATCH 2/9] verification/dot2k: Remove __buff_to_string() Steven Rostedt
` (7 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Steven Rostedt @ 2025-07-10 0:34 UTC (permalink / raw)
To: linux-kernel
Cc: Tomas Glozar, John Kacur, Masami Hiramatsu, Mathieu Desnoyers,
Gabriele Monaco, Nam Cao
From: Nam Cao <namcao@linutronix.de>
A generated container's Kconfig has an incorrect line:
select DA_MON_EVENTS_IMPLICIT
This is due to container generation uses the same template Kconfig file as
deterministic automaton monitor.
Therefore, make a separate Kconfig template for container which has only
the necessaries for container.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/d54fd7ee120785bec5695220e837dbbd6efb30e5.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
---
tools/verification/dot2/dot2k.py | 3 ++-
tools/verification/dot2/dot2k_templates/Kconfig_container | 5 +++++
2 files changed, 7 insertions(+), 1 deletion(-)
create mode 100644 tools/verification/dot2/dot2k_templates/Kconfig_container
diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/dot2/dot2k.py
index 745d35a4a379..dd4b5528a4f2 100644
--- a/tools/verification/dot2/dot2k.py
+++ b/tools/verification/dot2/dot2k.py
@@ -35,6 +35,7 @@ class dot2k(Dot2c):
self.states = []
self.main_c = self.__read_file(self.monitor_templates_dir + "main_container.c")
self.main_h = self.__read_file(self.monitor_templates_dir + "main_container.h")
+ self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig_container")
else:
super().__init__(file_path, extra_params.get("model_name"))
@@ -44,7 +45,7 @@ class dot2k(Dot2c):
self.monitor_type = MonitorType
self.main_c = self.__read_file(self.monitor_templates_dir + "main.c")
self.trace_h = self.__read_file(self.monitor_templates_dir + "trace.h")
- self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig")
+ self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig")
self.enum_suffix = "_%s" % self.name
self.description = extra_params.get("description", self.name) or "auto-generated"
self.auto_patch = extra_params.get("auto_patch")
diff --git a/tools/verification/dot2/dot2k_templates/Kconfig_container b/tools/verification/dot2/dot2k_templates/Kconfig_container
new file mode 100644
index 000000000000..a606111949c2
--- /dev/null
+++ b/tools/verification/dot2/dot2k_templates/Kconfig_container
@@ -0,0 +1,5 @@
+config RV_MON_%%MODEL_NAME_UP%%
+ depends on RV
+ bool "%%MODEL_NAME%% monitor"
+ help
+ %%DESCRIPTION%%
--
2.47.2
^ permalink raw reply related [flat|nested] 10+ messages in thread* [for-next][PATCH 2/9] verification/dot2k: Remove __buff_to_string()
2025-07-10 0:34 [for-next][PATCH 0/9] tracing/tools: rv: Updates for v6.17 Steven Rostedt
2025-07-10 0:34 ` [for-next][PATCH 1/9] verification/dot2k: Make a separate dot2k_templates/Kconfig_container Steven Rostedt
@ 2025-07-10 0:34 ` Steven Rostedt
2025-07-10 0:34 ` [for-next][PATCH 3/9] verification/dot2k: Replace is_container() hack with subparsers Steven Rostedt
` (6 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Steven Rostedt @ 2025-07-10 0:34 UTC (permalink / raw)
To: linux-kernel
Cc: Tomas Glozar, John Kacur, Masami Hiramatsu, Mathieu Desnoyers,
Gabriele Monaco, Nam Cao
From: Nam Cao <namcao@linutronix.de>
str.join() can do what __buff_to_string() does. Therefore replace
__buff_to_string() to make the scripts more pythonic.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/860d6002659f604c743e0f23d5cf3c99ea6a82d8.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
---
tools/verification/dot2/dot2k.py | 21 ++++++---------------
1 file changed, 6 insertions(+), 15 deletions(-)
diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/dot2/dot2k.py
index dd4b5528a4f2..0922754454b9 100644
--- a/tools/verification/dot2/dot2k.py
+++ b/tools/verification/dot2/dot2k.py
@@ -109,15 +109,6 @@ class dot2k(Dot2c):
fd.close()
return content
- def __buff_to_string(self, buff):
- string = ""
-
- for line in buff:
- string = string + line + "\n"
-
- # cut off the last \n
- return string[:-1]
-
def fill_monitor_type(self):
return self.monitor_type.upper()
@@ -148,19 +139,19 @@ class dot2k(Dot2c):
buff.append("\tda_%s_%s(%s%s);" % (handle, self.name, event, self.enum_suffix));
buff.append("}")
buff.append("")
- return self.__buff_to_string(buff)
+ return '\n'.join(buff)
def fill_tracepoint_attach_probe(self):
buff = []
for event in self.events:
buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event))
- return self.__buff_to_string(buff)
+ return '\n'.join(buff)
def fill_tracepoint_detach_helper(self):
buff = []
for event in self.events:
buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event))
- return self.__buff_to_string(buff)
+ return '\n'.join(buff)
def fill_main_c(self):
main_c = self.main_c
@@ -210,7 +201,7 @@ class dot2k(Dot2c):
buff = self.fill_model_h_header()
buff += self.format_model()
- return self.__buff_to_string(buff)
+ return '\n'.join(buff)
def fill_monitor_class_type(self):
if self.monitor_type == "per_task":
@@ -242,7 +233,7 @@ class dot2k(Dot2c):
tp_args_c = ", ".join([b for a,b in tp_args])
buff.append(" TP_PROTO(%s)," % tp_proto_c)
buff.append(" TP_ARGS(%s)" % tp_args_c)
- return self.__buff_to_string(buff)
+ return '\n'.join(buff)
def fill_monitor_deps(self):
buff = []
@@ -250,7 +241,7 @@ class dot2k(Dot2c):
if self.parent:
buff.append(" depends on RV_MON_%s" % self.parent.upper())
buff.append(" default y")
- return self.__buff_to_string(buff)
+ return '\n'.join(buff)
def fill_trace_h(self):
trace_h = self.trace_h
--
2.47.2
^ permalink raw reply related [flat|nested] 10+ messages in thread* [for-next][PATCH 3/9] verification/dot2k: Replace is_container() hack with subparsers
2025-07-10 0:34 [for-next][PATCH 0/9] tracing/tools: rv: Updates for v6.17 Steven Rostedt
2025-07-10 0:34 ` [for-next][PATCH 1/9] verification/dot2k: Make a separate dot2k_templates/Kconfig_container Steven Rostedt
2025-07-10 0:34 ` [for-next][PATCH 2/9] verification/dot2k: Remove __buff_to_string() Steven Rostedt
@ 2025-07-10 0:34 ` Steven Rostedt
2025-07-10 0:34 ` [for-next][PATCH 4/9] verification/dot2k: Prepare the frontend for LTL inclusion Steven Rostedt
` (5 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Steven Rostedt @ 2025-07-10 0:34 UTC (permalink / raw)
To: linux-kernel
Cc: Tomas Glozar, John Kacur, Masami Hiramatsu, Mathieu Desnoyers,
Gabriele Monaco, Nam Cao
From: Nam Cao <namcao@linutronix.de>
dot2k is used for both generating deterministic automaton (DA) monitor and
generating container monitor.
Generating DA monitor and generating container requires different
parameters. This is implemented by peeking at sys.argv and check whether
"--container" is specified, and use that information to make some
parameters optional or required.
This works, but is quite hacky and ugly.
Replace this hack with Python's built-in subparsers.
The old commands:
python3 dot2/dot2k -d wip.dot -t per_cpu
python3 dot2/dot2k -n sched --container
are equivalent to the new commands:
python3 dot2/dot2k monitor -d wip.dot -t per_cpu
python3 dot2/dot2k container -n sched
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/23c4e3c6e10c39e86d8e6a289208dde407efc4a8.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
---
tools/verification/dot2/dot2k | 37 +++++++++++++++++---------------
tools/verification/dot2/dot2k.py | 2 +-
2 files changed, 21 insertions(+), 18 deletions(-)
diff --git a/tools/verification/dot2/dot2k b/tools/verification/dot2/dot2k
index 767064f415e7..133fb17d9d47 100644
--- a/tools/verification/dot2/dot2k
+++ b/tools/verification/dot2/dot2k
@@ -13,30 +13,33 @@ if __name__ == '__main__':
import argparse
import sys
- def is_container():
- """Should work even before parsing the arguments"""
- return "-c" in sys.argv or "--container" in sys.argv
-
parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor')
- parser.add_argument('-d', "--dot", dest="dot_file", required=not is_container())
- parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=not is_container(),
- help=f"Available options: {', '.join(dot2k.monitor_types.keys())}")
- parser.add_argument('-n', "--model_name", dest="model_name", required=is_container())
parser.add_argument("-D", "--description", dest="description", required=False)
parser.add_argument("-a", "--auto_patch", dest="auto_patch",
action="store_true", required=False,
help="Patch the kernel in place")
- parser.add_argument("-p", "--parent", dest="parent",
- required=False, help="Create a monitor nested to parent")
- parser.add_argument("-c", "--container", dest="container",
- action="store_true", required=False,
- help="Create an empty monitor to be used as a container")
+
+ subparsers = parser.add_subparsers(dest="subcmd", required=True)
+
+ monitor_parser = subparsers.add_parser("monitor")
+ monitor_parser.add_argument('-n', "--model_name", dest="model_name")
+ monitor_parser.add_argument("-p", "--parent", dest="parent",
+ required=False, help="Create a monitor nested to parent")
+ monitor_parser.add_argument('-d', "--dot", dest="dot_file")
+ monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
+ help=f"Available options: {', '.join(dot2k.monitor_types.keys())}")
+
+ container_parser = subparsers.add_parser("container")
+ container_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
+
params = parser.parse_args()
- if not is_container():
- print("Opening and parsing the dot file %s" % params.dot_file)
try:
- monitor=dot2k(params.dot_file, params.monitor_type, vars(params))
+ if params.subcmd == "monitor":
+ print("Opening and parsing the dot file %s" % params.dot_file)
+ monitor = dot2k(params.dot_file, params.monitor_type, vars(params))
+ else:
+ monitor = dot2k(None, None, vars(params))
except Exception as e:
print('Error: '+ str(e))
print("Sorry : :-(")
@@ -45,7 +48,7 @@ if __name__ == '__main__':
print("Writing the monitor into the directory %s" % monitor.name)
monitor.print_files()
print("Almost done, checklist")
- if not is_container():
+ if params.subcmd == "monitor":
print(" - Edit the %s/%s.c to add the instrumentation" % (monitor.name, monitor.name))
print(monitor.fill_tracepoint_tooltip())
print(monitor.fill_makefile_tooltip())
diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/dot2/dot2k.py
index 0922754454b9..9ec99e297012 100644
--- a/tools/verification/dot2/dot2k.py
+++ b/tools/verification/dot2/dot2k.py
@@ -19,7 +19,7 @@ class dot2k(Dot2c):
monitor_type = "per_cpu"
def __init__(self, file_path, MonitorType, extra_params={}):
- self.container = extra_params.get("container")
+ self.container = extra_params.get("subcmd") == "container"
self.parent = extra_params.get("parent")
self.__fill_rv_templates_dir()
--
2.47.2
^ permalink raw reply related [flat|nested] 10+ messages in thread* [for-next][PATCH 4/9] verification/dot2k: Prepare the frontend for LTL inclusion
2025-07-10 0:34 [for-next][PATCH 0/9] tracing/tools: rv: Updates for v6.17 Steven Rostedt
` (2 preceding siblings ...)
2025-07-10 0:34 ` [for-next][PATCH 3/9] verification/dot2k: Replace is_container() hack with subparsers Steven Rostedt
@ 2025-07-10 0:34 ` Steven Rostedt
2025-07-10 0:34 ` [for-next][PATCH 5/9] Documentation/rv: Prepare monitor synthesis document " Steven Rostedt
` (4 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Steven Rostedt @ 2025-07-10 0:34 UTC (permalink / raw)
To: linux-kernel
Cc: Tomas Glozar, John Kacur, Masami Hiramatsu, Mathieu Desnoyers,
Gabriele Monaco, Nam Cao
From: Nam Cao <namcao@linutronix.de>
The dot2k tool has some code that can be reused for linear temporal logic
monitor. Prepare its frontend for LTL inclusion:
1. Rename to be generic: rvgen
2. Replace the parameter --dot with 2 parameters:
--class: to specific the monitor class, can be 'da' or 'ltl'
--spec: the monitor specification file, .dot file for DA, and .ltl
file for LTL
The old command:
python3 dot2/dot2k monitor -d wip.dot -t per_cpu
is equivalent to the new commands:
python3 rvgen monitor -c da -s wip.dot -t per_cpu
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/dea18f7a44374e4db8df5c7e785604bc3062ffc9.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
---
tools/verification/{dot2 => rvgen}/Makefile | 10 +++++-----
.../{dot2/dot2k => rvgen/__main__.py} | 18 +++++++++++++-----
tools/verification/{dot2 => rvgen}/dot2c | 2 +-
.../{dot2 => rvgen}/dot2k_templates/Kconfig | 0
.../dot2k_templates/Kconfig_container | 0
.../{dot2 => rvgen}/dot2k_templates/main.c | 0
.../dot2k_templates/main_container.c | 0
.../dot2k_templates/main_container.h | 0
.../{dot2 => rvgen}/dot2k_templates/trace.h | 0
.../{dot2 => rvgen/rvgen}/automata.py | 0
.../{dot2 => rvgen/rvgen}/dot2c.py | 2 +-
.../{dot2 => rvgen/rvgen}/dot2k.py | 10 +++++-----
12 files changed, 25 insertions(+), 17 deletions(-)
rename tools/verification/{dot2 => rvgen}/Makefile (55%)
rename tools/verification/{dot2/dot2k => rvgen/__main__.py} (72%)
rename tools/verification/{dot2 => rvgen}/dot2c (97%)
rename tools/verification/{dot2 => rvgen}/dot2k_templates/Kconfig (100%)
rename tools/verification/{dot2 => rvgen}/dot2k_templates/Kconfig_container (100%)
rename tools/verification/{dot2 => rvgen}/dot2k_templates/main.c (100%)
rename tools/verification/{dot2 => rvgen}/dot2k_templates/main_container.c (100%)
rename tools/verification/{dot2 => rvgen}/dot2k_templates/main_container.h (100%)
rename tools/verification/{dot2 => rvgen}/dot2k_templates/trace.h (100%)
rename tools/verification/{dot2 => rvgen/rvgen}/automata.py (100%)
rename tools/verification/{dot2 => rvgen/rvgen}/dot2c.py (99%)
rename tools/verification/{dot2 => rvgen/rvgen}/dot2k.py (98%)
diff --git a/tools/verification/dot2/Makefile b/tools/verification/rvgen/Makefile
similarity index 55%
rename from tools/verification/dot2/Makefile
rename to tools/verification/rvgen/Makefile
index 021beb07a521..cea9c21c3bce 100644
--- a/tools/verification/dot2/Makefile
+++ b/tools/verification/rvgen/Makefile
@@ -3,7 +3,7 @@ INSTALL=install
prefix ?= /usr
bindir ?= $(prefix)/bin
mandir ?= $(prefix)/share/man
-miscdir ?= $(prefix)/share/dot2
+miscdir ?= $(prefix)/share/rvgen
srcdir ?= $(prefix)/src
PYLIB ?= $(shell python3 -c 'import sysconfig; print (sysconfig.get_path("purelib"))')
@@ -16,11 +16,11 @@ clean:
.PHONY: install
install:
- $(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py
- $(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py
+ $(INSTALL) rvgen/automata.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/automata.py
+ $(INSTALL) rvgen/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2c.py
$(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/
- $(INSTALL) dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py
- $(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/
+ $(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py
+ $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen
mkdir -p ${miscdir}/
cp -rp dot2k_templates $(DESTDIR)$(miscdir)/
diff --git a/tools/verification/dot2/dot2k b/tools/verification/rvgen/__main__.py
similarity index 72%
rename from tools/verification/dot2/dot2k
rename to tools/verification/rvgen/__main__.py
index 133fb17d9d47..994d320ad2d1 100644
--- a/tools/verification/dot2/dot2k
+++ b/tools/verification/rvgen/__main__.py
@@ -9,11 +9,11 @@
# Documentation/trace/rv/da_monitor_synthesis.rst
if __name__ == '__main__':
- from dot2.dot2k import dot2k
+ from rvgen.dot2k import dot2k
import argparse
import sys
- parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor')
+ parser = argparse.ArgumentParser(description='Generate kernel rv monitor')
parser.add_argument("-D", "--description", dest="description", required=False)
parser.add_argument("-a", "--auto_patch", dest="auto_patch",
action="store_true", required=False,
@@ -25,7 +25,9 @@ if __name__ == '__main__':
monitor_parser.add_argument('-n', "--model_name", dest="model_name")
monitor_parser.add_argument("-p", "--parent", dest="parent",
required=False, help="Create a monitor nested to parent")
- monitor_parser.add_argument('-d', "--dot", dest="dot_file")
+ monitor_parser.add_argument('-c', "--class", dest="monitor_class",
+ help="Monitor class, either \"da\" or \"ltl\"")
+ monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor specification file")
monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
help=f"Available options: {', '.join(dot2k.monitor_types.keys())}")
@@ -36,8 +38,14 @@ if __name__ == '__main__':
try:
if params.subcmd == "monitor":
- print("Opening and parsing the dot file %s" % params.dot_file)
- monitor = dot2k(params.dot_file, params.monitor_type, vars(params))
+ print("Opening and parsing the specification file %s" % params.spec)
+ if params.monitor_class == "da":
+ monitor = dot2k(params.spec, params.monitor_type, vars(params))
+ elif params.monitor_class == "ltl":
+ raise NotImplementedError
+ else:
+ print("Unknown monitor class:", params.monitor_class)
+ sys.exit(1)
else:
monitor = dot2k(None, None, vars(params))
except Exception as e:
diff --git a/tools/verification/dot2/dot2c b/tools/verification/rvgen/dot2c
similarity index 97%
rename from tools/verification/dot2/dot2c
rename to tools/verification/rvgen/dot2c
index 3fe89ab88b65..bf0c67c5b66c 100644
--- a/tools/verification/dot2/dot2c
+++ b/tools/verification/rvgen/dot2c
@@ -14,7 +14,7 @@
# Documentation/trace/rv/deterministic_automata.rst
if __name__ == '__main__':
- from dot2 import dot2c
+ from rvgen import dot2c
import argparse
import sys
diff --git a/tools/verification/dot2/dot2k_templates/Kconfig b/tools/verification/rvgen/dot2k_templates/Kconfig
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/Kconfig
rename to tools/verification/rvgen/dot2k_templates/Kconfig
diff --git a/tools/verification/dot2/dot2k_templates/Kconfig_container b/tools/verification/rvgen/dot2k_templates/Kconfig_container
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/Kconfig_container
rename to tools/verification/rvgen/dot2k_templates/Kconfig_container
diff --git a/tools/verification/dot2/dot2k_templates/main.c b/tools/verification/rvgen/dot2k_templates/main.c
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/main.c
rename to tools/verification/rvgen/dot2k_templates/main.c
diff --git a/tools/verification/dot2/dot2k_templates/main_container.c b/tools/verification/rvgen/dot2k_templates/main_container.c
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/main_container.c
rename to tools/verification/rvgen/dot2k_templates/main_container.c
diff --git a/tools/verification/dot2/dot2k_templates/main_container.h b/tools/verification/rvgen/dot2k_templates/main_container.h
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/main_container.h
rename to tools/verification/rvgen/dot2k_templates/main_container.h
diff --git a/tools/verification/dot2/dot2k_templates/trace.h b/tools/verification/rvgen/dot2k_templates/trace.h
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/trace.h
rename to tools/verification/rvgen/dot2k_templates/trace.h
diff --git a/tools/verification/dot2/automata.py b/tools/verification/rvgen/rvgen/automata.py
similarity index 100%
rename from tools/verification/dot2/automata.py
rename to tools/verification/rvgen/rvgen/automata.py
diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
similarity index 99%
rename from tools/verification/dot2/dot2c.py
rename to tools/verification/rvgen/rvgen/dot2c.py
index fa2816ac7b61..6009caf568d9 100644
--- a/tools/verification/dot2/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -13,7 +13,7 @@
# For further information, see:
# Documentation/trace/rv/deterministic_automata.rst
-from dot2.automata import Automata
+from .automata import Automata
class Dot2c(Automata):
enum_suffix = ""
diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
similarity index 98%
rename from tools/verification/dot2/dot2k.py
rename to tools/verification/rvgen/rvgen/dot2k.py
index 9ec99e297012..e29462413194 100644
--- a/tools/verification/dot2/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -8,13 +8,13 @@
# For further information, see:
# Documentation/trace/rv/da_monitor_synthesis.rst
-from dot2.dot2c import Dot2c
+from .dot2c import Dot2c
import platform
import os
class dot2k(Dot2c):
monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 }
- monitor_templates_dir = "dot2/dot2k_templates/"
+ monitor_templates_dir = "rvgen/dot2k_templates/"
rv_dir = "kernel/trace/rv"
monitor_type = "per_cpu"
@@ -60,14 +60,14 @@ class dot2k(Dot2c):
if platform.system() != "Linux":
raise OSError("I can only run on Linux.")
- kernel_path = "/lib/modules/%s/build/tools/verification/dot2/dot2k_templates/" % (platform.release())
+ kernel_path = "/lib/modules/%s/build/tools/verification/rvgen/dot2k_templates/" % (platform.release())
if os.path.exists(kernel_path):
self.monitor_templates_dir = kernel_path
return
- if os.path.exists("/usr/share/dot2/dot2k_templates/"):
- self.monitor_templates_dir = "/usr/share/dot2/dot2k_templates/"
+ if os.path.exists("/usr/share/rvgen/dot2k_templates/"):
+ self.monitor_templates_dir = "/usr/share/rvgen/dot2k_templates/"
return
raise FileNotFoundError("Could not find the template directory, do you have the kernel source installed?")
--
2.47.2
^ permalink raw reply related [flat|nested] 10+ messages in thread* [for-next][PATCH 5/9] Documentation/rv: Prepare monitor synthesis document for LTL inclusion
2025-07-10 0:34 [for-next][PATCH 0/9] tracing/tools: rv: Updates for v6.17 Steven Rostedt
` (3 preceding siblings ...)
2025-07-10 0:34 ` [for-next][PATCH 4/9] verification/dot2k: Prepare the frontend for LTL inclusion Steven Rostedt
@ 2025-07-10 0:34 ` Steven Rostedt
2025-07-10 0:34 ` [for-next][PATCH 6/9] verification/rvgen: Restructure the templates files Steven Rostedt
` (3 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Steven Rostedt @ 2025-07-10 0:34 UTC (permalink / raw)
To: linux-kernel
Cc: Tomas Glozar, John Kacur, Masami Hiramatsu, Mathieu Desnoyers,
Gabriele Monaco, Nam Cao
From: Nam Cao <namcao@linutronix.de>
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.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/d91c6e4600287f4732d68a014219e576a75ce6dc.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
---
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..85624062073b 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
+======================================
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.
--
2.47.2
^ permalink raw reply related [flat|nested] 10+ messages in thread* [for-next][PATCH 6/9] verification/rvgen: Restructure the templates files
2025-07-10 0:34 [for-next][PATCH 0/9] tracing/tools: rv: Updates for v6.17 Steven Rostedt
` (4 preceding siblings ...)
2025-07-10 0:34 ` [for-next][PATCH 5/9] Documentation/rv: Prepare monitor synthesis document " Steven Rostedt
@ 2025-07-10 0:34 ` Steven Rostedt
2025-07-10 0:34 ` [for-next][PATCH 7/9] verification/rvgen: Restructure the classes to prepare for LTL inclusion Steven Rostedt
` (2 subsequent siblings)
8 siblings, 0 replies; 10+ messages in thread
From: Steven Rostedt @ 2025-07-10 0:34 UTC (permalink / raw)
To: linux-kernel
Cc: Tomas Glozar, John Kacur, Masami Hiramatsu, Mathieu Desnoyers,
Gabriele Monaco, Nam Cao
From: Nam Cao <namcao@linutronix.de>
To simply the scripts and to allow easy integration of new monitor types,
restructure the template files as followed:
1. Move the template files to be in the same directory as the rvgen
package. Furthermore, the installation will now only install the
templates to the package directory, not /usr/share/. This simplify
templates reading, as the scripts do not need to find the templates at
multiple places.
2. Move dot2k_templates/* to:
- templates/dot2k/
- templates/container/
This allows sharing templates reading code between DA monitor generation
and container generation (and any future generation type).
For template files which can be shared between different generation
types, support putting them in templates/
This restructure aligns with the recommendation from:
https://python-packaging.readthedocs.io/en/latest/non-code-files.html
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/462d90273f96804d3ba850474877d5f727031258.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
---
tools/verification/rvgen/Makefile | 5 +-
tools/verification/rvgen/rvgen/dot2k.py | 47 ++++++++-----------
.../templates}/Kconfig | 0
.../templates/container/Kconfig} | 0
.../templates/container/main.c} | 0
.../templates/container/main.h} | 0
.../templates/dot2k}/main.c | 0
.../templates/dot2k}/trace.h | 0
8 files changed, 20 insertions(+), 32 deletions(-)
rename tools/verification/rvgen/{dot2k_templates => rvgen/templates}/Kconfig (100%)
rename tools/verification/rvgen/{dot2k_templates/Kconfig_container => rvgen/templates/container/Kconfig} (100%)
rename tools/verification/rvgen/{dot2k_templates/main_container.c => rvgen/templates/container/main.c} (100%)
rename tools/verification/rvgen/{dot2k_templates/main_container.h => rvgen/templates/container/main.h} (100%)
rename tools/verification/rvgen/{dot2k_templates => rvgen/templates/dot2k}/main.c (100%)
rename tools/verification/rvgen/{dot2k_templates => rvgen/templates/dot2k}/trace.h (100%)
diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile
index cea9c21c3bce..8d08825e7e54 100644
--- a/tools/verification/rvgen/Makefile
+++ b/tools/verification/rvgen/Makefile
@@ -3,7 +3,6 @@ INSTALL=install
prefix ?= /usr
bindir ?= $(prefix)/bin
mandir ?= $(prefix)/share/man
-miscdir ?= $(prefix)/share/rvgen
srcdir ?= $(prefix)/src
PYLIB ?= $(shell python3 -c 'import sysconfig; print (sysconfig.get_path("purelib"))')
@@ -21,6 +20,4 @@ install:
$(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/
$(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py
$(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen
-
- mkdir -p ${miscdir}/
- cp -rp dot2k_templates $(DESTDIR)$(miscdir)/
+ cp -rp rvgen/templates $(DESTDIR)$(PYLIB)/rvgen/
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index e29462413194..a9ed97d0b224 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -14,14 +14,16 @@ import os
class dot2k(Dot2c):
monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 }
- monitor_templates_dir = "rvgen/dot2k_templates/"
rv_dir = "kernel/trace/rv"
monitor_type = "per_cpu"
def __init__(self, file_path, MonitorType, extra_params={}):
self.container = extra_params.get("subcmd") == "container"
self.parent = extra_params.get("parent")
- self.__fill_rv_templates_dir()
+ if self.container:
+ self.abs_template_dir = os.path.join(os.path.dirname(__file__), "templates/container")
+ else:
+ self.abs_template_dir = os.path.join(os.path.dirname(__file__), "templates/dot2k")
if self.container:
if file_path:
@@ -33,9 +35,7 @@ class dot2k(Dot2c):
self.name = extra_params.get("model_name")
self.events = []
self.states = []
- self.main_c = self.__read_file(self.monitor_templates_dir + "main_container.c")
- self.main_h = self.__read_file(self.monitor_templates_dir + "main_container.h")
- self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig_container")
+ self.main_h = self._read_template_file("main.h")
else:
super().__init__(file_path, extra_params.get("model_name"))
@@ -43,35 +43,16 @@ class dot2k(Dot2c):
if self.monitor_type is None:
raise ValueError("Unknown monitor type: %s" % MonitorType)
self.monitor_type = MonitorType
- self.main_c = self.__read_file(self.monitor_templates_dir + "main.c")
- self.trace_h = self.__read_file(self.monitor_templates_dir + "trace.h")
- self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig")
+ self.trace_h = self._read_template_file("trace.h")
+
+ self.main_c = self._read_template_file("main.c")
+ self.kconfig = self._read_template_file("Kconfig")
self.enum_suffix = "_%s" % self.name
self.description = extra_params.get("description", self.name) or "auto-generated"
self.auto_patch = extra_params.get("auto_patch")
if self.auto_patch:
self.__fill_rv_kernel_dir()
- def __fill_rv_templates_dir(self):
-
- if os.path.exists(self.monitor_templates_dir):
- return
-
- if platform.system() != "Linux":
- raise OSError("I can only run on Linux.")
-
- kernel_path = "/lib/modules/%s/build/tools/verification/rvgen/dot2k_templates/" % (platform.release())
-
- if os.path.exists(kernel_path):
- self.monitor_templates_dir = kernel_path
- return
-
- if os.path.exists("/usr/share/rvgen/dot2k_templates/"):
- self.monitor_templates_dir = "/usr/share/rvgen/dot2k_templates/"
- return
-
- raise FileNotFoundError("Could not find the template directory, do you have the kernel source installed?")
-
def __fill_rv_kernel_dir(self):
# first try if we are running in the kernel tree root
@@ -109,6 +90,16 @@ class dot2k(Dot2c):
fd.close()
return content
+ def _read_template_file(self, file):
+ try:
+ path = os.path.join(self.abs_template_dir, file)
+ return self.__read_file(path)
+ except Exception:
+ # Specific template file not found. Try the generic template file in the template/
+ # directory, which is one level up
+ path = os.path.join(self.abs_template_dir, "..", file)
+ return self.__read_file(path)
+
def fill_monitor_type(self):
return self.monitor_type.upper()
diff --git a/tools/verification/rvgen/dot2k_templates/Kconfig b/tools/verification/rvgen/rvgen/templates/Kconfig
similarity index 100%
rename from tools/verification/rvgen/dot2k_templates/Kconfig
rename to tools/verification/rvgen/rvgen/templates/Kconfig
diff --git a/tools/verification/rvgen/dot2k_templates/Kconfig_container b/tools/verification/rvgen/rvgen/templates/container/Kconfig
similarity index 100%
rename from tools/verification/rvgen/dot2k_templates/Kconfig_container
rename to tools/verification/rvgen/rvgen/templates/container/Kconfig
diff --git a/tools/verification/rvgen/dot2k_templates/main_container.c b/tools/verification/rvgen/rvgen/templates/container/main.c
similarity index 100%
rename from tools/verification/rvgen/dot2k_templates/main_container.c
rename to tools/verification/rvgen/rvgen/templates/container/main.c
diff --git a/tools/verification/rvgen/dot2k_templates/main_container.h b/tools/verification/rvgen/rvgen/templates/container/main.h
similarity index 100%
rename from tools/verification/rvgen/dot2k_templates/main_container.h
rename to tools/verification/rvgen/rvgen/templates/container/main.h
diff --git a/tools/verification/rvgen/dot2k_templates/main.c b/tools/verification/rvgen/rvgen/templates/dot2k/main.c
similarity index 100%
rename from tools/verification/rvgen/dot2k_templates/main.c
rename to tools/verification/rvgen/rvgen/templates/dot2k/main.c
diff --git a/tools/verification/rvgen/dot2k_templates/trace.h b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h
similarity index 100%
rename from tools/verification/rvgen/dot2k_templates/trace.h
rename to tools/verification/rvgen/rvgen/templates/dot2k/trace.h
--
2.47.2
^ permalink raw reply related [flat|nested] 10+ messages in thread* [for-next][PATCH 7/9] verification/rvgen: Restructure the classes to prepare for LTL inclusion
2025-07-10 0:34 [for-next][PATCH 0/9] tracing/tools: rv: Updates for v6.17 Steven Rostedt
` (5 preceding siblings ...)
2025-07-10 0:34 ` [for-next][PATCH 6/9] verification/rvgen: Restructure the templates files Steven Rostedt
@ 2025-07-10 0:34 ` Steven Rostedt
2025-07-10 0:34 ` [for-next][PATCH 8/9] verification/rvgen: Add support for linear temporal logic Steven Rostedt
2025-07-10 0:34 ` [for-next][PATCH 9/9] Documentation/rv: Add documentation for linear temporal logic monitors Steven Rostedt
8 siblings, 0 replies; 10+ messages in thread
From: Steven Rostedt @ 2025-07-10 0:34 UTC (permalink / raw)
To: linux-kernel
Cc: Tomas Glozar, John Kacur, Masami Hiramatsu, Mathieu Desnoyers,
Gabriele Monaco, Nam Cao
From: Nam Cao <namcao@linutronix.de>
Both container generation and DA monitor generation is implemented in the
class dot2k. That requires some ugly "if is_container ... else ...". If
linear temporal logic support is added at the current state, the "if else"
chain is longer and uglier.
Furthermore, container generation is irrevelant to .dot files. It is
therefore illogical to be implemented in class "dot2k".
Clean it up, restructure the dot2k class into the following class
hierarchy:
(RVGenerator)
/\
/ \
/ \
/ \
/ \
(Container) (Monitor)
/\
/ \
/ \
/ \
(dot2k) [ltl2k] <- intended
This allows a simple and clean integration of LTL.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/692137a581ba6bee7a64d37fb7173ae137c47bbd.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
---
tools/verification/rvgen/Makefile | 2 +
tools/verification/rvgen/__main__.py | 6 +-
tools/verification/rvgen/rvgen/container.py | 22 ++
tools/verification/rvgen/rvgen/dot2k.py | 275 ++------------------
tools/verification/rvgen/rvgen/generator.py | 264 +++++++++++++++++++
5 files changed, 308 insertions(+), 261 deletions(-)
create mode 100644 tools/verification/rvgen/rvgen/container.py
create mode 100644 tools/verification/rvgen/rvgen/generator.py
diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile
index 8d08825e7e54..cca8c9ba82e8 100644
--- a/tools/verification/rvgen/Makefile
+++ b/tools/verification/rvgen/Makefile
@@ -19,5 +19,7 @@ install:
$(INSTALL) rvgen/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2c.py
$(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/
$(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py
+ $(INSTALL) rvgen/container.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/container.py
+ $(INSTALL) rvgen/generator.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/generator.py
$(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen
cp -rp rvgen/templates $(DESTDIR)$(PYLIB)/rvgen/
diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 994d320ad2d1..63ecf0c37034 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -10,6 +10,8 @@
if __name__ == '__main__':
from rvgen.dot2k import dot2k
+ from rvgen.generator import Monitor
+ from rvgen.container import Container
import argparse
import sys
@@ -29,7 +31,7 @@ if __name__ == '__main__':
help="Monitor class, either \"da\" or \"ltl\"")
monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor specification file")
monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
- help=f"Available options: {', '.join(dot2k.monitor_types.keys())}")
+ help=f"Available options: {', '.join(Monitor.monitor_types.keys())}")
container_parser = subparsers.add_parser("container")
container_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
@@ -47,7 +49,7 @@ if __name__ == '__main__':
print("Unknown monitor class:", params.monitor_class)
sys.exit(1)
else:
- monitor = dot2k(None, None, vars(params))
+ monitor = Container(vars(params))
except Exception as e:
print('Error: '+ str(e))
print("Sorry : :-(")
diff --git a/tools/verification/rvgen/rvgen/container.py b/tools/verification/rvgen/rvgen/container.py
new file mode 100644
index 000000000000..47d8ab2ad3ec
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/container.py
@@ -0,0 +1,22 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+#
+# Generator for runtime verification monitor container
+
+from . import generator
+
+
+class Container(generator.RVGenerator):
+ template_dir = "container"
+
+ def __init__(self, extra_params={}):
+ super().__init__(extra_params)
+ self.name = extra_params.get("model_name")
+ self.main_h = self._read_template_file("main.h")
+
+ def fill_model_h(self):
+ main_h = self.main_h
+ main_h = main_h.replace("%%MODEL_NAME%%", self.name)
+ return main_h
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index a9ed97d0b224..ed0a3c901106 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -9,108 +9,21 @@
# Documentation/trace/rv/da_monitor_synthesis.rst
from .dot2c import Dot2c
-import platform
-import os
+from .generator import Monitor
-class dot2k(Dot2c):
- monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 }
- rv_dir = "kernel/trace/rv"
- monitor_type = "per_cpu"
- def __init__(self, file_path, MonitorType, extra_params={}):
- self.container = extra_params.get("subcmd") == "container"
- self.parent = extra_params.get("parent")
- if self.container:
- self.abs_template_dir = os.path.join(os.path.dirname(__file__), "templates/container")
- else:
- self.abs_template_dir = os.path.join(os.path.dirname(__file__), "templates/dot2k")
-
- if self.container:
- if file_path:
- raise ValueError("A container does not require a dot file")
- if MonitorType:
- raise ValueError("A container does not require a monitor type")
- if self.parent:
- raise ValueError("A container cannot have a parent")
- self.name = extra_params.get("model_name")
- self.events = []
- self.states = []
- self.main_h = self._read_template_file("main.h")
- else:
- super().__init__(file_path, extra_params.get("model_name"))
+class dot2k(Monitor, Dot2c):
+ template_dir = "dot2k"
- self.monitor_type = self.monitor_types.get(MonitorType)
- if self.monitor_type is None:
- raise ValueError("Unknown monitor type: %s" % MonitorType)
- self.monitor_type = MonitorType
- self.trace_h = self._read_template_file("trace.h")
-
- self.main_c = self._read_template_file("main.c")
- self.kconfig = self._read_template_file("Kconfig")
+ def __init__(self, file_path, MonitorType, extra_params={}):
+ self.monitor_type = MonitorType
+ Monitor.__init__(self, extra_params)
+ Dot2c.__init__(self, file_path, extra_params.get("model_name"))
self.enum_suffix = "_%s" % self.name
- self.description = extra_params.get("description", self.name) or "auto-generated"
- self.auto_patch = extra_params.get("auto_patch")
- if self.auto_patch:
- self.__fill_rv_kernel_dir()
-
- def __fill_rv_kernel_dir(self):
-
- # first try if we are running in the kernel tree root
- if os.path.exists(self.rv_dir):
- return
-
- # offset if we are running inside the kernel tree from verification/dot2
- kernel_path = os.path.join("../..", self.rv_dir)
-
- if os.path.exists(kernel_path):
- self.rv_dir = kernel_path
- return
-
- if platform.system() != "Linux":
- raise OSError("I can only run on Linux.")
-
- kernel_path = os.path.join("/lib/modules/%s/build" % platform.release(), self.rv_dir)
-
- # if the current kernel is from a distro this may not be a full kernel tree
- # verify that one of the files we are going to modify is available
- if os.path.exists(os.path.join(kernel_path, "rv_trace.h")):
- self.rv_dir = kernel_path
- return
-
- raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?")
-
- def __read_file(self, path):
- try:
- fd = open(path, 'r')
- except OSError:
- raise Exception("Cannot open the file: %s" % path)
-
- content = fd.read()
-
- fd.close()
- return content
-
- def _read_template_file(self, file):
- try:
- path = os.path.join(self.abs_template_dir, file)
- return self.__read_file(path)
- except Exception:
- # Specific template file not found. Try the generic template file in the template/
- # directory, which is one level up
- path = os.path.join(self.abs_template_dir, "..", file)
- return self.__read_file(path)
def fill_monitor_type(self):
return self.monitor_type.upper()
- def fill_parent(self):
- return "&rv_%s" % self.parent if self.parent else "NULL"
-
- def fill_include_parent(self):
- if self.parent:
- return "#include <monitors/%s/%s.h>\n" % (self.parent, self.parent)
- return ""
-
def fill_tracepoint_handlers_skel(self):
buff = []
for event in self.events:
@@ -144,30 +57,6 @@ class dot2k(Dot2c):
buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event))
return '\n'.join(buff)
- def fill_main_c(self):
- main_c = self.main_c
- monitor_type = self.fill_monitor_type()
- min_type = self.get_minimun_type()
- nr_events = len(self.events)
- tracepoint_handlers = self.fill_tracepoint_handlers_skel()
- tracepoint_attach = self.fill_tracepoint_attach_probe()
- tracepoint_detach = self.fill_tracepoint_detach_helper()
- parent = self.fill_parent()
- parent_include = self.fill_include_parent()
-
- main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type)
- main_c = main_c.replace("%%MIN_TYPE%%", min_type)
- main_c = main_c.replace("%%MODEL_NAME%%", self.name)
- main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events))
- main_c = main_c.replace("%%TRACEPOINT_HANDLERS_SKEL%%", tracepoint_handlers)
- main_c = main_c.replace("%%TRACEPOINT_ATTACH%%", tracepoint_attach)
- main_c = main_c.replace("%%TRACEPOINT_DETACH%%", tracepoint_detach)
- main_c = main_c.replace("%%DESCRIPTION%%", self.description)
- main_c = main_c.replace("%%PARENT%%", parent)
- main_c = main_c.replace("%%INCLUDE_PARENT%%", parent_include)
-
- return main_c
-
def fill_model_h_header(self):
buff = []
buff.append("/* SPDX-License-Identifier: GPL-2.0 */")
@@ -226,147 +115,15 @@ class dot2k(Dot2c):
buff.append(" TP_ARGS(%s)" % tp_args_c)
return '\n'.join(buff)
- def fill_monitor_deps(self):
- buff = []
- buff.append(" # XXX: add dependencies if there")
- if self.parent:
- buff.append(" depends on RV_MON_%s" % self.parent.upper())
- buff.append(" default y")
- return '\n'.join(buff)
-
- def fill_trace_h(self):
- trace_h = self.trace_h
- monitor_class = self.fill_monitor_class()
- monitor_class_type = self.fill_monitor_class_type()
- tracepoint_args_skel_event = self.fill_tracepoint_args_skel("event")
- tracepoint_args_skel_error = self.fill_tracepoint_args_skel("error")
- trace_h = trace_h.replace("%%MODEL_NAME%%", self.name)
- trace_h = trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper())
- trace_h = trace_h.replace("%%MONITOR_CLASS%%", monitor_class)
- trace_h = trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type)
- trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", tracepoint_args_skel_event)
- trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", tracepoint_args_skel_error)
- return trace_h
-
- def fill_kconfig(self):
- kconfig = self.kconfig
- monitor_class_type = self.fill_monitor_class_type()
- monitor_deps = self.fill_monitor_deps()
- kconfig = kconfig.replace("%%MODEL_NAME%%", self.name)
- kconfig = kconfig.replace("%%MODEL_NAME_UP%%", self.name.upper())
- kconfig = kconfig.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type)
- kconfig = kconfig.replace("%%DESCRIPTION%%", self.description)
- kconfig = kconfig.replace("%%MONITOR_DEPS%%", monitor_deps)
- return kconfig
-
- def fill_main_container_h(self):
- main_h = self.main_h
- main_h = main_h.replace("%%MODEL_NAME%%", self.name)
- return main_h
-
- def __patch_file(self, file, marker, line):
- file_to_patch = os.path.join(self.rv_dir, file)
- content = self.__read_file(file_to_patch)
- content = content.replace(marker, line + "\n" + marker)
- self.__write_file(file_to_patch, content)
-
- def fill_tracepoint_tooltip(self):
- monitor_class_type = self.fill_monitor_class_type()
- if self.auto_patch:
- self.__patch_file("rv_trace.h",
- "// Add new monitors based on CONFIG_%s here" % monitor_class_type,
- "#include <monitors/%s/%s_trace.h>" % (self.name, self.name))
- return " - Patching %s/rv_trace.h, double check the result" % self.rv_dir
-
- return """ - Edit %s/rv_trace.h:
-Add this line where other tracepoints are included and %s is defined:
-#include <monitors/%s/%s_trace.h>
-""" % (self.rv_dir, monitor_class_type, self.name, self.name)
-
- def fill_kconfig_tooltip(self):
- if self.auto_patch:
- self.__patch_file("Kconfig",
- "# Add new monitors here",
- "source \"kernel/trace/rv/monitors/%s/Kconfig\"" % (self.name))
- return " - Patching %s/Kconfig, double check the result" % self.rv_dir
-
- return """ - Edit %s/Kconfig:
-Add this line where other monitors are included:
-source \"kernel/trace/rv/monitors/%s/Kconfig\"
-""" % (self.rv_dir, self.name)
-
- def fill_makefile_tooltip(self):
- name = self.name
- name_up = name.upper()
- if self.auto_patch:
- self.__patch_file("Makefile",
- "# Add new monitors here",
- "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" % (name_up, name, name))
- return " - Patching %s/Makefile, double check the result" % self.rv_dir
-
- return """ - Edit %s/Makefile:
-Add this line where other monitors are included:
-obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
-""" % (self.rv_dir, name_up, name, name)
-
- def fill_monitor_tooltip(self):
- if self.auto_patch:
- return " - Monitor created in %s/monitors/%s" % (self.rv_dir, self. name)
- return " - Move %s/ to the kernel's monitor directory (%s/monitors)" % (self.name, self.rv_dir)
-
- def __create_directory(self):
- path = self.name
- if self.auto_patch:
- path = os.path.join(self.rv_dir, "monitors", path)
- try:
- os.mkdir(path)
- except FileExistsError:
- return
- except:
- print("Fail creating the output dir: %s" % self.name)
-
- def __write_file(self, file_name, content):
- try:
- file = open(file_name, 'w')
- except:
- print("Fail writing to file: %s" % file_name)
-
- file.write(content)
-
- file.close()
-
- def __create_file(self, file_name, content):
- path = "%s/%s" % (self.name, file_name)
- if self.auto_patch:
- path = os.path.join(self.rv_dir, "monitors", path)
- self.__write_file(path, content)
-
- def __get_main_name(self):
- path = "%s/%s" % (self.name, "main.c")
- if not os.path.exists(path):
- return "main.c"
- return "__main.c"
-
- def print_files(self):
- main_c = self.fill_main_c()
-
- self.__create_directory()
-
- path = "%s.c" % self.name
- self.__create_file(path, main_c)
+ def fill_main_c(self):
+ main_c = super().fill_main_c()
- if self.container:
- main_h = self.fill_main_container_h()
- path = "%s.h" % self.name
- self.__create_file(path, main_h)
- else:
- model_h = self.fill_model_h()
- path = "%s.h" % self.name
- self.__create_file(path, model_h)
+ min_type = self.get_minimun_type()
+ nr_events = len(self.events)
+ monitor_type = self.fill_monitor_type()
- trace_h = self.fill_trace_h()
- path = "%s_trace.h" % self.name
- self.__create_file(path, trace_h)
+ main_c = main_c.replace("%%MIN_TYPE%%", min_type)
+ main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events))
+ main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type)
- kconfig = self.fill_kconfig()
- self.__create_file("Kconfig", kconfig)
+ return main_c
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
new file mode 100644
index 000000000000..19d0078a3803
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -0,0 +1,264 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+#
+# Abtract class for generating kernel runtime verification monitors from specification file
+
+import platform
+import os
+
+
+class RVGenerator:
+ rv_dir = "kernel/trace/rv"
+
+ def __init__(self, extra_params={}):
+ self.name = extra_params.get("model_name")
+ self.parent = extra_params.get("parent")
+ self.abs_template_dir = \
+ os.path.join(os.path.dirname(__file__), "templates", self.template_dir)
+ self.main_c = self._read_template_file("main.c")
+ self.kconfig = self._read_template_file("Kconfig")
+ self.description = extra_params.get("description", self.name) or "auto-generated"
+ self.auto_patch = extra_params.get("auto_patch")
+ if self.auto_patch:
+ self.__fill_rv_kernel_dir()
+
+ def __fill_rv_kernel_dir(self):
+
+ # first try if we are running in the kernel tree root
+ if os.path.exists(self.rv_dir):
+ return
+
+ # offset if we are running inside the kernel tree from verification/dot2
+ kernel_path = os.path.join("../..", self.rv_dir)
+
+ if os.path.exists(kernel_path):
+ self.rv_dir = kernel_path
+ return
+
+ if platform.system() != "Linux":
+ raise OSError("I can only run on Linux.")
+
+ kernel_path = os.path.join("/lib/modules/%s/build" % platform.release(), self.rv_dir)
+
+ # if the current kernel is from a distro this may not be a full kernel tree
+ # verify that one of the files we are going to modify is available
+ if os.path.exists(os.path.join(kernel_path, "rv_trace.h")):
+ self.rv_dir = kernel_path
+ return
+
+ raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?")
+
+ def _read_file(self, path):
+ try:
+ fd = open(path, 'r')
+ except OSError:
+ raise Exception("Cannot open the file: %s" % path)
+
+ content = fd.read()
+
+ fd.close()
+ return content
+
+ def _read_template_file(self, file):
+ try:
+ path = os.path.join(self.abs_template_dir, file)
+ return self._read_file(path)
+ except Exception:
+ # Specific template file not found. Try the generic template file in the template/
+ # directory, which is one level up
+ path = os.path.join(self.abs_template_dir, "..", file)
+ return self._read_file(path)
+
+ def fill_parent(self):
+ return "&rv_%s" % self.parent if self.parent else "NULL"
+
+ def fill_include_parent(self):
+ if self.parent:
+ return "#include <monitors/%s/%s.h>\n" % (self.parent, self.parent)
+ return ""
+
+ def fill_tracepoint_handlers_skel(self):
+ return "NotImplemented"
+
+ def fill_tracepoint_attach_probe(self):
+ return "NotImplemented"
+
+ def fill_tracepoint_detach_helper(self):
+ return "NotImplemented"
+
+ def fill_main_c(self):
+ main_c = self.main_c
+ tracepoint_handlers = self.fill_tracepoint_handlers_skel()
+ tracepoint_attach = self.fill_tracepoint_attach_probe()
+ tracepoint_detach = self.fill_tracepoint_detach_helper()
+ parent = self.fill_parent()
+ parent_include = self.fill_include_parent()
+
+ main_c = main_c.replace("%%MODEL_NAME%%", self.name)
+ main_c = main_c.replace("%%TRACEPOINT_HANDLERS_SKEL%%", tracepoint_handlers)
+ main_c = main_c.replace("%%TRACEPOINT_ATTACH%%", tracepoint_attach)
+ main_c = main_c.replace("%%TRACEPOINT_DETACH%%", tracepoint_detach)
+ main_c = main_c.replace("%%DESCRIPTION%%", self.description)
+ main_c = main_c.replace("%%PARENT%%", parent)
+ main_c = main_c.replace("%%INCLUDE_PARENT%%", parent_include)
+
+ return main_c
+
+ def fill_model_h(self):
+ return "NotImplemented"
+
+ def fill_monitor_class_type(self):
+ return "NotImplemented"
+
+ def fill_monitor_class(self):
+ return "NotImplemented"
+
+ def fill_tracepoint_args_skel(self, tp_type):
+ return "NotImplemented"
+
+ def fill_monitor_deps(self):
+ buff = []
+ buff.append(" # XXX: add dependencies if there")
+ if self.parent:
+ buff.append(" depends on RV_MON_%s" % self.parent.upper())
+ buff.append(" default y")
+ return '\n'.join(buff)
+
+ def fill_kconfig(self):
+ kconfig = self.kconfig
+ monitor_class_type = self.fill_monitor_class_type()
+ monitor_deps = self.fill_monitor_deps()
+ kconfig = kconfig.replace("%%MODEL_NAME%%", self.name)
+ kconfig = kconfig.replace("%%MODEL_NAME_UP%%", self.name.upper())
+ kconfig = kconfig.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type)
+ kconfig = kconfig.replace("%%DESCRIPTION%%", self.description)
+ kconfig = kconfig.replace("%%MONITOR_DEPS%%", monitor_deps)
+ return kconfig
+
+ def __patch_file(self, file, marker, line):
+ file_to_patch = os.path.join(self.rv_dir, file)
+ content = self._read_file(file_to_patch)
+ content = content.replace(marker, line + "\n" + marker)
+ self.__write_file(file_to_patch, content)
+
+ def fill_tracepoint_tooltip(self):
+ monitor_class_type = self.fill_monitor_class_type()
+ if self.auto_patch:
+ self.__patch_file("rv_trace.h",
+ "// Add new monitors based on CONFIG_%s here" % monitor_class_type,
+ "#include <monitors/%s/%s_trace.h>" % (self.name, self.name))
+ return " - Patching %s/rv_trace.h, double check the result" % self.rv_dir
+
+ return """ - Edit %s/rv_trace.h:
+Add this line where other tracepoints are included and %s is defined:
+#include <monitors/%s/%s_trace.h>
+""" % (self.rv_dir, monitor_class_type, self.name, self.name)
+
+ def fill_kconfig_tooltip(self):
+ if self.auto_patch:
+ self.__patch_file("Kconfig",
+ "# Add new monitors here",
+ "source \"kernel/trace/rv/monitors/%s/Kconfig\"" % (self.name))
+ return " - Patching %s/Kconfig, double check the result" % self.rv_dir
+
+ return """ - Edit %s/Kconfig:
+Add this line where other monitors are included:
+source \"kernel/trace/rv/monitors/%s/Kconfig\"
+""" % (self.rv_dir, self.name)
+
+ def fill_makefile_tooltip(self):
+ name = self.name
+ name_up = name.upper()
+ if self.auto_patch:
+ self.__patch_file("Makefile",
+ "# Add new monitors here",
+ "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" % (name_up, name, name))
+ return " - Patching %s/Makefile, double check the result" % self.rv_dir
+
+ return """ - Edit %s/Makefile:
+Add this line where other monitors are included:
+obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
+""" % (self.rv_dir, name_up, name, name)
+
+ def fill_monitor_tooltip(self):
+ if self.auto_patch:
+ return " - Monitor created in %s/monitors/%s" % (self.rv_dir, self. name)
+ return " - Move %s/ to the kernel's monitor directory (%s/monitors)" % (self.name, self.rv_dir)
+
+ def __create_directory(self):
+ path = self.name
+ if self.auto_patch:
+ path = os.path.join(self.rv_dir, "monitors", path)
+ try:
+ os.mkdir(path)
+ except FileExistsError:
+ return
+ except:
+ print("Fail creating the output dir: %s" % self.name)
+
+ def __write_file(self, file_name, content):
+ try:
+ file = open(file_name, 'w')
+ except:
+ print("Fail writing to file: %s" % file_name)
+
+ file.write(content)
+
+ file.close()
+
+ def _create_file(self, file_name, content):
+ path = "%s/%s" % (self.name, file_name)
+ if self.auto_patch:
+ path = os.path.join(self.rv_dir, "monitors", path)
+ self.__write_file(path, content)
+
+ def __get_main_name(self):
+ path = "%s/%s" % (self.name, "main.c")
+ if not os.path.exists(path):
+ return "main.c"
+ return "__main.c"
+
+ def print_files(self):
+ main_c = self.fill_main_c()
+
+ self.__create_directory()
+
+ path = "%s.c" % self.name
+ self._create_file(path, main_c)
+
+ model_h = self.fill_model_h()
+ path = "%s.h" % self.name
+ self._create_file(path, model_h)
+
+ kconfig = self.fill_kconfig()
+ self._create_file("Kconfig", kconfig)
+
+
+class Monitor(RVGenerator):
+ monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 }
+
+ def __init__(self, extra_params={}):
+ super().__init__(extra_params)
+ self.trace_h = self._read_template_file("trace.h")
+
+ def fill_trace_h(self):
+ trace_h = self.trace_h
+ monitor_class = self.fill_monitor_class()
+ monitor_class_type = self.fill_monitor_class_type()
+ tracepoint_args_skel_event = self.fill_tracepoint_args_skel("event")
+ tracepoint_args_skel_error = self.fill_tracepoint_args_skel("error")
+ trace_h = trace_h.replace("%%MODEL_NAME%%", self.name)
+ trace_h = trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper())
+ trace_h = trace_h.replace("%%MONITOR_CLASS%%", monitor_class)
+ trace_h = trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type)
+ trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", tracepoint_args_skel_event)
+ trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", tracepoint_args_skel_error)
+ return trace_h
+
+ def print_files(self):
+ super().print_files()
+ trace_h = self.fill_trace_h()
+ path = "%s_trace.h" % self.name
+ self._create_file(path, trace_h)
--
2.47.2
^ permalink raw reply related [flat|nested] 10+ messages in thread* [for-next][PATCH 8/9] verification/rvgen: Add support for linear temporal logic
2025-07-10 0:34 [for-next][PATCH 0/9] tracing/tools: rv: Updates for v6.17 Steven Rostedt
` (6 preceding siblings ...)
2025-07-10 0:34 ` [for-next][PATCH 7/9] verification/rvgen: Restructure the classes to prepare for LTL inclusion Steven Rostedt
@ 2025-07-10 0:34 ` Steven Rostedt
2025-07-10 0:34 ` [for-next][PATCH 9/9] Documentation/rv: Add documentation for linear temporal logic monitors Steven Rostedt
8 siblings, 0 replies; 10+ messages in thread
From: Steven Rostedt @ 2025-07-10 0:34 UTC (permalink / raw)
To: linux-kernel
Cc: Tomas Glozar, John Kacur, Masami Hiramatsu, Mathieu Desnoyers,
Gabriele Monaco, Nam Cao
From: Nam Cao <namcao@linutronix.de>
Add support for generating RV monitors from linear temporal logic, similar
to the generation of deterministic automaton monitors.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Cc: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/f3c63b363ff9c5af3302ba2b5d92a26a98700eaf.1751634289.git.namcao@linutronix.de
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
---
tools/verification/rvgen/.gitignore | 3 +
tools/verification/rvgen/Makefile | 2 +
tools/verification/rvgen/__main__.py | 3 +-
tools/verification/rvgen/rvgen/ltl2ba.py | 540 ++++++++++++++++++
tools/verification/rvgen/rvgen/ltl2k.py | 252 ++++++++
.../rvgen/rvgen/templates/ltl2k/main.c | 102 ++++
.../rvgen/rvgen/templates/ltl2k/trace.h | 14 +
7 files changed, 915 insertions(+), 1 deletion(-)
create mode 100644 tools/verification/rvgen/.gitignore
create mode 100644 tools/verification/rvgen/rvgen/ltl2ba.py
create mode 100644 tools/verification/rvgen/rvgen/ltl2k.py
create mode 100644 tools/verification/rvgen/rvgen/templates/ltl2k/main.c
create mode 100644 tools/verification/rvgen/rvgen/templates/ltl2k/trace.h
diff --git a/tools/verification/rvgen/.gitignore b/tools/verification/rvgen/.gitignore
new file mode 100644
index 000000000000..1e288a076560
--- /dev/null
+++ b/tools/verification/rvgen/.gitignore
@@ -0,0 +1,3 @@
+__pycache__/
+parser.out
+parsetab.py
diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile
index cca8c9ba82e8..cfc4056c1e87 100644
--- a/tools/verification/rvgen/Makefile
+++ b/tools/verification/rvgen/Makefile
@@ -21,5 +21,7 @@ install:
$(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py
$(INSTALL) rvgen/container.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/container.py
$(INSTALL) rvgen/generator.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/generator.py
+ $(INSTALL) rvgen/ltl2ba.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2ba.py
+ $(INSTALL) rvgen/ltl2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2k.py
$(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen
cp -rp rvgen/templates $(DESTDIR)$(PYLIB)/rvgen/
diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 63ecf0c37034..fa6fc1f4de2f 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -12,6 +12,7 @@ if __name__ == '__main__':
from rvgen.dot2k import dot2k
from rvgen.generator import Monitor
from rvgen.container import Container
+ from rvgen.ltl2k import ltl2k
import argparse
import sys
@@ -44,7 +45,7 @@ if __name__ == '__main__':
if params.monitor_class == "da":
monitor = dot2k(params.spec, params.monitor_type, vars(params))
elif params.monitor_class == "ltl":
- raise NotImplementedError
+ monitor = ltl2k(params.spec, params.monitor_type, vars(params))
else:
print("Unknown monitor class:", params.monitor_class)
sys.exit(1)
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
new file mode 100644
index 000000000000..d11840af7f5f
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -0,0 +1,540 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Implementation based on
+# Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996).
+# Simple On-the-fly Automatic Verification of Linear Temporal Logic.
+# https://doi.org/10.1007/978-0-387-34892-6_1
+# With extra optimizations
+
+from ply.lex import lex
+from ply.yacc import yacc
+
+# Grammar:
+# ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
+#
+# Operands (opd):
+# true, false, user-defined names
+#
+# Unary Operators (unop):
+# always
+# eventually
+# not
+#
+# Binary Operators (binop):
+# until
+# and
+# or
+# imply
+# equivalent
+
+tokens = (
+ 'AND',
+ 'OR',
+ 'IMPLY',
+ 'UNTIL',
+ 'ALWAYS',
+ 'EVENTUALLY',
+ 'VARIABLE',
+ 'LITERAL',
+ 'NOT',
+ 'LPAREN',
+ 'RPAREN',
+ 'ASSIGN',
+)
+
+t_AND = r'and'
+t_OR = r'or'
+t_IMPLY = r'imply'
+t_UNTIL = r'until'
+t_ALWAYS = r'always'
+t_EVENTUALLY = r'eventually'
+t_VARIABLE = r'[A-Z_0-9]+'
+t_LITERAL = r'true|false'
+t_NOT = r'not'
+t_LPAREN = r'\('
+t_RPAREN = r'\)'
+t_ASSIGN = r'='
+t_ignore_COMMENT = r'\#.*'
+t_ignore = ' \t\n'
+
+def t_error(t):
+ raise ValueError(f"Illegal character '{t.value[0]}'")
+
+lexer = lex()
+
+class GraphNode:
+ uid = 0
+
+ def __init__(self, incoming: set['GraphNode'], new, old, _next):
+ self.init = False
+ self.outgoing = set()
+ self.labels = set()
+ self.incoming = incoming.copy()
+ self.new = new.copy()
+ self.old = old.copy()
+ self.next = _next.copy()
+ self.id = GraphNode.uid
+ GraphNode.uid += 1
+
+ def expand(self, node_set):
+ if not self.new:
+ for nd in node_set:
+ if nd.old == self.old and nd.next == self.next:
+ nd.incoming |= self.incoming
+ return node_set
+
+ new_current_node = GraphNode({self}, self.next, set(), set())
+ return new_current_node.expand({self} | node_set)
+ n = self.new.pop()
+ return n.expand(self, node_set)
+
+ def __lt__(self, other):
+ return self.id < other.id
+
+class ASTNode:
+ uid = 1
+
+ def __init__(self, op):
+ self.op = op
+ self.id = ASTNode.uid
+ ASTNode.uid += 1
+
+ def __hash__(self):
+ return hash(self.op)
+
+ def __eq__(self, other):
+ return self is other
+
+ def __iter__(self):
+ yield self
+ yield from self.op
+
+ def negate(self):
+ self.op = self.op.negate()
+ return self
+
+ def expand(self, node, node_set):
+ return self.op.expand(self, node, node_set)
+
+ def __str__(self):
+ if isinstance(self.op, Literal):
+ return str(self.op.value)
+ if isinstance(self.op, Variable):
+ return self.op.name.lower()
+ return "val" + str(self.id)
+
+ def normalize(self):
+ # Get rid of:
+ # - ALWAYS
+ # - EVENTUALLY
+ # - IMPLY
+ # And move all the NOT to be inside
+ self.op = self.op.normalize()
+ return self
+
+class BinaryOp:
+ op_str = "not_supported"
+
+ def __init__(self, left: ASTNode, right: ASTNode):
+ self.left = left
+ self.right = right
+
+ def __hash__(self):
+ return hash((self.left, self.right))
+
+ def __iter__(self):
+ yield from self.left
+ yield from self.right
+
+ def normalize(self):
+ raise NotImplementedError
+
+ def negate(self):
+ raise NotImplementedError
+
+ def _is_temporal(self):
+ raise NotImplementedError
+
+ def is_temporal(self):
+ if self.left.op.is_temporal():
+ return True
+ if self.right.op.is_temporal():
+ return True
+ return self._is_temporal()
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ raise NotImplementedError
+
+class AndOp(BinaryOp):
+ op_str = '&&'
+
+ def normalize(self):
+ return self
+
+ def negate(self):
+ return OrOp(self.left.negate(), self.right.negate())
+
+ def _is_temporal(self):
+ return False
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ if not n.op.is_temporal():
+ node.old.add(n)
+ return node.expand(node_set)
+
+ tmp = GraphNode(node.incoming,
+ node.new | ({n.op.left, n.op.right} - node.old),
+ node.old | {n},
+ node.next)
+ return tmp.expand(node_set)
+
+class OrOp(BinaryOp):
+ op_str = '||'
+
+ def normalize(self):
+ return self
+
+ def negate(self):
+ return AndOp(self.left.negate(), self.right.negate())
+
+ def _is_temporal(self):
+ return False
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ if not n.op.is_temporal():
+ node.old |= {n}
+ return node.expand(node_set)
+
+ node1 = GraphNode(node.incoming,
+ node.new | ({n.op.left} - node.old),
+ node.old | {n},
+ node.next)
+ node2 = GraphNode(node.incoming,
+ node.new | ({n.op.right} - node.old),
+ node.old | {n},
+ node.next)
+ return node2.expand(node1.expand(node_set))
+
+class UntilOp(BinaryOp):
+ def normalize(self):
+ return self
+
+ def negate(self):
+ return VOp(self.left.negate(), self.right.negate())
+
+ def _is_temporal(self):
+ return True
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ node1 = GraphNode(node.incoming,
+ node.new | ({n.op.left} - node.old),
+ node.old | {n},
+ node.next | {n})
+ node2 = GraphNode(node.incoming,
+ node.new | ({n.op.right} - node.old),
+ node.old | {n},
+ node.next)
+ return node2.expand(node1.expand(node_set))
+
+class VOp(BinaryOp):
+ def normalize(self):
+ return self
+
+ def negate(self):
+ return UntilOp(self.left.negate(), self.right.negate())
+
+ def _is_temporal(self):
+ return True
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ node1 = GraphNode(node.incoming,
+ node.new | ({n.op.right} - node.old),
+ node.old | {n},
+ node.next | {n})
+ node2 = GraphNode(node.incoming,
+ node.new | ({n.op.left, n.op.right} - node.old),
+ node.old | {n},
+ node.next)
+ return node2.expand(node1.expand(node_set))
+
+class ImplyOp(BinaryOp):
+ def normalize(self):
+ # P -> Q === !P | Q
+ return OrOp(self.left.negate(), self.right)
+
+ def _is_temporal(self):
+ return False
+
+ def negate(self):
+ # !(P -> Q) === !(!P | Q) === P & !Q
+ return AndOp(self.left, self.right.negate())
+
+class UnaryOp:
+ def __init__(self, child: ASTNode):
+ self.child = child
+
+ def __iter__(self):
+ yield from self.child
+
+ def __hash__(self):
+ return hash(self.child)
+
+ def normalize(self):
+ raise NotImplementedError
+
+ def _is_temporal(self):
+ raise NotImplementedError
+
+ def is_temporal(self):
+ if self.child.op.is_temporal():
+ return True
+ return self._is_temporal()
+
+ def negate(self):
+ raise NotImplementedError
+
+class EventuallyOp(UnaryOp):
+ def __str__(self):
+ return "eventually " + str(self.child)
+
+ def normalize(self):
+ # <>F == true U F
+ return UntilOp(ASTNode(Literal(True)), self.child)
+
+ def _is_temporal(self):
+ return True
+
+ def negate(self):
+ # !<>F == [](!F)
+ return AlwaysOp(self.child.negate()).normalize()
+
+class AlwaysOp(UnaryOp):
+ def normalize(self):
+ # []F === !(true U !F) == false V F
+ new = ASTNode(Literal(False))
+ return VOp(new, self.child)
+
+ def _is_temporal(self):
+ return True
+
+ def negate(self):
+ # ![]F == <>(!F)
+ return EventuallyOp(self.child.negate()).normalize()
+
+class NotOp(UnaryOp):
+ def __str__(self):
+ return "!" + str(self.child)
+
+ def normalize(self):
+ return self.child.op.negate()
+
+ def negate(self):
+ return self.child.op
+
+ def _is_temporal(self):
+ return False
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ for f in node.old:
+ if n.op.child is f:
+ return node_set
+ node.old |= {n}
+ return node.expand(node_set)
+
+class Variable:
+ def __init__(self, name: str):
+ self.name = name
+
+ def __hash__(self):
+ return hash(self.name)
+
+ def __iter__(self):
+ yield from ()
+
+ def negate(self):
+ new = ASTNode(self)
+ return NotOp(new)
+
+ def normalize(self):
+ return self
+
+ def is_temporal(self):
+ return False
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ for f in node.old:
+ if isinstance(f, NotOp) and f.op.child is n:
+ return node_set
+ node.old |= {n}
+ return node.expand(node_set)
+
+class Literal:
+ def __init__(self, value: bool):
+ self.value = value
+
+ def __iter__(self):
+ yield from ()
+
+ def __hash__(self):
+ return hash(self.value)
+
+ def __str__(self):
+ if self.value:
+ return "true"
+ return "false"
+
+ def negate(self):
+ self.value = not self.value
+ return self
+
+ def normalize(self):
+ return self
+
+ def is_temporal(self):
+ return False
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ if not n.op.value:
+ return node_set
+ node.old |= {n}
+ return node.expand(node_set)
+
+def p_spec(p):
+ '''
+ spec : assign
+ | assign spec
+ '''
+ if len(p) == 3:
+ p[2].append(p[1])
+ p[0] = p[2]
+ else:
+ p[0] = [p[1]]
+
+def p_assign(p):
+ '''
+ assign : VARIABLE ASSIGN ltl
+ '''
+ p[0] = (p[1], p[3])
+
+def p_ltl(p):
+ '''
+ ltl : opd
+ | binop
+ | unop
+ '''
+ p[0] = p[1]
+
+def p_opd(p):
+ '''
+ opd : VARIABLE
+ | LITERAL
+ | LPAREN ltl RPAREN
+ '''
+ if p[1] == "true":
+ p[0] = ASTNode(Literal(True))
+ elif p[1] == "false":
+ p[0] = ASTNode(Literal(False))
+ elif p[1] == '(':
+ p[0] = p[2]
+ else:
+ p[0] = ASTNode(Variable(p[1]))
+
+def p_unop(p):
+ '''
+ unop : ALWAYS ltl
+ | EVENTUALLY ltl
+ | NOT ltl
+ '''
+ if p[1] == "always":
+ op = AlwaysOp(p[2])
+ elif p[1] == "eventually":
+ op = EventuallyOp(p[2])
+ elif p[1] == "not":
+ op = NotOp(p[2])
+ else:
+ raise ValueError(f"Invalid unary operator {p[1]}")
+
+ p[0] = ASTNode(op)
+
+def p_binop(p):
+ '''
+ binop : opd UNTIL ltl
+ | opd AND ltl
+ | opd OR ltl
+ | opd IMPLY ltl
+ '''
+ if p[2] == "and":
+ op = AndOp(p[1], p[3])
+ elif p[2] == "until":
+ op = UntilOp(p[1], p[3])
+ elif p[2] == "or":
+ op = OrOp(p[1], p[3])
+ elif p[2] == "imply":
+ op = ImplyOp(p[1], p[3])
+ else:
+ raise ValueError(f"Invalid binary operator {p[2]}")
+
+ p[0] = ASTNode(op)
+
+parser = yacc()
+
+def parse_ltl(s: str) -> ASTNode:
+ spec = parser.parse(s)
+
+ rule = None
+ subexpr = {}
+
+ for assign in spec:
+ if assign[0] == "RULE":
+ rule = assign[1]
+ else:
+ subexpr[assign[0]] = assign[1]
+
+ if rule is None:
+ raise ValueError("Please define your specification in the \"RULE = <LTL spec>\" format")
+
+ for node in rule:
+ if not isinstance(node.op, Variable):
+ continue
+ replace = subexpr.get(node.op.name)
+ if replace is not None:
+ node.op = replace.op
+
+ return rule
+
+def create_graph(s: str):
+ atoms = set()
+
+ ltl = parse_ltl(s)
+ for c in ltl:
+ c.normalize()
+ if isinstance(c.op, Variable):
+ atoms.add(c.op.name)
+
+ init = GraphNode(set(), set(), set(), set())
+ head = GraphNode({init}, {ltl}, set(), set())
+ graph = sorted(head.expand(set()))
+
+ for i, node in enumerate(graph):
+ # The id assignment during graph generation has gaps. Reassign them
+ node.id = i
+
+ for incoming in node.incoming:
+ if incoming is init:
+ node.init = True
+ else:
+ incoming.outgoing.add(node)
+ for o in node.old:
+ if not o.op.is_temporal():
+ node.labels.add(str(o))
+
+ return sorted(atoms), graph, ltl
diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
new file mode 100644
index 000000000000..92e713861d86
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -0,0 +1,252 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+
+from pathlib import Path
+from . import generator
+from . import ltl2ba
+
+COLUMN_LIMIT = 100
+
+def line_len(line: str) -> int:
+ tabs = line.count('\t')
+ return tabs * 7 + len(line)
+
+def break_long_line(line: str, indent='') -> list[str]:
+ result = []
+ while line_len(line) > COLUMN_LIMIT:
+ i = line[:COLUMN_LIMIT - line_len(line)].rfind(' ')
+ result.append(line[:i])
+ line = indent + line[i + 1:]
+ if line:
+ result.append(line)
+ return result
+
+def build_condition_string(node: ltl2ba.GraphNode):
+ if not node.labels:
+ return "(true)"
+
+ result = "("
+
+ first = True
+ for label in sorted(node.labels):
+ if not first:
+ result += " && "
+ result += label
+ first = False
+
+ result += ")"
+
+ return result
+
+def abbreviate_atoms(atoms: list[str]) -> list[str]:
+ def shorten(s: str) -> str:
+ skip = ["is", "by", "or", "and"]
+ return '_'.join([x[:2] for x in s.lower().split('_') if x not in skip])
+
+ abbrs = []
+ for atom in atoms:
+ for i in range(len(atom), -1, -1):
+ if sum(a.startswith(atom[:i]) for a in atoms) > 1:
+ break
+ share = atom[:i]
+ unique = atom[i:]
+ abbrs.append((shorten(share) + shorten(unique)))
+ return abbrs
+
+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")
+ super().__init__(extra_params)
+ with open(file_path) as f:
+ self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read())
+ self.atoms_abbr = abbreviate_atoms(self.atoms)
+ self.name = extra_params.get("model_name")
+ if not self.name:
+ self.name = Path(file_path).stem
+
+ def _fill_states(self) -> str:
+ buf = [
+ "enum ltl_buchi_state {",
+ ]
+
+ for node in self.ba:
+ buf.append("\tS%i," % node.id)
+ buf.append("\tRV_NUM_BA_STATES")
+ buf.append("};")
+ buf.append("static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);")
+ return buf
+
+ def _fill_atoms(self):
+ buf = ["enum ltl_atom {"]
+ for a in sorted(self.atoms):
+ buf.append("\tLTL_%s," % a)
+ buf.append("\tLTL_NUM_ATOM")
+ buf.append("};")
+ buf.append("static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);")
+ return buf
+
+ def _fill_atoms_to_string(self):
+ buf = [
+ "static const char *ltl_atom_str(enum ltl_atom atom)",
+ "{",
+ "\tstatic const char *const names[] = {"
+ ]
+
+ for name in self.atoms_abbr:
+ buf.append("\t\t\"%s\"," % name)
+
+ buf.extend([
+ "\t};",
+ "",
+ "\treturn names[atom];",
+ "}"
+ ])
+ return buf
+
+ def _fill_atom_values(self):
+ buf = []
+ for node in self.ltl:
+ if node.op.is_temporal():
+ continue
+
+ if isinstance(node.op, ltl2ba.Variable):
+ buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" % (node, node.op.name))
+ elif isinstance(node.op, ltl2ba.AndOp):
+ buf.append("\tbool %s = %s && %s;" % (node, node.op.left, node.op.right))
+ elif isinstance(node.op, ltl2ba.OrOp):
+ buf.append("\tbool %s = %s || %s;" % (node, node.op.left, node.op.right))
+ elif isinstance(node.op, ltl2ba.NotOp):
+ buf.append("\tbool %s = !%s;" % (node, node.op.child))
+ buf.reverse()
+
+ buf2 = []
+ for line in buf:
+ buf2.extend(break_long_line(line, "\t "))
+ return buf2
+
+ def _fill_transitions(self):
+ buf = [
+ "static void",
+ "ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)",
+ "{"
+ ]
+ buf.extend(self._fill_atom_values())
+ buf.extend([
+ "",
+ "\tswitch (state) {"
+ ])
+
+ for node in self.ba:
+ buf.append("\tcase S%i:" % node.id)
+
+ for o in sorted(node.outgoing):
+ line = "\t\tif "
+ indent = "\t\t "
+
+ line += build_condition_string(o)
+ lines = break_long_line(line, indent)
+ buf.extend(lines)
+
+ buf.append("\t\t\t__set_bit(S%i, next);" % o.id)
+ buf.append("\t\tbreak;")
+ buf.extend([
+ "\t}",
+ "}"
+ ])
+
+ return buf
+
+ def _fill_start(self):
+ buf = [
+ "static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)",
+ "{"
+ ]
+ buf.extend(self._fill_atom_values())
+ buf.append("")
+
+ for node in self.ba:
+ if not node.init:
+ continue
+
+ line = "\tif "
+ indent = "\t "
+
+ line += build_condition_string(node)
+ lines = break_long_line(line, indent)
+ buf.extend(lines)
+
+ buf.append("\t\t__set_bit(S%i, mon->states);" % node.id)
+ buf.append("}")
+ return buf
+
+ def fill_tracepoint_handlers_skel(self):
+ 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("}")
+ buff.append("")
+ return '\n'.join(buff)
+
+ def fill_tracepoint_attach_probe(self):
+ return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_example_event);" \
+ % self.name
+
+ def fill_tracepoint_detach_helper(self):
+ return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_sample_event);" \
+ % self.name
+
+ def fill_atoms_init(self):
+ buff = []
+ for a in self.atoms:
+ buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % a)
+ return '\n'.join(buff)
+
+ def fill_model_h(self):
+ buf = [
+ "/* SPDX-License-Identifier: GPL-2.0 */",
+ "",
+ "/*",
+ " * C implementation of Buchi automaton, automatically generated by",
+ " * tools/verification/rvgen from the linear temporal logic specification.",
+ " * For further information, see kernel documentation:",
+ " * Documentation/trace/rv/linear_temporal_logic.rst",
+ " */",
+ "",
+ "#include <linux/rv.h>",
+ "",
+ "#define MONITOR_NAME " + self.name,
+ ""
+ ]
+
+ buf.extend(self._fill_atoms())
+ buf.append('')
+
+ buf.extend(self._fill_atoms_to_string())
+ buf.append('')
+
+ buf.extend(self._fill_states())
+ buf.append('')
+
+ buf.extend(self._fill_start())
+ buf.append('')
+
+ buf.extend(self._fill_transitions())
+ buf.append('')
+
+ return '\n'.join(buf)
+
+ def fill_monitor_class_type(self):
+ return "LTL_MON_EVENTS_ID"
+
+ def fill_monitor_class(self):
+ return "ltl_monitor_id"
+
+ def fill_main_c(self):
+ main_c = super().fill_main_c()
+ main_c = main_c.replace("%%ATOMS_INIT%%", self.fill_atoms_init())
+
+ return main_c
diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c
new file mode 100644
index 000000000000..f85d076fbf78
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c
@@ -0,0 +1,102 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "%%MODEL_NAME%%"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+%%INCLUDE_PARENT%%
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "%%MODEL_NAME%%.h"
+#include <rv/ltl_monitor.h>
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+ /*
+ * This is called everytime the Buchi automaton is triggered.
+ *
+ * This function could be used to fetch the atomic propositions which
+ * are expensive to trace. It is possible only if the atomic proposition
+ * does not need to be updated at precise time.
+ *
+ * It is recommended to use tracepoints and ltl_atom_update() instead.
+ */
+}
+
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_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.
+ */
+%%ATOMS_INIT%%
+}
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ */
+%%TRACEPOINT_HANDLERS_SKEL%%
+static int enable_%%MODEL_NAME%%(void)
+{
+ int retval;
+
+ retval = ltl_monitor_init();
+ if (retval)
+ return retval;
+
+%%TRACEPOINT_ATTACH%%
+
+ return 0;
+}
+
+static void disable_%%MODEL_NAME%%(void)
+{
+%%TRACEPOINT_DETACH%%
+
+ ltl_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_%%MODEL_NAME%% = {
+ .name = "%%MODEL_NAME%%",
+ .description = "%%DESCRIPTION%%",
+ .enable = enable_%%MODEL_NAME%%,
+ .disable = disable_%%MODEL_NAME%%,
+};
+
+static int __init register_%%MODEL_NAME%%(void)
+{
+ return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%);
+}
+
+static void __exit unregister_%%MODEL_NAME%%(void)
+{
+ rv_unregister_monitor(&rv_%%MODEL_NAME%%);
+}
+
+module_init(register_%%MODEL_NAME%%);
+module_exit(unregister_%%MODEL_NAME%%);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR(/* TODO */);
+MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");
diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h
new file mode 100644
index 000000000000..49394c4b0f1c
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h
@@ -0,0 +1,14 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#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));
+DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%,
+ TP_PROTO(struct task_struct *task),
+ TP_ARGS(task));
+#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */
--
2.47.2
^ permalink raw reply related [flat|nested] 10+ messages in thread* [for-next][PATCH 9/9] Documentation/rv: Add documentation for linear temporal logic monitors
2025-07-10 0:34 [for-next][PATCH 0/9] tracing/tools: rv: Updates for v6.17 Steven Rostedt
` (7 preceding siblings ...)
2025-07-10 0:34 ` [for-next][PATCH 8/9] verification/rvgen: Add support for linear temporal logic Steven Rostedt
@ 2025-07-10 0:34 ` Steven Rostedt
8 siblings, 0 replies; 10+ messages in thread
From: Steven Rostedt @ 2025-07-10 0:34 UTC (permalink / raw)
To: linux-kernel
Cc: Tomas Glozar, John Kacur, Masami Hiramatsu, Mathieu Desnoyers,
Gabriele Monaco, Nam Cao
From: Nam Cao <namcao@linutronix.de>
Add documents describing linear temporal logic runtime verification
monitors and how to generate them using rvgen.
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Cc: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/be13719e66fd8da147d7c69d5365aa23c52b743f.1751634289.git.namcao@linutronix.de
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
---
Documentation/trace/rv/index.rst | 1 +
.../trace/rv/linear_temporal_logic.rst | 133 +++++++++++++++
Documentation/trace/rv/monitor_synthesis.rst | 156 ++++++++++++++++--
3 files changed, 274 insertions(+), 16 deletions(-)
create mode 100644 Documentation/trace/rv/linear_temporal_logic.rst
diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/index.rst
index 8e411b76ec82..2a27f6bc9429 100644
--- a/Documentation/trace/rv/index.rst
+++ b/Documentation/trace/rv/index.rst
@@ -8,6 +8,7 @@ Runtime Verification
runtime-verification.rst
deterministic_automata.rst
+ linear_temporal_logic.rst
monitor_synthesis.rst
da_monitor_instrumentation.rst
monitor_wip.rst
diff --git a/Documentation/trace/rv/linear_temporal_logic.rst b/Documentation/trace/rv/linear_temporal_logic.rst
new file mode 100644
index 000000000000..57f107fcf6dd
--- /dev/null
+++ b/Documentation/trace/rv/linear_temporal_logic.rst
@@ -0,0 +1,133 @@
+Linear temporal logic
+=====================
+
+Introduction
+------------
+
+Runtime verification monitor is a verification technique which checks that the
+kernel follows a specification. It does so by using tracepoints to monitor the
+kernel's execution trace, and verifying that the execution trace sastifies the
+specification.
+
+Initially, the specification can only be written in the form of deterministic
+automaton (DA). However, while attempting to implement DA monitors for some
+complex specifications, deterministic automaton is found to be inappropriate as
+the specification language. The automaton is complicated, hard to understand,
+and error-prone.
+
+Thus, RV monitors based on linear temporal logic (LTL) are introduced. This type
+of monitor uses LTL as specification instead of DA. For some cases, writing the
+specification as LTL is more concise and intuitive.
+
+Many materials explain LTL in details. One book is::
+
+ Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT
+ Press, 2008.
+
+Grammar
+-------
+
+Unlike some existing syntax, kernel's implementation of LTL is more verbose.
+This is motivated by considering that the people who read the LTL specifications
+may not be well-versed in LTL.
+
+Grammar:
+ ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
+
+Operands (opd):
+ true, false, user-defined names consisting of upper-case characters, digits,
+ and underscore.
+
+Unary Operators (unop):
+ always
+ eventually
+ not
+
+Binary Operators (binop):
+ until
+ and
+ or
+ imply
+ equivalent
+
+This grammar is ambiguous: operator precedence is not defined. Parentheses must
+be used.
+
+Example linear temporal logic
+-----------------------------
+.. code-block::
+
+ RAIN imply (GO_OUTSIDE imply HAVE_UMBRELLA)
+
+means: if it is raining, going outside means having an umbrella.
+
+.. code-block::
+
+ RAIN imply (WET until not RAIN)
+
+means: if it is raining, it is going to be wet until the rain stops.
+
+.. code-block::
+
+ RAIN imply eventually not RAIN
+
+means: if it is raining, rain will eventually stop.
+
+The above examples are referring to the current time instance only. For kernel
+verification, the `always` operator is usually desirable, to specify that
+something is always true at the present and for all future. For example::
+
+ always (RAIN imply eventually not RAIN)
+
+means: *all* rain eventually stops.
+
+In the above examples, `RAIN`, `GO_OUTSIDE`, `HAVE_UMBRELLA` and `WET` are the
+"atomic propositions".
+
+Monitor synthesis
+-----------------
+
+To synthesize an LTL into a kernel monitor, the `rvgen` tool can be used:
+`tools/verification/rvgen`. The specification needs to be provided as a file,
+and it must have a "RULE = LTL" assignment. For example::
+
+ RULE = always (ACQUIRE imply ((not KILLED and not CRASHED) until RELEASE))
+
+which says: if `ACQUIRE`, then `RELEASE` must happen before `KILLED` or
+`CRASHED`.
+
+The LTL can be broken down using sub-expressions. The above is equivalent to:
+
+ .. code-block::
+
+ RULE = always (ACQUIRE imply (ALIVE until RELEASE))
+ ALIVE = not KILLED and not CRASHED
+
+From this specification, `rvgen` generates the C implementation of a Buchi
+automaton - a non-deterministic state machine which checks the satisfiability of
+the LTL. See Documentation/trace/rv/monitor_synthesis.rst for details on using
+`rvgen`.
+
+References
+----------
+
+One book covering model checking and linear temporal logic is::
+
+ Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT
+ Press, 2008.
+
+For an example of using linear temporal logic in software testing, see::
+
+ Ruijie Meng, Zhen Dong, Jialin Li, Ivan Beschastnikh, and Abhik Roychoudhury.
+ 2022. Linear-time temporal logic guided greybox fuzzing. In Proceedings of the
+ 44th International Conference on Software Engineering (ICSE '22). Association
+ for Computing Machinery, New York, NY, USA, 1343–1355.
+ https://doi.org/10.1145/3510003.3510082
+
+The kernel's LTL monitor implementation is based on::
+
+ Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). Simple On-the-fly
+ Automatic Verification of Linear Temporal Logic. In: Dembiński, P., Średniawa,
+ M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP
+ Advances in Information and Communication Technology. Springer, Boston, MA.
+ https://doi.org/10.1007/978-0-387-34892-6_1
diff --git a/Documentation/trace/rv/monitor_synthesis.rst b/Documentation/trace/rv/monitor_synthesis.rst
index 85624062073b..ac808a7554f5 100644
--- a/Documentation/trace/rv/monitor_synthesis.rst
+++ b/Documentation/trace/rv/monitor_synthesis.rst
@@ -39,16 +39,18 @@ below::
RV monitor synthesis
--------------------
-The synthesis of automata-based models into the Linux *RV monitor* abstraction
-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.
+The synthesis of a specification into the Linux *RV monitor* abstraction is
+automated by the rvgen tool and the header file containing common code for
+creating monitors. The header files are:
+
+ * rv/da_monitor.h for deterministic automaton monitor.
+ * rv/ltl_monitor.h for linear temporal logic monitor.
rvgen
-----
-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.
+The rvgen utility converts a specification into the C presentation 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::
@@ -63,18 +65,38 @@ This will create a directory named wip/ with the following files:
The wip.c file contains the monitor declaration and the starting point for
the system instrumentation.
-Monitor macros
---------------
+Similarly, a linear temporal logic monitor can be generated with the following
+command::
+
+ $ rvgen monitor -c ltl -s pagefault.ltl -t per_task
+
+This generates pagefault/ directory with:
+
+- pagefault.h: The Buchi automaton (the non-deterministic state machine to
+ verify the specification)
+- pagefault.c: The skeleton for the RV monitor
+
+Monitor header files
+--------------------
+
+The header files:
+
+- `rv/da_monitor.h` for deterministic automaton monitor
+- `rv/ltl_monitor` for linear temporal logic monitor
+
+include common macros and static functions for implementing *Monitor
+Instance(s)*.
-The rv/da_monitor.h enables automatic code generation for the *Monitor
-Instance(s)* using C macros.
+The benefits of having all common functionalities in a single header file are
+3-fold:
-The benefits of the usage of macro for monitor synthesis are 3-fold as it:
+ - Reduce the code duplication;
+ - Facilitate the bug fix/improvement;
+ - Avoid the case of developers changing the core of the monitor code to
+ manipulate the model in a (let's say) non-standard way.
-- Reduces the code duplication;
-- Facilitates the bug fix/improvement;
-- Avoids the case of developers changing the core of the monitor code
- to manipulate the model in a (let's say) non-standard way.
+rv/da_monitor.h
++++++++++++++++
This initial implementation presents three different types of monitor instances:
@@ -130,10 +152,112 @@ While the event "preempt_enabled" will use::
To notify the monitor that the system will be returning to the initial state,
so the system and the monitor should be in sync.
+rv/ltl_monitor.h
+++++++++++++++++
+This file must be combined with the $(MODEL_NAME).h file (generated by `rvgen`)
+to be complete. For example, for the `pagefault` monitor, the `pagefault.c`
+source file must include::
+
+ #include "pagefault.h"
+ #include <rv/ltl_monitor.h>
+
+(the skeleton monitor file generated by `rvgen` already does this).
+
+`$(MODEL_NAME).h` (`pagefault.h` in the above example) includes the
+implementation of the Buchi automaton - a non-deterministic state machine that
+verifies the LTL specification. While `rv/ltl_monitor.h` includes the common
+helper functions to interact with the Buchi automaton and to implement an RV
+monitor. An important definition in `$(MODEL_NAME).h` is::
+
+ enum ltl_atom {
+ LTL_$(FIRST_ATOMIC_PROPOSITION),
+ LTL_$(SECOND_ATOMIC_PROPOSITION),
+ ...
+ LTL_NUM_ATOM
+ };
+
+which is the list of atomic propositions present in the LTL specification
+(prefixed with "LTL\_" to avoid name collision). This `enum` is passed to the
+functions interacting with the Buchi automaton.
+
+While generating code, `rvgen` cannot understand the meaning of the atomic
+propositions. Thus, that task is left for manual work. The recommended pratice
+is adding tracepoints to places where the atomic propositions change; and in the
+tracepoints' handlers: the Buchi automaton is executed using::
+
+ void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)
+
+which tells the Buchi automaton that the atomic proposition `atom` is now
+`value`. The Buchi automaton checks whether the LTL specification is still
+satisfied, and invokes the monitor's error tracepoint and the reactor if
+violation is detected.
+
+Tracepoints and `ltl_atom_update()` should be used whenever possible. However,
+it is sometimes not the most convenient. For some atomic propositions which are
+changed in multiple places in the kernel, it is cumbersome to trace all those
+places. Furthermore, it may not be important that the atomic propositions are
+updated at precise times. For example, considering the following linear temporal
+logic::
+
+ RULE = always (RT imply not PAGEFAULT)
+
+This LTL states that a real-time task does not raise page faults. For this
+specification, it is not important when `RT` changes, as long as it has the
+correct value when `PAGEFAULT` is true. Motivated by this case, another
+function is introduced::
+
+ void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon)
+
+This function is called whenever the Buchi automaton is triggered. Therefore, it
+can be manually implemented to "fetch" `RT`::
+
+ void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon)
+ {
+ ltl_atom_set(mon, LTL_RT, rt_task(task));
+ }
+
+Effectively, whenever `PAGEFAULT` is updated with a call to `ltl_atom_update()`,
+`RT` is also fetched. Thus, the LTL specification can be verified without
+tracing `RT` everywhere.
+
+For atomic propositions which act like events, they usually need to be set (or
+cleared) and then immediately cleared (or set). A convenient function is
+provided::
+
+ void ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)
+
+which is equivalent to::
+
+ ltl_atom_update(task, atom, value);
+ ltl_atom_update(task, atom, !value);
+
+To initialize the atomic propositions, the following function must be
+implemented::
+
+ ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+
+This function is called for all running tasks when the monitor is enabled. It is
+also called for new tasks created after the enabling the monitor. It should
+initialize as many atomic propositions as possible, for example::
+
+ void ltl_atom_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+ {
+ ltl_atom_set(mon, LTL_RT, rt_task(task));
+ if (task_creation)
+ ltl_atom_set(mon, LTL_PAGEFAULT, false);
+ }
+
+Atomic propositions not initialized by `ltl_atom_init()` will stay in the
+unknown state until relevant tracepoints are hit, which can take some time. As
+monitoring for a task cannot be done until all atomic propositions is known for
+the task, the monitor may need some time to start validating tasks which have
+been running before the monitor is enabled. Therefore, it is recommended to
+start the tasks of interest after enabling the monitor.
+
Final remarks
-------------
-With the monitor synthesis in place using the rv/da_monitor.h and
+With the monitor synthesis in place using the header files and
rvgen, the developer's work should be limited to the instrumentation
of the system, increasing the confidence in the overall approach.
--
2.47.2
^ permalink raw reply related [flat|nested] 10+ messages in thread