* [PATCH v2 02/13] verification/rvgen: Introduce a parse tree for automata using Lark
From: Nam Cao @ 2026-05-28 8:27 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
The DOT parsing scripts directly parse the raw text and they are quite
fragile. If the input dot files' formats are slightly changed (for
instance, by breaking long some lines which is allowed by the DOT language
defined by graphviz), the scripts would fail.
To make the scripts robust, the parser should be implemented based on the
dot language specification, not based on how the existing dot files look.
As a first step, use Lark to implement a Parser based on the graphviz dot
language specification. The resulting parse tree is not used yet, but the
existing scripts will be converted one by one to use this new parse tree in
the follow-up commits.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v2:
- switch to use Lark's CNAME for identifier [Wander]
- switch to use Lark's ESCAPED_STRING for string [Sashiko]
- clean up variable name shadowing [Sashiko]
- Properly catch Lark exception
---
tools/verification/rvgen/rvgen/automata.py | 186 +++++++++++++++++++++
1 file changed, 186 insertions(+)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index b9f8149f7118..8649d982383d 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -13,6 +13,191 @@ import re
from typing import Iterator
from itertools import islice
+import lark
+
+class ParseTree:
+ # based on https://graphviz.org/doc/info/lang.html
+ # with the irrelevant stuffs (port and compass) removed
+ grammar = r'''
+ start: "strict"? ("graph" | "digraph") ID? "{" stmt_list "}"
+
+ stmt_list: (stmt ";"? stmt_list)?
+
+ stmt: node_stmt
+ | edge_stmt
+ | attr_stmt
+ | ID "=" ID
+ | subgraph
+
+ attr_stmt: attr_type attr_list
+
+ attr_type: "graph" -> graph
+ | "node" -> node
+ | "edge" -> edge
+
+ attr_list: "[" a_list? "]" attr_list?
+
+ a_list: ID "=" ID (";" | ",")? a_list?
+
+ edge_stmt: (node_id | subgraph) edgerhs attr_list?
+
+ edgerhs: edgeop (node_id | subgraph) edgerhs?
+
+ edgeop: "->" | "--"
+
+ node_stmt: node_id attr_list?
+
+ node_id: ID
+
+ subgraph: ("subgraph" ID?)? "{" stmt_list "}"
+
+ ID: CNAME
+ | /-?(\.[0-9]+|[0-9]+(\.[0-9]*))/
+ | ESCAPED_STRING
+
+ %import common.CNAME
+ %import common.ESCAPED_STRING
+ %import common.WS
+ %ignore WS
+ '''
+
+ @staticmethod
+ def parse_edge(tree: lark.Tree) -> tuple[str, str]:
+ # only support a simple node-to-node edge
+ nodes = []
+ for node in tree.iter_subtrees_topdown():
+ if node.data == "node_id":
+ nodes.append(node.children[0].strip('"'))
+
+ if len(nodes) != 2:
+ raise AutomataError("Only state-to-state transition is supported")
+
+ return tuple(nodes)
+
+ class ParseNodes(lark.visitors.Visitor):
+ def __init__(self, *args, **kwargs):
+ self.nodes = set()
+ super().__init__(*args, **kwargs)
+
+ def node_stmt(self, tree):
+ node_id = tree.children[0]
+ node = node_id.children[0].strip('"')
+ self.nodes.add(node)
+
+ class ParseEdges(lark.visitors.Visitor):
+ def __init__(self, *args, **kwargs):
+ self.edges = set()
+ super().__init__(*args, **kwargs)
+
+ def edge_stmt(self, tree):
+ edge = ParseTree.parse_edge(tree)
+ self.edges.add(edge)
+
+ class ParseAttributes(lark.visitors.Interpreter):
+ def __init__(self, *args, **kwargs):
+ '''
+ Stacks of default attributes. [0] is the default
+ attributes for the outermost scope, while [-1] is the
+ default attributes for the current scope.
+ '''
+ self.default_node_attrs = [{}]
+ self.default_edge_attrs = [{}]
+
+ self.node_attrs = {}
+ self.edge_attrs = {}
+
+ super().__init__(*args, **kwargs)
+
+ @staticmethod
+ def __get_attrs(stmt: lark.Tree) -> dict[str, str]:
+ attrs = {}
+
+ for node in stmt.iter_subtrees():
+ if node.data == "a_list":
+ attrs[node.children[0]] = node.children[1].strip('"')
+
+ return attrs
+
+
+ def subgraph(self, tree):
+ # We are entering a new scope, inherit the default
+ # attributes of the outer scope
+ self.default_node_attrs.append(self.default_node_attrs[-1].copy())
+ self.default_edge_attrs.append(self.default_edge_attrs[-1].copy())
+
+ children = self.visit_children(tree)
+
+ # Exiting the scope
+ del self.default_node_attrs[-1]
+ del self.default_edge_attrs[-1]
+
+ return children
+
+ def node_stmt(self, tree):
+ node_id = tree.children[0]
+ node = node_id.children[0].strip('"')
+
+ attrs = self.default_node_attrs[-1].copy()
+ attrs |= self.__get_attrs(tree)
+
+ if attrs:
+ if node in self.node_attrs:
+ self.node_attrs[node] = attrs | self.node_attrs[node]
+ else:
+ self.node_attrs[node] = attrs
+
+ return self.visit_children(tree)
+
+ def edge_stmt(self, tree):
+ edge = ParseTree.parse_edge(tree)
+
+ attrs = self.default_edge_attrs[-1].copy()
+ attrs |= self.__get_attrs(tree)
+
+ if attrs:
+ if edge in self.edge_attrs:
+ self.edge_attrs[edge] = attrs | self.edge_attrs[edge]
+ else:
+ self.edge_attrs[edge] = attrs
+
+ return self.visit_children(tree)
+
+ def attr_stmt(self, tree):
+ attr_type = tree.children[0].data
+ attrs = self.__get_attrs(tree)
+
+ if attr_type == "node":
+ self.default_node_attrs[-1] |= attrs
+ elif attr_type == "edge":
+ self.default_edge_attrs[-1] |= attrs
+ else:
+ # graph attributes are irrelevant
+ pass
+
+ self.visit_children(tree)
+
+ def __init__(self, dot_file):
+ parser = lark.Lark(self.grammar, parser='lalr')
+ node_parser = self.ParseNodes()
+ edge_parser = self.ParseEdges()
+ attributes_parser = self.ParseAttributes()
+
+ try:
+ with open(dot_file, "r") as f:
+ tree = parser.parse(f.read())
+ attributes_parser.visit(tree)
+ node_parser.visit(tree)
+ edge_parser.visit(tree)
+ except OSError as exc:
+ raise AutomataError(exc.strerror) from exc
+ except lark.exceptions.UnexpectedInput as exc:
+ raise AutomataError(str(exc))
+
+ self.nodes = node_parser.nodes
+ self.edges = edge_parser.edges
+ self.node_attrs = attributes_parser.node_attrs
+ self.edge_attrs = attributes_parser.edge_attrs
+
class _ConstraintKey:
"""Base class for constraint keys."""
@@ -66,6 +251,7 @@ class Automata:
self.__dot_path = file_path
self.name = model_name or self.__get_model_name()
self.__dot_lines = self.__open_dot()
+ self.__parse_tree = ParseTree(file_path)
self.states, self.initial_state, self.final_states = self.__get_state_variables()
self.env_types = {}
self.env_stored = set()
--
2.47.3
^ permalink raw reply related
* [PATCH v2 01/13] verification/rvgen: Switch LTL parser to Lark
From: Nam Cao @ 2026-05-28 8:27 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
The LTL parser is built using Ply. However, Ply is no longer
maintained [1].
Switch to use Lark instead. In addition to being actively maintained, Lark
also offers additional features (namely, automatically creating the
abstract syntax tree) which make the parser simpler.
Link: https://github.com/dabeaz/ply/commit/9d7c40099e23ff78f9d86ef69a26c1e8a83e706a [1]
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v2:
- fix identifier starting with a digit is allowed [Wander]
- fixup ast node uid [Gabriele]
- Fix up Literal AST node construction [Wander, Sashiko]
- FIx up unary op error message [Sashiko]
- Add nice exception handling [Gabriele]
---
tools/verification/rvgen/__main__.py | 5 +-
tools/verification/rvgen/rvgen/ltl2ba.py | 202 +++++++++--------------
2 files changed, 82 insertions(+), 125 deletions(-)
diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 5c923dc10d0f..0915cf86e43b 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -14,6 +14,7 @@ if __name__ == '__main__':
from rvgen.container import Container
from rvgen.ltl2k import ltl2k
from rvgen.automata import AutomataError
+ from rvgen.ltl2ba import LTLError
import argparse
import sys
@@ -57,8 +58,8 @@ if __name__ == '__main__':
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)
+ except (AutomataError, LTLError) as e:
+ print(f"There was an error processing {params.spec}:\n{e}", file=sys.stderr)
sys.exit(1)
print(f"Writing the monitor into the directory {monitor.name}")
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index 016e7cf93bbb..7cebda61bce8 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -7,9 +7,7 @@
# 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
+import lark
# Grammar:
# ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
@@ -30,42 +28,41 @@ from .automata import AutomataError
# 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()
+GRAMMAR = r'''
+start: assign+
+
+assign: VARIABLE "=" _ltl
+
+_ltl: _opd | binop | unop
+
+_opd : VARIABLE
+ | LITERAL
+ | "(" _ltl ")"
+
+unop: UNOP _ltl
+UNOP: "always"
+ | "eventually"
+ | "next"
+ | "not"
+
+binop: _opd BINOP _ltl
+BINOP: "until"
+ | "and"
+ | "or"
+ | "imply"
+
+VARIABLE: /[A-Z_][A-Z0-9_]*/
+LITERAL: "true" | "false"
+
+COMMENT: "#" /.*/ "\n"
+%ignore COMMENT
+
+%import common.WS
+%ignore WS
+'''
+
+class LTLError(Exception):
+ "Exception raised for malformed linear temporal logic"
class GraphNode:
uid = 0
@@ -97,7 +94,7 @@ class GraphNode:
return self.id < other.id
class ASTNode:
- uid = 1
+ uid = 0
def __init__(self, op):
self.op = op
@@ -433,90 +430,49 @@ class Literal:
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()
+class Transform(lark.visitors.Transformer):
+ def unop(self, node):
+ if node[0] == "always":
+ return ASTNode(AlwaysOp(node[1]))
+ if node[0] == "eventually":
+ return ASTNode(EventuallyOp(node[1]))
+ if node[0] == "next":
+ return ASTNode(NextOp(node[1]))
+ if node[0] == "not":
+ return ASTNode(NotOp(node[1]))
+ raise ValueError("Unknown operator %s" % node[0])
+
+ def binop(self, node):
+ if node[1] == "until":
+ return ASTNode(UntilOp(node[0], node[2]))
+ if node[1] == "and":
+ return ASTNode(AndOp(node[0], node[2]))
+ if node[1] == "or":
+ return ASTNode(OrOp(node[0], node[2]))
+ if node[1] == "imply":
+ return ASTNode(ImplyOp(node[0], node[2]))
+ raise ValueError("Unknown operator %s" % node[1])
+
+ def VARIABLE(self, args):
+ return ASTNode(Variable(args))
+
+ def LITERAL(self, args):
+ return ASTNode(Literal(args == "true"))
+
+ def start(self, node):
+ return node
+
+ def assign(self, node):
+ return node[0].op.name, node[1]
+
+parser = lark.Lark(GRAMMAR)
def parse_ltl(s: str) -> ASTNode:
- spec = parser.parse(s)
+ try:
+ spec = parser.parse(s)
+ except lark.exceptions.UnexpectedInput as e:
+ raise LTLError(str(e))
+ spec = Transform().transform(spec)
rule = None
subexpr = {}
@@ -528,7 +484,7 @@ def parse_ltl(s: str) -> ASTNode:
subexpr[assign[0]] = assign[1]
if rule is None:
- raise AutomataError("Please define your specification in the \"RULE = <LTL spec>\" format")
+ raise LTLError("Please define your specification in the \"RULE = <LTL spec>\" format")
for node in rule:
if not isinstance(node.op, Variable):
--
2.47.3
^ permalink raw reply related
* [PATCH v2 03/13] verification/rvgen: Implement state and transition parser based on Lark
From: Nam Cao @ 2026-05-28 8:27 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
The DOT parsing scripts directly parse the raw text and they are quite
fragile. If the input dot files' formats are slightly changed (for
instance, by breaking long some lines which is allowed by the DOT
language), the scripts would fail.
Prepare to move away from the raw text processing, implement parsers based
on Lark which parse states, transitions and constraints.
The parse results are not used yet. The existing scripts will be converted
one by one to them, and the raw text processing will eventually be removed.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v2:
- fixup guard grammar [Gabriele]
- fixup inconsistent types in a list [Wander]
- compiling the parsers only once to avoid overhead [Sashiko]
- fix up the signature of State.__init__() [Sashiko]
- gracefully handle node statement without label [Sashiko]
- lark parse exception handling
---
tools/verification/rvgen/rvgen/automata.py | 216 +++++++++++++++++++++
1 file changed, 216 insertions(+)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 8649d982383d..b86275e7bf28 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -198,6 +198,164 @@ class ParseTree:
self.node_attrs = attributes_parser.node_attrs
self.edge_attrs = attributes_parser.edge_attrs
+class ConstraintCondition:
+ def __init__(self, env: str, op: str, val: str, unit=None):
+ self.env = env
+ self.op = op
+ self.val = val
+ self.unit = unit
+ if unit is None:
+ # try to infer unit from constants or parameters
+ val_for_unit = val.lower().replace("()", "")
+ if val_for_unit.endswith("_ns"):
+ self.unit = "ns"
+ if val_for_unit.endswith("_jiffies"):
+ self.unit = "j"
+
+class ConstraintRule:
+ grammar = r'''
+ rule: condition (OP condition)*
+
+ OP: "&&" | "||"
+
+ condition: ENV CMP_OP VAL UNIT?
+
+ ENV: CNAME
+
+ CMP_OP: "==" | "<=" | "<" | ">=" | ">"
+
+ VAL: /[0-9]+/
+ | /[A-Z_]+\(\)/
+ | /[A-Z_]+/
+ | /[a-z_]+\(\)/
+ | /[a-z_]+/
+
+ UNIT: "ns" | "us" | "ms" | "s"
+ '''
+
+ def __init__(self, c: ConstraintCondition):
+ '''
+ A list of pairs of
+ - the condition (e.g. is_constr_dl == 1)
+ - the logical operator ("||" or "&&") combining this
+ condition with the next one if it exists, otherwise None
+
+ TODO: Perhaps use an abstract syntax tree instead, because
+ this representation cannot capture precedence
+ '''
+ self.rules = [[c, None]]
+
+ def chain(self, op: str, c: ConstraintCondition):
+ self.rules[-1][1] = op
+ self.rules.append([c, None])
+
+class ConstraintReset:
+ def __init__(self, env):
+ self.env = env
+
+class StateLabelParser:
+ grammar = r'''
+ label: CNAME ("\\n" condition)?
+
+ %import common.CNAME
+ %import common.WS
+ %ignore WS
+ ''' + ConstraintRule.grammar
+
+ parser = lark.Lark(grammar, parser='lalr', start="label")
+
+ def __init__(self, label: str):
+ try:
+ tree = self.parser.parse(label)
+ except lark.exceptions.UnexpectedInput as exc:
+ raise(AutomataError(f"Unrecognised state \"{label}\"\n{exc}"))
+
+ self.state = tree.children[0]
+ self.constraint = None
+
+ if len(tree.children) == 2:
+ self.constraint = ConstraintCondition(*tree.children[1].children)
+ if self.constraint.op not in ("<", "<="):
+ raise AutomataError("State constraints must be clock expirations like"
+ f" clk<N ({label})")
+
+class EventLabelParser:
+ grammar = r'''
+ events: event ("\\n" event)*
+
+ event: name (";" guard)?
+
+ guard: reset
+ | rule
+ | rule ";" reset
+ | reset ";" rule
+
+ name: CNAME
+
+ reset: "reset" "(" ENV ")"
+
+ %import common.CNAME
+ %import common.WS
+ %ignore WS
+ ''' + ConstraintRule.grammar
+
+ parser = lark.Lark(grammar, parser='lalr', start="events")
+
+ class GetEvents(lark.visitors.Transformer):
+ def guard(self, args):
+ reset = None
+ rule = None
+ for arg in args:
+ if arg.data == "reset":
+ reset = ConstraintReset(arg.children[0])
+ elif arg.data == "rule":
+ conditions = arg.children
+ rule = ConstraintRule(conditions[0])
+ for i in range(1, len(conditions), 2):
+ rule.chain(conditions[i], conditions[i + 1])
+ return reset, rule
+
+ def OP(self, args):
+ return args
+
+ def condition(self, args):
+ return ConstraintCondition(*args)
+
+ def event(self, args):
+ assert(len(args) <= 2)
+ name = args[0]
+ rule, reset = None, None
+ if len(args) == 2:
+ reset, rule = args[1]
+ return name, reset, rule
+
+ def events(self, args):
+ return args
+
+ def name(self, args):
+ return args[0]
+
+ def __init__(self, label: str):
+ try:
+ tree = self.parser.parse(label)
+ self.events = self.GetEvents().transform(tree)
+ except lark.exceptions.UnexpectedInput as exc:
+ raise(AutomataError(f"Unrecognised event \"{label}\"\n{exc}"))
+
+class Transition:
+ def __init__(self, src: str, dst: str, event: str,
+ reset: ConstraintReset, rule: ConstraintRule):
+ self.src = src
+ self.dst = dst
+ self.event = event
+ self.rule = rule
+ self.reset = reset
+
+class State:
+ def __init__(self, name: str, inv: ConstraintCondition):
+ self.name = name
+ self.inv = inv
+
class _ConstraintKey:
"""Base class for constraint keys."""
@@ -252,6 +410,8 @@ class Automata:
self.name = model_name or self.__get_model_name()
self.__dot_lines = self.__open_dot()
self.__parse_tree = ParseTree(file_path)
+ self.transitions = self.__parse_transitions()
+ self._states, self._initial_state, self._final_states = self.__parse_states()
self.states, self.initial_state, self.final_states = self.__get_state_variables()
self.env_types = {}
self.env_stored = set()
@@ -327,6 +487,62 @@ class Automata:
return cursor
+ def __parse_transitions(self):
+ transitions = []
+
+ for edge in self.__parse_tree.edges:
+ attr = self.__parse_tree.edge_attrs.get(edge)
+ if not attr:
+ continue
+
+ label = attr.get("label")
+
+ src, dst = edge
+
+ parser = EventLabelParser(label)
+ for event, reset, rule in parser.events:
+ transitions.append(Transition(src, dst, event, reset, rule))
+
+ transitions.sort(key=lambda t : (t.src, t.event))
+ return transitions
+
+ def __parse_states(self):
+ initial_state = ""
+ states = []
+ final_states = []
+
+ for node in self.__parse_tree.nodes:
+ attr = self.__parse_tree.node_attrs[node]
+ label = attr.get("label")
+
+ if node.startswith(Automata.init_marker):
+ initial_state = node[len(Automata.init_marker):]
+
+ if not label:
+ continue
+
+ parser = StateLabelParser(label)
+ state = State(parser.state, parser.constraint)
+
+ states.append(state)
+
+ shape = attr.get("shape")
+ if shape in ("doublecircle", "ellipse"):
+ final_states.append(state)
+
+
+ initial_state = next((s for s in states if s.name == initial_state), None)
+ if not initial_state:
+ raise AutomataError("The automaton doesn't have an initial state")
+
+ if not final_states:
+ final_states.append(initial_state)
+
+ states.remove(initial_state)
+ states.sort(key=lambda s : s.name)
+ states.insert(0, initial_state)
+ return states, initial_state, final_states
+
def __get_state_variables(self) -> tuple[list[str], str, list[str]]:
# wait for node declaration
states = []
--
2.47.3
^ permalink raw reply related
* [PATCH v2 04/13] verification/rvgen: Convert __fill_verify_invariants_func() to Lark
From: Nam Cao @ 2026-05-28 8:27 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
Convert __fill_verify_invariants_func() to use the parsed states
information from Lark, prepare to remove the old raw text parsing code.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v2: fix up __start_to_invariant_check()'s signature [Sashiko]
---
tools/verification/rvgen/rvgen/dot2k.py | 32 ++++++++++++++++---------
1 file changed, 21 insertions(+), 11 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index e6f476b903b0..a344cbbcb346 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -12,6 +12,7 @@ from collections import deque
from .dot2c import Dot2c
from .generator import Monitor
from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
+from .automata import ConstraintRule, ConstraintCondition
class dot2k(Monitor, Dot2c):
@@ -177,6 +178,14 @@ class ha2k(dot2k):
raise AutomataError("Detected deterministic automaton, use the 'da' class")
self.trace_h = self._read_template_file("trace_hybrid.h")
self.__parse_constraints()
+ self.has_invariant = False
+ self.has_guard = False
+ for state in self._states:
+ if state.inv:
+ self.has_invariant = True
+ for transition in self.transitions:
+ if transition.rule or transition.reset:
+ self.has_guard = True
def fill_monitor_class_type(self) -> str:
if self._is_id_monitor():
@@ -218,14 +227,13 @@ class ha2k(dot2k):
assert env.rstrip(f"_{self.name}") in self.envs
return env
- def __start_to_invariant_check(self, constr: str) -> str:
+ def __start_to_invariant_check(self, inv: ConstraintCondition) -> str:
# by default assume the timer has ns expiration
- env = self.__get_constraint_env(constr)
clock_type = "ns"
- if self.env_types.get(env.rstrip(f"_{self.name}")) == "j":
+ if inv.unit == "j":
clock_type = "jiffy"
- return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)"
+ return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns)"
def __start_to_conv(self, constr: str) -> str:
"""
@@ -320,20 +328,22 @@ class ha2k(dot2k):
self.invariants[key] = rules[0]
def __fill_verify_invariants_func(self) -> list[str]:
- buff = []
- if not self.invariants:
+ if not self.has_invariant:
return []
- buff.append(
+ buff = [
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})")
+ for state in self._states:
+ if not state.inv:
+ continue
+
+ check_str = self.__start_to_invariant_check(state.inv)
+ buff.append(f"\t{_else}if (curr_state == {state.name}{self.enum_suffix})")
buff.append(f"\t\t{check_str};")
_else = "else "
--
2.47.3
^ permalink raw reply related
* [PATCH v2 05/13] verification/rvgen: Convert __fill_setup_invariants_func() to Lark
From: Nam Cao @ 2026-05-28 8:27 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
Prepare for self.invariants and __parse_constraints() to be removed.
convert __fill_setup_invariants_func() to use the new parsed states from
Lark.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v2: add missing time conversion [Sashiko]
---
tools/verification/rvgen/rvgen/dot2k.py | 44 ++++++++++++++++++++-----
1 file changed, 35 insertions(+), 9 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index a344cbbcb346..d9f8e1c7737a 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -250,6 +250,26 @@ class ha2k(dot2k):
return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.enum_suffix},"
f" {value}, time_ns)")
+ def __parse_invariant(self, inv):
+ # by default assume the timer has ns expiration
+ clock_type = "ns"
+ if inv.unit == "j":
+ clock_type = "jiffy"
+
+ env = inv.env + self.enum_suffix
+ val = inv.val.replace("()", "(ha_mon)")
+
+ match inv.unit:
+ case "us":
+ val *= 10**3
+ case "ms":
+ val *= 10**6
+ case "s":
+ val *= 10**9
+
+ return (f"ha_start_timer_{clock_type}(ha_mon, {env},"
+ f" {val}, time_ns)")
+
def __format_guard_rules(self, rules: list[str]) -> list[str]:
"""
Merge guard constraints as a single C return statement.
@@ -463,15 +483,14 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
return conflict_guards, conflict_invs
def __fill_setup_invariants_func(self) -> list[str]:
- buff = []
- if not self.invariants:
+ if not self.has_invariant:
return []
- buff.append(
+ buff = [
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}"
@@ -480,13 +499,20 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
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};")
+ for state in self._states:
+ inv = state.inv
+ if not inv:
+ continue
+ inv = self.__parse_invariant(inv)
+ buff.append(f"\t{_else}if (next_state == {state.name}{self.enum_suffix})")
+ buff.append(f"\t\t{inv};")
_else = "else "
- for state in self.invariants:
- buff.append(f"\telse if (curr_state == {self.states[state]}{self.enum_suffix})")
+ for state in self._states:
+ inv = state.inv
+ if not inv:
+ continue
+ buff.append(f"\telse if (curr_state == {state.name}{self.enum_suffix})")
buff.append("\t\tha_cancel_timer(ha_mon);")
buff.append("}\n")
--
2.47.3
^ permalink raw reply related
* [PATCH v2 06/13] verification/rvgen: Convert __fill_verify_guards_func() to Lark
From: Nam Cao @ 2026-05-28 8:27 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
Prepare to remove self.guards and self.__parse_constraints(), convert
__fill_verify_guards_func() to use the parsed transitions from Lark.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v2:
- fix up the ';' separator [Gabriele]
- make return type consistent with the function's signature [Wander]
- fix up __parse_guard_rule()'s signature
---
tools/verification/rvgen/rvgen/dot2k.py | 38 +++++++++++++++++++------
1 file changed, 30 insertions(+), 8 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index d9f8e1c7737a..ebaa6c9135c2 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -221,6 +221,19 @@ class ha2k(dot2k):
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 __parse_guard_rule(self, rule) -> list[str]:
+ buff = []
+ for c, sep in rule.rules:
+ env = c.env + self.enum_suffix
+ op = c.op
+ val = self.__adjust_value(c.val, c.unit)
+
+ cond = f"ha_get_env(ha_mon, {env}, time_ns) {op} {val}"
+ if sep:
+ cond += f" {sep}"
+ buff.append(cond)
+ return buff
+
def __get_constraint_env(self, constr: str) -> str:
"""Extract the second argument from an ha_ function"""
env = constr.split("(")[1].split()[1].rstrip(")").rstrip(",")
@@ -287,7 +300,7 @@ class ha2k(dot2k):
rules = invalid_checks + rules
separator = "\n\t\t " if sum(len(r) for r in rules) > 80 else " "
- return ["res = " + separator.join(rules)]
+ return ["res = " + separator.join(rules) + ";"]
def __validate_constraint(self, key: tuple[int, int] | int, constr: str,
rule, reset) -> None:
@@ -406,7 +419,8 @@ f"""static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
def __fill_verify_guards_func(self) -> list[str]:
buff = []
- if not self.guards:
+
+ if not self.has_guard:
return []
buff.append(
@@ -418,14 +432,22 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
""")
_else = ""
- for edge, constr in sorted(self.guards.items()):
+ for transition in self.transitions:
+ if not transition.rule and not transition.reset:
+ continue
+
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:
+ f"{transition.src}{self.enum_suffix} && "
+ f"event == {transition.event}{self.enum_suffix})")
+ rule = transition.rule
+ reset = transition.reset
+ if rule and reset:
buff[-1] += " {"
- buff += [f"\t\t{c};" for c in constr.split(";")]
- if constr.count(";") > 0:
+ if rule:
+ buff.append("\t\t" + self.__format_guard_rules(self.__parse_guard_rule(rule))[0])
+ if reset:
+ buff.append(f"\t\tha_reset_env(ha_mon, {reset.env}{self.enum_suffix}, time_ns);")
+ if rule and reset:
_else = "} else "
else:
_else = "else "
--
2.47.3
^ permalink raw reply related
* [PATCH v2 08/13] verification/rvgen: Simplify the generation for clock variables
From: Nam Cao @ 2026-05-28 8:27 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
Hybrid automata monitors's clock variables have been changed to have
only a single representation. Now there is no need to generate code to
convert between the two representations.
Delete __fill_convert_inv_guard_func() and its associates. Update
__start_to_invariant_check() to how invariants now work.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v2:
- add missing __adjust_value() in __start_to_invariant_check() [Sashiko]
- remove obsolete comment about dual clock representation [Sashiko]
---
tools/verification/rvgen/rvgen/dot2k.py | 96 +------------------------
1 file changed, 3 insertions(+), 93 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index ebaa6c9135c2..3aee2e44ba7d 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -246,7 +246,9 @@ class ha2k(dot2k):
if inv.unit == "j":
clock_type = "jiffy"
- return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns)"
+ value = self.__adjust_value(inv.val, inv.unit)
+
+ return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {value})"
def __start_to_conv(self, constr: str) -> str:
"""
@@ -383,40 +385,6 @@ f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
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 = []
@@ -456,54 +424,6 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
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]:
if not self.has_invariant:
return []
@@ -554,16 +474,9 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
* 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()
@@ -576,9 +489,6 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
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, "
--
2.47.3
^ permalink raw reply related
* [PATCH v2 07/13] rv: Simply hybrid automata monitors's clock variables
From: Nam Cao @ 2026-05-28 8:27 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
Hybrid automata monitors's clock variables have two different
representations:
- The invariant representation, which is the timestamp when the invariant
expires
- The guard representation, which is the timestamp when the clock is last
reset
This dual representation makes the logic quite difficult to follow (well,
at least for me). It also complicates the monitors and the generation tool,
as it requires conversion back and forth between the representation.
Simplify by using the clock variables for a single purpose: storing the
time stamp since the clock is last reset.
This also allows simplifying rvgen, which will be done in a follow-up
commit.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v2:
- fix up invariant check when the env is not initialized [Gabriele]
- keep the two invariant check functions consistent [Gabriele]
- fix build failure [Gabriele, Sashiko]
---
include/rv/ha_monitor.h | 62 ++++++------------------
kernel/trace/rv/monitors/nomiss/nomiss.c | 18 +------
kernel/trace/rv/monitors/stall/stall.c | 2 +-
3 files changed, 18 insertions(+), 64 deletions(-)
diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h
index d59507e8cb30..3b607a247768 100644
--- a/include/rv/ha_monitor.h
+++ b/include/rv/ha_monitor.h
@@ -253,19 +253,8 @@ static inline void __ha_monitor_timer_callback(struct ha_monitor *ha_mon)
}
/*
- * The clock variables have 2 different representations in the env_store:
- * - The guard representation is the timestamp of the last reset
- * - The invariant representation is the timestamp when the invariant expires
- * As the representations are incompatible, care must be taken when switching
- * between them: the invariant representation can only be used when starting a
- * timer when the previous representation was guard (e.g. no other invariant
- * started since the last reset operation).
- * Likewise, switching from invariant to guard representation without a reset
- * can be done only by subtracting the exact value used to start the invariant.
- *
- * Reading the environment variable (ha_get_clk) also reflects this difference
- * any reads in states that have an invariant return the (possibly negative)
- * time since expiration, other reads return the time since last reset.
+ * The clock variables store the time epoch - the timestamp when the clock was last reset.
+ * They are read by subtracting the time epoch from the current time.
*/
/*
@@ -279,31 +268,21 @@ static inline void ha_reset_clk_ns(struct ha_monitor *ha_mon, enum envs env, u64
{
WRITE_ONCE(ha_mon->env_store[env], time_ns);
}
-static inline void ha_set_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
- u64 value, u64 time_ns)
-{
- WRITE_ONCE(ha_mon->env_store[env], time_ns + value);
-}
-static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon,
- enum envs env, u64 time_ns)
+static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
+ u64 time_ns, u64 expire_ns)
{
- return READ_ONCE(ha_mon->env_store[env]) >= time_ns;
+ return READ_ONCE(ha_mon->env_store[env]) >= time_ns - expire_ns;
}
/*
* ha_invariant_passed_ns - prepare the invariant and return the time since reset
*/
-static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env,
- u64 expire, u64 time_ns)
+static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
{
- u64 passed = 0;
-
if (env < 0 || env >= ENV_MAX_STORED)
return 0;
if (ha_monitor_env_invalid(ha_mon, env))
return 0;
- passed = ha_get_env(ha_mon, env, time_ns);
- ha_set_invariant_ns(ha_mon, env, expire - passed, time_ns);
- return passed;
+ return ha_get_env(ha_mon, env, time_ns);
}
/*
@@ -317,32 +296,21 @@ static inline void ha_reset_clk_jiffy(struct ha_monitor *ha_mon, enum envs env)
{
WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64());
}
-static inline void ha_set_invariant_jiffy(struct ha_monitor *ha_mon,
- enum envs env, u64 value)
+static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon, enum envs env,
+ u64 time_ns, u64 expire_jiffy)
{
- WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64() + value);
-}
-static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon,
- enum envs env, u64 time_ns)
-{
- return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64());
-
+ return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64() - expire_jiffy);
}
/*
* ha_invariant_passed_jiffy - prepare the invariant and return the time since reset
*/
-static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env,
- u64 expire, u64 time_ns)
+static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
{
- u64 passed = 0;
-
if (env < 0 || env >= ENV_MAX_STORED)
return 0;
if (ha_monitor_env_invalid(ha_mon, env))
return 0;
- passed = ha_get_env(ha_mon, env, time_ns);
- ha_set_invariant_jiffy(ha_mon, env, expire - passed);
- return passed;
+ return ha_get_env(ha_mon, env, time_ns);
}
/*
@@ -389,14 +357,14 @@ static inline void ha_setup_timer(struct ha_monitor *ha_mon)
static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
- u64 passed = ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns);
+ u64 passed = ha_invariant_passed_jiffy(ha_mon, env, time_ns);
mod_timer(&ha_mon->timer, get_jiffies_64() + expire - passed);
}
static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
- u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);
+ u64 passed = ha_invariant_passed_ns(ha_mon, env, time_ns);
ha_start_timer_jiffy(ha_mon, ENV_MAX_STORED,
nsecs_to_jiffies(expire - passed + TICK_NSEC - 1), time_ns);
@@ -438,7 +406,7 @@ static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
int mode = HRTIMER_MODE_REL_HARD;
- u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);
+ u64 passed = ha_invariant_passed_ns(ha_mon, env, time_ns);
if (RV_MON_TYPE == RV_MON_PER_CPU)
mode |= HRTIMER_MODE_PINNED;
diff --git a/kernel/trace/rv/monitors/nomiss/nomiss.c b/kernel/trace/rv/monitors/nomiss/nomiss.c
index a0b5641a1858..19d0e9aa4d58 100644
--- a/kernel/trace/rv/monitors/nomiss/nomiss.c
+++ b/kernel/trace/rv/monitors/nomiss/nomiss.c
@@ -57,24 +57,12 @@ static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
enum states next_state, u64 time_ns)
{
if (curr_state == ready_nomiss)
- return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns);
+ return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns, DEADLINE_NS(ha_mon));
else if (curr_state == running_nomiss)
- return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns);
+ return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns, DEADLINE_NS(ha_mon));
return true;
}
-static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
- enum states curr_state, enum events event,
- enum states next_state, u64 time_ns)
-{
- if (curr_state == next_state)
- return;
- if (curr_state == ready_nomiss)
- ha_inv_to_guard(ha_mon, clk_nomiss, DEADLINE_NS(ha_mon), time_ns);
- else if (curr_state == running_nomiss)
- ha_inv_to_guard(ha_mon, clk_nomiss, DEADLINE_NS(ha_mon), time_ns);
-}
-
static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
enum states curr_state, enum events event,
enum states next_state, u64 time_ns)
@@ -122,8 +110,6 @@ static bool ha_verify_constraint(struct ha_monitor *ha_mon,
if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
return false;
- ha_convert_inv_guard(ha_mon, curr_state, event, next_state, time_ns);
-
if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
return false;
diff --git a/kernel/trace/rv/monitors/stall/stall.c b/kernel/trace/rv/monitors/stall/stall.c
index 9ccfda6b0e73..1aa65d7e690d 100644
--- a/kernel/trace/rv/monitors/stall/stall.c
+++ b/kernel/trace/rv/monitors/stall/stall.c
@@ -38,7 +38,7 @@ static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
enum states next_state, u64 time_ns)
{
if (curr_state == enqueued_stall)
- return ha_check_invariant_jiffy(ha_mon, clk_stall, time_ns);
+ return ha_check_invariant_jiffy(ha_mon, clk_stall, time_ns, threshold_jiffies);
return true;
}
--
2.47.3
^ permalink raw reply related
* [PATCH v2 10/13] verification/rvgen: Switch __get_event_variables() to Lark
From: Nam Cao @ 2026-05-28 8:27 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
Switch __get_event_variables() to use the parsed results from Lark, instead
of raw text processing.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v2: fix signature of __extract_env_var()
---
tools/verification/rvgen/rvgen/automata.py | 78 ++++++----------------
1 file changed, 19 insertions(+), 59 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index b86275e7bf28..2e26bb863245 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -591,45 +591,22 @@ class Automata:
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
+ for transition in self.transitions:
+ events.append(transition.event)
- # 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(" ", "")])
+ if transition.reset:
+ envs.append(transition.reset.env)
+ self.env_stored.add(transition.reset.env)
+ if transition.rule:
+ for c, _ in transition.rule.rules:
+ envs.append(c.env)
+ self.__extract_env_var(c)
+
+ for state in self._states:
+ if state.inv:
+ envs.append(state.inv.env)
+ self.__extract_env_var(state.inv)
return sorted(set(events)), sorted(set(envs))
@@ -653,28 +630,11 @@ class Automata:
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 __extract_env_var(self, constraint: ConstraintCondition):
+ if constraint.unit:
+ self.env_types[constraint.env] = constraint.unit
+ if constraint.val[0].isalpha():
+ self.constraint_vars.add(constraint.val)
def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]:
# transform the array into a dictionary
--
2.47.3
^ permalink raw reply related
* [PATCH v2 09/13] verification/rvgen: Delete __parse_constraint()
From: Nam Cao @ 2026-05-28 8:27 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
All previous users of self.invariants and self.guards have been converted
to the Lark parser, delete __parse_constraints() and its associates.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 67 ++-----------------------
1 file changed, 4 insertions(+), 63 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 3aee2e44ba7d..cafa19b318da 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -177,7 +177,6 @@ class ha2k(dot2k):
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()
self.has_invariant = False
self.has_guard = False
for state in self._states:
@@ -304,64 +303,6 @@ class ha2k(dot2k):
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]:
if not self.has_invariant:
return []
@@ -486,15 +427,15 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
{{""")
- if self.invariants:
+ if self.has_invariant:
buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, "
"event, next_state, time_ns))\n\t\treturn false;\n")
- if self.guards:
+ if self.has_guard:
buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
"next_state, time_ns))\n\t\treturn false;\n")
- if self.invariants:
+ if self.has_invariant:
buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n")
buff.append("\treturn true;\n}\n")
@@ -571,7 +512,7 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func()
def _fill_timer_type(self) -> list:
- if self.invariants:
+ if self.has_invariant:
return [
"/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */",
"#define HA_TIMER_TYPE HA_TIMER_HRTIMER"
--
2.47.3
^ permalink raw reply related
* [PATCH v2 12/13] verification/rvgen: Remove the old state variables
From: Nam Cao @ 2026-05-28 8:28 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
The state variables (states, initial_state, final_states) only capture the
states' names and have less information than their Lark-based counterparts.
Switch to use the new state variables and delete these old ones.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 9 ++++-----
tools/verification/rvgen/rvgen/dot2c.py | 10 +++++-----
tools/verification/rvgen/rvgen/dot2k.py | 8 ++++----
3 files changed, 13 insertions(+), 14 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 4c302f5cba68..a3be327c2a73 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -411,8 +411,7 @@ class Automata:
self.__dot_lines = self.__open_dot()
self.__parse_tree = ParseTree(file_path)
self.transitions = self.__parse_transitions()
- self._states, self._initial_state, self._final_states = self.__parse_states()
- self.states, self.initial_state, self.final_states = self.__get_state_variables()
+ self.states, self.initial_state, self.final_states = self.__parse_states()
self.env_types = {}
self.env_stored = set()
self.constraint_vars = set()
@@ -603,7 +602,7 @@ class Automata:
envs.append(c.env)
self.__extract_env_var(c)
- for state in self._states:
+ for state in self.states:
if state.inv:
envs.append(state.inv.env)
self.__extract_env_var(state.inv)
@@ -639,7 +638,7 @@ class Automata:
def __create_matrix(self) -> list[list[str]]:
# transform the array into a dictionary
events = self.events
- states = [s.name for s in self._states]
+ states = [s.name for s in self.states]
events_dict = {}
states_dict = {}
nr_event = 0
@@ -675,7 +674,7 @@ class Automata:
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:
+ if self.function[j][i] == self.initial_state.name:
curr_event_will_init += 1
if self.function[0][i] != self.invalid_state_str:
curr_event_from_init = True
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index fc85ba1f649e..22938ce1bf6c 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -29,10 +29,10 @@ class Dot2c(Automata):
def __get_enum_states_content(self) -> list[str]:
buff = []
- buff.append(f"\t{self.initial_state}{self.enum_suffix},")
+ buff.append(f"\t{self.initial_state.name}{self.enum_suffix},")
for state in self.states:
if state != self.initial_state:
- buff.append(f"\t{state}{self.enum_suffix},")
+ buff.append(f"\t{state.name}{self.enum_suffix},")
buff.append(f"\tstate_max{self.enum_suffix},")
return buff
@@ -142,7 +142,7 @@ class Dot2c(Automata):
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(self.__get_string_vector_per_line_content([s.name for s in self.states]))
buff.append("\t},")
return buff
@@ -159,7 +159,7 @@ class Dot2c(Automata):
return buff
def __get_max_strlen_of_states(self) -> int:
- max_state_name = len(max(self.states, key=len))
+ max_state_name = max((len(s.name) for s in self.states))
return max(max_state_name, len(self.invalid_state_str))
def get_aut_init_function(self) -> str:
@@ -199,7 +199,7 @@ class Dot2c(Automata):
return buff
def get_aut_init_initial_state(self) -> str:
- return self.initial_state
+ return self.initial_state.name
def format_aut_init_initial_state(self) -> list[str]:
buff = []
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 8fa7494846a3..49cb3e724a93 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -179,7 +179,7 @@ class ha2k(dot2k):
self.trace_h = self._read_template_file("trace_hybrid.h")
self.has_invariant = False
self.has_guard = False
- for state in self._states:
+ for state in self.states:
if state.inv:
self.has_invariant = True
for transition in self.transitions:
@@ -314,7 +314,7 @@ f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
{{"""]
_else = ""
- for state in self._states:
+ for state in self.states:
if not state.inv:
continue
@@ -382,7 +382,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
buff.append(f"\tif ({condition_str})\n\t\treturn;")
_else = ""
- for state in self._states:
+ for state in self.states:
inv = state.inv
if not inv:
continue
@@ -391,7 +391,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
buff.append(f"\t\t{inv};")
_else = "else "
- for state in self._states:
+ for state in self.states:
inv = state.inv
if not inv:
continue
--
2.47.3
^ permalink raw reply related
* [PATCH v2 13/13] verification/rvgen: Remove dead code
From: Nam Cao @ 2026-05-28 8:28 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
The conversion to use Lark left some dead code behind. Remove them.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 154 ---------------------
tools/verification/rvgen/rvgen/dot2k.py | 28 +---
2 files changed, 1 insertion(+), 181 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index a3be327c2a73..b6ff5fceb820 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -356,19 +356,6 @@ class State:
self.name = name
self.inv = inv
-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.
@@ -387,28 +374,10 @@ class Automata:
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.__parse_tree = ParseTree(file_path)
self.transitions = self.__parse_transitions()
self.states, self.initial_state, self.final_states = self.__parse_states()
@@ -435,57 +404,6 @@ class Automata:
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 __parse_transitions(self):
transitions = []
@@ -542,51 +460,6 @@ class Automata:
states.insert(0, initial_state)
return states, initial_state, final_states
- 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] = []
@@ -609,26 +482,6 @@ class Automata:
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: ConstraintCondition):
if constraint.unit:
self.env_types[constraint.env] = constraint.unit
@@ -697,10 +550,3 @@ class Automata:
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/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 49cb3e724a93..d6779ac6b7dd 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -11,9 +11,7 @@
from collections import deque
from .dot2c import Dot2c
from .generator import Monitor
-from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
-from .automata import ConstraintRule, ConstraintCondition
-
+from .automata import ConstraintRule, ConstraintCondition, AutomataError
class dot2k(Monitor, Dot2c):
template_dir = "dot2k"
@@ -217,9 +215,6 @@ class ha2k(dot2k):
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 __parse_guard_rule(self, rule) -> list[str]:
buff = []
for c, sep in rule.rules:
@@ -233,12 +228,6 @@ class ha2k(dot2k):
buff.append(cond)
return buff
- 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.rstrip(f"_{self.name}") in self.envs
- return env
-
def __start_to_invariant_check(self, inv: ConstraintCondition) -> str:
# by default assume the timer has ns expiration
clock_type = "ns"
@@ -249,21 +238,6 @@ class ha2k(dot2k):
return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {value})"
- 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 __parse_invariant(self, inv):
# by default assume the timer has ns expiration
clock_type = "ns"
--
2.47.3
^ permalink raw reply related
* [PATCH v2 11/13] verification/rvgen: Switch __create_matrix() to Lark
From: Nam Cao @ 2026-05-28 8:27 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1779956342.git.namcao@linutronix.de>
Switch __create_matrix() to use the transitions parsed by Lark to avoid all
the raw text parsing.
Also stop parsing constraints in __create_matrix(), that is not used
anymore.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 47 ++++++----------------
tools/verification/rvgen/rvgen/dot2k.py | 2 +-
2 files changed, 13 insertions(+), 36 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 2e26bb863245..4c302f5cba68 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -418,7 +418,7 @@ class Automata:
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.function = 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)
@@ -636,10 +636,10 @@ class Automata:
if constraint.val[0].isalpha():
self.constraint_vars.add(constraint.val)
- def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]:
+ def __create_matrix(self) -> list[list[str]]:
# transform the array into a dictionary
events = self.events
- states = self.states
+ states = [s.name for s in self._states]
events_dict = {}
states_dict = {}
nr_event = 0
@@ -654,39 +654,16 @@ class Automata:
# 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
+ for transition in self.transitions:
+ src, dst = transition.src, transition.dst
+ event = transition.event
+ if src == dst and transition.reset:
+ # those events reset also on self loops
+ self.self_loop_reset_events.add(event)
+ matrix[states_dict[src]][events_dict[event]] = dst
+
+ return matrix
def __store_init_events(self) -> tuple[list[bool], list[bool]]:
events_start = [False] * len(self.events)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index cafa19b318da..8fa7494846a3 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -403,7 +403,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
def __fill_constr_func(self) -> list[str]:
buff = []
- if not self.constraints:
+ if not self.has_invariant and not self.has_guard:
return []
buff.append(
--
2.47.3
^ permalink raw reply related
* Re: [PATCH v2 01/12] rv: Fix __user specifier usage in extract_params()
From: Nam Cao @ 2026-05-28 8:38 UTC (permalink / raw)
To: Gabriele Monaco, linux-kernel, Steven Rostedt, Gabriele Monaco,
Masami Hiramatsu, linux-trace-kernel
Cc: kernel test robot, Wen Yang
In-Reply-To: <20260527062313.39908-2-gmonaco@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> The attributes variables extracted from syscalls in the helper are both
> defined with the __user specifier although only the actual pointer to
> user data should be marked.
>
> Remove the __user specifier from attr.
>
> Reported-by: kernel test robot <lkp@intel.com>
> Closes: https://lore.kernel.org/oe-kbuild-all/202604150820.Ny143u6X-lkp@intel.com
> Fixes: b133207deb72 ("rv: Add nomiss deadline monitor")
> Reviewed-by: Wen Yang <wen.yang@linux.dev>
> Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
^ permalink raw reply
* [PATCH v2 3/8] riscv: stacktrace: disable KASAN instrumentation for stacktrace.o
From: Wang Han @ 2026-05-28 8:23 UTC (permalink / raw)
To: Paul Walmsley, Palmer Dabbelt, Albert Ou
Cc: Steven Rostedt, Alexandre Ghiti, Masami Hiramatsu, Mark Rutland,
Catalin Marinas, Chen Pei, Andy Chiu, Björn Töpel,
Deepak Gupta, Puranjay Mohan, Conor Dooley, Josh Poimboeuf,
Jiri Kosina, Miroslav Benes, Petr Mladek, Joe Lawrence,
Shuah Khan, Peter Zijlstra, Ingo Molnar, Arnaldo Carvalho de Melo,
Namhyung Kim, oliver.yang, xueshuai, zhuo.song, jkchen,
linux-riscv, linux-kernel, linux-trace-kernel, live-patching,
linux-kselftest, linux-perf-users
In-Reply-To: <20260527123530.2593918-1-wanghan@linux.alibaba.com>
KASAN records stack traces for every alloc/free, which means it walks
the unwinder very frequently. Instrumenting the stack trace collection
code itself adds substantial overhead and makes the traces themselves
noisier.
Mark stacktrace.o as not KASAN-instrumented, matching the arm, arm64
and x86 treatment of their stack unwinding code. This is a prerequisite
preference for the upcoming reliable unwinder, but the change is valid
on its own.
Signed-off-by: Wang Han <wanghan@linux.alibaba.com>
---
arch/riscv/kernel/Makefile | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/arch/riscv/kernel/Makefile b/arch/riscv/kernel/Makefile
index cabb99cadfb6..1cb6c9ab2981 100644
--- a/arch/riscv/kernel/Makefile
+++ b/arch/riscv/kernel/Makefile
@@ -44,6 +44,11 @@ CFLAGS_REMOVE_return_address.o = $(CC_FLAGS_FTRACE)
CFLAGS_REMOVE_sbi_ecall.o = $(CC_FLAGS_FTRACE)
endif
+# When KASAN is enabled, a stack trace is recorded for every alloc/free, which
+# can significantly impact performance. Avoid instrumenting the stack trace
+# collection code to minimize this impact.
+KASAN_SANITIZE_stacktrace.o := n
+
always-$(KBUILD_BUILTIN) += vmlinux.lds
obj-y += head.o
--
2.43.0
^ permalink raw reply related
* Re: [PATCH mm-unstable v18 11/14] mm/khugepaged: Introduce mTHP collapse support
From: Wei Yang @ 2026-05-28 8:42 UTC (permalink / raw)
To: Nico Pache
Cc: Wei Yang, Andrew Morton, linux-doc, linux-kernel, linux-mm,
linux-trace-kernel, aarcange, anshuman.khandual, apopple, baohua,
baolin.wang, byungchul, catalin.marinas, cl, corbet, dave.hansen,
david, dev.jain, gourry, hannes, hughd, jack, jackmanb, jannh,
jglisse, joshua.hahnjy, kas, lance.yang, liam, ljs,
mathieu.desnoyers, matthew.brost, mhiramat, mhocko, peterx,
pfalcato, rakie.kim, raquini, rdunlap, rientjes, rostedt, rppt,
ryan.roberts, shivankg, sunnanyong, surenb, thomas.hellstrom,
tiwai, usamaarif642, vbabka, vishal.moola, wangkefeng.wang, will,
willy, yang, ying.huang, ziy, zokeefe
In-Reply-To: <CAA1CXcDXyDhMyiVAb8XbusqMU10JXA8nOUw6b4_2i9H-kV2vwQ@mail.gmail.com>
On Tue, May 26, 2026 at 06:07:38AM -0600, Nico Pache wrote:
>On Tue, May 26, 2026 at 12:57 AM Wei Yang <richard.weiyang@gmail.com> wrote:
>>
>> On Mon, May 25, 2026 at 12:10:41PM -0700, Andrew Morton wrote:
>> >On Mon, 25 May 2026 08:15:53 -0600 Nico Pache <npache@redhat.com> wrote:
>> >
>> >> Can you please append the following fixup that reverts one of the
>> >> changes requested in V17. The issue with the change is described
>> >> below.
>> >
>> >OK. fyi, what I received was badly mangled: wordwrapping, tabs messed
>> >up, etc.
>> >
>> >Here's my reconstruction:
>> >
>>
>> Hi, Nico
>>
>> I tried to reply your mail, but found it has some encoding problem, so reply
>> here.
>
>Yeah sorry I didnt properly configure my email client after getting a
>new laptop.
>
>>
>> >
>> >Author: Nico Pache <npache@redhat.com>
>> >Subject: fix potential use-after-free of vma in mthp_collapse()
>> >Date: Mon May 25 07:38:59 2026 -0600
>> >
>> >Between V17 and v18, one reviewer (Wei) brought up that we are not doing
>> >the uffd-armed check until deep in the collapse operation. While not
>> >functionally incorrect, it can lead to unnecessary work.
>>
>> So we decide to tolerate the behavioral change?
>
>Yes, I believe it is ok for now. Either way we needed to remove the
>potential UAF. It only affects the behavior if mTHP is enabled, so the
>legacy behavior is kept. And the uffd case is limited.
>
>My future work involves further optimizing and cleaning up khugepaged.
>I'll make this part of the goal too. My first thought is to do the
>revalidation at every order (between the locks dropping); but that
>essentially pays the same penalty... I can't think of a clean solution
>at the moment.
One way come into my mind is add a @was_uffd_armed field in collapse_control
and updates it in hugepage_vma_revalidate() when latest vma is retrieved.
Still not elegant enough.
>
>Does that sound ok?
>
Not sure. I can't imagine the impact it would have.
>Cheers,
>-- Nico
--
Wei Yang
Help you, Help me
^ permalink raw reply
* Re: [PATCH v2 02/12] rv: Fix read_lock scope in per-task DA cleanup
From: Nam Cao @ 2026-05-28 8:43 UTC (permalink / raw)
To: Gabriele Monaco, linux-kernel, Steven Rostedt, Gabriele Monaco,
linux-trace-kernel
Cc: Wen Yang
In-Reply-To: <20260527062313.39908-3-gmonaco@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> The da_monitor_reset_all() function for per-task monitors takes
> tasklist_lock while iterating over tasks, then keeps it also while
> iterating over idle tasks (one per CPU). The latter is not necessary
> since the lock needs to guard only for_each_process_thread().
>
> Use a scoped_guard for more compact syntax and adjust the scope only
> where the lock is necessary.
>
> Fixes: 30984ccf31b7f ("rv: Refactor da_monitor to minimise macros")
> Fixes: 8259cb14a7068 ("rv: Reset per-task monitors also for idle tasks")
Fixes: tag "indicates that the patch fixes a bug in a previous
commit". There is no bug here, so I don't think Fixes tags are
applicable.
> Reviewed-by: Wen Yang <wen.yang@linux.dev>
> Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
^ permalink raw reply
* Re: [PATCH v2 03/12] rv: Reset per-task DA monitors before releasing the slot
From: Nam Cao @ 2026-05-28 8:48 UTC (permalink / raw)
To: Gabriele Monaco, linux-kernel, Steven Rostedt, Gabriele Monaco,
linux-trace-kernel
Cc: Wen Yang
In-Reply-To: <20260527062313.39908-4-gmonaco@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> Per-task monitors use task_mon_slot to determine which slot in the array
> to use for the monitor. During destruction, this slot is returned but
> this is done before resetting the monitor. As a result, the monitor's
> reset is in fact resetting a slot that is outside of the array
> (RV_PER_TASK_MONITOR_INIT).
Oh crap.
> Release the slot only after the reset to avoid out-of-bound memory
> access.
I think KASAN can catch this type of issue.
> Fixes: f5587d1b6ec93 ("rv: Add Hybrid Automata monitor type")
> Suggested-by: Wen Yang <wen.yang@linux.dev>
> Reviewed-by: Wen Yang <wen.yang@linux.dev>
> Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Should we have
Cc: stable@vger.kernel.org
?
Reviewed-by: Nam Cao <namcao@linutronix.de>
^ permalink raw reply
* Re: [PATCH v2 04/12] rv: Prevent task migration while handling per-CPU events
From: Nam Cao @ 2026-05-28 8:56 UTC (permalink / raw)
To: Gabriele Monaco, linux-kernel, Steven Rostedt, Gabriele Monaco,
linux-trace-kernel
Cc: Wen Yang
In-Reply-To: <20260527062313.39908-5-gmonaco@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> Tracepoint handlers are now fully preemptible.
Would be nice to mention the commit that did this:
a46023d5616e ("tracing: Guard __DECLARE_TRACE() use of __DO_TRACE_CALL() with SRCU-fast")
> When a per-CPU monitor
> handles an event, it retrieves the monitor state using a per-CPU
> pointer. If the event itself doesn't disable preemption, the task can
> migrate to a different CPU and we risk updating the wrong monitor.
>
> Mitigate this by explicitly disabling task migration before acquiring
> the monitor pointer. This cannot guarantee the monitor runs on the
> correct CPU but reduces the race condition window and prevents warnings.
>
> Reviewed-by: Wen Yang <wen.yang@linux.dev>
> Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
^ permalink raw reply
* Re: [PATCH v2 05/12] rv: Prevent in-flight per-task handlers from using invalid slots
From: Nam Cao @ 2026-05-28 8:59 UTC (permalink / raw)
To: Gabriele Monaco, linux-kernel, Steven Rostedt, Gabriele Monaco,
linux-trace-kernel
Cc: Wen Yang
In-Reply-To: <20260527062313.39908-6-gmonaco@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> Per-task monitors use a slot in the task_struct->rv[] array and store
> that locally (e.g. task_mon_slot), this slot is returned during the
> destruction process but currently hanlers can be running while that slot
> is returning and this race may lead to accessing an invalid slot.
>
> Synchronise with all in-flight tracepoint handlers using
> tracepoint_synchronize_unregister() before returning the slot.
>
> Fixes: f5587d1b6ec9 ("rv: Add Hybrid Automata monitor type")
> Fixes: a9769a5b9878 ("rv: Add support for LTL monitors")
> Suggested-by: Wen Yang <wen.yang@linux.dev>
> Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
^ permalink raw reply
* Re: [PATCH v2 06/12] rv: Ensure all pending probes terminate on per-obj monitor destroy
From: Nam Cao @ 2026-05-28 9:01 UTC (permalink / raw)
To: Gabriele Monaco, linux-kernel, Steven Rostedt, Gabriele Monaco,
linux-trace-kernel
Cc: Wen Yang
In-Reply-To: <20260527062313.39908-7-gmonaco@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> The monitor disable/destroy sequence detaches all probes and resets the
> monitor's data, however it doesn't wait for pending probes. This is an
> issue with per-object monitors, which free the monitor storage.
>
> Call tracepoint_synchronize_unregister() to make sure to wait for all
> pending probes before destroying the monitor storage.
>
> Fixes: 4a24127bd6cb ("rv: Add support for per-object monitors in DA/HA")
> Reviewed-by: Wen Yang <wen.yang@linux.dev>
> Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
^ permalink raw reply
* Re: [PATCH v2 07/12] rv: Fix monitor start ordering and memory ordering for monitoring flag
From: Nam Cao @ 2026-05-28 9:09 UTC (permalink / raw)
To: Gabriele Monaco, linux-kernel, Steven Rostedt, Gabriele Monaco,
linux-trace-kernel
Cc: Wen Yang
In-Reply-To: <20260527062313.39908-8-gmonaco@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> From: Wen Yang <wen.yang@linux.dev>
>
> da_monitor_start() set monitoring=1 before calling da_monitor_init_hook(),
> may racing with the sched_switch handler:
>
> da_monitor_start() sched_switch handler
> ------------------------- ---------------------------------
> da_mon->monitoring = 1;
> if (da_monitoring(da_mon)) /* true */
> ha_start_timer_ns(...);
> /* hrtimer->base == NULL, crash */
> da_monitor_init_hook(da_mon);
> /* hrtimer_setup() sets base */
>
> Fix the ordering and pair with release/acquire semantics:
>
> da_monitor_init_hook(da_mon);
> smp_store_release(&da_mon->monitoring, 1); /* da_monitor_start() */
> return smp_load_acquire(&da_mon->monitoring); /* da_monitoring() */
>
> On ARM64 a plain STR + LDR does not form a release-acquire pair, so
> the load can observe monitoring=1 while hrtimer->base is still NULL.
> The plain accesses are also data races under KCSAN.
>
> Use WRITE_ONCE for the monitoring=0 store in da_monitor_reset() to
> cover the reset path.
>
> Fixes: 792575348ff7 ("rv/include: Add deterministic automata monitor definition via C macros")
> Signed-off-by: Wen Yang <wen.yang@linux.dev>
> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Looks correct to me.
Reviewed-by: Nam Cao <namcao@linutronix.de>
Wen, I am curious, how did you find this issue?
Nam
^ permalink raw reply
* [PATCH v3 0/6] rtla: Migrate to libsubcmd for command line option parsing
From: Tomas Glozar @ 2026-05-28 10:32 UTC (permalink / raw)
To: Steven Rostedt, Tomas Glozar
Cc: John Kacur, Luis Goncalves, Crystal Wood, Costa Shulyupin,
Wander Lairson Costa, Ivan Pravdin, Namhyung Kim, Ian Rogers,
Arnaldo Carvalho de Melo, LKML, linux-trace-kernel,
linux-perf-users
[ CC to linux-perf-users for the libsubcmd code changes ]
rtla currently uses its own implementation that uses getopt_long() to
parse command-line arguments.
Migrate rtla to use libsubcmd for command line argument parsing,
similarly to what is already done by other tools like perf, bpftool,
and objtool. Among other benefits, this allows help messages to be
generated automatically rather than having to be typed out manually
for each tool.
libsubcmd is extended with a flag to parse optarg from separate
argument if a new flag is turned on. Without the flag, the old behavior
is preserved. That keeps the parsing working for tools that use
positional arguments, and allows RTLA to keep its flexible syntax for -C
and -t options and their long variants, --cgroup and --trace-output.
Another flag is added to disable automatic definition of --no-xy for
every option --xy and vice versa, which overlaps for RTLA's --irq and
--thread options.
The new implementation is moved into a separate file, cli.c, together
with a tiny header counterpart, cli.h. This helps separate the parsing
logic, which has little in common with the rest of RTLA, in a separate
module. Another new file, cli_p.h, is used as a private header to contain
macros and static function declarations that are also used by unit tests
next to cli.c, but should not be imported from elsewhere.
Macros to generate struct option array fields for libsubcmd's
parse_args() are used to preserve the consolidation of argument parsing
code across different RTLA tools. Kernel and user threads are, as
an exception, treated as common, although they are currently implemented
for timerlat only, in line with earlier consolidation changes.
The test suite is expanded to include two levels of unit tests, one testing
the already existing tool_parse_args() functions, one tests option callbacks,
which are a new level of the CLI parser added in this patchset. This helps
to verify that no regressions are caused by this refactoring.
I expect more improvements to the code being possible in the future,
like creating macros for option groups to further deduplicate the code,
reducing the amount of extra code in the _parse_args() functions, or
implementing support for unsetting options (which is currently only
supported for those that do not use a custom callback).
Base commit:
- https://git.kernel.org/pub/scm/linux/kernel/git/tglozar/linux.git/commit/?h=rtla-for-next&id=f03a59f949176ce4312cb466245d1243aaf40389
Dependencies:
- https://lore.kernel.org/linux-trace-kernel/20260423130558.882022-1-tglozar@redhat.com/T/
- https://lore.kernel.org/linux-trace-kernel/20260424140244.958495-1-tglozar@redhat.com/
- https://lore.kernel.org/linux-trace-kernel/20260414185223.65353-1-costa.shul@redhat.com/
(apply in reverse order, alternatively, use base commit above)
v3 changes (all in cover letter or first commit):
- Add FORCE to all targets that feature a make subcommand to ensure changes
in the dependency will trigger rebuild correctly.
- Convert all dependencies on directory targets LIBSUBCMD_OUTPUT and
LIB_OUTPUT into order-only prerequisites to prevent modifications of
the directory content triggering rebuild of targets inside it.
- Properly mention depedencies of the patchset in the cover letter, as well
as the base commit.
v2: https://lore.kernel.org/linux-trace-kernel/20260521141833.2353025-1-tglozar@redhat.com/T/
v2 changes:
- Two unit test suites are added to cover regressions, after several
options were broken by the v1. The test suites cover all parsing
issues reported in the v1 as well as those found during additional
testing.
- Return value of all paths that print help, including those that
are handled in RTLA, are set to libsubcmd's help exit code of 129.
Previously, only the tool help returned 129. While some other tools
(e.g. bpftool) do that, RTLA unifies those for consistency. The return
value is also added to the corresponding section in documentation.
- Incorrect parsing of --no-irq and --no-thread is fixed using a newly
added libsubcmd option flag.
- Incorrect parsing of -n and -u timerlat options (which erroneously
required an argument in v1) is fixed.
- A now stale declaration of removed function common_parse_options()
is removed from common.h.
- Segmentation fault on abbreviated --help (e.g. --he) is fixed.
- Incorrect formatting of OPT_END macro (spurious tab) is fixed.
- All opt_* callbacks now reject unimplemented unset (--no-) correctly.
- opt_trigger_cb() and opt_filter_cb() now take only the required events
field, not the whole params structure.
- Spurious opt_osnoise_threshold_cb() which is actually just a wrapper for
opt_llong_callback() is removed.
- Old off-by-one typo is fixed in --dma-latency and -E/--entries error
messages, to make it consistent with the newly added unit tests.
- Fix a bug in Makefile that defined LIBSUBCMD_INCLUDES as -I... and then
used it as a target name: define it as the path only, and then add -I$(...)
to CFLAGS, as this is the only include path that is generated during the build
itself.
v1: https://lore.kernel.org/linux-trace-kernel/20260320150651.51057-1-tglozar@redhat.com/T
Tomas Glozar (6):
rtla: Add libsubcmd dependency
tools subcmd: support optarg as separate argument
tools subcmd: allow parsing distinct --opt and --no-opt
rtla: Parse cmdline using libsubcmd
rtla/tests: Add unit tests for _parse_args() functions
rtla/tests: Add unit tests for CLI option callbacks
Documentation/tools/rtla/common_appendix.txt | 7 +-
tools/lib/subcmd/parse-options.c | 63 +-
tools/lib/subcmd/parse-options.h | 4 +
tools/tracing/rtla/.gitignore | 2 +
tools/tracing/rtla/Makefile | 66 +-
tools/tracing/rtla/src/Build | 2 +-
tools/tracing/rtla/src/cli.c | 537 +++++++++++++
tools/tracing/rtla/src/cli.h | 9 +
tools/tracing/rtla/src/cli_p.h | 670 +++++++++++++++++
tools/tracing/rtla/src/common.c | 109 ---
tools/tracing/rtla/src/common.h | 27 +-
tools/tracing/rtla/src/osnoise.c | 9 +-
tools/tracing/rtla/src/osnoise_hist.c | 221 +-----
tools/tracing/rtla/src/osnoise_top.c | 200 +----
tools/tracing/rtla/src/rtla.c | 92 ---
tools/tracing/rtla/src/timerlat.c | 9 +-
tools/tracing/rtla/src/timerlat.h | 6 +-
tools/tracing/rtla/src/timerlat_hist.c | 317 +-------
tools/tracing/rtla/src/timerlat_top.c | 286 +------
tools/tracing/rtla/src/utils.c | 28 +-
tools/tracing/rtla/src/utils.h | 9 +-
tools/tracing/rtla/tests/hwnoise.t | 2 +-
tools/tracing/rtla/tests/osnoise.t | 6 +-
tools/tracing/rtla/tests/timerlat.t | 6 +-
tools/tracing/rtla/tests/unit/Build | 5 +
tools/tracing/rtla/tests/unit/Makefile.unit | 4 +-
.../rtla/tests/unit/cli_opt_callback.c | 704 ++++++++++++++++++
.../rtla/tests/unit/cli_params_assert.h | 68 ++
.../rtla/tests/unit/osnoise_hist_cli.c | 557 ++++++++++++++
.../tracing/rtla/tests/unit/osnoise_top_cli.c | 503 +++++++++++++
.../rtla/tests/unit/timerlat_hist_cli.c | 702 +++++++++++++++++
.../rtla/tests/unit/timerlat_top_cli.c | 634 ++++++++++++++++
tools/tracing/rtla/tests/unit/unit_tests.c | 13 +
33 files changed, 4566 insertions(+), 1311 deletions(-)
create mode 100644 tools/tracing/rtla/src/cli.c
create mode 100644 tools/tracing/rtla/src/cli.h
create mode 100644 tools/tracing/rtla/src/cli_p.h
delete mode 100644 tools/tracing/rtla/src/rtla.c
create mode 100644 tools/tracing/rtla/tests/unit/cli_opt_callback.c
create mode 100644 tools/tracing/rtla/tests/unit/cli_params_assert.h
create mode 100644 tools/tracing/rtla/tests/unit/osnoise_hist_cli.c
create mode 100644 tools/tracing/rtla/tests/unit/osnoise_top_cli.c
create mode 100644 tools/tracing/rtla/tests/unit/timerlat_hist_cli.c
create mode 100644 tools/tracing/rtla/tests/unit/timerlat_top_cli.c
--
2.54.0
^ permalink raw reply
* [PATCH v3 1/6] rtla: Add libsubcmd dependency
From: Tomas Glozar @ 2026-05-28 10:32 UTC (permalink / raw)
To: Steven Rostedt, Tomas Glozar
Cc: John Kacur, Luis Goncalves, Crystal Wood, Costa Shulyupin,
Wander Lairson Costa, Ivan Pravdin, Namhyung Kim, Ian Rogers,
Arnaldo Carvalho de Melo, LKML, linux-trace-kernel,
linux-perf-users
In-Reply-To: <20260528103254.2990068-1-tglozar@redhat.com>
In preparation for migrating RTLA to libsubcmd, build libsubcmd from the
appropriate directory next to the RTLA build proper, and link the
resulting object to RTLA.
libsubcmd uses str_error_r() and strlcpy() at several places. To support
these, also link the respective libraries from tools/lib.
For completeness, also add tools/include to include path. This will
allow other userspace functions and macros shipped with the kernel to be
used in RTLA; perf and bpftool, two other users of libsubcmd, already do
that.
To prevent a name conflict, rename RTLA's run_command() function to
run_tool_command(), and replace RTLA's own container_of implementation
with the one in tools/include/linux/container_of.h.
Assisted-by: Composer:composer-1
Signed-off-by: Tomas Glozar <tglozar@redhat.com>
---
tools/tracing/rtla/.gitignore | 2 ++
tools/tracing/rtla/Makefile | 66 ++++++++++++++++++++++++++++++----
tools/tracing/rtla/src/rtla.c | 8 ++---
tools/tracing/rtla/src/utils.h | 6 ++--
4 files changed, 67 insertions(+), 15 deletions(-)
diff --git a/tools/tracing/rtla/.gitignore b/tools/tracing/rtla/.gitignore
index 231fb8d67f97..c7b4bf1c8ba9 100644
--- a/tools/tracing/rtla/.gitignore
+++ b/tools/tracing/rtla/.gitignore
@@ -10,3 +10,5 @@ custom_filename.txt
osnoise_irq_noise_hist.txt
osnoise_trace.txt
timerlat_trace.txt
+libsubcmd/
+lib/
diff --git a/tools/tracing/rtla/Makefile b/tools/tracing/rtla/Makefile
index 45690ee14544..60a102538988 100644
--- a/tools/tracing/rtla/Makefile
+++ b/tools/tracing/rtla/Makefile
@@ -27,6 +27,30 @@ endif
RTLA := $(OUTPUT)rtla
RTLA_IN := $(RTLA)-in.o
+LIBSUBCMD_DIR = $(srctree)/tools/lib/subcmd/
+ifneq ($(OUTPUT),)
+ LIBSUBCMD_OUTPUT = $(abspath $(OUTPUT))/libsubcmd
+else
+ LIBSUBCMD_OUTPUT = $(CURDIR)/libsubcmd
+endif
+LIBSUBCMD = $(LIBSUBCMD_OUTPUT)/libsubcmd.a
+LIBSUBCMD_INCLUDES = $(LIBSUBCMD_OUTPUT)/include
+LIBSUBCMD_MAKEFLAGS = O=$(LIBSUBCMD_OUTPUT) DESTDIR=$(LIBSUBCMD_OUTPUT) prefix= subdir=
+
+TOOLS_INCLUDES = -I$(srctree)/tools/include
+
+ifneq ($(OUTPUT),)
+ LIB_OUTPUT = $(abspath $(OUTPUT))/lib
+else
+ LIB_OUTPUT = $(CURDIR)/lib
+endif
+
+LIB_STRING = $(LIB_OUTPUT)/string.o
+LIB_STRING_SRC = $(srctree)/tools/lib/string.c
+
+LIB_STR_ERROR_R = $(LIB_OUTPUT)/str_error_r.o
+LIB_STR_ERROR_R_SRC = $(srctree)/tools/lib/str_error_r.c
+
VERSION := $(shell sh -c "make -sC ../../.. kernelversion | grep -v make")
DOCSRC := ../../../Documentation/tools/rtla/
@@ -66,7 +90,7 @@ ifeq ($(config),1)
include Makefile.config
endif
-CFLAGS += $(INCLUDES) $(LIB_INCLUDES)
+CFLAGS += $(INCLUDES) $(LIB_INCLUDES) $(TOOLS_INCLUDES) -I$(LIBSUBCMD_INCLUDES)
export CFLAGS OUTPUT srctree
@@ -93,20 +117,48 @@ tests/bpf/bpf_action_map.o: tests/bpf/bpf_action_map.c
$(Q)echo "BPF skeleton support is disabled, skipping tests/bpf/bpf_action_map.o"
endif
-$(RTLA): $(RTLA_IN)
- $(QUIET_LINK)$(CC) $(LDFLAGS) -o $(RTLA) $(RTLA_IN) $(EXTLIBS)
+$(RTLA): $(RTLA_IN) $(LIBSUBCMD) $(LIB_STRING) $(LIB_STR_ERROR_R)
+ $(QUIET_LINK)$(CC) $(LDFLAGS) -o $(RTLA) $(RTLA_IN) $(LIBSUBCMD) $(LIB_STRING) $(LIB_STR_ERROR_R) $(EXTLIBS)
-static: $(RTLA_IN)
+static: $(RTLA_IN) $(LIBSUBCMD) $(LIB_STRING) $(LIB_STR_ERROR_R)
$(eval LDFLAGS += -static)
- $(QUIET_LINK)$(CC) -static $(LDFLAGS) -o $(RTLA)-static $(RTLA_IN) $(EXTLIBS)
+ $(QUIET_LINK)$(CC) -static $(LDFLAGS) -o $(RTLA)-static $(RTLA_IN) $(LIBSUBCMD) $(LIB_STRING) $(LIB_STR_ERROR_R) $(EXTLIBS)
rtla.%: fixdep FORCE
make -f $(srctree)/tools/build/Makefile.build dir=. $@
-$(RTLA_IN): fixdep FORCE src/timerlat.skel.h
+$(RTLA_IN): fixdep FORCE src/timerlat.skel.h $(LIBSUBCMD_INCLUDES)
make $(build)=rtla
-clean: doc_clean fixdep-clean
+$(LIBSUBCMD_OUTPUT):
+ $(Q)$(MKDIR) -p $@
+
+$(LIBSUBCMD_INCLUDES): FORCE | $(LIBSUBCMD_OUTPUT)
+ $(Q)$(MAKE) -C $(LIBSUBCMD_DIR) $(LIBSUBCMD_MAKEFLAGS) \
+ install_headers
+
+$(LIBSUBCMD): FORCE | $(LIBSUBCMD_OUTPUT)
+ $(Q)$(MAKE) -C $(LIBSUBCMD_DIR) $(LIBSUBCMD_MAKEFLAGS) \
+ $@
+
+$(LIB_OUTPUT):
+ $(Q)$(MKDIR) -p $@
+
+$(LIB_STR_ERROR_R): $(LIB_STR_ERROR_R_SRC) | $(LIB_OUTPUT)
+ $(QUIET_CC)$(CC) $(CFLAGS) -c -o $@ $<
+
+$(LIB_STRING): $(LIB_STRING_SRC) | $(LIB_OUTPUT)
+ $(QUIET_CC)$(CC) $(CFLAGS) -c -o $@ $<
+
+libsubcmd-clean:
+ $(call QUIET_CLEAN, libsubcmd)
+ $(Q)$(RM) -r -- $(LIBSUBCMD_OUTPUT)
+
+lib-clean:
+ $(call QUIET_CLEAN, lib)
+ $(Q)$(RM) -r -- $(LIB_OUTPUT)
+
+clean: doc_clean fixdep-clean libsubcmd-clean lib-clean
$(call QUIET_CLEAN, rtla)
$(Q)find . -name '*.o' -delete -o -name '\.*.cmd' -delete -o -name '\.*.d' -delete
$(Q)rm -f rtla rtla-static fixdep FEATURE-DUMP rtla-*
diff --git a/tools/tracing/rtla/src/rtla.c b/tools/tracing/rtla/src/rtla.c
index 3398250076ea..f4342ca684c3 100644
--- a/tools/tracing/rtla/src/rtla.c
+++ b/tools/tracing/rtla/src/rtla.c
@@ -38,12 +38,12 @@ static void rtla_usage(int err)
}
/*
- * run_command - try to run a rtla tool command
+ * run_tool_command - try to run a rtla tool command
*
* It returns 0 if it fails. The tool's main will generally not
* return as they should call exit().
*/
-int run_command(int argc, char **argv, int start_position)
+int run_tool_command(int argc, char **argv, int start_position)
{
if (strcmp(argv[start_position], "osnoise") == 0) {
osnoise_main(argc-start_position, &argv[start_position]);
@@ -69,7 +69,7 @@ int main(int argc, char *argv[])
int retval;
/* is it an alias? */
- retval = run_command(argc, argv, 0);
+ retval = run_tool_command(argc, argv, 0);
if (retval)
exit(0);
@@ -82,7 +82,7 @@ int main(int argc, char *argv[])
rtla_usage(0);
}
- retval = run_command(argc, argv, 1);
+ retval = run_tool_command(argc, argv, 1);
if (retval)
exit(0);
diff --git a/tools/tracing/rtla/src/utils.h b/tools/tracing/rtla/src/utils.h
index e794ede64b2c..96fd72042717 100644
--- a/tools/tracing/rtla/src/utils.h
+++ b/tools/tracing/rtla/src/utils.h
@@ -7,6 +7,8 @@
#include <stdbool.h>
#include <stdlib.h>
+#include <linux/container_of.h>
+
/*
* '18446744073709551615\0'
*/
@@ -37,10 +39,6 @@ static inline bool str_has_prefix(const char *str, const char *prefix)
return strncmp(str, prefix, strlen(prefix)) == 0;
}
-#define container_of(ptr, type, member)({ \
- const typeof(((type *)0)->member) *__mptr = (ptr); \
- (type *)((char *)__mptr - offsetof(type, member)) ; })
-
extern int config_debug;
void debug_msg(const char *fmt, ...);
void err_msg(const char *fmt, ...);
--
2.54.0
^ permalink raw reply related
* [PATCH v3 2/6] tools subcmd: support optarg as separate argument
From: Tomas Glozar @ 2026-05-28 10:32 UTC (permalink / raw)
To: Steven Rostedt, Tomas Glozar
Cc: John Kacur, Luis Goncalves, Crystal Wood, Costa Shulyupin,
Wander Lairson Costa, Ivan Pravdin, Namhyung Kim, Ian Rogers,
Arnaldo Carvalho de Melo, LKML, linux-trace-kernel,
linux-perf-users
In-Reply-To: <20260528103254.2990068-1-tglozar@redhat.com>
In addition to "-ovalue" and "--opt=value" syntax, allow also "-o value"
and "--opt value" for options with optional argument when the newly
added PARSE_OPT_OPTARG_ALLOW_NEXT flag is set.
This behavior is turned off by default since it does not make sense for
tools using non-option command line arguments. Consider the ambiguity
of "cmd -d x", where "-d x" can mean either "-d with argument of x" or
"-d without argument, followed by non-option argument x". This is not an
issue in the case that the tool takes no non-option arguments.
To implement this, a new local variable, force_defval, is created in
get_value(), along with a comment explaining the logic.
Signed-off-by: Tomas Glozar <tglozar@redhat.com>
---
tools/lib/subcmd/parse-options.c | 53 +++++++++++++++++++++++++++-----
tools/lib/subcmd/parse-options.h | 1 +
2 files changed, 46 insertions(+), 8 deletions(-)
diff --git a/tools/lib/subcmd/parse-options.c b/tools/lib/subcmd/parse-options.c
index 555d617c1f50..664b2053bb77 100644
--- a/tools/lib/subcmd/parse-options.c
+++ b/tools/lib/subcmd/parse-options.c
@@ -72,6 +72,7 @@ static int get_value(struct parse_opt_ctx_t *p,
const char *s, *arg = NULL;
const int unset = flags & OPT_UNSET;
int err;
+ bool force_defval = false;
if (unset && p->opt)
return opterror(opt, "takes no value", flags);
@@ -123,6 +124,42 @@ static int get_value(struct parse_opt_ctx_t *p,
}
}
+ if (opt->flags & PARSE_OPT_OPTARG && !p->opt) {
+ if (!(p->flags & PARSE_OPT_OPTARG_ALLOW_NEXT)) {
+ /*
+ * If the option has an optional argument, and the argument is not
+ * provided in the option itself, do not attempt to get it from
+ * the next argument, unless PARSE_OPT_OPTARG_ALLOW_NEXT is set.
+ *
+ * This prevents a non-option argument from being interpreted as an
+ * optional argument of a preceding option, for example:
+ *
+ * $ cmd --opt val
+ * -> is "val" argument of "--opt" or a separate non-option
+ * argument?
+ *
+ * With PARSE_OPT_OPTARG_ALLOW_NEXT, "val" is interpreted as
+ * the argument of "--opt", i.e. the same as "--opt=val".
+ * Without PARSE_OPT_OPTARG_ALLOW_NEXT, --opt is interpreted
+ * as having the default value, and "val" as a separate non-option
+ * argument.
+ *
+ * PARSE_OPT_OPTARG_ALLOW_NEXT is useful for commands that take no
+ * non-option arguments and want to allow more flexibility in
+ * optional argument passing.
+ */
+ force_defval = true;
+ }
+
+ if (p->argc <= 1 || p->argv[1][0] == '-') {
+ /*
+ * If next argument is an option or does not exist,
+ * use the default value.
+ */
+ force_defval = true;
+ }
+ }
+
if (opt->flags & PARSE_OPT_NOBUILD) {
char reason[128];
bool noarg = false;
@@ -148,7 +185,7 @@ static int get_value(struct parse_opt_ctx_t *p,
noarg = true;
if (opt->flags & PARSE_OPT_NOARG)
noarg = true;
- if (opt->flags & PARSE_OPT_OPTARG && !p->opt)
+ if (force_defval)
noarg = true;
switch (opt->type) {
@@ -212,7 +249,7 @@ static int get_value(struct parse_opt_ctx_t *p,
err = 0;
if (unset)
*(const char **)opt->value = NULL;
- else if (opt->flags & PARSE_OPT_OPTARG && !p->opt)
+ else if (force_defval)
*(const char **)opt->value = (const char *)opt->defval;
else
err = get_arg(p, opt, flags, (const char **)opt->value);
@@ -244,7 +281,7 @@ static int get_value(struct parse_opt_ctx_t *p,
return (*opt->callback)(opt, NULL, 1) ? (-1) : 0;
if (opt->flags & PARSE_OPT_NOARG)
return (*opt->callback)(opt, NULL, 0) ? (-1) : 0;
- if (opt->flags & PARSE_OPT_OPTARG && !p->opt)
+ if (force_defval)
return (*opt->callback)(opt, NULL, 0) ? (-1) : 0;
if (get_arg(p, opt, flags, &arg))
return -1;
@@ -255,7 +292,7 @@ static int get_value(struct parse_opt_ctx_t *p,
*(int *)opt->value = 0;
return 0;
}
- if (opt->flags & PARSE_OPT_OPTARG && !p->opt) {
+ if (force_defval) {
*(int *)opt->value = opt->defval;
return 0;
}
@@ -271,7 +308,7 @@ static int get_value(struct parse_opt_ctx_t *p,
*(unsigned int *)opt->value = 0;
return 0;
}
- if (opt->flags & PARSE_OPT_OPTARG && !p->opt) {
+ if (force_defval) {
*(unsigned int *)opt->value = opt->defval;
return 0;
}
@@ -289,7 +326,7 @@ static int get_value(struct parse_opt_ctx_t *p,
*(long *)opt->value = 0;
return 0;
}
- if (opt->flags & PARSE_OPT_OPTARG && !p->opt) {
+ if (force_defval) {
*(long *)opt->value = opt->defval;
return 0;
}
@@ -305,7 +342,7 @@ static int get_value(struct parse_opt_ctx_t *p,
*(unsigned long *)opt->value = 0;
return 0;
}
- if (opt->flags & PARSE_OPT_OPTARG && !p->opt) {
+ if (force_defval) {
*(unsigned long *)opt->value = opt->defval;
return 0;
}
@@ -321,7 +358,7 @@ static int get_value(struct parse_opt_ctx_t *p,
*(u64 *)opt->value = 0;
return 0;
}
- if (opt->flags & PARSE_OPT_OPTARG && !p->opt) {
+ if (force_defval) {
*(u64 *)opt->value = opt->defval;
return 0;
}
diff --git a/tools/lib/subcmd/parse-options.h b/tools/lib/subcmd/parse-options.h
index 8e9147358a28..c573a0ca5ca6 100644
--- a/tools/lib/subcmd/parse-options.h
+++ b/tools/lib/subcmd/parse-options.h
@@ -33,6 +33,7 @@ enum parse_opt_flags {
PARSE_OPT_KEEP_ARGV0 = 4,
PARSE_OPT_KEEP_UNKNOWN = 8,
PARSE_OPT_NO_INTERNAL_HELP = 16,
+ PARSE_OPT_OPTARG_ALLOW_NEXT = 32,
};
enum parse_opt_option_flags {
--
2.54.0
^ permalink raw reply related
page: next (older) | prev (newer) | latest
- recent:[subjects (threaded)|topics (new)|topics (active)]
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox