Message-ID: <817f3cb62b2632286e5c6fffde3163592a110eee.camel@redhat.com>
Date: Fri, 09 May 2025 16:50:29 +0200
From: Gabriele Monaco <gmonaco@...hat.com>
To: Nam Cao <namcao@...utronix.de>
Cc: john.ogness@...utronix.de, Steven Rostedt <rostedt@...dmis.org>, 
	linux-trace-kernel@...r.kernel.org, linux-kernel@...r.kernel.org
Subject: Re: [PATCH v7 13/22] rv: Add support for LTL monitors

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 <namcao@...utronix.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%% */

Powered by blists - more mailing lists