diff --git a/Documentation/trace/rv/linear_temporal_logic.rst b/Documentation/trace/rv/linear_temporal_logic.rst
new file mode 100644
index 000000000000..9b0ce6a143ec
--- /dev/null
+++ b/Documentation/trace/rv/linear_temporal_logic.rst
@@ -0,0 +1,73 @@
+Introduction
+============
+
+Deterministic automaton runtime verification monitor is a verification technique which checks that
+the kernel follows a specification in the form of deterministic automaton (DA). It does so by using
+tracepoints to monitor the kernel's execution trace, and verifying that the execution trace
+sastifies the specification.
+
+However, while attempting to implement DA monitors for some complex specifications, deterministic
+automaton is found to be inappropriate as the specification language. The automaton is complicated,
+hard to understand, and error-prone.
+
+Thus, RV monitors based on linear temporal logic (LTL for short) are introduced. This type of
+monitor uses LTL as specification, instead of DA. For some cases, writing the specification as LTL
+is more concise and intuitive.
+
+Documents regarding LTL are widely available on the internet, this document will not go into
+details.
+
+Grammar
+========
+
+Unlike some existing syntax, kernel's implementation of LTL is more verbose. This is motivated by
+considering that the people who read the LTL specifications may not be well-versed in LTL.
+
+Grammar:
+    ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
+
+Operands (opd):
+    true, false, user-defined names consisting of upper-case characters, digits, and underscore.
+
+Unary Operators (unop):
+    always
+    eventually
+    not
+
+Binary Operators (binop):
+    until
+    and
+    or
+    imply
+    equivalent
+
+This grammar is ambiguous: operator precedence is not defined. Parentheses must be used.
+
+Monitor synthesis
+=================
+
+To synthesize an LTL into a kernel monitor, conversion scripts are provided:
+`tools/verification/ltl2ba`. The specification needs to be provided as a file, and it must have a
+"RULE = LTL" assignment, which specifies the LTL property to verify. For example:
+
+   .. code-block::
+
+    RULE = always (ACQUIRE imply ((not KILLED and not CRASHED) until RELEASE))
+
+The LTL can be broken down if required using sub-expressions. For example, the above is equivalent
+to:
+
+   .. code-block::
+
+    RULE = always (ACQUIRE imply (ALIVE until RELEASE))
+    ALIVE = not KILLED and not CRASHED
+
+The ltl file can be converted into C code:
+
+   .. code-block::
+
+    .tools/verification/ltl2ba/generate.py -l <ltl file> -n <model name> -o <output diretory>
+
+The above command generates `ba.c` and `ba.h`, the Buchi automaton that verifies the LTL property.
+The Buchi automaton needs to be manually glued to the kernel. Please see the comments in `ba.h` for
+further details.
diff --git a/include/linux/rv.h b/include/linux/rv.h
index 5482651ed020..6de4f93b390e 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -10,6 +10,8 @@
 #define MAX_DA_NAME_LEN	24
 
 #ifdef CONFIG_RV
+#include <linux/types.h>
+
 /*
  * Deterministic automaton per-object variables.
  */
@@ -18,6 +20,24 @@ struct da_monitor {
 	unsigned int	curr_state;
 };
 
+enum ltl_truth_value {
+	LTL_FALSE,
+	LTL_TRUE,
+	LTL_UNDETERMINED,
+};
+
+/*
+ * In the future, if the number of atomic propositions or the custom data size is larger, we can
+ * switch to dynamic allocation. For now, the code is simpler this way.
+ */
+#define RV_MAX_LTL_ATOM 10
+#define RV_MAX_DATA_SIZE 16
+struct ltl_monitor {
+	unsigned int		state;
+	enum ltl_truth_value	atoms[RV_MAX_LTL_ATOM];
+	u8			data[RV_MAX_DATA_SIZE];
+};
+
 /*
  * Per-task RV monitors count. Nowadays fixed in RV_PER_TASK_MONITORS.
  * If we find justification for more monitors, we can think about
@@ -27,11 +47,9 @@ struct da_monitor {
 #define RV_PER_TASK_MONITORS		1
 #define RV_PER_TASK_MONITOR_INIT	(RV_PER_TASK_MONITORS)
 
-/*
- * Futher monitor types are expected, so make this a union.
- */
 union rv_task_monitor {
-	struct da_monitor da_mon;
+	struct da_monitor	da_mon;
+	struct ltl_monitor	ltl_mon;
 };
 
 #ifdef CONFIG_RV_REACTORS
