* Re: [PATCH v8 2/6] mm/memory-failure: surface unhandlable kernel pages as -ENOTRECOVERABLE
From: Breno Leitao @ 2026-06-08 14:15 UTC (permalink / raw)
To: David Hildenbrand (Arm)
Cc: Miaohe Lin, linux-mm, linux-kernel, linux-doc, linux-kselftest,
linux-trace-kernel, kernel-team, Lance Yang, Andrew Morton,
Lorenzo Stoakes, Vlastimil Babka, Mike Rapoport,
Suren Baghdasaryan, Michal Hocko, Shuah Khan, Naoya Horiguchi,
Steven Rostedt, Masami Hiramatsu, Mathieu Desnoyers,
Jonathan Corbet, Shuah Khan, Liam R. Howlett
In-Reply-To: <f1a742be-80cb-4256-b1f9-e50a0f83cb15@kernel.org>
On Fri, Jun 05, 2026 at 11:42:53AM +0200, David Hildenbrand (Arm) wrote:
> On 6/5/26 11:35, Breno Leitao wrote:
> > On Wed, Jun 03, 2026 at 10:33:04AM +0800, Miaohe Lin wrote:
> >> On 2026/6/2 17:41, David Hildenbrand (Arm) wrote:
> >>>
> >>> Races are fine. We might miss some pages, but that can happen on races either way.
> >>>
> >>>
> >>> I'd just do something like
> >>>
> >>> if (PageReserved(page))
> >>> return true;
> >>>
> >>> head = compound_head(page);
> >>
> >> If @head is split just after compound_head. And then @head is freed into buddy and re-allocated as slab
> >> page while @page is still in the buddy. We would panic on this scene as @head is PageSlab. But we were
> >> supposed to successfully handle @page. Or am I miss something?
> >
> > You're right that it is racy, but I think it is an acceptable race here.
> >
>
> I mean, any such races can currently already happen one way or the other?
>
> Really, the only way to not get races is to tryget the (compound)page,
> revalidate that the page is still part of the compound page.
>
> I'm not sure if that's really a good idea.
>
> But my memory is a bit vague in which scenarios we already hold a page reference
> here to prevent any concurrent freeing?
No, we don't hold one here in the case that matters.
HWPoisonKernelOwned() runs at the very top of get_any_page(), before
try_again: and before __get_hwpoison_page(). The first refcount taken in
the whole path is the folio_try_get() inside __get_hwpoison_page(), which
runs *after* the short-circuit.
So get_any_page() itself never holds a reference at the check -- the only way
one exists is if the caller passed MF_COUNT_INCREASED (count_increased ==
true).
So on the MCE/GHES path -- the one this panic option exists for -- no
reference is held when HWPoisonKernelOwned() does its compound_head() +
PageSlab()/PageTable()/PageLargeKmalloc() checks.
Given that, I'd rather keep it racy and take no refcount than add a
tryget + revalidate purely for this check. As I've said earleir, an operator
who enabled it has chosen to crash rather than run on corrupted memory;
mis-attributing one such rare, genuinely-poisoned page is within that contract.
^ permalink raw reply
* Re: [PATCH] rethook: Use tsk->on_cpu to check task execution state
From: Peter Zijlstra @ 2026-06-08 14:06 UTC (permalink / raw)
To: Masami Hiramatsu
Cc: bpf, Tengda Wu, Steven Rostedt, Mathieu Desnoyers,
Alexei Starovoitov, linux-trace-kernel, linux-kernel,
Josh Poimboeuf, jikos, mbenes, pmladek
In-Reply-To: <20260608220811.d4a0b58961cfb9eeb6bbbccb@kernel.org>
On Mon, Jun 08, 2026 at 10:08:11PM +0900, Masami Hiramatsu wrote:
> > > Anyway, I'm wondering what the purpose of this check here is, there is
> > > no real comment, and commit 5120d167e21c ("rethook: Remove warning
> > > messages printed for finding return address of a frame.") is just pure
> > > voodoo as well.
> >
> > FWIW, you should have had this discussion then.
>
> Indeed. The rethook is making a shadow stack by list, thus caller must
> guarantee the target process is blocked at least during this function.
>
> The commit messages suggest that when BPF takes a backtrace, it also
> includes other running tasks. Is that safe?
Well, you get to keep the pieces. At this point safe only pertains to
'doesn't-crash', all correctness is out the window.
I always forget the crazy BPF does ;-)
> > > Also, note the comment that goes with the usage of
> > > task_on_another_cpu(); that thing is racy as all heck.
> > >
> > > So it really comes down to what the purpose of this check is.
>
> This check has been introduced when it is copied from
> kretprobe_find_ret_addr(). It has the comment:
>
> * The @tsk must be 'current' or a task which is not running. @fp is a hint
>
> IIRC, I added this check to explicitly verify this condition.
Right, but it is a prescriptive comment, not an explanatory one. That
is, it doesn't explain the condition.
> > > I suspect the issue at hand is that tsk->rethook elements, such as
> > > iterated by __rethook_find_ret_addr() are not safe to be accessed for a
> > > running task.
> > >
> > > Notably while rethook_recycle() has some RCU thing on, that objpool
> > > thing (and the recycle name itself) seems to strongly suggest iterating
> > > these things is not sound (you could start with things from this task,
> > > hit a recycled entry and continue iterating rethooks from another task).
> > >
> > > Also note that the current check is also racy, nothing really prevents a
> > > wakeup from happening right after you observe task_is_running() being
> > > false. The task can then get scheduled in on another CPU and tear down
> > > its rethooks concurrent with __rethook_find_ret_addr().
>
> Yeah, but is there any way to ensure the task is blocked? Even if it is
> blocked, like TASK_UNINTERRUPTIBLE, unless holding the actual lock in
> the rethook, it may not be possible to ensure it?
>
> Of course, we could give up on checking within this function and leave
> everything to the caller to guarantee - as kretprobe does.
>
> BTW, the reason why we made it possible to pass tasks other than current
> is that the stack unwinding code itself supported unwinding tasks other
> than current, so we had no choice but to create this interface.
>
> However, it is a bad idea to check this in deep inside of unwinding.
This, you cannot take locks in unwinding. The only thing you can do is
try to do the best you can without crashing.
Typically unwind only happens on self -- this is natural, a task crashes
and unwinds itself, or a task does something (takes a lock, hits a
tracepoint, etc) and takes a snapshot of its own stack, and this is
safe.
Things like live-patch use task_call_func(), which ensures the callback
function is done while holding sufficient locks for the task to not
change state.
^ permalink raw reply
* Re: [syzbot] [trace?] KASAN: use-after-free Write in ring_buffer_read_page
From: Yash Suthar @ 2026-06-08 14:01 UTC (permalink / raw)
To: linux-trace-kernel
Cc: linux-kernel, rostedt, mhiramat, glider, nogikh,
mathieu.desnoyers, syzkaller-bugs, syzbot+2dd9d02f60775ce5c1fb
In-Reply-To: <CAG_fn=WVfi9=M8VjJQt8jCpXf-0D30-BQDCZZM+FX_0d8V+yhA@mail.gmail.com>
From syzbot initial report, I noticed that
ring_buffer_read_page() checks data_page->order against
buffer->subbuf_order , whereas in while
ring_buffer_subbuf_order_set() updates subbuf_size before
replacing the old pages. I think this allows reader to
use older spare page while observing a newer sub-buffer size.
That could explain the report (KASAN UAF, memset of 16308
bytes order 2 into an order 0 spare), while the AI
reproducer may hit a related race later in via copy_to_user()
tracing_buffers_read().
Before spending more time on a fix, does this sound
correct, or i am missing something in between?
Sincerely,
Yash Suthar
^ permalink raw reply
* Re: [PATCH] rethook: Use tsk->on_cpu to check task execution state
From: Masami Hiramatsu @ 2026-06-08 13:08 UTC (permalink / raw)
To: Peter Zijlstra, bpf
Cc: Tengda Wu, Masami Hiramatsu, Steven Rostedt, Mathieu Desnoyers,
Alexei Starovoitov, linux-trace-kernel, linux-kernel,
Josh Poimboeuf, jikos, mbenes, pmladek
In-Reply-To: <20260608102326.GB3161497@noisy.programming.kicks-ass.net>
On Mon, 8 Jun 2026 12:23:26 +0200
Peter Zijlstra <peterz@infradead.org> wrote:
> On Mon, Jun 08, 2026 at 11:34:49AM +0200, Peter Zijlstra wrote:
> >
> > +Live patching folks
> >
> > On Mon, Jun 08, 2026 at 09:52:37AM +0800, Tengda Wu wrote:
> >
> > > Background: We are verifying the support of live patches for functions that
> > > have a kretprobe. The specific verification method is as follows:
> > >
> > > We construct a function foo() that calls bar():
> > >
> > > void bar(void)
> > > {
> > > for (;;) {
> > > schedule();
> > > }
> > > }
> > >
> > > void foo(void)
> > > {
> > > bar();
> > > }
> > >
> > > A kretprobe is attached to bar():
> > >
> > > echo 'r:rp1 bar' > /sys/kernel/tracing/kprobe_events
> > > echo 1 > /sys/kernel/tracing/events/kprobes/rp1/enable
> > >
> > > Then foo() is triggered. The expected behavior is that bar() will call
> > > schedule() and yield the CPU.
> > >
> > > After that, the live patch is activated to attempt replacing the implementation
> > > of foo(). The expectation is that this should succeed.
> >
> > This wholly depends on how foo() calls bar(), if it is a normal call,
> > then no, it should not succeed, because foo() is still on the stack.
> >
> > If it is a tail-call, then yes, because foo() is no longer relevant.
> >
> > > However, in reality, because the task that called schedule() is still in the
> > > RUNNING state,
> >
> > So calling schedule() without setting state is dodgy in the first place.
> > Who is doing this? All wait primitives will set this to
> > TASK_UNINTERRUPTIBLE or something along those lines.
> >
> > > the condition task_is_running(tsk) inside rethook_find_ret_addr()
> > > is not satisfied, causing the function to return early. This, in turn,
> > > prevents stack_trace_save_tsk_reliable() from determining the stack as
> > > reliable, leading to a failure in activating the live patch.
> > >
> > > **Not sure if this is correct:**
> > >
> > > We believe that after a task voluntarily calls schedule(), when the stack
> > > is expected to be reliable, it is a safe time to activate a live patch.
> >
> > Calling schedule() without setting state is a no-op and really shouldn't
> > count much at all.
> >
> > > Additionally, a similar tsk->on_cpu check can be found elsewhere in the
> > > kernel (See task_on_another_cpu() in arch/x86/include/asm/unwind.h).
> > > Therefore, we propose changing the task_is_running(tsk) condition to
> > > tsk->on_cpu.
> >
> > Anyway, I'm wondering what the purpose of this check here is, there is
> > no real comment, and commit 5120d167e21c ("rethook: Remove warning
> > messages printed for finding return address of a frame.") is just pure
> > voodoo as well.
>
> FWIW, you should have had this discussion then.
Indeed. The rethook is making a shadow stack by list, thus caller must
guarantee the target process is blocked at least during this function.
The commit messages suggest that when BPF takes a backtrace, it also
includes other running tasks. Is that safe?
>
> > Also, note the comment that goes with the usage of
> > task_on_another_cpu(); that thing is racy as all heck.
> >
> > So it really comes down to what the purpose of this check is.
This check has been introduced when it is copied from
kretprobe_find_ret_addr(). It has the comment:
* The @tsk must be 'current' or a task which is not running. @fp is a hint
IIRC, I added this check to explicitly verify this condition.
> >
> > I suspect the issue at hand is that tsk->rethook elements, such as
> > iterated by __rethook_find_ret_addr() are not safe to be accessed for a
> > running task.
> >
> > Notably while rethook_recycle() has some RCU thing on, that objpool
> > thing (and the recycle name itself) seems to strongly suggest iterating
> > these things is not sound (you could start with things from this task,
> > hit a recycled entry and continue iterating rethooks from another task).
> >
> > Also note that the current check is also racy, nothing really prevents a
> > wakeup from happening right after you observe task_is_running() being
> > false. The task can then get scheduled in on another CPU and tear down
> > its rethooks concurrent with __rethook_find_ret_addr().
Yeah, but is there any way to ensure the task is blocked? Even if it is
blocked, like TASK_UNINTERRUPTIBLE, unless holding the actual lock in
the rethook, it may not be possible to ensure it?
Of course, we could give up on checking within this function and leave
everything to the caller to guarantee - as kretprobe does.
BTW, the reason why we made it possible to pass tasks other than current
is that the stack unwinding code itself supported unwinding tasks other
than current, so we had no choice but to create this interface.
However, it is a bad idea to check this in deep inside of unwinding.
> > Now, livepatch itself calls unwind from a proper context, but unwinds in
> > general are not. This rethook stuff doesn't seem to be sound in general.
>
> I suspect just entirely removing the check is the sanest option at this
> point. Callers that do it right (livepatch) are guaranteed consistent
> data, and the rest gets whatever pieces.
Agreed.
>
> Notably, unwind_next() holds rcu, so the iteration is protected from any
> of those rethook_node things getting freed. Its just that the iteration
> can go sideways and you might not get a sane answer.
>
> The very worst possible option is getting stuck in an infinite loop when
> concurrent with agressive rethook re-use or something daft like that,
> but that seems extremely unlikely.
OK, thanks for your review!
Tengda, can you send a patch to just remove the check?
Thank you,
--
Masami Hiramatsu (Google) <mhiramat@kernel.org>
^ permalink raw reply
* Re: [PATCH] mm/memory-failure: trace: change memory_failure_event to ras subsystem
From: Lance Yang @ 2026-06-08 12:14 UTC (permalink / raw)
To: xieyuanbin1
Cc: david, qiuxu.zhuo, bp, akpm, rostedt, linmiaohe, nao.horiguchi,
mhiramat, mchehab+huawei, tony.luck, yi1.lai, linux-edac,
linux-kernel, linux-mm, linux-trace-kernel, torvalds, lilinjie8,
liaohua4, Lance Yang
In-Reply-To: <20260605081213.154660-1-xieyuanbin1@huawei.com>
On Fri, Jun 05, 2026 at 04:12:13PM +0800, Xie Yuanbin wrote:
>For historical version, commit 97f0b1345219 ("tracing: add trace event
>for memory-failure") introduced memory_failure_event in ras subsystem.
>commit 31807483d395 ("mm/memory-failure: remove the selection of RAS")
>changed memory_failure_event to memory_failure subsystem. This breaks
>the backward compatibility, some user programs rely on it.
>
>Change memory_failure_event to ras subsystem to keep backward
>compatibility.
>
>Fixes: 31807483d395 ("mm/memory-failure: remove the selection of RAS")
>
>Reported-by: Yi Lai <yi1.lai@intel.com>
>Reported-by: Qiuxu Zhuo <qiuxu.zhuo@intel.com>
>Closes: https://lore.kernel.org/linux-mm/CY8PR11MB7134346A3E4BB28ECA28D6E989132@CY8PR11MB7134.namprd11.prod.outlook.com
>Cc: David Hildenbrand <david@kernel.org>
>Cc: Steven Rostedt <rostedt@goodmis.org>
>Cc: Borislav Petkov <bp@alien8.de>
>Cc: Andrew Morton <akpm@linux-foundation.org>
>Cc: Miaohe Lin <linmiaohe@huawei.com>
>Signed-off-by: Xie Yuanbin <xieyuanbin1@huawei.com>
>---
> include/trace/events/memory-failure.h | 6 +++++-
> 1 file changed, 5 insertions(+), 1 deletion(-)
>
>diff --git a/include/trace/events/memory-failure.h b/include/trace/events/memory-failure.h
>index aa57cc8f896b..7a8ee5d1a44e 100644
>--- a/include/trace/events/memory-failure.h
>+++ b/include/trace/events/memory-failure.h
>@@ -1,6 +1,10 @@
> /* SPDX-License-Identifier: GPL-2.0 */
> #undef TRACE_SYSTEM
>-#define TRACE_SYSTEM memory_failure
>+/*
>+ * For historical versions, memory_failure_event is in ras subsystem,
>+ * some user programs depend on it.
>+ */
>+#define TRACE_SYSTEM ras
> #define TRACE_INCLUDE_FILE memory-failure
>
> #if !defined(_TRACE_MEMORY_FAILURE_H) || defined(TRACE_HEADER_MULTI_READ)
>--
Thanks. Feel free to add:
Reviewed-by: Lance Yang <lance.yang@linux.dev>
^ permalink raw reply
* Re: [PATCH] mm/memory-failure: trace: change memory_failure_event to ras subsystem
From: Miaohe Lin @ 2026-06-08 11:27 UTC (permalink / raw)
To: Xie Yuanbin
Cc: linux-edac, linux-kernel, linux-mm, linux-trace-kernel, torvalds,
lilinjie8, liaohua4, david, qiuxu.zhuo, bp, akpm, rostedt,
nao.horiguchi, mhiramat, mchehab+huawei, tony.luck, yi1.lai
In-Reply-To: <20260605081213.154660-1-xieyuanbin1@huawei.com>
On 2026/6/5 16:12, Xie Yuanbin wrote:
> For historical version, commit 97f0b1345219 ("tracing: add trace event
> for memory-failure") introduced memory_failure_event in ras subsystem.
> commit 31807483d395 ("mm/memory-failure: remove the selection of RAS")
> changed memory_failure_event to memory_failure subsystem. This breaks
> the backward compatibility, some user programs rely on it.
>
> Change memory_failure_event to ras subsystem to keep backward
> compatibility.
>
> Fixes: 31807483d395 ("mm/memory-failure: remove the selection of RAS")
With David's comment addressed:
Reviewed-by: Miaohe Lin <linmiaohe@huawei.com>
Thanks.
.
^ permalink raw reply
* Re: [PATCH] rethook: Use tsk->on_cpu to check task execution state
From: Peter Zijlstra @ 2026-06-08 10:23 UTC (permalink / raw)
To: Tengda Wu
Cc: Masami Hiramatsu, Steven Rostedt, Mathieu Desnoyers,
Alexei Starovoitov, linux-trace-kernel, linux-kernel,
Josh Poimboeuf, jikos, mbenes, pmladek
In-Reply-To: <20260608093449.GH4149641@noisy.programming.kicks-ass.net>
On Mon, Jun 08, 2026 at 11:34:49AM +0200, Peter Zijlstra wrote:
>
> +Live patching folks
>
> On Mon, Jun 08, 2026 at 09:52:37AM +0800, Tengda Wu wrote:
>
> > Background: We are verifying the support of live patches for functions that
> > have a kretprobe. The specific verification method is as follows:
> >
> > We construct a function foo() that calls bar():
> >
> > void bar(void)
> > {
> > for (;;) {
> > schedule();
> > }
> > }
> >
> > void foo(void)
> > {
> > bar();
> > }
> >
> > A kretprobe is attached to bar():
> >
> > echo 'r:rp1 bar' > /sys/kernel/tracing/kprobe_events
> > echo 1 > /sys/kernel/tracing/events/kprobes/rp1/enable
> >
> > Then foo() is triggered. The expected behavior is that bar() will call
> > schedule() and yield the CPU.
> >
> > After that, the live patch is activated to attempt replacing the implementation
> > of foo(). The expectation is that this should succeed.
>
> This wholly depends on how foo() calls bar(), if it is a normal call,
> then no, it should not succeed, because foo() is still on the stack.
>
> If it is a tail-call, then yes, because foo() is no longer relevant.
>
> > However, in reality, because the task that called schedule() is still in the
> > RUNNING state,
>
> So calling schedule() without setting state is dodgy in the first place.
> Who is doing this? All wait primitives will set this to
> TASK_UNINTERRUPTIBLE or something along those lines.
>
> > the condition task_is_running(tsk) inside rethook_find_ret_addr()
> > is not satisfied, causing the function to return early. This, in turn,
> > prevents stack_trace_save_tsk_reliable() from determining the stack as
> > reliable, leading to a failure in activating the live patch.
> >
> > **Not sure if this is correct:**
> >
> > We believe that after a task voluntarily calls schedule(), when the stack
> > is expected to be reliable, it is a safe time to activate a live patch.
>
> Calling schedule() without setting state is a no-op and really shouldn't
> count much at all.
>
> > Additionally, a similar tsk->on_cpu check can be found elsewhere in the
> > kernel (See task_on_another_cpu() in arch/x86/include/asm/unwind.h).
> > Therefore, we propose changing the task_is_running(tsk) condition to
> > tsk->on_cpu.
>
> Anyway, I'm wondering what the purpose of this check here is, there is
> no real comment, and commit 5120d167e21c ("rethook: Remove warning
> messages printed for finding return address of a frame.") is just pure
> voodoo as well.
FWIW, you should have had this discussion then.
> Also, note the comment that goes with the usage of
> task_on_another_cpu(); that thing is racy as all heck.
>
> So it really comes down to what the purpose of this check is.
>
> I suspect the issue at hand is that tsk->rethook elements, such as
> iterated by __rethook_find_ret_addr() are not safe to be accessed for a
> running task.
>
> Notably while rethook_recycle() has some RCU thing on, that objpool
> thing (and the recycle name itself) seems to strongly suggest iterating
> these things is not sound (you could start with things from this task,
> hit a recycled entry and continue iterating rethooks from another task).
>
> Also note that the current check is also racy, nothing really prevents a
> wakeup from happening right after you observe task_is_running() being
> false. The task can then get scheduled in on another CPU and tear down
> its rethooks concurrent with __rethook_find_ret_addr().
>
>
> Now, livepatch itself calls unwind from a proper context, but unwinds in
> general are not. This rethook stuff doesn't seem to be sound in general.
I suspect just entirely removing the check is the sanest option at this
point. Callers that do it right (livepatch) are guaranteed consistent
data, and the rest gets whatever pieces.
Notably, unwind_next() holds rcu, so the iteration is protected from any
of those rethook_node things getting freed. Its just that the iteration
can go sideways and you might not get a sane answer.
The very worst possible option is getting stuck in an infinite loop when
concurrent with agressive rethook re-use or something daft like that,
but that seems extremely unlikely.
^ permalink raw reply
* Re: [PATCH v2 6/6] x86/setup: prepend embedded bootconfig cmdline before parse_early_param
From: Masami Hiramatsu @ 2026-06-08 10:19 UTC (permalink / raw)
To: Breno Leitao
Cc: Andrew Morton, Nathan Chancellor, paulmck, Nicolas Schier,
Thomas Gleixner, Ingo Molnar, Borislav Petkov, Dave Hansen, x86,
H. Peter Anvin, linux-kernel, linux-trace-kernel, linux-kbuild,
bpf, kernel-team
In-Reply-To: <20260605-bootconfig_using_tools-v2-6-d309f544b5f7@debian.org>
On Fri, 05 Jun 2026 05:03:37 -0700
Breno Leitao <leitao@debian.org> wrote:
> Call xbc_prepend_embedded_cmdline() in setup_arch() right after the
> CONFIG_CMDLINE merge and before strscpy(command_line, ...) so the
> build-time-rendered embedded bootconfig "kernel" subtree is part of
> boot_command_line by the time parse_early_param() runs. early_param()
> handlers (mem=, earlycon=, loglevel=, ...) now see values supplied via
> CONFIG_BOOT_CONFIG_EMBED_FILE without parsing bootconfig at runtime.
>
> Gate the prepend on the bootconfig opt-in: only fold in the embedded
> kernel.* keys when "bootconfig" is present on the command line, or
> CONFIG_BOOT_CONFIG_FORCE is set. Applying the embedded cmdline
> unconditionally would (a) diverge from how embedded init.* keys are
> treated and (b) break fail-safe recovery: a malformed embedded
> console=/mem= could panic the boot with no way for the admin to disable
> it by dropping "bootconfig" from the bootloader cmdline.
> cmdline_find_option_bool() runs before parse_early_param(), so the gate
> is cheap and correctly ordered.
>
> Select ARCH_SUPPORTS_CMDLINE_FROM_BOOTCONFIG so the user-visible
> CONFIG_BOOT_CONFIG_EMBED_CMDLINE option becomes selectable on x86.
This seems like a dummy config. what code does depend on this flag?
>
> With this select in place, setup_boot_config() in init/main.c would
> otherwise render the embedded "kernel" subtree a second time via
> xbc_make_cmdline("kernel") into extra_command_line, duplicating every
> embedded kernel.* key in saved_command_line and making accumulating
> handlers (console=, earlycon=, ...) register the same value twice. Skip
> that render only when xbc_prepend_embedded_cmdline() actually prepended
> the keys, reported by xbc_embedded_cmdline_applied().
>
> Keying the skip on the prepend itself, rather than re-deriving the
> opt-in, keeps the two paths consistent even when setup_arch() and the
> runtime parser detect "bootconfig" differently (e.g. "bootconfig=1"):
> the keys are then rendered at runtime instead of being dropped.
>
> Signed-off-by: Breno Leitao <leitao@debian.org>
> ---
> arch/x86/Kconfig | 1 +
> arch/x86/kernel/setup.c | 16 ++++++++++++++++
> init/main.c | 18 +++++++++++++++---
> 3 files changed, 32 insertions(+), 3 deletions(-)
>
> diff --git a/arch/x86/Kconfig b/arch/x86/Kconfig
> index f24810015234..f839795692b4 100644
> --- a/arch/x86/Kconfig
> +++ b/arch/x86/Kconfig
> @@ -126,6 +126,7 @@ config X86
> select ARCH_SUPPORTS_NUMA_BALANCING if X86_64
> select ARCH_SUPPORTS_KMAP_LOCAL_FORCE_MAP if NR_CPUS <= 4096
> select ARCH_SUPPORTS_CFI if X86_64
> + select ARCH_SUPPORTS_CMDLINE_FROM_BOOTCONFIG
> select ARCH_USES_CFI_TRAPS if X86_64 && CFI
> select ARCH_SUPPORTS_LTO_CLANG
> select ARCH_SUPPORTS_LTO_CLANG_THIN
> diff --git a/arch/x86/kernel/setup.c b/arch/x86/kernel/setup.c
> index 46882ce79c3a..26a82a41f44c 100644
> --- a/arch/x86/kernel/setup.c
> +++ b/arch/x86/kernel/setup.c
> @@ -6,6 +6,7 @@
> * parts of early kernel initialization.
> */
> #include <linux/acpi.h>
> +#include <linux/bootconfig.h>
> #include <linux/console.h>
> #include <linux/cpu.h>
> #include <linux/crash_dump.h>
> @@ -36,6 +37,7 @@
> #include <asm/bios_ebda.h>
> #include <asm/bugs.h>
> #include <asm/cacheinfo.h>
> +#include <asm/cmdline.h>
> #include <asm/coco.h>
> #include <asm/cpu.h>
> #include <asm/efi.h>
> @@ -924,6 +926,20 @@ void __init setup_arch(char **cmdline_p)
> builtin_cmdline_added = true;
> #endif
>
> + /*
> + * Honor the same opt-in as the runtime bootconfig parser: only fold
> + * the embedded kernel.* keys into the cmdline when "bootconfig" is
> + * present on the command line (or CONFIG_BOOT_CONFIG_FORCE is set).
> + * This keeps fail-safe recovery working -- dropping "bootconfig" from
> + * the bootloader cmdline disables the embedded keys -- so a malformed
> + * embedded console=/mem= cannot brick a boot with no way out. It also
> + * matches setup_boot_config(), which bails out under the same
> + * condition before parsing the embedded bootconfig at runtime.
> + */
> + if (IS_ENABLED(CONFIG_BOOT_CONFIG_FORCE) ||
> + cmdline_find_option_bool(boot_command_line, "bootconfig"))
> + xbc_prepend_embedded_cmdline(boot_command_line, COMMAND_LINE_SIZE);
> +
> strscpy(command_line, boot_command_line, COMMAND_LINE_SIZE);
> *cmdline_p = command_line;
>
> diff --git a/init/main.c b/init/main.c
> index e363232b428b..567f641a5731 100644
> --- a/init/main.c
> +++ b/init/main.c
> @@ -378,12 +378,15 @@ static void __init setup_boot_config(void)
> int pos, ret;
> size_t size;
> char *err;
> + bool from_embedded = false;
>
> /* Cut out the bootconfig data even if we have no bootconfig option */
> data = get_boot_config_from_initrd(&size);
> /* If there is no bootconfig in initrd, try embedded one. */
> - if (!data)
> + if (!data) {
> data = xbc_get_embedded_bootconfig(&size);
> + from_embedded = true;
Even from embedded bootconfig, if the arch set
ARCH_SUPPORTS_CMDLINE_FROM_BOOTCONFIG=n, this must be applied to
the cmdline as we are doing.
> + }
>
> strscpy(tmp_cmdline, boot_command_line, COMMAND_LINE_SIZE);
> err = parse_args("bootconfig", tmp_cmdline, NULL, 0, 0, 0, NULL,
> @@ -421,8 +424,17 @@ static void __init setup_boot_config(void)
> } else {
> xbc_get_info(&ret, NULL);
> pr_info("Load bootconfig: %ld bytes %d nodes\n", (long)size, ret);
> - /* keys starting with "kernel." are passed via cmdline */
> - extra_command_line = xbc_make_cmdline("kernel");
> + /*
> + * keys starting with "kernel." are passed via cmdline. When
> + * this bootconfig came from the embedded source and
> + * setup_arch() already prepended the rendered "kernel" subtree
> + * to boot_command_line, rendering again here would duplicate
> + * the keys in saved_command_line and make accumulating handlers
> + * (console=, earlycon=, ...) re-register the same value. Skip
> + * only when the prepend really happened.
Also, this should mention ARCH_SUPPORTS_CMDLINE_FROM_BOOTCONFIG=n case.
Thank you,
> + */
> + if (!from_embedded || !xbc_embedded_cmdline_applied())
> + extra_command_line = xbc_make_cmdline("kernel");
> /* Also, "init." keys are init arguments */
> extra_init_args = xbc_make_cmdline("init");
> }
>
> --
> 2.53.0-Meta
>
--
Masami Hiramatsu (Google) <mhiramat@kernel.org>
^ permalink raw reply
* Re: [PATCH] rethook: Use tsk->on_cpu to check task execution state
From: Peter Zijlstra @ 2026-06-08 9:34 UTC (permalink / raw)
To: Tengda Wu
Cc: Masami Hiramatsu, Steven Rostedt, Mathieu Desnoyers,
Alexei Starovoitov, linux-trace-kernel, linux-kernel,
Josh Poimboeuf, jikos, mbenes, pmladek
In-Reply-To: <679a1c8f-1e4d-4ae5-83e1-d0068e6de1a6@huaweicloud.com>
+Live patching folks
On Mon, Jun 08, 2026 at 09:52:37AM +0800, Tengda Wu wrote:
> Background: We are verifying the support of live patches for functions that
> have a kretprobe. The specific verification method is as follows:
>
> We construct a function foo() that calls bar():
>
> void bar(void)
> {
> for (;;) {
> schedule();
> }
> }
>
> void foo(void)
> {
> bar();
> }
>
> A kretprobe is attached to bar():
>
> echo 'r:rp1 bar' > /sys/kernel/tracing/kprobe_events
> echo 1 > /sys/kernel/tracing/events/kprobes/rp1/enable
>
> Then foo() is triggered. The expected behavior is that bar() will call
> schedule() and yield the CPU.
>
> After that, the live patch is activated to attempt replacing the implementation
> of foo(). The expectation is that this should succeed.
This wholly depends on how foo() calls bar(), if it is a normal call,
then no, it should not succeed, because foo() is still on the stack.
If it is a tail-call, then yes, because foo() is no longer relevant.
> However, in reality, because the task that called schedule() is still in the
> RUNNING state,
So calling schedule() without setting state is dodgy in the first place.
Who is doing this? All wait primitives will set this to
TASK_UNINTERRUPTIBLE or something along those lines.
> the condition task_is_running(tsk) inside rethook_find_ret_addr()
> is not satisfied, causing the function to return early. This, in turn,
> prevents stack_trace_save_tsk_reliable() from determining the stack as
> reliable, leading to a failure in activating the live patch.
>
> **Not sure if this is correct:**
>
> We believe that after a task voluntarily calls schedule(), when the stack
> is expected to be reliable, it is a safe time to activate a live patch.
Calling schedule() without setting state is a no-op and really shouldn't
count much at all.
> Additionally, a similar tsk->on_cpu check can be found elsewhere in the
> kernel (See task_on_another_cpu() in arch/x86/include/asm/unwind.h).
> Therefore, we propose changing the task_is_running(tsk) condition to
> tsk->on_cpu.
Anyway, I'm wondering what the purpose of this check here is, there is
no real comment, and commit 5120d167e21c ("rethook: Remove warning
messages printed for finding return address of a frame.") is just pure
voodoo as well.
Also, note the comment that goes with the usage of
task_on_another_cpu(); that thing is racy as all heck.
So it really comes down to what the purpose of this check is.
I suspect the issue at hand is that tsk->rethook elements, such as
iterated by __rethook_find_ret_addr() are not safe to be accessed for a
running task.
Notably while rethook_recycle() has some RCU thing on, that objpool
thing (and the recycle name itself) seems to strongly suggest iterating
these things is not sound (you could start with things from this task,
hit a recycled entry and continue iterating rethooks from another task).
Also note that the current check is also racy, nothing really prevents a
wakeup from happening right after you observe task_is_running() being
false. The task can then get scheduled in on another CPU and tear down
its rethooks concurrent with __rethook_find_ret_addr().
Now, livepatch itself calls unwind from a proper context, but unwinds in
general are not. This rethook stuff doesn't seem to be sound in general.
^ permalink raw reply
* Re: [PATCH 2/2] selftests/ftrace: Account for 8-byte aligned trace_marker_raw events
From: Masami Hiramatsu @ 2026-06-08 9:17 UTC (permalink / raw)
To: Hui Wang
Cc: rostedt, mathieu.desnoyers, pjw, linux-trace-kernel, shuah,
wangfushuai, linux-kselftest
In-Reply-To: <20260607072431.125633-3-hui.wang@canonical.com>
On Sun, 7 Jun 2026 15:24:31 +0800
Hui Wang <hui.wang@canonical.com> wrote:
> trace_marker_raw.tc assumes that the raw marker payload length
> reported in trace_pipe is the result of int((id + 3) / 4) * 4, but
> that is not true on kernels with CONFIG_HAVE_64BIT_ALIGNED_ACCESS
> enabled.
>
> With forced 8-byte alignment, the ring buffer event forces 8-byte
> alignment. The event length is stored in array[0], the payload data
> and id are placed in a struct raw_data_entry which is stored starting
> at array[1]. In this case, the printed payload data length is 8*N+4
> bytes.
>
> To make the testcase pass in this case, add a kconfig_enabled() helper
> and use it to detect CONFIG_HAVE_64BIT_ALIGNED_ACCESS so
> trace_marker_raw.tc can calculate the expected length correctly.
>
Hmm this fix lacks consideration for the environment.
> Assisted-by: Copilot:gpt-5.5
> Signed-off-by: Hui Wang <hui.wang@canonical.com>
> ---
> .../ftrace/test.d/00basic/trace_marker_raw.tc | 16 +++++++--
> .../testing/selftests/ftrace/test.d/functions | 33 +++++++++++++++++++
> 2 files changed, 46 insertions(+), 3 deletions(-)
>
> diff --git a/tools/testing/selftests/ftrace/test.d/00basic/trace_marker_raw.tc b/tools/testing/selftests/ftrace/test.d/00basic/trace_marker_raw.tc
> index 8e905d4fe6dd..beda0f8627b3 100644
> --- a/tools/testing/selftests/ftrace/test.d/00basic/trace_marker_raw.tc
> +++ b/tools/testing/selftests/ftrace/test.d/00basic/trace_marker_raw.tc
> @@ -15,6 +15,11 @@ is_little_endian() {
> }
>
> little=`is_little_endian`
> +raw_data_align=4
> +
> +if kconfig_enabled CONFIG_HAVE_64BIT_ALIGNED_ACCESS; then
Checking Kconfig is OK, but in this case, if the existence of the
dependent Kconfig file itself cannot be confirmed, this test should
return an unresolved error.
> + raw_data_align=8
> +fi
>
> make_str() {
> id=$1
> @@ -60,7 +65,8 @@ test_multiple_writes() {
> echo stop > trace_marker
>
> # Check to make sure the number of entries is the id (rounded up by 4)
> - awk '/.*: # [0-9a-f]* / {
> + # or is (((id + 3) rounded by 8) + 4) if raw_data_align is 8
> + awk -v data_align=$raw_data_align '/.*: # [0-9a-f]* / {
> print;
> cnt = -1;
> for (i = 0; i < NF; i++) {
> @@ -69,8 +75,12 @@ test_multiple_writes() {
> i++;
> cnt = strtonum("0x" $i);
> num = NF - (i + 1);
> - # The number of items is always rounded up by 4
> - cnt2 = int((cnt + 3) / 4) * 4;
> + # The number of items is rounded up by 4
> + # or is (8 * N + 4) if data_align is 8
> + if (data_align == 4)
> + cnt2 = int((cnt + 3) / 4) * 4;
> + else
> + cnt2 = int((cnt + 3) / 8) * 8 + 4;
> if (cnt2 != num) {
> exit 1;
> }
> diff --git a/tools/testing/selftests/ftrace/test.d/functions b/tools/testing/selftests/ftrace/test.d/functions
> index 826141e299e5..0f778087d81b 100644
> --- a/tools/testing/selftests/ftrace/test.d/functions
> +++ b/tools/testing/selftests/ftrace/test.d/functions
> @@ -177,6 +177,39 @@ check_awk_strtonum() { # strtonum is GNU awk extension
> awk 'BEGIN{strtonum("0x1")}'
> }
>
> +# a helper to check if a kconfig is enabled or not
> +# return value: 0 (if kconfig is enabled)
> +# 1 (if kconfig is not enabled)
> +# 2 (if the config files don't exist or are unreadable)
> +kconfig_enabled() { # config-name
> + local config="$1"
> + local uname_r=`uname -r`
> + local config_file
> +
> + case "$config" in
> + CONFIG_*) ;;
> + *) config="CONFIG_$config" ;;
> + esac
> +
> + if [ -f /proc/config.gz ] && zgrep --version >/dev/null 2>&1; then
> + zgrep -Eq "^${config}=(y|m)$" /proc/config.gz 2>/dev/null
Do not use zgrep (this requires to install zgrep pacakge) in this test,
instead, use more widely available `gzip -dc | grep ...`.
I would like to keep this runnable on a minimum environment.
> + return $?
> + fi
> +
> + for config_file in \
> + /boot/config-$uname_r \
> + /lib/modules/$uname_r/config \
> + /lib/modules/$uname_r/build/.config
Hmm, also I don't like this, because this highly depends on the environment.
Instead, we can add CONFIG_IKCONFIG_PROC=y in tools/testing/selftests/ftrace/config.
Thank you,
> + do
> + if [ -f "$config_file" ]; then
> + grep -Eq "^${config}=(y|m)$" "$config_file"
> + return $?
> + fi
> + done
> +
> + return 2
> +}
> +
> LOCALHOST=127.0.0.1
>
> yield() {
> --
> 2.43.0
>
>
--
Masami Hiramatsu (Google) <mhiramat@kernel.org>
^ permalink raw reply
* Re: [PATCH 1/2] ring-buffer: Fix event length with forced 8-byte alignment
From: Masami Hiramatsu @ 2026-06-08 9:02 UTC (permalink / raw)
To: Hui Wang
Cc: rostedt, mathieu.desnoyers, pjw, linux-trace-kernel, shuah,
wangfushuai, linux-kselftest
In-Reply-To: <20260607072431.125633-2-hui.wang@canonical.com>
On Sun, 7 Jun 2026 15:24:30 +0800
Hui Wang <hui.wang@canonical.com> wrote:
> When RB_FORCE_8BYTE_ALIGNMENT is true, rb_calculate_event_length()
> reserves the space of event->array[0] for placing the data length and
> rb_update_event() stores the data length in event->array[0]
> accordingly. As a result the whole event length will add extra 4 bytes
> for sizeof(event.array[0]) unconditionally.
>
> But ring_buffer_event_length() only subtracts the
> sizeof(event->array[0]) for events larger than RB_MAX_SMALL_DATA +
> sizeof(event->array[0]). As a result, small events on architectures
> with RB_FORCE_8BYTE_ALIGNMENT=true report a data length that is 4
> bytes larger than expected.
>
> To fix it, add the RB_FORCE_8BYTE_ALIGNMENT as a condition to subtract
> the size of that length field whenever RB_FORCE_8BYTE_ALIGNMENT is
> true.
>
> This issue is observed in a riscv64 kernel with
> CONFIG_HAVE_64BIT_ALIGNED_ACCESS set to y, when we run ftrace selftest
> trace_marker_raw.tc, we get the weird log: for cases where the id is
> 1..100, the number of data field is 8*N, but once id exceeds 100, the
> number of data field becomes 8*N+4:
> # 1 buf: 58 00 00 00 80 5e d1 63 (number of data field is 8*1)
> ...
> # a buf: 58 ... (number of data field is 8*2)
> ...
> # 64 buf: 58 ... (number of data field is 8*13)
> # 65 buf: 58 ... (number of data field is 8*13+4)
>
> After applying this change, the number of data field keeps being 8*N+4
> consistently.
>
Good catch!
This looks good to me.
Reviewed-by: Masami Hiramatsu (Google) <mhiramat@kernel.org>
Thanks,
> Fixes: 2271048d1b3b ("ring-buffer: Do 8 byte alignment for 64 bit that can not handle 4 byte align")
> Signed-off-by: Hui Wang <hui.wang@canonical.com>
> ---
> kernel/trace/ring_buffer.c | 3 ++-
> 1 file changed, 2 insertions(+), 1 deletion(-)
>
> diff --git a/kernel/trace/ring_buffer.c b/kernel/trace/ring_buffer.c
> index 56a328e94395..d9af2bbaf9c0 100644
> --- a/kernel/trace/ring_buffer.c
> +++ b/kernel/trace/ring_buffer.c
> @@ -270,7 +270,8 @@ unsigned ring_buffer_event_length(struct ring_buffer_event *event)
> if (event->type_len > RINGBUF_TYPE_DATA_TYPE_LEN_MAX)
> return length;
> length -= RB_EVNT_HDR_SIZE;
> - if (length > RB_MAX_SMALL_DATA + sizeof(event->array[0]))
> + if (length > RB_MAX_SMALL_DATA + sizeof(event->array[0]) ||
> + RB_FORCE_8BYTE_ALIGNMENT)
> length -= sizeof(event->array[0]);
> return length;
> }
> --
> 2.43.0
>
>
--
Masami Hiramatsu (Google) <mhiramat@kernel.org>
^ permalink raw reply
* [PATCH v3 13/13] verification/rvgen: Remove dead code
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
The conversion to use Lark left some dead code behind. Remove them.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v3: delete unused import
---
tools/verification/rvgen/rvgen/automata.py | 157 ---------------------
tools/verification/rvgen/rvgen/dot2k.py | 29 +---
2 files changed, 1 insertion(+), 185 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index a3be327c2a73..bfc997f630d7 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -9,9 +9,6 @@
# Documentation/trace/rv/deterministic_automata.rst
import ntpath
-import re
-from typing import Iterator
-from itertools import islice
import lark
@@ -356,19 +353,6 @@ class State:
self.name = name
self.inv = inv
-class _ConstraintKey:
- """Base class for constraint keys."""
-
-class _StateConstraintKey(_ConstraintKey, int):
- """Key for a state constraint. Under the hood just state_id."""
- def __new__(cls, state_id: int):
- return super().__new__(cls, state_id)
-
-class _EventConstraintKey(_ConstraintKey, tuple):
- """Key for an event constraint. Under the hood just tuple(state_id,event_id)."""
- def __new__(cls, state_id: int, event_id: int):
- return super().__new__(cls, (state_id, event_id))
-
class AutomataError(Exception):
"""Exception raised for errors in automata parsing and validation.
@@ -387,28 +371,10 @@ class Automata:
invalid_state_str = "INVALID_STATE"
init_marker = "__init_"
- node_marker = "{node"
- # val can be numerical, uppercase (constant or macro), lowercase (parameter or function)
- # only numerical values should have units
- constraint_rule = re.compile(r"""
- ^
- (?P<env>[a-zA-Z_][a-zA-Z0-9_]+) # C-like identifier for the env var
- (?P<op>[!<=>]{1,2}) # operator
- (?P<val>
- [0-9]+ | # numerical value
- [A-Z_]+\(\) | # macro
- [A-Z_]+ | # constant
- [a-z_]+\(\) | # function
- [a-z_]+ # parameter
- )
- (?P<unit>[a-z]{1,2})? # optional unit for numerical values
- """, re.VERBOSE)
- constraint_reset = re.compile(r"^reset\((?P<env>[a-zA-Z_][a-zA-Z0-9_]+)\)")
def __init__(self, file_path, model_name=None):
self.__dot_path = file_path
self.name = model_name or self.__get_model_name()
- self.__dot_lines = self.__open_dot()
self.__parse_tree = ParseTree(file_path)
self.transitions = self.__parse_transitions()
self.states, self.initial_state, self.final_states = self.__parse_states()
@@ -435,57 +401,6 @@ class Automata:
return model_name
- def __open_dot(self) -> list[str]:
- dot_lines = []
- try:
- with open(self.__dot_path) as dot_file:
- dot_lines = dot_file.readlines()
- except OSError as exc:
- raise AutomataError(exc.strerror) from exc
-
- if not dot_lines:
- raise AutomataError(f"{self.__dot_path} is empty")
-
- # checking the first line:
- line = dot_lines[0].split()
-
- if len(line) < 2 or line[0] != "digraph" or line[1] != "state_automaton":
- raise AutomataError(f"Not a valid .dot format: {self.__dot_path}")
-
- return dot_lines
-
- def __get_cursor_begin_states(self) -> int:
- for cursor, line in enumerate(self.__dot_lines):
- split_line = line.split()
-
- if len(split_line) and split_line[0] == self.node_marker:
- return cursor
-
- raise AutomataError("Could not find a beginning state")
-
- def __get_cursor_begin_events(self) -> int:
- state = 0
- cursor = 0 # make pyright happy
-
- for cursor, line in enumerate(self.__dot_lines):
- line = line.split()
- if not line:
- continue
-
- if state == 0:
- if line[0] == self.node_marker:
- state = 1
- elif line[0] != self.node_marker:
- break
- else:
- raise AutomataError("Could not find beginning event")
-
- cursor += 1 # skip initial state transition
- if cursor == len(self.__dot_lines):
- raise AutomataError("Dot file ended after event beginning")
-
- return cursor
-
def __parse_transitions(self):
transitions = []
@@ -542,51 +457,6 @@ class Automata:
states.insert(0, initial_state)
return states, initial_state, final_states
- def __get_state_variables(self) -> tuple[list[str], str, list[str]]:
- # wait for node declaration
- states = []
- final_states = []
- initial_state = ""
-
- has_final_states = False
- cursor = self.__get_cursor_begin_states()
-
- # process nodes
- for line in islice(self.__dot_lines, cursor, None):
- split_line = line.split()
- if not split_line or split_line[0] != self.node_marker:
- break
-
- raw_state = split_line[-1]
-
- # "enabled_fired"}; -> enabled_fired
- state = raw_state.replace('"', '').replace('};', '').replace(',', '_')
- if state.startswith(self.init_marker):
- initial_state = state[len(self.init_marker):]
- else:
- states.append(state)
- if "doublecircle" in line:
- final_states.append(state)
- has_final_states = True
-
- if "ellipse" in line:
- final_states.append(state)
- has_final_states = True
-
- if not initial_state:
- raise AutomataError("The automaton doesn't have an initial state")
-
- states = sorted(set(states))
- states.remove(initial_state)
-
- # Insert the initial state at the beginning of the states
- states.insert(0, initial_state)
-
- if not has_final_states:
- final_states.append(initial_state)
-
- return states, initial_state, final_states
-
def __get_event_variables(self) -> tuple[list[str], list[str]]:
events: list[str] = []
envs: list[str] = []
@@ -609,26 +479,6 @@ class Automata:
return sorted(set(events)), sorted(set(envs))
- def _split_constraint_expr(self, constr: list[str]) -> Iterator[tuple[str,
- str | None]]:
- """
- Get a list of strings of the type constr1 && constr2 and returns a list of
- constraints and separators: [[constr1,"&&"],[constr2,None]]
- """
- exprs = []
- seps = []
- for c in constr:
- while "&&" in c or "||" in c:
- a = c.find("&&")
- o = c.find("||")
- pos = a if o < 0 or 0 < a < o else o
- exprs.append(c[:pos].replace(" ", ""))
- seps.append(c[pos:pos + 2].replace(" ", ""))
- c = c[pos + 2:].replace(" ", "")
- exprs.append(c)
- seps.append(None)
- return zip(exprs, seps)
-
def __extract_env_var(self, constraint: ConstraintCondition):
if constraint.unit:
self.env_types[constraint.env] = constraint.unit
@@ -697,10 +547,3 @@ class Automata:
def is_hybrid_automata(self) -> bool:
return bool(self.envs)
-
- def is_event_constraint(self, key: _ConstraintKey) -> bool:
- """
- Given the key in self.constraints return true if it is an event
- constraint, false if it is a state constraint
- """
- return isinstance(key, _EventConstraintKey)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index e4b6c7c09170..a080b92334f9 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -8,12 +8,9 @@
# For further information, see:
# Documentation/trace/rv/da_monitor_synthesis.rst
-from collections import deque
from .dot2c import Dot2c
from .generator import Monitor
-from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
-from .automata import ConstraintCondition
-
+from .automata import ConstraintCondition, AutomataError
class dot2k(Monitor, Dot2c):
template_dir = "dot2k"
@@ -217,9 +214,6 @@ class ha2k(dot2k):
value *= 10**9
return str(value) + "ull"
- def __parse_single_constraint(self, rule: dict, value: str) -> str:
- return f"ha_get_env(ha_mon, {rule["env"]}{self.enum_suffix}, time_ns) {rule["op"]} {value}"
-
def __parse_guard_rule(self, rule) -> list[str]:
buff = []
for c, sep in rule.rules:
@@ -233,12 +227,6 @@ class ha2k(dot2k):
buff.append(cond)
return buff
- def __get_constraint_env(self, constr: str) -> str:
- """Extract the second argument from an ha_ function"""
- env = constr.split("(")[1].split()[1].rstrip(")").rstrip(",")
- assert env.removesuffix(f"_{self.name}") in self.envs
- return env
-
def __start_to_invariant_check(self, inv: ConstraintCondition) -> str:
# by default assume the timer has ns expiration
clock_type = "ns"
@@ -249,21 +237,6 @@ class ha2k(dot2k):
return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {value})"
- def __start_to_conv(self, constr: str) -> str:
- """
- Undo the storage conversion done by ha_start_timer_
- """
- return "ha_inv_to_guard" + constr[constr.find("("):]
-
- def __parse_timer_constraint(self, rule: dict, value: str) -> str:
- # by default assume the timer has ns expiration
- clock_type = "ns"
- if self.env_types.get(rule["env"]) == "j":
- clock_type = "jiffy"
-
- return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.enum_suffix},"
- f" {value}, time_ns)")
-
def __parse_invariant(self, inv):
# by default assume the timer has ns expiration
clock_type = "ns"
--
2.47.3
^ permalink raw reply related
* [PATCH v3 12/13] verification/rvgen: Remove the old state variables
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
The state variables (states, initial_state, final_states) only capture the
states' names and have less information than their Lark-based counterparts.
Switch to use the new state variables and delete these old ones.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 9 ++++-----
tools/verification/rvgen/rvgen/dot2c.py | 10 +++++-----
tools/verification/rvgen/rvgen/dot2k.py | 8 ++++----
3 files changed, 13 insertions(+), 14 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 4c302f5cba68..a3be327c2a73 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -411,8 +411,7 @@ class Automata:
self.__dot_lines = self.__open_dot()
self.__parse_tree = ParseTree(file_path)
self.transitions = self.__parse_transitions()
- self._states, self._initial_state, self._final_states = self.__parse_states()
- self.states, self.initial_state, self.final_states = self.__get_state_variables()
+ self.states, self.initial_state, self.final_states = self.__parse_states()
self.env_types = {}
self.env_stored = set()
self.constraint_vars = set()
@@ -603,7 +602,7 @@ class Automata:
envs.append(c.env)
self.__extract_env_var(c)
- for state in self._states:
+ for state in self.states:
if state.inv:
envs.append(state.inv.env)
self.__extract_env_var(state.inv)
@@ -639,7 +638,7 @@ class Automata:
def __create_matrix(self) -> list[list[str]]:
# transform the array into a dictionary
events = self.events
- states = [s.name for s in self._states]
+ states = [s.name for s in self.states]
events_dict = {}
states_dict = {}
nr_event = 0
@@ -675,7 +674,7 @@ class Automata:
for j in range(len(self.states)):
if self.function[j][i] != self.invalid_state_str:
curr_event_used += 1
- if self.function[j][i] == self.initial_state:
+ if self.function[j][i] == self.initial_state.name:
curr_event_will_init += 1
if self.function[0][i] != self.invalid_state_str:
curr_event_from_init = True
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index fc85ba1f649e..22938ce1bf6c 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -29,10 +29,10 @@ class Dot2c(Automata):
def __get_enum_states_content(self) -> list[str]:
buff = []
- buff.append(f"\t{self.initial_state}{self.enum_suffix},")
+ buff.append(f"\t{self.initial_state.name}{self.enum_suffix},")
for state in self.states:
if state != self.initial_state:
- buff.append(f"\t{state}{self.enum_suffix},")
+ buff.append(f"\t{state.name}{self.enum_suffix},")
buff.append(f"\tstate_max{self.enum_suffix},")
return buff
@@ -142,7 +142,7 @@ class Dot2c(Automata):
def format_aut_init_states_string(self) -> list[str]:
buff = []
buff.append("\t.state_names = {")
- buff.append(self.__get_string_vector_per_line_content(self.states))
+ buff.append(self.__get_string_vector_per_line_content([s.name for s in self.states]))
buff.append("\t},")
return buff
@@ -159,7 +159,7 @@ class Dot2c(Automata):
return buff
def __get_max_strlen_of_states(self) -> int:
- max_state_name = len(max(self.states, key=len))
+ max_state_name = max((len(s.name) for s in self.states))
return max(max_state_name, len(self.invalid_state_str))
def get_aut_init_function(self) -> str:
@@ -199,7 +199,7 @@ class Dot2c(Automata):
return buff
def get_aut_init_initial_state(self) -> str:
- return self.initial_state
+ return self.initial_state.name
def format_aut_init_initial_state(self) -> list[str]:
buff = []
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index dc6d6f33729b..e4b6c7c09170 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -179,7 +179,7 @@ class ha2k(dot2k):
self.trace_h = self._read_template_file("trace_hybrid.h")
self.has_invariant = False
self.has_guard = False
- for state in self._states:
+ for state in self.states:
if state.inv:
self.has_invariant = True
for transition in self.transitions:
@@ -314,7 +314,7 @@ f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
{{"""]
_else = ""
- for state in self._states:
+ for state in self.states:
if not state.inv:
continue
@@ -382,7 +382,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
buff.append(f"\tif ({condition_str})\n\t\treturn;")
_else = ""
- for state in self._states:
+ for state in self.states:
inv = state.inv
if not inv:
continue
@@ -391,7 +391,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
buff.append(f"\t\t{inv};")
_else = "else "
- for state in self._states:
+ for state in self.states:
inv = state.inv
if not inv:
continue
--
2.47.3
^ permalink raw reply related
* [PATCH v3 07/13] rv: Simplify hybrid automata monitors's clock variables
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
Hybrid automata monitors's clock variables have two different
representations:
- The invariant representation, which is the timestamp when the invariant
expires
- The guard representation, which is the timestamp when the clock is last
reset
This dual representation makes the logic quite difficult to follow (well,
at least for me). It also complicates the monitors and the generation tool,
as it requires conversion back and forth between the representation.
Simplify by using the clock variables for a single purpose: storing the
time stamp since the clock is last reset.
This also allows simplifying rvgen, which will be done in a follow-up
commit.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v3:
- fix wrongly passing expire to ha_invariant_passed_jiffy()
- typo
---
include/rv/ha_monitor.h | 64 ++++++------------------
kernel/trace/rv/monitors/nomiss/nomiss.c | 18 +------
kernel/trace/rv/monitors/stall/stall.c | 2 +-
3 files changed, 19 insertions(+), 65 deletions(-)
diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h
index 28d3c74cabfc..9144b4c06f3f 100644
--- a/include/rv/ha_monitor.h
+++ b/include/rv/ha_monitor.h
@@ -327,19 +327,8 @@ static inline void __ha_monitor_timer_callback(struct ha_monitor *ha_mon)
}
/*
- * The clock variables have 2 different representations in the env_store:
- * - The guard representation is the timestamp of the last reset
- * - The invariant representation is the timestamp when the invariant expires
- * As the representations are incompatible, care must be taken when switching
- * between them: the invariant representation can only be used when starting a
- * timer when the previous representation was guard (e.g. no other invariant
- * started since the last reset operation).
- * Likewise, switching from invariant to guard representation without a reset
- * can be done only by subtracting the exact value used to start the invariant.
- *
- * Reading the environment variable (ha_get_clk) also reflects this difference
- * any reads in states that have an invariant return the (possibly negative)
- * time since expiration, other reads return the time since last reset.
+ * The clock variables store the time epoch - the timestamp when the clock was last reset.
+ * They are read by subtracting the time epoch from the current time.
*/
/*
@@ -353,31 +342,21 @@ static inline void ha_reset_clk_ns(struct ha_monitor *ha_mon, enum envs env, u64
{
WRITE_ONCE(ha_mon->env_store[env], time_ns);
}
-static inline void ha_set_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
- u64 value, u64 time_ns)
-{
- WRITE_ONCE(ha_mon->env_store[env], time_ns + value);
-}
-static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon,
- enum envs env, u64 time_ns)
+static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
+ u64 time_ns, u64 expire_ns)
{
- return READ_ONCE(ha_mon->env_store[env]) >= time_ns;
+ return READ_ONCE(ha_mon->env_store[env]) >= time_ns - expire_ns;
}
/*
* ha_invariant_passed_ns - prepare the invariant and return the time since reset
*/
-static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env,
- u64 expire, u64 time_ns)
+static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
{
- u64 passed = 0;
-
if (env < 0 || env >= ENV_MAX_STORED)
return 0;
if (ha_monitor_env_invalid(ha_mon, env))
return 0;
- passed = ha_get_env(ha_mon, env, time_ns);
- ha_set_invariant_ns(ha_mon, env, expire - passed, time_ns);
- return passed;
+ return ha_get_env(ha_mon, env, time_ns);
}
/*
@@ -391,32 +370,21 @@ static inline void ha_reset_clk_jiffy(struct ha_monitor *ha_mon, enum envs env)
{
WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64());
}
-static inline void ha_set_invariant_jiffy(struct ha_monitor *ha_mon,
- enum envs env, u64 value)
+static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon, enum envs env,
+ u64 time_ns, u64 expire_jiffy)
{
- WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64() + value);
-}
-static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon,
- enum envs env, u64 time_ns)
-{
- return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64());
-
+ return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64() - expire_jiffy);
}
/*
* ha_invariant_passed_jiffy - prepare the invariant and return the time since reset
*/
-static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env,
- u64 expire, u64 time_ns)
+static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
{
- u64 passed = 0;
-
if (env < 0 || env >= ENV_MAX_STORED)
return 0;
if (ha_monitor_env_invalid(ha_mon, env))
return 0;
- passed = ha_get_env(ha_mon, env, time_ns);
- ha_set_invariant_jiffy(ha_mon, env, expire - passed);
- return passed;
+ return ha_get_env(ha_mon, env, time_ns);
}
/*
@@ -463,14 +431,14 @@ static inline void ha_setup_timer(struct ha_monitor *ha_mon)
static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
- u64 passed = ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns);
+ u64 passed = ha_invariant_passed_jiffy(ha_mon, env, time_ns);
mod_timer(&ha_mon->timer, get_jiffies_64() + expire - passed);
}
static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
- u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);
+ u64 passed = ha_invariant_passed_ns(ha_mon, env, time_ns);
ha_start_timer_jiffy(ha_mon, ENV_MAX_STORED,
nsecs_to_jiffies(expire - passed + TICK_NSEC - 1), time_ns);
@@ -516,7 +484,7 @@ static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
int mode = HRTIMER_MODE_REL_HARD;
- u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);
+ u64 passed = ha_invariant_passed_ns(ha_mon, env, time_ns);
if (RV_MON_TYPE == RV_MON_PER_CPU)
mode |= HRTIMER_MODE_PINNED;
@@ -525,7 +493,7 @@ static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
- u64 passed = ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns);
+ u64 passed = ha_invariant_passed_jiffy(ha_mon, env, time_ns);
ha_start_timer_ns(ha_mon, ENV_MAX_STORED,
jiffies_to_nsecs(expire - passed), time_ns);
diff --git a/kernel/trace/rv/monitors/nomiss/nomiss.c b/kernel/trace/rv/monitors/nomiss/nomiss.c
index 8ead8783c29f..515ece5ce0ca 100644
--- a/kernel/trace/rv/monitors/nomiss/nomiss.c
+++ b/kernel/trace/rv/monitors/nomiss/nomiss.c
@@ -57,24 +57,12 @@ static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
enum states next_state, u64 time_ns)
{
if (curr_state == ready_nomiss)
- return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns);
+ return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns, DEADLINE_NS(ha_mon));
else if (curr_state == running_nomiss)
- return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns);
+ return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns, DEADLINE_NS(ha_mon));
return true;
}
-static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
- enum states curr_state, enum events event,
- enum states next_state, u64 time_ns)
-{
- if (curr_state == next_state)
- return;
- if (curr_state == ready_nomiss)
- ha_inv_to_guard(ha_mon, clk_nomiss, DEADLINE_NS(ha_mon), time_ns);
- else if (curr_state == running_nomiss)
- ha_inv_to_guard(ha_mon, clk_nomiss, DEADLINE_NS(ha_mon), time_ns);
-}
-
static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
enum states curr_state, enum events event,
enum states next_state, u64 time_ns)
@@ -122,8 +110,6 @@ static bool ha_verify_constraint(struct ha_monitor *ha_mon,
if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
return false;
- ha_convert_inv_guard(ha_mon, curr_state, event, next_state, time_ns);
-
if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
return false;
diff --git a/kernel/trace/rv/monitors/stall/stall.c b/kernel/trace/rv/monitors/stall/stall.c
index 3c38fb1a0159..b265578f845c 100644
--- a/kernel/trace/rv/monitors/stall/stall.c
+++ b/kernel/trace/rv/monitors/stall/stall.c
@@ -38,7 +38,7 @@ static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
enum states next_state, u64 time_ns)
{
if (curr_state == enqueued_stall)
- return ha_check_invariant_jiffy(ha_mon, clk_stall, time_ns);
+ return ha_check_invariant_jiffy(ha_mon, clk_stall, time_ns, threshold_jiffies);
return true;
}
--
2.47.3
^ permalink raw reply related
* [PATCH v3 09/13] verification/rvgen: Delete __parse_constraint()
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
All previous users of self.invariants and self.guards have been converted
to the Lark parser, delete __parse_constraints() and its associates.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 67 ++-----------------------
1 file changed, 4 insertions(+), 63 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 6d346a718a39..a38ef735a861 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -177,7 +177,6 @@ class ha2k(dot2k):
if not self.is_hybrid_automata():
raise AutomataError("Detected deterministic automaton, use the 'da' class")
self.trace_h = self._read_template_file("trace_hybrid.h")
- self.__parse_constraints()
self.has_invariant = False
self.has_guard = False
for state in self._states:
@@ -304,64 +303,6 @@ class ha2k(dot2k):
separator = "\n\t\t " if sum(len(r) for r in rules) > 80 else " "
return ["res = " + separator.join(rules) + ";"]
- def __validate_constraint(self, key: tuple[int, int] | int, constr: str,
- rule, reset) -> None:
- # event constrains are tuples and allow both rules and reset
- # state constraints are only used for expirations (e.g. clk<N)
- if self.is_event_constraint(key):
- if not rule and not reset:
- raise AutomataError("Unrecognised event constraint "
- f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
- if rule and (rule["env"] in self.env_types and
- rule["env"] not in self.env_stored):
- raise AutomataError("Clocks in hybrid automata always require a storage"
- f" ({rule["env"]})")
- else:
- if not rule:
- raise AutomataError("Unrecognised state constraint "
- f"({self.states[key]}: {constr})")
- if rule["env"] not in self.env_stored:
- raise AutomataError("State constraints always require a storage "
- f"({rule["env"]})")
- if rule["op"] not in ["<", "<="]:
- raise AutomataError("State constraints must be clock expirations like"
- f" clk<N ({rule.string})")
-
- def __parse_constraints(self) -> None:
- self.guards: dict[_EventConstraintKey, str] = {}
- self.invariants: dict[_StateConstraintKey, str] = {}
- for key, constraint in self.constraints.items():
- rules = []
- resets = []
- for c, sep in self._split_constraint_expr(constraint):
- rule = self.constraint_rule.search(c)
- reset = self.constraint_reset.search(c)
- self.__validate_constraint(key, c, rule, reset)
- if rule:
- value = rule["val"]
- value_len = len(rule["val"])
- unit = None
- if rule.groupdict().get("unit"):
- value_len += len(rule["unit"])
- unit = rule["unit"]
- c = c[:-(value_len)]
- value = self.__adjust_value(value, unit)
- if self.is_event_constraint(key):
- c = self.__parse_single_constraint(rule, value)
- if sep:
- c += f" {sep}"
- else:
- c = self.__parse_timer_constraint(rule, value)
- rules.append(c)
- if reset:
- c = f"ha_reset_env(ha_mon, {reset["env"]}{self.enum_suffix}, time_ns)"
- resets.append(c)
- if self.is_event_constraint(key):
- res = self.__format_guard_rules(rules) + resets
- self.guards[key] = ";".join(res)
- else:
- self.invariants[key] = rules[0]
-
def __fill_verify_invariants_func(self) -> list[str]:
if not self.has_invariant:
return []
@@ -486,15 +427,15 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
{{""")
- if self.invariants:
+ if self.has_invariant:
buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, "
"event, next_state, time_ns))\n\t\treturn false;\n")
- if self.guards:
+ if self.has_guard:
buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
"next_state, time_ns))\n\t\treturn false;\n")
- if self.invariants:
+ if self.has_invariant:
buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n")
buff.append("\treturn true;\n}\n")
@@ -571,7 +512,7 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func()
def _fill_timer_type(self) -> list:
- if self.invariants:
+ if self.has_invariant:
return [
"/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */",
"#define HA_TIMER_TYPE HA_TIMER_HRTIMER"
--
2.47.3
^ permalink raw reply related
* [PATCH v3 11/13] verification/rvgen: Switch __create_matrix() to Lark
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
Switch __create_matrix() to use the transitions parsed by Lark to avoid all
the raw text parsing.
Also stop parsing constraints in __create_matrix(), that is not used
anymore.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 47 ++++++----------------
tools/verification/rvgen/rvgen/dot2k.py | 2 +-
2 files changed, 13 insertions(+), 36 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 2e26bb863245..4c302f5cba68 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -418,7 +418,7 @@ class Automata:
self.constraint_vars = set()
self.self_loop_reset_events = set()
self.events, self.envs = self.__get_event_variables()
- self.function, self.constraints = self.__create_matrix()
+ self.function = self.__create_matrix()
self.events_start, self.events_start_run = self.__store_init_events()
self.env_stored = sorted(self.env_stored)
self.constraint_vars = sorted(self.constraint_vars)
@@ -636,10 +636,10 @@ class Automata:
if constraint.val[0].isalpha():
self.constraint_vars.add(constraint.val)
- def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]:
+ def __create_matrix(self) -> list[list[str]]:
# transform the array into a dictionary
events = self.events
- states = self.states
+ states = [s.name for s in self._states]
events_dict = {}
states_dict = {}
nr_event = 0
@@ -654,39 +654,16 @@ class Automata:
# declare the matrix....
matrix = [[self.invalid_state_str for _ in range(nr_event)] for _ in range(nr_state)]
- constraints: dict[_ConstraintKey, list[str]] = {}
- # and we are back! Let's fill the matrix
- cursor = self.__get_cursor_begin_events()
-
- for line in map(str.lstrip,
- islice(self.__dot_lines, cursor, None)):
-
- if not line or line[0] != '"':
- break
-
- split_line = line.split()
-
- if len(split_line) > 2 and split_line[1] == "->":
- origin_state = split_line[0].replace('"', '').replace(',', '_')
- dest_state = split_line[2].replace('"', '').replace(',', '_')
- possible_events = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
- for event in possible_events.split("\\n"):
- event, *constr = event.split(";")
- if constr:
- key = _EventConstraintKey(states_dict[origin_state], events_dict[event])
- constraints[key] = constr
- # those events reset also on self loops
- if origin_state == dest_state and "reset" in "".join(constr):
- self.self_loop_reset_events.add(event)
- matrix[states_dict[origin_state]][events_dict[event]] = dest_state
- else:
- state = line.split("label")[1].split('"')[1]
- state, *constr = state.replace(" ", "").split("\\n")
- if constr:
- constraints[_StateConstraintKey(states_dict[state])] = constr
-
- return matrix, constraints
+ for transition in self.transitions:
+ src, dst = transition.src, transition.dst
+ event = transition.event
+ if src == dst and transition.reset:
+ # those events reset also on self loops
+ self.self_loop_reset_events.add(event)
+ matrix[states_dict[src]][events_dict[event]] = dst
+
+ return matrix
def __store_init_events(self) -> tuple[list[bool], list[bool]]:
events_start = [False] * len(self.events)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index a38ef735a861..dc6d6f33729b 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -403,7 +403,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
def __fill_constr_func(self) -> list[str]:
buff = []
- if not self.constraints:
+ if not self.has_invariant and not self.has_guard:
return []
buff.append(
--
2.47.3
^ permalink raw reply related
* [PATCH v3 06/13] verification/rvgen: Convert __fill_verify_guards_func() to Lark
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
Prepare to remove self.guards and self.__parse_constraints(), convert
__fill_verify_guards_func() to use the parsed transitions from Lark.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 38 +++++++++++++++++++------
1 file changed, 30 insertions(+), 8 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 1b29792ed630..e91717fde30d 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -221,6 +221,19 @@ class ha2k(dot2k):
def __parse_single_constraint(self, rule: dict, value: str) -> str:
return f"ha_get_env(ha_mon, {rule["env"]}{self.enum_suffix}, time_ns) {rule["op"]} {value}"
+ def __parse_guard_rule(self, rule) -> list[str]:
+ buff = []
+ for c, sep in rule.rules:
+ env = c.env + self.enum_suffix
+ op = c.op
+ val = self.__adjust_value(c.val, c.unit)
+
+ cond = f"ha_get_env(ha_mon, {env}, time_ns) {op} {val}"
+ if sep:
+ cond += f" {sep}"
+ buff.append(cond)
+ return buff
+
def __get_constraint_env(self, constr: str) -> str:
"""Extract the second argument from an ha_ function"""
env = constr.split("(")[1].split()[1].rstrip(")").rstrip(",")
@@ -287,7 +300,7 @@ class ha2k(dot2k):
rules = invalid_checks + rules
separator = "\n\t\t " if sum(len(r) for r in rules) > 80 else " "
- return ["res = " + separator.join(rules)]
+ return ["res = " + separator.join(rules) + ";"]
def __validate_constraint(self, key: tuple[int, int] | int, constr: str,
rule, reset) -> None:
@@ -406,7 +419,8 @@ f"""static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
def __fill_verify_guards_func(self) -> list[str]:
buff = []
- if not self.guards:
+
+ if not self.has_guard:
return []
buff.append(
@@ -418,14 +432,22 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
""")
_else = ""
- for edge, constr in sorted(self.guards.items()):
+ for transition in self.transitions:
+ if not transition.rule and not transition.reset:
+ continue
+
buff.append(f"\t{_else}if (curr_state == "
- f"{self.states[edge[0]]}{self.enum_suffix} && "
- f"event == {self.events[edge[1]]}{self.enum_suffix})")
- if constr.count(";") > 0:
+ f"{transition.src}{self.enum_suffix} && "
+ f"event == {transition.event}{self.enum_suffix})")
+ rule = transition.rule
+ reset = transition.reset
+ if rule and reset:
buff[-1] += " {"
- buff += [f"\t\t{c};" for c in constr.split(";")]
- if constr.count(";") > 0:
+ if rule:
+ buff.append("\t\t" + self.__format_guard_rules(self.__parse_guard_rule(rule))[0])
+ if reset:
+ buff.append(f"\t\tha_reset_env(ha_mon, {reset.env}{self.enum_suffix}, time_ns);")
+ if rule and reset:
_else = "} else "
else:
_else = "else "
--
2.47.3
^ permalink raw reply related
* [PATCH v3 10/13] verification/rvgen: Switch __get_event_variables() to Lark
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
Switch __get_event_variables() to use the parsed results from Lark, instead
of raw text processing.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 78 ++++++----------------
1 file changed, 19 insertions(+), 59 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index b86275e7bf28..2e26bb863245 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -591,45 +591,22 @@ class Automata:
def __get_event_variables(self) -> tuple[list[str], list[str]]:
events: list[str] = []
envs: list[str] = []
- # here we are at the begin of transitions, take a note, we will return later.
- cursor = self.__get_cursor_begin_events()
- for line in map(str.lstrip, islice(self.__dot_lines, cursor, None)):
- if not line.startswith('"'):
- break
+ for transition in self.transitions:
+ events.append(transition.event)
- # transitions have the format:
- # "all_fired" -> "both_fired" [ label = "disable_irq" ];
- # ------------ event is here ------------^^^^^
- split_line = line.split()
- if len(split_line) > 1 and split_line[1] == "->":
- event = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
-
- # when a transition has more than one label, they are like this
- # "local_irq_enable\nhw_local_irq_enable_n"
- # so split them.
-
- for i in event.split("\\n"):
- # if the event contains a constraint (hybrid automata),
- # it will be separated by a ";":
- # "sched_switch;x<1000;reset(x)"
- ev, *constr = i.split(";")
- if constr:
- if len(constr) > 2:
- raise AutomataError("Only 1 constraint and 1 reset are supported")
- envs += self.__extract_env_var(constr)
- events.append(ev)
- else:
- # state labels have the format:
- # "enable_fired" [label = "enable_fired\ncondition"];
- # ----- label is here -----^^^^^
- # label and node name must be the same, condition is optional
- state = line.split("label")[1].split('"')[1]
- _, *constr = state.split("\\n")
- if constr:
- if len(constr) > 1:
- raise AutomataError("Only 1 constraint is supported in the state")
- envs += self.__extract_env_var([constr[0].replace(" ", "")])
+ if transition.reset:
+ envs.append(transition.reset.env)
+ self.env_stored.add(transition.reset.env)
+ if transition.rule:
+ for c, _ in transition.rule.rules:
+ envs.append(c.env)
+ self.__extract_env_var(c)
+
+ for state in self._states:
+ if state.inv:
+ envs.append(state.inv.env)
+ self.__extract_env_var(state.inv)
return sorted(set(events)), sorted(set(envs))
@@ -653,28 +630,11 @@ class Automata:
seps.append(None)
return zip(exprs, seps)
- def __extract_env_var(self, constraint: list[str]) -> list[str]:
- env = []
- for c, _ in self._split_constraint_expr(constraint):
- rule = self.constraint_rule.search(c)
- reset = self.constraint_reset.search(c)
- if rule:
- env.append(rule["env"])
- if rule.groupdict().get("unit"):
- self.env_types[rule["env"]] = rule["unit"]
- if rule["val"][0].isalpha():
- self.constraint_vars.add(rule["val"])
- # try to infer unit from constants or parameters
- val_for_unit = rule["val"].lower().replace("()", "")
- if val_for_unit.endswith("_ns"):
- self.env_types[rule["env"]] = "ns"
- if val_for_unit.endswith("_jiffies"):
- self.env_types[rule["env"]] = "j"
- if reset:
- env.append(reset["env"])
- # environment variables that are reset need a storage
- self.env_stored.add(reset["env"])
- return env
+ def __extract_env_var(self, constraint: ConstraintCondition):
+ if constraint.unit:
+ self.env_types[constraint.env] = constraint.unit
+ if constraint.val[0].isalpha():
+ self.constraint_vars.add(constraint.val)
def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]:
# transform the array into a dictionary
--
2.47.3
^ permalink raw reply related
* [PATCH v3 08/13] verification/rvgen: Simplify the generation for clock variables
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
Hybrid automata monitors's clock variables have been changed to have
only a single representation. Now there is no need to generate code to
convert between the two representations.
Delete __fill_convert_inv_guard_func() and its associates. Update
__start_to_invariant_check() to how invariants now work.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 96 +------------------------
1 file changed, 3 insertions(+), 93 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index e91717fde30d..6d346a718a39 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -246,7 +246,9 @@ class ha2k(dot2k):
if inv.unit == "j":
clock_type = "jiffy"
- return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns)"
+ value = self.__adjust_value(inv.val, inv.unit)
+
+ return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {value})"
def __start_to_conv(self, constr: str) -> str:
"""
@@ -383,40 +385,6 @@ f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
buff.append("\treturn true;\n}\n")
return buff
- def __fill_convert_inv_guard_func(self) -> list[str]:
- buff = []
- if not self.invariants:
- return []
-
- conflict_guards, conflict_invs = self.__find_inv_conflicts()
- if not conflict_guards and not conflict_invs:
- return []
-
- buff.append(
-f"""static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
-\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
-\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
-{{""")
- buff.append("\tif (curr_state == next_state)\n\t\treturn;")
-
- _else = ""
- for state, constr in sorted(self.invariants.items()):
- # a state with invariant can reach us without reset
- # multiple conflicts must have the same invariant, otherwise we cannot
- # know how to reset the value
- conf_i = [start for start, end in conflict_invs if end == state]
- # we can reach a guard without reset
- conf_g = [e for s, e in conflict_guards if s == state]
- if not conf_i and not conf_g:
- continue
- buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
-
- buff.append(f"\t\t{self.__start_to_conv(constr)};")
- _else = "else "
-
- buff.append("}\n")
- return buff
-
def __fill_verify_guards_func(self) -> list[str]:
buff = []
@@ -456,54 +424,6 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
buff.append("\treturn res;\n}\n")
return buff
- def __find_inv_conflicts(self) -> tuple[set[tuple[int, _EventConstraintKey]],
- set[tuple[int, _StateConstraintKey]]]:
- """
- Run a breadth first search from all states with an invariant.
- Find any conflicting constraints reachable from there, this can be
- another state with an invariant or an edge with a non-reset guard.
- Stop when we find a reset.
-
- Return the set of conflicting guards and invariants as tuples of
- conflicting state and constraint key.
- """
- conflict_guards: set[tuple[int, _EventConstraintKey]] = set()
- conflict_invs: set[tuple[int, _StateConstraintKey]] = set()
- for start_idx in self.invariants:
- queue = deque([(start_idx, 0)]) # (state_idx, distance)
- env = self.__get_constraint_env(self.invariants[start_idx])
-
- while queue:
- curr_idx, distance = queue.popleft()
-
- # Check state condition
- if curr_idx != start_idx and curr_idx in self.invariants:
- conflict_invs.add((start_idx, _StateConstraintKey(curr_idx)))
- continue
-
- # Check if we should stop
- if distance > len(self.states):
- break
- if curr_idx != start_idx and distance > 1:
- continue
-
- for event_idx, next_state_name in enumerate(self.function[curr_idx]):
- if next_state_name == self.invalid_state_str:
- continue
- curr_guard = self.guards.get((curr_idx, event_idx), "")
- if "reset" in curr_guard and env in curr_guard:
- continue
-
- if env in curr_guard:
- conflict_guards.add((start_idx,
- _EventConstraintKey(curr_idx, event_idx)))
- continue
-
- next_idx = self.states.index(next_state_name)
- queue.append((next_idx, distance + 1))
-
- return conflict_guards, conflict_invs
-
def __fill_setup_invariants_func(self) -> list[str]:
if not self.has_invariant:
return []
@@ -554,16 +474,9 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
* the next state has a constraint, cancel it in any other case and to check
* that it didn't expire before the callback run. Transitions to the same state
* without a reset never affect timers.
- * Due to the different representations between invariants and guards, there is
- * a function to convert it in case invariants or guards are reachable from
- * another invariant without reset. Those are not present if not required in
- * the model. This is all automatic but is worth checking because it may show
- * errors in the model (e.g. missing resets).
*/""")
buff += self.__fill_verify_invariants_func()
- inv_conflicts = self.__fill_convert_inv_guard_func()
- buff += inv_conflicts
buff += self.__fill_verify_guards_func()
buff += self.__fill_setup_invariants_func()
@@ -576,9 +489,6 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
if self.invariants:
buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, "
"event, next_state, time_ns))\n\t\treturn false;\n")
- if inv_conflicts:
- buff.append("\tha_convert_inv_guard(ha_mon, curr_state, event, "
- "next_state, time_ns);\n")
if self.guards:
buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
--
2.47.3
^ permalink raw reply related
* [PATCH v3 05/13] verification/rvgen: Convert __fill_setup_invariants_func() to Lark
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
Prepare for self.invariants and __parse_constraints() to be removed.
convert __fill_setup_invariants_func() to use the new parsed states from
Lark.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 44 ++++++++++++++++++++-----
1 file changed, 35 insertions(+), 9 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 0595bfcd232e..1b29792ed630 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -250,6 +250,26 @@ class ha2k(dot2k):
return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.enum_suffix},"
f" {value}, time_ns)")
+ def __parse_invariant(self, inv):
+ # by default assume the timer has ns expiration
+ clock_type = "ns"
+ if inv.unit == "j":
+ clock_type = "jiffy"
+
+ env = inv.env + self.enum_suffix
+ val = inv.val.replace("()", "(ha_mon)")
+
+ match inv.unit:
+ case "us":
+ val *= 10**3
+ case "ms":
+ val *= 10**6
+ case "s":
+ val *= 10**9
+
+ return (f"ha_start_timer_{clock_type}(ha_mon, {env},"
+ f" {val}, time_ns)")
+
def __format_guard_rules(self, rules: list[str]) -> list[str]:
"""
Merge guard constraints as a single C return statement.
@@ -463,15 +483,14 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
return conflict_guards, conflict_invs
def __fill_setup_invariants_func(self) -> list[str]:
- buff = []
- if not self.invariants:
+ if not self.has_invariant:
return []
- buff.append(
+ buff = [
f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
-{{""")
+{{"""]
conditions = ["next_state == curr_state"]
conditions += [f"event != {e}{self.enum_suffix}"
@@ -480,13 +499,20 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
buff.append(f"\tif ({condition_str})\n\t\treturn;")
_else = ""
- for state, constr in sorted(self.invariants.items()):
- buff.append(f"\t{_else}if (next_state == {self.states[state]}{self.enum_suffix})")
- buff.append(f"\t\t{constr};")
+ for state in self._states:
+ inv = state.inv
+ if not inv:
+ continue
+ inv = self.__parse_invariant(inv)
+ buff.append(f"\t{_else}if (next_state == {state.name}{self.enum_suffix})")
+ buff.append(f"\t\t{inv};")
_else = "else "
- for state in self.invariants:
- buff.append(f"\telse if (curr_state == {self.states[state]}{self.enum_suffix})")
+ for state in self._states:
+ inv = state.inv
+ if not inv:
+ continue
+ buff.append(f"\telse if (curr_state == {state.name}{self.enum_suffix})")
buff.append("\t\tha_cancel_timer(ha_mon);")
buff.append("}\n")
--
2.47.3
^ permalink raw reply related
* [PATCH v3 04/13] verification/rvgen: Convert __fill_verify_invariants_func() to Lark
From: Nam Cao @ 2026-06-08 8:57 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
Convert __fill_verify_invariants_func() to use the parsed states
information from Lark, prepare to remove the old raw text parsing code.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
v3:
- remove unused import
---
tools/verification/rvgen/rvgen/dot2k.py | 32 ++++++++++++++++---------
1 file changed, 21 insertions(+), 11 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 110cfd69e53a..0595bfcd232e 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -12,6 +12,7 @@ from collections import deque
from .dot2c import Dot2c
from .generator import Monitor
from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
+from .automata import ConstraintCondition
class dot2k(Monitor, Dot2c):
@@ -177,6 +178,14 @@ class ha2k(dot2k):
raise AutomataError("Detected deterministic automaton, use the 'da' class")
self.trace_h = self._read_template_file("trace_hybrid.h")
self.__parse_constraints()
+ self.has_invariant = False
+ self.has_guard = False
+ for state in self._states:
+ if state.inv:
+ self.has_invariant = True
+ for transition in self.transitions:
+ if transition.rule or transition.reset:
+ self.has_guard = True
def fill_monitor_class_type(self) -> str:
if self._is_id_monitor():
@@ -218,14 +227,13 @@ class ha2k(dot2k):
assert env.removesuffix(f"_{self.name}") in self.envs
return env
- def __start_to_invariant_check(self, constr: str) -> str:
+ def __start_to_invariant_check(self, inv: ConstraintCondition) -> str:
# by default assume the timer has ns expiration
- env = self.__get_constraint_env(constr)
clock_type = "ns"
- if self.env_types.get(env.removesuffix(f"_{self.name}")) == "j":
+ if inv.unit == "j":
clock_type = "jiffy"
- return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)"
+ return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns)"
def __start_to_conv(self, constr: str) -> str:
"""
@@ -320,20 +328,22 @@ class ha2k(dot2k):
self.invariants[key] = rules[0]
def __fill_verify_invariants_func(self) -> list[str]:
- buff = []
- if not self.invariants:
+ if not self.has_invariant:
return []
- buff.append(
+ buff = [
f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
-{{""")
+{{"""]
_else = ""
- for state, constr in sorted(self.invariants.items()):
- check_str = self.__start_to_invariant_check(constr)
- buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
+ for state in self._states:
+ if not state.inv:
+ continue
+
+ check_str = self.__start_to_invariant_check(state.inv)
+ buff.append(f"\t{_else}if (curr_state == {state.name}{self.enum_suffix})")
buff.append(f"\t\t{check_str};")
_else = "else "
--
2.47.3
^ permalink raw reply related
* [PATCH v3 01/13] verification/rvgen: Switch LTL parser to Lark
From: Nam Cao @ 2026-06-08 8:56 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
The LTL parser is built using Ply. However, Ply is no longer
maintained [1].
Switch to use Lark instead. In addition to being actively maintained, Lark
also offers additional features (namely, automatically creating the
abstract syntax tree) which make the parser simpler.
Link: https://github.com/dabeaz/ply/commit/9d7c40099e23ff78f9d86ef69a26c1e8a83e706a [1]
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/__main__.py | 5 +-
tools/verification/rvgen/rvgen/ltl2ba.py | 202 +++++++++--------------
2 files changed, 82 insertions(+), 125 deletions(-)
diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 5c923dc10d0f..0915cf86e43b 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -14,6 +14,7 @@ if __name__ == '__main__':
from rvgen.container import Container
from rvgen.ltl2k import ltl2k
from rvgen.automata import AutomataError
+ from rvgen.ltl2ba import LTLError
import argparse
import sys
@@ -57,8 +58,8 @@ if __name__ == '__main__':
sys.exit(1)
else:
monitor = Container(vars(params))
- except AutomataError as e:
- print(f"There was an error processing {params.spec}: {e}", file=sys.stderr)
+ except (AutomataError, LTLError) as e:
+ print(f"There was an error processing {params.spec}:\n{e}", file=sys.stderr)
sys.exit(1)
print(f"Writing the monitor into the directory {monitor.name}")
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index 016e7cf93bbb..7cebda61bce8 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -7,9 +7,7 @@
# https://doi.org/10.1007/978-0-387-34892-6_1
# With extra optimizations
-from ply.lex import lex
-from ply.yacc import yacc
-from .automata import AutomataError
+import lark
# Grammar:
# ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
@@ -30,42 +28,41 @@ from .automata import AutomataError
# imply
# equivalent
-tokens = (
- 'AND',
- 'OR',
- 'IMPLY',
- 'UNTIL',
- 'ALWAYS',
- 'EVENTUALLY',
- 'NEXT',
- 'VARIABLE',
- 'LITERAL',
- 'NOT',
- 'LPAREN',
- 'RPAREN',
- 'ASSIGN',
-)
-
-t_AND = r'and'
-t_OR = r'or'
-t_IMPLY = r'imply'
-t_UNTIL = r'until'
-t_ALWAYS = r'always'
-t_NEXT = r'next'
-t_EVENTUALLY = r'eventually'
-t_VARIABLE = r'[A-Z_0-9]+'
-t_LITERAL = r'true|false'
-t_NOT = r'not'
-t_LPAREN = r'\('
-t_RPAREN = r'\)'
-t_ASSIGN = r'='
-t_ignore_COMMENT = r'\#.*'
-t_ignore = ' \t\n'
-
-def t_error(t):
- raise AutomataError(f"Illegal character '{t.value[0]}'")
-
-lexer = lex()
+GRAMMAR = r'''
+start: assign+
+
+assign: VARIABLE "=" _ltl
+
+_ltl: _opd | binop | unop
+
+_opd : VARIABLE
+ | LITERAL
+ | "(" _ltl ")"
+
+unop: UNOP _ltl
+UNOP: "always"
+ | "eventually"
+ | "next"
+ | "not"
+
+binop: _opd BINOP _ltl
+BINOP: "until"
+ | "and"
+ | "or"
+ | "imply"
+
+VARIABLE: /[A-Z_][A-Z0-9_]*/
+LITERAL: "true" | "false"
+
+COMMENT: "#" /.*/ "\n"
+%ignore COMMENT
+
+%import common.WS
+%ignore WS
+'''
+
+class LTLError(Exception):
+ "Exception raised for malformed linear temporal logic"
class GraphNode:
uid = 0
@@ -97,7 +94,7 @@ class GraphNode:
return self.id < other.id
class ASTNode:
- uid = 1
+ uid = 0
def __init__(self, op):
self.op = op
@@ -433,90 +430,49 @@ class Literal:
node.old |= {n}
return node.expand(node_set)
-def p_spec(p):
- '''
- spec : assign
- | assign spec
- '''
- if len(p) == 3:
- p[2].append(p[1])
- p[0] = p[2]
- else:
- p[0] = [p[1]]
-
-def p_assign(p):
- '''
- assign : VARIABLE ASSIGN ltl
- '''
- p[0] = (p[1], p[3])
-
-def p_ltl(p):
- '''
- ltl : opd
- | binop
- | unop
- '''
- p[0] = p[1]
-
-def p_opd(p):
- '''
- opd : VARIABLE
- | LITERAL
- | LPAREN ltl RPAREN
- '''
- if p[1] == "true":
- p[0] = ASTNode(Literal(True))
- elif p[1] == "false":
- p[0] = ASTNode(Literal(False))
- elif p[1] == '(':
- p[0] = p[2]
- else:
- p[0] = ASTNode(Variable(p[1]))
-
-def p_unop(p):
- '''
- unop : ALWAYS ltl
- | EVENTUALLY ltl
- | NEXT ltl
- | NOT ltl
- '''
- if p[1] == "always":
- op = AlwaysOp(p[2])
- elif p[1] == "eventually":
- op = EventuallyOp(p[2])
- elif p[1] == "next":
- op = NextOp(p[2])
- elif p[1] == "not":
- op = NotOp(p[2])
- else:
- raise AutomataError(f"Invalid unary operator {p[1]}")
-
- p[0] = ASTNode(op)
-
-def p_binop(p):
- '''
- binop : opd UNTIL ltl
- | opd AND ltl
- | opd OR ltl
- | opd IMPLY ltl
- '''
- if p[2] == "and":
- op = AndOp(p[1], p[3])
- elif p[2] == "until":
- op = UntilOp(p[1], p[3])
- elif p[2] == "or":
- op = OrOp(p[1], p[3])
- elif p[2] == "imply":
- op = ImplyOp(p[1], p[3])
- else:
- raise AutomataError(f"Invalid binary operator {p[2]}")
-
- p[0] = ASTNode(op)
-
-parser = yacc()
+class Transform(lark.visitors.Transformer):
+ def unop(self, node):
+ if node[0] == "always":
+ return ASTNode(AlwaysOp(node[1]))
+ if node[0] == "eventually":
+ return ASTNode(EventuallyOp(node[1]))
+ if node[0] == "next":
+ return ASTNode(NextOp(node[1]))
+ if node[0] == "not":
+ return ASTNode(NotOp(node[1]))
+ raise ValueError("Unknown operator %s" % node[0])
+
+ def binop(self, node):
+ if node[1] == "until":
+ return ASTNode(UntilOp(node[0], node[2]))
+ if node[1] == "and":
+ return ASTNode(AndOp(node[0], node[2]))
+ if node[1] == "or":
+ return ASTNode(OrOp(node[0], node[2]))
+ if node[1] == "imply":
+ return ASTNode(ImplyOp(node[0], node[2]))
+ raise ValueError("Unknown operator %s" % node[1])
+
+ def VARIABLE(self, args):
+ return ASTNode(Variable(args))
+
+ def LITERAL(self, args):
+ return ASTNode(Literal(args == "true"))
+
+ def start(self, node):
+ return node
+
+ def assign(self, node):
+ return node[0].op.name, node[1]
+
+parser = lark.Lark(GRAMMAR)
def parse_ltl(s: str) -> ASTNode:
- spec = parser.parse(s)
+ try:
+ spec = parser.parse(s)
+ except lark.exceptions.UnexpectedInput as e:
+ raise LTLError(str(e))
+ spec = Transform().transform(spec)
rule = None
subexpr = {}
@@ -528,7 +484,7 @@ def parse_ltl(s: str) -> ASTNode:
subexpr[assign[0]] = assign[1]
if rule is None:
- raise AutomataError("Please define your specification in the \"RULE = <LTL spec>\" format")
+ raise LTLError("Please define your specification in the \"RULE = <LTL spec>\" format")
for node in rule:
if not isinstance(node.op, Variable):
--
2.47.3
^ permalink raw reply related
* [PATCH v3 03/13] verification/rvgen: Implement state and transition parser based on Lark
From: Nam Cao @ 2026-06-08 8:56 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
The DOT parsing scripts directly parse the raw text and they are quite
fragile. If the input dot files' formats are slightly changed (for
instance, by breaking long some lines which is allowed by the DOT
language), the scripts would fail.
Prepare to move away from the raw text processing, implement parsers based
on Lark which parse states, transitions and constraints.
The parse results are not used yet. The existing scripts will be converted
one by one to them, and the raw text processing will eventually be removed.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 216 +++++++++++++++++++++
1 file changed, 216 insertions(+)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 8649d982383d..b86275e7bf28 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -198,6 +198,164 @@ class ParseTree:
self.node_attrs = attributes_parser.node_attrs
self.edge_attrs = attributes_parser.edge_attrs
+class ConstraintCondition:
+ def __init__(self, env: str, op: str, val: str, unit=None):
+ self.env = env
+ self.op = op
+ self.val = val
+ self.unit = unit
+ if unit is None:
+ # try to infer unit from constants or parameters
+ val_for_unit = val.lower().replace("()", "")
+ if val_for_unit.endswith("_ns"):
+ self.unit = "ns"
+ if val_for_unit.endswith("_jiffies"):
+ self.unit = "j"
+
+class ConstraintRule:
+ grammar = r'''
+ rule: condition (OP condition)*
+
+ OP: "&&" | "||"
+
+ condition: ENV CMP_OP VAL UNIT?
+
+ ENV: CNAME
+
+ CMP_OP: "==" | "<=" | "<" | ">=" | ">"
+
+ VAL: /[0-9]+/
+ | /[A-Z_]+\(\)/
+ | /[A-Z_]+/
+ | /[a-z_]+\(\)/
+ | /[a-z_]+/
+
+ UNIT: "ns" | "us" | "ms" | "s"
+ '''
+
+ def __init__(self, c: ConstraintCondition):
+ '''
+ A list of pairs of
+ - the condition (e.g. is_constr_dl == 1)
+ - the logical operator ("||" or "&&") combining this
+ condition with the next one if it exists, otherwise None
+
+ TODO: Perhaps use an abstract syntax tree instead, because
+ this representation cannot capture precedence
+ '''
+ self.rules = [[c, None]]
+
+ def chain(self, op: str, c: ConstraintCondition):
+ self.rules[-1][1] = op
+ self.rules.append([c, None])
+
+class ConstraintReset:
+ def __init__(self, env):
+ self.env = env
+
+class StateLabelParser:
+ grammar = r'''
+ label: CNAME ("\\n" condition)?
+
+ %import common.CNAME
+ %import common.WS
+ %ignore WS
+ ''' + ConstraintRule.grammar
+
+ parser = lark.Lark(grammar, parser='lalr', start="label")
+
+ def __init__(self, label: str):
+ try:
+ tree = self.parser.parse(label)
+ except lark.exceptions.UnexpectedInput as exc:
+ raise(AutomataError(f"Unrecognised state \"{label}\"\n{exc}"))
+
+ self.state = tree.children[0]
+ self.constraint = None
+
+ if len(tree.children) == 2:
+ self.constraint = ConstraintCondition(*tree.children[1].children)
+ if self.constraint.op not in ("<", "<="):
+ raise AutomataError("State constraints must be clock expirations like"
+ f" clk<N ({label})")
+
+class EventLabelParser:
+ grammar = r'''
+ events: event ("\\n" event)*
+
+ event: name (";" guard)?
+
+ guard: reset
+ | rule
+ | rule ";" reset
+ | reset ";" rule
+
+ name: CNAME
+
+ reset: "reset" "(" ENV ")"
+
+ %import common.CNAME
+ %import common.WS
+ %ignore WS
+ ''' + ConstraintRule.grammar
+
+ parser = lark.Lark(grammar, parser='lalr', start="events")
+
+ class GetEvents(lark.visitors.Transformer):
+ def guard(self, args):
+ reset = None
+ rule = None
+ for arg in args:
+ if arg.data == "reset":
+ reset = ConstraintReset(arg.children[0])
+ elif arg.data == "rule":
+ conditions = arg.children
+ rule = ConstraintRule(conditions[0])
+ for i in range(1, len(conditions), 2):
+ rule.chain(conditions[i], conditions[i + 1])
+ return reset, rule
+
+ def OP(self, args):
+ return args
+
+ def condition(self, args):
+ return ConstraintCondition(*args)
+
+ def event(self, args):
+ assert(len(args) <= 2)
+ name = args[0]
+ rule, reset = None, None
+ if len(args) == 2:
+ reset, rule = args[1]
+ return name, reset, rule
+
+ def events(self, args):
+ return args
+
+ def name(self, args):
+ return args[0]
+
+ def __init__(self, label: str):
+ try:
+ tree = self.parser.parse(label)
+ self.events = self.GetEvents().transform(tree)
+ except lark.exceptions.UnexpectedInput as exc:
+ raise(AutomataError(f"Unrecognised event \"{label}\"\n{exc}"))
+
+class Transition:
+ def __init__(self, src: str, dst: str, event: str,
+ reset: ConstraintReset, rule: ConstraintRule):
+ self.src = src
+ self.dst = dst
+ self.event = event
+ self.rule = rule
+ self.reset = reset
+
+class State:
+ def __init__(self, name: str, inv: ConstraintCondition):
+ self.name = name
+ self.inv = inv
+
class _ConstraintKey:
"""Base class for constraint keys."""
@@ -252,6 +410,8 @@ class Automata:
self.name = model_name or self.__get_model_name()
self.__dot_lines = self.__open_dot()
self.__parse_tree = ParseTree(file_path)
+ self.transitions = self.__parse_transitions()
+ self._states, self._initial_state, self._final_states = self.__parse_states()
self.states, self.initial_state, self.final_states = self.__get_state_variables()
self.env_types = {}
self.env_stored = set()
@@ -327,6 +487,62 @@ class Automata:
return cursor
+ def __parse_transitions(self):
+ transitions = []
+
+ for edge in self.__parse_tree.edges:
+ attr = self.__parse_tree.edge_attrs.get(edge)
+ if not attr:
+ continue
+
+ label = attr.get("label")
+
+ src, dst = edge
+
+ parser = EventLabelParser(label)
+ for event, reset, rule in parser.events:
+ transitions.append(Transition(src, dst, event, reset, rule))
+
+ transitions.sort(key=lambda t : (t.src, t.event))
+ return transitions
+
+ def __parse_states(self):
+ initial_state = ""
+ states = []
+ final_states = []
+
+ for node in self.__parse_tree.nodes:
+ attr = self.__parse_tree.node_attrs[node]
+ label = attr.get("label")
+
+ if node.startswith(Automata.init_marker):
+ initial_state = node[len(Automata.init_marker):]
+
+ if not label:
+ continue
+
+ parser = StateLabelParser(label)
+ state = State(parser.state, parser.constraint)
+
+ states.append(state)
+
+ shape = attr.get("shape")
+ if shape in ("doublecircle", "ellipse"):
+ final_states.append(state)
+
+
+ initial_state = next((s for s in states if s.name == initial_state), None)
+ if not initial_state:
+ raise AutomataError("The automaton doesn't have an initial state")
+
+ if not final_states:
+ final_states.append(initial_state)
+
+ states.remove(initial_state)
+ states.sort(key=lambda s : s.name)
+ states.insert(0, initial_state)
+ return states, initial_state, final_states
+
def __get_state_variables(self) -> tuple[list[str], str, list[str]]:
# wait for node declaration
states = []
--
2.47.3
^ permalink raw reply related
* [PATCH v3 02/13] verification/rvgen: Introduce a parse tree for automata using Lark
From: Nam Cao @ 2026-06-08 8:56 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1780908661.git.namcao@linutronix.de>
The DOT parsing scripts directly parse the raw text and they are quite
fragile. If the input dot files' formats are slightly changed (for
instance, by breaking long some lines which is allowed by the DOT language
defined by graphviz), the scripts would fail.
To make the scripts robust, the parser should be implemented based on the
dot language specification, not based on how the existing dot files look.
As a first step, use Lark to implement a Parser based on the graphviz dot
language specification. The resulting parse tree is not used yet, but the
existing scripts will be converted one by one to use this new parse tree in
the follow-up commits.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 186 +++++++++++++++++++++
1 file changed, 186 insertions(+)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index b9f8149f7118..8649d982383d 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -13,6 +13,191 @@ import re
from typing import Iterator
from itertools import islice
+import lark
+
+class ParseTree:
+ # based on https://graphviz.org/doc/info/lang.html
+ # with the irrelevant stuffs (port and compass) removed
+ grammar = r'''
+ start: "strict"? ("graph" | "digraph") ID? "{" stmt_list "}"
+
+ stmt_list: (stmt ";"? stmt_list)?
+
+ stmt: node_stmt
+ | edge_stmt
+ | attr_stmt
+ | ID "=" ID
+ | subgraph
+
+ attr_stmt: attr_type attr_list
+
+ attr_type: "graph" -> graph
+ | "node" -> node
+ | "edge" -> edge
+
+ attr_list: "[" a_list? "]" attr_list?
+
+ a_list: ID "=" ID (";" | ",")? a_list?
+
+ edge_stmt: (node_id | subgraph) edgerhs attr_list?
+
+ edgerhs: edgeop (node_id | subgraph) edgerhs?
+
+ edgeop: "->" | "--"
+
+ node_stmt: node_id attr_list?
+
+ node_id: ID
+
+ subgraph: ("subgraph" ID?)? "{" stmt_list "}"
+
+ ID: CNAME
+ | /-?(\.[0-9]+|[0-9]+(\.[0-9]*))/
+ | ESCAPED_STRING
+
+ %import common.CNAME
+ %import common.ESCAPED_STRING
+ %import common.WS
+ %ignore WS
+ '''
+
+ @staticmethod
+ def parse_edge(tree: lark.Tree) -> tuple[str, str]:
+ # only support a simple node-to-node edge
+ nodes = []
+ for node in tree.iter_subtrees_topdown():
+ if node.data == "node_id":
+ nodes.append(node.children[0].strip('"'))
+
+ if len(nodes) != 2:
+ raise AutomataError("Only state-to-state transition is supported")
+
+ return tuple(nodes)
+
+ class ParseNodes(lark.visitors.Visitor):
+ def __init__(self, *args, **kwargs):
+ self.nodes = set()
+ super().__init__(*args, **kwargs)
+
+ def node_stmt(self, tree):
+ node_id = tree.children[0]
+ node = node_id.children[0].strip('"')
+ self.nodes.add(node)
+
+ class ParseEdges(lark.visitors.Visitor):
+ def __init__(self, *args, **kwargs):
+ self.edges = set()
+ super().__init__(*args, **kwargs)
+
+ def edge_stmt(self, tree):
+ edge = ParseTree.parse_edge(tree)
+ self.edges.add(edge)
+
+ class ParseAttributes(lark.visitors.Interpreter):
+ def __init__(self, *args, **kwargs):
+ '''
+ Stacks of default attributes. [0] is the default
+ attributes for the outermost scope, while [-1] is the
+ default attributes for the current scope.
+ '''
+ self.default_node_attrs = [{}]
+ self.default_edge_attrs = [{}]
+
+ self.node_attrs = {}
+ self.edge_attrs = {}
+
+ super().__init__(*args, **kwargs)
+
+ @staticmethod
+ def __get_attrs(stmt: lark.Tree) -> dict[str, str]:
+ attrs = {}
+
+ for node in stmt.iter_subtrees():
+ if node.data == "a_list":
+ attrs[node.children[0]] = node.children[1].strip('"')
+
+ return attrs
+
+
+ def subgraph(self, tree):
+ # We are entering a new scope, inherit the default
+ # attributes of the outer scope
+ self.default_node_attrs.append(self.default_node_attrs[-1].copy())
+ self.default_edge_attrs.append(self.default_edge_attrs[-1].copy())
+
+ children = self.visit_children(tree)
+
+ # Exiting the scope
+ del self.default_node_attrs[-1]
+ del self.default_edge_attrs[-1]
+
+ return children
+
+ def node_stmt(self, tree):
+ node_id = tree.children[0]
+ node = node_id.children[0].strip('"')
+
+ attrs = self.default_node_attrs[-1].copy()
+ attrs |= self.__get_attrs(tree)
+
+ if attrs:
+ if node in self.node_attrs:
+ self.node_attrs[node] = attrs | self.node_attrs[node]
+ else:
+ self.node_attrs[node] = attrs
+
+ return self.visit_children(tree)
+
+ def edge_stmt(self, tree):
+ edge = ParseTree.parse_edge(tree)
+
+ attrs = self.default_edge_attrs[-1].copy()
+ attrs |= self.__get_attrs(tree)
+
+ if attrs:
+ if edge in self.edge_attrs:
+ self.edge_attrs[edge] = attrs | self.edge_attrs[edge]
+ else:
+ self.edge_attrs[edge] = attrs
+
+ return self.visit_children(tree)
+
+ def attr_stmt(self, tree):
+ attr_type = tree.children[0].data
+ attrs = self.__get_attrs(tree)
+
+ if attr_type == "node":
+ self.default_node_attrs[-1] |= attrs
+ elif attr_type == "edge":
+ self.default_edge_attrs[-1] |= attrs
+ else:
+ # graph attributes are irrelevant
+ pass
+
+ self.visit_children(tree)
+
+ def __init__(self, dot_file):
+ parser = lark.Lark(self.grammar, parser='lalr')
+ node_parser = self.ParseNodes()
+ edge_parser = self.ParseEdges()
+ attributes_parser = self.ParseAttributes()
+
+ try:
+ with open(dot_file, "r") as f:
+ tree = parser.parse(f.read())
+ attributes_parser.visit(tree)
+ node_parser.visit(tree)
+ edge_parser.visit(tree)
+ except OSError as exc:
+ raise AutomataError(exc.strerror) from exc
+ except lark.exceptions.UnexpectedInput as exc:
+ raise AutomataError(str(exc))
+
+ self.nodes = node_parser.nodes
+ self.edges = edge_parser.edges
+ self.node_attrs = attributes_parser.node_attrs
+ self.edge_attrs = attributes_parser.edge_attrs
+
class _ConstraintKey:
"""Base class for constraint keys."""
@@ -66,6 +251,7 @@ class Automata:
self.__dot_path = file_path
self.name = model_name or self.__get_model_name()
self.__dot_lines = self.__open_dot()
+ self.__parse_tree = ParseTree(file_path)
self.states, self.initial_state, self.final_states = self.__get_state_variables()
self.env_types = {}
self.env_stored = set()
--
2.47.3
^ permalink raw reply related
* [PATCH v3 00/13] rv: Convert rvgen to Lark
From: Nam Cao @ 2026-06-08 8:56 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
This series converts the linear temporal logic parser and the automata
parser into using Lark.
The LTL parser has been using ply - a parsing library. However, ply
was recently announced to be abandoned. Furthermore, ply does not
offer the features that lark has.
On the other hand, the automata parser is mostly raw text processing
which is quite fragile. For instance, by slightly deform wwnr.dot (but
does not make it an invalid dot file):
digraph state_automaton {
{node [shape = plaintext, style=invis, label=""] "__init_not_running"};
{node [shape = ellipse]
"not_running"};
{node [shape=plaintext] "not_running"};
{node [shape = plaintext] "running"};
"__init_not_running"
-> "not_running";
"not_running" [label = "not_running", color = green3];
"not_running" ->
"not_running" [ label = "wakeup" ];
"not_running" -> "running" [ label = "switch_in" ];
"running" [label = "running"];
"running" -> "not_running" [ label = "switch_out" ];
}
the parser would be broken. Furthermore, the code is a bit hard to
follow with raw text being stored in lots of variables and sometimes
it is hard to figure out what sort of text is stored in the variables
while reading the code.
This motivates me to convert the automata parser as well. The plan is:
- Introduce Lark and prepare the parsed states, transitions and
constraints
- Convert the parser piece by piece to the parsed results from Lark
- Delete the old code
I struggled with converting __find_inv_conflicts(). So I decided to
remove the dual clock representation in the HA monitors, which allows
me to delete __find_inv_conflicts() entirely. This makes the code
simpler overall.
After the series, the generated HA monitors are mostly unchanged,
except:
- Clock representation conversion is gone and
ha_check_invariant_[ns|jiffy]() takes a new argument
- The ordering in ha_verify_guards() is changed, but still
equivalent. This is because it is now sorted lexically.
The generated LTL monitors are sadly significantly different, but proved to
be equivalent with runtime testing. Further work will make LTL monitor
generation more consistent.
v3..v2: https://lore.kernel.org/lkml/cover.1779956342.git.namcao@linutronix.de/
- remove some redundant imports
- fix build failure due to passing wrong parameters to ha_invariant_passed_jiffy()
v2..v1: https://lore.kernel.org/lkml/cover.1777962130.git.namcao@linutronix.de/
- address human's reviews and sashiko's reviews
- handle lark's exception, yielding a much better error message
Nam Cao (13):
verification/rvgen: Switch LTL parser to Lark
verification/rvgen: Introduce a parse tree for automata using Lark
verification/rvgen: Implement state and transition parser based on
Lark
verification/rvgen: Convert __fill_verify_invariants_func() to Lark
verification/rvgen: Convert __fill_setup_invariants_func() to Lark
verification/rvgen: Convert __fill_verify_guards_func() to Lark
rv: Simplify hybrid automata monitors's clock variables
verification/rvgen: Simplify the generation for clock variables
verification/rvgen: Delete __parse_constraint()
verification/rvgen: Switch __get_event_variables() to Lark
verification/rvgen: Switch __create_matrix() to Lark
verification/rvgen: Remove the old state variables
verification/rvgen: Remove dead code
include/rv/ha_monitor.h | 64 +-
kernel/trace/rv/monitors/nomiss/nomiss.c | 18 +-
kernel/trace/rv/monitors/stall/stall.c | 2 +-
tools/verification/rvgen/__main__.py | 5 +-
tools/verification/rvgen/rvgen/automata.py | 643 +++++++++++++--------
tools/verification/rvgen/rvgen/dot2c.py | 10 +-
tools/verification/rvgen/rvgen/dot2k.py | 290 +++-------
tools/verification/rvgen/rvgen/ltl2ba.py | 202 +++----
8 files changed, 604 insertions(+), 630 deletions(-)
--
2.47.3
^ permalink raw reply
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