On Fri, 2025-05-09 at 10:12 +0200, Nam Cao wrote: > 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. > > For these cases, linear temporal logic is more suitable as the > specification language. > > Add support for linear temporal logic runtime verification monitor. > > For all the details, see the documentations added by this commit. > > Signed-off-by: Nam Cao <nam...@linutronix.de> > ---
I tried generating some less than trivial monitors and I'm getting a few errors, please find below some questions/comments. There are also some typos in the references. > diff --git a/Documentation/trace/rv/linear_temporal_logic.rst > b/Documentation/trace/rv/linear_temporal_logic.rst > new file mode 100644 > index 000000000000..6bf10d8e3761 > --- /dev/null > +++ b/Documentation/trace/rv/linear_temporal_logic.rst > @@ -0,0 +1,122 @@ > +Linear temporal logic > +===================== > + > +Introduction > +------------ > + > +Runtime verification monitor is a verification technique which checks that > the kernel follows a > +specification. It does so by using tracepoints to monitor the kernel's > execution trace, and > +verifying that the execution trace sastifies the specification. > + > +Initially, the specification can only be written in the form of > deterministic automaton (DA). > +However, while attempting to implement DA monitors for some complex > specifications, deterministic > +automaton is found to be inappropriate as the specification language. The > automaton is complicated, > +hard to understand, and error-prone. > + > +Thus, RV monitors based on linear temporal logic (LTL) are introduced. This > type of monitor uses LTL > +as specification instead of DA. For some cases, writing the specification as > LTL is more concise and > +intuitive. > + > +Many materials explain LTL in details. One book is:: > + > + Christel Baier **aund** Joost-Pieter Katoen: Principles of Model Checking, > The MIT Press, 2008. Typo here and also in the references at the end of the page (omitted for brevity). + Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT Press, 2008. > [...] > diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py > b/tools/verification/rvgen/rvgen/ltl2ba.py > new file mode 100644 > index 000000000000..aa5c3339aab8 > --- /dev/null > +++ b/tools/verification/rvgen/rvgen/ltl2ba.py > @@ -0,0 +1,558 @@ > +#!/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() > + > +class GraphNode: > + uid = 0 > + > + def __init__(self, incoming: set['GraphNode'], new, old, _next): > + self.init = False > + self.outgoing = set() > + self.labels = set() > + self.incoming = incoming.copy() > + self.new = new.copy() > + self.old = old.copy() > + self.next = _next.copy() > + self.id = GraphNode.uid > + GraphNode.uid += 1 > + > + def expand(self, node_set): > + if not self.new: > + for nd in node_set: > + if nd.old == self.old and nd.next == self.next: > + nd.incoming |= self.incoming > + return node_set > + > + new_current_node = GraphNode({self}, self.next, set(), > set()) > + return new_current_node.expand({self} | node_set) > + n = self.new.pop() > + return n.expand(self, node_set) > + > + def __lt__(self, other): > + return self.id < other.id > + > +class ASTNode: > + uid = 1 > + > + def __init__(self, op): > + self.op = op > + self.id = ASTNode.uid > + ASTNode.uid += 1 > + > + def __hash__(self): > + return hash(self.op) > + > + def __eq__(self, other): > + return self is other > + > + def __iter__(self): > + yield self > + yield from self.op > + > + def negate(self): > + self.op = self.op.negate() > + return self > + > + def expand(self, node, node_set): > + return self.op.expand(self, node, node_set) > + > + def __str__(self): > + if isinstance(self.op, Literal): > + return str(self.op.value) > + elif isinstance(self.op, Variable): > + return self.op.name.lower() > + return "val" + str(self.id) > + > + def normalize(self): > + # Get rid of: > + # - ALWAYS > + # - EVENTUALLY > + # - IMPLY > + # And move all the NOT to be inside > + self.op = self.op.normalize() > + return self > + > +class BinaryOp: > + op_str = "not_supported" > + > + def __init__(self, left: ASTNode, right: ASTNode): > + self.left = left > + self.right = right > + > + def __hash__(self): > + return hash((self.left, self.right)) > + > + def __iter__(self): > + yield from self.left > + yield from self.right > + > + def normalize(self): > + raise NotImplementedError > + > + def negate(self): > + raise NotImplementedError > + > + def _is_temporal(self): > + raise NotImplementedError > + > + def is_temporal(self): > + if self.left.op.is_temporal(): > + return True > + if self.right.op.is_temporal(): > + return True > + return self._is_temporal() > + > + @staticmethod > + def expand(n: ASTNode, node: GraphNode, node_set) -> > set[GraphNode]: > + raise NotImplementedError > + > +class AndOp(BinaryOp): > + op_str = '&&' > + > + def __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.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(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 __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(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 __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(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 __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(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 __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() Shouldn't this be: + return AlwaysOp(self.child.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() Shouldn't this be: + return EventuallyOp(self.child.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 __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]) Pylint is complaining about this one, wouldn't it be better changing it to an if/elif chain and addding: else: raise ValueError("Invalid unary operator: %s" % p[1]) > + > + p[0] = ASTNode(op) > + > +def p_binop(p): > + ''' > + binop : opd UNTIL ltl > + | opd AND ltl > + | opd OR ltl > + | opd IMPLY ltl > + ''' > + if p[2] == "and": > + op = AndOp(p[1], p[3]) > + elif p[2] == "until": > + op = UntilOp(p[1], p[3]) > + elif p[2] == "or": > + op = OrOp(p[1], p[3]) > + elif p[2] == "imply": > + op = ImplyOp(p[1], p[3]) > + else: > + raise ValueError("Invalid binary operator: %s" % p[2]) > + > + p[0] = ASTNode(op) > + > +parser = yacc() > + > +def parse_ltl(s: str) -> ASTNode: > + spec = parser.parse(s) > + > + subexpr = dict() > + > + for assign in spec: > + if assign[0] == "RULE": > + rule = assign[1] > + else: > + subexpr[assign[0]] = assign[1] rule may be undefined here (but I guess python will just say variable rule is undefined and it would be quite clear the ltl didn't start with a rule. I'm still getting a few more errors but my model may be to blame, still need to play a bit. Cheers, Gabriele > + > + for node in rule: > + if not isinstance(node.op, Variable): > + continue > + replace = subexpr.get(node.op.name) > + if replace is not None: > + node.op = replace.op > + > + return rule > + > +def create_graph(s: str): > + atoms = set() > + > + ltl = parse_ltl(s) > + for c in ltl: > + c.normalize() > + if isinstance(c.op, Variable): > + atoms.add(c.op.name) > + > + init = GraphNode(set(), set(), set(), set()) > + head = GraphNode({init}, {ltl}, set(), set()) > + graph = sorted(head.expand(set())) > + > + for i, node in enumerate(graph): > + # The id assignment during graph generation has gaps. > Reassign them > + node.id = i > + > + for incoming in node.incoming: > + if incoming is init: > + node.init = True > + else: > + incoming.outgoing.add(node) > + for o in node.old: > + if not o.op.is_temporal(): > + node.labels.add(str(o)) > + > + return sorted(atoms), graph, ltl > diff --git a/tools/verification/rvgen/rvgen/ltl2k.py > b/tools/verification/rvgen/rvgen/ltl2k.py > new file mode 100644 > index 000000000000..b8da9094fb4f > --- /dev/null > +++ b/tools/verification/rvgen/rvgen/ltl2k.py > @@ -0,0 +1,245 @@ > +#!/usr/bin/env python3 > +# SPDX-License-Identifier: GPL-2.0-only > + > +from pathlib import Path > +from . import generator > +from . import ltl2ba > + > +COLUMN_LIMIT = 100 > + > +def line_len(line: str) -> int: > + tabs = line.count('\t') > + return tabs * 7 + len(line) > + > +def break_long_line(line: str, indent='') -> list[str]: > + result = [] > + while line_len(line) > COLUMN_LIMIT: > + i = line[:COLUMN_LIMIT - line_len(line)].rfind(' ') > + result.append(line[:i]) > + line = indent + line[i + 1:] > + if line: > + result.append(line) > + return result > + > +def build_condition_string(node: ltl2ba.GraphNode): > + if not node.labels: > + return "(true)" > + > + result = "(" > + > + first = True > + for label in sorted(node.labels): > + if not first: > + result += " && " > + result += label > + first = False > + > + result += ")" > + > + return result > + > +def abbreviate_atoms(atoms: list[str]) -> list[str]: > + def shorten(s: str) -> str: > + skip = ["is", "by", "or", "and"] > + return '_'.join([x[:2] for x in s.lower().split('_') if x > not in skip]) > + > + abbrs = [] > + for atom in atoms: > + for i in range(len(atom), -1, -1): > + if sum(a.startswith(atom[:i]) for a in atoms) > 1: > + break > + share = atom[:i] > + unique = atom[i:] > + abbrs.append((shorten(share) + shorten(unique))) > + return abbrs > + > +class ltl2k(generator.Monitor): > + template_dir = "ltl2k" > + > + def __init__(self, file_path, MonitorType, extra_params={}): > + if MonitorType != "per_task": > + raise NotImplementedError("Only per_task monitor is > supported for LTL") > + super().__init__(extra_params) > + with open(file_path) as f: > + self.atoms, self.ba, self.ltl = > ltl2ba.create_graph(f.read()) > + self.atoms_abbr = abbreviate_atoms(self.atoms) > + self.name = extra_params.get("model_name") > + if not self.name: > + self.name = Path(file_path).stem > + > + def _fill_states(self) -> str: > + buf = [ > + "enum ltl_buchi_state {", > + ] > + > + for node in self.ba: > + buf.append("\tS%i," % node.id) > + buf.append("\tRV_NUM_BA_STATES") > + buf.append("};") > + buf.append("static_assert(RV_NUM_BA_STATES <= > RV_MAX_BA_STATES);") > + return buf > + > + def _fill_atoms(self): > + buf = ["enum ltl_atom {"] > + for a in sorted(self.atoms): > + buf.append("\tLTL_%s," % a) > + buf.append("\tLTL_NUM_ATOM") > + buf.append("};") > + buf.append("static_assert(LTL_NUM_ATOM <= > RV_MAX_LTL_ATOM);") > + return buf > + > + def _fill_atoms_to_string(self): > + buf = [ > + "static const char *ltl_atom_str(enum ltl_atom atom)", > + "{", > + "\tstatic const char *const names[] = {" > + ] > + > + for name in self.atoms_abbr: > + buf.append("\t\t\"%s\"," % name) > + > + buf.extend([ > + "\t};", > + "", > + "\treturn names[atom];", > + "}" > + ]) > + return buf > + > + def _fill_atom_values(self): > + buf = [] > + for node in self.ltl: > + if node.op.is_temporal(): > + continue > + > + if isinstance(node.op, ltl2ba.Variable): > + buf.append("\tbool %s = test_bit(LTL_%s, mon- > >atoms);" % (node, node.op.name)) > + elif isinstance(node.op, ltl2ba.AndOp): > + buf.append("\tbool %s = %s && %s;" % (node, > node.op.left, node.op.right)) > + elif isinstance(node.op, ltl2ba.OrOp): > + buf.append("\tbool %s = %s || %s;" % (node, > node.op.left, node.op.right)) > + elif isinstance(node.op, ltl2ba.NotOp): > + buf.append("\tbool %s = !%s;" % (node, > node.op.child)) > + buf.reverse() > + > + buf2 = [] > + for line in buf: > + buf2.extend(break_long_line(line, "\t ")) > + return buf2 > + > + def _fill_transitions(self): > + buf = [ > + "static void", > + "ltl_possible_next_states(struct ltl_monitor *mon, > unsigned int state, unsigned long *next)", > + "{" > + ] > + buf.extend(self._fill_atom_values()) > + buf.extend([ > + "", > + "\tswitch (state) {" > + ]) > + > + for node in self.ba: > + buf.append("\tcase S%i:" % node.id) > + > + for o in sorted(node.outgoing): > + line = "\t\tif " > + indent = "\t\t " > + > + line += build_condition_string(o) > + lines = break_long_line(line, indent) > + buf.extend(lines) > + > + buf.append("\t\t\t__set_bit(S%i, next);" % o.id) > + buf.append("\t\tbreak;") > + buf.extend([ > + "\t}", > + "}" > + ]) > + > + return buf > + > + def _fill_start(self): > + buf = [ > + "static void ltl_start(struct task_struct *task, struct > ltl_monitor *mon)", > + "{" > + ] > + buf.extend(self._fill_atom_values()) > + buf.append("") > + > + for node in self.ba: > + if not node.init: > + continue > + > + line = "\tif " > + indent = "\t " > + > + line += build_condition_string(node) > + lines = break_long_line(line, indent) > + buf.extend(lines) > + > + buf.append("\t\t__set_bit(S%i, mon->states);" % node.id) > + buf.append("}") > + return buf > + > + def fill_tracepoint_handlers_skel(self): > + buff = [] > + buff.append("static void handle_example_event(void *data, /* > XXX: fill header */)") > + buff.append("{") > + buff.append("\tltl_atom_update(task, LTL_%s, true/false);" % > self.atoms[0]) > + buff.append("}") > + buff.append("") > + return '\n'.join(buff) > + > + def fill_tracepoint_attach_probe(self): > + return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint > */, handle_example_event);" \ > + % self.name > + > + def fill_tracepoint_detach_helper(self): > + return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint > */, handle_sample_event);" \ > + % self.name > + > + def fill_atoms_init(self): > + buff = [] > + for a in self.atoms: > + buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % > a) > + return '\n'.join(buff) > + > + def fill_model_h(self): > + buf = [ > + "/* SPDX-License-Identifier: GPL-2.0 */", > + "", > + "#include <linux/rv.h>", > + "", > + "#define MONITOR_NAME " + self.name, > + "" > + ] > + > + buf.extend(self._fill_atoms()) > + buf.append('') > + > + buf.extend(self._fill_atoms_to_string()) > + buf.append('') > + > + buf.extend(self._fill_states()) > + buf.append('') > + > + buf.extend(self._fill_start()) > + buf.append('') > + > + buf.extend(self._fill_transitions()) > + buf.append('') > + > + return '\n'.join(buf) > + > + def fill_monitor_class_type(self): > + return "LTL_MON_EVENTS_ID" > + > + def fill_monitor_class(self): > + return "ltl_monitor_id" > + > + def fill_main_c(self): > + main_c = super().fill_main_c() > + main_c = main_c.replace("%%ATOMS_INIT%%", > self.fill_atoms_init()) > + > + return main_c > diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c > b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c > new file mode 100644 > index 000000000000..2f3c4d642746 > --- /dev/null > +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c > @@ -0,0 +1,102 @@ > +// SPDX-License-Identifier: GPL-2.0 > +#include <linux/ftrace.h> > +#include <linux/tracepoint.h> > +#include <linux/kernel.h> > +#include <linux/module.h> > +#include <linux/init.h> > +#include <linux/rv.h> > +#include <rv/instrumentation.h> > + > +#define MODULE_NAME "%%MODEL_NAME%%" > + > +/* > + * XXX: include required tracepoint headers, e.g., > + * #include <trace/events/sched.h> > + */ > +#include <rv_trace.h> > +%%INCLUDE_PARENT%% > + > +/* > + * This is the self-generated part of the monitor. Generally, there > is no need > + * to touch this section. > + */ > +#include "%%MODEL_NAME%%.h" > +#include <rv/ltl_monitor.h> > + > +static void ltl_atoms_fetch(struct task_struct *task, struct > ltl_monitor *mon) > +{ > + /* > + * This is called everytime the Buchi automaton is > triggered. > + * > + * This function could be used to fetch the atomic > propositions which are expensive to > + * trace. It is possible only if the atomic proposition does > not need to be updated at > + * precise time. > + * > + * It is recommended to use tracepoints and > ltl_atom_update() instead. > + */ > +} > + > +static void ltl_atoms_init(struct task_struct *task, struct > ltl_monitor *mon, bool task_creation) > +{ > + /* > + * This should initialize as many atomic propositions as > possible. > + * > + * @task_creation indicates whether the task is being > created. This is false if the task is > + * already running before the monitor is enabled. > + */ > +%%ATOMS_INIT%% > +} > + > +/* > + * This is the instrumentation part of the monitor. > + * > + * This is the section where manual work is required. Here the > kernel events > + * are translated into model's event. > + */ > +%%TRACEPOINT_HANDLERS_SKEL%% > +static int enable_%%MODEL_NAME%%(void) > +{ > + int retval; > + > + retval = ltl_monitor_init(); > + if (retval) > + return retval; > + > +%%TRACEPOINT_ATTACH%% > + > + return 0; > +} > + > +static void disable_%%MODEL_NAME%%(void) > +{ > +%%TRACEPOINT_DETACH%% > + > + ltl_monitor_destroy(); > +} > + > +/* > + * This is the monitor register section. > + */ > +static struct rv_monitor rv_%%MODEL_NAME%% = { > + .name = "%%MODEL_NAME%%", > + .description = "%%DESCRIPTION%%", > + .enable = enable_%%MODEL_NAME%%, > + .disable = disable_%%MODEL_NAME%%, > +}; > + > +static int __init register_%%MODEL_NAME%%(void) > +{ > + return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); > +} > + > +static void __exit unregister_%%MODEL_NAME%%(void) > +{ > + rv_unregister_monitor(&rv_%%MODEL_NAME%%); > +} > + > +module_init(register_%%MODEL_NAME%%); > +module_exit(unregister_%%MODEL_NAME%%); > + > +MODULE_LICENSE("GPL"); > +MODULE_AUTHOR(/* TODO */); > +MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); > diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h > b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h > new file mode 100644 > index 000000000000..49394c4b0f1c > --- /dev/null > +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h > @@ -0,0 +1,14 @@ > +/* SPDX-License-Identifier: GPL-2.0 */ > + > +/* > + * Snippet to be included in rv_trace.h > + */ > + > +#ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%% > +DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%, > + TP_PROTO(struct task_struct *task, char *states, char > *atoms, char *next), > + TP_ARGS(task, states, atoms, next)); > +DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%, > + TP_PROTO(struct task_struct *task), > + TP_ARGS(task)); > +#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */
