* Re: [PATCH 14/26] rv/rvgen: remove redundant initial_state removal
From: Gabriele Monaco @ 2026-01-20 8:01 UTC (permalink / raw)
To: Wander Lairson Costa
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <20260119205601.105821-15-wander@redhat.com>
On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> Remove an unnecessary and incorrect list removal operation in the
> automata state variable processing. The code attempted to remove
> initial_state from the states list, but this element was never
> added to the list in the first place. States with the __init_
> prefix are explicitly excluded from the states list during the
> parsing loop, with only the initial_state variable being set
> from them.
The initial state is not the state with __init_, but the state pointed to by
that, the purpose of removing it after sorting and putting it back is for it to
be the first (we may argue there are better ways to do that, but it works).
After this change, the initial state is duplicated..
I think we should just drop this.
Thanks,
Gabriele
>
> Calling remove() on an element that does not exist in a list
> raises a ValueError. This code would have failed during execution
> when processing any DOT file containing an initial state marker.
> The subsequent insert operation at index 0 correctly adds the
> initial_state to the beginning of the states list, making the
> removal operation both incorrect and redundant.
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> ---
> tools/verification/rvgen/rvgen/automata.py | 1 -
> 1 file changed, 1 deletion(-)
>
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 7841a6e70bad2..b302af3e5133e 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -111,7 +111,6 @@ class Automata:
> cursor += 1
>
> states = sorted(set(states))
> - states.remove(initial_state)
>
> # Insert the initial state at the beginning of the states
> states.insert(0, initial_state)
^ permalink raw reply
* Re: [PATCH 15/26] rv/rvgen: use class constant for init marker
From: Gabriele Monaco @ 2026-01-20 8:06 UTC (permalink / raw)
To: Wander Lairson Costa
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <20260119205601.105821-16-wander@redhat.com>
On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> Replace hardcoded string literal and magic number with a class
> constant for the initial state marker in DOT file parsing. The
> previous implementation used the magic string "__init_" directly
> in the code along with a hardcoded length of 7 for substring
> extraction, which made the code less maintainable and harder to
> understand.
>
> This change introduces a class constant init_marker to serve as
> a single source of truth for the initial state prefix. The code
> now uses startswith() for clearer intent and calculates the
> substring position dynamically using len(), eliminating the magic
> number. If the marker value needs to change in the future, only
> the constant definition requires updating rather than multiple
> locations in the code.
>
> The refactoring improves code readability and maintainability
> while preserving the exact same runtime behavior.
>
Looks good, thanks.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> ---
> tools/verification/rvgen/rvgen/automata.py | 5 +++--
> 1 file changed, 3 insertions(+), 2 deletions(-)
>
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index b302af3e5133e..8548265955570 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -25,6 +25,7 @@ class Automata:
> """
>
> invalid_state_str = "INVALID_STATE"
> + init_marker = "__init_"
>
> def __init__(self, file_path, model_name=None):
> self.__dot_path = file_path
> @@ -96,8 +97,8 @@ class Automata:
>
> # "enabled_fired"}; -> enabled_fired
> state = raw_state.replace('"', '').replace('};', '').replace(',',
> '_')
> - if state[0:7] == "__init_":
> - initial_state = state[7:]
> + if state.startswith(self.init_marker):
> + initial_state = state[len(self.init_marker):]
> else:
> states.append(state)
> if "doublecircle" in self.__dot_lines[cursor]:
^ permalink raw reply
* Re: [PATCH bpf RESEND v2 2/2] bpf: Require ARG_PTR_TO_MEM with memory flag
From: Zesen Liu @ 2026-01-20 8:11 UTC (permalink / raw)
To: Eduard Zingerman
Cc: Alexei Starovoitov, Daniel Borkmann, Andrii Nakryiko,
Martin KaFai Lau, Song Liu, Yonghong Song, John Fastabend,
KP Singh, Stanislav Fomichev, Hao Luo, Jiri Olsa, Matt Bobrowski,
Steven Rostedt, Masami Hiramatsu, Mathieu Desnoyers,
David S. Miller, Eric Dumazet, Jakub Kicinski, Paolo Abeni,
Simon Horman, Daniel Xu, bpf, linux-kernel, linux-trace-kernel,
netdev, Shuran Liu, Peili Gao, Haoran Ni
In-Reply-To: <600177c05c552f470cc5e25c7dba6990d96790e9.camel@gmail.com>
[...]
> On Jan 20, 2026, at 04:25, Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> Note: this patch no longer applies properly because of the change in
> the check_func_proto() signature.
Thanks for pointing this out. I will rebase to bpf-next in v3 to
address the check_func_proto() signature changes.
^ permalink raw reply
* Re: [PATCH v4 2/4] tracing: Make the backup instance non-reusable
From: kernel test robot @ 2026-01-20 8:17 UTC (permalink / raw)
To: Masami Hiramatsu (Google), Steven Rostedt
Cc: oe-kbuild-all, Masami Hiramatsu, Mathieu Desnoyers, linux-kernel,
linux-trace-kernel
In-Reply-To: <176887137556.578403.17994205756247311821.stgit@mhiramat.tok.corp.google.com>
Hi Masami,
kernel test robot noticed the following build warnings:
[auto build test WARNING on trace/for-next]
[also build test WARNING on linus/master v6.19-rc6 next-20260119]
[If your patch is applied to the wrong git tree, kindly drop us a note.
And when submitting patch, we suggest to use '--base' as documented in
https://git-scm.com/docs/git-format-patch#_base_tree_information]
url: https://github.com/intel-lab-lkp/linux/commits/Masami-Hiramatsu-Google/tracing-Reset-last_boot_info-if-ring-buffer-is-reset/20260120-091429
base: https://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace for-next
patch link: https://lore.kernel.org/r/176887137556.578403.17994205756247311821.stgit%40mhiramat.tok.corp.google.com
patch subject: [PATCH v4 2/4] tracing: Make the backup instance non-reusable
config: arc-defconfig (https://download.01.org/0day-ci/archive/20260120/202601201531.ng4kqZhn-lkp@intel.com/config)
compiler: arc-linux-gcc (GCC) 15.2.0
reproduce (this is a W=1 build): (https://download.01.org/0day-ci/archive/20260120/202601201531.ng4kqZhn-lkp@intel.com/reproduce)
If you fix the issue in a separate patch/commit (i.e. not just a new version of
the same patch/commit), kindly add following tags
| Reported-by: kernel test robot <lkp@intel.com>
| Closes: https://lore.kernel.org/oe-kbuild-all/202601201531.ng4kqZhn-lkp@intel.com/
All warnings (new ones prefixed by >>):
kernel/trace/trace.c: In function 'tracing_init_tracefs_percpu':
>> kernel/trace/trace.c:9398:17: warning: variable 'writable_mode' set but not used [-Wunused-but-set-variable]
9398 | umode_t writable_mode = TRACE_MODE_WRITE;
| ^~~~~~~~~~~~~
vim +/writable_mode +9398 kernel/trace/trace.c
9393
9394 static void
9395 tracing_init_tracefs_percpu(struct trace_array *tr, long cpu)
9396 {
9397 struct dentry *d_percpu = tracing_dentry_percpu(tr, cpu);
> 9398 umode_t writable_mode = TRACE_MODE_WRITE;
9399 struct dentry *d_cpu;
9400 char cpu_dir[30]; /* 30 characters should be more than enough */
9401
9402 if (!d_percpu)
9403 return;
9404
9405 if (trace_array_is_readonly(tr))
9406 writable_mode = TRACE_MODE_READ;
9407
9408 snprintf(cpu_dir, 30, "cpu%ld", cpu);
9409 d_cpu = tracefs_create_dir(cpu_dir, d_percpu);
9410 if (!d_cpu) {
9411 pr_warn("Could not create tracefs '%s' entry\n", cpu_dir);
9412 return;
9413 }
9414
9415 /* per cpu trace_pipe */
9416 trace_create_cpu_file("trace_pipe", TRACE_MODE_READ, d_cpu,
9417 tr, cpu, &tracing_pipe_fops);
9418
9419 /* per cpu trace */
9420 trace_create_cpu_file("trace", TRACE_MODE_WRITE, d_cpu,
9421 tr, cpu, &tracing_fops);
9422
9423 trace_create_cpu_file("trace_pipe_raw", TRACE_MODE_READ, d_cpu,
9424 tr, cpu, &tracing_buffers_fops);
9425
9426 trace_create_cpu_file("stats", TRACE_MODE_READ, d_cpu,
9427 tr, cpu, &tracing_stats_fops);
9428
9429 trace_create_cpu_file("buffer_size_kb", TRACE_MODE_READ, d_cpu,
9430 tr, cpu, &tracing_entries_fops);
9431
9432 if (tr->range_addr_start)
9433 trace_create_cpu_file("buffer_meta", TRACE_MODE_READ, d_cpu,
9434 tr, cpu, &tracing_buffer_meta_fops);
9435 #ifdef CONFIG_TRACER_SNAPSHOT
9436 if (!tr->range_addr_start) {
9437 trace_create_cpu_file("snapshot", TRACE_MODE_WRITE, d_cpu,
9438 tr, cpu, &snapshot_fops);
9439
9440 trace_create_cpu_file("snapshot_raw", TRACE_MODE_READ, d_cpu,
9441 tr, cpu, &snapshot_raw_fops);
9442 }
9443 #endif
9444 }
9445
--
0-DAY CI Kernel Test Service
https://github.com/intel/lkp-tests/wiki
^ permalink raw reply
* Re: [PATCH bpf-next v3 1/2] bpf: support bpf_get_func_arg() for BPF_TRACE_RAW_TP
From: Jiri Olsa @ 2026-01-20 8:18 UTC (permalink / raw)
To: Menglong Dong
Cc: Menglong Dong, Jiri Olsa, andrii, ast, daniel, john.fastabend,
martin.lau, eddyz87, song, yonghong.song, kpsingh, sdf, haoluo,
mattbobrowski, rostedt, mhiramat, mathieu.desnoyers, bpf,
linux-kernel, linux-trace-kernel
In-Reply-To: <6099572.DvuYhMxLoT@7950hx>
On Tue, Jan 20, 2026 at 09:24:46AM +0800, Menglong Dong wrote:
> On 2026/1/20 07:37, Jiri Olsa wrote:
> > On Mon, Jan 19, 2026 at 10:37:31AM +0800, Menglong Dong wrote:
> > > For now, bpf_get_func_arg() and bpf_get_func_arg_cnt() is not supported by
> > > the BPF_TRACE_RAW_TP, which is not convenient to get the argument of the
> > > tracepoint, especially for the case that the position of the arguments in
> > > a tracepoint can change.
> > >
> > > The target tracepoint BTF type id is specified during loading time,
> > > therefore we can get the function argument count from the function
> > > prototype instead of the stack.
> > >
> > > Signed-off-by: Menglong Dong <dongml2@chinatelecom.cn>
> > > ---
> > > v3:
> > > - remove unnecessary NULL checking for prog->aux->attach_func_proto
> > >
> > > v2:
> > > - for nr_args, skip first 'void *__data' argument in btf_trace_##name
> > > typedef
> > > ---
> > > kernel/bpf/verifier.c | 32 ++++++++++++++++++++++++++++----
> > > kernel/trace/bpf_trace.c | 4 ++--
> > > 2 files changed, 30 insertions(+), 6 deletions(-)
> > >
> > > diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> > > index faa1ecc1fe9d..4f52342573f0 100644
> > > --- a/kernel/bpf/verifier.c
> > > +++ b/kernel/bpf/verifier.c
> > > @@ -23316,8 +23316,20 @@ static int do_misc_fixups(struct bpf_verifier_env *env)
> > > /* Implement bpf_get_func_arg inline. */
> > > if (prog_type == BPF_PROG_TYPE_TRACING &&
> > > insn->imm == BPF_FUNC_get_func_arg) {
> > > - /* Load nr_args from ctx - 8 */
> > > - insn_buf[0] = BPF_LDX_MEM(BPF_DW, BPF_REG_0, BPF_REG_1, -8);
> > > + if (eatype == BPF_TRACE_RAW_TP) {
> > > + int nr_args = btf_type_vlen(prog->aux->attach_func_proto);
> > > +
> > > + /*
> > > + * skip first 'void *__data' argument in btf_trace_##name
> > > + * typedef
> > > + */
> > > + nr_args--;
> > > + /* Save nr_args to reg0 */
> > > + insn_buf[0] = BPF_MOV64_IMM(BPF_REG_0, nr_args);
> > > + } else {
> > > + /* Load nr_args from ctx - 8 */
> > > + insn_buf[0] = BPF_LDX_MEM(BPF_DW, BPF_REG_0, BPF_REG_1, -8);
> > > + }
> > > insn_buf[1] = BPF_JMP32_REG(BPF_JGE, BPF_REG_2, BPF_REG_0, 6);
> > > insn_buf[2] = BPF_ALU64_IMM(BPF_LSH, BPF_REG_2, 3);
> > > insn_buf[3] = BPF_ALU64_REG(BPF_ADD, BPF_REG_2, BPF_REG_1);
> > > @@ -23369,8 +23381,20 @@ static int do_misc_fixups(struct bpf_verifier_env *env)
> > > /* Implement get_func_arg_cnt inline. */
> > > if (prog_type == BPF_PROG_TYPE_TRACING &&
> > > insn->imm == BPF_FUNC_get_func_arg_cnt) {
> > > - /* Load nr_args from ctx - 8 */
> > > - insn_buf[0] = BPF_LDX_MEM(BPF_DW, BPF_REG_0, BPF_REG_1, -8);
> > > + if (eatype == BPF_TRACE_RAW_TP) {
> > > + int nr_args = btf_type_vlen(prog->aux->attach_func_proto);
> > > +
> > > + /*
> > > + * skip first 'void *__data' argument in btf_trace_##name
> > > + * typedef
> > > + */
> > > + nr_args--;
> > > + /* Save nr_args to reg0 */
> >
> > I think we can attach single bpf program to multiple rawtp tracepoints,
> > in which case this would not work properly for such program links on
> > tracepoints with different nr_args, right?
>
> Hi, Jiri. As for now, I think we can't do that when I look into
> bpf_raw_tp_link_attach(). For the BPF_TRACE_RAW_TP, we specify
> a target btf type id when loading the bpf prog. And during
> attaching, it seems that we can only attach to that target, which
> means that we can't attach to multiple rawtp tracepoint. And
> we can't change the target btf id when reattach, too. Right?
>
> Part of the implement of bpf_raw_tp_link_attach():
>
> static int bpf_raw_tp_link_attach(struct bpf_prog *prog,
> const char __user *user_tp_name, u64 cookie,
> enum bpf_attach_type attach_type)
> {
> struct bpf_link_primer link_primer;
> struct bpf_raw_tp_link *link;
> struct bpf_raw_event_map *btp;
> const char *tp_name;
> char buf[128];
> int err;
>
> switch (prog->type) {
> case BPF_PROG_TYPE_TRACING:
> case BPF_PROG_TYPE_EXT:
> case BPF_PROG_TYPE_LSM:
> if (user_tp_name)
> /* The attach point for this category of programs
> * should be specified via btf_id during program load.
> */
ah there's the name check, ok.. got confused by the max_ctx_offset
check in bpf_probe_register
thanks,
jirka
> return -EINVAL;
> if (prog->type == BPF_PROG_TYPE_TRACING &&
> prog->expected_attach_type == BPF_TRACE_RAW_TP) {
> tp_name = prog->aux->attach_func_name;
> break;
> }
> [......]
> }
> [......]
> }
>
> Thanks!
> Menglong Dong
>
> >
> > jirka
> >
> >
> > > + insn_buf[0] = BPF_MOV64_IMM(BPF_REG_0, nr_args);
> > > + } else {
> > > + /* Load nr_args from ctx - 8 */
> > > + insn_buf[0] = BPF_LDX_MEM(BPF_DW, BPF_REG_0, BPF_REG_1, -8);
> > > + }
> > >
> > > new_prog = bpf_patch_insn_data(env, i + delta, insn_buf, 1);
> > > if (!new_prog)
> > > diff --git a/kernel/trace/bpf_trace.c b/kernel/trace/bpf_trace.c
> > > index 6e076485bf70..9b1b56851d26 100644
> > > --- a/kernel/trace/bpf_trace.c
> > > +++ b/kernel/trace/bpf_trace.c
> > > @@ -1734,11 +1734,11 @@ tracing_prog_func_proto(enum bpf_func_id func_id, const struct bpf_prog *prog)
> > > case BPF_FUNC_d_path:
> > > return &bpf_d_path_proto;
> > > case BPF_FUNC_get_func_arg:
> > > - return bpf_prog_has_trampoline(prog) ? &bpf_get_func_arg_proto : NULL;
> > > + return &bpf_get_func_arg_proto;
> > > case BPF_FUNC_get_func_ret:
> > > return bpf_prog_has_trampoline(prog) ? &bpf_get_func_ret_proto : NULL;
> > > case BPF_FUNC_get_func_arg_cnt:
> > > - return bpf_prog_has_trampoline(prog) ? &bpf_get_func_arg_cnt_proto : NULL;
> > > + return &bpf_get_func_arg_cnt_proto;
> > > case BPF_FUNC_get_attach_cookie:
> > > if (prog->type == BPF_PROG_TYPE_TRACING &&
> > > prog->expected_attach_type == BPF_TRACE_RAW_TP)
> >
> >
>
>
>
>
^ permalink raw reply
* Re: [PATCH 16/26] rv/rvgen: fix unbound initial_state variable
From: Gabriele Monaco @ 2026-01-20 8:21 UTC (permalink / raw)
To: Wander Lairson Costa
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <20260119205601.105821-17-wander@redhat.com>
On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
[...]
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 8548265955570..083d0f5cfb773 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -10,6 +10,7 @@
>
> import ntpath
>
> +
> class AutomataError(OSError):
> """Exception raised for errors in automata parsing and validation.
>
> @@ -17,6 +18,7 @@ class AutomataError(OSError):
> or malformed automaton definitions.
> """
>
> +
I believe these newlines were added automatically by some tools, not sure if we
really want them but they don't belong in this patch (since 1/26 added this
class).
> class Automata:
> """Automata class: Reads a dot file and parses it as an automata.
>
> @@ -31,7 +33,9 @@ class Automata:
> self.__dot_path = file_path
> self.name = model_name or self.__get_model_name()
> self.__dot_lines = self.__open_dot()
> - self.states, self.initial_state, self.final_states =
> self.__get_state_variables()
> + self.states, self.initial_state, self.final_states = (
> + self.__get_state_variables()
> + )
There is no strict 80 character limit for python code and I personally find this
less readable. Is this again what the tool suggested?
> self.events = self.__get_event_variables()
> self.function = self.__create_matrix()
> self.events_start, self.events_start_run = self.__store_init_events()
> @@ -86,6 +90,7 @@ class Automata:
> # wait for node declaration
> states = []
> final_states = []
> + initial_state = None
>
> has_final_states = False
> cursor = self.__get_cursor_begin_states()
> @@ -96,9 +101,9 @@ class Automata:
> raw_state = line[-1]
>
> # "enabled_fired"}; -> enabled_fired
> - state = raw_state.replace('"', '').replace('};', '').replace(',',
> '_')
> + state = raw_state.replace('"', "").replace("};", "").replace(",",
> "_")
Ok this change is good.
> if state.startswith(self.init_marker):
> - initial_state = state[len(self.init_marker):]
> + initial_state = state[len(self.init_marker) :]
You fixed spacing in 12/26. We could either keep move this change there or just
merge that patch with others touching the same files.
> else:
> states.append(state)
> if "doublecircle" in self.__dot_lines[cursor]:
> @@ -111,6 +116,9 @@ class Automata:
>
> cursor += 1
>
> + if initial_state is None:
> + raise AutomataError("The automaton doesn't have a initial state")
> +
Yeah that's needed.
> states = sorted(set(states))
>
> # Insert the initial state at the beginning of the states
> @@ -132,7 +140,7 @@ class Automata:
> # ------------ event is here ------------^^^^^
> if self.__dot_lines[cursor].split()[1] == "->":
> line = self.__dot_lines[cursor].split()
> - event = line[-2].replace('"', '')
> + event = line[-2].replace('"', "")
>
> # when a transition has more than one labels, they are like
> this
> # "local_irq_enable\nhw_local_irq_enable_n"
> @@ -162,7 +170,9 @@ class Automata:
> nr_state += 1
>
> # declare the matrix....
> - matrix = [[self.invalid_state_str for x in range(nr_event)] for y in
> range(nr_state)]
> + matrix = [
> + [self.invalid_state_str for x in range(nr_event)] for y in
> range(nr_state)
> + ]
>
> # and we are back! Let's fill the matrix
> cursor = self.__get_cursor_begin_events()
> @@ -170,9 +180,9 @@ class Automata:
> while self.__dot_lines[cursor].lstrip()[0] == '"':
> if self.__dot_lines[cursor].split()[1] == "->":
> line = self.__dot_lines[cursor].split()
> - origin_state = line[0].replace('"', '').replace(',', '_')
> - dest_state = line[2].replace('"', '').replace(',', '_')
> - possible_events = line[-2].replace('"', '').replace("\\n", "
> ")
> + origin_state = line[0].replace('"', "").replace(",", "_")
> + dest_state = line[2].replace('"', "").replace(",", "_")
> + possible_events = line[-2].replace('"', "").replace("\\n", "
> ")
All in all looks good, thanks.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> for event in possible_events.split():
> matrix[states_dict[origin_state]][events_dict[event]] =
> dest_state
> cursor += 1
^ permalink raw reply
* [PATCH bpf-next v3 0/2] bpf: Fix memory access flags in helper prototypes
From: Zesen Liu @ 2026-01-20 8:28 UTC (permalink / raw)
To: Alexei Starovoitov, Daniel Borkmann, Andrii Nakryiko,
Martin KaFai Lau, Eduard Zingerman, Song Liu, Yonghong Song,
John Fastabend, KP Singh, Stanislav Fomichev, Hao Luo, Jiri Olsa,
Matt Bobrowski, Steven Rostedt, Masami Hiramatsu,
Mathieu Desnoyers, David S. Miller, Eric Dumazet, Jakub Kicinski,
Paolo Abeni, Simon Horman, Daniel Xu
Cc: bpf, linux-kernel, linux-trace-kernel, netdev, Shuran Liu,
Peili Gao, Haoran Ni, Zesen Liu
Hi,
This series adds missing memory access flags (MEM_RDONLY or MEM_WRITE) to
several bpf helper function prototypes that use ARG_PTR_TO_MEM but lack the
correct flag. It also adds a new check in verifier to ensure the flag is
specified.
Missing memory access flags in helper prototypes can lead to critical
correctness issues when the verifier tries to perform code optimization.
After commit 37cce22dbd51 ("bpf: verifier: Refactor helper access type
tracking"), the verifier relies on the memory access flags, rather than
treating all arguments in helper functions as potentially modifying the
pointed-to memory.
Using ARG_PTR_TO_MEM alone without flags does not make sense because:
- If the helper does not change the argument, missing MEM_RDONLY causes the
verifier to incorrectly reject a read-only buffer.
- If the helper does change the argument, missing MEM_WRITE causes the
verifier to incorrectly assume the memory is unchanged, leading to
errors in code optimization.
We have already seen several reports regarding this:
- commit ac44dcc788b9 ("bpf: Fix verifier assumptions of bpf_d_path's
output buffer") adds MEM_WRITE to bpf_d_path;
- commit 2eb7648558a7 ("bpf: Specify access type of bpf_sysctl_get_name
args") adds MEM_WRITE to bpf_sysctl_get_name.
This series looks through all prototypes in the kernel and completes the
flags. It also adds check_mem_arg_rw_flag_ok() and wires it into
check_func_proto() to statically restrict ARG_PTR_TO_MEM from appearing
without memory access flags.
Changelog
=========
v3:
- Rebased to bpf-next to address check_func_proto() signature changes, as
suggested by Eduard Zingerman.
v2:
- Add missing MEM_RDONLY flags to protos with ARG_PTR_TO_FIXED_SIZE_MEM.
Thanks,
Zesen Liu
---
Zesen Liu (2):
bpf: Fix memory access flags in helper prototypes
bpf: Require ARG_PTR_TO_MEM with memory flag
kernel/bpf/helpers.c | 2 +-
kernel/bpf/syscall.c | 2 +-
kernel/bpf/verifier.c | 17 +++++++++++++++++
kernel/trace/bpf_trace.c | 6 +++---
net/core/filter.c | 20 ++++++++++----------
5 files changed, 32 insertions(+), 15 deletions(-)
---
base-commit: efad162f5a840ae178e7761c176c49f433c7bb68
change-id: 20251220-helper_proto-fb6e64182467
Best regards,
--
Zesen Liu <ftyghome@gmail.com>
^ permalink raw reply
* [PATCH bpf-next v3 1/2] bpf: Fix memory access flags in helper prototypes
From: Zesen Liu @ 2026-01-20 8:28 UTC (permalink / raw)
To: Alexei Starovoitov, Daniel Borkmann, Andrii Nakryiko,
Martin KaFai Lau, Eduard Zingerman, Song Liu, Yonghong Song,
John Fastabend, KP Singh, Stanislav Fomichev, Hao Luo, Jiri Olsa,
Matt Bobrowski, Steven Rostedt, Masami Hiramatsu,
Mathieu Desnoyers, David S. Miller, Eric Dumazet, Jakub Kicinski,
Paolo Abeni, Simon Horman, Daniel Xu
Cc: bpf, linux-kernel, linux-trace-kernel, netdev, Shuran Liu,
Peili Gao, Haoran Ni, Zesen Liu
In-Reply-To: <20260120-helper_proto-v3-0-27b0180b4e77@gmail.com>
After commit 37cce22dbd51 ("bpf: verifier: Refactor helper access type tracking"),
the verifier started relying on the access type flags in helper
function prototypes to perform memory access optimizations.
Currently, several helper functions utilizing ARG_PTR_TO_MEM lack the
corresponding MEM_RDONLY or MEM_WRITE flags. This omission causes the
verifier to incorrectly assume that the buffer contents are unchanged
across the helper call. Consequently, the verifier may optimize away
subsequent reads based on this wrong assumption, leading to correctness
issues.
For bpf_get_stack_proto_raw_tp, the original MEM_RDONLY was incorrect
since the helper writes to the buffer. Change it to ARG_PTR_TO_UNINIT_MEM
which correctly indicates write access to potentially uninitialized memory.
Similar issues were recently addressed for specific helpers in commit
ac44dcc788b9 ("bpf: Fix verifier assumptions of bpf_d_path's output buffer")
and commit 2eb7648558a7 ("bpf: Specify access type of bpf_sysctl_get_name args").
Fix these prototypes by adding the correct memory access flags.
Fixes: 37cce22dbd51 ("bpf: verifier: Refactor helper access type tracking")
Co-developed-by: Shuran Liu <electronlsr@gmail.com>
Signed-off-by: Shuran Liu <electronlsr@gmail.com>
Co-developed-by: Peili Gao <gplhust955@gmail.com>
Signed-off-by: Peili Gao <gplhust955@gmail.com>
Co-developed-by: Haoran Ni <haoran.ni.cs@gmail.com>
Signed-off-by: Haoran Ni <haoran.ni.cs@gmail.com>
Signed-off-by: Zesen Liu <ftyghome@gmail.com>
---
kernel/bpf/helpers.c | 2 +-
kernel/bpf/syscall.c | 2 +-
kernel/trace/bpf_trace.c | 6 +++---
net/core/filter.c | 20 ++++++++++----------
4 files changed, 15 insertions(+), 15 deletions(-)
diff --git a/kernel/bpf/helpers.c b/kernel/bpf/helpers.c
index 9eaa4185e0a7..fa1232873c00 100644
--- a/kernel/bpf/helpers.c
+++ b/kernel/bpf/helpers.c
@@ -1077,7 +1077,7 @@ const struct bpf_func_proto bpf_snprintf_proto = {
.func = bpf_snprintf,
.gpl_only = true,
.ret_type = RET_INTEGER,
- .arg1_type = ARG_PTR_TO_MEM_OR_NULL,
+ .arg1_type = ARG_PTR_TO_MEM_OR_NULL | MEM_WRITE,
.arg2_type = ARG_CONST_SIZE_OR_ZERO,
.arg3_type = ARG_PTR_TO_CONST_STR,
.arg4_type = ARG_PTR_TO_MEM | PTR_MAYBE_NULL | MEM_RDONLY,
diff --git a/kernel/bpf/syscall.c b/kernel/bpf/syscall.c
index ecc0929ce462..3c5c03d43f5f 100644
--- a/kernel/bpf/syscall.c
+++ b/kernel/bpf/syscall.c
@@ -6451,7 +6451,7 @@ static const struct bpf_func_proto bpf_kallsyms_lookup_name_proto = {
.func = bpf_kallsyms_lookup_name,
.gpl_only = false,
.ret_type = RET_INTEGER,
- .arg1_type = ARG_PTR_TO_MEM,
+ .arg1_type = ARG_PTR_TO_MEM | MEM_RDONLY,
.arg2_type = ARG_CONST_SIZE_OR_ZERO,
.arg3_type = ARG_ANYTHING,
.arg4_type = ARG_PTR_TO_FIXED_SIZE_MEM | MEM_UNINIT | MEM_WRITE | MEM_ALIGNED,
diff --git a/kernel/trace/bpf_trace.c b/kernel/trace/bpf_trace.c
index f73e08c223b5..bd15ff62490b 100644
--- a/kernel/trace/bpf_trace.c
+++ b/kernel/trace/bpf_trace.c
@@ -1022,7 +1022,7 @@ const struct bpf_func_proto bpf_snprintf_btf_proto = {
.func = bpf_snprintf_btf,
.gpl_only = false,
.ret_type = RET_INTEGER,
- .arg1_type = ARG_PTR_TO_MEM,
+ .arg1_type = ARG_PTR_TO_MEM | MEM_WRITE,
.arg2_type = ARG_CONST_SIZE,
.arg3_type = ARG_PTR_TO_MEM | MEM_RDONLY,
.arg4_type = ARG_CONST_SIZE,
@@ -1526,7 +1526,7 @@ static const struct bpf_func_proto bpf_read_branch_records_proto = {
.gpl_only = true,
.ret_type = RET_INTEGER,
.arg1_type = ARG_PTR_TO_CTX,
- .arg2_type = ARG_PTR_TO_MEM_OR_NULL,
+ .arg2_type = ARG_PTR_TO_MEM_OR_NULL | MEM_WRITE,
.arg3_type = ARG_CONST_SIZE_OR_ZERO,
.arg4_type = ARG_ANYTHING,
};
@@ -1661,7 +1661,7 @@ static const struct bpf_func_proto bpf_get_stack_proto_raw_tp = {
.gpl_only = true,
.ret_type = RET_INTEGER,
.arg1_type = ARG_PTR_TO_CTX,
- .arg2_type = ARG_PTR_TO_MEM | MEM_RDONLY,
+ .arg2_type = ARG_PTR_TO_UNINIT_MEM,
.arg3_type = ARG_CONST_SIZE_OR_ZERO,
.arg4_type = ARG_ANYTHING,
};
diff --git a/net/core/filter.c b/net/core/filter.c
index d43df98e1ded..d14401193b01 100644
--- a/net/core/filter.c
+++ b/net/core/filter.c
@@ -6399,7 +6399,7 @@ static const struct bpf_func_proto bpf_xdp_fib_lookup_proto = {
.gpl_only = true,
.ret_type = RET_INTEGER,
.arg1_type = ARG_PTR_TO_CTX,
- .arg2_type = ARG_PTR_TO_MEM,
+ .arg2_type = ARG_PTR_TO_MEM | MEM_WRITE,
.arg3_type = ARG_CONST_SIZE,
.arg4_type = ARG_ANYTHING,
};
@@ -6454,7 +6454,7 @@ static const struct bpf_func_proto bpf_skb_fib_lookup_proto = {
.gpl_only = true,
.ret_type = RET_INTEGER,
.arg1_type = ARG_PTR_TO_CTX,
- .arg2_type = ARG_PTR_TO_MEM,
+ .arg2_type = ARG_PTR_TO_MEM | MEM_WRITE,
.arg3_type = ARG_CONST_SIZE,
.arg4_type = ARG_ANYTHING,
};
@@ -8008,9 +8008,9 @@ static const struct bpf_func_proto bpf_tcp_raw_gen_syncookie_ipv4_proto = {
.gpl_only = true, /* __cookie_v4_init_sequence() is GPL */
.pkt_access = true,
.ret_type = RET_INTEGER,
- .arg1_type = ARG_PTR_TO_FIXED_SIZE_MEM,
+ .arg1_type = ARG_PTR_TO_FIXED_SIZE_MEM | MEM_RDONLY,
.arg1_size = sizeof(struct iphdr),
- .arg2_type = ARG_PTR_TO_MEM,
+ .arg2_type = ARG_PTR_TO_MEM | MEM_RDONLY,
.arg3_type = ARG_CONST_SIZE_OR_ZERO,
};
@@ -8040,9 +8040,9 @@ static const struct bpf_func_proto bpf_tcp_raw_gen_syncookie_ipv6_proto = {
.gpl_only = true, /* __cookie_v6_init_sequence() is GPL */
.pkt_access = true,
.ret_type = RET_INTEGER,
- .arg1_type = ARG_PTR_TO_FIXED_SIZE_MEM,
+ .arg1_type = ARG_PTR_TO_FIXED_SIZE_MEM | MEM_RDONLY,
.arg1_size = sizeof(struct ipv6hdr),
- .arg2_type = ARG_PTR_TO_MEM,
+ .arg2_type = ARG_PTR_TO_MEM | MEM_RDONLY,
.arg3_type = ARG_CONST_SIZE_OR_ZERO,
};
@@ -8060,9 +8060,9 @@ static const struct bpf_func_proto bpf_tcp_raw_check_syncookie_ipv4_proto = {
.gpl_only = true, /* __cookie_v4_check is GPL */
.pkt_access = true,
.ret_type = RET_INTEGER,
- .arg1_type = ARG_PTR_TO_FIXED_SIZE_MEM,
+ .arg1_type = ARG_PTR_TO_FIXED_SIZE_MEM | MEM_RDONLY,
.arg1_size = sizeof(struct iphdr),
- .arg2_type = ARG_PTR_TO_FIXED_SIZE_MEM,
+ .arg2_type = ARG_PTR_TO_FIXED_SIZE_MEM | MEM_RDONLY,
.arg2_size = sizeof(struct tcphdr),
};
@@ -8084,9 +8084,9 @@ static const struct bpf_func_proto bpf_tcp_raw_check_syncookie_ipv6_proto = {
.gpl_only = true, /* __cookie_v6_check is GPL */
.pkt_access = true,
.ret_type = RET_INTEGER,
- .arg1_type = ARG_PTR_TO_FIXED_SIZE_MEM,
+ .arg1_type = ARG_PTR_TO_FIXED_SIZE_MEM | MEM_RDONLY,
.arg1_size = sizeof(struct ipv6hdr),
- .arg2_type = ARG_PTR_TO_FIXED_SIZE_MEM,
+ .arg2_type = ARG_PTR_TO_FIXED_SIZE_MEM | MEM_RDONLY,
.arg2_size = sizeof(struct tcphdr),
};
#endif /* CONFIG_SYN_COOKIES */
--
2.43.0
^ permalink raw reply related
* [PATCH bpf-next v3 2/2] bpf: Require ARG_PTR_TO_MEM with memory flag
From: Zesen Liu @ 2026-01-20 8:28 UTC (permalink / raw)
To: Alexei Starovoitov, Daniel Borkmann, Andrii Nakryiko,
Martin KaFai Lau, Eduard Zingerman, Song Liu, Yonghong Song,
John Fastabend, KP Singh, Stanislav Fomichev, Hao Luo, Jiri Olsa,
Matt Bobrowski, Steven Rostedt, Masami Hiramatsu,
Mathieu Desnoyers, David S. Miller, Eric Dumazet, Jakub Kicinski,
Paolo Abeni, Simon Horman, Daniel Xu
Cc: bpf, linux-kernel, linux-trace-kernel, netdev, Shuran Liu,
Peili Gao, Haoran Ni, Zesen Liu
In-Reply-To: <20260120-helper_proto-v3-0-27b0180b4e77@gmail.com>
Add check to ensure that ARG_PTR_TO_MEM is used with either MEM_WRITE or
MEM_RDONLY.
Using ARG_PTR_TO_MEM alone without flags does not make sense because:
- If the helper does not change the argument, missing MEM_RDONLY causes the
verifier to incorrectly reject a read-only buffer.
- If the helper does change the argument, missing MEM_WRITE causes the
verifier to incorrectly assume the memory is unchanged, leading to errors
in code optimization.
Co-developed-by: Shuran Liu <electronlsr@gmail.com>
Signed-off-by: Shuran Liu <electronlsr@gmail.com>
Co-developed-by: Peili Gao <gplhust955@gmail.com>
Signed-off-by: Peili Gao <gplhust955@gmail.com>
Co-developed-by: Haoran Ni <haoran.ni.cs@gmail.com>
Signed-off-by: Haoran Ni <haoran.ni.cs@gmail.com>
Signed-off-by: Zesen Liu <ftyghome@gmail.com>
---
kernel/bpf/verifier.c | 17 +++++++++++++++++
1 file changed, 17 insertions(+)
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 9de0ec0c3ed9..a89f5bc7eff7 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -10351,10 +10351,27 @@ static bool check_btf_id_ok(const struct bpf_func_proto *fn)
return true;
}
+static bool check_mem_arg_rw_flag_ok(const struct bpf_func_proto *fn)
+{
+ int i;
+
+ for (i = 0; i < ARRAY_SIZE(fn->arg_type); i++) {
+ enum bpf_arg_type arg_type = fn->arg_type[i];
+
+ if (base_type(arg_type) != ARG_PTR_TO_MEM)
+ continue;
+ if (!(arg_type & (MEM_WRITE | MEM_RDONLY)))
+ return false;
+ }
+
+ return true;
+}
+
static int check_func_proto(const struct bpf_func_proto *fn)
{
return check_raw_mode_ok(fn) &&
check_arg_pair_ok(fn) &&
+ check_mem_arg_rw_flag_ok(fn) &&
check_btf_id_ok(fn) ? 0 : -EINVAL;
}
--
2.43.0
^ permalink raw reply related
* Re: [PATCH 17/26] rv/rvgen: fix possibly unbound variable in ltl2k
From: Gabriele Monaco @ 2026-01-20 8:59 UTC (permalink / raw)
To: Wander Lairson Costa
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <20260119205601.105821-18-wander@redhat.com>
On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> Initialize loop variable `i` before the for loop in abbreviate_atoms
> function to fix pyright static type checker error. The previous code
> left `i` potentially unbound in edge cases where the range could be
> empty, though this would not occur in practice since the loop always
> executes at least once with the given range parameters.
>
> The initialization to zero ensures that `i` has a defined value before
> entering the loop scope, satisfying static analysis requirements
> while preserving the existing logic. The for loop immediately assigns
> i to the first value from the range, so the initialization value is
> never actually used in normal execution paths.
>
> This change resolves the pyright reportPossiblyUnbound error without
> altering the function's behavior or performance characteristics.
So are we just pleasing the tool or is there a real implication of this?
Apparently code like
for i in range(len([]), -1, -1):
pass
print(i)
works just fine since range() returns at least 0 (as you mentioned in the commit
message) and i is not used before assignation in the loop, so I don't really see
a problem.
Apparently pyright devs don't want ([1]) to implement a logic to sort out the
/possibly/ unbound error here.
From what I understand, this code is already not pythonic, so rather than
silence the warning to please this tool I'd just refactor the code not to use i
after the loop (or leave it as it is, since it works fine).
What do you think?
Thanks,
Gabriele
[1] - https://github.com/microsoft/pyright/issues/844
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> ---
> tools/verification/rvgen/rvgen/ltl2k.py | 1 +
> 1 file changed, 1 insertion(+)
>
> diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> b/tools/verification/rvgen/rvgen/ltl2k.py
> index fa9ea6d597095..94dc64af1716d 100644
> --- a/tools/verification/rvgen/rvgen/ltl2k.py
> +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> @@ -45,6 +45,7 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
>
> abbrs = []
> for atom in atoms:
> + i = 0
> for i in range(len(atom), -1, -1):
> if sum(a.startswith(atom[:i]) for a in atoms) > 1:
> break
^ permalink raw reply
* Re: [PATCH 26/26] rv/rvgen: extract node marker string to class constant
From: Gabriele Monaco @ 2026-01-20 9:03 UTC (permalink / raw)
To: Wander Lairson Costa
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <20260119205601.105821-27-wander@redhat.com>
On Mon, 2026-01-19 at 17:46 -0300, Wander Lairson Costa wrote:
> Add a node_marker class constant to the Automata class to replace the
> hardcoded "{node" string literal used throughout the DOT file parsing
> logic. This follows the existing pattern established by the init_marker
> and invalid_state_str class constants in the same class.
>
> The "{node" string is used as a marker to identify node declaration
> lines in DOT files during state variable extraction and cursor
> positioning. Extracting it to a named constant improves code
> maintainability and makes the marker's purpose explicit.
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Looks fine for me, thanks!
I wonder if we could merge this patch with 15/26 that is introducing a very
similar change on init_marker.
Anyway:
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> ---
> tools/verification/rvgen/rvgen/automata.py | 9 +++++----
> 1 file changed, 5 insertions(+), 4 deletions(-)
>
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index a6889d0c26c3f..5f23db1855cd3 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -29,6 +29,7 @@ class Automata:
>
> invalid_state_str = "INVALID_STATE"
> init_marker = "__init_"
> + node_marker = "{node"
>
> def __init__(self, file_path, model_name=None):
> self.__dot_path = file_path
> @@ -76,7 +77,7 @@ class Automata:
> for cursor, line in enumerate(self.__dot_lines):
> split_line = line.split()
>
> - if len(split_line) and split_line[0] == "{node":
> + if len(split_line) and split_line[0] == self.node_marker:
> return cursor
>
> raise AutomataError("Could not find a beginning state")
> @@ -91,9 +92,9 @@ class Automata:
> continue
>
> if state == 0:
> - if line[0] == "{node":
> + if line[0] == self.node_marker:
> state = 1
> - elif line[0] != "{node":
> + elif line[0] != self.node_marker:
> break
> else:
> raise AutomataError("Could not find beginning event")
> @@ -116,7 +117,7 @@ class Automata:
> # process nodes
> for line in islice(self.__dot_lines, cursor, None):
> split_line = line.split()
> - if not split_line or split_line[0] != "{node":
> + if not split_line or split_line[0] != self.node_marker:
> break
>
> raw_state = split_line[-1]
^ permalink raw reply
* Re: [PATCH 24/26] rv/rvgen: make monitor arguments required in rvgen
From: Gabriele Monaco @ 2026-01-20 9:07 UTC (permalink / raw)
To: Wander Lairson Costa
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <20260119205601.105821-25-wander@redhat.com>
On Mon, 2026-01-19 at 17:46 -0300, Wander Lairson Costa wrote:
> Add required=True to the monitor subcommand arguments for class, spec,
> and monitor_type in rvgen. These arguments are essential for monitor
> generation and attempting to run without them would cause AttributeError
> exceptions later in the code when the script tries to access them.
>
> Making these arguments explicitly required provides clearer error
> messages to users at parse time rather than cryptic exceptions during
> execution. This improves the user experience by catching missing
> arguments early with helpful usage information.
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Good catch, thanks!
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> ---
> tools/verification/rvgen/__main__.py | 7 ++++---
> 1 file changed, 4 insertions(+), 3 deletions(-)
>
> diff --git a/tools/verification/rvgen/__main__.py
> b/tools/verification/rvgen/__main__.py
> index eeeccf81d4b90..f3e79b14c5d5d 100644
> --- a/tools/verification/rvgen/__main__.py
> +++ b/tools/verification/rvgen/__main__.py
> @@ -28,10 +28,11 @@ if __name__ == '__main__':
> monitor_parser.add_argument('-n', "--model_name", dest="model_name")
> monitor_parser.add_argument("-p", "--parent", dest="parent",
> required=False, help="Create a monitor nested
> to parent")
> - monitor_parser.add_argument('-c', "--class", dest="monitor_class",
> + monitor_parser.add_argument('-c', "--class", dest="monitor_class",
> required=True,
> help="Monitor class, either \"da\" or
> \"ltl\"")
> - monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor
> specification file")
> - monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
> + monitor_parser.add_argument('-s', "--spec", dest="spec", required=True,
> + help="Monitor specification file")
> + monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
> required=True,
> help=f"Available options: {',
> '.join(Monitor.monitor_types.keys())}")
>
> container_parser = subparsers.add_parser("container")
^ permalink raw reply
* Re: [PATCH 22/26] rv/rvgen: remove unused __get_main_name method
From: Gabriele Monaco @ 2026-01-20 9:08 UTC (permalink / raw)
To: Wander Lairson Costa
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <20260119205601.105821-23-wander@redhat.com>
On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> The __get_main_name() method in the generator module is never called
> from anywhere in the codebase. Remove this dead code to improve
> maintainability.
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Good catch, thanks!
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> ---
> tools/verification/rvgen/rvgen/generator.py | 6 ------
> 1 file changed, 6 deletions(-)
>
> diff --git a/tools/verification/rvgen/rvgen/generator.py
> b/tools/verification/rvgen/rvgen/generator.py
> index 0491f8c9cb0b9..d99a980850d64 100644
> --- a/tools/verification/rvgen/rvgen/generator.py
> +++ b/tools/verification/rvgen/rvgen/generator.py
> @@ -206,12 +206,6 @@ obj-$(CONFIG_RV_MON_{name_up}) +=
> monitors/{name}/{name}.o
> path = os.path.join(self.rv_dir, "monitors", path)
> self.__write_file(path, content)
>
> - def __get_main_name(self):
> - path = f"{self.name}/main.c"
> - if not os.path.exists(path):
> - return "main.c"
> - return "__main.c"
> -
> def print_files(self):
> main_c = self.fill_main_c()
>
^ permalink raw reply
* Re: [PATCH 21/26] rv/rvgen: remove unused sys import from dot2c
From: Gabriele Monaco @ 2026-01-20 9:16 UTC (permalink / raw)
To: Wander Lairson Costa
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <20260119205601.105821-22-wander@redhat.com>
On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> The sys module was imported in the dot2c frontend script but never
> used. This import was likely left over from earlier development or
> copied from a template that required sys for exit handling.
>
> Remove the unused import to clean up the code and satisfy linters
> that flag unused imports as errors.
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Good catch, thanks!
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> ---
> tools/verification/rvgen/dot2c | 1 -
> 1 file changed, 1 deletion(-)
>
> diff --git a/tools/verification/rvgen/dot2c b/tools/verification/rvgen/dot2c
> index bf0c67c5b66c8..1012becc7fab6 100644
> --- a/tools/verification/rvgen/dot2c
> +++ b/tools/verification/rvgen/dot2c
> @@ -16,7 +16,6 @@
> if __name__ == '__main__':
> from rvgen import dot2c
> import argparse
> - import sys
>
> parser = argparse.ArgumentParser(description='dot2c: converts a .dot file
> into a C structure')
> parser.add_argument('dot_file', help='The dot file to be converted')
^ permalink raw reply
* Re: [PATCH 20/26] rv/rvgen: refactor automata.py to use iterator-based parsing
From: Gabriele Monaco @ 2026-01-20 9:43 UTC (permalink / raw)
To: Wander Lairson Costa
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <20260119205601.105821-21-wander@redhat.com>
On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> Refactor the DOT file parsing logic in automata.py to use Python's
> iterator-based patterns instead of manual cursor indexing. The previous
> implementation relied on while loops with explicit cursor management,
> which made the code prone to off-by-one errors and would crash on
> malformed input files containing empty lines.
>
> The new implementation uses enumerate and itertools.islice to iterate
> over lines, eliminating manual cursor tracking. Functions that search
> for specific markers now use for loops with early returns and explicit
> AutomataError exceptions for missing markers, rather than assuming the
> markers exist. Additional bounds checking ensures that split line
> arrays have sufficient elements before accessing specific indices,
> preventing IndexError exceptions on malformed DOT files.
>
> The matrix creation and event variable extraction methods now use
> functional patterns with map combined with itertools.islice,
> making the intent clearer while maintaining the same behavior. Minor
> improvements include using extend instead of append in a loop, adding
> empty file validation, and replacing enumerate with range where the
> enumerated value was unused.
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
The changes look sensible, thanks.
Just know that this parser is already quite fragile and we are planning a major
refactor using ply with a well-defined grammar and tokenizer, like how the LTL
parser is implemented.
So I wouldn't spend too much time on this implementation.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> ---
> tools/verification/rvgen/rvgen/automata.py | 109 +++++++++++++--------
> 1 file changed, 67 insertions(+), 42 deletions(-)
>
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 083d0f5cfb773..a6889d0c26c3f 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -9,6 +9,7 @@
> # Documentation/trace/rv/deterministic_automata.rst
>
> import ntpath
> +from itertools import islice
>
>
> class AutomataError(OSError):
> @@ -53,37 +54,54 @@ class Automata:
> return model_name
>
> def __open_dot(self):
> - cursor = 0
> dot_lines = []
> try:
> with open(self.__dot_path) as dot_file:
> - dot_lines = dot_file.read().splitlines()
> + dot_lines = dot_file.readlines()
> except OSError as exc:
> raise AutomataError(f"Cannot open the file: {self.__dot_path}")
> from exc
>
> + if not dot_lines:
> + raise AutomataError(f"{self.__dot_path} is empty")
> +
> # checking the first line:
> - line = dot_lines[cursor].split()
> + line = dot_lines[0].split()
>
> - if (line[0] != "digraph") or (line[1] != "state_automaton"):
> + if len(line) < 2 or line[0] != "digraph" or line[1] !=
> "state_automaton":
> raise AutomataError(f"Not a valid .dot format:
> {self.__dot_path}")
> - else:
> - cursor += 1
> +
> return dot_lines
>
> def __get_cursor_begin_states(self):
> - cursor = 0
> - while self.__dot_lines[cursor].split()[0] != "{node":
> - cursor += 1
> - return cursor
> + for cursor, line in enumerate(self.__dot_lines):
> + split_line = line.split()
> +
> + if len(split_line) and split_line[0] == "{node":
> + return cursor
> +
> + raise AutomataError("Could not find a beginning state")
>
> def __get_cursor_begin_events(self):
> - cursor = 0
> - while self.__dot_lines[cursor].split()[0] != "{node":
> - cursor += 1
> - while self.__dot_lines[cursor].split()[0] == "{node":
> - cursor += 1
> - # skip initial state transition
> - cursor += 1
> + state = 0
> + cursor = 0 # make pyright happy
> +
> + for cursor, line in enumerate(self.__dot_lines):
> + line = line.split()
> + if not line:
> + continue
> +
> + if state == 0:
> + if line[0] == "{node":
> + state = 1
> + elif line[0] != "{node":
> + break
> + else:
> + raise AutomataError("Could not find beginning event")
> +
> + cursor += 1 # skip initial state transition
> + if cursor == len(self.__dot_lines):
> + raise AutomataError("Dot file ended after event beginning")
> +
> return cursor
>
> def __get_state_variables(self):
> @@ -96,9 +114,12 @@ class Automata:
> cursor = self.__get_cursor_begin_states()
>
> # process nodes
> - while self.__dot_lines[cursor].split()[0] == "{node":
> - line = self.__dot_lines[cursor].split()
> - raw_state = line[-1]
> + for line in islice(self.__dot_lines, cursor, None):
> + split_line = line.split()
> + if not split_line or split_line[0] != "{node":
> + break
> +
> + raw_state = split_line[-1]
>
> # "enabled_fired"}; -> enabled_fired
> state = raw_state.replace('"', "").replace("};", "").replace(",",
> "_")
> @@ -106,16 +127,14 @@ class Automata:
> initial_state = state[len(self.init_marker) :]
> else:
> states.append(state)
> - if "doublecircle" in self.__dot_lines[cursor]:
> + if "doublecircle" in line:
> final_states.append(state)
> has_final_states = True
>
> - if "ellipse" in self.__dot_lines[cursor]:
> + if "ellipse" in line:
> final_states.append(state)
> has_final_states = True
>
> - cursor += 1
> -
> if initial_state is None:
> raise AutomataError("The automaton doesn't have a initial state")
>
> @@ -130,26 +149,27 @@ class Automata:
> return states, initial_state, final_states
>
> def __get_event_variables(self):
> + events: list[str] = []
> # here we are at the begin of transitions, take a note, we will
> return later.
> cursor = self.__get_cursor_begin_events()
>
> - events = []
> - while self.__dot_lines[cursor].lstrip()[0] == '"':
> + for line in map(str.lstrip, islice(self.__dot_lines, cursor, None)):
> + if not line.startswith('"'):
> + break
> +
> # transitions have the format:
> # "all_fired" -> "both_fired" [ label = "disable_irq" ];
> # ------------ event is here ------------^^^^^
> - if self.__dot_lines[cursor].split()[1] == "->":
> - line = self.__dot_lines[cursor].split()
> - event = line[-2].replace('"', "")
> + split_line = line.split()
> + if len(split_line) > 1 and split_line[1] == "->":
> + event = split_line[-2].replace('"', "")
>
> # when a transition has more than one labels, they are like
> this
> # "local_irq_enable\nhw_local_irq_enable_n"
> # so split them.
>
> event = event.replace("\\n", " ")
> - for i in event.split():
> - events.append(i)
> - cursor += 1
> + events.extend(event.split())
>
> return sorted(set(events))
>
> @@ -171,32 +191,37 @@ class Automata:
>
> # declare the matrix....
> matrix = [
> - [self.invalid_state_str for x in range(nr_event)] for y in
> range(nr_state)
> + [self.invalid_state_str for _ in range(nr_event)] for _ in
> range(nr_state)
> ]
>
> # and we are back! Let's fill the matrix
> cursor = self.__get_cursor_begin_events()
>
> - while self.__dot_lines[cursor].lstrip()[0] == '"':
> - if self.__dot_lines[cursor].split()[1] == "->":
> - line = self.__dot_lines[cursor].split()
> - origin_state = line[0].replace('"', "").replace(",", "_")
> - dest_state = line[2].replace('"', "").replace(",", "_")
> - possible_events = line[-2].replace('"', "").replace("\\n", "
> ")
> + 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 = split_line[-2].replace('"',
> "").replace("\\n", " ")
> for event in possible_events.split():
> matrix[states_dict[origin_state]][events_dict[event]] =
> dest_state
> - cursor += 1
>
> return matrix
>
> def __store_init_events(self):
> events_start = [False] * len(self.events)
> events_start_run = [False] * len(self.events)
> - for i, _ in enumerate(self.events):
> + for i in range(len(self.events)):
> curr_event_will_init = 0
> curr_event_from_init = False
> curr_event_used = 0
> - for j, _ in enumerate(self.states):
> + for j in range(len(self.states)):
> if self.function[j][i] != self.invalid_state_str:
> curr_event_used += 1
> if self.function[j][i] == self.initial_state:
^ permalink raw reply
* Re: [PATCH v2] scripts/tracepoint-update: fix memory leak in add_string() on failure
From: Markus Elfring @ 2026-01-20 10:00 UTC (permalink / raw)
To: Weigang He, linux-trace-kernel
Cc: LKML, Masami Hiramatsu, Mathieu Desnoyers, Steven Rostedt
In-Reply-To: <20260119114542.1714405-1-geoffreyhe2@gmail.com>
…
> This bug is found by my static analysis tool …
Will any additional background information become more helpful here?
> ---
> scripts/tracepoint-update.c | 2 ++
…
Some contributors would appreciate patch version descriptions.
https://lore.kernel.org/all/?q=%22This+looks+like+a+new+version+of+a+previously+submitted+patch%22
https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/tree/Documentation/process/submitting-patches.rst?h=v6.19-rc6#n310
Regards,
Markus
^ permalink raw reply
* Re: [PATCH 03/26] rv/rvgen: replace % string formatting with f-strings
From: Gabriele Monaco @ 2026-01-20 10:02 UTC (permalink / raw)
To: Wander Lairson Costa
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <20260119205601.105821-4-wander@redhat.com>
On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> Replace all instances of percent-style string formatting with
> f-strings across the rvgen codebase. This modernizes the string
> formatting to use Python 3.6+ features, providing clearer and more
> maintainable code while improving runtime performance.
>
> The conversion handles all formatting cases including simple variable
> substitution, multi-variable formatting, and complex format specifiers.
> Dynamic width formatting is converted from "%*s" to "{var:>{width}}"
> using proper alignment syntax. Template strings for generated C code
> properly escape braces using double-brace syntax to produce literal
> braces in the output.
>
> F-strings provide approximately 2x performance improvement over percent
> formatting and are the recommended approach in modern Python.
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Sad to see the printf-style things go, but it's for better. Thanks.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> ---
> tools/verification/rvgen/__main__.py | 6 +--
> tools/verification/rvgen/rvgen/automata.py | 6 +--
> tools/verification/rvgen/rvgen/dot2c.py | 40 +++++++-------
> tools/verification/rvgen/rvgen/dot2k.py | 26 ++++-----
> tools/verification/rvgen/rvgen/generator.py | 59 ++++++++++-----------
> tools/verification/rvgen/rvgen/ltl2k.py | 30 +++++------
> 6 files changed, 82 insertions(+), 85 deletions(-)
>
> diff --git a/tools/verification/rvgen/__main__.py
> b/tools/verification/rvgen/__main__.py
> index 768b11a1e978b..eeeccf81d4b90 100644
> --- a/tools/verification/rvgen/__main__.py
> +++ b/tools/verification/rvgen/__main__.py
> @@ -40,7 +40,7 @@ if __name__ == '__main__':
> params = parser.parse_args()
>
> if params.subcmd == "monitor":
> - print("Opening and parsing the specification file %s" % params.spec)
> + print(f"Opening and parsing the specification file {params.spec}")
> if params.monitor_class == "da":
> monitor = dot2k(params.spec, params.monitor_type, vars(params))
> elif params.monitor_class == "ltl":
> @@ -51,11 +51,11 @@ if __name__ == '__main__':
> else:
> monitor = Container(vars(params))
>
> - print("Writing the monitor into the directory %s" % monitor.name)
> + print(f"Writing the monitor into the directory {monitor.name}")
> monitor.print_files()
> print("Almost done, checklist")
> if params.subcmd == "monitor":
> - print(" - Edit the %s/%s.c to add the instrumentation" %
> (monitor.name, monitor.name))
> + print(f" - Edit the {monitor.name}/{monitor.name}.c to add the
> instrumentation")
> print(monitor.fill_tracepoint_tooltip())
> print(monitor.fill_makefile_tooltip())
> print(monitor.fill_kconfig_tooltip())
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 8d88c3b65d00d..3e24313a2eaec 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -39,11 +39,11 @@ class Automata:
> basename = ntpath.basename(self.__dot_path)
> if not basename.endswith(".dot") and not basename.endswith(".gv"):
> print("not a dot file")
> - raise AutomataError("not a dot file: %s" % self.__dot_path)
> + raise AutomataError(f"not a dot file: {self.__dot_path}")
>
> model_name = ntpath.splitext(basename)[0]
> if model_name.__len__() == 0:
> - raise AutomataError("not a dot file: %s" % self.__dot_path)
> + raise AutomataError(f"not a dot file: {self.__dot_path}")
>
> return model_name
>
> @@ -62,7 +62,7 @@ class Automata:
> line = dot_lines[cursor].split()
>
> if (line[0] != "digraph") and (line[1] != "state_automaton"):
> - raise AutomataError("Not a valid .dot format: %s" %
> self.__dot_path)
> + raise AutomataError(f"Not a valid .dot format:
> {self.__dot_path}")
> else:
> cursor += 1
> return dot_lines
> diff --git a/tools/verification/rvgen/rvgen/dot2c.py
> b/tools/verification/rvgen/rvgen/dot2c.py
> index 1a1770e7f20c0..78959d345c26e 100644
> --- a/tools/verification/rvgen/rvgen/dot2c.py
> +++ b/tools/verification/rvgen/rvgen/dot2c.py
> @@ -37,11 +37,11 @@ class Dot2c(Automata):
>
> def __get_enum_states_content(self):
> buff = []
> - buff.append("\t%s%s = 0," % (self.initial_state, self.enum_suffix))
> + buff.append(f"\t{self.initial_state}{self.enum_suffix} = 0,")
> for state in self.states:
> if state != self.initial_state:
> - buff.append("\t%s%s," % (state, self.enum_suffix))
> - buff.append("\tstate_max%s" % (self.enum_suffix))
> + buff.append(f"\t{state}{self.enum_suffix},")
> + buff.append(f"\tstate_max{self.enum_suffix}")
>
> return buff
>
> @@ -51,7 +51,7 @@ class Dot2c(Automata):
>
> def format_states_enum(self):
> buff = []
> - buff.append("enum %s {" % self.enum_states_def)
> + buff.append(f"enum {self.enum_states_def} {{")
> buff.append(self.get_enum_states_string())
> buff.append("};\n")
>
> @@ -62,12 +62,12 @@ class Dot2c(Automata):
> first = True
> for event in self.events:
> if first:
> - buff.append("\t%s%s = 0," % (event, self.enum_suffix))
> + buff.append(f"\t{event}{self.enum_suffix} = 0,")
> first = False
> else:
> - buff.append("\t%s%s," % (event, self.enum_suffix))
> + buff.append(f"\t{event}{self.enum_suffix},")
>
> - buff.append("\tevent_max%s" % self.enum_suffix)
> + buff.append(f"\tevent_max{self.enum_suffix}")
>
> return buff
>
> @@ -77,7 +77,7 @@ class Dot2c(Automata):
>
> def format_events_enum(self):
> buff = []
> - buff.append("enum %s {" % self.enum_events_def)
> + buff.append(f"enum {self.enum_events_def} {{")
> buff.append(self.get_enum_events_string())
> buff.append("};\n")
>
> @@ -93,25 +93,25 @@ class Dot2c(Automata):
> min_type = "unsigned int"
>
> if self.states.__len__() > 1000000:
> - raise AutomataError("Too many states: %d" %
> self.states.__len__())
> + raise AutomataError(f"Too many states: {self.states.__len__()}")
>
> return min_type
>
> def format_automaton_definition(self):
> min_type = self.get_minimun_type()
> buff = []
> - buff.append("struct %s {" % self.struct_automaton_def)
> - buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix))
> - buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix))
> - buff.append("\t%s function[state_max%s][event_max%s];" % (min_type,
> self.enum_suffix, self.enum_suffix))
> - buff.append("\t%s initial_state;" % min_type)
> - buff.append("\tbool final_states[state_max%s];" % (self.enum_suffix))
> + buff.append(f"struct {self.struct_automaton_def} {{")
> + buff.append(f"\tchar *state_names[state_max{self.enum_suffix}];")
> + buff.append(f"\tchar *event_names[event_max{self.enum_suffix}];")
> + buff.append(f"\t{min_type}
> function[state_max{self.enum_suffix}][event_max{self.enum_suffix}];")
> + buff.append(f"\t{min_type} initial_state;")
> + buff.append(f"\tbool final_states[state_max{self.enum_suffix}];")
> buff.append("};\n")
> return buff
>
> def format_aut_init_header(self):
> buff = []
> - buff.append("static const struct %s %s = {" %
> (self.struct_automaton_def, self.var_automaton_def))
> + buff.append(f"static const struct {self.struct_automaton_def}
> {self.var_automaton_def} = {{")
> return buff
>
> def __get_string_vector_per_line_content(self, buff):
> @@ -169,9 +169,9 @@ class Dot2c(Automata):
> next_state = self.function[x][y] + self.enum_suffix
>
> if linetoolong:
> - line += "\t\t\t%s" % next_state
> + line += f"\t\t\t{next_state}"
> else:
> - line += "%*s" % (maxlen, next_state)
> + line += f"{next_state:>{maxlen}}"
> if y != nr_events-1:
> line += ",\n" if linetoolong else ", "
> else:
> @@ -215,7 +215,7 @@ class Dot2c(Automata):
>
> def format_aut_init_final_states(self):
> buff = []
> - buff.append("\t.final_states = { %s }," %
> self.get_aut_init_final_states())
> + buff.append(f"\t.final_states = {{ {self.get_aut_init_final_states()}
> }},")
>
> return buff
>
> @@ -231,7 +231,7 @@ class Dot2c(Automata):
>
> def format_invalid_state(self):
> buff = []
> - buff.append("#define %s state_max%s\n" % (self.invalid_state_str,
> self.enum_suffix))
> + buff.append(f"#define {self.invalid_state_str}
> state_max{self.enum_suffix}\n")
>
> return buff
>
> diff --git a/tools/verification/rvgen/rvgen/dot2k.py
> b/tools/verification/rvgen/rvgen/dot2k.py
> index ed0a3c9011069..1c0d0235bdf62 100644
> --- a/tools/verification/rvgen/rvgen/dot2k.py
> +++ b/tools/verification/rvgen/rvgen/dot2k.py
> @@ -19,7 +19,7 @@ class dot2k(Monitor, Dot2c):
> self.monitor_type = MonitorType
> Monitor.__init__(self, extra_params)
> Dot2c.__init__(self, file_path, extra_params.get("model_name"))
> - self.enum_suffix = "_%s" % self.name
> + self.enum_suffix = f"_{self.name}"
>
> def fill_monitor_type(self):
> return self.monitor_type.upper()
> @@ -27,7 +27,7 @@ class dot2k(Monitor, Dot2c):
> def fill_tracepoint_handlers_skel(self):
> buff = []
> for event in self.events:
> - buff.append("static void handle_%s(void *data, /* XXX: fill
> header */)" % event)
> + buff.append(f"static void handle_{event}(void *data, /* XXX: fill
> header */)")
> buff.append("{")
> handle = "handle_event"
> if self.is_start_event(event):
> @@ -38,9 +38,9 @@ class dot2k(Monitor, Dot2c):
> handle = "handle_start_run_event"
> if self.monitor_type == "per_task":
> buff.append("\tstruct task_struct *p = /* XXX: how do I get
> p? */;");
> - buff.append("\tda_%s_%s(p, %s%s);" % (handle, self.name,
> event, self.enum_suffix));
> + buff.append(f"\tda_{handle}_{self.name}(p,
> {event}{self.enum_suffix});");
> else:
> - buff.append("\tda_%s_%s(%s%s);" % (handle, self.name, event,
> self.enum_suffix));
> +
> buff.append(f"\tda_{handle}_{self.name}({event}{self.enum_suffix});");
> buff.append("}")
> buff.append("")
> return '\n'.join(buff)
> @@ -48,20 +48,20 @@ class dot2k(Monitor, Dot2c):
> def fill_tracepoint_attach_probe(self):
> buff = []
> for event in self.events:
> - buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint
> */, handle_%s);" % (self.name, event))
> + buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX:
> tracepoint */, handle_{event});")
> return '\n'.join(buff)
>
> def fill_tracepoint_detach_helper(self):
> buff = []
> for event in self.events:
> - buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint
> */, handle_%s);" % (self.name, event))
> + buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX:
> tracepoint */, handle_{event});")
> return '\n'.join(buff)
>
> def fill_model_h_header(self):
> buff = []
> buff.append("/* SPDX-License-Identifier: GPL-2.0 */")
> buff.append("/*")
> - buff.append(" * Automatically generated C representation of %s
> automaton" % (self.name))
> + buff.append(f" * Automatically generated C representation of
> {self.name} automaton")
> buff.append(" * For further information about this format, see kernel
> documentation:")
> buff.append(" * Documentation/trace/rv/deterministic_automata.rst")
> buff.append(" */")
> @@ -73,10 +73,10 @@ class dot2k(Monitor, Dot2c):
> #
> # Adjust the definition names
> #
> - self.enum_states_def = "states_%s" % self.name
> - self.enum_events_def = "events_%s" % self.name
> - self.struct_automaton_def = "automaton_%s" % self.name
> - self.var_automaton_def = "automaton_%s" % self.name
> + self.enum_states_def = f"states_{self.name}"
> + self.enum_events_def = f"events_{self.name}"
> + self.struct_automaton_def = f"automaton_{self.name}"
> + self.var_automaton_def = f"automaton_{self.name}"
>
> buff = self.fill_model_h_header()
> buff += self.format_model()
> @@ -111,8 +111,8 @@ class dot2k(Monitor, Dot2c):
> tp_args.insert(0, tp_args_id)
> tp_proto_c = ", ".join([a+b for a,b in tp_args])
> tp_args_c = ", ".join([b for a,b in tp_args])
> - buff.append(" TP_PROTO(%s)," % tp_proto_c)
> - buff.append(" TP_ARGS(%s)" % tp_args_c)
> + buff.append(f" TP_PROTO({tp_proto_c}),")
> + buff.append(f" TP_ARGS({tp_args_c})")
> return '\n'.join(buff)
>
> def fill_main_c(self):
> diff --git a/tools/verification/rvgen/rvgen/generator.py
> b/tools/verification/rvgen/rvgen/generator.py
> index af1662e2c20a7..6d16fb68798a7 100644
> --- a/tools/verification/rvgen/rvgen/generator.py
> +++ b/tools/verification/rvgen/rvgen/generator.py
> @@ -40,7 +40,7 @@ class RVGenerator:
> if platform.system() != "Linux":
> raise OSError("I can only run on Linux.")
>
> - kernel_path = os.path.join("/lib/modules/%s/build" %
> platform.release(), self.rv_dir)
> + kernel_path =
> os.path.join(f"/lib/modules/{platform.release()}/build", self.rv_dir)
>
> # if the current kernel is from a distro this may not be a full
> kernel tree
> # verify that one of the files we are going to modify is available
> @@ -69,11 +69,11 @@ class RVGenerator:
> return self._read_file(path)
>
> def fill_parent(self):
> - return "&rv_%s" % self.parent if self.parent else "NULL"
> + return f"&rv_{self.parent}" if self.parent else "NULL"
>
> def fill_include_parent(self):
> if self.parent:
> - return "#include <monitors/%s/%s.h>\n" % (self.parent,
> self.parent)
> + return f"#include <monitors/{self.parent}/{self.parent}.h>\n"
> return ""
>
> def fill_tracepoint_handlers_skel(self):
> @@ -119,7 +119,7 @@ class RVGenerator:
> buff = []
> buff.append(" # XXX: add dependencies if there")
> if self.parent:
> - buff.append(" depends on RV_MON_%s" % self.parent.upper())
> + buff.append(f" depends on RV_MON_{self.parent.upper()}")
> buff.append(" default y")
> return '\n'.join(buff)
>
> @@ -145,31 +145,30 @@ class RVGenerator:
> monitor_class_type = self.fill_monitor_class_type()
> if self.auto_patch:
> self._patch_file("rv_trace.h",
> - "// Add new monitors based on CONFIG_%s here" %
> monitor_class_type,
> - "#include <monitors/%s/%s_trace.h>" % (self.name,
> self.name))
> - return " - Patching %s/rv_trace.h, double check the result" %
> self.rv_dir
> + f"// Add new monitors based on
> CONFIG_{monitor_class_type} here",
> + f"#include
> <monitors/{self.name}/{self.name}_trace.h>")
> + return f" - Patching {self.rv_dir}/rv_trace.h, double check the
> result"
>
> - return """ - Edit %s/rv_trace.h:
> -Add this line where other tracepoints are included and %s is defined:
> -#include <monitors/%s/%s_trace.h>
> -""" % (self.rv_dir, monitor_class_type, self.name, self.name)
> + return f""" - Edit {self.rv_dir}/rv_trace.h:
> +Add this line where other tracepoints are included and {monitor_class_type}
> is defined:
> +#include <monitors/{self.name}/{self.name}_trace.h>
> +"""
>
> def _kconfig_marker(self, container=None) -> str:
> - return "# Add new %smonitors here" % (container + " "
> - if container else "")
> + return f"# Add new {container + ' ' if container else ''}monitors
> here"
>
> def fill_kconfig_tooltip(self):
> if self.auto_patch:
> # monitors with a container should stay together in the Kconfig
> self._patch_file("Kconfig",
> self._kconfig_marker(self.parent),
> - "source \"kernel/trace/rv/monitors/%s/Kconfig\""
> % (self.name))
> - return " - Patching %s/Kconfig, double check the result" %
> self.rv_dir
> + f"source
> \"kernel/trace/rv/monitors/{self.name}/Kconfig\"")
> + return f" - Patching {self.rv_dir}/Kconfig, double check the
> result"
>
> - return """ - Edit %s/Kconfig:
> + return f""" - Edit {self.rv_dir}/Kconfig:
> Add this line where other monitors are included:
> -source \"kernel/trace/rv/monitors/%s/Kconfig\"
> -""" % (self.rv_dir, self.name)
> +source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"
> +"""
>
> def fill_makefile_tooltip(self):
> name = self.name
> @@ -177,18 +176,18 @@ source \"kernel/trace/rv/monitors/%s/Kconfig\"
> if self.auto_patch:
> self._patch_file("Makefile",
> "# Add new monitors here",
> - "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" %
> (name_up, name, name))
> - return " - Patching %s/Makefile, double check the result" %
> self.rv_dir
> + f"obj-$(CONFIG_RV_MON_{name_up}) +=
> monitors/{name}/{name}.o")
> + return f" - Patching {self.rv_dir}/Makefile, double check the
> result"
>
> - return """ - Edit %s/Makefile:
> + return f""" - Edit {self.rv_dir}/Makefile:
> Add this line where other monitors are included:
> -obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
> -""" % (self.rv_dir, name_up, name, name)
> +obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
> +"""
>
> def fill_monitor_tooltip(self):
> if self.auto_patch:
> - return " - Monitor created in %s/monitors/%s" % (self.rv_dir,
> self. name)
> - return " - Move %s/ to the kernel's monitor directory (%s/monitors)"
> % (self.name, self.rv_dir)
> + return f" - Monitor created in
> {self.rv_dir}/monitors/{self.name}"
> + return f" - Move {self.name}/ to the kernel's monitor directory
> ({self.rv_dir}/monitors)"
>
> def __create_directory(self):
> path = self.name
> @@ -205,13 +204,13 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
> file.close()
>
> def _create_file(self, file_name, content):
> - path = "%s/%s" % (self.name, file_name)
> + path = f"{self.name}/{file_name}"
> if self.auto_patch:
> path = os.path.join(self.rv_dir, "monitors", path)
> self.__write_file(path, content)
>
> def __get_main_name(self):
> - path = "%s/%s" % (self.name, "main.c")
> + path = f"{self.name}/main.c"
> if not os.path.exists(path):
> return "main.c"
> return "__main.c"
> @@ -221,11 +220,11 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
>
> self.__create_directory()
>
> - path = "%s.c" % self.name
> + path = f"{self.name}.c"
> self._create_file(path, main_c)
>
> model_h = self.fill_model_h()
> - path = "%s.h" % self.name
> + path = f"{self.name}.h"
> self._create_file(path, model_h)
>
> kconfig = self.fill_kconfig()
> @@ -256,5 +255,5 @@ class Monitor(RVGenerator):
> def print_files(self):
> super().print_files()
> trace_h = self.fill_trace_h()
> - path = "%s_trace.h" % self.name
> + path = f"{self.name}_trace.h"
> self._create_file(path, trace_h)
> diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> b/tools/verification/rvgen/rvgen/ltl2k.py
> index b075f98d50c47..fa9ea6d597095 100644
> --- a/tools/verification/rvgen/rvgen/ltl2k.py
> +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> @@ -73,7 +73,7 @@ class ltl2k(generator.Monitor):
> ]
>
> for node in self.ba:
> - buf.append("\tS%i," % node.id)
> + buf.append(f"\tS{node.id},")
> buf.append("\tRV_NUM_BA_STATES")
> buf.append("};")
> buf.append("static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);")
> @@ -82,7 +82,7 @@ class ltl2k(generator.Monitor):
> def _fill_atoms(self):
> buf = ["enum ltl_atom {"]
> for a in sorted(self.atoms):
> - buf.append("\tLTL_%s," % a)
> + buf.append(f"\tLTL_{a},")
> buf.append("\tLTL_NUM_ATOM")
> buf.append("};")
> buf.append("static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);")
> @@ -96,7 +96,7 @@ class ltl2k(generator.Monitor):
> ]
>
> for name in self.atoms_abbr:
> - buf.append("\t\t\"%s\"," % name)
> + buf.append(f"\t\t\"{name}\",")
>
> buf.extend([
> "\t};",
> @@ -113,19 +113,19 @@ class ltl2k(generator.Monitor):
> continue
>
> if isinstance(node.op, ltl2ba.AndOp):
> - buf.append("\tbool %s = %s && %s;" % (node, node.op.left,
> node.op.right))
> + buf.append(f"\tbool {node} = {node.op.left} &&
> {node.op.right};")
> required_values |= {str(node.op.left), str(node.op.right)}
> elif isinstance(node.op, ltl2ba.OrOp):
> - buf.append("\tbool %s = %s || %s;" % (node, node.op.left,
> node.op.right))
> + buf.append(f"\tbool {node} = {node.op.left} ||
> {node.op.right};")
> required_values |= {str(node.op.left), str(node.op.right)}
> elif isinstance(node.op, ltl2ba.NotOp):
> - buf.append("\tbool %s = !%s;" % (node, node.op.child))
> + buf.append(f"\tbool {node} = !{node.op.child};")
> required_values.add(str(node.op.child))
>
> for atom in self.atoms:
> if atom.lower() not in required_values:
> continue
> - buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" %
> (atom.lower(), atom))
> + buf.append(f"\tbool {atom.lower()} = test_bit(LTL_{atom}, mon-
> >atoms);")
>
> buf.reverse()
>
> @@ -153,7 +153,7 @@ class ltl2k(generator.Monitor):
> ])
>
> for node in self.ba:
> - buf.append("\tcase S%i:" % node.id)
> + buf.append(f"\tcase S{node.id}:")
>
> for o in sorted(node.outgoing):
> line = "\t\tif "
> @@ -163,7 +163,7 @@ class ltl2k(generator.Monitor):
> lines = break_long_line(line, indent)
> buf.extend(lines)
>
> - buf.append("\t\t\t__set_bit(S%i, next);" % o.id)
> + buf.append(f"\t\t\t__set_bit(S{o.id}, next);")
> buf.append("\t\tbreak;")
> buf.extend([
> "\t}",
> @@ -197,7 +197,7 @@ class ltl2k(generator.Monitor):
> lines = break_long_line(line, indent)
> buf.extend(lines)
>
> - buf.append("\t\t__set_bit(S%i, mon->states);" % node.id)
> + buf.append(f"\t\t__set_bit(S{node.id}, mon->states);")
> buf.append("}")
> return buf
>
> @@ -205,23 +205,21 @@ class ltl2k(generator.Monitor):
> buff = []
> buff.append("static void handle_example_event(void *data, /* XXX:
> fill header */)")
> buff.append("{")
> - buff.append("\tltl_atom_update(task, LTL_%s, true/false);" %
> self.atoms[0])
> + buff.append(f"\tltl_atom_update(task, LTL_{self.atoms[0]},
> true/false);")
> buff.append("}")
> buff.append("")
> return '\n'.join(buff)
>
> def fill_tracepoint_attach_probe(self):
> - return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */,
> handle_example_event);" \
> - % self.name
> + return f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint
> */, handle_example_event);"
>
> def fill_tracepoint_detach_helper(self):
> - return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */,
> handle_sample_event);" \
> - % self.name
> + return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint
> */, handle_sample_event);"
>
> def fill_atoms_init(self):
> buff = []
> for a in self.atoms:
> - buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % a)
> + buff.append(f"\tltl_atom_set(mon, LTL_{a}, true/false);")
> return '\n'.join(buff)
>
> def fill_model_h(self):
^ permalink raw reply
* Re: [PATCH 02/26] rv/rvgen: remove bare except clauses in generator
From: Gabriele Monaco @ 2026-01-20 10:05 UTC (permalink / raw)
To: Wander Lairson Costa
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <20260119205601.105821-3-wander@redhat.com>
On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> Remove bare except clauses from the generator module that were
> catching all exceptions including KeyboardInterrupt and SystemExit.
> This follows the same exception handling improvements made in the
> previous AutomataError commit and addresses PEP 8 violations.
>
> The bare except clause in __create_directory was silently catching
> and ignoring all errors after printing a message, which could mask
> serious issues. For __write_file, the bare except created a critical
> bug where the file variable could remain undefined if open() failed,
> causing a NameError when attempting to write to or close the file.
>
> These methods now let OSError propagate naturally, allowing callers
> to handle file system errors appropriately. This provides clearer
> error reporting and allows Python's exception handling to show
> complete stack traces with proper error types and locations.
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Looks good to me, thanks!
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> ---
> tools/verification/rvgen/rvgen/generator.py | 9 +--------
> 1 file changed, 1 insertion(+), 8 deletions(-)
>
> diff --git a/tools/verification/rvgen/rvgen/generator.py
> b/tools/verification/rvgen/rvgen/generator.py
> index a7bee6b1ea70c..af1662e2c20a7 100644
> --- a/tools/verification/rvgen/rvgen/generator.py
> +++ b/tools/verification/rvgen/rvgen/generator.py
> @@ -198,17 +198,10 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
> os.mkdir(path)
> except FileExistsError:
> return
> - except:
> - print("Fail creating the output dir: %s" % self.name)
>
> def __write_file(self, file_name, content):
> - try:
> - file = open(file_name, 'w')
> - except:
> - print("Fail writing to file: %s" % file_name)
> -
> + file = open(file_name, 'w')
> file.write(content)
> -
> file.close()
>
> def _create_file(self, file_name, content):
^ permalink raw reply
* [RFC v4 0/7] ext4: fast commit: snapshot inode state for FC log
From: Li Chen @ 2026-01-20 11:25 UTC (permalink / raw)
To: Zhang Yi, Theodore Ts'o, Andreas Dilger
Cc: Steven Rostedt, Masami Hiramatsu, Mathieu Desnoyers, linux-ext4,
linux-trace-kernel, linux-kernel
Hi,
(This RFC v4 series is based on linux-next tag next-20260106, plus the
prerequisite patch "ext4: fast commit: make s_fc_lock reclaim-safe" posted at:
https://lore.kernel.org/all/20260106120621.440126-1-me@linux.beauty/)
Zhang Yi in RFC v3 review pointed out that postponing lockdep assertions only
masks the issue, and that sleeping in ext4_fc_track_inode() while holding
i_data_sem can form a real ABBA deadlock if the fast commit writer also needs
i_data_sem while the inode is in FC_COMMITTING.
Zhang Yi suggested two possible directions to address the root cause:
1. "Ha, the solution seems to have already been listed in the TODOs in
fast_commit.c.
Change ext4_fc_commit() to lookup logical to physical mapping using extent
status tree. This would get rid of the need to call ext4_fc_track_inode()
before acquiring i_data_sem. To do that we would need to ensure that
modified extents from the extent status tree are not evicted from memory."
2. "Alternatively, recording the mapped range of tracking might also be
feasible."
This series implements a hybrid way: it implements approach 2 by snapshotting inode image
and mapped ranges at commit time, and consuming only snapshots during log
writing.
Approach 2 still needs a mapping source while building the snapshot
(logical-to-physical and unwritten/hole semantics). Calling ext4_map_blocks()
there would take i_data_sem and can block inside the
jbd2_journal_lock_updates() window, which risks deadlocks or unbounded stalls.
So the snapshot path uses approach 1's extent status lookups as a best-effort
mapping source to avoid ext4_map_blocks().
I did not fuly implement approach 1 (making extent status lookups
authoritative by preventing reclaim of needed entries) because that would need
additional pinning/integration under memory pressure and a larger correctness
surface. Instead, the extent status tree is treated as a cache and the
snapshot path falls back to full commit on cache misses or unstable mappings
(e.g. delayed allocation).
Lock inversion / deadlock model (before):
CPU0 (metadata update) CPU1 (fast commit)
-------------------- -----------------
... hold i_data_sem (A) mutex_lock(s_fc_lock) (B)
ext4_fc_track_inode() ext4_fc_write_inode_data()
mutex_lock(s_fc_lock) (B) ext4_map_blocks()
wait FC_COMMITTING (sleep) down_read(i_data_sem) (A)
This creates i_data_sem (A) -> s_fc_lock (B) on update paths, and
s_fc_lock (B) -> i_data_sem (A) on commit paths. Once CPU0 sleeps while
holding (A), CPU1 can block on (A) while holding (B), completing the ABBA
cycle.
New model (this series):
CPU0 (metadata update) CPU1 (fast commit)
-------------------- -----------------
... maybe hold i_data_sem (A) jbd2_journal_lock_updates()
ext4_fc_track_*() snapshot inode + ranges (no map_blocks)
mutex_lock(s_fc_lock) (B) jbd2_journal_unlock_updates()
if FC_COMMITTING: set FC_REQUEUE s_fc_lock (B)
no sleep write FC log from snapshots only
cleanup: clear COMMITTING, requeue if set
The commit path no longer takes i_data_sem while holding s_fc_lock, and
tracking no longer sleeps waiting for FC_COMMITTING. If an inode is updated
during a fast commit, EXT4_STATE_FC_REQUEUE records that fact and the inode
is moved to FC_Q_STAGING for the next commit.
The only remaning FC_COMMITTING waiter is ext4_fc_del(), which drops
s_fc_lock before sleeping.
This series snapshots the on-disk inode and tracked data ranges while journal
updates are locked and existing handles are drained. The log writing phase then
serializes only snapshots, so it no longer needs to call ext4_map_blocks() and
take i_data_sem under s_fc_lock. This is done in two steps: patch 1 drops
ext4_map_blocks() from log writing by introducing commit-time snapshots, and
patch 5 drops ext4_map_blocks() from the snapshot path by using the extent
status cache. The snapshot also records whether a mapped extent is unwritten,
so the ADD_RANGE records (and replay) preserve unwritten semantics.
Snapshotting runs under jbd2_journal_lock_updates(). Since a cache miss in
ext4_get_inode_loc() can start synchronous inode table I/O and stall handle
starts for milliseconds, patch 1 uses ext4_get_inode_loc_noio() and falls back
to full commit if the inode table block is not present or not uptodate.
ext4_fc_track_inode() also stops waiting for FC_COMMITTING. Updates during an
ongoing fast commit are marked with EXT4_STATE_FC_REQUEUE and are replayed in
the next fast commit, while ext4_fc_del() waits for FC_COMMITTING so an inode
cannot be removed while the commit thread is still using it.
The extent status tree is a cache, not an authoritative source, so the snapshot
path falls back to full commit on cache misses or unstable mappings (e.g.
delayed allocation). This includes cases where extent status entries are not
present (or have been reclaimed) under memory pressure. The snapshot path does
not try to rebuild mappings by calling ext4_map_blocks(); instead it simply
marks the transaction fast commit ineligible.
To keep the updates-locked window bounded, the snapshot path caps the number of
snapshotted inodes and ranges per fast commit (currently 1024 inodes and 2048
ranges) and falls back to full commit when the cap is exceeded. The series also
handles the journal inode i_data_sem lockdep false positive via subclassing;
journal inode mapping may still take i_data_sem even when data inode mapping is
avoided.
Patch 6 adds the ext4_fc_lock_updates tracepoint to quantify the updates-locked
window and snapshot fallback reasons. Patch 7 extends
/proc/fs/ext4/<sb_id>/fc_info with best-effort snapshot counters. If the /proc
interface is undesirable, I can drop patch 7 and keep the tracepoint only, or
drop even both.
Testing and mesurement were done on a QEMU/KVM guest with virtio-pmem + dax
(ext4 -O fast_commit, mounted dax,noatime). The workload does python3 500x
{4K write + fsync}, fallocate 256M, and python3 500x {creat + fsync(dir)}.
Over 3 cold boots, ext4_fc_lock_updates reported locked_ns p50 2.88-2.92 us,
p99 <= 6.71 us, and max <= 102.71 us, with snap_err always 0. Under stress-ng
memory pressure (stress-ng --vm 4 --vm-bytes 75% --timeout 60s), locked_ns p50
2.94 us, p99 <= 4.97 us, and max <= 20.07 us. The fc_info snapshot failure
counters stayed at 0.
These hold times are in the low microseconds range, and the caps keep the
worst case bounded.
Comments and guidance are very welcome. Please let me know if there are any
concerns about correctness, corner cases, or better approaches.
RFC v3 -> RFC v4:
- Replace lockdep_assert movement with removing the wait in
ext4_fc_track_inode() and using EXT4_STATE_FC_REQUEUE to capture updates
during an ongoing fast commit.
- Replace dropping s_fc_lock around log writing with commit-time snapshots of
inode image and mapped ranges (recording the mapped range of tracking as
suggested by Zhang Yi) so log writing consumes only snapshots.
- Avoid inode table I/O under jbd2_journal_lock_updates() via
ext4_get_inode_loc_noio() and fallback to full commit on cache misses.
- Use the extent status cache for snapshot mappings and fall back to full
commit on cache misses or unstable mappings (e.g. delayed allocation).
- Add tracepoint and /proc snapshot stats to quantify the updates-locked window
and snapshot fallback reasons.
RFC v2 -> RFC v3:
- rebase ontop of https://lore.kernel.org/linux-ext4/20251223131342.287864-1-me@linux.beauty/T/#u
RFC v1 -> RFC v2:
- patch 1: move comments to correct place
- patch 2: add it to patchset.
- add missing RFC prefix
RFC v1: https://lore.kernel.org/linux-ext4/20251222032655.87056-1-me@linux.beauty/T/#u
RFC v2: https://lore.kernel.org/linux-ext4/20251222151906.24607-1-me@linux.beauty/T/#t
RFC v3: https://lore.kernel.org/linux-ext4/20251224032943.134063-1-me@linux.beauty/
Thanks,
Li Chen (7):
ext4: fast commit: snapshot inode state before writing log
ext4: lockdep: handle i_data_sem subclassing for special inodes
ext4: fast commit: avoid waiting for FC_COMMITTING
ext4: fast commit: avoid self-deadlock in inode snapshotting
ext4: fast commit: avoid i_data_sem by dropping ext4_map_blocks() in
snapshots
ext4: fast commit: add lock_updates tracepoint
ext4: fast commit: export snapshot stats in fc_info
fs/ext4/ext4.h | 58 ++-
fs/ext4/fast_commit.c | 718 +++++++++++++++++++++++++++++-------
fs/ext4/inode.c | 51 +++
fs/ext4/super.c | 9 +
include/trace/events/ext4.h | 33 ++
5 files changed, 735 insertions(+), 134 deletions(-)
--
2.52.0
^ permalink raw reply
* [RFC v4 6/7] ext4: fast commit: add lock_updates tracepoint
From: Li Chen @ 2026-01-20 11:25 UTC (permalink / raw)
To: Zhang Yi, Theodore Ts'o, Andreas Dilger, Steven Rostedt,
Masami Hiramatsu, Mathieu Desnoyers, linux-ext4, linux-kernel,
linux-trace-kernel
Cc: Li Chen
In-Reply-To: <20260120112538.132774-1-me@linux.beauty>
Commit-time fast commit snapshots run under jbd2_journal_lock_updates(),
so it is useful to quantify the time spent with updates locked and to
understand why snapshotting can fail.
Add a new tracepoint, ext4_fc_lock_updates, reporting the time spent in
the updates-locked window along with the number of snapshotted inodes
and ranges. Record the first snapshot failure reason in a stable snap_err
field for tooling.
Signed-off-by: Li Chen <me@linux.beauty>
---
fs/ext4/fast_commit.c | 86 ++++++++++++++++++++++++++++++-------
include/trace/events/ext4.h | 33 ++++++++++++++
2 files changed, 104 insertions(+), 15 deletions(-)
diff --git a/fs/ext4/fast_commit.c b/fs/ext4/fast_commit.c
index d1eefee60912..d266eb2a4219 100644
--- a/fs/ext4/fast_commit.c
+++ b/fs/ext4/fast_commit.c
@@ -193,6 +193,27 @@ static struct kmem_cache *ext4_fc_range_cachep;
#define EXT4_FC_SNAPSHOT_MAX_INODES 1024
#define EXT4_FC_SNAPSHOT_MAX_RANGES 2048
+/*
+ * Snapshot failure reasons for ext4_fc_lock_updates tracepoint.
+ * Keep these stable for tooling.
+ */
+enum ext4_fc_snap_err {
+ EXT4_FC_SNAP_ERR_NONE = 0,
+ EXT4_FC_SNAP_ERR_ES_MISS,
+ EXT4_FC_SNAP_ERR_ES_DELAYED,
+ EXT4_FC_SNAP_ERR_ES_OTHER,
+ EXT4_FC_SNAP_ERR_INODES_CAP,
+ EXT4_FC_SNAP_ERR_RANGES_CAP,
+ EXT4_FC_SNAP_ERR_NOMEM,
+ EXT4_FC_SNAP_ERR_INODE_LOC,
+};
+
+static inline void ext4_fc_set_snap_err(int *snap_err, int err)
+{
+ if (snap_err && *snap_err == EXT4_FC_SNAP_ERR_NONE)
+ *snap_err = err;
+}
+
static void ext4_end_buffer_io_sync(struct buffer_head *bh, int uptodate)
{
BUFFER_TRACE(bh, "");
@@ -983,11 +1004,12 @@ static void ext4_fc_free_inode_snap(struct inode *inode)
static int ext4_fc_snapshot_inode_data(struct inode *inode,
struct list_head *ranges,
unsigned int nr_ranges_total,
- unsigned int *nr_rangesp)
+ unsigned int *nr_rangesp,
+ int *snap_err)
{
struct ext4_inode_info *ei = EXT4_I(inode);
- unsigned int nr_ranges = 0;
ext4_lblk_t start_lblk, end_lblk, cur_lblk;
+ unsigned int nr_ranges = 0;
spin_lock(&ei->i_fc_lock);
if (ei->i_fc_lblk_len == 0) {
@@ -1010,11 +1032,16 @@ static int ext4_fc_snapshot_inode_data(struct inode *inode,
struct ext4_fc_range *range;
ext4_lblk_t len;
- if (!ext4_es_lookup_extent(inode, cur_lblk, NULL, &es, NULL))
+ if (!ext4_es_lookup_extent(inode, cur_lblk, NULL, &es, NULL)) {
+ ext4_fc_set_snap_err(snap_err, EXT4_FC_SNAP_ERR_ES_MISS);
return -EAGAIN;
+ }
- if (ext4_es_is_delayed(&es))
+ if (ext4_es_is_delayed(&es)) {
+ ext4_fc_set_snap_err(snap_err,
+ EXT4_FC_SNAP_ERR_ES_DELAYED);
return -EAGAIN;
+ }
len = es.es_len - (cur_lblk - es.es_lblk);
if (len > end_lblk - cur_lblk + 1)
@@ -1024,12 +1051,17 @@ static int ext4_fc_snapshot_inode_data(struct inode *inode,
continue;
}
- if (nr_ranges_total + nr_ranges >= EXT4_FC_SNAPSHOT_MAX_RANGES)
+ if (nr_ranges_total + nr_ranges >= EXT4_FC_SNAPSHOT_MAX_RANGES) {
+ ext4_fc_set_snap_err(snap_err,
+ EXT4_FC_SNAP_ERR_RANGES_CAP);
return -E2BIG;
+ }
range = kmem_cache_alloc(ext4_fc_range_cachep, GFP_NOFS);
- if (!range)
+ if (!range) {
+ ext4_fc_set_snap_err(snap_err, EXT4_FC_SNAP_ERR_NOMEM);
return -ENOMEM;
+ }
nr_ranges++;
range->lblk = cur_lblk;
@@ -1054,6 +1086,7 @@ static int ext4_fc_snapshot_inode_data(struct inode *inode,
range->len = max;
} else {
kmem_cache_free(ext4_fc_range_cachep, range);
+ ext4_fc_set_snap_err(snap_err, EXT4_FC_SNAP_ERR_ES_OTHER);
return -EAGAIN;
}
@@ -1070,7 +1103,7 @@ static int ext4_fc_snapshot_inode_data(struct inode *inode,
static int ext4_fc_snapshot_inode(struct inode *inode,
unsigned int nr_ranges_total,
- unsigned int *nr_rangesp)
+ unsigned int *nr_rangesp, int *snap_err)
{
struct ext4_inode_info *ei = EXT4_I(inode);
struct ext4_fc_inode_snap *snap;
@@ -1082,8 +1115,10 @@ static int ext4_fc_snapshot_inode(struct inode *inode,
int alloc_ctx;
ret = ext4_get_inode_loc_noio(inode, &iloc);
- if (ret)
+ if (ret) {
+ ext4_fc_set_snap_err(snap_err, EXT4_FC_SNAP_ERR_INODE_LOC);
return ret;
+ }
if (ext4_test_inode_flag(inode, EXT4_INODE_INLINE_DATA))
inode_len = EXT4_INODE_SIZE(inode->i_sb);
@@ -1092,6 +1127,7 @@ static int ext4_fc_snapshot_inode(struct inode *inode,
snap = kmalloc(struct_size(snap, inode_buf, inode_len), GFP_NOFS);
if (!snap) {
+ ext4_fc_set_snap_err(snap_err, EXT4_FC_SNAP_ERR_NOMEM);
brelse(iloc.bh);
return -ENOMEM;
}
@@ -1102,7 +1138,7 @@ static int ext4_fc_snapshot_inode(struct inode *inode,
brelse(iloc.bh);
ret = ext4_fc_snapshot_inode_data(inode, &ranges, nr_ranges_total,
- &nr_ranges);
+ &nr_ranges, snap_err);
if (ret) {
kfree(snap);
ext4_fc_free_ranges(&ranges);
@@ -1203,7 +1239,10 @@ static int ext4_fc_alloc_snapshot_inodes(struct super_block *sb,
unsigned int *nr_inodesp);
static int ext4_fc_snapshot_inodes(journal_t *journal, struct inode **inodes,
- unsigned int inodes_size)
+ unsigned int inodes_size,
+ unsigned int *nr_inodesp,
+ unsigned int *nr_rangesp,
+ int *snap_err)
{
struct super_block *sb = journal->j_private;
struct ext4_sb_info *sbi = EXT4_SB(sb);
@@ -1221,6 +1260,8 @@ static int ext4_fc_snapshot_inodes(journal_t *journal, struct inode **inodes,
alloc_ctx = ext4_fc_lock(sb);
list_for_each_entry(iter, &sbi->s_fc_q[FC_Q_MAIN], i_fc_list) {
if (i >= inodes_size) {
+ ext4_fc_set_snap_err(snap_err,
+ EXT4_FC_SNAP_ERR_INODES_CAP);
ret = -E2BIG;
goto unlock;
}
@@ -1244,6 +1285,8 @@ static int ext4_fc_snapshot_inodes(journal_t *journal, struct inode **inodes,
continue;
if (i >= inodes_size) {
+ ext4_fc_set_snap_err(snap_err,
+ EXT4_FC_SNAP_ERR_INODES_CAP);
ret = -E2BIG;
goto unlock;
}
@@ -1268,16 +1311,20 @@ static int ext4_fc_snapshot_inodes(journal_t *journal, struct inode **inodes,
unsigned int inode_ranges = 0;
ret = ext4_fc_snapshot_inode(inodes[idx], nr_ranges,
- &inode_ranges);
+ &inode_ranges, snap_err);
if (ret)
break;
nr_ranges += inode_ranges;
}
+ if (nr_inodesp)
+ *nr_inodesp = i;
+ if (nr_rangesp)
+ *nr_rangesp = nr_ranges;
return ret;
}
-static int ext4_fc_perform_commit(journal_t *journal)
+static int ext4_fc_perform_commit(journal_t *journal, tid_t commit_tid)
{
struct super_block *sb = journal->j_private;
struct ext4_sb_info *sbi = EXT4_SB(sb);
@@ -1286,10 +1333,15 @@ static int ext4_fc_perform_commit(journal_t *journal)
struct inode *inode;
struct inode **inodes;
unsigned int inodes_size;
+ unsigned int snap_inodes = 0;
+ unsigned int snap_ranges = 0;
+ int snap_err = EXT4_FC_SNAP_ERR_NONE;
struct blk_plug plug;
int ret = 0;
u32 crc = 0;
int alloc_ctx;
+ ktime_t lock_start;
+ u64 locked_ns;
/*
* Step 1: Mark all inodes on s_fc_q[MAIN] with
@@ -1337,13 +1389,13 @@ static int ext4_fc_perform_commit(journal_t *journal)
if (ret)
return ret;
-
ret = ext4_fc_alloc_snapshot_inodes(sb, &inodes, &inodes_size);
if (ret)
return ret;
/* Step 4: Mark all inodes as being committed. */
jbd2_journal_lock_updates(journal);
+ lock_start = ktime_get();
/*
* The journal is now locked. No more handles can start and all the
* previous handles are now drained. Snapshotting happens in this
@@ -1357,8 +1409,12 @@ static int ext4_fc_perform_commit(journal_t *journal)
}
ext4_fc_unlock(sb, alloc_ctx);
- ret = ext4_fc_snapshot_inodes(journal, inodes, inodes_size);
+ ret = ext4_fc_snapshot_inodes(journal, inodes, inodes_size,
+ &snap_inodes, &snap_ranges, &snap_err);
jbd2_journal_unlock_updates(journal);
+ locked_ns = ktime_to_ns(ktime_sub(ktime_get(), lock_start));
+ trace_ext4_fc_lock_updates(sb, commit_tid, locked_ns, snap_inodes,
+ snap_ranges, ret, snap_err);
kvfree(inodes);
if (ret)
return ret;
@@ -1563,7 +1619,7 @@ int ext4_fc_commit(journal_t *journal, tid_t commit_tid)
journal_ioprio = EXT4_DEF_JOURNAL_IOPRIO;
set_task_ioprio(current, journal_ioprio);
fc_bufs_before = (sbi->s_fc_bytes + bsize - 1) / bsize;
- ret = ext4_fc_perform_commit(journal);
+ ret = ext4_fc_perform_commit(journal, commit_tid);
if (ret < 0) {
if (ret == -EAGAIN || ret == -E2BIG || ret == -ECANCELED)
status = EXT4_FC_STATUS_INELIGIBLE;
diff --git a/include/trace/events/ext4.h b/include/trace/events/ext4.h
index fd76d14c2776..a1493971821d 100644
--- a/include/trace/events/ext4.h
+++ b/include/trace/events/ext4.h
@@ -2812,6 +2812,39 @@ TRACE_EVENT(ext4_fc_commit_stop,
__entry->num_fc_ineligible, __entry->nblks_agg, __entry->tid)
);
+TRACE_EVENT(ext4_fc_lock_updates,
+ TP_PROTO(struct super_block *sb, tid_t commit_tid, u64 locked_ns,
+ unsigned int nr_inodes, unsigned int nr_ranges, int err,
+ int snap_err),
+
+ TP_ARGS(sb, commit_tid, locked_ns, nr_inodes, nr_ranges, err, snap_err),
+
+ TP_STRUCT__entry(/* entry */
+ __field(dev_t, dev)
+ __field(tid_t, tid)
+ __field(u64, locked_ns)
+ __field(unsigned int, nr_inodes)
+ __field(unsigned int, nr_ranges)
+ __field(int, err)
+ __field(int, snap_err)
+ ),
+
+ TP_fast_assign(/* assign */
+ __entry->dev = sb->s_dev;
+ __entry->tid = commit_tid;
+ __entry->locked_ns = locked_ns;
+ __entry->nr_inodes = nr_inodes;
+ __entry->nr_ranges = nr_ranges;
+ __entry->err = err;
+ __entry->snap_err = snap_err;
+ ),
+
+ TP_printk("dev %d,%d tid %u locked_ns %llu nr_inodes %u nr_ranges %u err %d snap_err %d",
+ MAJOR(__entry->dev), MINOR(__entry->dev), __entry->tid,
+ __entry->locked_ns, __entry->nr_inodes, __entry->nr_ranges,
+ __entry->err, __entry->snap_err)
+);
+
#define FC_REASON_NAME_STAT(reason) \
show_fc_reason(reason), \
__entry->fc_ineligible_rc[reason]
--
2.52.0
^ permalink raw reply related
* Re: [PATCH 26/26] rv/rvgen: extract node marker string to class constant
From: Wander Lairson Costa @ 2026-01-20 11:34 UTC (permalink / raw)
To: Gabriele Monaco
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <0383d9a3fdaeb2b66e48a7857791bcbfe324958d.camel@redhat.com>
On Tue, Jan 20, 2026 at 10:03:20AM +0100, Gabriele Monaco wrote:
> On Mon, 2026-01-19 at 17:46 -0300, Wander Lairson Costa wrote:
> > Add a node_marker class constant to the Automata class to replace the
> > hardcoded "{node" string literal used throughout the DOT file parsing
> > logic. This follows the existing pattern established by the init_marker
> > and invalid_state_str class constants in the same class.
> >
> > The "{node" string is used as a marker to identify node declaration
> > lines in DOT files during state variable extraction and cursor
> > positioning. Extracting it to a named constant improves code
> > maintainability and makes the marker's purpose explicit.
> >
> > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
>
> Looks fine for me, thanks!
>
> I wonder if we could merge this patch with 15/26 that is introducing a very
> similar change on init_marker.
The idea was to make each patch doing one thing to make the reviewer's
life easier (I think I broke my own rule in a couple of patch). But if
there is a strong feeling about the merge, I could merged them in a
possible v2 patch series.
>
> Anyway:
>
> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
>
> > ---
> > tools/verification/rvgen/rvgen/automata.py | 9 +++++----
> > 1 file changed, 5 insertions(+), 4 deletions(-)
> >
> > diff --git a/tools/verification/rvgen/rvgen/automata.py
> > b/tools/verification/rvgen/rvgen/automata.py
> > index a6889d0c26c3f..5f23db1855cd3 100644
> > --- a/tools/verification/rvgen/rvgen/automata.py
> > +++ b/tools/verification/rvgen/rvgen/automata.py
> > @@ -29,6 +29,7 @@ class Automata:
> >
> > invalid_state_str = "INVALID_STATE"
> > init_marker = "__init_"
> > + node_marker = "{node"
> >
> > def __init__(self, file_path, model_name=None):
> > self.__dot_path = file_path
> > @@ -76,7 +77,7 @@ class Automata:
> > for cursor, line in enumerate(self.__dot_lines):
> > split_line = line.split()
> >
> > - if len(split_line) and split_line[0] == "{node":
> > + if len(split_line) and split_line[0] == self.node_marker:
> > return cursor
> >
> > raise AutomataError("Could not find a beginning state")
> > @@ -91,9 +92,9 @@ class Automata:
> > continue
> >
> > if state == 0:
> > - if line[0] == "{node":
> > + if line[0] == self.node_marker:
> > state = 1
> > - elif line[0] != "{node":
> > + elif line[0] != self.node_marker:
> > break
> > else:
> > raise AutomataError("Could not find beginning event")
> > @@ -116,7 +117,7 @@ class Automata:
> > # process nodes
> > for line in islice(self.__dot_lines, cursor, None):
> > split_line = line.split()
> > - if not split_line or split_line[0] != "{node":
> > + if not split_line or split_line[0] != self.node_marker:
> > break
> >
> > raw_state = split_line[-1]
^ permalink raw reply
* Re: [PATCH 17/26] rv/rvgen: fix possibly unbound variable in ltl2k
From: Wander Lairson Costa @ 2026-01-20 11:37 UTC (permalink / raw)
To: Gabriele Monaco
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <b8a2b88e484cac27a82e1c27d0e27599515c4bc6.camel@redhat.com>
On Tue, Jan 20, 2026 at 09:59:11AM +0100, Gabriele Monaco wrote:
> On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> > Initialize loop variable `i` before the for loop in abbreviate_atoms
> > function to fix pyright static type checker error. The previous code
> > left `i` potentially unbound in edge cases where the range could be
> > empty, though this would not occur in practice since the loop always
> > executes at least once with the given range parameters.
> >
> > The initialization to zero ensures that `i` has a defined value before
> > entering the loop scope, satisfying static analysis requirements
> > while preserving the existing logic. The for loop immediately assigns
> > i to the first value from the range, so the initialization value is
> > never actually used in normal execution paths.
> >
> > This change resolves the pyright reportPossiblyUnbound error without
> > altering the function's behavior or performance characteristics.
>
> So are we just pleasing the tool or is there a real implication of this?
>
> Apparently code like
>
> for i in range(len([]), -1, -1):
> pass
> print(i)
>
> works just fine since range() returns at least 0 (as you mentioned in the commit
> message) and i is not used before assignation in the loop, so I don't really see
> a problem.
>
> Apparently pyright devs don't want ([1]) to implement a logic to sort out the
> /possibly/ unbound error here.
>
> From what I understand, this code is already not pythonic, so rather than
> silence the warning to please this tool I'd just refactor the code not to use i
> after the loop (or leave it as it is, since it works fine).
>
> What do you think?
You're right, I could have done:
for atom in reversed(atoms): ...
I will modify it in v2.
>
> Thanks,
> Gabriele
>
> [1] - https://github.com/microsoft/pyright/issues/844
>
> >
> > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> > ---
> > tools/verification/rvgen/rvgen/ltl2k.py | 1 +
> > 1 file changed, 1 insertion(+)
> >
> > diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> > b/tools/verification/rvgen/rvgen/ltl2k.py
> > index fa9ea6d597095..94dc64af1716d 100644
> > --- a/tools/verification/rvgen/rvgen/ltl2k.py
> > +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> > @@ -45,6 +45,7 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
> >
> > abbrs = []
> > for atom in atoms:
> > + i = 0
> > for i in range(len(atom), -1, -1):
> > if sum(a.startswith(atom[:i]) for a in atoms) > 1:
> > break
>
^ permalink raw reply
* Re: [PATCH 16/26] rv/rvgen: fix unbound initial_state variable
From: Wander Lairson Costa @ 2026-01-20 11:42 UTC (permalink / raw)
To: Gabriele Monaco
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <7d37e29989e08e62a419f2ae8000ed7ec1913713.camel@redhat.com>
On Tue, Jan 20, 2026 at 09:21:01AM +0100, Gabriele Monaco wrote:
> On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
>
>
> [...]
> > diff --git a/tools/verification/rvgen/rvgen/automata.py
> > b/tools/verification/rvgen/rvgen/automata.py
> > index 8548265955570..083d0f5cfb773 100644
> > --- a/tools/verification/rvgen/rvgen/automata.py
> > +++ b/tools/verification/rvgen/rvgen/automata.py
> > @@ -10,6 +10,7 @@
> >
> > import ntpath
> >
> > +
> > class AutomataError(OSError):
> > """Exception raised for errors in automata parsing and validation.
> >
> > @@ -17,6 +18,7 @@ class AutomataError(OSError):
> > or malformed automaton definitions.
> > """
> >
> > +
>
> I believe these newlines were added automatically by some tools, not sure if we
> really want them but they don't belong in this patch (since 1/26 added this
> class).
>
There are python formatting tools that put 2 lines after a type
definition. Anyway, I can remove it in v2.
> > class Automata:
> > """Automata class: Reads a dot file and parses it as an automata.
> >
> > @@ -31,7 +33,9 @@ class Automata:
> > self.__dot_path = file_path
> > self.name = model_name or self.__get_model_name()
> > self.__dot_lines = self.__open_dot()
> > - self.states, self.initial_state, self.final_states =
> > self.__get_state_variables()
> > + self.states, self.initial_state, self.final_states = (
> > + self.__get_state_variables()
> > + )
>
> There is no strict 80 character limit for python code and I personally find this
> less readable. Is this again what the tool suggested?
>
In general, 100 lines is assumed the to a good limit. Anyway, this is
minor and I can remove the change in v2 if desired.
> > self.events = self.__get_event_variables()
> > self.function = self.__create_matrix()
> > self.events_start, self.events_start_run = self.__store_init_events()
> > @@ -86,6 +90,7 @@ class Automata:
> > # wait for node declaration
> > states = []
> > final_states = []
> > + initial_state = None
> >
> > has_final_states = False
> > cursor = self.__get_cursor_begin_states()
> > @@ -96,9 +101,9 @@ class Automata:
> > raw_state = line[-1]
> >
> > # "enabled_fired"}; -> enabled_fired
> > - state = raw_state.replace('"', '').replace('};', '').replace(',',
> > '_')
> > + state = raw_state.replace('"', "").replace("};", "").replace(",",
> > "_")
>
> Ok this change is good.
>
> > if state.startswith(self.init_marker):
> > - initial_state = state[len(self.init_marker):]
> > + initial_state = state[len(self.init_marker) :]
>
> You fixed spacing in 12/26. We could either keep move this change there or just
> merge that patch with others touching the same files.
>
Np, I can move this change to there.
> > else:
> > states.append(state)
> > if "doublecircle" in self.__dot_lines[cursor]:
> > @@ -111,6 +116,9 @@ class Automata:
> >
> > cursor += 1
> >
> > + if initial_state is None:
> > + raise AutomataError("The automaton doesn't have a initial state")
> > +
>
> Yeah that's needed.
>
> > states = sorted(set(states))
> >
> > # Insert the initial state at the beginning of the states
> > @@ -132,7 +140,7 @@ class Automata:
> > # ------------ event is here ------------^^^^^
> > if self.__dot_lines[cursor].split()[1] == "->":
> > line = self.__dot_lines[cursor].split()
> > - event = line[-2].replace('"', '')
> > + event = line[-2].replace('"', "")
> >
> > # when a transition has more than one labels, they are like
> > this
> > # "local_irq_enable\nhw_local_irq_enable_n"
> > @@ -162,7 +170,9 @@ class Automata:
> > nr_state += 1
> >
> > # declare the matrix....
> > - matrix = [[self.invalid_state_str for x in range(nr_event)] for y in
> > range(nr_state)]
> > + matrix = [
> > + [self.invalid_state_str for x in range(nr_event)] for y in
> > range(nr_state)
> > + ]
> >
> > # and we are back! Let's fill the matrix
> > cursor = self.__get_cursor_begin_events()
> > @@ -170,9 +180,9 @@ class Automata:
> > while self.__dot_lines[cursor].lstrip()[0] == '"':
> > if self.__dot_lines[cursor].split()[1] == "->":
> > line = self.__dot_lines[cursor].split()
> > - origin_state = line[0].replace('"', '').replace(',', '_')
> > - dest_state = line[2].replace('"', '').replace(',', '_')
> > - possible_events = line[-2].replace('"', '').replace("\\n", "
> > ")
> > + origin_state = line[0].replace('"', "").replace(",", "_")
> > + dest_state = line[2].replace('"', "").replace(",", "_")
> > + possible_events = line[-2].replace('"', "").replace("\\n", "
> > ")
>
> All in all looks good, thanks.
>
> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
>
> > for event in possible_events.split():
> > matrix[states_dict[origin_state]][events_dict[event]] =
> > dest_state
> > cursor += 1
^ permalink raw reply
* Re: [PATCH 16/26] rv/rvgen: fix unbound initial_state variable
From: Gabriele Monaco @ 2026-01-20 11:53 UTC (permalink / raw)
To: Wander Lairson Costa
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <aW9o_lSOvSdME6MP@fedora>
On Tue, 2026-01-20 at 08:42 -0300, Wander Lairson Costa wrote:
> On Tue, Jan 20, 2026 at 09:21:01AM +0100, Gabriele Monaco wrote:
>
> >
> > I believe these newlines were added automatically by some tools, not sure if
> > we
> > really want them but they don't belong in this patch (since 1/26 added this
> > class).
> >
> There are python formatting tools that put 2 lines after a type
> definition. Anyway, I can remove it in v2.
If that's common practice I'm fine keeping it, I just would create this class
directly with the newlines separators in 1/26 instead of adding these lines
later in the same series. Just to reduce the noise.
>
> > > class Automata:
> > > """Automata class: Reads a dot file and parses it as an automata.
> > >
> > > @@ -31,7 +33,9 @@ class Automata:
> > > self.__dot_path = file_path
> > > self.name = model_name or self.__get_model_name()
> > > self.__dot_lines = self.__open_dot()
> > > - self.states, self.initial_state, self.final_states =
> > > self.__get_state_variables()
> > > + self.states, self.initial_state, self.final_states = (
> > > + self.__get_state_variables()
> > > + )
> >
> > There is no strict 80 character limit for python code and I personally find
> > this
> > less readable. Is this again what the tool suggested?
> >
>
> In general, 100 lines is assumed the to a good limit. Anyway, this is
> minor and I can remove the change in v2 if desired.
Yeah 100 is probably also what checkpatch.pl uses (although I think it skips
python files), since this is below 90 columns, I wouldn't touch it.
Thanks,
Gabriele
>
> > > self.events = self.__get_event_variables()
> > > self.function = self.__create_matrix()
> > > self.events_start, self.events_start_run =
> > > self.__store_init_events()
> > > @@ -86,6 +90,7 @@ class Automata:
> > > # wait for node declaration
> > > states = []
> > > final_states = []
> > > + initial_state = None
> > >
> > > has_final_states = False
> > > cursor = self.__get_cursor_begin_states()
> > > @@ -96,9 +101,9 @@ class Automata:
> > > raw_state = line[-1]
> > >
> > > # "enabled_fired"}; -> enabled_fired
> > > - state = raw_state.replace('"', '').replace('};',
> > > '').replace(',',
> > > '_')
> > > + state = raw_state.replace('"', "").replace("};",
> > > "").replace(",",
> > > "_")
> >
> > Ok this change is good.
> >
> > > if state.startswith(self.init_marker):
> > > - initial_state = state[len(self.init_marker):]
> > > + initial_state = state[len(self.init_marker) :]
> >
> > You fixed spacing in 12/26. We could either keep move this change there or
> > just
> > merge that patch with others touching the same files.
> >
>
> Np, I can move this change to there.
>
> > > else:
> > > states.append(state)
> > > if "doublecircle" in self.__dot_lines[cursor]:
> > > @@ -111,6 +116,9 @@ class Automata:
> > >
> > > cursor += 1
> > >
> > > + if initial_state is None:
> > > + raise AutomataError("The automaton doesn't have a initial
> > > state")
> > > +
> >
> > Yeah that's needed.
> >
> > > states = sorted(set(states))
> > >
> > > # Insert the initial state at the beginning of the states
> > > @@ -132,7 +140,7 @@ class Automata:
> > > # ------------ event is here ------------^^^^^
> > > if self.__dot_lines[cursor].split()[1] == "->":
> > > line = self.__dot_lines[cursor].split()
> > > - event = line[-2].replace('"', '')
> > > + event = line[-2].replace('"', "")
> > >
> > > # when a transition has more than one labels, they are
> > > like
> > > this
> > > # "local_irq_enable\nhw_local_irq_enable_n"
> > > @@ -162,7 +170,9 @@ class Automata:
> > > nr_state += 1
> > >
> > > # declare the matrix....
> > > - matrix = [[self.invalid_state_str for x in range(nr_event)] for y
> > > in
> > > range(nr_state)]
> > > + matrix = [
> > > + [self.invalid_state_str for x in range(nr_event)] for y in
> > > range(nr_state)
> > > + ]
> > >
> > > # and we are back! Let's fill the matrix
> > > cursor = self.__get_cursor_begin_events()
> > > @@ -170,9 +180,9 @@ class Automata:
> > > while self.__dot_lines[cursor].lstrip()[0] == '"':
> > > if self.__dot_lines[cursor].split()[1] == "->":
> > > line = self.__dot_lines[cursor].split()
> > > - origin_state = line[0].replace('"', '').replace(',', '_')
> > > - dest_state = line[2].replace('"', '').replace(',', '_')
> > > - possible_events = line[-2].replace('"',
> > > '').replace("\\n", "
> > > ")
> > > + origin_state = line[0].replace('"', "").replace(",", "_")
> > > + dest_state = line[2].replace('"', "").replace(",", "_")
> > > + possible_events = line[-2].replace('"',
> > > "").replace("\\n", "
> > > ")
> >
> > All in all looks good, thanks.
> >
> > Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> >
> > > for event in possible_events.split():
> > > matrix[states_dict[origin_state]][events_dict[event]]
> > > =
> > > dest_state
> > > cursor += 1
^ permalink raw reply
* Re: [PATCH 14/26] rv/rvgen: remove redundant initial_state removal
From: Wander Lairson Costa @ 2026-01-20 12:05 UTC (permalink / raw)
To: Gabriele Monaco
Cc: Steven Rostedt, Nam Cao, open list,
open list:RUNTIME VERIFICATION (RV)
In-Reply-To: <63e032341807f9ece73937d5e20eee9e3162fb61.camel@redhat.com>
On Tue, Jan 20, 2026 at 09:01:01AM +0100, Gabriele Monaco wrote:
> On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> > Remove an unnecessary and incorrect list removal operation in the
> > automata state variable processing. The code attempted to remove
> > initial_state from the states list, but this element was never
> > added to the list in the first place. States with the __init_
> > prefix are explicitly excluded from the states list during the
> > parsing loop, with only the initial_state variable being set
> > from them.
>
> The initial state is not the state with __init_, but the state pointed to by
> that, the purpose of removing it after sorting and putting it back is for it to
> be the first (we may argue there are better ways to do that, but it works).
>
> After this change, the initial state is duplicated..
> I think we should just drop this.
Ah, now I understood the reasoning, thanks. I will drop the patch.
>
> Thanks,
> Gabriele
>
> >
> > Calling remove() on an element that does not exist in a list
> > raises a ValueError. This code would have failed during execution
> > when processing any DOT file containing an initial state marker.
> > The subsequent insert operation at index 0 correctly adds the
> > initial_state to the beginning of the states list, making the
> > removal operation both incorrect and redundant.
> >
> > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> > ---
> > tools/verification/rvgen/rvgen/automata.py | 1 -
> > 1 file changed, 1 deletion(-)
> >
> > diff --git a/tools/verification/rvgen/rvgen/automata.py
> > b/tools/verification/rvgen/rvgen/automata.py
> > index 7841a6e70bad2..b302af3e5133e 100644
> > --- a/tools/verification/rvgen/rvgen/automata.py
> > +++ b/tools/verification/rvgen/rvgen/automata.py
> > @@ -111,7 +111,6 @@ class Automata:
> > cursor += 1
> >
> > states = sorted(set(states))
> > - states.remove(initial_state)
> >
> > # Insert the initial state at the beginning of the states
> > states.insert(0, initial_state)
>
^ 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