scftorture: Count single_rpc offline failures in statistics outputgrafted

scf_torture_stats_print() aggregates each invoker thread's counters
into a local scf_statistics structure before printing, but the
n_single_rpc_ofl field is missing from the aggregation loop.  As a
result, the "single_rpc_ofl" value printed in the statistics line is
always zero, even when smp_call_function_single() invocations for the
RPC test have failed due to offline CPUs and been counted by the
invoker threads.

Add the missing accumulation so that the printed value reflects the
actual counts.

Signed-off-by: Joel Fernandes <joelagnelf@nvidia.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

20 files changed, 2782 insertions, 0 deletions

diff --git a/tools/verification/rvgen/.gitignore b/tools/verification/rvgen/.gitignore
new file mode 100644
index 000000000..1e288a076
--- /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
new file mode 100644
index 000000000..cfc4056c1
--- /dev/null
+++ b/tools/verification/rvgen/Makefile
@@ -0,0 +1,27 @@
+INSTALL=install
+
+prefix  ?= /usr
+bindir  ?= $(prefix)/bin
+mandir  ?= $(prefix)/share/man
+srcdir  ?= $(prefix)/src
+
+PYLIB  ?= $(shell python3 -c 'import sysconfig;  print (sysconfig.get_path("purelib"))')
+
+.PHONY: all
+all:
+
+.PHONY: clean
+clean:
+
+.PHONY: install
+install:
+	$(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) 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
new file mode 100644
index 000000000..5c923dc10
--- /dev/null
+++ b/tools/verification/rvgen/__main__.py
@@ -0,0 +1,72 @@
+#!/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>
+#
+# dot2k: transform dot files into a monitor for the Linux kernel.
+#
+# For further information, see:
+#   Documentation/trace/rv/da_monitor_synthesis.rst
+
+if __name__ == '__main__':
+    from rvgen.dot2k import da2k, ha2k
+    from rvgen.generator import Monitor
+    from rvgen.container import Container
+    from rvgen.ltl2k import ltl2k
+    from rvgen.automata import AutomataError
+    import argparse
+    import sys
+
+    parser = argparse.ArgumentParser(description='Generate kernel rv monitor')
+
+    parent_parser = argparse.ArgumentParser(add_help=False)
+    parent_parser.add_argument("-D", "--description", dest="description", required=False)
+    parent_parser.add_argument("-a", "--auto_patch", dest="auto_patch",
+                        action="store_true", required=False,
+                        help="Patch the kernel in place")
+
+    subparsers = parser.add_subparsers(dest="subcmd", required=True)
+
+    monitor_parser = subparsers.add_parser("monitor", parents=[parent_parser])
+    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('-c', "--class", dest="monitor_class", required=True,
+                                help="Monitor class, either \"da\", \"ha\" or \"ltl\"")
+    monitor_parser.add_argument('-s', "--spec", dest="spec", required=True,
+                                help="Monitor specification file")
+    monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True,
+                                help=f"Available options: {', '.join(Monitor.monitor_types.keys())}")
+
+    container_parser = subparsers.add_parser("container", parents=[parent_parser])
+    container_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
+
+    params = parser.parse_args()
+
+    try:
+        if params.subcmd == "monitor":
+            print(f"Opening and parsing the specification file {params.spec}")
+            if params.monitor_class == "da":
+                monitor = da2k(params.spec, params.monitor_type, vars(params))
+            elif params.monitor_class == "ha":
+                monitor = ha2k(params.spec, params.monitor_type, vars(params))
+            elif params.monitor_class == "ltl":
+                monitor = ltl2k(params.spec, params.monitor_type, vars(params))
+            else:
+                print("Unknown monitor class:", params.monitor_class)
+                sys.exit(1)
+        else:
+            monitor = Container(vars(params))
+    except AutomataError as e:
+        print(f"There was an error processing {params.spec}: {e}", file=sys.stderr)
+        sys.exit(1)
+
+    print(f"Writing the monitor into the directory {monitor.name}")
+    monitor.print_files()
+    print("Almost done, checklist")
+    if params.subcmd == "monitor":
+        print(f"  - Edit the {monitor.name}/{monitor.name}.c to add the instrumentation")
+        print(monitor.fill_tracepoint_tooltip())
+    print(monitor.fill_makefile_tooltip())
+    print(monitor.fill_kconfig_tooltip())
+    print(monitor.fill_monitor_tooltip())
diff --git a/tools/verification/rvgen/dot2c b/tools/verification/rvgen/dot2c
new file mode 100644
index 000000000..1012becc7
--- /dev/null
+++ b/tools/verification/rvgen/dot2c
@@ -0,0 +1,25 @@
+#!/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>
+#
+# dot2c: parse an automata in dot file digraph format into a C
+#
+# This program was written in the development of this paper:
+#  de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
+#  "Efficient Formal Verification for the Linux Kernel." International
+#  Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# For further information, see:
+#   Documentation/trace/rv/deterministic_automata.rst
+
+if __name__ == '__main__':
+    from rvgen import dot2c
+    import argparse
+
+    parser = argparse.ArgumentParser(description='dot2c: converts a .dot file into a C structure')
+    parser.add_argument('dot_file',  help='The dot file to be converted')
+
+    args = parser.parse_args()
+    d = dot2c.Dot2c(args.dot_file)
+    d.print_model_classic()
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
new file mode 100644
index 000000000..b9f8149f7
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -0,0 +1,368 @@
+#!/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>
+#
+# Automata class: parse an automaton in dot file digraph format into a python object
+#
+# For further information, see:
+#   Documentation/trace/rv/deterministic_automata.rst
+
+import ntpath
+import re
+from typing import Iterator
+from itertools import islice
+
+class _ConstraintKey:
+    """Base class for constraint keys."""
+
+class _StateConstraintKey(_ConstraintKey, int):
+    """Key for a state constraint. Under the hood just state_id."""
+    def __new__(cls, state_id: int):
+        return super().__new__(cls, state_id)
+
+class _EventConstraintKey(_ConstraintKey, tuple):
+    """Key for an event constraint. Under the hood just tuple(state_id,event_id)."""
+    def __new__(cls, state_id: int, event_id: int):
+        return super().__new__(cls, (state_id, event_id))
+
+class AutomataError(Exception):
+    """Exception raised for errors in automata parsing and validation.
+
+    Raised when DOT file processing fails due to invalid format, I/O errors,
+    or malformed automaton definitions.
+    """
+
+class Automata:
+    """Automata class: Reads a dot file and parses it as an automaton.
+
+    It supports both deterministic and hybrid automata.
+
+    Attributes:
+        dot_file: A dot file with an state_automaton definition.
+    """
+
+    invalid_state_str = "INVALID_STATE"
+    init_marker = "__init_"
+    node_marker = "{node"
+    # val can be numerical, uppercase (constant or macro), lowercase (parameter or function)
+    # only numerical values should have units
+    constraint_rule = re.compile(r"""
+        ^
+        (?P<env>[a-zA-Z_][a-zA-Z0-9_]+)  # C-like identifier for the env var
+        (?P<op>[!<=>]{1,2})              # operator
+        (?P<val>
+            [0-9]+ |                     # numerical value
+            [A-Z_]+\(\) |                # macro
+            [A-Z_]+ |                    # constant
+            [a-z_]+\(\) |                # function
+            [a-z_]+                      # parameter
+        )
+        (?P<unit>[a-z]{1,2})?            # optional unit for numerical values
+        """, re.VERBOSE)
+    constraint_reset = re.compile(r"^reset\((?P<env>[a-zA-Z_][a-zA-Z0-9_]+)\)")
+
+    def __init__(self, file_path, model_name=None):
+        self.__dot_path = file_path
+        self.name = model_name or self.__get_model_name()
+        self.__dot_lines = self.__open_dot()
+        self.states, self.initial_state, self.final_states = self.__get_state_variables()
+        self.env_types = {}
+        self.env_stored = set()
+        self.constraint_vars = set()
+        self.self_loop_reset_events = set()
+        self.events, self.envs = self.__get_event_variables()
+        self.function, self.constraints = self.__create_matrix()
+        self.events_start, self.events_start_run = self.__store_init_events()
+        self.env_stored = sorted(self.env_stored)
+        self.constraint_vars = sorted(self.constraint_vars)
+        self.self_loop_reset_events = sorted(self.self_loop_reset_events)
+
+    def __get_model_name(self) -> str:
+        basename = ntpath.basename(self.__dot_path)
+        if not basename.endswith(".dot") and not basename.endswith(".gv"):
+            print("not a dot file")
+            raise AutomataError(f"not a dot file: {self.__dot_path}")
+
+        model_name = ntpath.splitext(basename)[0]
+        if not model_name:
+            raise AutomataError(f"not a dot file: {self.__dot_path}")
+
+        return model_name
+
+    def __open_dot(self) -> list[str]:
+        dot_lines = []
+        try:
+            with open(self.__dot_path) as dot_file:
+                dot_lines = dot_file.readlines()
+        except OSError as exc:
+            raise AutomataError(exc.strerror) from exc
+
+        if not dot_lines:
+            raise AutomataError(f"{self.__dot_path} is empty")
+
+        # checking the first line:
+        line = dot_lines[0].split()
+
+        if len(line) < 2 or line[0] != "digraph" or line[1] != "state_automaton":
+            raise AutomataError(f"Not a valid .dot format: {self.__dot_path}")
+
+        return dot_lines
+
+    def __get_cursor_begin_states(self) -> int:
+        for cursor, line in enumerate(self.__dot_lines):
+            split_line = line.split()
+
+            if len(split_line) and split_line[0] == self.node_marker:
+                return cursor
+
+        raise AutomataError("Could not find a beginning state")
+
+    def __get_cursor_begin_events(self) -> int:
+        state = 0
+        cursor = 0 # make pyright happy
+
+        for cursor, line in enumerate(self.__dot_lines):
+            line = line.split()
+            if not line:
+                continue
+
+            if state == 0:
+                if line[0] == self.node_marker:
+                    state = 1
+            elif line[0] != self.node_marker:
+                break
+        else:
+            raise AutomataError("Could not find beginning event")
+
+        cursor += 1 # skip initial state transition
+        if cursor == len(self.__dot_lines):
+            raise AutomataError("Dot file ended after event beginning")
+
+        return cursor
+
+    def __get_state_variables(self) -> tuple[list[str], str, list[str]]:
+        # wait for node declaration
+        states = []
+        final_states = []
+        initial_state = ""
+
+        has_final_states = False
+        cursor = self.__get_cursor_begin_states()
+
+        # process nodes
+        for line in islice(self.__dot_lines, cursor, None):
+            split_line = line.split()
+            if not split_line or split_line[0] != self.node_marker:
+                break
+
+            raw_state = split_line[-1]
+
+            #  "enabled_fired"}; -> enabled_fired
+            state = raw_state.replace('"', '').replace('};', '').replace(',', '_')
+            if state.startswith(self.init_marker):
+                initial_state = state[len(self.init_marker):]
+            else:
+                states.append(state)
+                if "doublecircle" in line:
+                    final_states.append(state)
+                    has_final_states = True
+
+                if "ellipse" in line:
+                    final_states.append(state)
+                    has_final_states = True
+
+        if not initial_state:
+            raise AutomataError("The automaton doesn't have an initial state")
+
+        states = sorted(set(states))
+        states.remove(initial_state)
+
+        # Insert the initial state at the beginning of the states
+        states.insert(0, initial_state)
+
+        if not has_final_states:
+            final_states.append(initial_state)
+
+        return states, initial_state, final_states
+
+    def __get_event_variables(self) -> tuple[list[str], list[str]]:
+        events: list[str] = []
+        envs: list[str] = []
+        # here we are at the begin of transitions, take a note, we will return later.
+        cursor = self.__get_cursor_begin_events()
+
+        for line in map(str.lstrip, islice(self.__dot_lines, cursor, None)):
+            if not line.startswith('"'):
+                break
+
+            # transitions have the format:
+            # "all_fired" -> "both_fired" [ label = "disable_irq" ];
+            #  ------------ event is here ------------^^^^^
+            split_line = line.split()
+            if len(split_line) > 1 and split_line[1] == "->":
+                event = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
+
+                # when a transition has more than one label, they are like this
+                # "local_irq_enable\nhw_local_irq_enable_n"
+                # so split them.
+
+                for i in event.split("\\n"):
+                    # if the event contains a constraint (hybrid automata),
+                    # it will be separated by a ";":
+                    # "sched_switch;x<1000;reset(x)"
+                    ev, *constr = i.split(";")
+                    if constr:
+                        if len(constr) > 2:
+                            raise AutomataError("Only 1 constraint and 1 reset are supported")
+                        envs += self.__extract_env_var(constr)
+                    events.append(ev)
+            else:
+                # state labels have the format:
+                # "enable_fired" [label = "enable_fired\ncondition"];
+                #  ----- label is here -----^^^^^
+                # label and node name must be the same, condition is optional
+                state = line.split("label")[1].split('"')[1]
+                _, *constr = state.split("\\n")
+                if constr:
+                    if len(constr) > 1:
+                        raise AutomataError("Only 1 constraint is supported in the state")
+                    envs += self.__extract_env_var([constr[0].replace(" ", "")])
+
+        return sorted(set(events)), sorted(set(envs))
+
+    def _split_constraint_expr(self, constr: list[str]) -> Iterator[tuple[str,
+                                                                          str | None]]:
+        """
+        Get a list of strings of the type constr1 && constr2 and returns a list of
+        constraints and separators: [[constr1,"&&"],[constr2,None]]
+        """
+        exprs = []
+        seps = []
+        for c in constr:
+            while "&&" in c or "||" in c:
+                a = c.find("&&")
+                o = c.find("||")
+                pos = a if o < 0 or 0 < a < o else o
+                exprs.append(c[:pos].replace(" ", ""))
+                seps.append(c[pos:pos + 2].replace(" ", ""))
+                c = c[pos + 2:].replace(" ", "")
+            exprs.append(c)
+            seps.append(None)
+        return zip(exprs, seps)
+
+    def __extract_env_var(self, constraint: list[str]) -> list[str]:
+        env = []
+        for c, _ in self._split_constraint_expr(constraint):
+            rule = self.constraint_rule.search(c)
+            reset = self.constraint_reset.search(c)
+            if rule:
+                env.append(rule["env"])
+                if rule.groupdict().get("unit"):
+                    self.env_types[rule["env"]] = rule["unit"]
+                if rule["val"][0].isalpha():
+                    self.constraint_vars.add(rule["val"])
+                # try to infer unit from constants or parameters
+                val_for_unit = rule["val"].lower().replace("()", "")
+                if val_for_unit.endswith("_ns"):
+                    self.env_types[rule["env"]] = "ns"
+                if val_for_unit.endswith("_jiffies"):
+                    self.env_types[rule["env"]] = "j"
+            if reset:
+                env.append(reset["env"])
+                # environment variables that are reset need a storage
+                self.env_stored.add(reset["env"])
+        return env
+
+    def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]:
+        # transform the array into a dictionary
+        events = self.events
+        states = self.states
+        events_dict = {}
+        states_dict = {}
+        nr_event = 0
+        for event in events:
+            events_dict[event] = nr_event
+            nr_event += 1
+
+        nr_state = 0
+        for state in states:
+            states_dict[state] = nr_state
+            nr_state += 1
+
+        # declare the matrix....
+        matrix = [[self.invalid_state_str for _ in range(nr_event)] for _ in range(nr_state)]
+        constraints: dict[_ConstraintKey, list[str]] = {}
+
+        # and we are back! Let's fill the matrix
+        cursor = self.__get_cursor_begin_events()
+
+        for line in map(str.lstrip,
+                        islice(self.__dot_lines, cursor, None)):
+
+            if not line or line[0] != '"':
+                break
+
+            split_line = line.split()
+
+            if len(split_line) > 2 and split_line[1] == "->":
+                origin_state = split_line[0].replace('"', '').replace(',', '_')
+                dest_state = split_line[2].replace('"', '').replace(',', '_')
+                possible_events = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
+                for event in possible_events.split("\\n"):
+                    event, *constr = event.split(";")
+                    if constr:
+                        key = _EventConstraintKey(states_dict[origin_state], events_dict[event])
+                        constraints[key] = constr
+                        # those events reset also on self loops
+                        if origin_state == dest_state and "reset" in "".join(constr):
+                            self.self_loop_reset_events.add(event)
+                    matrix[states_dict[origin_state]][events_dict[event]] = dest_state
+            else:
+                state = line.split("label")[1].split('"')[1]
+                state, *constr = state.replace(" ", "").split("\\n")
+                if constr:
+                    constraints[_StateConstraintKey(states_dict[state])] = constr
+
+        return matrix, constraints
+
+    def __store_init_events(self) -> tuple[list[bool], list[bool]]:
+        events_start = [False] * len(self.events)
+        events_start_run = [False] * len(self.events)
+        for i in range(len(self.events)):
+            curr_event_will_init = 0
+            curr_event_from_init = False
+            curr_event_used = 0
+            for j in range(len(self.states)):
+                if self.function[j][i] != self.invalid_state_str:
+                    curr_event_used += 1
+                if self.function[j][i] == self.initial_state:
+                    curr_event_will_init += 1
+            if self.function[0][i] != self.invalid_state_str:
+                curr_event_from_init = True
+            # this event always leads to init
+            if curr_event_will_init and curr_event_used == curr_event_will_init:
+                events_start[i] = True
+            # this event is only called from init
+            if curr_event_from_init and curr_event_used == 1:
+                events_start_run[i] = True
+        return events_start, events_start_run
+
+    def is_start_event(self, event: str) -> bool:
+        return self.events_start[self.events.index(event)]
+
+    def is_start_run_event(self, event: str) -> bool:
+        # prefer handle_start_event if there
+        if any(self.events_start):
+            return False
+        return self.events_start_run[self.events.index(event)]
+
+    def is_hybrid_automata(self) -> bool:
+        return bool(self.envs)
+
+    def is_event_constraint(self, key: _ConstraintKey) -> bool:
+        """
+        Given the key in self.constraints return true if it is an event
+        constraint, false if it is a state constraint
+        """
+        return isinstance(key, _EventConstraintKey)
diff --git a/tools/verification/rvgen/rvgen/container.py b/tools/verification/rvgen/rvgen/container.py
new file mode 100644
index 000000000..51f188530
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/container.py
@@ -0,0 +1,32 @@
+#!/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
+
+    def fill_kconfig_tooltip(self):
+        """Override to produce a marker for this container in the Kconfig"""
+        container_marker = self._kconfig_marker(self.name) + "\n"
+        result = super().fill_kconfig_tooltip()
+        if self.auto_patch:
+            self._patch_file("Kconfig",
+                             self._kconfig_marker(), container_marker)
+            return result
+        return result + container_marker
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
new file mode 100644
index 000000000..fc85ba1f6
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -0,0 +1,268 @@
+#!/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>
+#
+# dot2c: parse an automaton in dot file digraph format into a C
+#
+# This program was written in the development of this paper:
+#  de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
+#  "Efficient Formal Verification for the Linux Kernel." International
+#  Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# For further information, see:
+#   Documentation/trace/rv/deterministic_automata.rst
+
+from .automata import Automata, AutomataError
+
+class Dot2c(Automata):
+    enum_suffix = ""
+    enum_states_def = "states"
+    enum_events_def = "events"
+    enum_envs_def = "envs"
+    struct_automaton_def = "automaton"
+    var_automaton_def = "aut"
+
+    def __init__(self, file_path, model_name=None):
+        super().__init__(file_path, model_name)
+        self.line_length = 100
+
+    def __get_enum_states_content(self) -> list[str]:
+        buff = []
+        buff.append(f"\t{self.initial_state}{self.enum_suffix},")
+        for state in self.states:
+            if state != self.initial_state:
+                buff.append(f"\t{state}{self.enum_suffix},")
+        buff.append(f"\tstate_max{self.enum_suffix},")
+
+        return buff
+
+    def format_states_enum(self) -> list[str]:
+        buff = []
+        buff.append(f"enum {self.enum_states_def} {{")
+        buff += self.__get_enum_states_content()
+        buff.append("};\n")
+
+        return buff
+
+    def __get_enum_events_content(self) -> list[str]:
+        buff = []
+        for event in self.events:
+            buff.append(f"\t{event}{self.enum_suffix},")
+
+        buff.append(f"\tevent_max{self.enum_suffix},")
+
+        return buff
+
+    def format_events_enum(self) -> list[str]:
+        buff = []
+        buff.append(f"enum {self.enum_events_def} {{")
+        buff += self.__get_enum_events_content()
+        buff.append("};\n")
+
+        return buff
+
+    def __get_non_stored_envs(self) -> list[str]:
+        return [e for e in self.envs if e not in self.env_stored]
+
+    def __get_enum_envs_content(self) -> list[str]:
+        buff = []
+        # We first place env variables that have a u64 storage.
+        # Those are limited by MAX_HA_ENV_LEN, other variables
+        # are read only and don't require a storage.
+        unstored = self.__get_non_stored_envs()
+        for env in list(self.env_stored) + unstored:
+            buff.append(f"\t{env}{self.enum_suffix},")
+
+        buff.append(f"\tenv_max{self.enum_suffix},")
+        max_stored = unstored[0] if len(unstored) else "env_max"
+        buff.append(f"\tenv_max_stored{self.enum_suffix} = {max_stored}{self.enum_suffix},")
+
+        return buff
+
+    def format_envs_enum(self) -> list[str]:
+        buff = []
+        if self.is_hybrid_automata():
+            buff.append(f"enum {self.enum_envs_def} {{")
+            buff += self.__get_enum_envs_content()
+            buff.append("};\n")
+            buff.append(f"_Static_assert(env_max_stored{self.enum_suffix} <= MAX_HA_ENV_LEN,"
+                        ' "Not enough slots");')
+            if {"ns", "us", "ms", "s"}.intersection(self.env_types.values()):
+                buff.append("#define HA_CLK_NS")
+            buff.append("")
+        return buff
+
+    def get_minimun_type(self) -> str:
+        min_type = "unsigned char"
+
+        if len(self.states) > 255:
+            min_type = "unsigned short"
+
+        if len(self.states) > 65535:
+            min_type = "unsigned int"
+
+        if len(self.states) > 1000000:
+            raise AutomataError(f"Too many states: {len(self.states)}")
+
+        return min_type
+
+    def format_automaton_definition(self) -> list[str]:
+        min_type = self.get_minimun_type()
+        buff = []
+        buff.append(f"struct {self.struct_automaton_def} {{")
+        buff.append(f"\tchar *state_names[state_max{self.enum_suffix}];")
+        buff.append(f"\tchar *event_names[event_max{self.enum_suffix}];")
+        if self.is_hybrid_automata():
+            buff.append(f"\tchar *env_names[env_max{self.enum_suffix}];")
+        buff.append(f"\t{min_type} function[state_max{self.enum_suffix}][event_max{self.enum_suffix}];")
+        buff.append(f"\t{min_type} initial_state;")
+        buff.append(f"\tbool final_states[state_max{self.enum_suffix}];")
+        buff.append("};\n")
+        return buff
+
+    def format_aut_init_header(self) -> list[str]:
+        buff = []
+        buff.append(f"static const struct {self.struct_automaton_def} {self.var_automaton_def} = {{")
+        return buff
+
+    def __get_string_vector_per_line_content(self, entries: list[str]) -> str:
+        buff = []
+        for entry in entries:
+            buff.append(f"\t\t\"{entry}\",")
+        return "\n".join(buff)
+
+    def format_aut_init_events_string(self) -> list[str]:
+        buff = []
+        buff.append("\t.event_names = {")
+        buff.append(self.__get_string_vector_per_line_content(self.events))
+        buff.append("\t},")
+        return buff
+
+    def format_aut_init_states_string(self) -> list[str]:
+        buff = []
+        buff.append("\t.state_names = {")
+        buff.append(self.__get_string_vector_per_line_content(self.states))
+        buff.append("\t},")
+
+        return buff
+
+    def format_aut_init_envs_string(self) -> list[str]:
+        buff = []
+        if self.is_hybrid_automata():
+            buff.append("\t.env_names = {")
+            # maintain consistent order with the enum
+            ordered_envs = list(self.env_stored) + self.__get_non_stored_envs()
+            buff.append(self.__get_string_vector_per_line_content(ordered_envs))
+            buff.append("\t},")
+
+        return buff
+
+    def __get_max_strlen_of_states(self) -> int:
+        max_state_name = len(max(self.states, key=len))
+        return max(max_state_name, len(self.invalid_state_str))
+
+    def get_aut_init_function(self) -> str:
+        nr_states = len(self.states)
+        nr_events = len(self.events)
+        buff = []
+
+        maxlen = self.__get_max_strlen_of_states() + len(self.enum_suffix)
+        tab_braces = 2 * 8 + 2 + 1  # "\t\t{ " ... "}"
+        comma_space = 2  # ", " count last comma here
+        linetoolong = tab_braces + (maxlen + comma_space) * nr_events > self.line_length
+        for x in range(nr_states):
+            line = "\t\t{\n" if linetoolong else "\t\t{ "
+            for y in range(nr_events):
+                next_state = self.function[x][y]
+                if next_state != self.invalid_state_str:
+                    next_state = self.function[x][y] + self.enum_suffix
+
+                if linetoolong:
+                    line += f"\t\t\t{next_state}"
+                else:
+                    line += f"{next_state:>{maxlen}}"
+                if y != nr_events - 1:
+                    line += ",\n" if linetoolong else ", "
+                else:
+                    line += ",\n\t\t}," if linetoolong else " },"
+            buff.append(line)
+
+        return '\n'.join(buff)
+
+    def format_aut_init_function(self) -> list[str]:
+        buff = []
+        buff.append("\t.function = {")
+        buff.append(self.get_aut_init_function())
+        buff.append("\t},")
+
+        return buff
+
+    def get_aut_init_initial_state(self) -> str:
+        return self.initial_state
+
+    def format_aut_init_initial_state(self) -> list[str]:
+        buff = []
+        initial_state = self.get_aut_init_initial_state()
+        buff.append("\t.initial_state = " + initial_state + self.enum_suffix + ",")
+
+        return buff
+
+    def get_aut_init_final_states(self) -> str:
+        line = ""
+        first = True
+        for state in self.states:
+            if not first:
+                line = line + ', '
+            else:
+                first = False
+
+            if state in self.final_states:
+                line = line + '1'
+            else:
+                line = line + '0'
+        return line
+
+    def format_aut_init_final_states(self) -> list[str]:
+       buff = []
+       buff.append(f"\t.final_states = {{ {self.get_aut_init_final_states()} }},")
+
+       return buff
+
+    def __get_automaton_initialization_footer_string(self) -> str:
+        footer = "};\n"
+        return footer
+
+    def format_aut_init_footer(self) -> list[str]:
+        buff = []
+        buff.append(self.__get_automaton_initialization_footer_string())
+
+        return buff
+
+    def format_invalid_state(self) -> list[str]:
+        buff = []
+        buff.append(f"#define {self.invalid_state_str} state_max{self.enum_suffix}\n")
+
+        return buff
+
+    def format_model(self) -> list[str]:
+        buff = []
+        buff += self.format_states_enum()
+        buff += self.format_invalid_state()
+        buff += self.format_events_enum()
+        buff += self.format_envs_enum()
+        buff += self.format_automaton_definition()
+        buff += self.format_aut_init_header()
+        buff += self.format_aut_init_states_string()
+        buff += self.format_aut_init_events_string()
+        buff += self.format_aut_init_envs_string()
+        buff += self.format_aut_init_function()
+        buff += self.format_aut_init_initial_state()
+        buff += self.format_aut_init_final_states()
+        buff += self.format_aut_init_footer()
+
+        return buff
+
+    def print_model_classic(self):
+        buff = self.format_model()
+        print('\n'.join(buff))
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
new file mode 100644
index 000000000..110cfd69e
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -0,0 +1,611 @@
+#!/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>
+#
+# dot2k: transform dot files into a monitor for the Linux kernel.
+#
+# For further information, see:
+#   Documentation/trace/rv/da_monitor_synthesis.rst
+
+from collections import deque
+from .dot2c import Dot2c
+from .generator import Monitor
+from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
+
+
+class dot2k(Monitor, Dot2c):
+    template_dir = "dot2k"
+
+    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 = f"_{self.name}"
+        self.enum_suffix = f"_{self.name}"
+        self.monitor_class = extra_params["monitor_class"]
+
+    def fill_monitor_type(self) -> str:
+        buff = [ self.monitor_type.upper() ]
+        buff += self._fill_timer_type()
+        if self.monitor_type == "per_obj":
+            buff.append("typedef /* XXX: define the target type */ *monitor_target;")
+        return "\n".join(buff)
+
+    def fill_tracepoint_handlers_skel(self) -> str:
+        buff = []
+        buff += self._fill_hybrid_definitions()
+        for event in self.events:
+            buff.append(f"static void handle_{event}(void *data, /* XXX: fill header */)")
+            buff.append("{")
+            handle = "handle_event"
+            if self.is_start_event(event):
+                buff.append("\t/* XXX: validate that this event always leads to the initial state */")
+                handle = "handle_start_event"
+            elif self.is_start_run_event(event):
+                buff.append("\t/* XXX: validate that this event is only valid in the initial state */")
+                handle = "handle_start_run_event"
+            if self.monitor_type == "per_task":
+                buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;")
+                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});")
+            elif self.monitor_type == "per_obj":
+                buff.append("\tint id = /* XXX: how do I get the id? */;")
+                buff.append("\tmonitor_target t = /* XXX: how do I get t? */;")
+                buff.append(f"\tda_{handle}(id, t, {event}{self.enum_suffix});")
+            else:
+                buff.append(f"\tda_{handle}({event}{self.enum_suffix});")
+            buff.append("}")
+            buff.append("")
+        return '\n'.join(buff)
+
+    def fill_tracepoint_attach_probe(self) -> str:
+        buff = []
+        for event in self.events:
+            buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
+        return '\n'.join(buff)
+
+    def fill_tracepoint_detach_helper(self) -> str:
+        buff = []
+        for event in self.events:
+            buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
+        return '\n'.join(buff)
+
+    def fill_model_h_header(self) -> list[str]:
+        buff = []
+        buff.append("/* SPDX-License-Identifier: GPL-2.0 */")
+        buff.append("/*")
+        buff.append(f" * Automatically generated C representation of {self.name} automaton")
+        buff.append(" * For further information about this format, see kernel documentation:")
+        buff.append(" *   Documentation/trace/rv/deterministic_automata.rst")
+        buff.append(" */")
+        buff.append("")
+        buff.append(f"#define MONITOR_NAME {self.name}")
+        buff.append("")
+
+        return buff
+
+    def fill_model_h(self) -> str:
+        #
+        # Adjust the definition names
+        #
+        self.enum_states_def = f"states_{self.name}"
+        self.enum_events_def = f"events_{self.name}"
+        self.enum_envs_def = f"envs_{self.name}"
+        self.struct_automaton_def = f"automaton_{self.name}"
+        self.var_automaton_def = f"automaton_{self.name}"
+
+        buff = self.fill_model_h_header()
+        buff += self.format_model()
+
+        return '\n'.join(buff)
+
+    def _is_id_monitor(self) -> bool:
+        return self.monitor_type in ("per_task", "per_obj")
+
+    def fill_monitor_class_type(self) -> str:
+        if self._is_id_monitor():
+            return "DA_MON_EVENTS_ID"
+        return "DA_MON_EVENTS_IMPLICIT"
+
+    def fill_monitor_class(self) -> str:
+        if self._is_id_monitor():
+            return "da_monitor_id"
+        return "da_monitor"
+
+    def fill_tracepoint_args_skel(self, tp_type: str) -> str:
+        buff = []
+        tp_args_event = [
+                ("char *", "state"),
+                ("char *", "event"),
+                ("char *", "next_state"),
+                ("bool ",  "final_state"),
+                ]
+        tp_args_error = [
+                ("char *", "state"),
+                ("char *", "event"),
+                ]
+        tp_args_error_env = tp_args_error + [("char *", "env")]
+        tp_args_dict = {
+                "event": tp_args_event,
+                "error": tp_args_error,
+                "error_env": tp_args_error_env
+                }
+        tp_args_id = ("int ", "id")
+        tp_args = tp_args_dict[tp_type]
+        if self._is_id_monitor():
+            tp_args.insert(0, tp_args_id)
+        tp_proto_c = ", ".join([a + b for a, b in tp_args])
+        tp_args_c = ", ".join([b for a, b in tp_args])
+        buff.append(f"	     TP_PROTO({tp_proto_c}),")
+        buff.append(f"	     TP_ARGS({tp_args_c})")
+        return '\n'.join(buff)
+
+    def _fill_hybrid_definitions(self) -> list:
+        """Stub, not valid for deterministic automata"""
+        return []
+
+    def _fill_timer_type(self) -> list:
+        """Stub, not valid for deterministic automata"""
+        return []
+
+    def fill_main_c(self) -> str:
+        main_c = super().fill_main_c()
+
+        min_type = self.get_minimun_type()
+        nr_events = len(self.events)
+        monitor_type = self.fill_monitor_type()
+
+        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)
+        main_c = main_c.replace("%%MONITOR_CLASS%%", self.monitor_class)
+
+        return main_c
+
+class da2k(dot2k):
+    """Deterministic automata only"""
+    def __init__(self, *args, **kwargs):
+        super().__init__(*args, **kwargs)
+        if self.is_hybrid_automata():
+            raise AutomataError("Detected hybrid automaton, use the 'ha' class")
+
+class ha2k(dot2k):
+    """Hybrid automata only"""
+    def __init__(self, *args, **kwargs):
+        super().__init__(*args, **kwargs)
+        if not self.is_hybrid_automata():
+            raise AutomataError("Detected deterministic automaton, use the 'da' class")
+        self.trace_h = self._read_template_file("trace_hybrid.h")
+        self.__parse_constraints()
+
+    def fill_monitor_class_type(self) -> str:
+        if self._is_id_monitor():
+            return "HA_MON_EVENTS_ID"
+        return "HA_MON_EVENTS_IMPLICIT"
+
+    def fill_monitor_class(self) -> str:
+        """
+        Used for tracepoint classes, since they are shared we keep da
+        instead of ha (also for the ha specific tracepoints).
+        The tracepoint class is not visible to the tools.
+        """
+        return super().fill_monitor_class()
+
+    def __adjust_value(self, value: str | int, unit: str | None) -> str:
+        """Adjust the value in ns"""
+        try:
+            value = int(value)
+        except ValueError:
+            # it's a constant, a parameter or a function
+            if value.endswith("()"):
+                return value.replace("()", "(ha_mon)")
+            return value
+        match unit:
+            case "us":
+                value *= 10**3
+            case "ms":
+                value *= 10**6
+            case "s":
+                value *= 10**9
+        return str(value) + "ull"
+
+    def __parse_single_constraint(self, rule: dict, value: str) -> str:
+        return f"ha_get_env(ha_mon, {rule["env"]}{self.enum_suffix}, time_ns) {rule["op"]} {value}"
+
+    def __get_constraint_env(self, constr: str) -> str:
+        """Extract the second argument from an ha_ function"""
+        env = constr.split("(")[1].split()[1].rstrip(")").rstrip(",")
+        assert env.removesuffix(f"_{self.name}") in self.envs
+        return env
+
+    def __start_to_invariant_check(self, constr: str) -> str:
+        # by default assume the timer has ns expiration
+        env = self.__get_constraint_env(constr)
+        clock_type = "ns"
+        if self.env_types.get(env.removesuffix(f"_{self.name}")) == "j":
+            clock_type = "jiffy"
+
+        return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)"
+
+    def __start_to_conv(self, constr: str) -> str:
+        """
+        Undo the storage conversion done by ha_start_timer_
+        """
+        return "ha_inv_to_guard" + constr[constr.find("("):]
+
+    def __parse_timer_constraint(self, rule: dict, value: str) -> str:
+        # by default assume the timer has ns expiration
+        clock_type = "ns"
+        if self.env_types.get(rule["env"]) == "j":
+            clock_type = "jiffy"
+
+        return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.enum_suffix},"
+                f" {value}, time_ns)")
+
+    def __format_guard_rules(self, rules: list[str]) -> list[str]:
+        """
+        Merge guard constraints as a single C return statement.
+        If the rules include a stored env, also check its validity.
+        Break lines in a best effort way that tries to keep readability.
+        """
+        if not rules:
+            return []
+
+        invalid_checks = [f"ha_monitor_env_invalid(ha_mon, {env}{self.enum_suffix}) ||"
+                          for env in self.env_stored if any(env in rule for rule in rules)]
+        if invalid_checks and len(rules) > 1:
+            rules[0] = "(" + rules[0]
+            rules[-1] = rules[-1] + ")"
+        rules = invalid_checks + rules
+
+        separator = "\n\t\t      " if sum(len(r) for r in rules) > 80 else " "
+        return ["res = " + separator.join(rules)]
+
+    def __validate_constraint(self, key: tuple[int, int] | int, constr: str,
+                              rule, reset) -> None:
+        # event constrains are tuples and allow both rules and reset
+        # state constraints are only used for expirations (e.g. clk<N)
+        if self.is_event_constraint(key):
+            if not rule and not reset:
+                raise AutomataError("Unrecognised event constraint "
+                                    f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
+            if rule and (rule["env"] in self.env_types and
+                         rule["env"] not in self.env_stored):
+                raise AutomataError("Clocks in hybrid automata always require a storage"
+                                    f" ({rule["env"]})")
+        else:
+            if not rule:
+                raise AutomataError("Unrecognised state constraint "
+                                    f"({self.states[key]}: {constr})")
+            if rule["env"] not in self.env_stored:
+                raise AutomataError("State constraints always require a storage "
+                                    f"({rule["env"]})")
+            if rule["op"] not in ["<", "<="]:
+                raise AutomataError("State constraints must be clock expirations like"
+                                    f" clk<N ({rule.string})")
+
+    def __parse_constraints(self) -> None:
+        self.guards: dict[_EventConstraintKey, str] = {}
+        self.invariants: dict[_StateConstraintKey, str] = {}
+        for key, constraint in self.constraints.items():
+            rules = []
+            resets = []
+            for c, sep in self._split_constraint_expr(constraint):
+                rule = self.constraint_rule.search(c)
+                reset = self.constraint_reset.search(c)
+                self.__validate_constraint(key, c, rule, reset)
+                if rule:
+                    value = rule["val"]
+                    value_len = len(rule["val"])
+                    unit = None
+                    if rule.groupdict().get("unit"):
+                        value_len += len(rule["unit"])
+                        unit = rule["unit"]
+                    c = c[:-(value_len)]
+                    value = self.__adjust_value(value, unit)
+                    if self.is_event_constraint(key):
+                        c = self.__parse_single_constraint(rule, value)
+                        if sep:
+                            c += f" {sep}"
+                    else:
+                        c = self.__parse_timer_constraint(rule, value)
+                    rules.append(c)
+                if reset:
+                    c = f"ha_reset_env(ha_mon, {reset["env"]}{self.enum_suffix}, time_ns)"
+                    resets.append(c)
+            if self.is_event_constraint(key):
+                res = self.__format_guard_rules(rules) + resets
+                self.guards[key] = ";".join(res)
+            else:
+                self.invariants[key] = rules[0]
+
+    def __fill_verify_invariants_func(self) -> list[str]:
+        buff = []
+        if not self.invariants:
+            return []
+
+        buff.append(
+f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
+\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
+\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
+{{""")
+
+        _else = ""
+        for state, constr in sorted(self.invariants.items()):
+            check_str = self.__start_to_invariant_check(constr)
+            buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
+            buff.append(f"\t\t{check_str};")
+            _else = "else "
+
+        buff.append("\treturn true;\n}\n")
+        return buff
+
+    def __fill_convert_inv_guard_func(self) -> list[str]:
+        buff = []
+        if not self.invariants:
+            return []
+
+        conflict_guards, conflict_invs = self.__find_inv_conflicts()
+        if not conflict_guards and not conflict_invs:
+            return []
+
+        buff.append(
+f"""static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
+\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
+\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
+{{""")
+        buff.append("\tif (curr_state == next_state)\n\t\treturn;")
+
+        _else = ""
+        for state, constr in sorted(self.invariants.items()):
+            # a state with invariant can reach us without reset
+            # multiple conflicts must have the same invariant, otherwise we cannot
+            # know how to reset the value
+            conf_i = [start for start, end in conflict_invs if end == state]
+            # we can reach a guard without reset
+            conf_g = [e for s, e in conflict_guards if s == state]
+            if not conf_i and not conf_g:
+                continue
+            buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
+
+            buff.append(f"\t\t{self.__start_to_conv(constr)};")
+            _else = "else "
+
+        buff.append("}\n")
+        return buff
+
+    def __fill_verify_guards_func(self) -> list[str]:
+        buff = []
+        if not self.guards:
+            return []
+
+        buff.append(
+f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
+\t\t\t\t    enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
+\t\t\t\t    enum {self.enum_states_def} next_state, u64 time_ns)
+{{
+\tbool res = true;
+""")
+
+        _else = ""
+        for edge, constr in sorted(self.guards.items()):
+            buff.append(f"\t{_else}if (curr_state == "
+                        f"{self.states[edge[0]]}{self.enum_suffix} && "
+                        f"event == {self.events[edge[1]]}{self.enum_suffix})")
+            if constr.count(";") > 0:
+                buff[-1] += " {"
+            buff += [f"\t\t{c};" for c in constr.split(";")]
+            if constr.count(";") > 0:
+                _else = "} else "
+            else:
+                _else = "else "
+        if _else[0] == "}":
+            buff.append("\t}")
+        buff.append("\treturn res;\n}\n")
+        return buff
+
+    def __find_inv_conflicts(self) -> tuple[set[tuple[int, _EventConstraintKey]],
+                                            set[tuple[int, _StateConstraintKey]]]:
+        """
+        Run a breadth first search from all states with an invariant.
+        Find any conflicting constraints reachable from there, this can be
+        another state with an invariant or an edge with a non-reset guard.
+        Stop when we find a reset.
+
+        Return the set of conflicting guards and invariants as tuples of
+        conflicting state and constraint key.
+        """
+        conflict_guards: set[tuple[int, _EventConstraintKey]] = set()
+        conflict_invs: set[tuple[int, _StateConstraintKey]] = set()
+        for start_idx in self.invariants:
+            queue = deque([(start_idx, 0)])  # (state_idx, distance)
+            env = self.__get_constraint_env(self.invariants[start_idx])
+
+            while queue:
+                curr_idx, distance = queue.popleft()
+
+                # Check state condition
+                if curr_idx != start_idx and curr_idx in self.invariants:
+                    conflict_invs.add((start_idx, _StateConstraintKey(curr_idx)))
+                    continue
+
+                # Check if we should stop
+                if distance > len(self.states):
+                    break
+                if curr_idx != start_idx and distance > 1:
+                    continue
+
+                for event_idx, next_state_name in enumerate(self.function[curr_idx]):
+                    if next_state_name == self.invalid_state_str:
+                        continue
+                    curr_guard = self.guards.get((curr_idx, event_idx), "")
+                    if "reset" in curr_guard and env in curr_guard:
+                        continue
+
+                    if env in curr_guard:
+                        conflict_guards.add((start_idx,
+                                             _EventConstraintKey(curr_idx, event_idx)))
+                        continue
+
+                    next_idx = self.states.index(next_state_name)
+                    queue.append((next_idx, distance + 1))
+
+        return conflict_guards, conflict_invs
+
+    def __fill_setup_invariants_func(self) -> list[str]:
+        buff = []
+        if not self.invariants:
+            return []
+
+        buff.append(
+f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
+\t\t\t\t       enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
+\t\t\t\t       enum {self.enum_states_def} next_state, u64 time_ns)
+{{""")
+
+        conditions = ["next_state == curr_state"]
+        conditions += [f"event != {e}{self.enum_suffix}"
+                       for e in self.self_loop_reset_events]
+        condition_str = " && ".join(conditions)
+        buff.append(f"\tif ({condition_str})\n\t\treturn;")
+
+        _else = ""
+        for state, constr in sorted(self.invariants.items()):
+            buff.append(f"\t{_else}if (next_state == {self.states[state]}{self.enum_suffix})")
+            buff.append(f"\t\t{constr};")
+            _else = "else "
+
+        for state in self.invariants:
+            buff.append(f"\telse if (curr_state == {self.states[state]}{self.enum_suffix})")
+            buff.append("\t\tha_cancel_timer(ha_mon);")
+
+        buff.append("}\n")
+        return buff
+
+    def __fill_constr_func(self) -> list[str]:
+        buff = []
+        if not self.constraints:
+            return []
+
+        buff.append(
+"""/*
+ * These functions are used to validate state transitions.
+ *
+ * They are generated by parsing the model, there is usually no need to change them.
+ * If the monitor requires a timer, there are functions responsible to arm it when
+ * the next state has a constraint, cancel it in any other case and to check
+ * that it didn't expire before the callback run. Transitions to the same state
+ * without a reset never affect timers.
+ * Due to the different representations between invariants and guards, there is
+ * a function to convert it in case invariants or guards are reachable from
+ * another invariant without reset. Those are not present if not required in
+ * the model. This is all automatic but is worth checking because it may show
+ * errors in the model (e.g. missing resets).
+ */""")
+
+        buff += self.__fill_verify_invariants_func()
+        inv_conflicts = self.__fill_convert_inv_guard_func()
+        buff += inv_conflicts
+        buff += self.__fill_verify_guards_func()
+        buff += self.__fill_setup_invariants_func()
+
+        buff.append(
+f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
+\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
+\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
+{{""")
+
+        if self.invariants:
+            buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, "
+                        "event, next_state, time_ns))\n\t\treturn false;\n")
+        if inv_conflicts:
+            buff.append("\tha_convert_inv_guard(ha_mon, curr_state, event, "
+                        "next_state, time_ns);\n")
+
+        if self.guards:
+            buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
+                        "next_state, time_ns))\n\t\treturn false;\n")
+
+        if self.invariants:
+            buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n")
+
+        buff.append("\treturn true;\n}\n")
+        return buff
+
+    def __fill_env_getter(self, env: str) -> str:
+        if env in self.env_types:
+            match self.env_types[env]:
+                case "ns" | "us" | "ms" | "s":
+                    return "ha_get_clk_ns(ha_mon, env, time_ns);"
+                case "j":
+                    return "ha_get_clk_jiffy(ha_mon, env);"
+        return f"/* XXX: how do I read {env}? */"
+
+    def __fill_env_resetter(self, env: str) -> str:
+        if env in self.env_types:
+            match self.env_types[env]:
+                case "ns" | "us" | "ms" | "s":
+                    return "ha_reset_clk_ns(ha_mon, env, time_ns);"
+                case "j":
+                    return "ha_reset_clk_jiffy(ha_mon, env);"
+        return f"/* XXX: how do I reset {env}? */"
+
+    def __fill_hybrid_get_reset_functions(self) -> list[str]:
+        buff = []
+        if self.is_hybrid_automata():
+            for var in self.constraint_vars:
+                if var.endswith("()"):
+                    func_name = var.replace("()", "")
+                    if func_name.isupper():
+                        buff.append(f"#define {func_name}(ha_mon) "
+                                    f"/* XXX: what is {func_name}(ha_mon)? */\n")
+                    else:
+                        buff.append(f"static inline u64 {func_name}(struct ha_monitor *ha_mon)\n{{")
+                        buff.append(f"\treturn /* XXX: what is {func_name}(ha_mon)? */;")
+                        buff.append("}\n")
+                elif var.isupper():
+                    buff.append(f"#define {var} /* XXX: what is {var}? */\n")
+                else:
+                    buff.append(f"static u64 {var} = /* XXX: default value */;")
+                    buff.append(f"module_param({var}, ullong, 0644);\n")
+            buff.append("""/*
+ * These functions define how to read and reset the environment variable.
+ *
+ * Common environment variables like ns-based and jiffy-based clocks have
+ * pre-define getters and resetters you can use. The parser can infer the type
+ * of the environment variable if you supply a measure unit in the constraint.
+ * If you define your own functions, make sure to add appropriate memory
+ * barriers if required.
+ * Some environment variables don't require a storage as they read a system
+ * state (e.g. preemption count). Those variables are never reset, so we don't
+ * define a reset function on monitors only relying on this type of variables.
+ */""")
+            buff.append("static u64 ha_get_env(struct ha_monitor *ha_mon, "
+                        f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{")
+            _else = ""
+            for env in self.envs:
+                buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})")
+                buff.append(f"\t\treturn {self.__fill_env_getter(env)}")
+                _else = "else "
+            buff.append("\treturn ENV_INVALID_VALUE;\n}\n")
+            if len(self.env_stored):
+                buff.append("static void ha_reset_env(struct ha_monitor *ha_mon, "
+                            f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{")
+                _else = ""
+                for env in self.env_stored:
+                    buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})")
+                    buff.append(f"\t\t{self.__fill_env_resetter(env)}")
+                    _else = "else "
+                buff.append("}\n")
+        return buff
+
+    def _fill_hybrid_definitions(self) -> list[str]:
+        return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func()
+
+    def _fill_timer_type(self) -> list:
+        if self.invariants:
+            return [
+                    "/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */",
+                    "#define HA_TIMER_TYPE HA_TIMER_HRTIMER"
+                    ]
+        return []
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
new file mode 100644
index 000000000..56f3bd8db
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -0,0 +1,251 @@
+#!/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>
+#
+# Abstract 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(f"/lib/modules/{platform.release()}/build", 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):
+        with open(path, 'r') as fd:
+            content = fd.read()
+        return content
+
+    def _read_template_file(self, file):
+        try:
+            path = os.path.join(self.abs_template_dir, file)
+            return self._read_file(path)
+        except OSError:
+            # 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 f"&rv_{self.parent}" if self.parent else "NULL"
+
+    def fill_include_parent(self):
+        if self.parent:
+            return f"#include <monitors/{self.parent}/{self.parent}.h>\n"
+        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(f"	depends on RV_MON_{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):
+        assert self.auto_patch
+        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",
+                            f"// Add new monitors based on CONFIG_{monitor_class_type} here",
+                            f"#include <monitors/{self.name}/{self.name}_trace.h>")
+            return f"  - Patching {self.rv_dir}/rv_trace.h, double check the result"
+
+        return f"""  - Edit {self.rv_dir}/rv_trace.h:
+Add this line where other tracepoints are included and {monitor_class_type} is defined:
+#include <monitors/{self.name}/{self.name}_trace.h>
+"""
+
+    def _kconfig_marker(self, container=None) -> str:
+        return f"# Add new {container + ' ' if container else ''}monitors here"
+
+    def fill_kconfig_tooltip(self):
+        if self.auto_patch:
+            # monitors with a container should stay together in the Kconfig
+            self._patch_file("Kconfig",
+                             self._kconfig_marker(self.parent),
+                            f"source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"")
+            return f"  - Patching {self.rv_dir}/Kconfig, double check the result"
+
+        return f"""  - Edit {self.rv_dir}/Kconfig:
+Add this line where other monitors are included:
+source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"
+"""
+
+    def fill_makefile_tooltip(self):
+        name = self.name
+        name_up = name.upper()
+        if self.auto_patch:
+            self._patch_file("Makefile",
+                            "# Add new monitors here",
+                            f"obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o")
+            return f"  - Patching {self.rv_dir}/Makefile, double check the result"
+
+        return f"""  - Edit {self.rv_dir}/Makefile:
+Add this line where other monitors are included:
+obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
+"""
+
+    def fill_monitor_tooltip(self):
+        if self.auto_patch:
+            return f"  - Monitor created in {self.rv_dir}/monitors/{self.name}"
+        return f"  - Move {self.name}/ to the kernel's monitor directory ({self.rv_dir}/monitors)"
+
+    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
+
+    def __write_file(self, file_name, content):
+        with open(file_name, 'w') as file:
+            file.write(content)
+
+    def _create_file(self, file_name, content):
+        path = f"{self.name}/{file_name}"
+        if self.auto_patch:
+            path = os.path.join(self.rv_dir, "monitors", path)
+        self.__write_file(path, content)
+
+    def print_files(self):
+        main_c = self.fill_main_c()
+
+        self.__create_directory()
+
+        path = f"{self.name}.c"
+        self._create_file(path, main_c)
+
+        model_h = self.fill_model_h()
+        path = f"{self.name}.h"
+        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, "per_obj": 4}
+
+    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")
+        tracepoint_args_skel_error_env = self.fill_tracepoint_args_skel("error_env")
+        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)
+        trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR_ENV%%", tracepoint_args_skel_error_env)
+        return trace_h
+
+    def print_files(self):
+        super().print_files()
+        trace_h = self.fill_trace_h()
+        path = f"{self.name}_trace.h"
+        self._create_file(path, trace_h)
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
new file mode 100644
index 000000000..016e7cf93
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -0,0 +1,568 @@
+#!/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
+from .automata import AutomataError
+
+# Grammar:
+# 	ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
+#
+# Operands (opd):
+# 	true, false, user-defined names
+#
+# Unary Operators (unop):
+#       always
+#       eventually
+#       next
+#       not
+#
+# Binary Operators (binop):
+#       until
+#       and
+#       or
+#       imply
+#       equivalent
+
+tokens = (
+   'AND',
+   'OR',
+   'IMPLY',
+   'UNTIL',
+   'ALWAYS',
+   'EVENTUALLY',
+   'NEXT',
+   '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_NEXT = r'next'
+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 AutomataError(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, Variable)):
+            return str(self.op)
+        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 NextOp(UnaryOp):
+    def normalize(self):
+        return self
+
+    def _is_temporal(self):
+        return True
+
+    def negate(self):
+        # not (next A) == next (not A)
+        self.child = self.child.negate()
+        return self
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        tmp = GraphNode(node.incoming,
+                        node.new,
+                        node.old | {n},
+                        node.next | {n.op.child})
+        return tmp.expand(node_set)
+
+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 __str__(self):
+        return self.name.lower()
+
+    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.op, 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
+         | NEXT ltl
+         | NOT ltl
+    '''
+    if p[1] == "always":
+        op = AlwaysOp(p[2])
+    elif p[1] == "eventually":
+        op = EventuallyOp(p[2])
+    elif p[1] == "next":
+        op = NextOp(p[2])
+    elif p[1] == "not":
+        op = NotOp(p[2])
+    else:
+        raise AutomataError(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 AutomataError(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 AutomataError("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 000000000..81fd1f5ea
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -0,0 +1,277 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+
+from pathlib import Path
+from . import generator
+from . import ltl2ba
+from .automata import AutomataError
+
+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])
+
+    def find_share_length(atom: str) -> int:
+        for i in range(len(atom), -1, -1):
+            if sum(a.startswith(atom[:i]) for a in atoms) > 1:
+                return i
+        return 0
+
+    abbrs = []
+    for atom in atoms:
+        share_len = find_share_length(atom)
+        share = atom[:share_len]
+        unique = atom[share_len:]
+        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)
+        try:
+            with open(file_path) as f:
+                self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read())
+        except OSError as exc:
+            raise AutomataError(exc.strerror) from exc
+        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) -> list[str]:
+        buf = [
+            "enum ltl_buchi_state {",
+        ]
+
+        for node in self.ba:
+            buf.append(f"\tS{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(f"\tLTL_{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(f"\t\t\"{name}\",")
+
+        buf.extend([
+            "\t};",
+            "",
+            "\treturn names[atom];",
+            "}"
+        ])
+        return buf
+
+    def _fill_atom_values(self, required_values):
+        buf = []
+        for node in self.ltl:
+            if str(node) not in required_values:
+                continue
+
+            if isinstance(node.op, ltl2ba.AndOp):
+                buf.append(f"\tbool {node} = {node.op.left} && {node.op.right};")
+                required_values |= {str(node.op.left), str(node.op.right)}
+            elif isinstance(node.op, ltl2ba.OrOp):
+                buf.append(f"\tbool {node} = {node.op.left} || {node.op.right};")
+                required_values |= {str(node.op.left), str(node.op.right)}
+            elif isinstance(node.op, ltl2ba.NotOp):
+                buf.append(f"\tbool {node} = !{node.op.child};")
+                required_values.add(str(node.op.child))
+
+        for atom in self.atoms:
+            if atom.lower() not in required_values:
+                continue
+            buf.append(f"\tbool {atom.lower()} = test_bit(LTL_{atom}, mon->atoms);")
+
+        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)",
+            "{"
+        ]
+
+        required_values = set()
+        for node in self.ba:
+            for o in sorted(node.outgoing):
+                required_values |= o.labels
+
+        buf.extend(self._fill_atom_values(required_values))
+        buf.extend([
+            "",
+            "\tswitch (state) {"
+        ])
+
+        for node in self.ba:
+            buf.append(f"\tcase S{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(f"\t\t\t__set_bit(S{o.id}, next);")
+            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)",
+            "{"
+        ]
+
+        required_values = set()
+        for node in self.ba:
+            if node.init:
+                required_values |= node.labels
+
+        buf.extend(self._fill_atom_values(required_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(f"\t\t__set_bit(S{node.id}, mon->states);")
+        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(f"\tltl_atom_update(task, LTL_{self.atoms[0]}, true/false);")
+        buff.append("}")
+        buff.append("")
+        return '\n'.join(buff)
+
+    def fill_tracepoint_attach_probe(self):
+        return f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_example_event);"
+
+    def fill_tracepoint_detach_helper(self):
+        return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_sample_event);"
+
+    def fill_atoms_init(self):
+        buff = []
+        for a in self.atoms:
+            buff.append(f"\tltl_atom_set(mon, LTL_{a}, true/false);")
+        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/Kconfig b/tools/verification/rvgen/rvgen/templates/Kconfig
new file mode 100644
index 000000000..291b29ea2
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/Kconfig
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_%%MODEL_NAME_UP%%
+	depends on RV
+%%MONITOR_DEPS%%
+	select %%MONITOR_CLASS_TYPE%%
+	bool "%%MODEL_NAME%% monitor"
+	help
+	  %%DESCRIPTION%%
diff --git a/tools/verification/rvgen/rvgen/templates/container/Kconfig b/tools/verification/rvgen/rvgen/templates/container/Kconfig
new file mode 100644
index 000000000..a60611194
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/container/Kconfig
@@ -0,0 +1,5 @@
+config RV_MON_%%MODEL_NAME_UP%%
+	depends on RV
+	bool "%%MODEL_NAME%% monitor"
+	help
+	  %%DESCRIPTION%%
diff --git a/tools/verification/rvgen/rvgen/templates/container/main.c b/tools/verification/rvgen/rvgen/templates/container/main.c
new file mode 100644
index 000000000..5fc89b46f
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/container/main.c
@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+
+#define MODULE_NAME "%%MODEL_NAME%%"
+
+#include "%%MODEL_NAME%%.h"
+
+struct rv_monitor rv_%%MODEL_NAME%% = {
+	.name = "%%MODEL_NAME%%",
+	.description = "%%DESCRIPTION%%",
+	.enable = NULL,
+	.disable = NULL,
+	.reset = NULL,
+	.enabled = 0,
+};
+
+static int __init register_%%MODEL_NAME%%(void)
+{
+	return rv_register_monitor(&rv_%%MODEL_NAME%%, NULL);
+}
+
+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("dot2k: auto-generated");
+MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");
diff --git a/tools/verification/rvgen/rvgen/templates/container/main.h b/tools/verification/rvgen/rvgen/templates/container/main.h
new file mode 100644
index 000000000..0f6883ab4
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/container/main.h
@@ -0,0 +1,3 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+extern struct rv_monitor rv_%%MODEL_NAME%%;
diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/main.c b/tools/verification/rvgen/rvgen/templates/dot2k/main.c
new file mode 100644
index 000000000..889446760
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/dot2k/main.c
@@ -0,0 +1,83 @@
+// 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.
+ */
+#define RV_MON_TYPE RV_MON_%%MONITOR_TYPE%%
+#include "%%MODEL_NAME%%.h"
+#include <rv/%%MONITOR_CLASS%%_monitor.h>
+
+/*
+ * 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 = %%MONITOR_CLASS%%_monitor_init();
+	if (retval)
+		return retval;
+
+%%TRACEPOINT_ATTACH%%
+
+	return 0;
+}
+
+static void disable_%%MODEL_NAME%%(void)
+{
+	rv_this.enabled = 0;
+
+%%TRACEPOINT_DETACH%%
+
+	%%MONITOR_CLASS%%_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "%%MODEL_NAME%%",
+	.description = "%%DESCRIPTION%%",
+	.enable = enable_%%MODEL_NAME%%,
+	.disable = disable_%%MODEL_NAME%%,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_%%MODEL_NAME%%(void)
+{
+	return rv_register_monitor(&rv_this, %%PARENT%%);
+}
+
+static void __exit unregister_%%MODEL_NAME%%(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_%%MODEL_NAME%%);
+module_exit(unregister_%%MODEL_NAME%%);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");
diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/trace.h b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h
new file mode 100644
index 000000000..87d3a1308
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h
@@ -0,0 +1,13 @@
+/* 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%%,
+%%TRACEPOINT_ARGS_SKEL_EVENT%%);
+
+DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%,
+%%TRACEPOINT_ARGS_SKEL_ERROR%%);
+#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */
diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h b/tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h
new file mode 100644
index 000000000..c8290e9ba
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h
@@ -0,0 +1,16 @@
+/* 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%%,
+%%TRACEPOINT_ARGS_SKEL_EVENT%%);
+
+DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%,
+%%TRACEPOINT_ARGS_SKEL_ERROR%%);
+
+DEFINE_EVENT(error_env_%%MONITOR_CLASS%%, error_env_%%MODEL_NAME%%,
+%%TRACEPOINT_ARGS_SKEL_ERROR_ENV%%);
+#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */
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 000000000..f85d076fb
--- /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 000000000..49394c4b0
--- /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%% */