diff --git a/kernel/fork.c b/kernel/fork.c
index 735405a9c5f3..5d6c1caca702 100644
--- a/kernel/fork.c
+++ b/kernel/fork.c
@@ -2127,10 +2127,7 @@ static void copy_oom_score_adj(u64 clone_flags, struct task_struct *tsk)
 #ifdef CONFIG_RV
 static void rv_task_fork(struct task_struct *p)
 {
-	int i;
-
-	for (i = 0; i < RV_PER_TASK_MONITORS; i++)
-		p->rv[i].da_mon.monitoring = false;
+	memset(p->rv, 0, sizeof(p->rv));
 }
 #else
 #define rv_task_fork(p) do {} while (0)
diff --git a/tools/verification/ltl2ba/.gitignore b/tools/verification/ltl2ba/.gitignore
new file mode 100644
index 000000000000..9c47b9724860
--- /dev/null
+++ b/tools/verification/ltl2ba/.gitignore
@@ -0,0 +1,3 @@
+__pycache__/
+parsetab.py
+parser.out
diff --git a/tools/verification/ltl2ba/generate.py b/tools/verification/ltl2ba/generate.py
new file mode 100755
index 000000000000..52d5b3618e64
--- /dev/null
+++ b/tools/verification/ltl2ba/generate.py
@@ -0,0 +1,154 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+
+import argparse
+import ntpath
+import os
+import platform
+from pathlib import Path
+import sys
+import ltl
+
+parser = argparse.ArgumentParser(description='transform ltl file into kernel rv monitor')
+parser.add_argument('-l', "--ltl", dest="ltl", required=True)
+parser.add_argument('-n', "--model_name", dest="model_name", required=True)
+parser.add_argument('-o', "--outdir", dest="outdir", required=True)
+params = parser.parse_args()
+
+with open(params.ltl) as f:
+    atoms, graph = ltl.create_graph(f.read())
+states = []
+transitions = []
+init_conditions = []
+
+COLUMN_LIMIT = 100
+
+def build_condition_string(node: ltl.GraphNode):
+    if not node.labels:
+        return "(true)"
+
+    result = "("
+
+    first = True
+    for l in sorted(node.labels):
+        if not first:
+            result += " && "
+        result += '(' + l + ')'
+        first = False
+
+    result += ")"
+
+    return result
+
+def build_states() -> str:
+    states = ''
+    for node in graph:
+        states += "\t%s,\n" % node.name
+    return states
+
+def build_atoms() -> str:
+    global atoms
+    s = ''
+    for a in sorted(atoms):
+        s += "\t%s,\n" % a
+    return s
+
+def build_transitions() -> list[str]:
+    transitions = []
+    for node in graph:
+        transitions.append("\tcase %s:\n" % node.name)
+
+        result = ""
+        first = True
+        for o in sorted(node.outgoing):
+            if first:
+                result += "\t\tif "
+                cursor = 19
+            else:
+                result += "\t\telse if "
+                cursor = 24
+
+            condition = build_condition_string(o)
+
+            while len(condition) + cursor > COLUMN_LIMIT:
+                i = condition[:COLUMN_LIMIT - cursor].rfind(' ')
+                result += condition[:i]
+                if cursor == 19:
+                    result += '\n\t\t   '
+                elif cursor == 24:
+                    result += '\t\t\t\t'
+                else:
+                    raise ValueError()
+                condition = condition[i + 1:]
+
+            result += condition
+
+            result += '\n'
+            result += ("\t\t\tmon->state = %s;\n" % o.name)
+            first = False
+        result += "\t\telse\n\t\t\tillegal_state(task, mon);\n"
+        result += "\t\tbreak;\n"
+        transitions.append(result)
+    return transitions
+
+def build_initial_conditions() -> str:
+    result = ""
+    first = True
+
+    for node in graph:
+        if not node.init:
+            continue
+
+        if not first:
+            result += "\telse if "
+            cursor = 16
+        else:
+            result += "\tif "
+            cursor = 11
+
+        condition = build_condition_string(node)
+        while len(condition) + cursor > COLUMN_LIMIT:
+            i = condition[:COLUMN_LIMIT - cursor].rfind(' ')
+            result += condition[:i]
+            if cursor == 16:
+                result += '\n\t\t'
+            elif cursor == 11:
+                result += '\n\t   '
+            else:
+                raise ValueError()
+            condition = condition[i + 1:]
+
+        result += condition
+        result += '\n'
+        result += ("\t\tmon->state = %s;\n" % node.name)
+        first = False
+    result += "\telse\n\t\tillegal_state(task, mon);\n"
+    return result
+
+template = Path(__file__).with_name('template.h')
+out = os.path.join(params.outdir, "ba.h")
+with template.open() as template, open(out, "w") as file:
+    for line in template:
+        if line == "%%ATOM_LIST%%\n":
+            file.write(build_atoms())
+        else:
+            line = line.replace("%%MODEL_NAME%%", params.model_name)
+            file.write(line)
+
+template = Path(__file__).with_name('template.c')
+out = os.path.join(params.outdir, "ba.c")
+with template.open() as template, open(out, "w") as file:
+    for line in template:
+        if line == "%%STATE_LIST%%\n":
+            file.write(build_states())
+        elif line == "%%BUCHI_START%%\n":
+            file.write(build_initial_conditions())
+        elif line == "%%BUCHI_TRANSITIONS%%\n":
+            for t in build_transitions():
+                file.write(t)
+        elif line == "%%ERROR_MESSAGE%%\n":
+            file.write(build_error_message())
+        else:
+            line = line.replace("%%MODEL_NAME%%", params.model_name)
+            line = line.replace("%%LTL%%", params.ltl)
+            file.write(line)
diff --git a/tools/verification/ltl2ba/ltl.py b/tools/verification/ltl2ba/ltl.py
new file mode 100644
index 000000000000..aa3a11d78a8e
--- /dev/null
+++ b/tools/verification/ltl2ba/ltl.py
@@ -0,0 +1,556 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Implementation based on
+# Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996).
+# Simple On-the-fly Automatic Verification of Linear Temporal Logic.
+# https://doi.org/10.1007/978-0-387-34892-6_1
+# With extra optimizations
+
+from ply.lex import lex
+from ply.yacc import yacc
+
+# Grammar:
+# 	ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
+#
+# Operands (opd):
+# 	true, false, user-defined names
+#
+# Unary Operators (unop):
+#       always
+#       eventually
+#       not
+#
+# Binary Operators (binop):
+#       until
+#       and
+#       or
+#       imply
+#       equivalent
+
+tokens = (
+   'AND',
+   'OR',
+   'IMPLY',
+   'UNTIL',
+   'ALWAYS',
+   'EVENTUALLY',
+   'VARIABLE',
+   'LITERAL',
+   'NOT',
+   'LPAREN',
+   'RPAREN',
+   'ASSIGN',
+)
+
+t_AND     = r'and'
+t_OR      = r'or'
+t_IMPLY   = r'imply'
+t_UNTIL   = r'until'
+t_ALWAYS = r'always'
+t_EVENTUALLY = r'eventually'
+t_VARIABLE = r'[A-Z_0-9]+'
+t_LITERAL = r'true|false'
+t_NOT = r'not'
+t_LPAREN = r'\('
+t_RPAREN = r'\)'
+t_ASSIGN = r'='
+t_ignore_COMMENT = r'\#.*'
+t_ignore  = ' \t\n'
+
+def t_error(t):
+    raise ValueError("Illegal character '%s'" % t.value[0])
+
+lexer = lex()
+
+_new_name_counter = 0
+def new_name():
+    global _new_name_counter
+
+    _new_name_counter += 1
+
+    return "S" + str(_new_name_counter)
+
+class GraphNode:
+    def __init__(self, name: str, incoming: set['GraphNode'], new, old, _next):
+        self.init = False
+        self.outgoing = set()
+        self.labels = set()
+        self.incoming = incoming
+        self.name = name
+        self.new = new.copy()
+        self.old = old.copy()
+        self.next = _next.copy()
+
+    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
+                    for i in self.incoming:
+                        i.outgoing.add(nd)
+                    return node_set
+
+            new_current_node = GraphNode(new_name(), {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.name < other.name
+
+class ASTNode:
+    def __init__(self,op):
+        self.op = op
+
+    def __hash__(self):
+        return hash(self.op)
+
+    def __str__(self):
+        return str(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 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 __str__(self):
+        return "(%s %s %s)" % (self.left, self.op_str, self.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 NotImplemented
+
+    def negate(self):
+        raise NotImplemented
+
+    def _is_temporal(self):
+        raise NotImplemented
+
+    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 NotImplemented
+
+class AndOp(BinaryOp):
+    op_str = '&&'
+
+    def __init__(self, left, right):
+        super().__init__(left, right)
+
+    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.name, 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 __init__(self, left, right):
+        super().__init__(left, right)
+
+    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(new_name(), node.incoming,
+                          node.new | ({n.op.left} - node.old),
+                          node.old | {n},
+                          node.next)
+        node2 = GraphNode(new_name(), 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 __init__(self, left, right):
+        super().__init__(left, right)
+
+    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(new_name(), node.incoming,
+                          node.new | ({n.op.left} - node.old),
+                          node.old | {n},
+                          node.next | {n})
+        node2 = GraphNode(new_name(), 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 __init__(self, left, right):
+        super().__init__(left, right)
+
+    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(new_name(), node.incoming,
+                          node.new | ({n.op.right} - node.old),
+                          node.old | {n},
+                          node.next | {n})
+        node2 = GraphNode(new_name(), 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 __init__(self, left, right):
+        super().__init__(left, right)
+
+    def normalize(self):
+        # P -> Q === !P | Q
+        return OrOp(self.left.negate(), self.right)
+
+    def _is_temporal(self):
+        return False
+
+    def negate():
+        # !(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 NotImplemented
+
+    def _is_temporal(self):
+        raise NotImplemented
+
+    def is_temporal(self):
+        if self.child.op.is_temporal():
+            return True
+        return self._is_temporal()
+
+    def negate(self):
+        raise NotImplemented
+
+class EventuallyOp(UnaryOp):
+    def __init__(self, child):
+        super().__init__(child)
+
+    def __str__(self):
+        return "eventually " + str(self.child)
+
+    def normalize(self):
+        # <>F == true U F
+        return UntilOp(Literal(True), self.right)
+
+    def _is_temporal(self):
+        return True
+
+    def negate(self):
+        # !<>F == [](!F)
+        return AlwaysOp(self.right.negate()).normalize()
+
+class AlwaysOp(UnaryOp):
+    def __init__(self, child):
+        super().__init__(child)
+
+    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.left, self.right.negate()).normalize()
+
+class NotOp(UnaryOp):
+    def __init__(self, child):
+        super().__init__(child)
+
+    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 __str__(self):
+        return "mon->atoms[%s]" % self.name
+
+    def __hash__(self):
+        return hash(self.name)
+
+    def __iter__(self):
+        yield from ()
+
+    def negate(self):
+        new = ASTNode(self)
+        return NotOp(new)
+
+    def normalize(self):
+        return self
+
+    def is_temporal(self):
+        return False
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        for f in node.old:
+            if isinstance(f, NotOp) and f.op.child is n:
+                return node_set
+        node.old |= {n}
+        return node.expand(node_set)
+
+class Literal:
+    def __init__(self, value: bool):
+        self.value = value
+
+    def __iter__(self):
+        yield from ()
+
+    def __hash__(self):
+        return hash(self.value)
+
+    def __str__(self):
+        if self.value:
+            return "true"
+        return "false"
+
+    def negate(self):
+        self.value = not self.value
+        return self
+
+    def normalize(self):
+        return self
+
+    def is_temporal(self):
+        return False
+
+    @staticmethod
+    def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+        if not n.op.value:
+            return node_set
+        node.old |= {n}
+        return node.expand(node_set)
+
+def p_spec(p):
+    '''
+    spec : assign
+         | assign spec
+    '''
+    if len(p) == 3:
+        p[2].append(p[1])
+        p[0] = p[2]
+    else:
+        p[0] = [p[1]]
+
+def p_assign(p):
+    '''
+    assign : VARIABLE ASSIGN ltl
+    '''
+    p[0] = (p[1], p[3])
+
+def p_ltl(p):
+    '''
+    ltl : opd
+        | binop
+        | unop
+    '''
+    p[0] = p[1]
+
+def p_opd(p):
+    '''
+    opd : VARIABLE
+        | LITERAL
+        | LPAREN ltl RPAREN
+    '''
+    if p[1] == "true":
+        p[0] = ASTNode(Literal(True))
+    elif p[1] == "false":
+        p[0] = ASTNode(Literal(False))
+    elif p[1] == '(':
+        p[0] = p[2]
+    else:
+        p[0] = ASTNode(Variable(p[1]))
+
+def p_unop(p):
+    '''
+    unop : ALWAYS ltl
+         | EVENTUALLY ltl
+         | NOT ltl
+    '''
+    if p[1] == "always":
+        op = AlwaysOp(p[2])
+    if p[1] == "eventually":
+        op = EventuallyOp(p[2])
+    if p[1] == "not":
+        op = NotOp(p[2])
+
+    p[0] = ASTNode(op)
+
+def p_binop(p):
+    '''
+    binop : opd UNTIL ltl
+          | opd AND ltl
+          | opd OR ltl
+          | opd IMPLY ltl
+    '''
+    if p[2] == "and":
+        op = AndOp(p[1], p[3])
+    elif p[2] == "until":
+        op = UntilOp(p[1], p[3])
+    elif p[2] == "or":
+        op = OrOp(p[1], p[3])
+    elif p[2] == "imply":
+        op = ImplyOp(p[1], p[3])
+    else:
+        raise ValueError("Invalid binary operator: %s" % p[2])
+
+    p[0] = ASTNode(op)
+
+parser = yacc()
+
+def parse_ltl(s: str) -> ASTNode:
+    spec = parser.parse(s)
+
+    for assign in spec:
+        if assign[0] == "RULE":
+            rule = assign[1]
+
+    for assign in spec:
+        if assign[0] == "RULE":
+            continue
+
+        subexpr = assign[0]
+        for node in rule:
+            if isinstance(node.op, Variable) and node.op.name == subexpr:
+                node.op = assign[1].op
+
+    return rule
+
+def create_graph(s: str):
+    atoms = set()
+
+    x = parse_ltl(s)
+    for c in x:
+        c.normalize()
+        if isinstance(c.op, Variable):
+            atoms.add(c.op.name)
+
+    init = GraphNode("init", set(), set(), set(), set())
+    head = GraphNode("first", {init}, {x}, set(), set())
+    graph = head.expand(set())
+
+    for node in graph:
+        for incoming in node.incoming:
+            if incoming.name == "init":
+                node.init = True
+        for o in node.old:
+            if not o.op.is_temporal():
+                node.labels.add(str(o))
+
+    return atoms, sorted(graph)
diff --git a/tools/verification/ltl2ba/template.c b/tools/verification/ltl2ba/template.c
new file mode 100644
index 000000000000..31c5a209d71d
--- /dev/null
+++ b/tools/verification/ltl2ba/template.c
@@ -0,0 +1,131 @@
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * This file is generated, do not edit.
+ */
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+#include <trace/events/task.h>
+#include <trace/events/sched.h>
+
+#include "ba.h"
+
+static_assert(NUM_ATOM <= RV_MAX_LTL_ATOM);
+
+enum buchi_state {
+	INIT,
+%%STATE_LIST%%
+	DEAD,
+};
+
+int rv_%%MODEL_NAME%%_task_slot = RV_PER_TASK_MONITOR_INIT;
+
+static void init_monitor(struct task_struct *task)
+{
+	struct ltl_monitor *mon = rv_%%MODEL_NAME%%_get_monitor(task);
+
+	for (int i = 0; i < NUM_ATOM; ++i)
+		mon->atoms[i] = LTL_UNDETERMINED;
+	mon->state = INIT;
+}
+
+static void handle_task_newtask(void *data, struct task_struct *task, unsigned long flags)
+{
+	struct ltl_monitor *mon = rv_%%MODEL_NAME%%_get_monitor(task);
+
+	init_monitor(task);
+
+	rv_%%MODEL_NAME%%_atoms_init(task, mon);
+	rv_%%MODEL_NAME%%_atoms_fetch(task, mon);
+}
+
+int rv_%%MODEL_NAME%%_init(size_t data_size)
+{
+	struct task_struct *g, *p;
+	int ret, cpu;
+
+	if (WARN_ON(data_size > RV_MAX_DATA_SIZE))
+		return -EINVAL;
+
+	ret = rv_get_task_monitor_slot();
+	if (ret < 0)
+		return ret;
+
+	rv_%%MODEL_NAME%%_task_slot = ret;
+
+	rv_attach_trace_probe("%%MODEL_NAME%%", task_newtask, handle_task_newtask);
+
+	read_lock(&tasklist_lock);
+
+	for_each_process_thread(g, p)
+		init_monitor(p);
+
+	for_each_present_cpu(cpu)
+		init_monitor(idle_task(cpu));
+
+	read_unlock(&tasklist_lock);
+
+	return 0;
+}
+
+void rv_%%MODEL_NAME%%_destroy(void)
+{
+	rv_put_task_monitor_slot(rv_%%MODEL_NAME%%_task_slot);
+	rv_%%MODEL_NAME%%_task_slot = RV_PER_TASK_MONITOR_INIT;
+
+	rv_detach_trace_probe("%%MODEL_NAME%%", task_newtask, handle_task_newtask);
+}
+
+static void illegal_state(struct task_struct *task, struct ltl_monitor *mon)
+{
+	mon->state = INIT;
+	rv_%%MODEL_NAME%%_error(task, mon);
+}
+
+static void rv_%%MODEL_NAME%%_attempt_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+	int i;
+
+	mon = rv_%%MODEL_NAME%%_get_monitor(task);
+
+	rv_%%MODEL_NAME%%_atoms_fetch(task, mon);
+
+	for (i = 0; i < NUM_ATOM; ++i) {
+		if (mon->atoms[i] == LTL_UNDETERMINED)
+			return;
+	}
+
+%%BUCHI_START%%
+}
+
+static void rv_%%MODEL_NAME%%_step(struct task_struct *task, struct ltl_monitor *mon)
+{
+	switch (mon->state) {
+%%BUCHI_TRANSITIONS%%
+	case DEAD:
+	case INIT:
+		break;
+	default:
+		WARN_ON_ONCE(1);
+	}
+}
+
+void rv_%%MODEL_NAME%%_atom_update(struct task_struct *task, unsigned int atom, bool value)
+{
+	struct ltl_monitor *mon = rv_%%MODEL_NAME%%_get_monitor(task);
+
+	rv_%%MODEL_NAME%%_atom_set(mon, atom, value);
+
+	if (mon->state == DEAD)
+		return;
+
+	if (mon->state == INIT)
+		rv_%%MODEL_NAME%%_attempt_start(task, mon);
+	if (mon->state == INIT)
+		return;
+
+	mon->atoms[atom] = value;
+
+	rv_%%MODEL_NAME%%_atoms_fetch(task, mon);
+
+	rv_%%MODEL_NAME%%_step(task, mon);
+}
diff --git a/tools/verification/ltl2ba/template.h b/tools/verification/ltl2ba/template.h
new file mode 100644
index 000000000000..65d342891e70
--- /dev/null
+++ b/tools/verification/ltl2ba/template.h
@@ -0,0 +1,157 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * This file is generated, do not edit.
+ *
+ * This file includes necessary functions to glue the Buchi automaton and the kernel together.
+ * Some of these functions must be manually implemented (look for "Must be implemented", or just
+ * let the compiler tells you).
+ *
+ * Essentially, you need to manually define the meaning of the atomic propositions in the LTL
+ * property. The primary function for that is rv_%%MODEL_NAME%%_atom_update(), which can be called
+ * in tracepoints' handlers for example. In some specific cases where
+ * rv_%%MODEL_NAME%%_atom_update() is not convenient, rv_%%MODEL_NAME%%_atoms_fetch() can be used.
+ *
+ * rv_%%MODEL_NAME%%_init()/rv_%%MODEL_NAME%%_destroy() must be called while enabling/disabling
+ * the monitor.
+ *
+ * If the fields in struct ltl_monitor is not enough, extra custom data can be used. See
+ * rv_%%MODEL_NAME%%_get_data().
+ */
+
+#include <linux/sched.h>
+
+enum %%MODEL_NAME%%_atom {
+%%ATOM_LIST%%
+	NUM_ATOM
+};
+
+/**
+ * rv_%%MODEL_NAME%%_init
+ * @data_size:	required custom data size, can be zero
+ *
+ * Must be called while enabling the monitor
+ */
+int rv_%%MODEL_NAME%%_init(size_t data_size);
+
+/**
+ * rv_%%MODEL_NAME%%_destroy
+ *
+ * must be called while disabling the monitor
+ */
+void rv_%%MODEL_NAME%%_destroy(void);
+
+/**
+ * rv_%%MODEL_NAME%%_error - report violation of the LTL property
+ * @task:	the task violating the LTL property
+ * @mon:	the LTL monitor
+ *
+ * Must be implemented. This function should invoke the RV reactor and the monitor's tracepoints.
+ */
+void rv_%%MODEL_NAME%%_error(struct task_struct *task, struct ltl_monitor *mon);
+
+extern int rv_%%MODEL_NAME%%_task_slot;
+
+/**
+ * rv_%%MODEL_NAME%%_get_monitor - get the struct ltl_monitor of a task
+ */
+static inline struct ltl_monitor *rv_%%MODEL_NAME%%_get_monitor(struct task_struct *task)
+{
+	return &task->rv[rv_%%MODEL_NAME%%_task_slot].ltl_mon;
+}
+
+/**
+ * rv_%%MODEL_NAME%%_atoms_init - initialize the atomic propositions
+ * @task:	the task
+ * @mon:	the LTL monitor
+ *
+ * Must be implemented. This function is called during task creation, and should initialize all
+ * atomic propositions. rv_%%MODEL_NAME%%_atom_set() should be used to implement this function.
+ *
+ * This function does not have to initialize atomic propositions that are updated by
+ * rv_%%MODEL_NAME%%_atoms_fetch(), because the two functions are called together.
+ */
+void rv_%%MODEL_NAME%%_atoms_init(struct task_struct *task, struct ltl_monitor *mon);
+
+/**
+ * rv_%%MODEL_NAME%%_atoms_fetch - fetch the atomic propositions
+ * @task:	the task
+ * @mon:	the LTL monitor
+ *
+ * Must be implemented. This function is called anytime the Buchi automaton is triggered. Its
+ * intended purpose is to update the atomic propositions which are expensive to trace and can be
+ * easily read from @task. rv_%%MODEL_NAME%%_atom_set() should be used to implement this function.
+ *
+ * Using this function may cause incorrect verification result if it is important for the LTL that
+ * the atomic propositions must be updated at the correct time. Therefore, if it is possible,
+ * updating atomic propositions should be done with rv_%%MODEL_NAME%%_atom_update() instead.
+ *
+ * An example where this function is useful is with the LTL property:
+ *    always (RT imply not PAGEFAULT)
+ * (a realtime task does not raise page faults)
+ *
+ * In this example, adding tracepoints to track RT is complicated, because it is changed in
+ * differrent places (mutex's priority boosting, sched_setscheduler). Furthermore, for this LTL
+ * property, we don't care exactly when RT changes, as long as we have its correct value when
+ * PAGEFAULT==true. Therefore, it is better to update RT in rv_%%MODEL_NAME%%_atoms_fetch(), as it
+ * can easily be retrieved from task_struct.
+ *
+ * This function can be empty.
+ */
+void rv_%%MODEL_NAME%%_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon);
+
+/**
+ * rv_%%MODEL_NAME%%_atom_update - update an atomic proposition
+ * @task:	the task
+ * @atom:	the atomic proposition, one of enum %%MODEL_NAME%%_atom
+ * @value:	the new value for @atom
+ *
+ * Update an atomic proposition and trigger the Buchi atomaton to check for violation of the LTL
+ * property. This function can be called in tracepoints' handler, for example.
+ */
+void rv_%%MODEL_NAME%%_atom_update(struct task_struct *task, unsigned int atom, bool value);
+
+/**
+ * rv_%%MODEL_NAME%%_atom_get - get an atomic proposition
+ * @mon:	the monitor
+ * @atom:	the atomic proposition, one of enum %%MODEL_NAME%%_atom
+ *
+ * Returns the value of an atomic proposition.
+ */
+static inline
+enum ltl_truth_value rv_%%MODEL_NAME%%_atom_get(struct ltl_monitor *mon, unsigned int atom)
+{
+	return mon->atoms[atom];
+}
+
+/**
+ * rv_%%MODEL_NAME%%_atom_set - set an atomic proposition
+ * @mon:	the monitor
+ * @atom:	the atomic proposition, one of enum %%MODEL_NAME%%_atom
+ * @value:	the new value for @atom
+ *
+ * Update an atomic proposition without triggering the Buchi automaton. This can be useful to
+ * implement rv_%%MODEL_NAME%%_atoms_fetch() and rv_%%MODEL_NAME%%_atoms_init().
+ *
+ * Another use case for this function is when multiple atomic propositions change at the same time,
+ * because calling rv_%%MODEL_NAME%%_atom_update() (and thus triggering the Buchi automaton)
+ * multiple times may be incorrect. In that case, rv_%%MODEL_NAME%%_atom_set() can be used to avoid
+ * triggering the Buchi automaton, and rv_%%MODEL_NAME%%_atom_update() is only used for the last
+ * atomic proposition.
+ */
+static inline
+void rv_%%MODEL_NAME%%_atom_set(struct ltl_monitor *mon, unsigned int atom, bool value)
+{
+	mon->atoms[atom] = value;
+}
+
+/**
+ * rv_%%MODEL_NAME%%_get_data - get the custom data of this monitor.
+ * @mon: the monitor
+ *
+ * If this function is used, rv_%%MODEL_NAME%%_init() must have been called with a positive
+ * data_size.
+ */
+static inline void *rv_%%MODEL_NAME%%_get_data(struct ltl_monitor *mon)
+{
+	return &mon->data;
+}
