* [PATCH 07/13] rv: Simply hybrid automata monitors's clock variables
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1777962130.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>
---
include/rv/ha_monitor.h | 60 ++++++------------------
kernel/trace/rv/monitors/nomiss/nomiss.c | 18 +------
kernel/trace/rv/monitors/stall/stall.c | 2 +-
3 files changed, 17 insertions(+), 63 deletions(-)
diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h
index d59507e8cb30..1ce3fd324d2c 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 time_ns - READ_ONCE(ha_mon->env_store[env]) <= 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)
-{
- 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)
+static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon, enum envs env,
+ u64 time_ns, u64 expire_jiffy)
{
- return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64());
-
+ return time_after64(READ_ONCE(ha_mon->env_store[env]) + expire_jiffy, get_jiffies_64());
}
/*
* 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);
diff --git a/kernel/trace/rv/monitors/nomiss/nomiss.c b/kernel/trace/rv/monitors/nomiss/nomiss.c
index 31f90f3638d8..6b3f93866d56 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 08/13] verification/rvgen: Simplify the generation for clock variables
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1777962130.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>
---
tools/verification/rvgen/rvgen/dot2k.py | 89 +------------------------
1 file changed, 1 insertion(+), 88 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index cf7e5ddc649c..c662c888f991 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -247,7 +247,7 @@ 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)"
+ return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {inv.val})"
def __start_to_conv(self, constr: str) -> str:
"""
@@ -376,40 +376,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 = []
@@ -449,54 +415,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 []
@@ -555,8 +473,6 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
*/""")
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()
@@ -569,9 +485,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 06/13] verification/rvgen: Convert __fill_verify_guards_func() to Lark
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1777962130.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>
---
tools/verification/rvgen/rvgen/dot2k.py | 39 ++++++++++++++++++++-----
1 file changed, 31 insertions(+), 8 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 3a39ae29e41e..cf7e5ddc649c 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -221,6 +221,20 @@ 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) -> 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)
+ buff[-1] += ';'
+ 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(",")
@@ -398,8 +412,9 @@ 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:
- return []
+
+ if not self.has_guard:
+ return
buff.append(
f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
@@ -410,14 +425,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 05/13] verification/rvgen: Convert __fill_setup_invariants_func() to Lark
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1777962130.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>
---
tools/verification/rvgen/rvgen/dot2k.py | 36 ++++++++++++++++++-------
1 file changed, 27 insertions(+), 9 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 3e7040398a20..3a39ae29e41e 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -250,6 +250,18 @@ 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)")
+
+ 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 +475,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 +491,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 04/13] verification/rvgen: Convert __fill_verify_invariants_func() to Lark
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1777962130.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>
---
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..3e7040398a20 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
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: ConstraintRule) -> 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 02/13] verification/rvgen: Introduce a parse tree for automata using Lark
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1777962130.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>
---
tools/verification/rvgen/rvgen/automata.py | 182 +++++++++++++++++++++
1 file changed, 182 insertions(+)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index b9f8149f7118..4e3d719a0952 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -13,6 +13,187 @@ 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: /[_a-zA-Z][_a-zA-Z0-9]+/
+ | /-?(\.[0-9]+|[0-9]+(\.[0-9]*))/
+ | /".*?"/
+
+ %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 dot_file:
+ tree = parser.parse(dot_file.read())
+ attributes_parser.visit(tree)
+ node_parser.visit(tree)
+ edge_parser.visit(tree)
+ except OSError as exc:
+ raise AutomataError(exc.strerror) from 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 +247,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 03/13] verification/rvgen: Implement state and transition parser based on Lark
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1777962130.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>
---
tools/verification/rvgen/rvgen/automata.py | 207 +++++++++++++++++++++
1 file changed, 207 insertions(+)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 4e3d719a0952..32c16736a41b 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -194,6 +194,155 @@ 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
+
+ def __init__(self, label: str):
+ parser = lark.Lark(self.grammar, parser='lalr', start="label")
+ tree = parser.parse(label)
+
+ 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
+
+ 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):
+ 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):
+ parser = lark.Lark(self.grammar, parser='lalr', start="events")
+ tree = parser.parse(label)
+ self.events = self.GetEvents().transform(tree)
+
+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: ConstraintRule):
+ self.name = name
+ self.inv = inv
+
class _ConstraintKey:
"""Base class for constraint keys."""
@@ -248,6 +397,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()
@@ -323,6 +474,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["label"]
+
+ if node.startswith(Automata.init_marker):
+ initial_state = node[len(Automata.init_marker):]
+
+ if not label:
+ continue
+
+ parser = StateLabelParser(attr["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 01/13] verification/rvgen: Switch LTL parser to Lark
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1777962130.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>
---
tools/verification/rvgen/rvgen/ltl2ba.py | 189 +++++++++--------------
1 file changed, 70 insertions(+), 119 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index 7f538598a868..b2dee2dbe257 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -7,8 +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
+import lark
from .automata import AutomataError
# Grammar:
@@ -30,42 +29,38 @@ 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_0-9]+/
+LITERAL: "true" | "false"
+
+COMMENT: "#" /.*/ "\n"
+%ignore COMMENT
+
+%import common.WS
+%ignore WS
+'''
class GraphNode:
uid = 0
@@ -432,90 +427,46 @@ 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[1])
+
+ 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(Variable(args))
+
+ 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)
+ spec = Transform().transform(spec)
rule = None
subexpr = {}
--
2.47.3
^ permalink raw reply related
* [PATCH 00/13] rv: Convert rvgen to Lark
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
This series converts the linear temporal logic parser and the automata
parser into using Lark.
The LTL parser has been using ply - a parsing library. However, ply
was recently announced to be abandoned. Furthermore, ply does not
offer the features that lark has.
On the other hand, the automata parser is mostly raw text processing
which is quite fragile. For instance, by slightly deform wwnr.dot (but
does not make it an invalid dot file):
digraph state_automaton {
{node [shape = plaintext, style=invis, label=""] "__init_not_running"};
{node [shape = ellipse]
"not_running"};
{node [shape=plaintext] "not_running"};
{node [shape = plaintext] "running"};
"__init_not_running"
-> "not_running";
"not_running" [label = "not_running", color = green3];
"not_running" ->
"not_running" [ label = "wakeup" ];
"not_running" -> "running" [ label = "switch_in" ];
"running" [label = "running"];
"running" -> "not_running" [ label = "switch_out" ];
}
the parser would be broken. Furthermore, the code is a bit hard to
follow with raw text being stored in lots of variables and sometimes
it is hard to figure out what sort of text is stored in the variables
while reading the code.
This motivates me to convert the automata parser as well. The plan is:
- Introduce Lark and prepare the parsed states, transitions and
constraints
- Convert the parser piece by piece to the parsed results from Lark
- Delete the old code
I struggled with converting __find_inv_conflicts(). So I decided to
remove the dual clock representation in the HA monitors, which allows
me to delete __find_inv_conflicts() entirely. This makes the code
simpler overall.
After the series, the generated HA monitors are mostly unchanged,
except:
- Clock representation conversion is gone and
ha_check_invariant_[ns|jiffy]() takes a new argument
- The ordering in ha_verify_guards() is changed, but still
equivalent. This is because it is now sorted lexically.
The generated LTL monitors are sadly significantly different, but proved to
be equivalent with runtime testing. Further work will make LTL monitor
generation more consistent.
Nam Cao (13):
verification/rvgen: Switch LTL parser to Lark
verification/rvgen: Introduce a parse tree for automata using Lark
verification/rvgen: Implement state and transition parser based on
Lark
verification/rvgen: Convert __fill_verify_invariants_func() to Lark
verification/rvgen: Convert __fill_setup_invariants_func() to Lark
verification/rvgen: Convert __fill_verify_guards_func() to Lark
rv: Simply hybrid automata monitors's clock variables
verification/rvgen: Simplify the generation for clock variables
verification/rvgen: Delete __parse_constraint()
verification/rvgen: Switch __get_event_variables() to Lark
verification/rvgen: Switch __create_matrix() to Lark
verification/rvgen: Remove the old state variables
verification/rvgen: Remove dead code
include/rv/ha_monitor.h | 60 +-
kernel/trace/rv/monitors/nomiss/nomiss.c | 18 +-
kernel/trace/rv/monitors/stall/stall.c | 2 +-
tools/verification/rvgen/rvgen/automata.py | 627 +++++++++++++--------
tools/verification/rvgen/rvgen/dot2c.py | 10 +-
tools/verification/rvgen/rvgen/dot2k.py | 277 +++------
tools/verification/rvgen/rvgen/ltl2ba.py | 189 +++----
7 files changed, 569 insertions(+), 614 deletions(-)
--
2.47.3
^ permalink raw reply
* Re: [RFC PATCH 10/12] rv: Add KUnit tests for some DA/HA monitors
From: Gabriele Monaco @ 2026-05-04 14:02 UTC (permalink / raw)
To: Nam Cao, linux-trace-kernel, linux-kernel
Cc: Steven Rostedt, Masami Hiramatsu, Thomas Weissschuh, Tomas Glozar,
John Kacur, Wen Yang
In-Reply-To: <87v7d38fk3.fsf@yellow.woof>
On Mon, 2026-05-04 at 15:33 +0200, Nam Cao wrote:
> I added that missing RV_KUNIT_EXPECT_REACTION(), but I still see a test
> failure:
>
> [ 1.070721] # module: rv_monitors_test
> [ 1.073512] 1..7
> [ 1.077641] scsi 1:0:0:0: CD-ROM QEMU QEMU DVD-ROM 2.5+
> PQ: 0 ANSI: 5
> [ 1.078494] ok 1 rv_test_sco
> [ 1.083256] ok 2 rv_test_sssw
> [ 1.085783] ok 3 rv_test_sts # SKIP Monitor not enabled
> [ 1.092365] ok 4 rv_test_opid
> [ 1.093462] # rv_test_nomiss: EXPECTATION FAILED at
> kernel/trace/rv/monitors/nomiss/nomiss.c:306
> [ 1.093462] Expected ctx->reactions == ++ctx->expected, but
> [ 1.093462] ctx->reactions == 2 (0x2)
> [ 1.093462] ++ctx->expected == 1 (0x1)
> [ 1.095699] not ok 5 rv_test_nomiss
> [ 1.109418] ok 6 rv_test_pagefault # SKIP Monitor not enabled
> [ 1.115146] ok 7 rv_test_sleep # SKIP Monitor not enabled
> [ 1.118050] # rv_trigger: pass:3 fail:1 skip:3 total:7
> [ 1.118053] # Totals: pass:3 fail:1 skip:3 total:7
> [ 1.120622] not ok 1 rv_trigger
>
> Any idea why?
The nomiss test is broken, it was not failing by sheer luck, maybe your run was
not lucky.
Basically a few silly mistakes like using deadline instead of dl_deadline (which
is left uninitialised) and doing udelay(10 / 1000) (which is 0).
I'm going to fix it in V2.
> > So I'm actually thinking of defining yet another macro that fundamentally
> > does
> >
> > RV_KUNIT_EXPECT_NO_REACTION()
> > handle_event()
> > RV_KUNIT_EXPECT_REACTION()
> >
> > which would make sure the reaction happens exactly there, plus I'd add an
> > RV_KUNIT_EXPECT_NO_REACTION() in the cleanup sequence to ensure no
> > unexpected
> > reaction occurred (or nobody forgot to expect a reaction like I did above).
>
> Sounds nice, go for it.
>
> > Yeah that should be neater, but weren't you the one not liking macros? ;)
>
> It's not black and white, I like whatever makes the code clean and easy
> to read. Sometimes macros are nice, other times not so much. I have
> spent hours reading the tracepoints' macros and they are still black
> magic to me (but to be fair, macros are probably the best we can do for
> that case). I hope we can rewrite those in Rust's generic one day.
Yeah makes sense, tracepoints are a fun one indeed.
Rust would probably be black magic to me but I'm going to have to learn it for
good one day!
Thanks,
Gabriele
^ permalink raw reply
* Re: [LSF/MM/BPF TOPIC][RFC PATCH v4 00/27] Private Memory Nodes (w/ Compressed RAM)
From: Arun George/Arun George @ 2026-05-04 13:08 UTC (permalink / raw)
To: Gregory Price
Cc: lsf-pc, linux-kernel, linux-cxl, cgroups, linux-mm,
linux-trace-kernel, damon, kernel-team, gregkh, rafael, dakr,
dave, jonathan.cameron, dave.jiang, alison.schofield,
vishal.l.verma, ira.weiny, longman, akpm, david, lorenzo.stoakes,
Liam.Howlett, vbabka, rppt, surenb, mhocko, osalvador, ziy,
matthew.brost, joshua.hahnjy, rakie.kim, byungchul, ying.huang,
apopple, axelrasmussen, yuanchu, weixugc, yury.norov, linux,
mhiramat, mathieu.desnoyers, tj, hannes, mkoutny, jackmanb, sj,
baolin.wang, npache, ryan.roberts, dev.jain, baohua, lance.yang,
muchun.song, xu.xin16, chengming.zhou, jannh, linmiaohe,
nao.horiguchi, pfalcato, rientjes, shakeel.butt, riel, harry.yoo,
cl, roman.gushchin, chrisl, kasong, shikemeng, nphamcs, bhe,
zhengqi.arch, terry.bowman, gost.dev, arungeorge05, cpgs
In-Reply-To: <afIKxG5mJZE6QgpR@gourry-fedora-PF4VCD3F>
On 29-04-2026 07:12 pm, Gregory Price wrote:
>>
>> Great! I believe "writable budget" could be an interesting idea which
>> can solve the 'bus error' sort of scenarios due to device not capable of
>> taking any more writes. The write budget could be replenished using the
>> control path and writes will not go ahead without the budget available,
>> right?>
>>
>
> Write budget is simple
>
> budget=1 (up to 1 page can be writable
> 1) swap 1 page -> cram alloc 1 page, put VSWAP_CRAM in PTE
> 2) read-fault -> cram upgrades VSWAP_CRAM to R/O PTE
> 3) write-fault ->
> a) if (writable_cnt < budget) { budget++; mkwrite(pte); }
> b) else: normal swap semantic -> promote to normal memory
>
> Meanwhile - use ballooning and a simple shrinker to dynamically size the
> region to respond to real compression ratio.
>
>
> All said an done - you get something close to zswap but with R/O
> mappings for all entries, and optional R/W-mappings for administrators
> who know something about their workload and can afford to take the risk
> of some amount of capacity being written to uncontended in exchange for
> performance.
>
> The writable-budget is a risk-dial: How much do you trust your workload
> to now spew un/poorly-compressible memory? The write-budget is a direct
> measure of that. (so take P99.99999 compression ratios, and you can make
> a good chunk of that writable).
>
> ~Gregory
>
>
I believe we are converging. Agree to most points you mentioned.
I see this problem statement can be solved by 'write-control + write
budget' approach similar to what you have described, whether we take
swap path or not.
But I see this 'write budget' (budget in terms of number of write
operations that can be handled by the device, not capacity) to be
provided by the device in control plane; not by the workloads in the host.
The budget can be communicated by the device in the device control plane
periodically (to be handled in the specific cram back-end driver; may be
interpreting the device back-pressure indications into a write budget
value). Even if the control plane breaks down, the host does not run
into issues except that it will not write further.
I assume you see this value coming from the workloads. This might be a
place where I have a different opinion.
There are multiple advantages of this value coming from the device:
1) We can modulate the write budget depending on the actual
compressibility in the device (and so workloads data). We don't have to
do estimation based on the workloads.
2) We don't have to do the capacity modulation - as in ballooning or
shrinker.
3) Even if the control path is broken, host can write only till the
available 'write budget'; so it won't get into 'bus error' situations.
~Arun George
^ permalink raw reply
* Re: [RFC PATCH 10/12] rv: Add KUnit tests for some DA/HA monitors
From: Nam Cao @ 2026-05-04 13:33 UTC (permalink / raw)
To: Gabriele Monaco, linux-trace-kernel, linux-kernel
Cc: Steven Rostedt, Masami Hiramatsu, Thomas Weissschuh, Tomas Glozar,
John Kacur, Wen Yang
In-Reply-To: <edc43db747832223dc2e7800c7b692327a1f5f82.camel@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> On Mon, 2026-05-04 at 10:39 +0200, Nam Cao wrote:
>> Gabriele Monaco <gmonaco@redhat.com> writes:
>> > +obj-$(CONFIG_RV_MONITORS_KUNIT_TEST) += rv_monitors_test.o
>> > +# Stubbing rv_react triggers the error
>> > +CFLAGS_rv_monitors_test.o += -Wno-suggest-attribute=format
>>
>> I try removing this flag, but my compiler does not produce any
>> warning. Which warning did you see?
>
> That's quite odd, I don't remember the exact GCC version that was showing the
> warning, my current one does not enable it by default, you can however enable it
> with:
>
> CFLAGS_rv_monitors_test.o += -Wsuggest-attribute=format
>
> Then you get:
>
> In file included from kernel/trace/rv/rv_monitors_test.c:11:
> kernel/trace/rv/rv_monitors_test.c: In function ‘rv_trigger_test_init’:
> kernel/trace/rv/rv_monitors_test.c:68:42: error: argument 2 of ‘__kunit_activate_static_stub’ might be a candidate for a format attribute [-Werror=suggest-attribute=format]
> 68 | kunit_activate_static_stub(test, rv_react, stub_rv_react);
> | ^~~~~~~~
> ./include/kunit/static_stub.h:97:44: note: in definition of macro ‘kunit_activate_static_stub’
> 97 | __kunit_activate_static_stub(test, real_fn_addr, replacement_addr); \
> | ^~~~~~~~~~~~
> kernel/trace/rv/rv_monitors_test.c:68:52: error: argument 3 of ‘__kunit_activate_static_stub’ might be a candidate for a format attribute [-Werror=suggest-attribute=format]
> 68 | kunit_activate_static_stub(test, rv_react, stub_rv_react);
> | ^~~~~~~~~~~~~
> ./include/kunit/static_stub.h:97:58: note: in definition of macro ‘kunit_activate_static_stub’
> 97 | __kunit_activate_static_stub(test, real_fn_addr, replacement_addr); \
> | ^~~~~~~~~~~~~~~~
>
>> If it is not a hassle, I would prefer to address the warning in C code.
>> Grep tells me the rest of the kernel does not use this, how do other
>> subsystems not suffer from this warning?
>
> When the compiler was caring about it, I tried all I could think of to avoid the
> warning, but I didn't manage, some other places do disable this warning (just
> not in the makefile but with pragmas):
>
> $ git grep "suggest-attribute=format"
> drivers/infiniband/hw/hfi1/trace_dbg.h:#pragma GCC diagnostic ignored "-Wsuggest-attribute=format"
> drivers/net/wireless/broadcom/brcm80211/brcmfmac/tracepoint.h:#pragma GCC diagnostic ignored "-Wsuggest-attribute=format"
> drivers/net/wireless/broadcom/brcm80211/brcmsmac/brcms_trace_brcmsmac_msg.h:#pragma GCC diagnostic ignored "-Wsuggest-attribute=format"
> drivers/net/wireless/intel/iwlwifi/iwl-devtrace.c:#pragma GCC diagnostic ignored "-Wsuggest-attribute=format"
> include/trace/events/qla.h:#pragma GCC diagnostic ignored "-Wsuggest-attribute=format"
> kernel/panic.c:#pragma GCC diagnostic ignored "-Wsuggest-attribute=format"
> lib/vsprintf.c:__diag_ignore(GCC, all, "-Wsuggest-attribute=format",
>
>
> Here, the error comes from macro expansions in KUnit and I'm not sure there's
> any practical way to solve it, that's why I resorted to disabling the warning
> altogether.
> I'm not sure whether a pragma would be cleaner though.
Thanks for sharing the details. I can see now that disabling the warning
is the way to go.
>> > +void rv_test_opid(struct kunit *test)
>> > +{
>> > + struct rv_kunit_ctx *ctx = test->priv;
>> > +
>> > + da_prepare_test(test, &rv_this);
>> > +
>> > + /*
>> > + * The handlers are called with an additional level of preemption,
>> > + * ensure we start from 0 but apply it here to avoid warnings.
>> > + */
>> > + KUNIT_ASSERT_TRUE(test, preemptible());
>> > + guard(preempt)();
>> > +
>> > + /* Wakeup with preemption and interrupts enabled */
>> > + handle_sched_waking(NULL, NULL);
>> > + RV_KUNIT_EXPECT_REACTION(test, ctx);
>> > +
>> > + /* Need resched with interrupts enabled */
>> > + scoped_guard(preempt)
>> > + handle_sched_need_resched(NULL, NULL, 0, TIF_NEED_RESCHED);
>>
>> From my understanding, this last one is testing that need_resched with
>> interrupt enabled does not invoke the reactor? And if the monitor is
>> broken and the reactor is invoked, we would have no test failure here,
>> but instead we have test failure the next time
>> RV_KUNIT_EXPECT_REACTION() is called. And if this is the last test, we
>> would not see a failure?
>
> Not really, I just forgot an RV_KUNIT_EXPECT_REACTION().
I added that missing RV_KUNIT_EXPECT_REACTION(), but I still see a test
failure:
[ 1.070721] # module: rv_monitors_test
[ 1.073512] 1..7
[ 1.077641] scsi 1:0:0:0: CD-ROM QEMU QEMU DVD-ROM 2.5+ PQ: 0 ANSI: 5
[ 1.078494] ok 1 rv_test_sco
[ 1.083256] ok 2 rv_test_sssw
[ 1.085783] ok 3 rv_test_sts # SKIP Monitor not enabled
[ 1.092365] ok 4 rv_test_opid
[ 1.093462] # rv_test_nomiss: EXPECTATION FAILED at kernel/trace/rv/monitors/nomiss/nomiss.c:306
[ 1.093462] Expected ctx->reactions == ++ctx->expected, but
[ 1.093462] ctx->reactions == 2 (0x2)
[ 1.093462] ++ctx->expected == 1 (0x1)
[ 1.095699] not ok 5 rv_test_nomiss
[ 1.109418] ok 6 rv_test_pagefault # SKIP Monitor not enabled
[ 1.115146] ok 7 rv_test_sleep # SKIP Monitor not enabled
[ 1.118050] # rv_trigger: pass:3 fail:1 skip:3 total:7
[ 1.118053] # Totals: pass:3 fail:1 skip:3 total:7
[ 1.120622] not ok 1 rv_trigger
Any idea why?
> So I'm actually thinking of defining yet another macro that fundamentally does
>
> RV_KUNIT_EXPECT_NO_REACTION()
> handle_event()
> RV_KUNIT_EXPECT_REACTION()
>
> which would make sure the reaction happens exactly there, plus I'd add an
> RV_KUNIT_EXPECT_NO_REACTION() in the cleanup sequence to ensure no unexpected
> reaction occurred (or nobody forgot to expect a reaction like I did above).
Sounds nice, go for it.
> Yeah that should be neater, but weren't you the one not liking macros? ;)
It's not black and white, I like whatever makes the code clean and easy
to read. Sometimes macros are nice, other times not so much. I have
spent hours reading the tracepoints' macros and they are still black
magic to me (but to be fair, macros are probably the best we can do for
that case). I hope we can rewrite those in Rust's generic one day.
Nam
^ permalink raw reply
* Re: [RFC PATCH 10/12] rv: Add KUnit tests for some DA/HA monitors
From: Gabriele Monaco @ 2026-05-04 11:42 UTC (permalink / raw)
To: Nam Cao, linux-trace-kernel, linux-kernel
Cc: Steven Rostedt, Masami Hiramatsu, Thomas Weissschuh, Tomas Glozar,
John Kacur, Wen Yang
In-Reply-To: <875x531scg.fsf@yellow.woof>
On Mon, 2026-05-04 at 10:39 +0200, Nam Cao wrote:
> Gabriele Monaco <gmonaco@redhat.com> writes:
> > +obj-$(CONFIG_RV_MONITORS_KUNIT_TEST) += rv_monitors_test.o
> > +# Stubbing rv_react triggers the error
> > +CFLAGS_rv_monitors_test.o += -Wno-suggest-attribute=format
>
> I try removing this flag, but my compiler does not produce any
> warning. Which warning did you see?
That's quite odd, I don't remember the exact GCC version that was showing the
warning, my current one does not enable it by default, you can however enable it
with:
CFLAGS_rv_monitors_test.o += -Wsuggest-attribute=format
Then you get:
In file included from kernel/trace/rv/rv_monitors_test.c:11:
kernel/trace/rv/rv_monitors_test.c: In function ‘rv_trigger_test_init’:
kernel/trace/rv/rv_monitors_test.c:68:42: error: argument 2 of ‘__kunit_activate_static_stub’ might be a candidate for a format attribute [-Werror=suggest-attribute=format]
68 | kunit_activate_static_stub(test, rv_react, stub_rv_react);
| ^~~~~~~~
./include/kunit/static_stub.h:97:44: note: in definition of macro ‘kunit_activate_static_stub’
97 | __kunit_activate_static_stub(test, real_fn_addr, replacement_addr); \
| ^~~~~~~~~~~~
kernel/trace/rv/rv_monitors_test.c:68:52: error: argument 3 of ‘__kunit_activate_static_stub’ might be a candidate for a format attribute [-Werror=suggest-attribute=format]
68 | kunit_activate_static_stub(test, rv_react, stub_rv_react);
| ^~~~~~~~~~~~~
./include/kunit/static_stub.h:97:58: note: in definition of macro ‘kunit_activate_static_stub’
97 | __kunit_activate_static_stub(test, real_fn_addr, replacement_addr); \
| ^~~~~~~~~~~~~~~~
> If it is not a hassle, I would prefer to address the warning in C code.
> Grep tells me the rest of the kernel does not use this, how do other
> subsystems not suffer from this warning?
When the compiler was caring about it, I tried all I could think of to avoid the
warning, but I didn't manage, some other places do disable this warning (just
not in the makefile but with pragmas):
$ git grep "suggest-attribute=format"
drivers/infiniband/hw/hfi1/trace_dbg.h:#pragma GCC diagnostic ignored "-Wsuggest-attribute=format"
drivers/net/wireless/broadcom/brcm80211/brcmfmac/tracepoint.h:#pragma GCC diagnostic ignored "-Wsuggest-attribute=format"
drivers/net/wireless/broadcom/brcm80211/brcmsmac/brcms_trace_brcmsmac_msg.h:#pragma GCC diagnostic ignored "-Wsuggest-attribute=format"
drivers/net/wireless/intel/iwlwifi/iwl-devtrace.c:#pragma GCC diagnostic ignored "-Wsuggest-attribute=format"
include/trace/events/qla.h:#pragma GCC diagnostic ignored "-Wsuggest-attribute=format"
kernel/panic.c:#pragma GCC diagnostic ignored "-Wsuggest-attribute=format"
lib/vsprintf.c:__diag_ignore(GCC, all, "-Wsuggest-attribute=format",
Here, the error comes from macro expansions in KUnit and I'm not sure there's
any practical way to solve it, that's why I resorted to disabling the warning
altogether.
I'm not sure whether a pragma would be cleaner though.
> > +void rv_test_opid(struct kunit *test)
> > +{
> > + struct rv_kunit_ctx *ctx = test->priv;
> > +
> > + da_prepare_test(test, &rv_this);
> > +
> > + /*
> > + * The handlers are called with an additional level of preemption,
> > + * ensure we start from 0 but apply it here to avoid warnings.
> > + */
> > + KUNIT_ASSERT_TRUE(test, preemptible());
> > + guard(preempt)();
> > +
> > + /* Wakeup with preemption and interrupts enabled */
> > + handle_sched_waking(NULL, NULL);
> > + RV_KUNIT_EXPECT_REACTION(test, ctx);
> > +
> > + /* Need resched with interrupts enabled */
> > + scoped_guard(preempt)
> > + handle_sched_need_resched(NULL, NULL, 0, TIF_NEED_RESCHED);
>
> From my understanding, this last one is testing that need_resched with
> interrupt enabled does not invoke the reactor? And if the monitor is
> broken and the reactor is invoked, we would have no test failure here,
> but instead we have test failure the next time
> RV_KUNIT_EXPECT_REACTION() is called. And if this is the last test, we
> would not see a failure?
Not really, I just forgot an RV_KUNIT_EXPECT_REACTION().
sched_need_resched just requires interrupts disabled, so I disable preemption
and show that seeing it with only interrupts enabled should react (touching
preemption is actually not required, but just to get a different test case).
> If so, should we perhaps have something like RV_KUNIT_EXPECT_NO_REACTION()
> here? So that if the monitor is broken and the reactor is called, then
> the kunit test will fail exactly where the failure is.
>
> Reading the patch further down below, we actually do have that
> macro! Shouldn't we use it here?
So I'm actually thinking of defining yet another macro that fundamentally does
RV_KUNIT_EXPECT_NO_REACTION()
handle_event()
RV_KUNIT_EXPECT_REACTION()
which would make sure the reaction happens exactly there, plus I'd add an
RV_KUNIT_EXPECT_NO_REACTION() in the cleanup sequence to ensure no unexpected
reaction occurred (or nobody forgot to expect a reaction like I did above).
> > +#ifdef CONFIG_RV_MON_SCO
> > +extern void rv_test_sco(struct kunit *test);
> > +#else
> > +static inline void rv_test_sco(struct kunit *test)
> > +{
> > + kunit_skip(test, "Monitor not enabled\n");
> > +}
> > +#endif
>
> Instead of these, I would prefer we have something like
>
> #define KUNIT_CASE_IF(test_name, enabled) \
> { .run_case = enabled ? test_name : some_stub, ... }
>
> and
>
> static struct kunit_case rv_trigger_test_cases[] = {
> KUNIT_CASE_IF(rv_test_sco, CONFIG_RV_MON_SCO),
> ...
> {}
> };
>
> or something like that. But no big deal.
Yeah that should be neater, but weren't you the one not liking macros? ;)
Thanks,
Gabriele
^ permalink raw reply
* Re: [RFC PATCH 07/12] verification/rvgen: Add golden and spec folders for tests
From: Nam Cao @ 2026-05-04 9:07 UTC (permalink / raw)
To: Gabriele Monaco, linux-trace-kernel, linux-kernel
Cc: Steven Rostedt, Thomas Weissschuh, Tomas Glozar, John Kacur,
Wen Yang
In-Reply-To: <b12301e81688e1795e0f73adcc33a9e6dca9435e.camel@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> Yeah, that'd do, keeping in mind the label after a \n can be different (HA
> invariants). The invariant parsing should then make sure nothing else appears
> after the \n .
Thanks for the info. The new grammar [1]:
class StateLabelParser:
grammar = r'''
label: CNAME ("\\n" condition)?
...
will handle that nicely.
Nam
[1] https://github.com/covanam/linux/commit/361efb610ba7c06b3668a953a6847ea80453c2e3#diff-904e482d5fa6374ab7ae9356df1340da53da564b16c81f3d932c0ae521fe2d13R253-R254
^ permalink raw reply
* Re: [PATCH] tracing: probes: remove unused variable
From: Markus Schneider-Pargmann @ 2026-05-04 8:59 UTC (permalink / raw)
To: Martin Kaiser, Steven Rostedt, Masami Hiramatsu
Cc: Markus Schneider-Pargmann, linux-trace-kernel, linux-kernel
In-Reply-To: <20260502135826.146257-1-martin@kaiser.cx>
[-- Attachment #1: Type: text/plain, Size: 1488 bytes --]
On Sat May 2, 2026 at 3:57 PM CEST, Martin Kaiser wrote:
> params is always NULL in traceprobe_expand_meta_args, it can be removed.
>
> Signed-off-by: Martin Kaiser <martin@kaiser.cx>
Reviewed-by: Markus Schneider-Pargmann (The Capable Hub) <msp@baylibre.com>
Best
Markus
> ---
> Would it be better to return ERR_PTR(-EOPNOTSUPP) instead of NULL, similar to
> what is done in other places where NOSUP_BTFARG is logged? This would make the
> parsing fail if $arg* is used without BTF support. At the moment, we skip the
> $arg*...
>
> kernel/trace/trace_probe.c | 3 +--
> 1 file changed, 1 insertion(+), 2 deletions(-)
>
> diff --git a/kernel/trace/trace_probe.c b/kernel/trace/trace_probe.c
> index e0d3a0da26af..b627093a941e 100644
> --- a/kernel/trace/trace_probe.c
> +++ b/kernel/trace/trace_probe.c
> @@ -1729,7 +1729,6 @@ const char **traceprobe_expand_meta_args(int argc, const char *argv[],
> int *new_argc, char *buf, int bufsize,
> struct traceprobe_parse_context *ctx)
> {
> - const struct btf_param *params = NULL;
> int i, j, n, used, ret, args_idx = -1;
> const char **new_argv __free(kfree) = NULL;
>
> @@ -1747,7 +1746,7 @@ const char **traceprobe_expand_meta_args(int argc, const char *argv[],
> if (args_idx != -1) {
> /* $arg* requires BTF info */
> trace_probe_log_err(0, NOSUP_BTFARG);
> - return (const char **)params;
> + return NULL;
> }
> *new_argc = argc;
> return NULL;
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 289 bytes --]
^ permalink raw reply
* Re: [RFC PATCH 07/12] verification/rvgen: Add golden and spec folders for tests
From: Gabriele Monaco @ 2026-05-04 8:49 UTC (permalink / raw)
To: Nam Cao, linux-trace-kernel, linux-kernel
Cc: Steven Rostedt, Thomas Weissschuh, Tomas Glozar, John Kacur,
Wen Yang
In-Reply-To: <8734071s43.fsf@yellow.woof>
On Mon, 2026-05-04 at 10:44 +0200, Nam Cao wrote:
> Gabriele Monaco <gmonaco@redhat.com> writes:
> > Do you have any other reason to prefer "state_d" in your example?
>
> Because "state_d" is what my dot renderer displays, not "state_c".
>
Right, in that case it gets more confusing..
Then I see no reason to allow a different label, let's just count it as error.
> > Either way we are opening for confusion (like in your example), so if you
> > believe throwing an error makes the grammar simpler, we could also go down
> > that path.
>
> I can simply add a check that the node's name matches the label.
Yeah, that'd do, keeping in mind the label after a \n can be different (HA
invariants). The invariant parsing should then make sure nothing else appears
after the \n .
Thanks,
Gabriele
>
> > In any case, I would make the label definition mandatory. So my current
> > sample
> > model is wrong.
>
> Cool, so no work for me then.
>
> Nam
^ permalink raw reply
* Re: [RFC PATCH 07/12] verification/rvgen: Add golden and spec folders for tests
From: Nam Cao @ 2026-05-04 8:44 UTC (permalink / raw)
To: Gabriele Monaco, linux-trace-kernel, linux-kernel, Steven Rostedt
Cc: Thomas Weissschuh, Tomas Glozar, John Kacur, Wen Yang
In-Reply-To: <ffb994110f4ec8165aa5a3e7cd83a57beeb609f9.camel@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> Do you have any other reason to prefer "state_d" in your example?
Because "state_d" is what my dot renderer displays, not "state_c".
> Either way we are opening for confusion (like in your example), so if you
> believe throwing an error makes the grammar simpler, we could also go down that
> path.
I can simply add a check that the node's name matches the label.
> In any case, I would make the label definition mandatory. So my current sample
> model is wrong.
Cool, so no work for me then.
Nam
^ permalink raw reply
* Re: [RFC PATCH 10/12] rv: Add KUnit tests for some DA/HA monitors
From: Nam Cao @ 2026-05-04 8:39 UTC (permalink / raw)
To: Gabriele Monaco, linux-trace-kernel, linux-kernel, Steven Rostedt,
Gabriele Monaco, Masami Hiramatsu
Cc: Thomas Weissschuh, Tomas Glozar, John Kacur, Wen Yang
In-Reply-To: <20260427151134.192971-11-gmonaco@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> +#ifdef CONFIG_RV_MONITORS_KUNIT_TEST
> +#include <kunit/test.h>
> +
> +/*
> + * rv_prepare_test - Disable the monitor for a kunit test
^^^^^^^^^^^^^^^
wrong name
> +obj-$(CONFIG_RV_MONITORS_KUNIT_TEST) += rv_monitors_test.o
> +# Stubbing rv_react triggers the error
> +CFLAGS_rv_monitors_test.o += -Wno-suggest-attribute=format
I try removing this flag, but my compiler does not produce any
warning. Which warning did you see?
If it is not a hassle, I would prefer to address the warning in C code.
Grep tells me the rest of the kernel does not use this, how do other
subsystems not suffer from this warning?
> +void rv_test_opid(struct kunit *test)
> +{
> + struct rv_kunit_ctx *ctx = test->priv;
> +
> + da_prepare_test(test, &rv_this);
> +
> + /*
> + * The handlers are called with an additional level of preemption,
> + * ensure we start from 0 but apply it here to avoid warnings.
> + */
> + KUNIT_ASSERT_TRUE(test, preemptible());
> + guard(preempt)();
> +
> + /* Wakeup with preemption and interrupts enabled */
> + handle_sched_waking(NULL, NULL);
> + RV_KUNIT_EXPECT_REACTION(test, ctx);
> +
> + /* Need resched with interrupts enabled */
> + scoped_guard(preempt)
> + handle_sched_need_resched(NULL, NULL, 0, TIF_NEED_RESCHED);
From my understanding, this last one is testing that need_resched with
interrupt enabled does not invoke the reactor? And if the monitor is
broken and the reactor is invoked, we would have no test failure here,
but instead we have test failure the next time
RV_KUNIT_EXPECT_REACTION() is called. And if this is the last test, we
would not see a failure?
If so, should we perhaps have something like RV_KUNIT_EXPECT_NO_REACTION()
here? So that if the monitor is broken and the reactor is called, then
the kunit test will fail exactly where the failure is.
Reading the patch further down below, we actually do have that
macro! Shouldn't we use it here?
> +#ifdef CONFIG_RV_MON_SCO
> +extern void rv_test_sco(struct kunit *test);
> +#else
> +static inline void rv_test_sco(struct kunit *test)
> +{
> + kunit_skip(test, "Monitor not enabled\n");
> +}
> +#endif
Instead of these, I would prefer we have something like
#define KUNIT_CASE_IF(test_name, enabled) \
{ .run_case = enabled ? test_name : some_stub, ... }
and
static struct kunit_case rv_trigger_test_cases[] = {
KUNIT_CASE_IF(rv_test_sco, CONFIG_RV_MON_SCO),
...
{}
};
or something like that. But no big deal.
Nam
^ permalink raw reply
* Re: [RFC PATCH 07/12] verification/rvgen: Add golden and spec folders for tests
From: Gabriele Monaco @ 2026-05-04 8:26 UTC (permalink / raw)
To: Nam Cao, linux-trace-kernel, linux-kernel, Steven Rostedt
Cc: Thomas Weissschuh, Tomas Glozar, John Kacur, Wen Yang
In-Reply-To: <878q9z1up7.fsf@yellow.woof>
On Mon, 2026-05-04 at 09:48 +0200, Nam Cao wrote:
> I am working on converting rvgen to use Lark, a parsing library:
> https://github.com/lark-parser/lark
>
> This test case breaks the current version of the new script, because
> state_c has no label while the script expects one - the script read the
> state's name from the label.
Right, good point, I forgot to add that.. Thanks for checking!
> We should define if the label or the node's name is our state's
> name. For example, if we have:
>
> "state_c" [label = "state_d"];
>
> Will the state's name be state_c or state_d? Or should that be a parsing
> error?
>
> I propose using the label if one is provided, otherwise using the node's
> name. So
>
> "state_c" [label = "state_d"];
>
> means the state's name is "state_d". But without that statement, the
> state's name is "state_c".
>
> What do you think?
Mmh, the only valid usecase I can think for DAs is to tweak the dot
representation, e.g.:
"state_c" [label = "State C"];
in this case the user might want to have a better display on the graph while
still keeping a valid state name.
Also keep in mind that in HA we could do something like
"state_c" [label = "state_c\nclk < 10"];
Here it's probably simpler to just parse the node name rather than the label.
Do you have any other reason to prefer "state_d" in your example?
Either way we are opening for confusion (like in your example), so if you
believe throwing an error makes the grammar simpler, we could also go down that
path.
In any case, I would make the label definition mandatory. So my current sample
model is wrong.
> (just FYI, my work-in-progress:
> https://github.com/covanam/linux/commits/rv-lark/)
Thanks for sharing, I'll have a look!
Gabriele
^ permalink raw reply
* Re: [RFC PATCH 07/12] verification/rvgen: Add golden and spec folders for tests
From: Nam Cao @ 2026-05-04 7:48 UTC (permalink / raw)
To: Gabriele Monaco, linux-trace-kernel, linux-kernel, Steven Rostedt,
Gabriele Monaco
Cc: Thomas Weissschuh, Tomas Glozar, John Kacur, Wen Yang
In-Reply-To: <20260427151134.192971-8-gmonaco@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> diff --git a/tools/verification/rvgen/tests/specs/test_da2.dot b/tools/verification/rvgen/tests/specs/test_da2.dot
> new file mode 100644
> index 000000000000..bfee6e535cf7
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/specs/test_da2.dot
> @@ -0,0 +1,18 @@
> +digraph state_automaton {
> + {node [shape = circle] "state_b"};
> + {node [shape = circle] "state_c"};
> + {node [shape = plaintext, style=invis, label=""] "__init_state_a"};
> + {node [shape = doublecircle] "state_a"};
> + {node [shape = circle] "state_a"};
> + "__init_state_a" -> "state_a";
> + "state_a" [label = "state_a"];
> + "state_a" -> "state_b" [ label = "event_1" ];
> + "state_a" -> "state_c" [ label = "event_2" ];
> + "state_b" [label = "state_b"];
> + "state_b" -> "state_a" [ label = "event_2" ];
> + "state_b" -> "state_c" [ label = "event_3" ];
> + { rank = min ;
> + "__init_state_a";
> + "state_a";
> + }
> +}
I am working on converting rvgen to use Lark, a parsing library:
https://github.com/lark-parser/lark
This test case breaks the current version of the new script, because
state_c has no label while the script expects one - the script read the
state's name from the label.
We should define if the label or the node's name is our state's
name. For example, if we have:
"state_c" [label = "state_d"];
Will the state's name be state_c or state_d? Or should that be a parsing error?
I propose using the label if one is provided, otherwise using the node's
name. So
"state_c" [label = "state_d"];
means the state's name is "state_d". But without that statement, the
state's name is "state_c".
What do you think?
(just FYI, my work-in-progress: https://github.com/covanam/linux/commits/rv-lark/)
Nam
^ permalink raw reply
* Re: [RFC PATCH v3] bpf: introduce TAINT_UNSAFE_BPF for mutating helpers
From: Aaron Tomlin @ 2026-05-03 20:14 UTC (permalink / raw)
To: Alexei Starovoitov
Cc: Jonathan Corbet, Song Liu, KP Singh, Matt Bobrowski,
Alexei Starovoitov, Daniel Borkmann, Andrii Nakryiko, Eduard,
Kumar Kartikeya Dwivedi, Steven Rostedt, Masami Hiramatsu,
Shuah Khan, Jiri Olsa, Martin KaFai Lau, Yonghong Song,
Mathieu Desnoyers, Randy Dunlap, neelx, sean, chjohnst, steve,
mproche, nick.lange, open list:DOCUMENTATION, LKML, bpf,
linux-trace-kernel
In-Reply-To: <CAADnVQJ5fatNF4auH+a8E39zWMfja3rm4BM_xGcTnLX8uuCQ9Q@mail.gmail.com>
[-- Attachment #1: Type: text/plain, Size: 760 bytes --]
On Sun, May 03, 2026 at 09:51:49PM +0200, Alexei Starovoitov wrote:
[ ... ]
> > + /*
> > + * Flag the program if it attempts to use mutating helpers.
> > + * The actual taint is deferred until successful verification.
> > + */
> > + if (func_id == BPF_FUNC_probe_write_user ||
> > + func_id == BPF_FUNC_override_return)
> > + env->prog->aux->taints_kernel = true;
>
> Nack.
>
> Please stop this spam.
> We're not doing it. These helpers have been around for a long time.
> There was no need to taint then. There is no need to taint now.
Hi Alexei,
Fair enough. I will drop the entire series. Please ignore the v4.
Thank you for your time.
Kind regards,
--
Aaron Tomlin
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 833 bytes --]
^ permalink raw reply
* Re: [RFC PATCH v4] bpf: introduce TAINT_UNSAFE_BPF for mutating helpers
From: Alexei Starovoitov @ 2026-05-03 19:52 UTC (permalink / raw)
To: Aaron Tomlin
Cc: Jonathan Corbet, Song Liu, KP Singh, Matt Bobrowski,
Alexei Starovoitov, Daniel Borkmann, Andrii Nakryiko, Eduard,
Kumar Kartikeya Dwivedi, Steven Rostedt, Masami Hiramatsu,
Shuah Khan, Jiri Olsa, Martin KaFai Lau, Yonghong Song,
Mathieu Desnoyers, Randy Dunlap, neelx, sean, chjohnst, steve,
mproche, nick.lange, open list:DOCUMENTATION, LKML, bpf,
linux-trace-kernel
In-Reply-To: <20260503190119.559696-1-atomlin@atomlin.com>
On Sun, May 3, 2026 at 9:01 PM Aaron Tomlin <atomlin@atomlin.com> wrote:
>
Nack.
See reply in v3.
^ permalink raw reply
* Re: [RFC PATCH v3] bpf: introduce TAINT_UNSAFE_BPF for mutating helpers
From: Alexei Starovoitov @ 2026-05-03 19:51 UTC (permalink / raw)
To: Aaron Tomlin
Cc: Jonathan Corbet, Song Liu, KP Singh, Matt Bobrowski,
Alexei Starovoitov, Daniel Borkmann, Andrii Nakryiko, Eduard,
Kumar Kartikeya Dwivedi, Steven Rostedt, Masami Hiramatsu,
Shuah Khan, Jiri Olsa, Martin KaFai Lau, Yonghong Song,
Mathieu Desnoyers, Randy Dunlap, neelx, sean, chjohnst, steve,
mproche, nick.lange, open list:DOCUMENTATION, LKML, bpf,
linux-trace-kernel
In-Reply-To: <20260503164700.548164-1-atomlin@atomlin.com>
On Sun, May 3, 2026 at 6:47 PM Aaron Tomlin <atomlin@atomlin.com> wrote:
>
> struct taint_flag {
> diff --git a/kernel/bpf/syscall.c b/kernel/bpf/syscall.c
> index a3c0214ca934..34b25609e72b 100644
> --- a/kernel/bpf/syscall.c
> +++ b/kernel/bpf/syscall.c
> @@ -3083,6 +3083,13 @@ static int bpf_prog_load(union bpf_attr *attr, bpfptr_t uattr, u32 uattr_size)
> if (err < 0)
> goto free_used_maps;
>
> + /*
> + * The program has passed the verifier. If it utilises unsafe
> + * helpers, formally taint the kernel now.
> + */
> + if (prog->aux->taints_kernel)
> + add_taint(TAINT_UNSAFE_BPF, LOCKDEP_STILL_OK);
> +
> err = bpf_prog_mark_insn_arrays_ready(prog);
> if (err < 0)
> goto free_used_maps;
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 69d75515ed3f..9d56082a2ac1 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -10287,6 +10287,14 @@ static int check_helper_call(struct bpf_verifier_env *env, struct bpf_insn *insn
> return err;
> }
>
> + /*
> + * Flag the program if it attempts to use mutating helpers.
> + * The actual taint is deferred until successful verification.
> + */
> + if (func_id == BPF_FUNC_probe_write_user ||
> + func_id == BPF_FUNC_override_return)
> + env->prog->aux->taints_kernel = true;
Nack.
Please stop this spam.
We're not doing it. These helpers have been around for a long time.
There was no need to taint then. There is no need to taint now.
pw-bot: cr
^ permalink raw reply
* [RFC PATCH v4] bpf: introduce TAINT_UNSAFE_BPF for mutating helpers
From: Aaron Tomlin @ 2026-05-03 19:01 UTC (permalink / raw)
To: corbet, song, kpsingh, mattbobrowski, ast, daniel, andrii,
eddyz87, memxor, rostedt, mhiramat
Cc: skhan, jolsa, martin.lau, yonghong.song, mathieu.desnoyers,
rdunlap, atomlin, neelx, sean, chjohnst, steve, mproche,
nick.lange, linux-doc, linux-kernel, bpf, linux-trace-kernel
The primary remit of the eBPF verifier is to ensure that eBPF programs
can neither crash the kernel nor corrupt memory. Nevertheless,
administrative utilities such as "bpftrace --unsafe" permit the loading
of programs that employ destructive or mutating helpers, most notably
bpf_probe_write_user() and bpf_override_return().
Since commit b28573ebfabe ("bpf: Remove bpf_probe_write_user() warning
message"), the kernel no longer issues a warning when an attempt is made to
invoke such destructive helpers.
Consequently, this patch introduces a novel kernel taint flag,
TAINT_UNSAFE_BPF ("V"). Tainting the kernel establishes a permanent and
readily auditable indicator (i.e., /proc/sys/kernel/tainted) to alert
maintainers that the kernel's execution flow or user memory may have been
compromised by an eBPF program.
Signed-off-by: Aaron Tomlin <atomlin@atomlin.com>
---
Changes since v3 [1]:
- Deferred add_taint() until after bpf_prog_alloc_id() completes
successfully to prevent false-positive kernel tainting
Changes since v2 [2]:
- Deferred the application of TAINT_UNSAFE_BPF until after the eBPF
verifier successfully completes
- Added taints_kernel to struct bpf_prog_aux to track the presence of
mutating helpers during static analysis without causing premature
side effects
Changes since v1 [3]:
- Moved the taint from run-time execution to load-time verification
- Added "V" flag decoding to tools/debugging/kernel-chktaint
(Randy Dunlap)
- Updated the seq command in tainted-kernels.rst to check all 21 bits
(Randy Dunlap)
- Fixed a Sphinx "Malformed table" warning by expanding the number
column boundaries in tainted-kernels.rst
[1]: https://lore.kernel.org/lkml/20260503164700.548164-1-atomlin@atomlin.com/
[2]: https://lore.kernel.org/lkml/20260503153730.541685-1-atomlin@atomlin.com/
[3]: https://lore.kernel.org/lkml/20260503035220.520479-1-atomlin@atomlin.com/
---
Documentation/admin-guide/tainted-kernels.rst | 56 ++++++++++---------
include/linux/bpf.h | 1 +
include/linux/panic.h | 3 +-
kernel/bpf/syscall.c | 7 +++
kernel/bpf/verifier.c | 8 +++
kernel/panic.c | 1 +
tools/debugging/kernel-chktaint | 8 +++
7 files changed, 58 insertions(+), 26 deletions(-)
diff --git a/Documentation/admin-guide/tainted-kernels.rst b/Documentation/admin-guide/tainted-kernels.rst
index 9ead927a37c0..d26a8d29808c 100644
--- a/Documentation/admin-guide/tainted-kernels.rst
+++ b/Documentation/admin-guide/tainted-kernels.rst
@@ -74,35 +74,36 @@ a particular type of taint. It's best to leave that to the aforementioned
script, but if you need something quick you can use this shell command to check
which bits are set::
- $ for i in $(seq 20); do echo $(($i-1)) $(($(cat /proc/sys/kernel/tainted)>>($i-1)&1));done
+ $ for i in $(seq 21); do echo $(($i-1)) $(($(cat /proc/sys/kernel/tainted)>>($i-1)&1));done
Table for decoding tainted state
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-=== === ====== ========================================================
-Bit Log Number Reason that got the kernel tainted
-=== === ====== ========================================================
- 0 G/P 1 proprietary module was loaded
- 1 _/F 2 module was force loaded
- 2 _/S 4 kernel running on an out of specification system
- 3 _/R 8 module was force unloaded
- 4 _/M 16 processor reported a Machine Check Exception (MCE)
- 5 _/B 32 bad page referenced or some unexpected page flags
- 6 _/U 64 taint requested by userspace application
- 7 _/D 128 kernel died recently, i.e. there was an OOPS or BUG
- 8 _/A 256 ACPI table overridden by user
- 9 _/W 512 kernel issued warning
- 10 _/C 1024 staging driver was loaded
- 11 _/I 2048 workaround for bug in platform firmware applied
- 12 _/O 4096 externally-built ("out-of-tree") module was loaded
- 13 _/E 8192 unsigned module was loaded
- 14 _/L 16384 soft lockup occurred
- 15 _/K 32768 kernel has been live patched
- 16 _/X 65536 auxiliary taint, defined for and used by distros
- 17 _/T 131072 kernel was built with the struct randomization plugin
- 18 _/N 262144 an in-kernel test has been run
- 19 _/J 524288 userspace used a mutating debug operation in fwctl
-=== === ====== ========================================================
+=== === ======= ========================================================
+Bit Log Number Reason that got the kernel tainted
+=== === ======= ========================================================
+ 0 G/P 1 proprietary module was loaded
+ 1 _/F 2 module was force loaded
+ 2 _/S 4 kernel running on an out of specification system
+ 3 _/R 8 module was force unloaded
+ 4 _/M 16 processor reported a Machine Check Exception (MCE)
+ 5 _/B 32 bad page referenced or some unexpected page flags
+ 6 _/U 64 taint requested by userspace application
+ 7 _/D 128 kernel died recently, i.e. there was an OOPS or BUG
+ 8 _/A 256 ACPI table overridden by user
+ 9 _/W 512 kernel issued warning
+ 10 _/C 1024 staging driver was loaded
+ 11 _/I 2048 workaround for bug in platform firmware applied
+ 12 _/O 4096 externally-built ("out-of-tree") module was loaded
+ 13 _/E 8192 unsigned module was loaded
+ 14 _/L 16384 soft lockup occurred
+ 15 _/K 32768 kernel has been live patched
+ 16 _/X 65536 auxiliary taint, defined for and used by distros
+ 17 _/T 131072 kernel was built with the struct randomization plugin
+ 18 _/N 262144 an in-kernel test has been run
+ 19 _/J 524288 userspace used a mutating debug operation in fwctl
+ 20 _/V 1048576 an unsafe eBPF program (mutating helper) was loaded
+=== === ======= ========================================================
Note: The character ``_`` is representing a blank in this table to make reading
easier.
@@ -189,3 +190,8 @@ More detailed explanation for tainting
19) ``J`` if userspace opened /dev/fwctl/* and performed a FWTCL_RPC_DEBUG_WRITE
to use the devices debugging features. Device debugging features could
cause the device to malfunction in undefined ways.
+
+ 20) ``V`` if an eBPF program utilising unsafe, mutating helpers (such as
+ bpf_probe_write_user() or bpf_override_return()) was loaded. These helpers
+ bypass standard eBPF safety guarantees and can alter execution flow or
+ corrupt memory.
diff --git a/include/linux/bpf.h b/include/linux/bpf.h
index b4b703c90ca9..b2e236a7ed0d 100644
--- a/include/linux/bpf.h
+++ b/include/linux/bpf.h
@@ -1698,6 +1698,7 @@ struct bpf_prog_aux {
bool changes_pkt_data;
bool might_sleep;
bool kprobe_write_ctx;
+ bool taints_kernel;
u64 prog_array_member_cnt; /* counts how many times as member of prog_array */
struct mutex ext_mutex; /* mutex for is_extended and prog_array_member_cnt */
struct bpf_arena *arena;
diff --git a/include/linux/panic.h b/include/linux/panic.h
index f1dd417e54b2..8622c02c2c24 100644
--- a/include/linux/panic.h
+++ b/include/linux/panic.h
@@ -88,7 +88,8 @@ static inline void set_arch_panic_timeout(int timeout, int arch_default_timeout)
#define TAINT_RANDSTRUCT 17
#define TAINT_TEST 18
#define TAINT_FWCTL 19
-#define TAINT_FLAGS_COUNT 20
+#define TAINT_UNSAFE_BPF 20
+#define TAINT_FLAGS_COUNT 21
#define TAINT_FLAGS_MAX ((1UL << TAINT_FLAGS_COUNT) - 1)
struct taint_flag {
diff --git a/kernel/bpf/syscall.c b/kernel/bpf/syscall.c
index a3c0214ca934..47bf0d10af98 100644
--- a/kernel/bpf/syscall.c
+++ b/kernel/bpf/syscall.c
@@ -3109,6 +3109,13 @@ static int bpf_prog_load(union bpf_attr *attr, bpfptr_t uattr, u32 uattr_size)
perf_event_bpf_event(prog, PERF_BPF_EVENT_PROG_LOAD, 0);
bpf_audit_prog(prog, BPF_AUDIT_LOAD);
+ /*
+ * The program has passed the verifier and is now publicly exposed.
+ * If it utilises unsafe helpers, formally taint the kernel now.
+ */
+ if (prog->aux->taints_kernel)
+ add_taint(TAINT_UNSAFE_BPF, LOCKDEP_STILL_OK);
+
err = bpf_prog_new_fd(prog);
if (err < 0)
bpf_prog_put(prog);
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 69d75515ed3f..9d56082a2ac1 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -10287,6 +10287,14 @@ static int check_helper_call(struct bpf_verifier_env *env, struct bpf_insn *insn
return err;
}
+ /*
+ * Flag the program if it attempts to use mutating helpers.
+ * The actual taint is deferred until successful verification.
+ */
+ if (func_id == BPF_FUNC_probe_write_user ||
+ func_id == BPF_FUNC_override_return)
+ env->prog->aux->taints_kernel = true;
+
/* eBPF programs must be GPL compatible to use GPL-ed functions */
if (!env->prog->gpl_compatible && fn->gpl_only) {
verbose(env, "cannot call GPL-restricted function from non-GPL compatible program\n");
diff --git a/kernel/panic.c b/kernel/panic.c
index 20feada5319d..1ae19bd8fc1d 100644
--- a/kernel/panic.c
+++ b/kernel/panic.c
@@ -825,6 +825,7 @@ const struct taint_flag taint_flags[TAINT_FLAGS_COUNT] = {
TAINT_FLAG(RANDSTRUCT, 'T', ' '),
TAINT_FLAG(TEST, 'N', ' '),
TAINT_FLAG(FWCTL, 'J', ' '),
+ TAINT_FLAG(UNSAFE_BPF, 'V', ' '),
};
#undef TAINT_FLAG
diff --git a/tools/debugging/kernel-chktaint b/tools/debugging/kernel-chktaint
index e1571c04afb5..c0fbd7bcfcfd 100755
--- a/tools/debugging/kernel-chktaint
+++ b/tools/debugging/kernel-chktaint
@@ -211,6 +211,14 @@ else
addout "J"
echo " * fwctl's mutating debug interface was used (#19)"
fi
+
+T=`expr $T / 2`
+if [ `expr $T % 2` -eq 0 ]; then
+ addout " "
+else
+ addout "V"
+ echo " * an unsafe eBPF program (mutating helper) was loaded (#20)"
+fi
echo "Raw taint value as int/string: $taint/'$out'"
# report on any tainted loadable modules
--
2.51.0
^ permalink raw reply related
* [RFC PATCH v3] bpf: introduce TAINT_UNSAFE_BPF for mutating helpers
From: Aaron Tomlin @ 2026-05-03 16:47 UTC (permalink / raw)
To: corbet, song, kpsingh, mattbobrowski, ast, daniel, andrii,
eddyz87, memxor, rostedt, mhiramat
Cc: skhan, jolsa, martin.lau, yonghong.song, mathieu.desnoyers,
rdunlap, atomlin, neelx, sean, chjohnst, steve, mproche,
nick.lange, linux-doc, linux-kernel, bpf, linux-trace-kernel
The primary remit of the eBPF verifier is to ensure that eBPF programs
can neither crash the kernel nor corrupt memory. Nevertheless,
administrative utilities such as "bpftrace --unsafe" permit the loading
of programs that employ destructive or mutating helpers, most notably
bpf_probe_write_user() and bpf_override_return().
Since commit b28573ebfabe ("bpf: Remove bpf_probe_write_user() warning
message"), the kernel no longer issues a warning when an attempt is made to
invoke such destructive helpers.
Consequently, this patch introduces a novel kernel taint flag,
TAINT_UNSAFE_BPF ("V"). Tainting the kernel establishes a permanent and
readily auditable indicator (i.e., /proc/sys/kernel/tainted) to alert
maintainers that the kernel's execution flow or user memory may have been
compromised by an eBPF program.
Signed-off-by: Aaron Tomlin <atomlin@atomlin.com>
---
Changes since v2 [1]:
- Deferred the application of TAINT_UNSAFE_BPF until after the eBPF
verifier successfully completes
- Added taints_kernel to struct bpf_prog_aux to track the presence of
mutating helpers during static analysis without causing premature
side effects
Changes since v1 [2]:
- Moved the taint from run-time execution to load-time verification
- Added "V" flag decoding to tools/debugging/kernel-chktaint
(Randy Dunlap)
- Updated the seq command in tainted-kernels.rst to check all 21 bits
(Randy Dunlap)
- Fixed a Sphinx "Malformed table" warning by expanding the number
column boundaries in tainted-kernels.rst
[1]: https://lore.kernel.org/lkml/20260503153730.541685-1-atomlin@atomlin.com/
[2]: https://lore.kernel.org/lkml/20260503035220.520479-1-atomlin@atomlin.com/
---
Documentation/admin-guide/tainted-kernels.rst | 56 ++++++++++---------
include/linux/bpf.h | 1 +
include/linux/panic.h | 3 +-
kernel/bpf/syscall.c | 7 +++
kernel/bpf/verifier.c | 8 +++
kernel/panic.c | 1 +
tools/debugging/kernel-chktaint | 8 +++
7 files changed, 58 insertions(+), 26 deletions(-)
diff --git a/Documentation/admin-guide/tainted-kernels.rst b/Documentation/admin-guide/tainted-kernels.rst
index 9ead927a37c0..d26a8d29808c 100644
--- a/Documentation/admin-guide/tainted-kernels.rst
+++ b/Documentation/admin-guide/tainted-kernels.rst
@@ -74,35 +74,36 @@ a particular type of taint. It's best to leave that to the aforementioned
script, but if you need something quick you can use this shell command to check
which bits are set::
- $ for i in $(seq 20); do echo $(($i-1)) $(($(cat /proc/sys/kernel/tainted)>>($i-1)&1));done
+ $ for i in $(seq 21); do echo $(($i-1)) $(($(cat /proc/sys/kernel/tainted)>>($i-1)&1));done
Table for decoding tainted state
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-=== === ====== ========================================================
-Bit Log Number Reason that got the kernel tainted
-=== === ====== ========================================================
- 0 G/P 1 proprietary module was loaded
- 1 _/F 2 module was force loaded
- 2 _/S 4 kernel running on an out of specification system
- 3 _/R 8 module was force unloaded
- 4 _/M 16 processor reported a Machine Check Exception (MCE)
- 5 _/B 32 bad page referenced or some unexpected page flags
- 6 _/U 64 taint requested by userspace application
- 7 _/D 128 kernel died recently, i.e. there was an OOPS or BUG
- 8 _/A 256 ACPI table overridden by user
- 9 _/W 512 kernel issued warning
- 10 _/C 1024 staging driver was loaded
- 11 _/I 2048 workaround for bug in platform firmware applied
- 12 _/O 4096 externally-built ("out-of-tree") module was loaded
- 13 _/E 8192 unsigned module was loaded
- 14 _/L 16384 soft lockup occurred
- 15 _/K 32768 kernel has been live patched
- 16 _/X 65536 auxiliary taint, defined for and used by distros
- 17 _/T 131072 kernel was built with the struct randomization plugin
- 18 _/N 262144 an in-kernel test has been run
- 19 _/J 524288 userspace used a mutating debug operation in fwctl
-=== === ====== ========================================================
+=== === ======= ========================================================
+Bit Log Number Reason that got the kernel tainted
+=== === ======= ========================================================
+ 0 G/P 1 proprietary module was loaded
+ 1 _/F 2 module was force loaded
+ 2 _/S 4 kernel running on an out of specification system
+ 3 _/R 8 module was force unloaded
+ 4 _/M 16 processor reported a Machine Check Exception (MCE)
+ 5 _/B 32 bad page referenced or some unexpected page flags
+ 6 _/U 64 taint requested by userspace application
+ 7 _/D 128 kernel died recently, i.e. there was an OOPS or BUG
+ 8 _/A 256 ACPI table overridden by user
+ 9 _/W 512 kernel issued warning
+ 10 _/C 1024 staging driver was loaded
+ 11 _/I 2048 workaround for bug in platform firmware applied
+ 12 _/O 4096 externally-built ("out-of-tree") module was loaded
+ 13 _/E 8192 unsigned module was loaded
+ 14 _/L 16384 soft lockup occurred
+ 15 _/K 32768 kernel has been live patched
+ 16 _/X 65536 auxiliary taint, defined for and used by distros
+ 17 _/T 131072 kernel was built with the struct randomization plugin
+ 18 _/N 262144 an in-kernel test has been run
+ 19 _/J 524288 userspace used a mutating debug operation in fwctl
+ 20 _/V 1048576 an unsafe eBPF program (mutating helper) was loaded
+=== === ======= ========================================================
Note: The character ``_`` is representing a blank in this table to make reading
easier.
@@ -189,3 +190,8 @@ More detailed explanation for tainting
19) ``J`` if userspace opened /dev/fwctl/* and performed a FWTCL_RPC_DEBUG_WRITE
to use the devices debugging features. Device debugging features could
cause the device to malfunction in undefined ways.
+
+ 20) ``V`` if an eBPF program utilising unsafe, mutating helpers (such as
+ bpf_probe_write_user() or bpf_override_return()) was loaded. These helpers
+ bypass standard eBPF safety guarantees and can alter execution flow or
+ corrupt memory.
diff --git a/include/linux/bpf.h b/include/linux/bpf.h
index b4b703c90ca9..b2e236a7ed0d 100644
--- a/include/linux/bpf.h
+++ b/include/linux/bpf.h
@@ -1698,6 +1698,7 @@ struct bpf_prog_aux {
bool changes_pkt_data;
bool might_sleep;
bool kprobe_write_ctx;
+ bool taints_kernel;
u64 prog_array_member_cnt; /* counts how many times as member of prog_array */
struct mutex ext_mutex; /* mutex for is_extended and prog_array_member_cnt */
struct bpf_arena *arena;
diff --git a/include/linux/panic.h b/include/linux/panic.h
index f1dd417e54b2..8622c02c2c24 100644
--- a/include/linux/panic.h
+++ b/include/linux/panic.h
@@ -88,7 +88,8 @@ static inline void set_arch_panic_timeout(int timeout, int arch_default_timeout)
#define TAINT_RANDSTRUCT 17
#define TAINT_TEST 18
#define TAINT_FWCTL 19
-#define TAINT_FLAGS_COUNT 20
+#define TAINT_UNSAFE_BPF 20
+#define TAINT_FLAGS_COUNT 21
#define TAINT_FLAGS_MAX ((1UL << TAINT_FLAGS_COUNT) - 1)
struct taint_flag {
diff --git a/kernel/bpf/syscall.c b/kernel/bpf/syscall.c
index a3c0214ca934..34b25609e72b 100644
--- a/kernel/bpf/syscall.c
+++ b/kernel/bpf/syscall.c
@@ -3083,6 +3083,13 @@ static int bpf_prog_load(union bpf_attr *attr, bpfptr_t uattr, u32 uattr_size)
if (err < 0)
goto free_used_maps;
+ /*
+ * The program has passed the verifier. If it utilises unsafe
+ * helpers, formally taint the kernel now.
+ */
+ if (prog->aux->taints_kernel)
+ add_taint(TAINT_UNSAFE_BPF, LOCKDEP_STILL_OK);
+
err = bpf_prog_mark_insn_arrays_ready(prog);
if (err < 0)
goto free_used_maps;
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 69d75515ed3f..9d56082a2ac1 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -10287,6 +10287,14 @@ static int check_helper_call(struct bpf_verifier_env *env, struct bpf_insn *insn
return err;
}
+ /*
+ * Flag the program if it attempts to use mutating helpers.
+ * The actual taint is deferred until successful verification.
+ */
+ if (func_id == BPF_FUNC_probe_write_user ||
+ func_id == BPF_FUNC_override_return)
+ env->prog->aux->taints_kernel = true;
+
/* eBPF programs must be GPL compatible to use GPL-ed functions */
if (!env->prog->gpl_compatible && fn->gpl_only) {
verbose(env, "cannot call GPL-restricted function from non-GPL compatible program\n");
diff --git a/kernel/panic.c b/kernel/panic.c
index 20feada5319d..1ae19bd8fc1d 100644
--- a/kernel/panic.c
+++ b/kernel/panic.c
@@ -825,6 +825,7 @@ const struct taint_flag taint_flags[TAINT_FLAGS_COUNT] = {
TAINT_FLAG(RANDSTRUCT, 'T', ' '),
TAINT_FLAG(TEST, 'N', ' '),
TAINT_FLAG(FWCTL, 'J', ' '),
+ TAINT_FLAG(UNSAFE_BPF, 'V', ' '),
};
#undef TAINT_FLAG
diff --git a/tools/debugging/kernel-chktaint b/tools/debugging/kernel-chktaint
index e1571c04afb5..c0fbd7bcfcfd 100755
--- a/tools/debugging/kernel-chktaint
+++ b/tools/debugging/kernel-chktaint
@@ -211,6 +211,14 @@ else
addout "J"
echo " * fwctl's mutating debug interface was used (#19)"
fi
+
+T=`expr $T / 2`
+if [ `expr $T % 2` -eq 0 ]; then
+ addout " "
+else
+ addout "V"
+ echo " * an unsafe eBPF program (mutating helper) was loaded (#20)"
+fi
echo "Raw taint value as int/string: $taint/'$out'"
# report on any tainted loadable modules
--
2.51.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