* [PATCH v3 07/13] rv: Simplify hybrid automata monitors's clock variables
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.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.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v3:
- fix wrongly passing expire to ha_invariant_passed_jiffy()
- typo
---
include/rv/ha_monitor.h | 64 ++++++------------------
kernel/trace/rv/monitors/nomiss/nomiss.c | 18 +------
kernel/trace/rv/monitors/stall/stall.c | 2 +-
3 files changed, 19 insertions(+), 65 deletions(-)
diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h
index 28d3c74cabfc..9144b4c06f3f 100644
--- a/include/rv/ha_monitor.h
+++ b/include/rv/ha_monitor.h
@@ -327,19 +327,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.
*/
/*
@@ -353,31 +342,21 @@ static inline void ha_reset_clk_ns(struct ha_monitor *ha_mon, enum envs env, u64
{
WRITE_ONCE(ha_mon->env_store[env], time_ns);
}
-static inline void ha_set_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
- u64 value, u64 time_ns)
-{
- WRITE_ONCE(ha_mon->env_store[env], time_ns + value);
-}
-static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon,
- enum envs env, u64 time_ns)
+static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
+ u64 time_ns, u64 expire_ns)
{
- return READ_ONCE(ha_mon->env_store[env]) >= time_ns;
+ return READ_ONCE(ha_mon->env_store[env]) >= time_ns - expire_ns;
}
/*
* ha_invariant_passed_ns - prepare the invariant and return the time since reset
*/
-static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env,
- u64 expire, u64 time_ns)
+static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
{
- u64 passed = 0;
-
if (env < 0 || env >= ENV_MAX_STORED)
return 0;
if (ha_monitor_env_invalid(ha_mon, env))
return 0;
- passed = ha_get_env(ha_mon, env, time_ns);
- ha_set_invariant_ns(ha_mon, env, expire - passed, time_ns);
- return passed;
+ return ha_get_env(ha_mon, env, time_ns);
}
/*
@@ -391,32 +370,21 @@ static inline void ha_reset_clk_jiffy(struct ha_monitor *ha_mon, enum envs env)
{
WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64());
}
-static inline void ha_set_invariant_jiffy(struct ha_monitor *ha_mon,
- enum envs env, u64 value)
+static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon, enum envs env,
+ u64 time_ns, u64 expire_jiffy)
{
- WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64() + value);
-}
-static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon,
- enum envs env, u64 time_ns)
-{
- return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64());
-
+ return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64() - expire_jiffy);
}
/*
* ha_invariant_passed_jiffy - prepare the invariant and return the time since reset
*/
-static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env,
- u64 expire, u64 time_ns)
+static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
{
- u64 passed = 0;
-
if (env < 0 || env >= ENV_MAX_STORED)
return 0;
if (ha_monitor_env_invalid(ha_mon, env))
return 0;
- passed = ha_get_env(ha_mon, env, time_ns);
- ha_set_invariant_jiffy(ha_mon, env, expire - passed);
- return passed;
+ return ha_get_env(ha_mon, env, time_ns);
}
/*
@@ -463,14 +431,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);
@@ -516,7 +484,7 @@ static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
int mode = HRTIMER_MODE_REL_HARD;
- u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);
+ u64 passed = ha_invariant_passed_ns(ha_mon, env, time_ns);
if (RV_MON_TYPE == RV_MON_PER_CPU)
mode |= HRTIMER_MODE_PINNED;
@@ -525,7 +493,7 @@ static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
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);
ha_start_timer_ns(ha_mon, ENV_MAX_STORED,
jiffies_to_nsecs(expire - passed), time_ns);
diff --git a/kernel/trace/rv/monitors/nomiss/nomiss.c b/kernel/trace/rv/monitors/nomiss/nomiss.c
index 8ead8783c29f..515ece5ce0ca 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 3c38fb1a0159..b265578f845c 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 v3 09/13] verification/rvgen: Delete __parse_constraint()
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
All previous users of self.invariants and self.guards have been converted
to the Lark parser, delete __parse_constraints() and its associates.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 67 ++-----------------------
1 file changed, 4 insertions(+), 63 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 6d346a718a39..a38ef735a861 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -177,7 +177,6 @@ class ha2k(dot2k):
if not self.is_hybrid_automata():
raise AutomataError("Detected deterministic automaton, use the 'da' class")
self.trace_h = self._read_template_file("trace_hybrid.h")
- self.__parse_constraints()
self.has_invariant = False
self.has_guard = False
for state in self._states:
@@ -304,64 +303,6 @@ class ha2k(dot2k):
separator = "\n\t\t " if sum(len(r) for r in rules) > 80 else " "
return ["res = " + separator.join(rules) + ";"]
- def __validate_constraint(self, key: tuple[int, int] | int, constr: str,
- rule, reset) -> None:
- # event constrains are tuples and allow both rules and reset
- # state constraints are only used for expirations (e.g. clk<N)
- if self.is_event_constraint(key):
- if not rule and not reset:
- raise AutomataError("Unrecognised event constraint "
- f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
- if rule and (rule["env"] in self.env_types and
- rule["env"] not in self.env_stored):
- raise AutomataError("Clocks in hybrid automata always require a storage"
- f" ({rule["env"]})")
- else:
- if not rule:
- raise AutomataError("Unrecognised state constraint "
- f"({self.states[key]}: {constr})")
- if rule["env"] not in self.env_stored:
- raise AutomataError("State constraints always require a storage "
- f"({rule["env"]})")
- if rule["op"] not in ["<", "<="]:
- raise AutomataError("State constraints must be clock expirations like"
- f" clk<N ({rule.string})")
-
- def __parse_constraints(self) -> None:
- self.guards: dict[_EventConstraintKey, str] = {}
- self.invariants: dict[_StateConstraintKey, str] = {}
- for key, constraint in self.constraints.items():
- rules = []
- resets = []
- for c, sep in self._split_constraint_expr(constraint):
- rule = self.constraint_rule.search(c)
- reset = self.constraint_reset.search(c)
- self.__validate_constraint(key, c, rule, reset)
- if rule:
- value = rule["val"]
- value_len = len(rule["val"])
- unit = None
- if rule.groupdict().get("unit"):
- value_len += len(rule["unit"])
- unit = rule["unit"]
- c = c[:-(value_len)]
- value = self.__adjust_value(value, unit)
- if self.is_event_constraint(key):
- c = self.__parse_single_constraint(rule, value)
- if sep:
- c += f" {sep}"
- else:
- c = self.__parse_timer_constraint(rule, value)
- rules.append(c)
- if reset:
- c = f"ha_reset_env(ha_mon, {reset["env"]}{self.enum_suffix}, time_ns)"
- resets.append(c)
- if self.is_event_constraint(key):
- res = self.__format_guard_rules(rules) + resets
- self.guards[key] = ";".join(res)
- else:
- self.invariants[key] = rules[0]
-
def __fill_verify_invariants_func(self) -> list[str]:
if not self.has_invariant:
return []
@@ -486,15 +427,15 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
{{""")
- if self.invariants:
+ if self.has_invariant:
buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, "
"event, next_state, time_ns))\n\t\treturn false;\n")
- if self.guards:
+ if self.has_guard:
buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
"next_state, time_ns))\n\t\treturn false;\n")
- if self.invariants:
+ if self.has_invariant:
buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n")
buff.append("\treturn true;\n}\n")
@@ -571,7 +512,7 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func()
def _fill_timer_type(self) -> list:
- if self.invariants:
+ if self.has_invariant:
return [
"/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */",
"#define HA_TIMER_TYPE HA_TIMER_HRTIMER"
--
2.47.3
^ permalink raw reply related
* [PATCH v3 11/13] verification/rvgen: Switch __create_matrix() to Lark
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
Switch __create_matrix() to use the transitions parsed by Lark to avoid all
the raw text parsing.
Also stop parsing constraints in __create_matrix(), that is not used
anymore.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 47 ++++++----------------
tools/verification/rvgen/rvgen/dot2k.py | 2 +-
2 files changed, 13 insertions(+), 36 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 2e26bb863245..4c302f5cba68 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -418,7 +418,7 @@ class Automata:
self.constraint_vars = set()
self.self_loop_reset_events = set()
self.events, self.envs = self.__get_event_variables()
- self.function, self.constraints = self.__create_matrix()
+ self.function = self.__create_matrix()
self.events_start, self.events_start_run = self.__store_init_events()
self.env_stored = sorted(self.env_stored)
self.constraint_vars = sorted(self.constraint_vars)
@@ -636,10 +636,10 @@ class Automata:
if constraint.val[0].isalpha():
self.constraint_vars.add(constraint.val)
- def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]:
+ def __create_matrix(self) -> list[list[str]]:
# transform the array into a dictionary
events = self.events
- states = self.states
+ states = [s.name for s in self._states]
events_dict = {}
states_dict = {}
nr_event = 0
@@ -654,39 +654,16 @@ class Automata:
# declare the matrix....
matrix = [[self.invalid_state_str for _ in range(nr_event)] for _ in range(nr_state)]
- constraints: dict[_ConstraintKey, list[str]] = {}
- # and we are back! Let's fill the matrix
- cursor = self.__get_cursor_begin_events()
-
- for line in map(str.lstrip,
- islice(self.__dot_lines, cursor, None)):
-
- if not line or line[0] != '"':
- break
-
- split_line = line.split()
-
- if len(split_line) > 2 and split_line[1] == "->":
- origin_state = split_line[0].replace('"', '').replace(',', '_')
- dest_state = split_line[2].replace('"', '').replace(',', '_')
- possible_events = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
- for event in possible_events.split("\\n"):
- event, *constr = event.split(";")
- if constr:
- key = _EventConstraintKey(states_dict[origin_state], events_dict[event])
- constraints[key] = constr
- # those events reset also on self loops
- if origin_state == dest_state and "reset" in "".join(constr):
- self.self_loop_reset_events.add(event)
- matrix[states_dict[origin_state]][events_dict[event]] = dest_state
- else:
- state = line.split("label")[1].split('"')[1]
- state, *constr = state.replace(" ", "").split("\\n")
- if constr:
- constraints[_StateConstraintKey(states_dict[state])] = constr
-
- return matrix, constraints
+ for transition in self.transitions:
+ src, dst = transition.src, transition.dst
+ event = transition.event
+ if src == dst and transition.reset:
+ # those events reset also on self loops
+ self.self_loop_reset_events.add(event)
+ matrix[states_dict[src]][events_dict[event]] = dst
+
+ return matrix
def __store_init_events(self) -> tuple[list[bool], list[bool]]:
events_start = [False] * len(self.events)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index a38ef735a861..dc6d6f33729b 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -403,7 +403,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
def __fill_constr_func(self) -> list[str]:
buff = []
- if not self.constraints:
+ if not self.has_invariant and not self.has_guard:
return []
buff.append(
--
2.47.3
^ permalink raw reply related
* [PATCH v3 06/13] verification/rvgen: Convert __fill_verify_guards_func() to Lark
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.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.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 38 +++++++++++++++++++------
1 file changed, 30 insertions(+), 8 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 1b29792ed630..e91717fde30d 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -221,6 +221,19 @@ class ha2k(dot2k):
def __parse_single_constraint(self, rule: dict, value: str) -> str:
return f"ha_get_env(ha_mon, {rule["env"]}{self.enum_suffix}, time_ns) {rule["op"]} {value}"
+ def __parse_guard_rule(self, rule) -> list[str]:
+ buff = []
+ for c, sep in rule.rules:
+ env = c.env + self.enum_suffix
+ op = c.op
+ val = self.__adjust_value(c.val, c.unit)
+
+ cond = f"ha_get_env(ha_mon, {env}, time_ns) {op} {val}"
+ if sep:
+ cond += f" {sep}"
+ buff.append(cond)
+ return buff
+
def __get_constraint_env(self, constr: str) -> str:
"""Extract the second argument from an ha_ function"""
env = constr.split("(")[1].split()[1].rstrip(")").rstrip(",")
@@ -287,7 +300,7 @@ class ha2k(dot2k):
rules = invalid_checks + rules
separator = "\n\t\t " if sum(len(r) for r in rules) > 80 else " "
- return ["res = " + separator.join(rules)]
+ return ["res = " + separator.join(rules) + ";"]
def __validate_constraint(self, key: tuple[int, int] | int, constr: str,
rule, reset) -> None:
@@ -406,7 +419,8 @@ f"""static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
def __fill_verify_guards_func(self) -> list[str]:
buff = []
- if not self.guards:
+
+ if not self.has_guard:
return []
buff.append(
@@ -418,14 +432,22 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
""")
_else = ""
- for edge, constr in sorted(self.guards.items()):
+ for transition in self.transitions:
+ if not transition.rule and not transition.reset:
+ continue
+
buff.append(f"\t{_else}if (curr_state == "
- f"{self.states[edge[0]]}{self.enum_suffix} && "
- f"event == {self.events[edge[1]]}{self.enum_suffix})")
- if constr.count(";") > 0:
+ f"{transition.src}{self.enum_suffix} && "
+ f"event == {transition.event}{self.enum_suffix})")
+ rule = transition.rule
+ reset = transition.reset
+ if rule and reset:
buff[-1] += " {"
- buff += [f"\t\t{c};" for c in constr.split(";")]
- if constr.count(";") > 0:
+ if rule:
+ buff.append("\t\t" + self.__format_guard_rules(self.__parse_guard_rule(rule))[0])
+ if reset:
+ buff.append(f"\t\tha_reset_env(ha_mon, {reset.env}{self.enum_suffix}, time_ns);")
+ if rule and reset:
_else = "} else "
else:
_else = "else "
--
2.47.3
^ permalink raw reply related
* [PATCH v3 10/13] verification/rvgen: Switch __get_event_variables() to Lark
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
Switch __get_event_variables() to use the parsed results from Lark, instead
of raw text processing.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 78 ++++++----------------
1 file changed, 19 insertions(+), 59 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index b86275e7bf28..2e26bb863245 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -591,45 +591,22 @@ class Automata:
def __get_event_variables(self) -> tuple[list[str], list[str]]:
events: list[str] = []
envs: list[str] = []
- # here we are at the begin of transitions, take a note, we will return later.
- cursor = self.__get_cursor_begin_events()
- for line in map(str.lstrip, islice(self.__dot_lines, cursor, None)):
- if not line.startswith('"'):
- break
+ for transition in self.transitions:
+ events.append(transition.event)
- # transitions have the format:
- # "all_fired" -> "both_fired" [ label = "disable_irq" ];
- # ------------ event is here ------------^^^^^
- split_line = line.split()
- if len(split_line) > 1 and split_line[1] == "->":
- event = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
-
- # when a transition has more than one label, they are like this
- # "local_irq_enable\nhw_local_irq_enable_n"
- # so split them.
-
- for i in event.split("\\n"):
- # if the event contains a constraint (hybrid automata),
- # it will be separated by a ";":
- # "sched_switch;x<1000;reset(x)"
- ev, *constr = i.split(";")
- if constr:
- if len(constr) > 2:
- raise AutomataError("Only 1 constraint and 1 reset are supported")
- envs += self.__extract_env_var(constr)
- events.append(ev)
- else:
- # state labels have the format:
- # "enable_fired" [label = "enable_fired\ncondition"];
- # ----- label is here -----^^^^^
- # label and node name must be the same, condition is optional
- state = line.split("label")[1].split('"')[1]
- _, *constr = state.split("\\n")
- if constr:
- if len(constr) > 1:
- raise AutomataError("Only 1 constraint is supported in the state")
- envs += self.__extract_env_var([constr[0].replace(" ", "")])
+ if transition.reset:
+ envs.append(transition.reset.env)
+ self.env_stored.add(transition.reset.env)
+ if transition.rule:
+ for c, _ in transition.rule.rules:
+ envs.append(c.env)
+ self.__extract_env_var(c)
+
+ for state in self._states:
+ if state.inv:
+ envs.append(state.inv.env)
+ self.__extract_env_var(state.inv)
return sorted(set(events)), sorted(set(envs))
@@ -653,28 +630,11 @@ class Automata:
seps.append(None)
return zip(exprs, seps)
- def __extract_env_var(self, constraint: list[str]) -> list[str]:
- env = []
- for c, _ in self._split_constraint_expr(constraint):
- rule = self.constraint_rule.search(c)
- reset = self.constraint_reset.search(c)
- if rule:
- env.append(rule["env"])
- if rule.groupdict().get("unit"):
- self.env_types[rule["env"]] = rule["unit"]
- if rule["val"][0].isalpha():
- self.constraint_vars.add(rule["val"])
- # try to infer unit from constants or parameters
- val_for_unit = rule["val"].lower().replace("()", "")
- if val_for_unit.endswith("_ns"):
- self.env_types[rule["env"]] = "ns"
- if val_for_unit.endswith("_jiffies"):
- self.env_types[rule["env"]] = "j"
- if reset:
- env.append(reset["env"])
- # environment variables that are reset need a storage
- self.env_stored.add(reset["env"])
- return env
+ def __extract_env_var(self, constraint: ConstraintCondition):
+ if constraint.unit:
+ self.env_types[constraint.env] = constraint.unit
+ if constraint.val[0].isalpha():
+ self.constraint_vars.add(constraint.val)
def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]:
# transform the array into a dictionary
--
2.47.3
^ permalink raw reply related
* [PATCH v3 08/13] verification/rvgen: Simplify the generation for clock variables
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.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 | 96 +------------------------
1 file changed, 3 insertions(+), 93 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index e91717fde30d..6d346a718a39 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -246,7 +246,9 @@ class ha2k(dot2k):
if inv.unit == "j":
clock_type = "jiffy"
- return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns)"
+ value = self.__adjust_value(inv.val, inv.unit)
+
+ return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {value})"
def __start_to_conv(self, constr: str) -> str:
"""
@@ -383,40 +385,6 @@ f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
buff.append("\treturn true;\n}\n")
return buff
- def __fill_convert_inv_guard_func(self) -> list[str]:
- buff = []
- if not self.invariants:
- return []
-
- conflict_guards, conflict_invs = self.__find_inv_conflicts()
- if not conflict_guards and not conflict_invs:
- return []
-
- buff.append(
-f"""static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
-\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
-\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
-{{""")
- buff.append("\tif (curr_state == next_state)\n\t\treturn;")
-
- _else = ""
- for state, constr in sorted(self.invariants.items()):
- # a state with invariant can reach us without reset
- # multiple conflicts must have the same invariant, otherwise we cannot
- # know how to reset the value
- conf_i = [start for start, end in conflict_invs if end == state]
- # we can reach a guard without reset
- conf_g = [e for s, e in conflict_guards if s == state]
- if not conf_i and not conf_g:
- continue
- buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
-
- buff.append(f"\t\t{self.__start_to_conv(constr)};")
- _else = "else "
-
- buff.append("}\n")
- return buff
-
def __fill_verify_guards_func(self) -> list[str]:
buff = []
@@ -456,54 +424,6 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
buff.append("\treturn res;\n}\n")
return buff
- def __find_inv_conflicts(self) -> tuple[set[tuple[int, _EventConstraintKey]],
- set[tuple[int, _StateConstraintKey]]]:
- """
- Run a breadth first search from all states with an invariant.
- Find any conflicting constraints reachable from there, this can be
- another state with an invariant or an edge with a non-reset guard.
- Stop when we find a reset.
-
- Return the set of conflicting guards and invariants as tuples of
- conflicting state and constraint key.
- """
- conflict_guards: set[tuple[int, _EventConstraintKey]] = set()
- conflict_invs: set[tuple[int, _StateConstraintKey]] = set()
- for start_idx in self.invariants:
- queue = deque([(start_idx, 0)]) # (state_idx, distance)
- env = self.__get_constraint_env(self.invariants[start_idx])
-
- while queue:
- curr_idx, distance = queue.popleft()
-
- # Check state condition
- if curr_idx != start_idx and curr_idx in self.invariants:
- conflict_invs.add((start_idx, _StateConstraintKey(curr_idx)))
- continue
-
- # Check if we should stop
- if distance > len(self.states):
- break
- if curr_idx != start_idx and distance > 1:
- continue
-
- for event_idx, next_state_name in enumerate(self.function[curr_idx]):
- if next_state_name == self.invalid_state_str:
- continue
- curr_guard = self.guards.get((curr_idx, event_idx), "")
- if "reset" in curr_guard and env in curr_guard:
- continue
-
- if env in curr_guard:
- conflict_guards.add((start_idx,
- _EventConstraintKey(curr_idx, event_idx)))
- continue
-
- next_idx = self.states.index(next_state_name)
- queue.append((next_idx, distance + 1))
-
- return conflict_guards, conflict_invs
-
def __fill_setup_invariants_func(self) -> list[str]:
if not self.has_invariant:
return []
@@ -554,16 +474,9 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
* the next state has a constraint, cancel it in any other case and to check
* that it didn't expire before the callback run. Transitions to the same state
* without a reset never affect timers.
- * Due to the different representations between invariants and guards, there is
- * a function to convert it in case invariants or guards are reachable from
- * another invariant without reset. Those are not present if not required in
- * the model. This is all automatic but is worth checking because it may show
- * errors in the model (e.g. missing resets).
*/""")
buff += self.__fill_verify_invariants_func()
- inv_conflicts = self.__fill_convert_inv_guard_func()
- buff += inv_conflicts
buff += self.__fill_verify_guards_func()
buff += self.__fill_setup_invariants_func()
@@ -576,9 +489,6 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
if self.invariants:
buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, "
"event, next_state, time_ns))\n\t\treturn false;\n")
- if inv_conflicts:
- buff.append("\tha_convert_inv_guard(ha_mon, curr_state, event, "
- "next_state, time_ns);\n")
if self.guards:
buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
--
2.47.3
^ permalink raw reply related
* [PATCH v3 05/13] verification/rvgen: Convert __fill_setup_invariants_func() to Lark
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.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.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 44 ++++++++++++++++++++-----
1 file changed, 35 insertions(+), 9 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 0595bfcd232e..1b29792ed630 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -250,6 +250,26 @@ class ha2k(dot2k):
return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.enum_suffix},"
f" {value}, time_ns)")
+ def __parse_invariant(self, inv):
+ # by default assume the timer has ns expiration
+ clock_type = "ns"
+ if inv.unit == "j":
+ clock_type = "jiffy"
+
+ env = inv.env + self.enum_suffix
+ val = inv.val.replace("()", "(ha_mon)")
+
+ match inv.unit:
+ case "us":
+ val *= 10**3
+ case "ms":
+ val *= 10**6
+ case "s":
+ val *= 10**9
+
+ return (f"ha_start_timer_{clock_type}(ha_mon, {env},"
+ f" {val}, time_ns)")
+
def __format_guard_rules(self, rules: list[str]) -> list[str]:
"""
Merge guard constraints as a single C return statement.
@@ -463,15 +483,14 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
return conflict_guards, conflict_invs
def __fill_setup_invariants_func(self) -> list[str]:
- buff = []
- if not self.invariants:
+ if not self.has_invariant:
return []
- buff.append(
+ buff = [
f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
-{{""")
+{{"""]
conditions = ["next_state == curr_state"]
conditions += [f"event != {e}{self.enum_suffix}"
@@ -480,13 +499,20 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
buff.append(f"\tif ({condition_str})\n\t\treturn;")
_else = ""
- for state, constr in sorted(self.invariants.items()):
- buff.append(f"\t{_else}if (next_state == {self.states[state]}{self.enum_suffix})")
- buff.append(f"\t\t{constr};")
+ for state in self._states:
+ inv = state.inv
+ if not inv:
+ continue
+ inv = self.__parse_invariant(inv)
+ buff.append(f"\t{_else}if (next_state == {state.name}{self.enum_suffix})")
+ buff.append(f"\t\t{inv};")
_else = "else "
- for state in self.invariants:
- buff.append(f"\telse if (curr_state == {self.states[state]}{self.enum_suffix})")
+ for state in self._states:
+ inv = state.inv
+ if not inv:
+ continue
+ buff.append(f"\telse if (curr_state == {state.name}{self.enum_suffix})")
buff.append("\t\tha_cancel_timer(ha_mon);")
buff.append("}\n")
--
2.47.3
^ permalink raw reply related
* [PATCH v3 04/13] verification/rvgen: Convert __fill_verify_invariants_func() to Lark
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.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.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v3:
- remove unused import
---
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 110cfd69e53a..0595bfcd232e 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 ConstraintCondition
class dot2k(Monitor, Dot2c):
@@ -177,6 +178,14 @@ class ha2k(dot2k):
raise AutomataError("Detected deterministic automaton, use the 'da' class")
self.trace_h = self._read_template_file("trace_hybrid.h")
self.__parse_constraints()
+ self.has_invariant = False
+ self.has_guard = False
+ for state in self._states:
+ if state.inv:
+ self.has_invariant = True
+ for transition in self.transitions:
+ if transition.rule or transition.reset:
+ self.has_guard = True
def fill_monitor_class_type(self) -> str:
if self._is_id_monitor():
@@ -218,14 +227,13 @@ class ha2k(dot2k):
assert env.removesuffix(f"_{self.name}") in self.envs
return env
- def __start_to_invariant_check(self, constr: str) -> str:
+ def __start_to_invariant_check(self, inv: ConstraintCondition) -> str:
# by default assume the timer has ns expiration
- env = self.__get_constraint_env(constr)
clock_type = "ns"
- if self.env_types.get(env.removesuffix(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 v3 01/13] verification/rvgen: Switch LTL parser to Lark
From: Nam Cao @ 2026-06-08 8:56 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.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]
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/__main__.py | 5 +-
tools/verification/rvgen/rvgen/ltl2ba.py | 202 +++++++++--------------
2 files changed, 82 insertions(+), 125 deletions(-)
diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 5c923dc10d0f..0915cf86e43b 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -14,6 +14,7 @@ if __name__ == '__main__':
from rvgen.container import Container
from rvgen.ltl2k import ltl2k
from rvgen.automata import AutomataError
+ from rvgen.ltl2ba import LTLError
import argparse
import sys
@@ -57,8 +58,8 @@ if __name__ == '__main__':
sys.exit(1)
else:
monitor = Container(vars(params))
- except AutomataError as e:
- print(f"There was an error processing {params.spec}: {e}", file=sys.stderr)
+ except (AutomataError, LTLError) as e:
+ print(f"There was an error processing {params.spec}:\n{e}", file=sys.stderr)
sys.exit(1)
print(f"Writing the monitor into the directory {monitor.name}")
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index 016e7cf93bbb..7cebda61bce8 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -7,9 +7,7 @@
# https://doi.org/10.1007/978-0-387-34892-6_1
# With extra optimizations
-from ply.lex import lex
-from ply.yacc import yacc
-from .automata import AutomataError
+import lark
# Grammar:
# ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
@@ -30,42 +28,41 @@ from .automata import AutomataError
# imply
# equivalent
-tokens = (
- 'AND',
- 'OR',
- 'IMPLY',
- 'UNTIL',
- 'ALWAYS',
- 'EVENTUALLY',
- 'NEXT',
- 'VARIABLE',
- 'LITERAL',
- 'NOT',
- 'LPAREN',
- 'RPAREN',
- 'ASSIGN',
-)
-
-t_AND = r'and'
-t_OR = r'or'
-t_IMPLY = r'imply'
-t_UNTIL = r'until'
-t_ALWAYS = r'always'
-t_NEXT = r'next'
-t_EVENTUALLY = r'eventually'
-t_VARIABLE = r'[A-Z_0-9]+'
-t_LITERAL = r'true|false'
-t_NOT = r'not'
-t_LPAREN = r'\('
-t_RPAREN = r'\)'
-t_ASSIGN = r'='
-t_ignore_COMMENT = r'\#.*'
-t_ignore = ' \t\n'
-
-def t_error(t):
- raise AutomataError(f"Illegal character '{t.value[0]}'")
-
-lexer = lex()
+GRAMMAR = r'''
+start: assign+
+
+assign: VARIABLE "=" _ltl
+
+_ltl: _opd | binop | unop
+
+_opd : VARIABLE
+ | LITERAL
+ | "(" _ltl ")"
+
+unop: UNOP _ltl
+UNOP: "always"
+ | "eventually"
+ | "next"
+ | "not"
+
+binop: _opd BINOP _ltl
+BINOP: "until"
+ | "and"
+ | "or"
+ | "imply"
+
+VARIABLE: /[A-Z_][A-Z0-9_]*/
+LITERAL: "true" | "false"
+
+COMMENT: "#" /.*/ "\n"
+%ignore COMMENT
+
+%import common.WS
+%ignore WS
+'''
+
+class LTLError(Exception):
+ "Exception raised for malformed linear temporal logic"
class GraphNode:
uid = 0
@@ -97,7 +94,7 @@ class GraphNode:
return self.id < other.id
class ASTNode:
- uid = 1
+ uid = 0
def __init__(self, op):
self.op = op
@@ -433,90 +430,49 @@ class Literal:
node.old |= {n}
return node.expand(node_set)
-def p_spec(p):
- '''
- spec : assign
- | assign spec
- '''
- if len(p) == 3:
- p[2].append(p[1])
- p[0] = p[2]
- else:
- p[0] = [p[1]]
-
-def p_assign(p):
- '''
- assign : VARIABLE ASSIGN ltl
- '''
- p[0] = (p[1], p[3])
-
-def p_ltl(p):
- '''
- ltl : opd
- | binop
- | unop
- '''
- p[0] = p[1]
-
-def p_opd(p):
- '''
- opd : VARIABLE
- | LITERAL
- | LPAREN ltl RPAREN
- '''
- if p[1] == "true":
- p[0] = ASTNode(Literal(True))
- elif p[1] == "false":
- p[0] = ASTNode(Literal(False))
- elif p[1] == '(':
- p[0] = p[2]
- else:
- p[0] = ASTNode(Variable(p[1]))
-
-def p_unop(p):
- '''
- unop : ALWAYS ltl
- | EVENTUALLY ltl
- | NEXT ltl
- | NOT ltl
- '''
- if p[1] == "always":
- op = AlwaysOp(p[2])
- elif p[1] == "eventually":
- op = EventuallyOp(p[2])
- elif p[1] == "next":
- op = NextOp(p[2])
- elif p[1] == "not":
- op = NotOp(p[2])
- else:
- raise AutomataError(f"Invalid unary operator {p[1]}")
-
- p[0] = ASTNode(op)
-
-def p_binop(p):
- '''
- binop : opd UNTIL ltl
- | opd AND ltl
- | opd OR ltl
- | opd IMPLY ltl
- '''
- if p[2] == "and":
- op = AndOp(p[1], p[3])
- elif p[2] == "until":
- op = UntilOp(p[1], p[3])
- elif p[2] == "or":
- op = OrOp(p[1], p[3])
- elif p[2] == "imply":
- op = ImplyOp(p[1], p[3])
- else:
- raise AutomataError(f"Invalid binary operator {p[2]}")
-
- p[0] = ASTNode(op)
-
-parser = yacc()
+class Transform(lark.visitors.Transformer):
+ def unop(self, node):
+ if node[0] == "always":
+ return ASTNode(AlwaysOp(node[1]))
+ if node[0] == "eventually":
+ return ASTNode(EventuallyOp(node[1]))
+ if node[0] == "next":
+ return ASTNode(NextOp(node[1]))
+ if node[0] == "not":
+ return ASTNode(NotOp(node[1]))
+ raise ValueError("Unknown operator %s" % node[0])
+
+ def binop(self, node):
+ if node[1] == "until":
+ return ASTNode(UntilOp(node[0], node[2]))
+ if node[1] == "and":
+ return ASTNode(AndOp(node[0], node[2]))
+ if node[1] == "or":
+ return ASTNode(OrOp(node[0], node[2]))
+ if node[1] == "imply":
+ return ASTNode(ImplyOp(node[0], node[2]))
+ raise ValueError("Unknown operator %s" % node[1])
+
+ def VARIABLE(self, args):
+ return ASTNode(Variable(args))
+
+ def LITERAL(self, args):
+ return ASTNode(Literal(args == "true"))
+
+ def start(self, node):
+ return node
+
+ def assign(self, node):
+ return node[0].op.name, node[1]
+
+parser = lark.Lark(GRAMMAR)
def parse_ltl(s: str) -> ASTNode:
- spec = parser.parse(s)
+ try:
+ spec = parser.parse(s)
+ except lark.exceptions.UnexpectedInput as e:
+ raise LTLError(str(e))
+ spec = Transform().transform(spec)
rule = None
subexpr = {}
@@ -528,7 +484,7 @@ def parse_ltl(s: str) -> ASTNode:
subexpr[assign[0]] = assign[1]
if rule is None:
- raise AutomataError("Please define your specification in the \"RULE = <LTL spec>\" format")
+ raise LTLError("Please define your specification in the \"RULE = <LTL spec>\" format")
for node in rule:
if not isinstance(node.op, Variable):
--
2.47.3
^ permalink raw reply related
* [PATCH v3 03/13] verification/rvgen: Implement state and transition parser based on Lark
From: Nam Cao @ 2026-06-08 8:56 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.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.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 216 +++++++++++++++++++++
1 file changed, 216 insertions(+)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 8649d982383d..b86275e7bf28 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -198,6 +198,164 @@ class ParseTree:
self.node_attrs = attributes_parser.node_attrs
self.edge_attrs = attributes_parser.edge_attrs
+class ConstraintCondition:
+ def __init__(self, env: str, op: str, val: str, unit=None):
+ self.env = env
+ self.op = op
+ self.val = val
+ self.unit = unit
+ if unit is None:
+ # try to infer unit from constants or parameters
+ val_for_unit = val.lower().replace("()", "")
+ if val_for_unit.endswith("_ns"):
+ self.unit = "ns"
+ if val_for_unit.endswith("_jiffies"):
+ self.unit = "j"
+
+class ConstraintRule:
+ grammar = r'''
+ rule: condition (OP condition)*
+
+ OP: "&&" | "||"
+
+ condition: ENV CMP_OP VAL UNIT?
+
+ ENV: CNAME
+
+ CMP_OP: "==" | "<=" | "<" | ">=" | ">"
+
+ VAL: /[0-9]+/
+ | /[A-Z_]+\(\)/
+ | /[A-Z_]+/
+ | /[a-z_]+\(\)/
+ | /[a-z_]+/
+
+ UNIT: "ns" | "us" | "ms" | "s"
+ '''
+
+ def __init__(self, c: ConstraintCondition):
+ '''
+ A list of pairs of
+ - the condition (e.g. is_constr_dl == 1)
+ - the logical operator ("||" or "&&") combining this
+ condition with the next one if it exists, otherwise None
+
+ TODO: Perhaps use an abstract syntax tree instead, because
+ this representation cannot capture precedence
+ '''
+ self.rules = [[c, None]]
+
+ def chain(self, op: str, c: ConstraintCondition):
+ self.rules[-1][1] = op
+ self.rules.append([c, None])
+
+class ConstraintReset:
+ def __init__(self, env):
+ self.env = env
+
+class StateLabelParser:
+ grammar = r'''
+ label: CNAME ("\\n" condition)?
+
+ %import common.CNAME
+ %import common.WS
+ %ignore WS
+ ''' + ConstraintRule.grammar
+
+ parser = lark.Lark(grammar, parser='lalr', start="label")
+
+ def __init__(self, label: str):
+ try:
+ tree = self.parser.parse(label)
+ except lark.exceptions.UnexpectedInput as exc:
+ raise(AutomataError(f"Unrecognised state \"{label}\"\n{exc}"))
+
+ self.state = tree.children[0]
+ self.constraint = None
+
+ if len(tree.children) == 2:
+ self.constraint = ConstraintCondition(*tree.children[1].children)
+ if self.constraint.op not in ("<", "<="):
+ raise AutomataError("State constraints must be clock expirations like"
+ f" clk<N ({label})")
+
+class EventLabelParser:
+ grammar = r'''
+ events: event ("\\n" event)*
+
+ event: name (";" guard)?
+
+ guard: reset
+ | rule
+ | rule ";" reset
+ | reset ";" rule
+
+ name: CNAME
+
+ reset: "reset" "(" ENV ")"
+
+ %import common.CNAME
+ %import common.WS
+ %ignore WS
+ ''' + ConstraintRule.grammar
+
+ parser = lark.Lark(grammar, parser='lalr', start="events")
+
+ class GetEvents(lark.visitors.Transformer):
+ def guard(self, args):
+ reset = None
+ rule = None
+ for arg in args:
+ if arg.data == "reset":
+ reset = ConstraintReset(arg.children[0])
+ elif arg.data == "rule":
+ conditions = arg.children
+ rule = ConstraintRule(conditions[0])
+ for i in range(1, len(conditions), 2):
+ rule.chain(conditions[i], conditions[i + 1])
+ return reset, rule
+
+ def OP(self, args):
+ return args
+
+ def condition(self, args):
+ return ConstraintCondition(*args)
+
+ def event(self, args):
+ assert(len(args) <= 2)
+ name = args[0]
+ rule, reset = None, None
+ if len(args) == 2:
+ reset, rule = args[1]
+ return name, reset, rule
+
+ def events(self, args):
+ return args
+
+ def name(self, args):
+ return args[0]
+
+ def __init__(self, label: str):
+ try:
+ tree = self.parser.parse(label)
+ self.events = self.GetEvents().transform(tree)
+ except lark.exceptions.UnexpectedInput as exc:
+ raise(AutomataError(f"Unrecognised event \"{label}\"\n{exc}"))
+
+class Transition:
+ def __init__(self, src: str, dst: str, event: str,
+ reset: ConstraintReset, rule: ConstraintRule):
+ self.src = src
+ self.dst = dst
+ self.event = event
+ self.rule = rule
+ self.reset = reset
+
+class State:
+ def __init__(self, name: str, inv: ConstraintCondition):
+ self.name = name
+ self.inv = inv
+
class _ConstraintKey:
"""Base class for constraint keys."""
@@ -252,6 +410,8 @@ class Automata:
self.name = model_name or self.__get_model_name()
self.__dot_lines = self.__open_dot()
self.__parse_tree = ParseTree(file_path)
+ self.transitions = self.__parse_transitions()
+ self._states, self._initial_state, self._final_states = self.__parse_states()
self.states, self.initial_state, self.final_states = self.__get_state_variables()
self.env_types = {}
self.env_stored = set()
@@ -327,6 +487,62 @@ class Automata:
return cursor
+ def __parse_transitions(self):
+ transitions = []
+
+ for edge in self.__parse_tree.edges:
+ attr = self.__parse_tree.edge_attrs.get(edge)
+ if not attr:
+ continue
+
+ label = attr.get("label")
+
+ src, dst = edge
+
+ parser = EventLabelParser(label)
+ for event, reset, rule in parser.events:
+ transitions.append(Transition(src, dst, event, reset, rule))
+
+ transitions.sort(key=lambda t : (t.src, t.event))
+ return transitions
+
+ def __parse_states(self):
+ initial_state = ""
+ states = []
+ final_states = []
+
+ for node in self.__parse_tree.nodes:
+ attr = self.__parse_tree.node_attrs[node]
+ label = attr.get("label")
+
+ if node.startswith(Automata.init_marker):
+ initial_state = node[len(Automata.init_marker):]
+
+ if not label:
+ continue
+
+ parser = StateLabelParser(label)
+ state = State(parser.state, parser.constraint)
+
+ states.append(state)
+
+ shape = attr.get("shape")
+ if shape in ("doublecircle", "ellipse"):
+ final_states.append(state)
+
+
+ initial_state = next((s for s in states if s.name == initial_state), None)
+ if not initial_state:
+ raise AutomataError("The automaton doesn't have an initial state")
+
+ if not final_states:
+ final_states.append(initial_state)
+
+ states.remove(initial_state)
+ states.sort(key=lambda s : s.name)
+ states.insert(0, initial_state)
+ return states, initial_state, final_states
+
def __get_state_variables(self) -> tuple[list[str], str, list[str]]:
# wait for node declaration
states = []
--
2.47.3
^ permalink raw reply related
* [PATCH v3 02/13] verification/rvgen: Introduce a parse tree for automata using Lark
From: Nam Cao @ 2026-06-08 8:56 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.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.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 186 +++++++++++++++++++++
1 file changed, 186 insertions(+)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index b9f8149f7118..8649d982383d 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -13,6 +13,191 @@ import re
from typing import Iterator
from itertools import islice
+import lark
+
+class ParseTree:
+ # based on https://graphviz.org/doc/info/lang.html
+ # with the irrelevant stuffs (port and compass) removed
+ grammar = r'''
+ start: "strict"? ("graph" | "digraph") ID? "{" stmt_list "}"
+
+ stmt_list: (stmt ";"? stmt_list)?
+
+ stmt: node_stmt
+ | edge_stmt
+ | attr_stmt
+ | ID "=" ID
+ | subgraph
+
+ attr_stmt: attr_type attr_list
+
+ attr_type: "graph" -> graph
+ | "node" -> node
+ | "edge" -> edge
+
+ attr_list: "[" a_list? "]" attr_list?
+
+ a_list: ID "=" ID (";" | ",")? a_list?
+
+ edge_stmt: (node_id | subgraph) edgerhs attr_list?
+
+ edgerhs: edgeop (node_id | subgraph) edgerhs?
+
+ edgeop: "->" | "--"
+
+ node_stmt: node_id attr_list?
+
+ node_id: ID
+
+ subgraph: ("subgraph" ID?)? "{" stmt_list "}"
+
+ ID: CNAME
+ | /-?(\.[0-9]+|[0-9]+(\.[0-9]*))/
+ | ESCAPED_STRING
+
+ %import common.CNAME
+ %import common.ESCAPED_STRING
+ %import common.WS
+ %ignore WS
+ '''
+
+ @staticmethod
+ def parse_edge(tree: lark.Tree) -> tuple[str, str]:
+ # only support a simple node-to-node edge
+ nodes = []
+ for node in tree.iter_subtrees_topdown():
+ if node.data == "node_id":
+ nodes.append(node.children[0].strip('"'))
+
+ if len(nodes) != 2:
+ raise AutomataError("Only state-to-state transition is supported")
+
+ return tuple(nodes)
+
+ class ParseNodes(lark.visitors.Visitor):
+ def __init__(self, *args, **kwargs):
+ self.nodes = set()
+ super().__init__(*args, **kwargs)
+
+ def node_stmt(self, tree):
+ node_id = tree.children[0]
+ node = node_id.children[0].strip('"')
+ self.nodes.add(node)
+
+ class ParseEdges(lark.visitors.Visitor):
+ def __init__(self, *args, **kwargs):
+ self.edges = set()
+ super().__init__(*args, **kwargs)
+
+ def edge_stmt(self, tree):
+ edge = ParseTree.parse_edge(tree)
+ self.edges.add(edge)
+
+ class ParseAttributes(lark.visitors.Interpreter):
+ def __init__(self, *args, **kwargs):
+ '''
+ Stacks of default attributes. [0] is the default
+ attributes for the outermost scope, while [-1] is the
+ default attributes for the current scope.
+ '''
+ self.default_node_attrs = [{}]
+ self.default_edge_attrs = [{}]
+
+ self.node_attrs = {}
+ self.edge_attrs = {}
+
+ super().__init__(*args, **kwargs)
+
+ @staticmethod
+ def __get_attrs(stmt: lark.Tree) -> dict[str, str]:
+ attrs = {}
+
+ for node in stmt.iter_subtrees():
+ if node.data == "a_list":
+ attrs[node.children[0]] = node.children[1].strip('"')
+
+ return attrs
+
+
+ def subgraph(self, tree):
+ # We are entering a new scope, inherit the default
+ # attributes of the outer scope
+ self.default_node_attrs.append(self.default_node_attrs[-1].copy())
+ self.default_edge_attrs.append(self.default_edge_attrs[-1].copy())
+
+ children = self.visit_children(tree)
+
+ # Exiting the scope
+ del self.default_node_attrs[-1]
+ del self.default_edge_attrs[-1]
+
+ return children
+
+ def node_stmt(self, tree):
+ node_id = tree.children[0]
+ node = node_id.children[0].strip('"')
+
+ attrs = self.default_node_attrs[-1].copy()
+ attrs |= self.__get_attrs(tree)
+
+ if attrs:
+ if node in self.node_attrs:
+ self.node_attrs[node] = attrs | self.node_attrs[node]
+ else:
+ self.node_attrs[node] = attrs
+
+ return self.visit_children(tree)
+
+ def edge_stmt(self, tree):
+ edge = ParseTree.parse_edge(tree)
+
+ attrs = self.default_edge_attrs[-1].copy()
+ attrs |= self.__get_attrs(tree)
+
+ if attrs:
+ if edge in self.edge_attrs:
+ self.edge_attrs[edge] = attrs | self.edge_attrs[edge]
+ else:
+ self.edge_attrs[edge] = attrs
+
+ return self.visit_children(tree)
+
+ def attr_stmt(self, tree):
+ attr_type = tree.children[0].data
+ attrs = self.__get_attrs(tree)
+
+ if attr_type == "node":
+ self.default_node_attrs[-1] |= attrs
+ elif attr_type == "edge":
+ self.default_edge_attrs[-1] |= attrs
+ else:
+ # graph attributes are irrelevant
+ pass
+
+ self.visit_children(tree)
+
+ def __init__(self, dot_file):
+ parser = lark.Lark(self.grammar, parser='lalr')
+ node_parser = self.ParseNodes()
+ edge_parser = self.ParseEdges()
+ attributes_parser = self.ParseAttributes()
+
+ try:
+ with open(dot_file, "r") as f:
+ tree = parser.parse(f.read())
+ attributes_parser.visit(tree)
+ node_parser.visit(tree)
+ edge_parser.visit(tree)
+ except OSError as exc:
+ raise AutomataError(exc.strerror) from exc
+ except lark.exceptions.UnexpectedInput as exc:
+ raise AutomataError(str(exc))
+
+ self.nodes = node_parser.nodes
+ self.edges = edge_parser.edges
+ self.node_attrs = attributes_parser.node_attrs
+ self.edge_attrs = attributes_parser.edge_attrs
+
class _ConstraintKey:
"""Base class for constraint keys."""
@@ -66,6 +251,7 @@ class Automata:
self.__dot_path = file_path
self.name = model_name or self.__get_model_name()
self.__dot_lines = self.__open_dot()
+ self.__parse_tree = ParseTree(file_path)
self.states, self.initial_state, self.final_states = self.__get_state_variables()
self.env_types = {}
self.env_stored = set()
--
2.47.3
^ permalink raw reply related
* [PATCH v3 00/13] rv: Convert rvgen to Lark
From: Nam Cao @ 2026-06-08 8:56 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.
v3..v2: https://lore.kernel.org/lkml/cover.1779956342.git.namcao@linutronix.de/
- remove some redundant imports
- fix build failure due to passing wrong parameters to ha_invariant_passed_jiffy()
v2..v1: https://lore.kernel.org/lkml/cover.1777962130.git.namcao@linutronix.de/
- address human's reviews and sashiko's reviews
- handle lark's exception, yielding a much better error message
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: Simplify 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 | 64 +-
kernel/trace/rv/monitors/nomiss/nomiss.c | 18 +-
kernel/trace/rv/monitors/stall/stall.c | 2 +-
tools/verification/rvgen/__main__.py | 5 +-
tools/verification/rvgen/rvgen/automata.py | 643 +++++++++++++--------
tools/verification/rvgen/rvgen/dot2c.py | 10 +-
tools/verification/rvgen/rvgen/dot2k.py | 290 +++-------
tools/verification/rvgen/rvgen/ltl2ba.py | 202 +++----
8 files changed, 604 insertions(+), 630 deletions(-)
--
2.47.3
^ permalink raw reply
* Re: [PATCH v7 10/42] KVM: guest_memfd: Ensure pages are not in use before conversion
From: Vlastimil Babka (SUSE) @ 2026-06-08 8:55 UTC (permalink / raw)
To: ackerleytng, aik, andrew.jones, binbin.wu, brauner, chao.p.peng,
david, ira.weiny, jmattson, jthoughton, michael.roth, oupton,
pankaj.gupta, qperret, rick.p.edgecombe, rientjes, shivankg,
steven.price, tabba, willy, wyihan, yan.y.zhao, forkloop,
pratyush, suzuki.poulose, aneesh.kumar, liam, Paolo Bonzini,
Sean Christopherson, Thomas Gleixner, Ingo Molnar,
Borislav Petkov, Dave Hansen, x86, H. Peter Anvin, Steven Rostedt,
Masami Hiramatsu, Mathieu Desnoyers, Jonathan Corbet, Shuah Khan,
Shuah Khan, Vishal Annapurve, Andrew Morton, Chris Li,
Kairui Song, Kemeng Shi, Nhat Pham, Baoquan He, Barry Song,
Axel Rasmussen, Yuanchu Xie, Wei Xu, Youngjun Park, Qi Zheng,
Shakeel Butt, Kiryl Shutsemau, Jason Gunthorpe
Cc: kvm, linux-kernel, linux-trace-kernel, linux-doc, linux-kselftest,
linux-mm, linux-coco
In-Reply-To: <20260522-gmem-inplace-conversion-v7-10-2f0fae496530@google.com>
On 5/23/26 02:17, Ackerley Tng via B4 Relay wrote:
> From: Ackerley Tng <ackerleytng@google.com>
>
> When converting memory to private in guest_memfd, it is necessary to ensure
> that the pages are not currently being accessed by any other part of the
> kernel or userspace to avoid any current user writing to guest private
> memory.
>
> guest_memfd checks for unexpected refcounts to determine whether a page is
> still in use. The only expected refcounts after unmapping the range
> requested for conversion are those that are held by guest_memfd itself.
Is it sufficient to only check, and not also freeze the refcount? (i.e.
using folio_ref_freeze()), because without freezing, anything (e.g.
compaction's pfn-based scanner) could do a speculative folio_try_get() and
the checked refcount becomes stale.
Might be ok if we know that no such speculative increment can result in
actually touching the page contents, and the extra refcount and something
inspecting the struct folio won't interfere with anything else. Then it
could be just a comment mentioning why it's safe.
IIRC the compaction's scanning can result in a migration here so it's
probably ok?
> Update the kvm_memory_attributes2 structure to include an error_offset
> field. This allows KVM to report the exact offset where a conversion
> failed to userspace. If the safety check fails, return -EAGAIN and copy
> the error_offset back to userspace so that it can potentially retry the
> operation or handle the failure gracefully.
>
> Suggested-by: David Hildenbrand <david@kernel.org>
> Co-developed-by: Vishal Annapurve <vannapurve@google.com>
> Signed-off-by: Vishal Annapurve <vannapurve@google.com>
> Reviewed-by: Fuad Tabba <tabba@google.com>
> Signed-off-by: Ackerley Tng <ackerleytng@google.com>
> ---
> include/uapi/linux/kvm.h | 3 ++-
> virt/kvm/guest_memfd.c | 68 ++++++++++++++++++++++++++++++++++++++++++++----
> 2 files changed, 65 insertions(+), 6 deletions(-)
>
> diff --git a/include/uapi/linux/kvm.h b/include/uapi/linux/kvm.h
> index e6bbf68a83813..0b55258573d3d 100644
> --- a/include/uapi/linux/kvm.h
> +++ b/include/uapi/linux/kvm.h
> @@ -1658,7 +1658,8 @@ struct kvm_memory_attributes2 {
> __u64 size;
> __u64 attributes;
> __u64 flags;
> - __u64 reserved[12];
> + __u64 error_offset;
> + __u64 reserved[11];
> };
>
> #define KVM_MEMORY_ATTRIBUTE_PRIVATE (1ULL << 3)
> diff --git a/virt/kvm/guest_memfd.c b/virt/kvm/guest_memfd.c
> index 426917d22a2b6..2767992955752 100644
> --- a/virt/kvm/guest_memfd.c
> +++ b/virt/kvm/guest_memfd.c
> @@ -572,9 +572,45 @@ static int kvm_gmem_mas_preallocate(struct ma_state *mas, u64 attributes,
> return mas_preallocate(mas, xa_mk_value(attributes), GFP_KERNEL);
> }
>
> +static bool kvm_gmem_is_safe_for_conversion(struct inode *inode, pgoff_t start,
> + size_t nr_pages, pgoff_t *err_index)
> +{
> + struct address_space *mapping = inode->i_mapping;
> + const int filemap_get_folios_refcount = 1;
> + pgoff_t last = start + nr_pages - 1;
> + struct folio_batch fbatch;
> + bool safe = true;
> + pgoff_t next;
> + int i;
> +
> + folio_batch_init(&fbatch);
> +
> + next = start;
> + while (safe && filemap_get_folios(mapping, &next, last, &fbatch)) {
> +
> + for (i = 0; i < folio_batch_count(&fbatch); ++i) {
> + struct folio *folio = fbatch.folios[i];
> +
> + if (folio_ref_count(folio) !=
> + folio_nr_pages(folio) + filemap_get_folios_refcount) {
> + safe = false;
> + *err_index = max(start, folio->index);
> + break;
> + }
> + }
> +
> + folio_batch_release(&fbatch);
> + cond_resched();
> + }
> +
> + return safe;
> +}
> +
> static int __kvm_gmem_set_attributes(struct inode *inode, pgoff_t start,
> - size_t nr_pages, uint64_t attrs)
> + size_t nr_pages, uint64_t attrs,
> + pgoff_t *err_index)
> {
> + bool to_private = attrs & KVM_MEMORY_ATTRIBUTE_PRIVATE;
> struct address_space *mapping = inode->i_mapping;
> struct gmem_inode *gi = GMEM_I(inode);
> pgoff_t end = start + nr_pages;
> @@ -588,8 +624,21 @@ static int __kvm_gmem_set_attributes(struct inode *inode, pgoff_t start,
>
> mas_init(&mas, mt, start);
> r = kvm_gmem_mas_preallocate(&mas, attrs, start, nr_pages);
> - if (r)
> + if (r) {
> + *err_index = start;
> goto out;
> + }
> +
> + if (to_private) {
> + unmap_mapping_pages(mapping, start, nr_pages, false);
> +
> + if (!kvm_gmem_is_safe_for_conversion(inode, start, nr_pages,
> + err_index)) {
> + mas_destroy(&mas);
> + r = -EAGAIN;
> + goto out;
> + }
> + }
>
> /*
> * From this point on guest_memfd has performed necessary
> @@ -609,9 +658,10 @@ static long kvm_gmem_set_attributes(struct file *file, void __user *argp)
> struct gmem_file *f = file->private_data;
> struct inode *inode = file_inode(file);
> struct kvm_memory_attributes2 attrs;
> + pgoff_t err_index;
> size_t nr_pages;
> pgoff_t index;
> - int i;
> + int i, r;
>
> if (copy_from_user(&attrs, argp, sizeof(attrs)))
> return -EFAULT;
> @@ -635,8 +685,16 @@ static long kvm_gmem_set_attributes(struct file *file, void __user *argp)
>
> nr_pages = attrs.size >> PAGE_SHIFT;
> index = attrs.offset >> PAGE_SHIFT;
> - return __kvm_gmem_set_attributes(inode, index, nr_pages,
> - attrs.attributes);
> + r = __kvm_gmem_set_attributes(inode, index, nr_pages, attrs.attributes,
> + &err_index);
> + if (r) {
> + attrs.error_offset = ((uint64_t)err_index) << PAGE_SHIFT;
> +
> + if (copy_to_user(argp, &attrs, sizeof(attrs)))
> + return -EFAULT;
> + }
> +
> + return r;
> }
>
> static long kvm_gmem_ioctl(struct file *file, unsigned int ioctl,
>
^ permalink raw reply
* Re: [PATCH v7 14/42] KVM: guest_memfd: Handle lru_add fbatch refcounts during conversion safety check
From: Vlastimil Babka (SUSE) @ 2026-06-08 8:45 UTC (permalink / raw)
To: ackerleytng, aik, andrew.jones, binbin.wu, brauner, chao.p.peng,
david, ira.weiny, jmattson, jthoughton, michael.roth, oupton,
pankaj.gupta, qperret, rick.p.edgecombe, rientjes, shivankg,
steven.price, tabba, willy, wyihan, yan.y.zhao, forkloop,
pratyush, suzuki.poulose, aneesh.kumar, liam, Paolo Bonzini,
Sean Christopherson, Thomas Gleixner, Ingo Molnar,
Borislav Petkov, Dave Hansen, x86, H. Peter Anvin, Steven Rostedt,
Masami Hiramatsu, Mathieu Desnoyers, Jonathan Corbet, Shuah Khan,
Shuah Khan, Vishal Annapurve, Andrew Morton, Chris Li,
Kairui Song, Kemeng Shi, Nhat Pham, Baoquan He, Barry Song,
Axel Rasmussen, Yuanchu Xie, Wei Xu, Youngjun Park, Qi Zheng,
Shakeel Butt, Kiryl Shutsemau, Jason Gunthorpe
Cc: kvm, linux-kernel, linux-trace-kernel, linux-doc, linux-kselftest,
linux-mm, linux-coco
In-Reply-To: <20260522-gmem-inplace-conversion-v7-14-2f0fae496530@google.com>
On 5/23/26 02:17, Ackerley Tng via B4 Relay wrote:
> From: Ackerley Tng <ackerleytng@google.com>
>
> When checking if a guest_memfd folio is safe for conversion, its refcount
> is examined. A folio may be present in a per-CPU lru_add fbatch, which
> temporarily increases its refcount. This can lead to a false positive,
> incorrectly indicating that the folio is in use and preventing the
> conversion, even if it is otherwise safe. The conversion process might not
> be on the same CPU that holds the folio in its fbatch, making a simple
> per-CPU check insufficient.
>
> To address this, drain all CPUs' lru_add fbatches if an unexpectedly high
> refcount is encountered during the safety check. This is performed at most
> once per conversion request. Draining only if the folio in question may be
> lru cached.
>
> guest_memfd folios are unevictable, so they can only reside in the lru_add
> fbatch. If the folio's refcount is still unsafe after draining, then the
> conversion is truly deemed unsafe.
>
> Reviewed-by: Fuad Tabba <tabba@google.com>
> Signed-off-by: Ackerley Tng <ackerleytng@google.com>
Acked-by: Vlastimil Babka (SUSE) <vbabka@kernel.org>
^ permalink raw reply
* Re: [PATCH] rethook: Use tsk->on_cpu to check task execution state
From: Tengda Wu @ 2026-06-08 8:31 UTC (permalink / raw)
To: Masami Hiramatsu
Cc: Peter Zijlstra, Josh Poimboeuf, Steven Rostedt, Mathieu Desnoyers,
Alexei Starovoitov, linux-trace-kernel, linux-kernel
In-Reply-To: <20260608115646.97d80d30aed182d468496449@kernel.org>
On 2026/6/8 10:56, Masami Hiramatsu wrote:
> On Mon, 8 Jun 2026 09:52:37 +0800
> Tengda Wu <wutengda@huaweicloud.com> wrote:
>
>>
>>
>> On 2026/6/5 21:43, Masami Hiramatsu wrote:
>>> On Thu, 4 Jun 2026 11:34:45 +0200
>>> Peter Zijlstra <peterz@infradead.org> wrote:
>>>
>>>> On Mon, Jun 01, 2026 at 08:40:01AM +0900, Masami Hiramatsu wrote:
>>>>
>>>>> Peter, is it OK to drop @rq from task_on_cpu()?
>>>>
>>>> Sure.
>>>>
>>>>> Then we can use it from rethook.
>>>>
>>>> Well, it is in sched/sched.h, which is an internal header, and no you
>>>> cannot use that header in rethook.
>>>
>>> Ah, OK. Hmm, then we should not use it. Maybe ->on_cpu is also internal
>>> state?
>>>
>>>>
>>>> But lets step back first, what is the actual problem here, why are we
>>>> looking at ->on_cpu at all?
>>>
>>> Tengda, can you explain it?
>>> I think you want to take a stacktrace on !current process, and
>>> rethook_find_ret_addr() is rejected i the task is running state.
>>>
>>> But if you can share actual situation what you need, it is
>>> helpful for us to understand.
>>>
>>> Thank you,
>>>
>>>
>>
>>
>> Sure.
>>
>> Background: We are verifying the support of live patches for functions that
>> have a kretprobe. The specific verification method is as follows:
>>
>> We construct a function foo() that calls bar():
>>
>> void bar(void)
>> {
>> for (;;) {
>> schedule();
>> }
>> }
>>
>> void foo(void)
>> {
>> bar();
>> }
>>
>> A kretprobe is attached to bar():
>>
>> echo 'r:rp1 bar' > /sys/kernel/tracing/kprobe_events
>> echo 1 > /sys/kernel/tracing/events/kprobes/rp1/enable
>>
>> Then foo() is triggered. The expected behavior is that bar() will call
>> schedule() and yield the CPU.
>>
>> After that, the live patch is activated to attempt replacing the implementation
>> of foo(). The expectation is that this should succeed.
>>
>> However, in reality, because the task that called schedule() is still in the
>> RUNNING state, the condition task_is_running(tsk) inside rethook_find_ret_addr()
>> is not satisfied, causing the function to return early. This, in turn,
>> prevents stack_trace_save_tsk_reliable() from determining the stack as
>> reliable, leading to a failure in activating the live patch.
>
> Hmm is the bar() doing infinite loop, or limited loop but take a long time
> so just yield a while? Anyway, it seems like a non-good design pattern.
> Is it possible to avoid busy loops and instead use Workers, or wait for
> something to complete or for input within a loop?
>
>>
>> **Not sure if this is correct:**
>>
>> We believe that after a task voluntarily calls schedule(), when the stack
>> is expected to be reliable, it is a safe time to activate a live patch.
>
> In this case, I don't know how to block the loop inside the bar.
> Even if !tsk->on_cpu, the tsk can restart running right after checking
> the flag.
>
The infinite loop in bar() is indeed a poor design pattern. This test
case is only artificial, not from real-world code. It is merely
intended to verify live patch support for various cases.
However, the point you raised has indeed made me think. I realize that
checking only tsk->on_cpu is not sufficient -- there is also a race
condition where the task could be scheduled back onto a CPU right after
the check. I need to re-examine the validity of this test case and
whether it represents a safe live patch activation scenario.
Thank you again for your patience and for pointing out these
fundamental issues. Your guidance is much appreciated.
Best regards,
Tengda
^ permalink raw reply
* Re: [PATCH v2 13/13] verification/rvgen: Remove dead code
From: Nam Cao @ 2026-06-08 8:29 UTC (permalink / raw)
To: Gabriele Monaco, Wander Lairson Costa, Steven Rostedt,
linux-trace-kernel, linux-kernel
In-Reply-To: <310e485ce394c7d258e142e14d5e51c5e15e1d30.camel@redhat.com>
Gabriele Monaco <gmonaco@redhat.com> writes:
> You might want to remove unused imports (linters should help you with
> that too):
> * re, typing.Iterator, and itertools.islice from automata.py
> * deque and ConstraintRule from dot2k
Thanks, I overlooked those warnings due to the noises from the existing
warnings :(
Let me clean up the existing pylint issues, so that new warnings are
easily noticed.
Nam
^ permalink raw reply
* Re: [PATCH next] kernel/trace/trace_printk: Use kstrdup() instead of kmalloc() and strcpy()
From: Masami Hiramatsu @ 2026-06-08 8:27 UTC (permalink / raw)
To: david.laight.linux
Cc: Kees Cook, linux-hardening, Arnd Bergmann, linux-kernel,
linux-trace-kernel, Masami Hiramatsu, Steven Rostedt
In-Reply-To: <20260606202633.5018-34-david.laight.linux@gmail.com>
On Sat, 6 Jun 2026 21:26:28 +0100
david.laight.linux@gmail.com wrote:
> From: David Laight <david.laight.linux@gmail.com>
>
> Signed-off-by: David Laight <david.laight.linux@gmail.com>
> ---
> This is one of a group of patches that remove potentially unbounded
> strcpy() calls.
>
> They are mostly replaced by strscpy() or, when strlen() has just been
> called, with memcpy() (usually including the '\0').
>
> Calls with copy string literals into arrays are left unchanged.
> They are safe and easily detected as such.
>
> The changes were made by getting the compiler to detect the calls and
> then fixing the code by hand.
>
> Note that all the changes are only compile tested.
>
> Some Makefiles were changed to allow files to contain strcpy().
> As well as 'difficult to fix' files, this included 'show' functions
> as they really need to use sysfs_emit() or seq_printf().
>
> All the patches are being sent individually to avoid very long cc lists.
> Apologies for the terse commit messages and likely unexpected tags.
> (There are about 100 patches in total.)
>
This looks good to me.
Reviewed-by: Masami Hiramatsu (Google) <mhiramat@kernel.org>
Thanks,
> kernel/trace/trace_printk.c | 3 +--
> 1 file changed, 1 insertion(+), 2 deletions(-)
>
> diff --git a/kernel/trace/trace_printk.c b/kernel/trace/trace_printk.c
> index 3ea17af60169..98171a2398e4 100644
> --- a/kernel/trace/trace_printk.c
> +++ b/kernel/trace/trace_printk.c
> @@ -71,10 +71,9 @@ void hold_module_trace_bprintk_format(const char **start, const char **end)
> fmt = NULL;
> tb_fmt = kmalloc_obj(*tb_fmt);
> if (tb_fmt) {
> - fmt = kmalloc(strlen(*iter) + 1, GFP_KERNEL);
> + fmt = kstrdup(*iter, GFP_KERNEL);
> if (fmt) {
> list_add_tail(&tb_fmt->list, &trace_bprintk_fmt_list);
> - strcpy(fmt, *iter);
> tb_fmt->fmt = fmt;
> } else
> kfree(tb_fmt);
> --
> 2.39.5
>
--
Masami Hiramatsu (Google) <mhiramat@kernel.org>
^ permalink raw reply
* Re: [PATCHv8 bpf-next 28/29] selftests/bpf: Add tracing multi attach benchmark test
From: Jiri Olsa @ 2026-06-08 8:25 UTC (permalink / raw)
To: Alexei Starovoitov
Cc: Alexei Starovoitov, Daniel Borkmann, Andrii Nakryiko, bpf,
linux-trace-kernel, Martin KaFai Lau, Eduard Zingerman, Song Liu,
Yonghong Song, Menglong Dong, Steven Rostedt
In-Reply-To: <DJ30RPYRXESZ.2P3LP98X55VMG@gmail.com>
On Sun, Jun 07, 2026 at 11:13:32AM -0700, Alexei Starovoitov wrote:
> On Sat Jun 6, 2026 at 5:39 AM PDT, Jiri Olsa wrote:
> > Adding benchmark test that attaches to (almost) all allowed tracing
> > functions and display attach/detach times.
> >
> > # ./test_progs -t tracing_multi_bench_attach -v
> > bpf_testmod.ko is already unloaded.
> > Loading bpf_testmod.ko...
> > Successfully loaded bpf_testmod.ko.
> > serial_test_tracing_multi_bench_attach:PASS:btf__load_vmlinux_btf 0 nsec
> > serial_test_tracing_multi_bench_attach:PASS:tracing_multi_bench__open_and_load 0 nsec
> > serial_test_tracing_multi_bench_attach:PASS:get_syms 0 nsec
> > serial_test_tracing_multi_bench_attach:PASS:bpf_program__attach_tracing_multi 0 nsec
> > serial_test_tracing_multi_bench_attach: found 51186 functions
> > serial_test_tracing_multi_bench_attach: attached in 1.295s
> > serial_test_tracing_multi_bench_attach: detached in 0.243s
>
> ...
>
> > + if (!ASSERT_OK(bpf_get_ksyms(&ksyms, true), "get_syms"))
> > + goto cleanup;
> > +
> > + /* Get all ftrace 'safe' symbols.. */
> > + for (i = 0; i < ksyms->filtered_cnt; i++) {
> > + if (!tsearch(&ksyms->filtered_syms[i], &root, compare)) {
> > + ASSERT_FAIL("tsearch failed");
> > + goto cleanup;
> > + }
> > + }
> > +
> > + /* ..and filter them through BTF and btf_type_is_traceable_func. */
> > + nr = btf__type_cnt(btf);
> > + for (type_id = 1; type_id < nr; type_id++) {
> > + const struct btf_type *type;
> > + const char *str;
> > +
> > + type = btf__type_by_id(btf, type_id);
> > + if (!type)
> > + break;
> > +
> > + if (BTF_INFO_KIND(type->info) != BTF_KIND_FUNC)
> > + continue;
> > +
> > + str = btf__name_by_offset(btf, type->name_off);
> > + if (!str)
> > + break;
> > +
> > + if (!tfind(&str, &root, compare))
> > + continue;
> > +
> > + if (!btf_type_is_traceable_func(btf, type))
> > + continue;
> > +
> > + err = libbpf_ensure_mem((void **) &ids, &cap, sizeof(*ids), cnt + 1);
> > + if (err)
> > + goto cleanup;
> > +
> > + ids[cnt++] = type_id;
> > + }
>
> This filtering wasn't enough.
> I've added removal of duplicates here while applying:
>
> + /*
> + * Collect names that are not unique in kallsyms. The kernel resolves a
> + * tracing-multi BTF id to an address with kallsyms_lookup_name(), which
> + * returns the first symbol of that name. For a duplicate name that may
> + * be a different (non-ftrace-able) instance than the ftrace-able one in
> + * available_filter_functions, so attaching to it by BTF id fails with
> + * -ENOENT (e.g. t_start/t_next/t_stop). ksyms->syms is sorted by name,
> + * so equal names are adjacent.
> + */
> + for (i = 1; i < ksyms->sym_cnt; i++) {
> + if (strcmp(ksyms->syms[i].name, ksyms->syms[i - 1].name))
> + continue;
> + if (!tsearch(&ksyms->syms[i].name, &dups, compare)) {
> + ASSERT_FAIL("tsearch failed");
> + goto cleanup;
> + }
> + }
>
>
> + /* Skip names that are not unique in kallsyms, see above. */
> + if (tfind(&str, &dups, compare))
> + continue;
>
>
> As claude explains it:
> ----
> 1. The kernel attaches tracing_multi by BTF id. To get an address it resolves
> the BTF function name via kallsyms_lookup_name(tname) and requires
> ftrace_location(addr) — kernel/bpf/verifier.c:19380:
> addr = kallsyms_lookup_name(tname);
> ...
> if (!addr || !ftrace_location(addr))
> return -ENOENT;
> 2. t_start/t_next/t_stop each have 5 instances in this kernel. Only one is
> ftrace-able — the copies in kernel/trace/* are built notrace (ftrace's Makefile
> strips -pg), so only the unrelated copy is in available_filter_functions:
> 3. kallsyms_lookup_name() returns the lowest-address instance among equal names
> (exact strcmp, lowest seq). That instance has no fentry → ftrace_location()
> returns 0 → -ENOENT, which aborts the whole all-or-nothing bench attach.
>
> Why the bench includes them: it intersects BTF FUNC names with
> available_filter_functions names. Since some t_start is ftrace-able, the name
> passes the filter — but the kernel resolves the wrong (non-ftrace-able)
> t_start. The author's kernel apparently had the ftrace-able copy at the lowest
> address, so it passed there.
>
> This is a pre-existing limitation, not multi-specific: single fentry attach by
> BTF id uses the same kallsyms_lookup_name(tname) path (verifier.c:19120) — you
> can't reliably fentry-attach to any duplicate-named function on this kernel
> either.
> ----
strange I never triggered that.. but makes sense
>
> Maybe we should adjust bpf_get_ksyms() instead. Not sure.
the only other user is test_kprobe_multi_bench_attach which does
not care about this, so I think at this point keeping this in the
serial_test_tracing_multi_bench_attach is enough for now
thanks,
jirka
^ permalink raw reply
* Re: [PATCH mm-unstable v19 14/14] Documentation: mm: update the admin guide for mTHP collapse
From: Lance Yang @ 2026-06-08 7:41 UTC (permalink / raw)
To: npache
Cc: linux-doc, linux-kernel, linux-mm, linux-trace-kernel, aarcange,
akpm, anshuman.khandual, apopple, baohua, baolin.wang, byungchul,
catalin.marinas, cl, corbet, dave.hansen, david, dev.jain, gourry,
hannes, hughd, jack, jackmanb, jannh, jglisse, joshua.hahnjy, kas,
lance.yang, liam, ljs, mathieu.desnoyers, matthew.brost, mhiramat,
mhocko, peterx, pfalcato, rakie.kim, raquini, rdunlap,
richard.weiyang, rientjes, rostedt, rppt, ryan.roberts, shivankg,
sunnanyong, surenb, thomas.hellstrom, tiwai, usamaarif642, vbabka,
vishal.moola, wangkefeng.wang, will, willy, yang, ying.huang, ziy,
zokeefe, bagasdotme
In-Reply-To: <20260605161422.213817-15-npache@redhat.com>
On Fri, Jun 05, 2026 at 10:14:21AM -0600, Nico Pache wrote:
>Now that we can collapse to mTHPs lets update the admin guide to
>reflect these changes and provide proper guidance on how to utilize it.
>
>Reviewed-by: Lorenzo Stoakes <ljs@kernel.org>
>Reviewed-by: Bagas Sanjaya <bagasdotme@gmail.com>
>Signed-off-by: Nico Pache <npache@redhat.com>
>---
Reviewed-by: Lance Yang <lance.yang@linux.dev>
^ permalink raw reply
* Re: [PATCH mm-unstable v19 12/14] mm/khugepaged: avoid unnecessary mTHP collapse attempts
From: Lance Yang @ 2026-06-08 7:36 UTC (permalink / raw)
To: npache
Cc: linux-doc, linux-kernel, linux-mm, linux-trace-kernel, aarcange,
akpm, anshuman.khandual, apopple, baohua, baolin.wang, byungchul,
catalin.marinas, cl, corbet, dave.hansen, david, dev.jain, gourry,
hannes, hughd, jack, jackmanb, jannh, jglisse, joshua.hahnjy, kas,
lance.yang, liam, ljs, mathieu.desnoyers, matthew.brost, mhiramat,
mhocko, peterx, pfalcato, rakie.kim, raquini, rdunlap,
richard.weiyang, rientjes, rostedt, rppt, ryan.roberts, shivankg,
sunnanyong, surenb, thomas.hellstrom, tiwai, usamaarif642, vbabka,
vishal.moola, wangkefeng.wang, will, willy, yang, ying.huang, ziy,
zokeefe, usama.arif
In-Reply-To: <20260605161422.213817-13-npache@redhat.com>
On Fri, Jun 05, 2026 at 10:14:19AM -0600, Nico Pache wrote:
>There are cases where, if an attempted collapse fails, all subsequent
>orders are guaranteed to also fail. Avoid these collapse attempts by
>bailing out early.
>
>Reviewed-by: Lorenzo Stoakes <ljs@kernel.org>
>Acked-by: Usama Arif <usama.arif@linux.dev>
>Acked-by: David Hildenbrand (Arm) <david@kernel.org>
>Signed-off-by: Nico Pache <npache@redhat.com>
>---
Reviewed-by: Lance Yang <lance.yang@linux.dev>
^ permalink raw reply
* Re: [PATCH mm-unstable v19 10/14] mm/khugepaged: introduce collapse_possible_orders helper functions
From: Lance Yang @ 2026-06-08 7:27 UTC (permalink / raw)
To: npache
Cc: linux-doc, linux-kernel, linux-mm, linux-trace-kernel, aarcange,
akpm, anshuman.khandual, apopple, baohua, baolin.wang, byungchul,
catalin.marinas, cl, corbet, dave.hansen, david, dev.jain, gourry,
hannes, hughd, jack, jackmanb, jannh, jglisse, joshua.hahnjy, kas,
lance.yang, liam, ljs, mathieu.desnoyers, matthew.brost, mhiramat,
mhocko, peterx, pfalcato, rakie.kim, raquini, rdunlap,
richard.weiyang, rientjes, rostedt, rppt, ryan.roberts, shivankg,
sunnanyong, surenb, thomas.hellstrom, tiwai, usamaarif642, vbabka,
vishal.moola, wangkefeng.wang, will, willy, yang, ying.huang, ziy,
zokeefe
In-Reply-To: <20260605161422.213817-11-npache@redhat.com>
On Fri, Jun 05, 2026 at 10:14:17AM -0600, Nico Pache wrote:
>Add collapse_possible_orders() to generalize THP order eligibility. The
>function determines which THP orders are permitted based on collapse
>context (khugepaged vs madv_collapse). We also add collapse_possible()
>as a thin wrapper around collapse_possible_orders() that returns a bool
>rather than the whole bitmap.
>
>This consolidates collapse configuration logic and provides a clean
>interface for future mTHP collapse support where the orders may be
>different.
>
>Acked-by: David Hildenbrand (Arm) <david@kernel.org>
>Reviewed-by: Baolin Wang <baolin.wang@linux.alibaba.com>
>Signed-off-by: Nico Pache <npache@redhat.com>
>---
Reviewed-by: Lance Yang <lance.yang@linux.dev>
^ permalink raw reply
* Re: [PATCH mm-unstable v19 09/14] mm/khugepaged: improve tracepoints for mTHP orders
From: Lance Yang @ 2026-06-08 7:19 UTC (permalink / raw)
To: npache
Cc: linux-doc, linux-kernel, linux-mm, linux-trace-kernel, aarcange,
akpm, anshuman.khandual, apopple, baohua, baolin.wang, byungchul,
catalin.marinas, cl, corbet, dave.hansen, david, dev.jain, gourry,
hannes, hughd, jack, jackmanb, jannh, jglisse, joshua.hahnjy, kas,
lance.yang, liam, ljs, mathieu.desnoyers, matthew.brost, mhiramat,
mhocko, peterx, pfalcato, rakie.kim, raquini, rdunlap,
richard.weiyang, rientjes, rostedt, rppt, ryan.roberts, shivankg,
sunnanyong, surenb, thomas.hellstrom, tiwai, usamaarif642, vbabka,
vishal.moola, wangkefeng.wang, will, willy, yang, ying.huang, ziy,
zokeefe
In-Reply-To: <20260605161422.213817-10-npache@redhat.com>
On Fri, Jun 05, 2026 at 10:14:16AM -0600, Nico Pache wrote:
>Add the order to the mm_collapse_huge_page<_swapin,_isolate> tracepoints to
>give better insight into what order is being operated at for.
>
>Reviewed-by: Lorenzo Stoakes <ljs@kernel.org>
>Reviewed-by: Baolin Wang <baolin.wang@linux.alibaba.com>
>Acked-by: David Hildenbrand (Arm) <david@kernel.org>
>Signed-off-by: Nico Pache <npache@redhat.com>
>---
Reviewed-by: Lance Yang <lance.yang@linux.dev>
^ permalink raw reply
* Re: [PATCH mm-unstable v19 08/14] mm/khugepaged: add per-order mTHP collapse failure statistics
From: Lance Yang @ 2026-06-08 7:13 UTC (permalink / raw)
To: npache
Cc: linux-doc, linux-kernel, linux-mm, linux-trace-kernel, aarcange,
akpm, anshuman.khandual, apopple, baohua, baolin.wang, byungchul,
catalin.marinas, cl, corbet, dave.hansen, david, dev.jain, gourry,
hannes, hughd, jack, jackmanb, jannh, jglisse, joshua.hahnjy, kas,
lance.yang, liam, ljs, mathieu.desnoyers, matthew.brost, mhiramat,
mhocko, peterx, pfalcato, rakie.kim, raquini, rdunlap,
richard.weiyang, rientjes, rostedt, rppt, ryan.roberts, shivankg,
sunnanyong, surenb, thomas.hellstrom, tiwai, usamaarif642, vbabka,
vishal.moola, wangkefeng.wang, will, willy, yang, ying.huang, ziy,
zokeefe
In-Reply-To: <20260605161422.213817-9-npache@redhat.com>
On Fri, Jun 05, 2026 at 10:14:15AM -0600, Nico Pache wrote:
>Add three new mTHP statistics to track collapse failures for different
>orders when encountering swap PTEs, excessive none PTEs, and shared PTEs:
>
>- collapse_exceed_swap_pte: Increment when mTHP collapse fails due to
> encountering a swap PTE.
>
>- collapse_exceed_none_pte: Counts when mTHP collapse fails due to
> exceeding the none PTE threshold for the given order
>
>- collapse_exceed_shared_pte: Counts when mTHP collapse fails due to
> encountering a shared PTE.
>
>These statistics complement the existing THP_SCAN_EXCEED_* events by
>providing per-order granularity for mTHP collapse attempts. The stats are
>exposed via sysfs under
>`/sys/kernel/mm/transparent_hugepage/hugepages-*/stats/` for each
>supported hugepage size.
>
>As we currently do not support collapsing mTHPs that contain a swap or
>shared entry, those statistics keep track of how often we are
>encountering failed mTHP collapses due to these restrictions.
>
>We will add support for mTHP collapse for anonymous pages next; lets also
>track when this happens at the PMD level within the per-mTHP stats.
>
>Reviewed-by: Lorenzo Stoakes <ljs@kernel.org>
>Acked-by: David Hildenbrand (Arm) <david@kernel.org>
>Signed-off-by: Nico Pache <npache@redhat.com>
>---
Reviewed-by: Lance Yang <lance.yang@linux.dev>
^ permalink raw reply
* Re: [PATCH mm-unstable v19 07/14] mm/khugepaged: skip collapsing mTHP to smaller orders
From: Lance Yang @ 2026-06-08 6:59 UTC (permalink / raw)
To: npache
Cc: linux-doc, linux-kernel, linux-mm, linux-trace-kernel, aarcange,
akpm, anshuman.khandual, apopple, baohua, baolin.wang, byungchul,
catalin.marinas, cl, corbet, dave.hansen, david, dev.jain, gourry,
hannes, hughd, jack, jackmanb, jannh, jglisse, joshua.hahnjy, kas,
lance.yang, liam, ljs, mathieu.desnoyers, matthew.brost, mhiramat,
mhocko, peterx, pfalcato, rakie.kim, raquini, rdunlap,
richard.weiyang, rientjes, rostedt, rppt, ryan.roberts, shivankg,
sunnanyong, surenb, thomas.hellstrom, tiwai, usamaarif642, vbabka,
vishal.moola, wangkefeng.wang, will, willy, yang, ying.huang, ziy,
zokeefe, usama.arif
In-Reply-To: <20260605161422.213817-8-npache@redhat.com>
On Fri, Jun 05, 2026 at 10:14:14AM -0600, Nico Pache wrote:
>khugepaged may try to collapse a mTHP to a folio of equal or smaller size,
>possibly resulting in a partially mapped source folio, which is undesired.
>Skip these cases until we have a way to check if its ok to collapse to a
>smaller mTHP size (like in the case of a partially mapped folio). This
>check is not done during the scan phase as the current collapse order is
>unknown at that time.
>
>This patch is inspired by Dev Jain's work on khugepaged mTHP support [1].
>
>[1] https://lore.kernel.org/lkml/20241216165105.56185-11-dev.jain@arm.com/
>
>Reviewed-by: Lorenzo Stoakes <ljs@kernel.org>
>Reviewed-by: Baolin Wang <baolin.wang@linux.alibaba.com>
>Acked-by: David Hildenbrand (arm) <david@kernel.org>
>Acked-by: Usama Arif <usama.arif@linux.dev>
>Co-developed-by: Dev Jain <dev.jain@arm.com>
>Signed-off-by: Dev Jain <dev.jain@arm.com>
>Signed-off-by: Nico Pache <npache@redhat.com>
>---
> mm/khugepaged.c | 8 ++++++++
> 1 file changed, 8 insertions(+)
>
>diff --git a/mm/khugepaged.c b/mm/khugepaged.c
>index c2769d82a719..191e529c185c 100644
>--- a/mm/khugepaged.c
>+++ b/mm/khugepaged.c
>@@ -697,6 +697,14 @@ static enum scan_result __collapse_huge_page_isolate(struct vm_area_struct *vma,
> goto out;
> }
> }
>+ /*
>+ * TODO: In some cases of partially-mapped folios, we'd actually
>+ * want to collapse.
>+ */
Partially mapped folios can be handled later :)
Reviewed-by: Lance Yang <lance.yang@linux.dev>
>+ if (!is_pmd_order(order) && folio_order(folio) >= order) {
>+ result = SCAN_PTE_MAPPED_HUGEPAGE;
>+ goto out;
>+ }
>
> if (folio_test_large(folio)) {
> struct folio *f;
>--
>2.54.0
>
>
^ permalink raw reply
* Re: [PATCH mm-unstable v19 06/14] mm/khugepaged: generalize collapse_huge_page for mTHP collapse
From: Lance Yang @ 2026-06-08 4:54 UTC (permalink / raw)
To: npache
Cc: linux-doc, linux-kernel, linux-mm, linux-trace-kernel, aarcange,
akpm, anshuman.khandual, apopple, baohua, baolin.wang, byungchul,
catalin.marinas, cl, corbet, dave.hansen, david, dev.jain, gourry,
hannes, hughd, jack, jackmanb, jannh, jglisse, joshua.hahnjy, kas,
lance.yang, liam, ljs, mathieu.desnoyers, matthew.brost, mhiramat,
mhocko, peterx, pfalcato, rakie.kim, raquini, rdunlap,
richard.weiyang, rientjes, rostedt, rppt, ryan.roberts, shivankg,
sunnanyong, surenb, thomas.hellstrom, tiwai, usamaarif642, vbabka,
vishal.moola, wangkefeng.wang, will, willy, yang, ying.huang, ziy,
zokeefe
In-Reply-To: <20260605161422.213817-7-npache@redhat.com>
On Fri, Jun 05, 2026 at 10:14:13AM -0600, Nico Pache wrote:
>Pass an order to collapse_huge_page to support collapsing anon memory to
>arbitrary orders within a PMD. order indicates what mTHP size we are
>attempting to collapse to.
>
>For non-PMD collapse we must leave the anon VMA write locked until after
>we collapse the mTHP-- in the PMD case all the pages are isolated, but in
>the mTHP case this is not true, and we must keep the lock to prevent
>access/changes to the page tables. This can happen if the rmap walkers hit
>a pmd_none while the PMD entry is currently unavailable due to being
>temporarily removed during the collapse phase.
>
>To properly establish the page table hierarchy without violating any
>expectations from certain architectures (e.g. MIPS), we must make sure to
>have the PMD reinstalled before the PTEs, and hold both PTE/PMD locks
>before calling update_mmu_cache_range() (if they are distinct locks).
>
>Signed-off-by: Nico Pache <npache@redhat.com>
>---
Nothing else jumped out at me. Anything left can be sorted out later, as
David and Lorenzo said :)
Reviewed-by: Lance Yang <lance.yang@linux.dev>
^ permalink raw reply
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