* [PATCH v2 4/4] rv/rtapp: Add wakeup monitor
From: Nam Cao @ 2026-06-19 7:21 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, linux-trace-kernel, linux-doc,
linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781852967.git.namcao@linutronix.de>
Add a wakeup monitor to detect a lower-priority task waking up a
higher-priority task.
The rtapp/sleep monitor already detects this. However, that monitor
triggers an error in the context of the wakee task and user only gets
the stacktrace of that task. It is also extremely useful to get the
stacktrace of the waker task, which this monitor offers. In other
words, this monitor complements the rtapp/sleep monitor.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Documentation/trace/rv/monitor_rtapp.rst | 20 +++
kernel/trace/rv/Kconfig | 1 +
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/monitors/rtapp/Kconfig | 2 +-
kernel/trace/rv/monitors/wakeup/Kconfig | 16 ++
kernel/trace/rv/monitors/wakeup/wakeup.c | 153 ++++++++++++++++++
kernel/trace/rv/monitors/wakeup/wakeup.h | 92 +++++++++++
.../trace/rv/monitors/wakeup/wakeup_trace.h | 14 ++
kernel/trace/rv/rv_trace.h | 1 +
tools/verification/models/rtapp/wakeup.ltl | 5 +
10 files changed, 304 insertions(+), 1 deletion(-)
create mode 100644 kernel/trace/rv/monitors/wakeup/Kconfig
create mode 100644 kernel/trace/rv/monitors/wakeup/wakeup.c
create mode 100644 kernel/trace/rv/monitors/wakeup/wakeup.h
create mode 100644 kernel/trace/rv/monitors/wakeup/wakeup_trace.h
create mode 100644 tools/verification/models/rtapp/wakeup.ltl
diff --git a/Documentation/trace/rv/monitor_rtapp.rst b/Documentation/trace/rv/monitor_rtapp.rst
index 502d3ea412eb..238b59395ff5 100644
--- a/Documentation/trace/rv/monitor_rtapp.rst
+++ b/Documentation/trace/rv/monitor_rtapp.rst
@@ -124,3 +124,23 @@ to handle some special cases:
real-time-safe because preemption is disabled for the duration.
- `FUTEX_LOCK_PI` is included in the allowlist for the same reason as
`BLOCK_ON_RT_MUTEX`.
+
+Monitor wakeup
+++++++++++++++
+
+The `wakeup` monitor reports real-time threads being woken by lower-priority threads,
+which is a hint of priority inversion. Its specification is::
+
+ RULE = always (((RT and USER_THREAD) imply
+ (not (WOKEN_BY_LOWER_PRIO or WOKEN_BY_SOFTIRQ)) or ALLOWLIST))
+
+ ALLOWLIST = BLOCK_ON_RT_MUTEX
+ or FUTEX_LOCK_PI
+
+The `sleep` monitor already reports this type of problem. The difference is the
+context in which the problem is reported. While the `sleep` monitor reports the problem
+in the context of the wakee, this `wakeup` monitor reports the problem in the context of
+the waker. This monitor complement the `sleep` monitor, giving user better
+understanding of the issue. For instance, to debug a lower-priority task waking a
+higher-priority task scenario, user can enable both `wakeup` monitor and `sleep`
+monitor to get the stack traces of both tasks.
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 3884b14df375..4d3a14a0bac2 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -76,6 +76,7 @@ source "kernel/trace/rv/monitors/opid/Kconfig"
source "kernel/trace/rv/monitors/rtapp/Kconfig"
source "kernel/trace/rv/monitors/pagefault/Kconfig"
source "kernel/trace/rv/monitors/sleep/Kconfig"
+source "kernel/trace/rv/monitors/wakeup/Kconfig"
# Add new rtapp monitors here
source "kernel/trace/rv/monitors/stall/Kconfig"
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index 94498da35b37..c2c0e4142eb4 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -20,6 +20,7 @@ obj-$(CONFIG_RV_MON_OPID) += monitors/opid/opid.o
obj-$(CONFIG_RV_MON_STALL) += monitors/stall/stall.o
obj-$(CONFIG_RV_MON_DEADLINE) += monitors/deadline/deadline.o
obj-$(CONFIG_RV_MON_NOMISS) += monitors/nomiss/nomiss.o
+obj-$(CONFIG_RV_MON_WAKEUP) += monitors/wakeup/wakeup.o
# Add new monitors here
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
diff --git a/kernel/trace/rv/monitors/rtapp/Kconfig b/kernel/trace/rv/monitors/rtapp/Kconfig
index 1ce9370a9ba8..1fcd7a400ded 100644
--- a/kernel/trace/rv/monitors/rtapp/Kconfig
+++ b/kernel/trace/rv/monitors/rtapp/Kconfig
@@ -1,6 +1,6 @@
config RV_MON_RTAPP
depends on RV
- depends on RV_PER_TASK_MONITORS >= 2
+ depends on RV_PER_TASK_MONITORS >= 3
bool "rtapp monitor"
help
Collection of monitors to check for common problems with real-time
diff --git a/kernel/trace/rv/monitors/wakeup/Kconfig b/kernel/trace/rv/monitors/wakeup/Kconfig
new file mode 100644
index 000000000000..ec3a5c06a8c4
--- /dev/null
+++ b/kernel/trace/rv/monitors/wakeup/Kconfig
@@ -0,0 +1,16 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_WAKEUP
+ depends on RV
+ depends on RV_MON_RTAPP
+ depends on HAVE_SYSCALL_TRACEPOINTS
+ default y
+ select LTL_MON_EVENTS_ID
+ bool "wakeup monitor"
+ help
+ This monitor detects a lower-priority task waking up a
+ higher-priority task. The RV_MON_SLEEP monitor already
+ detects this case, but this monitor detects in the context
+ of the waker task instead. This and RV_MON_SLEEP can be
+ enabled together to get the stacktrace of both the waker
+ task and the wakee task.
diff --git a/kernel/trace/rv/monitors/wakeup/wakeup.c b/kernel/trace/rv/monitors/wakeup/wakeup.c
new file mode 100644
index 000000000000..01b47416f24e
--- /dev/null
+++ b/kernel/trace/rv/monitors/wakeup/wakeup.c
@@ -0,0 +1,153 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "wakeup"
+
+#include <trace/events/syscalls.h>
+#include <trace/events/sched.h>
+#include <trace/events/lock.h>
+#include <uapi/linux/futex.h>
+
+#include <rv_trace.h>
+#include <monitors/rtapp/rtapp.h>
+
+
+#ifndef __NR_futex
+#define __NR_futex (-__COUNTER__)
+#endif
+#ifndef __NR_futex_time64
+#define __NR_futex_time64 (-__COUNTER__)
+#endif
+
+#include "wakeup.h"
+#include <rv/ltl_monitor.h>
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+ /*
+ * This includes "actual" real-time tasks and also PI-boosted
+ * tasks. A task being PI-boosted means it is blocking an "actual"
+ * real-task, therefore it should also obey the monitor's rule,
+ * otherwise the "actual" real-task may be delayed.
+ */
+ ltl_atom_set(mon, LTL_RT, rt_or_dl_task(task));
+}
+
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+{
+ ltl_atom_set(mon, LTL_WOKEN_BY_LOWER_PRIO, false);
+ ltl_atom_set(mon, LTL_WOKEN_BY_SOFTIRQ, false);
+
+ if (task_creation) {
+ ltl_atom_set(mon, LTL_BLOCK_ON_RT_MUTEX, false);
+ ltl_atom_set(mon, LTL_FUTEX_LOCK_PI, false);
+ }
+
+ ltl_atom_set(mon, LTL_USER_THREAD, !(task->flags & PF_KTHREAD));
+}
+
+static void handle_sched_waking(void *data, struct task_struct *task)
+{
+ if (in_task()) {
+ if (current->prio > task->prio)
+ ltl_atom_pulse(task, LTL_WOKEN_BY_LOWER_PRIO, true);
+ } else if (in_serving_softirq()) {
+ ltl_atom_pulse(task, LTL_WOKEN_BY_SOFTIRQ, true);
+ }
+}
+
+static void handle_contention_begin(void *data, void *lock, unsigned int flags)
+{
+ if (flags & LCB_F_RT)
+ ltl_atom_update(current, LTL_BLOCK_ON_RT_MUTEX, true);
+}
+
+static void handle_contention_end(void *data, void *lock, int ret)
+{
+ ltl_atom_update(current, LTL_BLOCK_ON_RT_MUTEX, false);
+}
+
+static void handle_sys_enter(void *data, struct pt_regs *regs, long id)
+{
+ unsigned long args[6];
+ int op, cmd;
+
+ switch (id) {
+ case __NR_futex:
+ case __NR_futex_time64:
+ syscall_get_arguments(current, regs, args);
+ op = args[1];
+ cmd = op & FUTEX_CMD_MASK;
+
+ switch (cmd) {
+ case FUTEX_LOCK_PI:
+ case FUTEX_LOCK_PI2:
+ ltl_atom_update(current, LTL_FUTEX_LOCK_PI, true);
+ break;
+ }
+ break;
+ }
+}
+
+static void handle_sys_exit(void *data, struct pt_regs *regs, long ret)
+{
+ ltl_atom_update(current, LTL_FUTEX_LOCK_PI, false);
+}
+
+static int enable_wakeup(void)
+{
+ int retval;
+
+ retval = ltl_monitor_init();
+ if (retval)
+ return retval;
+
+ rv_attach_trace_probe("rtapp_wakeup", sched_waking, handle_sched_waking);
+ rv_attach_trace_probe("rtapp_wakeup", contention_begin, handle_contention_begin);
+ rv_attach_trace_probe("rtapp_wakeup", contention_end, handle_contention_end);
+ rv_attach_trace_probe("rtapp_wakeup", sys_enter, handle_sys_enter);
+ rv_attach_trace_probe("rtapp_wakeup", sys_exit, handle_sys_exit);
+
+ return 0;
+}
+
+static void disable_wakeup(void)
+{
+ rv_detach_trace_probe("rtapp_wakeup", sched_waking, handle_sched_waking);
+ rv_detach_trace_probe("rtapp_wakeup", contention_begin, handle_contention_begin);
+ rv_detach_trace_probe("rtapp_wakeup", contention_end, handle_contention_end);
+ rv_detach_trace_probe("rtapp_wakeup", sys_enter, handle_sys_enter);
+ rv_detach_trace_probe("rtapp_wakeup", sys_exit, handle_sys_exit);
+
+ ltl_monitor_destroy();
+}
+
+static struct rv_monitor rv_wakeup = {
+ .name = "wakeup",
+ .description = "Monitor that real-time tasks are not woken by lower-priority tasks",
+ .enable = enable_wakeup,
+ .disable = disable_wakeup,
+};
+
+static int __init register_wakeup(void)
+{
+ return rv_register_monitor(&rv_wakeup, &rv_rtapp);
+}
+
+static void __exit unregister_wakeup(void)
+{
+ rv_unregister_monitor(&rv_wakeup);
+}
+
+module_init(register_wakeup);
+module_exit(unregister_wakeup);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Nam Cao <namcao@linutronix.de>");
+MODULE_DESCRIPTION("Monitor that real-time tasks are not woken by lower-priority tasks");
diff --git a/kernel/trace/rv/monitors/wakeup/wakeup.h b/kernel/trace/rv/monitors/wakeup/wakeup.h
new file mode 100644
index 000000000000..6f80da64e0e1
--- /dev/null
+++ b/kernel/trace/rv/monitors/wakeup/wakeup.h
@@ -0,0 +1,92 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * C implementation of Buchi automaton, automatically generated by
+ * tools/verification/rvgen from the linear temporal logic specification.
+ * For further information, see kernel documentation:
+ * Documentation/trace/rv/linear_temporal_logic.rst
+ */
+
+#include <linux/rv.h>
+
+#define MONITOR_NAME wakeup
+
+enum ltl_atom {
+ LTL_BLOCK_ON_RT_MUTEX,
+ LTL_FUTEX_LOCK_PI,
+ LTL_RT,
+ LTL_USER_THREAD,
+ LTL_WOKEN_BY_LOWER_PRIO,
+ LTL_WOKEN_BY_SOFTIRQ,
+ LTL_NUM_ATOM
+};
+static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);
+
+static const char *ltl_atom_str(enum ltl_atom atom)
+{
+ static const char *const names[] = {
+ "bl_on_rt_mu",
+ "fu_lo_pi",
+ "rt",
+ "us_th",
+ "wo_lo_pr",
+ "wo_so",
+ };
+
+ return names[atom];
+}
+
+enum ltl_buchi_state {
+ S0,
+ RV_NUM_BA_STATES
+};
+static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
+
+static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+ bool woken_by_softirq = test_bit(LTL_WOKEN_BY_SOFTIRQ, mon->atoms);
+ bool woken_by_lower_prio = test_bit(LTL_WOKEN_BY_LOWER_PRIO, mon->atoms);
+ bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms);
+ bool rt = test_bit(LTL_RT, mon->atoms);
+ bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
+ bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
+ bool val9 = block_on_rt_mutex || futex_lock_pi;
+ bool val6 = !woken_by_softirq;
+ bool val5 = !woken_by_lower_prio;
+ bool val8 = val5 && val6;
+ bool val10 = val8 || val9;
+ bool val3 = !user_thread;
+ bool val2 = !rt;
+ bool val4 = val2 || val3;
+ bool val11 = val4 || val10;
+
+ if (val11)
+ __set_bit(S0, mon->states);
+}
+
+static void
+ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
+{
+ bool woken_by_softirq = test_bit(LTL_WOKEN_BY_SOFTIRQ, mon->atoms);
+ bool woken_by_lower_prio = test_bit(LTL_WOKEN_BY_LOWER_PRIO, mon->atoms);
+ bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms);
+ bool rt = test_bit(LTL_RT, mon->atoms);
+ bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
+ bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
+ bool val9 = block_on_rt_mutex || futex_lock_pi;
+ bool val6 = !woken_by_softirq;
+ bool val5 = !woken_by_lower_prio;
+ bool val8 = val5 && val6;
+ bool val10 = val8 || val9;
+ bool val3 = !user_thread;
+ bool val2 = !rt;
+ bool val4 = val2 || val3;
+ bool val11 = val4 || val10;
+
+ switch (state) {
+ case S0:
+ if (val11)
+ __set_bit(S0, next);
+ break;
+ }
+}
diff --git a/kernel/trace/rv/monitors/wakeup/wakeup_trace.h b/kernel/trace/rv/monitors/wakeup/wakeup_trace.h
new file mode 100644
index 000000000000..7e056183f920
--- /dev/null
+++ b/kernel/trace/rv/monitors/wakeup/wakeup_trace.h
@@ -0,0 +1,14 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_WAKEUP
+DEFINE_EVENT(event_ltl_monitor_id, event_wakeup,
+ TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
+ TP_ARGS(task, states, atoms, next));
+DEFINE_EVENT(error_ltl_monitor_id, error_wakeup,
+ TP_PROTO(struct task_struct *task),
+ TP_ARGS(task));
+#endif /* CONFIG_RV_MON_WAKEUP */
diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index 9622c269789c..2f8a932432c9 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -241,6 +241,7 @@ DECLARE_EVENT_CLASS(error_ltl_monitor_id,
);
#include <monitors/pagefault/pagefault_trace.h>
#include <monitors/sleep/sleep_trace.h>
+#include <monitors/wakeup/wakeup_trace.h>
// Add new monitors based on CONFIG_LTL_MON_EVENTS_ID here
#endif /* CONFIG_LTL_MON_EVENTS_ID */
diff --git a/tools/verification/models/rtapp/wakeup.ltl b/tools/verification/models/rtapp/wakeup.ltl
new file mode 100644
index 000000000000..a5d63ca0811a
--- /dev/null
+++ b/tools/verification/models/rtapp/wakeup.ltl
@@ -0,0 +1,5 @@
+RULE = always (((RT and USER_THREAD) imply
+ (not (WOKEN_BY_LOWER_PRIO or WOKEN_BY_SOFTIRQ)) or ALLOWLIST))
+
+ALLOWLIST = BLOCK_ON_RT_MUTEX
+ or FUTEX_LOCK_PI
--
2.47.3
^ permalink raw reply related
* [PATCH v2 3/4] rv/rtapp/sleep: Stop monitoring kernel threads
From: Nam Cao @ 2026-06-19 7:21 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, linux-trace-kernel, linux-doc,
linux-kernel
Cc: Nam Cao, Sebastian Andrzej Siewior
In-Reply-To: <cover.1781852967.git.namcao@linutronix.de>
The rtapp/sleep monitor's primary purpose is detecting common mistakes
with user-space real-time design. Monitoring real-time issues with
kernel threads is a bonus.
However, accomodating kernel threads complicates the monitor due to
the edge cases which is seen by the monitor as lower-priority task
waking higher-priority task:
- kthread_stop() wakes up the task in order to stop it.
- The rcu thread and migration thread can be woken by any task.
- The ktimerd thread is woken near the end of irq_exit_rcu(), where
the preempt counter is "broken" and falsely says this is task
context. This requires the monitor to use the hardirq_context flag
instead of the preempt counter.
Beside complicating the monitor, the final case also requires enabling
CONFIG_TRACE_IRQFLAGS (so that "hardirq_context" can be used). This
adds overhead to the kernel even when the monitor is not active. This
may be an obstacle to enabling this monitor in distros' kernels.
Furthermore, kernel threads usually are started before the monitor is
enabled. Consequently, the threads' states (i.o.w. the monitor's
atomic propositions for the threads) are not fully known to the
monitor. As a result, the kernel threads mostly cannot be monitored.
Overall, the downsides of accomodating kernel threads outweights the
benefits. Thus, exclude kernel threads to simplify the monitor.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Sebastian Andrzej Siewior <bigeasy@linutronix.de>
---
Documentation/trace/rv/monitor_rtapp.rst | 22 ++---
kernel/trace/rv/monitors/sleep/Kconfig | 1 -
kernel/trace/rv/monitors/sleep/sleep.c | 39 +-------
kernel/trace/rv/monitors/sleep/sleep.h | 104 +++++++++-------------
tools/verification/models/rtapp/sleep.ltl | 7 +-
5 files changed, 54 insertions(+), 119 deletions(-)
diff --git a/Documentation/trace/rv/monitor_rtapp.rst b/Documentation/trace/rv/monitor_rtapp.rst
index 570be67a8f3b..502d3ea412eb 100644
--- a/Documentation/trace/rv/monitor_rtapp.rst
+++ b/Documentation/trace/rv/monitor_rtapp.rst
@@ -93,9 +93,9 @@ assessment.
The monitor's specification is::
- RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
+ RULE = always ((RT and SLEEP and USER_THREAD) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
- RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
+ RT_FRIENDLY_SLEEP = RT_VALID_SLEEP_REASON
and ((not SCHEDULE_IN) until RT_FRIENDLY_WAKE)
RT_VALID_SLEEP_REASON = FUTEX_WAIT
@@ -110,23 +110,13 @@ The monitor's specification is::
or WOKEN_BY_HARDIRQ
or WOKEN_BY_NMI
or ABORT_SLEEP
- or KTHREAD_SHOULD_STOP
ALLOWLIST = BLOCK_ON_RT_MUTEX
or FUTEX_LOCK_PI
- or TASK_IS_RCU
- or TASK_IS_MIGRATION
-
-Beside the scenarios described above, this specification also handle some
-special cases:
-
- - `KERNEL_THREAD`: kernel tasks do not have any pattern that can be recognized
- as valid real-time sleeping reasons. Therefore sleeping reason is not
- checked for kernel tasks.
- - `KTHREAD_SHOULD_STOP`: a non-real-time thread may stop a real-time kernel
- thread by waking it and waiting for it to exit (`kthread_stop()`). This
- wakeup is safe for real-time.
- - `ALLOWLIST`: to handle known false positives with the kernel.
+
+Beside the scenarios described above, this specification also defines an allow list
+to handle some special cases:
+
- `BLOCK_ON_RT_MUTEX` is included in the allowlist due to its implementation.
In the release path of rt_mutex, a boosted task is de-boosted before waking
the rt_mutex's waiter. Consequently, the monitor may see a real-time-unsafe
diff --git a/kernel/trace/rv/monitors/sleep/Kconfig b/kernel/trace/rv/monitors/sleep/Kconfig
index 6b7a122e7b47..d6ec3e9a91b6 100644
--- a/kernel/trace/rv/monitors/sleep/Kconfig
+++ b/kernel/trace/rv/monitors/sleep/Kconfig
@@ -5,7 +5,6 @@ config RV_MON_SLEEP
select RV_LTL_MONITOR
depends on HAVE_SYSCALL_TRACEPOINTS
depends on RV_MON_RTAPP
- select TRACE_IRQFLAGS
default y
select LTL_MON_EVENTS_ID
bool "sleep monitor"
diff --git a/kernel/trace/rv/monitors/sleep/sleep.c b/kernel/trace/rv/monitors/sleep/sleep.c
index 638be7d8747f..aa5a984853b5 100644
--- a/kernel/trace/rv/monitors/sleep/sleep.c
+++ b/kernel/trace/rv/monitors/sleep/sleep.c
@@ -43,7 +43,6 @@ static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bo
ltl_atom_set(mon, LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO, false);
if (task_creation) {
- ltl_atom_set(mon, LTL_KTHREAD_SHOULD_STOP, false);
ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_REALTIME, false);
ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false);
ltl_atom_set(mon, LTL_CLOCK_NANOSLEEP, false);
@@ -53,33 +52,7 @@ static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bo
ltl_atom_set(mon, LTL_BLOCK_ON_RT_MUTEX, false);
}
- if (task->flags & PF_KTHREAD) {
- ltl_atom_set(mon, LTL_KERNEL_THREAD, true);
-
- /* kernel tasks do not do syscall */
- ltl_atom_set(mon, LTL_FUTEX_WAIT, false);
- ltl_atom_set(mon, LTL_FUTEX_LOCK_PI, false);
- ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_REALTIME, false);
- ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false);
- ltl_atom_set(mon, LTL_CLOCK_NANOSLEEP, false);
- ltl_atom_set(mon, LTL_EPOLL_WAIT, false);
-
- if (strstarts(task->comm, "migration/"))
- ltl_atom_set(mon, LTL_TASK_IS_MIGRATION, true);
- else
- ltl_atom_set(mon, LTL_TASK_IS_MIGRATION, false);
-
- if (strstarts(task->comm, "rcu"))
- ltl_atom_set(mon, LTL_TASK_IS_RCU, true);
- else
- ltl_atom_set(mon, LTL_TASK_IS_RCU, false);
- } else {
- ltl_atom_set(mon, LTL_KTHREAD_SHOULD_STOP, false);
- ltl_atom_set(mon, LTL_KERNEL_THREAD, false);
- ltl_atom_set(mon, LTL_TASK_IS_RCU, false);
- ltl_atom_set(mon, LTL_TASK_IS_MIGRATION, false);
- }
-
+ ltl_atom_set(mon, LTL_USER_THREAD, !(task->flags & PF_KTHREAD));
}
static void handle_sched_set_state(void *data, struct task_struct *task, int state)
@@ -97,7 +70,7 @@ static void handle_sched_exit(void *data, bool is_switch)
static void handle_sched_waking(void *data, struct task_struct *task)
{
- if (this_cpu_read(hardirq_context)) {
+ if (in_hardirq()) {
ltl_atom_pulse(task, LTL_WOKEN_BY_HARDIRQ, true);
} else if (in_task()) {
if (current->prio <= task->prio)
@@ -181,12 +154,6 @@ static void handle_sys_exit(void *data, struct pt_regs *regs, long ret)
ltl_atom_update(current, LTL_CLOCK_NANOSLEEP, false);
}
-static void handle_kthread_stop(void *data, struct task_struct *task)
-{
- /* FIXME: this could race with other tracepoint handlers */
- ltl_atom_update(task, LTL_KTHREAD_SHOULD_STOP, true);
-}
-
static int enable_sleep(void)
{
int retval;
@@ -200,7 +167,6 @@ static int enable_sleep(void)
rv_attach_trace_probe("rtapp_sleep", sched_set_state_tp, handle_sched_set_state);
rv_attach_trace_probe("rtapp_sleep", contention_begin, handle_contention_begin);
rv_attach_trace_probe("rtapp_sleep", contention_end, handle_contention_end);
- rv_attach_trace_probe("rtapp_sleep", sched_kthread_stop, handle_kthread_stop);
rv_attach_trace_probe("rtapp_sleep", sys_enter, handle_sys_enter);
rv_attach_trace_probe("rtapp_sleep", sys_exit, handle_sys_exit);
return 0;
@@ -213,7 +179,6 @@ static void disable_sleep(void)
rv_detach_trace_probe("rtapp_sleep", sched_set_state_tp, handle_sched_set_state);
rv_detach_trace_probe("rtapp_sleep", contention_begin, handle_contention_begin);
rv_detach_trace_probe("rtapp_sleep", contention_end, handle_contention_end);
- rv_detach_trace_probe("rtapp_sleep", sched_kthread_stop, handle_kthread_stop);
rv_detach_trace_probe("rtapp_sleep", sys_enter, handle_sys_enter);
rv_detach_trace_probe("rtapp_sleep", sys_exit, handle_sys_exit);
diff --git a/kernel/trace/rv/monitors/sleep/sleep.h b/kernel/trace/rv/monitors/sleep/sleep.h
index 2fe2ec7edae8..44e593f41e6a 100644
--- a/kernel/trace/rv/monitors/sleep/sleep.h
+++ b/kernel/trace/rv/monitors/sleep/sleep.h
@@ -18,15 +18,12 @@ enum ltl_atom {
LTL_EPOLL_WAIT,
LTL_FUTEX_LOCK_PI,
LTL_FUTEX_WAIT,
- LTL_KERNEL_THREAD,
- LTL_KTHREAD_SHOULD_STOP,
LTL_NANOSLEEP_CLOCK_REALTIME,
LTL_NANOSLEEP_TIMER_ABSTIME,
LTL_RT,
LTL_SCHEDULE_IN,
LTL_SLEEP,
- LTL_TASK_IS_MIGRATION,
- LTL_TASK_IS_RCU,
+ LTL_USER_THREAD,
LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
LTL_WOKEN_BY_HARDIRQ,
LTL_WOKEN_BY_NMI,
@@ -43,15 +40,12 @@ static const char *ltl_atom_str(enum ltl_atom atom)
"ep_wa",
"fu_lo_pi",
"fu_wa",
- "ker_th",
- "kth_sh_st",
"na_cl_re",
"na_ti_ab",
"rt",
"sch_in",
"sle",
- "ta_mi",
- "ta_rc",
+ "us_th",
"wo_eq_hi_pr",
"wo_ha",
"wo_nm",
@@ -79,46 +73,41 @@ static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
mon->atoms);
- bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
- bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
+ bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms);
bool sleep = test_bit(LTL_SLEEP, mon->atoms);
bool schedule_in = test_bit(LTL_SCHEDULE_IN, mon->atoms);
bool rt = test_bit(LTL_RT, mon->atoms);
bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
bool nanosleep_clock_realtime = test_bit(LTL_NANOSLEEP_CLOCK_REALTIME, mon->atoms);
- bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
- bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
bool epoll_wait = test_bit(LTL_EPOLL_WAIT, mon->atoms);
bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
- bool val41 = task_is_rcu || task_is_migration;
- bool val42 = futex_lock_pi || val41;
- bool val5 = block_on_rt_mutex || val42;
- bool val33 = abort_sleep || kthread_should_stop;
- bool val34 = woken_by_nmi || val33;
- bool val35 = woken_by_hardirq || val34;
- bool val14 = woken_by_equal_or_higher_prio || val35;
+ bool val7 = block_on_rt_mutex || futex_lock_pi;
+ bool val32 = woken_by_nmi || abort_sleep;
+ bool val33 = woken_by_hardirq || val32;
+ bool val14 = woken_by_equal_or_higher_prio || val33;
bool val13 = !schedule_in;
bool val25 = !nanosleep_clock_realtime;
bool val26 = nanosleep_timer_abstime && val25;
bool val18 = clock_nanosleep && val26;
bool val20 = val18 || epoll_wait;
- bool val9 = futex_wait || val20;
- bool val11 = val9 || kernel_thread;
+ bool val11 = futex_wait || val20;
+ bool val3 = !user_thread;
bool val2 = !sleep;
+ bool val4 = val2 || val3;
bool val1 = !rt;
- bool val3 = val1 || val2;
+ bool val5 = val1 || val4;
- if (val3)
+ if (val5)
__set_bit(S0, mon->states);
if (val11 && val13)
__set_bit(S1, mon->states);
if (val11 && val14)
__set_bit(S4, mon->states);
- if (val5)
+ if (val7)
__set_bit(S5, mon->states);
}
@@ -129,130 +118,125 @@ ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned l
bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
mon->atoms);
- bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
- bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
+ bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms);
bool sleep = test_bit(LTL_SLEEP, mon->atoms);
bool schedule_in = test_bit(LTL_SCHEDULE_IN, mon->atoms);
bool rt = test_bit(LTL_RT, mon->atoms);
bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
bool nanosleep_clock_realtime = test_bit(LTL_NANOSLEEP_CLOCK_REALTIME, mon->atoms);
- bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
- bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
bool epoll_wait = test_bit(LTL_EPOLL_WAIT, mon->atoms);
bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
- bool val41 = task_is_rcu || task_is_migration;
- bool val42 = futex_lock_pi || val41;
- bool val5 = block_on_rt_mutex || val42;
- bool val33 = abort_sleep || kthread_should_stop;
- bool val34 = woken_by_nmi || val33;
- bool val35 = woken_by_hardirq || val34;
- bool val14 = woken_by_equal_or_higher_prio || val35;
+ bool val7 = block_on_rt_mutex || futex_lock_pi;
+ bool val32 = woken_by_nmi || abort_sleep;
+ bool val33 = woken_by_hardirq || val32;
+ bool val14 = woken_by_equal_or_higher_prio || val33;
bool val13 = !schedule_in;
bool val25 = !nanosleep_clock_realtime;
bool val26 = nanosleep_timer_abstime && val25;
bool val18 = clock_nanosleep && val26;
bool val20 = val18 || epoll_wait;
- bool val9 = futex_wait || val20;
- bool val11 = val9 || kernel_thread;
+ bool val11 = futex_wait || val20;
+ bool val3 = !user_thread;
bool val2 = !sleep;
+ bool val4 = val2 || val3;
bool val1 = !rt;
- bool val3 = val1 || val2;
+ bool val5 = val1 || val4;
switch (state) {
case S0:
- if (val3)
+ if (val5)
__set_bit(S0, next);
if (val11 && val13)
__set_bit(S1, next);
if (val11 && val14)
__set_bit(S4, next);
- if (val5)
+ if (val7)
__set_bit(S5, next);
break;
case S1:
if (val11 && val13)
__set_bit(S1, next);
- if (val13 && val3)
+ if (val13 && val5)
__set_bit(S2, next);
- if (val14 && val3)
+ if (val14 && val5)
__set_bit(S3, next);
if (val11 && val14)
__set_bit(S4, next);
- if (val13 && val5)
+ if (val13 && val7)
__set_bit(S6, next);
- if (val14 && val5)
+ if (val14 && val7)
__set_bit(S7, next);
break;
case S2:
if (val11 && val13)
__set_bit(S1, next);
- if (val13 && val3)
+ if (val13 && val5)
__set_bit(S2, next);
- if (val14 && val3)
+ if (val14 && val5)
__set_bit(S3, next);
if (val11 && val14)
__set_bit(S4, next);
- if (val13 && val5)
+ if (val13 && val7)
__set_bit(S6, next);
- if (val14 && val5)
+ if (val14 && val7)
__set_bit(S7, next);
break;
case S3:
- if (val3)
+ if (val5)
__set_bit(S0, next);
if (val11 && val13)
__set_bit(S1, next);
if (val11 && val14)
__set_bit(S4, next);
- if (val5)
+ if (val7)
__set_bit(S5, next);
break;
case S4:
- if (val3)
+ if (val5)
__set_bit(S0, next);
if (val11 && val13)
__set_bit(S1, next);
if (val11 && val14)
__set_bit(S4, next);
- if (val5)
+ if (val7)
__set_bit(S5, next);
break;
case S5:
- if (val3)
+ if (val5)
__set_bit(S0, next);
if (val11 && val13)
__set_bit(S1, next);
if (val11 && val14)
__set_bit(S4, next);
- if (val5)
+ if (val7)
__set_bit(S5, next);
break;
case S6:
if (val11 && val13)
__set_bit(S1, next);
- if (val13 && val3)
+ if (val13 && val5)
__set_bit(S2, next);
- if (val14 && val3)
+ if (val14 && val5)
__set_bit(S3, next);
if (val11 && val14)
__set_bit(S4, next);
- if (val13 && val5)
+ if (val13 && val7)
__set_bit(S6, next);
- if (val14 && val5)
+ if (val14 && val7)
__set_bit(S7, next);
break;
case S7:
- if (val3)
+ if (val5)
__set_bit(S0, next);
if (val11 && val13)
__set_bit(S1, next);
if (val11 && val14)
__set_bit(S4, next);
- if (val5)
+ if (val7)
__set_bit(S5, next);
break;
}
diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl
index 5923e58d7810..4d78fdd204c0 100644
--- a/tools/verification/models/rtapp/sleep.ltl
+++ b/tools/verification/models/rtapp/sleep.ltl
@@ -1,6 +1,6 @@
-RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
+RULE = always ((RT and SLEEP and USER_THREAD) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
-RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
+RT_FRIENDLY_SLEEP = RT_VALID_SLEEP_REASON
and ((not SCHEDULE_IN) until RT_FRIENDLY_WAKE)
RT_VALID_SLEEP_REASON = FUTEX_WAIT
@@ -15,9 +15,6 @@ RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO
or WOKEN_BY_HARDIRQ
or WOKEN_BY_NMI
or ABORT_SLEEP
- or KTHREAD_SHOULD_STOP
ALLOWLIST = BLOCK_ON_RT_MUTEX
or FUTEX_LOCK_PI
- or TASK_IS_RCU
- or TASK_IS_MIGRATION
--
2.47.3
^ permalink raw reply related
* [PATCH v2 2/4] rv/rtapp/sleep: Update nanosleep rule
From: Nam Cao @ 2026-06-19 7:21 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, linux-trace-kernel, linux-doc,
linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781852967.git.namcao@linutronix.de>
CLOCK_REALTIME is the only clock that often is misused in real-time
applications. The other clocks either are safe for real-time uses
(CLOCK_TAI, CLOCK_MONOTONIC, CLOCK_BOOTTIME) or are unlikely to be misused
(CLOCK_AUX, CLOCK_PROCESS_CPUTIME_ID).
Update the monitor to only warn about CLOCK_REALTIME.
While at it, update the out-of-sync documentation.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Documentation/trace/rv/monitor_rtapp.rst | 17 +++++---
kernel/trace/rv/monitors/sleep/sleep.c | 12 ++----
kernel/trace/rv/monitors/sleep/sleep.h | 52 +++++++++++------------
tools/verification/models/rtapp/sleep.ltl | 2 +-
4 files changed, 39 insertions(+), 44 deletions(-)
diff --git a/Documentation/trace/rv/monitor_rtapp.rst b/Documentation/trace/rv/monitor_rtapp.rst
index 01656bf7080a..570be67a8f3b 100644
--- a/Documentation/trace/rv/monitor_rtapp.rst
+++ b/Documentation/trace/rv/monitor_rtapp.rst
@@ -51,12 +51,13 @@ The `sleep` monitor reports real-time threads sleeping in a manner that may
cause undesirable latency. Real-time applications should only put a real-time
thread to sleep for one of the following reasons:
- - Cyclic work: real-time thread sleeps waiting for the next cycle. For this
- case, only the `clock_nanosleep` syscall should be used with `TIMER_ABSTIME`
- (to avoid time drift) and `CLOCK_MONOTONIC` (to avoid the clock being
- changed). No other method is safe for real-time. For example, threads
- waiting for timerfd can be woken by softirq which provides no real-time
- guarantee.
+ - Cyclic work: real-time thread sleeps waiting for the next
+ cycle. For this case, only the `clock_nanosleep` syscall should be
+ used with `TIMER_ABSTIME` (to avoid time drift). Additionally,
+ `CLOCK_REALTIME` should not be used (to avoid the clock being
+ changed). No other method is safe for real-time. For example,
+ threads waiting for timerfd can be woken by softirq which provides
+ no real-time guarantee.
- Real-time thread waiting for something to happen (e.g. another thread
releasing shared resources, or a completion signal from another thread). In
this case, only futexes (FUTEX_LOCK_PI, FUTEX_LOCK_PI2 or one of
@@ -99,14 +100,16 @@ The monitor's specification is::
RT_VALID_SLEEP_REASON = FUTEX_WAIT
or RT_FRIENDLY_NANOSLEEP
+ or EPOLL_WAIT
RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP
and NANOSLEEP_TIMER_ABSTIME
- and NANOSLEEP_CLOCK_MONOTONIC
+ and not NANOSLEEP_CLOCK_REALTIME
RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO
or WOKEN_BY_HARDIRQ
or WOKEN_BY_NMI
+ or ABORT_SLEEP
or KTHREAD_SHOULD_STOP
ALLOWLIST = BLOCK_ON_RT_MUTEX
diff --git a/kernel/trace/rv/monitors/sleep/sleep.c b/kernel/trace/rv/monitors/sleep/sleep.c
index d6b677fab8f8..638be7d8747f 100644
--- a/kernel/trace/rv/monitors/sleep/sleep.c
+++ b/kernel/trace/rv/monitors/sleep/sleep.c
@@ -44,8 +44,7 @@ static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bo
if (task_creation) {
ltl_atom_set(mon, LTL_KTHREAD_SHOULD_STOP, false);
- ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, false);
- ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, false);
+ ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_REALTIME, false);
ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false);
ltl_atom_set(mon, LTL_CLOCK_NANOSLEEP, false);
ltl_atom_set(mon, LTL_FUTEX_WAIT, false);
@@ -60,8 +59,7 @@ static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bo
/* kernel tasks do not do syscall */
ltl_atom_set(mon, LTL_FUTEX_WAIT, false);
ltl_atom_set(mon, LTL_FUTEX_LOCK_PI, false);
- ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, false);
- ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, false);
+ ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_REALTIME, false);
ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false);
ltl_atom_set(mon, LTL_CLOCK_NANOSLEEP, false);
ltl_atom_set(mon, LTL_EPOLL_WAIT, false);
@@ -136,8 +134,7 @@ static void handle_sys_enter(void *data, struct pt_regs *regs, long id)
case __NR_clock_nanosleep_time64:
#endif
syscall_get_arguments(current, regs, args);
- ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, args[0] == CLOCK_MONOTONIC);
- ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, args[0] == CLOCK_TAI);
+ ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_REALTIME, args[0] == CLOCK_REALTIME);
ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, args[1] == TIMER_ABSTIME);
ltl_atom_update(current, LTL_CLOCK_NANOSLEEP, true);
break;
@@ -178,8 +175,7 @@ static void handle_sys_exit(void *data, struct pt_regs *regs, long ret)
ltl_atom_set(mon, LTL_FUTEX_LOCK_PI, false);
ltl_atom_set(mon, LTL_FUTEX_WAIT, false);
- ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, false);
- ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, false);
+ ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_REALTIME, false);
ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false);
ltl_atom_set(mon, LTL_EPOLL_WAIT, false);
ltl_atom_update(current, LTL_CLOCK_NANOSLEEP, false);
diff --git a/kernel/trace/rv/monitors/sleep/sleep.h b/kernel/trace/rv/monitors/sleep/sleep.h
index 403dc2852c52..2fe2ec7edae8 100644
--- a/kernel/trace/rv/monitors/sleep/sleep.h
+++ b/kernel/trace/rv/monitors/sleep/sleep.h
@@ -20,8 +20,7 @@ enum ltl_atom {
LTL_FUTEX_WAIT,
LTL_KERNEL_THREAD,
LTL_KTHREAD_SHOULD_STOP,
- LTL_NANOSLEEP_CLOCK_MONOTONIC,
- LTL_NANOSLEEP_CLOCK_TAI,
+ LTL_NANOSLEEP_CLOCK_REALTIME,
LTL_NANOSLEEP_TIMER_ABSTIME,
LTL_RT,
LTL_SCHEDULE_IN,
@@ -46,8 +45,7 @@ static const char *ltl_atom_str(enum ltl_atom atom)
"fu_wa",
"ker_th",
"kth_sh_st",
- "na_cl_mo",
- "na_cl_ta",
+ "na_cl_re",
"na_ti_ab",
"rt",
"sch_in",
@@ -87,8 +85,7 @@ static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
bool schedule_in = test_bit(LTL_SCHEDULE_IN, mon->atoms);
bool rt = test_bit(LTL_RT, mon->atoms);
bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
- bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms);
- bool nanosleep_clock_monotonic = test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms);
+ bool nanosleep_clock_realtime = test_bit(LTL_NANOSLEEP_CLOCK_REALTIME, mon->atoms);
bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
@@ -97,17 +94,17 @@ static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
- bool val42 = task_is_rcu || task_is_migration;
- bool val43 = futex_lock_pi || val42;
- bool val5 = block_on_rt_mutex || val43;
- bool val34 = abort_sleep || kthread_should_stop;
- bool val35 = woken_by_nmi || val34;
- bool val36 = woken_by_hardirq || val35;
- bool val14 = woken_by_equal_or_higher_prio || val36;
+ bool val41 = task_is_rcu || task_is_migration;
+ bool val42 = futex_lock_pi || val41;
+ bool val5 = block_on_rt_mutex || val42;
+ bool val33 = abort_sleep || kthread_should_stop;
+ bool val34 = woken_by_nmi || val33;
+ bool val35 = woken_by_hardirq || val34;
+ bool val14 = woken_by_equal_or_higher_prio || val35;
bool val13 = !schedule_in;
- bool val26 = nanosleep_clock_monotonic || nanosleep_clock_tai;
- bool val27 = nanosleep_timer_abstime && val26;
- bool val18 = clock_nanosleep && val27;
+ bool val25 = !nanosleep_clock_realtime;
+ bool val26 = nanosleep_timer_abstime && val25;
+ bool val18 = clock_nanosleep && val26;
bool val20 = val18 || epoll_wait;
bool val9 = futex_wait || val20;
bool val11 = val9 || kernel_thread;
@@ -138,8 +135,7 @@ ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned l
bool schedule_in = test_bit(LTL_SCHEDULE_IN, mon->atoms);
bool rt = test_bit(LTL_RT, mon->atoms);
bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
- bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms);
- bool nanosleep_clock_monotonic = test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms);
+ bool nanosleep_clock_realtime = test_bit(LTL_NANOSLEEP_CLOCK_REALTIME, mon->atoms);
bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
@@ -148,17 +144,17 @@ ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned l
bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
- bool val42 = task_is_rcu || task_is_migration;
- bool val43 = futex_lock_pi || val42;
- bool val5 = block_on_rt_mutex || val43;
- bool val34 = abort_sleep || kthread_should_stop;
- bool val35 = woken_by_nmi || val34;
- bool val36 = woken_by_hardirq || val35;
- bool val14 = woken_by_equal_or_higher_prio || val36;
+ bool val41 = task_is_rcu || task_is_migration;
+ bool val42 = futex_lock_pi || val41;
+ bool val5 = block_on_rt_mutex || val42;
+ bool val33 = abort_sleep || kthread_should_stop;
+ bool val34 = woken_by_nmi || val33;
+ bool val35 = woken_by_hardirq || val34;
+ bool val14 = woken_by_equal_or_higher_prio || val35;
bool val13 = !schedule_in;
- bool val26 = nanosleep_clock_monotonic || nanosleep_clock_tai;
- bool val27 = nanosleep_timer_abstime && val26;
- bool val18 = clock_nanosleep && val27;
+ bool val25 = !nanosleep_clock_realtime;
+ bool val26 = nanosleep_timer_abstime && val25;
+ bool val18 = clock_nanosleep && val26;
bool val20 = val18 || epoll_wait;
bool val9 = futex_wait || val20;
bool val11 = val9 || kernel_thread;
diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl
index 464c84b9df87..5923e58d7810 100644
--- a/tools/verification/models/rtapp/sleep.ltl
+++ b/tools/verification/models/rtapp/sleep.ltl
@@ -9,7 +9,7 @@ RT_VALID_SLEEP_REASON = FUTEX_WAIT
RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP
and NANOSLEEP_TIMER_ABSTIME
- and (NANOSLEEP_CLOCK_MONOTONIC or NANOSLEEP_CLOCK_TAI)
+ and not NANOSLEEP_CLOCK_REALTIME
RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO
or WOKEN_BY_HARDIRQ
--
2.47.3
^ permalink raw reply related
* [PATCH v2 1/4] rv/rtapp/sleep: Make the error more informative for user
From: Nam Cao @ 2026-06-19 7:21 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, linux-trace-kernel, linux-doc,
linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781852967.git.namcao@linutronix.de>
The rtapp/sleep monitor detects real-time tasks which go to sleep in an
real-time-unsafe manner. If this happen, the monitor triggers a trace event
in the sched_wakeup tracepoint's handler.
However, the invoking context of that trace event is not the most
informative, because of the stack trace of that event is the wakeup's code
path which is not very helpful:
74.669317: rv:error_sleep: condvar[254]: violation detected
ltl_validate+0x345 ([kernel.kallsyms])
handle_sched_wakeup+0x34 ([kernel.kallsyms])
ttwu_do_activate+0xff ([kernel.kallsyms])
sched_ttwu_pending+0x104 ([kernel.kallsyms])
__flush_smp_call_function_queue+0x15b ([kernel.kallsyms])
__sysvec_call_function_single+0x18 ([kernel.kallsyms])
sysvec_call_function_single+0x66 ([kernel.kallsyms])
asm_sysvec_call_function_single+0x1a ([kernel.kallsyms])
pv_native_safe_halt+0xf ([kernel.kallsyms])
default_idle+0x9 ([kernel.kallsyms])
default_idle_call+0x33 ([kernel.kallsyms])
do_idle+0x234 ([kernel.kallsyms])
cpu_startup_entry+0x24 ([kernel.kallsyms])
start_secondary+0xf8 ([kernel.kallsyms])
common_startup_64+0x13e ([kernel.kallsyms])
What would be much more valuable is the stack trace of the task itself.
Instead of using the sched_wakeup tracepoint, use the sched_exit
tracepoint. This makes the event happen in the task's context, making
the stack trace far more informative for user:
rv:error_sleep: condvar[254]: violation detected
ltl_validate+0x345 ([kernel.kallsyms])
handle_sched_exit+0x39 ([kernel.kallsyms])
__schedule+0x80f ([kernel.kallsyms])
schedule+0x22 ([kernel.kallsyms])
futex_do_wait+0x33 ([kernel.kallsyms])
__futex_wait+0x8c ([kernel.kallsyms])
futex_wait+0x73 ([kernel.kallsyms])
do_futex+0xc6 ([kernel.kallsyms])
__x64_sys_futex+0x121 ([kernel.kallsyms])
do_syscall_64+0xf3 ([kernel.kallsyms])
entry_SYSCALL_64_after_hwframe+0x77 ([kernel.kallsyms])
__futex_abstimed_wait_common64+0xc6 (inlined)
__futex_abstimed_wait_common+0xc6 (/usr/lib/x86_64-linux-gnu/libc.so.6)
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Documentation/trace/rv/monitor_rtapp.rst | 2 +-
kernel/trace/rv/monitors/sleep/sleep.c | 10 +++++-----
kernel/trace/rv/monitors/sleep/sleep.h | 14 +++++++-------
tools/verification/models/rtapp/sleep.ltl | 2 +-
4 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/Documentation/trace/rv/monitor_rtapp.rst b/Documentation/trace/rv/monitor_rtapp.rst
index c8104eda924a..01656bf7080a 100644
--- a/Documentation/trace/rv/monitor_rtapp.rst
+++ b/Documentation/trace/rv/monitor_rtapp.rst
@@ -95,7 +95,7 @@ The monitor's specification is::
RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
- and ((not WAKE) until RT_FRIENDLY_WAKE)
+ and ((not SCHEDULE_IN) until RT_FRIENDLY_WAKE)
RT_VALID_SLEEP_REASON = FUTEX_WAIT
or RT_FRIENDLY_NANOSLEEP
diff --git a/kernel/trace/rv/monitors/sleep/sleep.c b/kernel/trace/rv/monitors/sleep/sleep.c
index 8dfe5ec13e19..d6b677fab8f8 100644
--- a/kernel/trace/rv/monitors/sleep/sleep.c
+++ b/kernel/trace/rv/monitors/sleep/sleep.c
@@ -36,7 +36,7 @@ static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
{
ltl_atom_set(mon, LTL_SLEEP, false);
- ltl_atom_set(mon, LTL_WAKE, false);
+ ltl_atom_set(mon, LTL_SCHEDULE_IN, false);
ltl_atom_set(mon, LTL_ABORT_SLEEP, false);
ltl_atom_set(mon, LTL_WOKEN_BY_HARDIRQ, false);
ltl_atom_set(mon, LTL_WOKEN_BY_NMI, false);
@@ -92,9 +92,9 @@ static void handle_sched_set_state(void *data, struct task_struct *task, int sta
ltl_atom_pulse(task, LTL_ABORT_SLEEP, true);
}
-static void handle_sched_wakeup(void *data, struct task_struct *task)
+static void handle_sched_exit(void *data, bool is_switch)
{
- ltl_atom_pulse(task, LTL_WAKE, true);
+ ltl_atom_pulse(current, LTL_SCHEDULE_IN, true);
}
static void handle_sched_waking(void *data, struct task_struct *task)
@@ -200,7 +200,7 @@ static int enable_sleep(void)
return retval;
rv_attach_trace_probe("rtapp_sleep", sched_waking, handle_sched_waking);
- rv_attach_trace_probe("rtapp_sleep", sched_wakeup, handle_sched_wakeup);
+ rv_attach_trace_probe("rtapp_sleep", sched_exit_tp, handle_sched_exit);
rv_attach_trace_probe("rtapp_sleep", sched_set_state_tp, handle_sched_set_state);
rv_attach_trace_probe("rtapp_sleep", contention_begin, handle_contention_begin);
rv_attach_trace_probe("rtapp_sleep", contention_end, handle_contention_end);
@@ -213,7 +213,7 @@ static int enable_sleep(void)
static void disable_sleep(void)
{
rv_detach_trace_probe("rtapp_sleep", sched_waking, handle_sched_waking);
- rv_detach_trace_probe("rtapp_sleep", sched_wakeup, handle_sched_wakeup);
+ rv_detach_trace_probe("rtapp_sleep", sched_exit_tp, handle_sched_exit);
rv_detach_trace_probe("rtapp_sleep", sched_set_state_tp, handle_sched_set_state);
rv_detach_trace_probe("rtapp_sleep", contention_begin, handle_contention_begin);
rv_detach_trace_probe("rtapp_sleep", contention_end, handle_contention_end);
diff --git a/kernel/trace/rv/monitors/sleep/sleep.h b/kernel/trace/rv/monitors/sleep/sleep.h
index 95dc2727c059..403dc2852c52 100644
--- a/kernel/trace/rv/monitors/sleep/sleep.h
+++ b/kernel/trace/rv/monitors/sleep/sleep.h
@@ -24,10 +24,10 @@ enum ltl_atom {
LTL_NANOSLEEP_CLOCK_TAI,
LTL_NANOSLEEP_TIMER_ABSTIME,
LTL_RT,
+ LTL_SCHEDULE_IN,
LTL_SLEEP,
LTL_TASK_IS_MIGRATION,
LTL_TASK_IS_RCU,
- LTL_WAKE,
LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
LTL_WOKEN_BY_HARDIRQ,
LTL_WOKEN_BY_NMI,
@@ -50,10 +50,10 @@ static const char *ltl_atom_str(enum ltl_atom atom)
"na_cl_ta",
"na_ti_ab",
"rt",
- "sl",
+ "sch_in",
+ "sle",
"ta_mi",
"ta_rc",
- "wak",
"wo_eq_hi_pr",
"wo_ha",
"wo_nm",
@@ -81,10 +81,10 @@ static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
mon->atoms);
- bool wake = test_bit(LTL_WAKE, mon->atoms);
bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
bool sleep = test_bit(LTL_SLEEP, mon->atoms);
+ bool schedule_in = test_bit(LTL_SCHEDULE_IN, mon->atoms);
bool rt = test_bit(LTL_RT, mon->atoms);
bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms);
@@ -104,7 +104,7 @@ static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
bool val35 = woken_by_nmi || val34;
bool val36 = woken_by_hardirq || val35;
bool val14 = woken_by_equal_or_higher_prio || val36;
- bool val13 = !wake;
+ bool val13 = !schedule_in;
bool val26 = nanosleep_clock_monotonic || nanosleep_clock_tai;
bool val27 = nanosleep_timer_abstime && val26;
bool val18 = clock_nanosleep && val27;
@@ -132,10 +132,10 @@ ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned l
bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
mon->atoms);
- bool wake = test_bit(LTL_WAKE, mon->atoms);
bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
bool sleep = test_bit(LTL_SLEEP, mon->atoms);
+ bool schedule_in = test_bit(LTL_SCHEDULE_IN, mon->atoms);
bool rt = test_bit(LTL_RT, mon->atoms);
bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms);
@@ -155,7 +155,7 @@ ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned l
bool val35 = woken_by_nmi || val34;
bool val36 = woken_by_hardirq || val35;
bool val14 = woken_by_equal_or_higher_prio || val36;
- bool val13 = !wake;
+ bool val13 = !schedule_in;
bool val26 = nanosleep_clock_monotonic || nanosleep_clock_tai;
bool val27 = nanosleep_timer_abstime && val26;
bool val18 = clock_nanosleep && val27;
diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl
index 6f26c4810f78..464c84b9df87 100644
--- a/tools/verification/models/rtapp/sleep.ltl
+++ b/tools/verification/models/rtapp/sleep.ltl
@@ -1,7 +1,7 @@
RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
- and ((not WAKE) until RT_FRIENDLY_WAKE)
+ and ((not SCHEDULE_IN) until RT_FRIENDLY_WAKE)
RT_VALID_SLEEP_REASON = FUTEX_WAIT
or RT_FRIENDLY_NANOSLEEP
--
2.47.3
^ permalink raw reply related
* [PATCH v2 0/4] rv: rtapp monitor update
From: Nam Cao @ 2026-06-19 7:21 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, linux-trace-kernel, linux-doc,
linux-kernel
Cc: Nam Cao
A couple of minor improvements to the rtapp monitor:
- Making the monitor more informative to user by changing the
context of the tracepoint into the monitored task itself, not the
IPI wakeup path.
- and update the allow list regarding clock_nanosleep syscall.
- Stop monitoring the kernel threads to simplify the monitors.
- Add a new rtapp/wakeup monitor to give complement the rtapp/sleep
monitor.
v2..v1 https://lore.kernel.org/lkml/cover.1779176466.git.namcao@linutronix.de/
- Use clearer waker/wakee terminologies
- Fix build issue
- Add new patch "rv/rtapp/sleep: Stop monitoring kernel threads"
- Require RV_PER_TASK_MONITORS >= 3
Nam Cao (4):
rv/rtapp/sleep: Make the error more informative for user
rv/rtapp/sleep: Update nanosleep rule
rv/rtapp/sleep: Stop monitoring kernel threads
rv/rtapp: Add wakeup monitor
Documentation/trace/rv/monitor_rtapp.rst | 61 ++++---
kernel/trace/rv/Kconfig | 1 +
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/monitors/rtapp/Kconfig | 2 +-
kernel/trace/rv/monitors/sleep/Kconfig | 1 -
kernel/trace/rv/monitors/sleep/sleep.c | 59 ++-----
kernel/trace/rv/monitors/sleep/sleep.h | 142 +++++++---------
kernel/trace/rv/monitors/wakeup/Kconfig | 16 ++
kernel/trace/rv/monitors/wakeup/wakeup.c | 153 ++++++++++++++++++
kernel/trace/rv/monitors/wakeup/wakeup.h | 92 +++++++++++
.../trace/rv/monitors/wakeup/wakeup_trace.h | 14 ++
kernel/trace/rv/rv_trace.h | 1 +
tools/verification/models/rtapp/sleep.ltl | 11 +-
tools/verification/models/rtapp/wakeup.ltl | 5 +
14 files changed, 396 insertions(+), 163 deletions(-)
create mode 100644 kernel/trace/rv/monitors/wakeup/Kconfig
create mode 100644 kernel/trace/rv/monitors/wakeup/wakeup.c
create mode 100644 kernel/trace/rv/monitors/wakeup/wakeup.h
create mode 100644 kernel/trace/rv/monitors/wakeup/wakeup_trace.h
create mode 100644 tools/verification/models/rtapp/wakeup.ltl
--
2.47.3
^ permalink raw reply
* [PATCH v4 13/13] verification/rvgen: Remove dead code
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.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>
---
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 2cb7443ea00f..fd37ce304276 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 b93d0ccc9bdf..4d39f229c970 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 v4 11/13] verification/rvgen: Switch __create_matrix() to Lark
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.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.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
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 c34e916516ba..1726e82546a7 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 f1f5fa297adb..03141e9ef45d 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -407,7 +407,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 v4 12/13] verification/rvgen: Remove the old state variables
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.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.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
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 1726e82546a7..2cb7443ea00f 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 03141e9ef45d..b93d0ccc9bdf 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:
@@ -318,7 +318,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
@@ -386,7 +386,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
@@ -395,7 +395,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 v4 10/13] verification/rvgen: Switch __get_event_variables() to Lark
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.git.namcao@linutronix.de>
Switch __get_event_variables() to use the parsed results from Lark, instead
of raw text processing.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
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 ea7eabd4c173..c34e916516ba 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 v4 07/13] rv: Simplify hybrid automata monitors's clock variables
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.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>
---
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 v4 09/13] verification/rvgen: Delete __parse_constraint()
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.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 4ea1ecc55c80..f1f5fa297adb 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:
@@ -308,64 +307,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 []
@@ -490,15 +431,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")
@@ -575,7 +516,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 v4 05/13] verification/rvgen: Convert __fill_setup_invariants_func() to Lark
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.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>
---
v4:
fix bug when the time value has a unit
---
tools/verification/rvgen/rvgen/dot2k.py | 48 ++++++++++++++++++++-----
1 file changed, 39 insertions(+), 9 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 0595bfcd232e..93674505f07b 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -250,6 +250,30 @@ 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
+ try:
+ val = int(inv.val)
+ except ValueError:
+ # it's a constant, a parameter or a function
+ 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 +487,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 +503,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 v4 08/13] verification/rvgen: Simplify the generation for clock variables
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.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.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
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 ced4e6288ff4..4ea1ecc55c80 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:
"""
@@ -387,40 +389,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 = []
@@ -460,54 +428,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 []
@@ -558,16 +478,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()
@@ -580,9 +493,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 v4 06/13] verification/rvgen: Convert __fill_verify_guards_func() to Lark
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.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 93674505f07b..ced4e6288ff4 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(",")
@@ -291,7 +304,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:
@@ -410,7 +423,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(
@@ -422,14 +436,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 v4 04/13] verification/rvgen: Convert __fill_verify_invariants_func() to Lark
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.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>
---
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 v4 01/13] verification/rvgen: Switch LTL parser to Lark
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.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 v4 03/13] verification/rvgen: Implement state and transition parser based on Lark
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.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>
---
v4:
add missing != operator
add missing 'j' as a time unit
---
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..ea7eabd4c173 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" | "j"
+ '''
+
+ 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 v4 02/13] verification/rvgen: Introduce a parse tree for automata using Lark
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
In-Reply-To: <cover.1781847583.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 v4 00/13] rv: Convert rvgen to Lark
From: Nam Cao @ 2026-06-19 5:52 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, 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.
v4..v3: https://lore.kernel.org/linux-trace-kernel/cover.1780908661.git.namcao@linutronix.de/
- fix missing operator "!=" and unit "j" in the grammar
- fix generation error when time values have units
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 | 294 +++-------
tools/verification/rvgen/rvgen/ltl2ba.py | 202 +++----
8 files changed, 608 insertions(+), 630 deletions(-)
--
2.47.3
^ permalink raw reply
* [PATCH v8 46/46] KVM: selftests: Update private memory exits test to work with per-gmem attributes
From: Ackerley Tng via B4 Relay @ 2026-06-19 0:32 UTC (permalink / raw)
To: aik, andrew.jones, binbin.wu, brauner, chao.p.peng, david,
jmattson, jthoughton, michael.roth, oupton, pankaj.gupta, qperret,
rick.p.edgecombe, rientjes, shivankg, steven.price, tabba, willy,
wyihan, yan.y.zhao, forkloop, pratyush, suzuki.poulose,
aneesh.kumar, liam, Paolo Bonzini, Sean Christopherson,
Thomas Gleixner, Ingo Molnar, Borislav Petkov, Dave Hansen, x86,
H. Peter Anvin, Steven Rostedt, Masami Hiramatsu,
Mathieu Desnoyers, Jonathan Corbet, Shuah Khan, Shuah Khan,
Vishal Annapurve, Andrew Morton, Chris Li, Kairui Song,
Kemeng Shi, Nhat Pham, Barry Song, Axel Rasmussen, Yuanchu Xie,
Wei Xu, Youngjun Park, Qi Zheng, Shakeel Butt, Kiryl Shutsemau,
Baoquan He, Jason Gunthorpe, Vlastimil Babka, Baoquan He
Cc: kvm, linux-kernel, linux-trace-kernel, linux-doc, linux-kselftest,
linux-mm, linux-coco, Ackerley Tng
In-Reply-To: <20260618-gmem-inplace-conversion-v8-0-9d2959357853@google.com>
From: Sean Christopherson <seanjc@google.com>
Skip setting memory to private in the private memory exits test when using
per-gmem memory attributes, as memory is initialized to private by default
for guest_memfd, and using vm_mem_set_private() on a guest_memfd instance
requires creating guest_memfd with GUEST_MEMFD_FLAG_MMAP (which is totally
doable, but would need to be conditional and is ultimately unnecessary).
Expect an emulated MMIO instead of a memory fault exit when attributes are
per-gmem, as deleting the memslot effectively drops the private status,
i.e. the GPA becomes shared and thus supports emulated MMIO.
Skip the "memslot not private" test entirely, as private vs. shared state
for x86 software-protected VMs comes from the memory attributes themselves,
and so when doing in-place conversions there can never be a disconnect
between the expected and actual states.
Signed-off-by: Sean Christopherson <seanjc@google.com>
---
.../selftests/kvm/x86/private_mem_kvm_exits_test.c | 36 ++++++++++++++++++----
1 file changed, 30 insertions(+), 6 deletions(-)
diff --git a/tools/testing/selftests/kvm/x86/private_mem_kvm_exits_test.c b/tools/testing/selftests/kvm/x86/private_mem_kvm_exits_test.c
index 10db9fe6d9063..70ed16066c63e 100644
--- a/tools/testing/selftests/kvm/x86/private_mem_kvm_exits_test.c
+++ b/tools/testing/selftests/kvm/x86/private_mem_kvm_exits_test.c
@@ -62,8 +62,9 @@ static void test_private_access_memslot_deleted(void)
virt_map(vm, EXITS_TEST_GVA, EXITS_TEST_GPA, EXITS_TEST_NPAGES);
- /* Request to access page privately */
- vm_mem_set_private(vm, EXITS_TEST_GPA, EXITS_TEST_SIZE);
+ /* Request to access page privately. */
+ if (!kvm_has_gmem_attributes)
+ vm_mem_set_private(vm, EXITS_TEST_GPA, EXITS_TEST_SIZE);
pthread_create(&vm_thread, NULL,
(void *(*)(void *))run_vcpu_get_exit_reason,
@@ -74,10 +75,26 @@ static void test_private_access_memslot_deleted(void)
pthread_join(vm_thread, &thread_return);
exit_reason = (u32)(u64)thread_return;
- TEST_ASSERT_EQ(exit_reason, KVM_EXIT_MEMORY_FAULT);
- TEST_ASSERT_EQ(vcpu->run->memory_fault.flags, KVM_MEMORY_EXIT_FLAG_PRIVATE);
- TEST_ASSERT_EQ(vcpu->run->memory_fault.gpa, EXITS_TEST_GPA);
- TEST_ASSERT_EQ(vcpu->run->memory_fault.size, EXITS_TEST_SIZE);
+ /*
+ * If attributes are tracked per-gmem, deleting the memslot that points
+ * at the gmem instance effectively makes the memory shared, and so the
+ * read should trigger emulated MMIO.
+ *
+ * If attributes are tracked per-VM, deleting the memslot shouldn't
+ * affect the private attribute, and so KVM should generate a memory
+ * fault exit (emulated MMIO on private GPAs is disallowed).
+ */
+ if (kvm_has_gmem_attributes) {
+ TEST_ASSERT_EQ(exit_reason, KVM_EXIT_MMIO);
+ TEST_ASSERT_EQ(vcpu->run->mmio.phys_addr, EXITS_TEST_GPA);
+ TEST_ASSERT_EQ(vcpu->run->mmio.len, sizeof(u64));
+ TEST_ASSERT_EQ(vcpu->run->mmio.is_write, false);
+ } else {
+ TEST_ASSERT_EQ(exit_reason, KVM_EXIT_MEMORY_FAULT);
+ TEST_ASSERT_EQ(vcpu->run->memory_fault.flags, KVM_MEMORY_EXIT_FLAG_PRIVATE);
+ TEST_ASSERT_EQ(vcpu->run->memory_fault.gpa, EXITS_TEST_GPA);
+ TEST_ASSERT_EQ(vcpu->run->memory_fault.size, EXITS_TEST_SIZE);
+ }
kvm_vm_free(vm);
}
@@ -88,6 +105,13 @@ static void test_private_access_memslot_not_private(void)
struct kvm_vcpu *vcpu;
u32 exit_reason;
+ /*
+ * Accessing non-private memory as private with a software-protected VM
+ * isn't possible when doing in-place conversions.
+ */
+ if (kvm_has_gmem_attributes)
+ return;
+
vm = vm_create_shape_with_one_vcpu(protected_vm_shape, &vcpu,
guest_repeatedly_read);
--
2.55.0.rc0.738.g0c8ab3ebcc-goog
^ permalink raw reply related
* [PATCH v8 44/46] KVM: selftests: Make TEST_EXPECT_SIGBUS thread-safe
From: Ackerley Tng via B4 Relay @ 2026-06-19 0:32 UTC (permalink / raw)
To: aik, andrew.jones, binbin.wu, brauner, chao.p.peng, david,
jmattson, jthoughton, michael.roth, oupton, pankaj.gupta, qperret,
rick.p.edgecombe, rientjes, shivankg, steven.price, tabba, willy,
wyihan, yan.y.zhao, forkloop, pratyush, suzuki.poulose,
aneesh.kumar, liam, Paolo Bonzini, Sean Christopherson,
Thomas Gleixner, Ingo Molnar, Borislav Petkov, Dave Hansen, x86,
H. Peter Anvin, Steven Rostedt, Masami Hiramatsu,
Mathieu Desnoyers, Jonathan Corbet, Shuah Khan, Shuah Khan,
Vishal Annapurve, Andrew Morton, Chris Li, Kairui Song,
Kemeng Shi, Nhat Pham, Barry Song, Axel Rasmussen, Yuanchu Xie,
Wei Xu, Youngjun Park, Qi Zheng, Shakeel Butt, Kiryl Shutsemau,
Baoquan He, Jason Gunthorpe, Vlastimil Babka, Baoquan He
Cc: kvm, linux-kernel, linux-trace-kernel, linux-doc, linux-kselftest,
linux-mm, linux-coco, Ackerley Tng
In-Reply-To: <20260618-gmem-inplace-conversion-v8-0-9d2959357853@google.com>
From: Ackerley Tng <ackerleytng@google.com>
The TEST_EXPECT_SIGBUS macro is not thread-safe as it uses a global
sigjmp_buf and installs a global SIGBUS signal handler. If multiple threads
execute the macro concurrently, they will race on installing the signal
handler and stomp on other threads' jump buffers, leading to incorrect test
behavior.
Make TEST_EXPECT_SIGBUS thread-safe with the following changes:
Share the KVM tests' global signal handler. sigaction() applies to all
threads; without sharing a global signal handler, one thread may have
removed the signal handler that another thread added, hence leading to
unexpected signals.
The alternative of layering signal handlers was considered, but calling
sigaction() within TEST_EXPECT_SIGBUS() necessarily creates a race. To
avoid adding new setup and teardown routines to do sigaction() and keep
usage of TEST_EXPECT_SIGBUS() simple, share the KVM tests' global signal
handler.
Opportunistically rename report_unexpected_signal to
catchall_signal_handler.
To continue to only expect SIGBUS within specific regions of code, use a
thread-specific variable, expecting_sigbus, to replace installing and
removing signal handlers.
Make the execution environment for the thread, sigjmp_buf, a
thread-specific variable.
As part of TEST_EXPECT_SIGBUS(), assert the prerequisite for this setup,
that the current signal handler is the catchall_signal_handler.
Signed-off-by: Ackerley Tng <ackerleytng@google.com>
---
tools/testing/selftests/kvm/include/test_util.h | 32 +++++++++++++------------
tools/testing/selftests/kvm/lib/kvm_util.c | 18 ++++++++++----
tools/testing/selftests/kvm/lib/test_util.c | 7 ------
3 files changed, 30 insertions(+), 27 deletions(-)
diff --git a/tools/testing/selftests/kvm/include/test_util.h b/tools/testing/selftests/kvm/include/test_util.h
index 51287fac8138a..bd75162ec868d 100644
--- a/tools/testing/selftests/kvm/include/test_util.h
+++ b/tools/testing/selftests/kvm/include/test_util.h
@@ -82,21 +82,23 @@ do { \
__builtin_unreachable(); \
} while (0)
-extern sigjmp_buf expect_sigbus_jmpbuf;
-void expect_sigbus_handler(int signum);
-
-#define TEST_EXPECT_SIGBUS(action) \
-do { \
- struct sigaction sa_old, sa_new = { \
- .sa_handler = expect_sigbus_handler, \
- }; \
- \
- sigaction(SIGBUS, &sa_new, &sa_old); \
- if (sigsetjmp(expect_sigbus_jmpbuf, 1) == 0) { \
- action; \
- TEST_FAIL("'%s' should have triggered SIGBUS", #action); \
- } \
- sigaction(SIGBUS, &sa_old, NULL); \
+extern __thread sigjmp_buf expect_sigbus_jmpbuf;
+extern __thread volatile sig_atomic_t expecting_sigbus;
+extern void catchall_signal_handler(int signum);
+
+#define TEST_EXPECT_SIGBUS(action) \
+do { \
+ struct sigaction __sa = {}; \
+ \
+ TEST_ASSERT_EQ(sigaction(SIGBUS, NULL, &__sa), 0); \
+ TEST_ASSERT_EQ(__sa.sa_handler, &catchall_signal_handler); \
+ \
+ expecting_sigbus = true; \
+ if (sigsetjmp(expect_sigbus_jmpbuf, 1) == 0) { \
+ action; \
+ TEST_FAIL("'%s' should have triggered SIGBUS", #action);\
+ } \
+ expecting_sigbus = false; \
} while (0)
size_t parse_size(const char *size);
diff --git a/tools/testing/selftests/kvm/lib/kvm_util.c b/tools/testing/selftests/kvm/lib/kvm_util.c
index 6b304e8a0e0d5..b4f104436875b 100644
--- a/tools/testing/selftests/kvm/lib/kvm_util.c
+++ b/tools/testing/selftests/kvm/lib/kvm_util.c
@@ -2292,13 +2292,20 @@ __weak void kvm_selftest_arch_init(void)
{
}
-static void report_unexpected_signal(int signum)
+__thread sigjmp_buf expect_sigbus_jmpbuf;
+__thread volatile sig_atomic_t expecting_sigbus;
+
+void catchall_signal_handler(int signum)
{
+ switch (signum) {
+ case SIGBUS: {
+ if (expecting_sigbus)
+ siglongjmp(expect_sigbus_jmpbuf, 1);
+
+ TEST_FAIL("Unexpected SIGBUS (%d)\n", signum);
+ }
#define KVM_CASE_SIGNUM(sig) \
case sig: TEST_FAIL("Unexpected " #sig " (%d)\n", signum)
-
- switch (signum) {
- KVM_CASE_SIGNUM(SIGBUS);
KVM_CASE_SIGNUM(SIGSEGV);
KVM_CASE_SIGNUM(SIGILL);
KVM_CASE_SIGNUM(SIGFPE);
@@ -2310,12 +2317,13 @@ static void report_unexpected_signal(int signum)
void __attribute((constructor)) kvm_selftest_init(void)
{
struct sigaction sig_sa = {
- .sa_handler = report_unexpected_signal,
+ .sa_handler = catchall_signal_handler,
};
/* Tell stdout not to buffer its content. */
setbuf(stdout, NULL);
+ expecting_sigbus = false;
sigaction(SIGBUS, &sig_sa, NULL);
sigaction(SIGSEGV, &sig_sa, NULL);
sigaction(SIGILL, &sig_sa, NULL);
diff --git a/tools/testing/selftests/kvm/lib/test_util.c b/tools/testing/selftests/kvm/lib/test_util.c
index bab1bd2b775b6..30eb701e4becd 100644
--- a/tools/testing/selftests/kvm/lib/test_util.c
+++ b/tools/testing/selftests/kvm/lib/test_util.c
@@ -18,13 +18,6 @@
#include "test_util.h"
-sigjmp_buf expect_sigbus_jmpbuf;
-
-void __attribute__((used)) expect_sigbus_handler(int signum)
-{
- siglongjmp(expect_sigbus_jmpbuf, 1);
-}
-
/*
* Random number generator that is usable from guest code. This is the
* Park-Miller LCG using standard constants.
--
2.55.0.rc0.738.g0c8ab3ebcc-goog
^ permalink raw reply related
* [PATCH v8 45/46] KVM: selftests: Update private_mem_conversions_test to mmap() guest_memfd
From: Ackerley Tng via B4 Relay @ 2026-06-19 0:32 UTC (permalink / raw)
To: aik, andrew.jones, binbin.wu, brauner, chao.p.peng, david,
jmattson, jthoughton, michael.roth, oupton, pankaj.gupta, qperret,
rick.p.edgecombe, rientjes, shivankg, steven.price, tabba, willy,
wyihan, yan.y.zhao, forkloop, pratyush, suzuki.poulose,
aneesh.kumar, liam, Paolo Bonzini, Sean Christopherson,
Thomas Gleixner, Ingo Molnar, Borislav Petkov, Dave Hansen, x86,
H. Peter Anvin, Steven Rostedt, Masami Hiramatsu,
Mathieu Desnoyers, Jonathan Corbet, Shuah Khan, Shuah Khan,
Vishal Annapurve, Andrew Morton, Chris Li, Kairui Song,
Kemeng Shi, Nhat Pham, Barry Song, Axel Rasmussen, Yuanchu Xie,
Wei Xu, Youngjun Park, Qi Zheng, Shakeel Butt, Kiryl Shutsemau,
Baoquan He, Jason Gunthorpe, Vlastimil Babka, Baoquan He
Cc: kvm, linux-kernel, linux-trace-kernel, linux-doc, linux-kselftest,
linux-mm, linux-coco, Ackerley Tng
In-Reply-To: <20260618-gmem-inplace-conversion-v8-0-9d2959357853@google.com>
From: Ackerley Tng <ackerleytng@google.com>
Update the private memory conversions selftest to also test conversions
that are done "in-place" via per-guest_memfd memory attributes. In-place
conversions require the host to be able to mmap() the guest_memfd so that
the host and guest can share the same backing physical memory.
This includes several updates, that are conditioned on the system
supporting per-guest_memfd attributes (kvm_has_gmem_attributes):
1. Set up guest_memfd requesting MMAP and INIT_SHARED.
2. With in-place conversions, the host's mapping points directly to the
guest's memory. When the guest converts a region to private, host access
to that region is blocked. Update the test to expect a SIGBUS when
attempting to access the host virtual address (HVA) of private memory.
3. Use vm_mem_set_memory_attributes(), which chooses how to set memory
attributes based on whether kvm_has_gmem_attributes.
Restrict the test to using VM_MEM_SRC_SHMEM because guest_memfd's required
mmap() flags and page sizes happens to align with those of
VM_MEM_SRC_SHMEM. As long as VM_MEM_SRC_SHMEM is used for src_type,
vm_mem_add() works as intended.
Signed-off-by: Ackerley Tng <ackerleytng@google.com>
Co-developed-by: Sean Christopherson <seanjc@google.com>
Signed-off-by: Sean Christopherson <seanjc@google.com>
---
.../kvm/x86/private_mem_conversions_test.c | 44 ++++++++++++++++++----
1 file changed, 36 insertions(+), 8 deletions(-)
diff --git a/tools/testing/selftests/kvm/x86/private_mem_conversions_test.c b/tools/testing/selftests/kvm/x86/private_mem_conversions_test.c
index 289ad10063fca..4308c67952310 100644
--- a/tools/testing/selftests/kvm/x86/private_mem_conversions_test.c
+++ b/tools/testing/selftests/kvm/x86/private_mem_conversions_test.c
@@ -306,9 +306,12 @@ static void handle_exit_hypercall(struct kvm_vcpu *vcpu)
if (do_fallocate)
vm_guest_mem_fallocate(vm, gpa, size, map_shared);
- if (set_attributes)
- vm_set_memory_attributes(vm, gpa, size,
- map_shared ? 0 : KVM_MEMORY_ATTRIBUTE_PRIVATE);
+ if (set_attributes) {
+ u64 attrs = map_shared ? 0 : KVM_MEMORY_ATTRIBUTE_PRIVATE;
+
+ vm_mem_set_memory_attributes(vm, gpa, size, attrs);
+ }
+
run->hypercall.ret = 0;
}
@@ -352,8 +355,20 @@ static void *__test_mem_conversions(void *__vcpu)
size_t nr_bytes = min_t(size_t, vm->page_size, size - i);
u8 *hva = addr_gpa2hva(vm, gpa + i);
- /* In all cases, the host should observe the shared data. */
- memcmp_h(hva, gpa + i, uc.args[3], nr_bytes);
+ /*
+ * When using per-guest_memfd memory attributes,
+ * i.e. in-place conversion, host accesses will
+ * point at guest memory and should SIGBUS when
+ * guest memory is private. When using per-VM
+ * attributes, i.e. separate backing for shared
+ * vs. private, the host should always observe
+ * the shared data.
+ */
+ if (kvm_has_gmem_attributes &&
+ uc.args[0] == SYNC_PRIVATE)
+ TEST_EXPECT_SIGBUS(READ_ONCE(*hva));
+ else
+ memcmp_h(hva, gpa + i, uc.args[3], nr_bytes);
/* For shared, write the new pattern to guest memory. */
if (uc.args[0] == SYNC_SHARED)
@@ -382,6 +397,7 @@ static void test_mem_conversions(enum vm_mem_backing_src_type src_type, u32 nr_v
const size_t slot_size = memfd_size / nr_memslots;
struct kvm_vcpu *vcpus[KVM_MAX_VCPUS];
pthread_t threads[KVM_MAX_VCPUS];
+ u64 gmem_flags;
struct kvm_vm *vm;
int memfd, i;
@@ -397,12 +413,17 @@ static void test_mem_conversions(enum vm_mem_backing_src_type src_type, u32 nr_v
vm_enable_cap(vm, KVM_CAP_EXIT_HYPERCALL, (1 << KVM_HC_MAP_GPA_RANGE));
- memfd = vm_create_guest_memfd(vm, memfd_size, 0);
+ if (kvm_has_gmem_attributes)
+ gmem_flags = GUEST_MEMFD_FLAG_MMAP | GUEST_MEMFD_FLAG_INIT_SHARED;
+ else
+ gmem_flags = 0;
+
+ memfd = vm_create_guest_memfd(vm, memfd_size, gmem_flags);
for (i = 0; i < nr_memslots; i++)
vm_mem_add(vm, src_type, BASE_DATA_GPA + slot_size * i,
BASE_DATA_SLOT + i, slot_size / vm->page_size,
- KVM_MEM_GUEST_MEMFD, memfd, slot_size * i, 0);
+ KVM_MEM_GUEST_MEMFD, memfd, slot_size * i, gmem_flags);
for (i = 0; i < nr_vcpus; i++) {
gpa_t gpa = BASE_DATA_GPA + i * per_cpu_size;
@@ -452,17 +473,24 @@ static void usage(const char *cmd)
int main(int argc, char *argv[])
{
- enum vm_mem_backing_src_type src_type = DEFAULT_VM_MEM_SRC;
+ enum vm_mem_backing_src_type src_type;
u32 nr_memslots = 1;
u32 nr_vcpus = 1;
int opt;
TEST_REQUIRE(kvm_check_cap(KVM_CAP_VM_TYPES) & BIT(KVM_X86_SW_PROTECTED_VM));
+ src_type = kvm_has_gmem_attributes ? VM_MEM_SRC_SHMEM :
+ DEFAULT_VM_MEM_SRC;
+
while ((opt = getopt(argc, argv, "hm:s:n:")) != -1) {
switch (opt) {
case 's':
src_type = parse_backing_src_type(optarg);
+ TEST_ASSERT(!kvm_has_gmem_attributes ||
+ src_type == VM_MEM_SRC_SHMEM,
+ "Testing in-place conversions, only %s mem_type supported\n",
+ vm_mem_backing_src_alias(VM_MEM_SRC_SHMEM)->name);
break;
case 'n':
nr_vcpus = atoi_positive("nr_vcpus", optarg);
--
2.55.0.rc0.738.g0c8ab3ebcc-goog
^ permalink raw reply related
* [PATCH v8 42/46] KVM: selftests: Provide common function to set memory attributes
From: Ackerley Tng via B4 Relay @ 2026-06-19 0:32 UTC (permalink / raw)
To: aik, andrew.jones, binbin.wu, brauner, chao.p.peng, david,
jmattson, jthoughton, michael.roth, oupton, pankaj.gupta, qperret,
rick.p.edgecombe, rientjes, shivankg, steven.price, tabba, willy,
wyihan, yan.y.zhao, forkloop, pratyush, suzuki.poulose,
aneesh.kumar, liam, Paolo Bonzini, Sean Christopherson,
Thomas Gleixner, Ingo Molnar, Borislav Petkov, Dave Hansen, x86,
H. Peter Anvin, Steven Rostedt, Masami Hiramatsu,
Mathieu Desnoyers, Jonathan Corbet, Shuah Khan, Shuah Khan,
Vishal Annapurve, Andrew Morton, Chris Li, Kairui Song,
Kemeng Shi, Nhat Pham, Barry Song, Axel Rasmussen, Yuanchu Xie,
Wei Xu, Youngjun Park, Qi Zheng, Shakeel Butt, Kiryl Shutsemau,
Baoquan He, Jason Gunthorpe, Vlastimil Babka, Baoquan He
Cc: kvm, linux-kernel, linux-trace-kernel, linux-doc, linux-kselftest,
linux-mm, linux-coco, Ackerley Tng
In-Reply-To: <20260618-gmem-inplace-conversion-v8-0-9d2959357853@google.com>
From: Sean Christopherson <seanjc@google.com>
Introduce vm_mem_set_memory_attributes(), which handles setting of memory
attributes for a range of guest physical addresses, regardless of whether
the attributes should be set via guest_memfd or via the memory attributes
at the VM level.
Refactor existing vm_mem_set_{shared,private} functions to use the new
function. Opportunistically update the size parameter to use size_t instead
of u64.
Signed-off-by: Sean Christopherson <seanjc@google.com>
Co-developed-by: Ackerley Tng <ackerleytng@google.com>
Signed-off-by: Ackerley Tng <ackerleytng@google.com>
---
tools/testing/selftests/kvm/include/kvm_util.h | 46 +++++++++++++++++++-------
1 file changed, 34 insertions(+), 12 deletions(-)
diff --git a/tools/testing/selftests/kvm/include/kvm_util.h b/tools/testing/selftests/kvm/include/kvm_util.h
index 3a6b1fa7f26ef..db1442da21bb1 100644
--- a/tools/testing/selftests/kvm/include/kvm_util.h
+++ b/tools/testing/selftests/kvm/include/kvm_util.h
@@ -454,18 +454,6 @@ static inline void vm_set_memory_attributes(struct kvm_vm *vm, gpa_t gpa,
vm_ioctl(vm, KVM_SET_MEMORY_ATTRIBUTES, &attr);
}
-static inline void vm_mem_set_private(struct kvm_vm *vm, gpa_t gpa,
- u64 size)
-{
- vm_set_memory_attributes(vm, gpa, size, KVM_MEMORY_ATTRIBUTE_PRIVATE);
-}
-
-static inline void vm_mem_set_shared(struct kvm_vm *vm, gpa_t gpa,
- u64 size)
-{
- vm_set_memory_attributes(vm, gpa, size, 0);
-}
-
static inline int __gmem_set_memory_attributes(int fd, u64 offset,
size_t size, u64 attributes,
u64 *error_offset)
@@ -532,6 +520,40 @@ static inline void gmem_set_shared(int fd, u64 offset, size_t size)
gmem_set_memory_attributes(fd, offset, size, 0);
}
+static inline void vm_mem_set_memory_attributes(struct kvm_vm *vm, gpa_t gpa,
+ size_t size, u64 attrs)
+{
+ if (kvm_has_gmem_attributes) {
+ gpa_t end = gpa + size;
+ off_t fd_offset;
+ gpa_t addr;
+ size_t len;
+ int fd;
+
+ for (addr = gpa; addr < end; addr += len) {
+ fd = kvm_gpa_to_guest_memfd(vm, addr, &fd_offset, &len);
+ len = min(end - addr, len);
+
+ gmem_set_memory_attributes(fd, fd_offset, len, attrs);
+ }
+ } else {
+ vm_set_memory_attributes(vm, gpa, size, attrs);
+ }
+}
+
+static inline void vm_mem_set_private(struct kvm_vm *vm, gpa_t gpa,
+ size_t size)
+{
+ vm_mem_set_memory_attributes(vm, gpa, size,
+ KVM_MEMORY_ATTRIBUTE_PRIVATE);
+}
+
+static inline void vm_mem_set_shared(struct kvm_vm *vm, gpa_t gpa,
+ size_t size)
+{
+ vm_mem_set_memory_attributes(vm, gpa, size, 0);
+}
+
void vm_guest_mem_fallocate(struct kvm_vm *vm, gpa_t gpa, u64 size,
bool punch_hole);
--
2.55.0.rc0.738.g0c8ab3ebcc-goog
^ permalink raw reply related
* [PATCH v8 43/46] KVM: selftests: Check fd/flags provided to mmap() when setting up memslot
From: Ackerley Tng via B4 Relay @ 2026-06-19 0:32 UTC (permalink / raw)
To: aik, andrew.jones, binbin.wu, brauner, chao.p.peng, david,
jmattson, jthoughton, michael.roth, oupton, pankaj.gupta, qperret,
rick.p.edgecombe, rientjes, shivankg, steven.price, tabba, willy,
wyihan, yan.y.zhao, forkloop, pratyush, suzuki.poulose,
aneesh.kumar, liam, Paolo Bonzini, Sean Christopherson,
Thomas Gleixner, Ingo Molnar, Borislav Petkov, Dave Hansen, x86,
H. Peter Anvin, Steven Rostedt, Masami Hiramatsu,
Mathieu Desnoyers, Jonathan Corbet, Shuah Khan, Shuah Khan,
Vishal Annapurve, Andrew Morton, Chris Li, Kairui Song,
Kemeng Shi, Nhat Pham, Barry Song, Axel Rasmussen, Yuanchu Xie,
Wei Xu, Youngjun Park, Qi Zheng, Shakeel Butt, Kiryl Shutsemau,
Baoquan He, Jason Gunthorpe, Vlastimil Babka, Baoquan He
Cc: kvm, linux-kernel, linux-trace-kernel, linux-doc, linux-kselftest,
linux-mm, linux-coco, Ackerley Tng
In-Reply-To: <20260618-gmem-inplace-conversion-v8-0-9d2959357853@google.com>
From: Sean Christopherson <seanjc@google.com>
Check that a valid fd provided to mmap() must be accompanied by MAP_SHARED.
With an invalid fd (usually used for anonymous mappings), there are no
constraints on mmap() flags.
Add this check to make sure that when a guest_memfd is used as region->fd,
the flag provided to mmap() will include MAP_SHARED.
Signed-off-by: Sean Christopherson <seanjc@google.com>
[Rephrase assertion message.]
Signed-off-by: Ackerley Tng <ackerleytng@google.com>
---
tools/testing/selftests/kvm/lib/kvm_util.c | 3 +++
1 file changed, 3 insertions(+)
diff --git a/tools/testing/selftests/kvm/lib/kvm_util.c b/tools/testing/selftests/kvm/lib/kvm_util.c
index 0b2256ea65ff9..6b304e8a0e0d5 100644
--- a/tools/testing/selftests/kvm/lib/kvm_util.c
+++ b/tools/testing/selftests/kvm/lib/kvm_util.c
@@ -1110,6 +1110,9 @@ void vm_mem_add(struct kvm_vm *vm, enum vm_mem_backing_src_type src_type,
src_type == VM_MEM_SRC_SHARED_HUGETLB);
}
+ TEST_ASSERT(region->fd == -1 || backing_src_is_shared(src_type),
+ "A valid fd provided to mmap() must be accompanied by MAP_SHARED.");
+
region->mmap_start = __kvm_mmap(region->mmap_size, PROT_READ | PROT_WRITE,
vm_mem_backing_src_alias(src_type)->flag,
region->fd, mmap_offset);
--
2.55.0.rc0.738.g0c8ab3ebcc-goog
^ permalink raw reply related
* [PATCH v8 41/46] KVM: selftests: Provide function to look up guest_memfd details from gpa
From: Ackerley Tng via B4 Relay @ 2026-06-19 0:32 UTC (permalink / raw)
To: aik, andrew.jones, binbin.wu, brauner, chao.p.peng, david,
jmattson, jthoughton, michael.roth, oupton, pankaj.gupta, qperret,
rick.p.edgecombe, rientjes, shivankg, steven.price, tabba, willy,
wyihan, yan.y.zhao, forkloop, pratyush, suzuki.poulose,
aneesh.kumar, liam, Paolo Bonzini, Sean Christopherson,
Thomas Gleixner, Ingo Molnar, Borislav Petkov, Dave Hansen, x86,
H. Peter Anvin, Steven Rostedt, Masami Hiramatsu,
Mathieu Desnoyers, Jonathan Corbet, Shuah Khan, Shuah Khan,
Vishal Annapurve, Andrew Morton, Chris Li, Kairui Song,
Kemeng Shi, Nhat Pham, Barry Song, Axel Rasmussen, Yuanchu Xie,
Wei Xu, Youngjun Park, Qi Zheng, Shakeel Butt, Kiryl Shutsemau,
Baoquan He, Jason Gunthorpe, Vlastimil Babka, Baoquan He
Cc: kvm, linux-kernel, linux-trace-kernel, linux-doc, linux-kselftest,
linux-mm, linux-coco, Ackerley Tng
In-Reply-To: <20260618-gmem-inplace-conversion-v8-0-9d2959357853@google.com>
From: Ackerley Tng <ackerleytng@google.com>
Introduce a new helper, kvm_gpa_to_guest_memfd(), to find the
guest_memfd-related details of a memory region that contains a given guest
physical address (GPA).
The function returns the file descriptor for the memfd, the offset into
the file that corresponds to the GPA, and the number of bytes remaining
in the region from that GPA.
kvm_gpa_to_guest_memfd() was factored out from vm_guest_mem_fallocate();
refactor vm_guest_mem_fallocate() to use the new helper.
Signed-off-by: Ackerley Tng <ackerleytng@google.com>
Co-developed-by: Sean Christopherson <seanjc@google.com>
Signed-off-by: Sean Christopherson <seanjc@google.com>
---
tools/testing/selftests/kvm/include/kvm_util.h | 3 +++
tools/testing/selftests/kvm/lib/kvm_util.c | 37 ++++++++++++++++----------
2 files changed, 26 insertions(+), 14 deletions(-)
diff --git a/tools/testing/selftests/kvm/include/kvm_util.h b/tools/testing/selftests/kvm/include/kvm_util.h
index 79ab64ac8b869..3a6b1fa7f26ef 100644
--- a/tools/testing/selftests/kvm/include/kvm_util.h
+++ b/tools/testing/selftests/kvm/include/kvm_util.h
@@ -428,6 +428,9 @@ static inline void vm_enable_cap(struct kvm_vm *vm, u32 cap, u64 arg0)
vm_ioctl(vm, KVM_ENABLE_CAP, &enable_cap);
}
+int kvm_gpa_to_guest_memfd(struct kvm_vm *vm, gpa_t gpa, off_t *fd_offset,
+ size_t *nr_bytes);
+
/*
* KVM_SET_MEMORY_ATTRIBUTES{,2} overwrites _all_ attributes. These
* flows need significant enhancements to support multiple attributes.
diff --git a/tools/testing/selftests/kvm/lib/kvm_util.c b/tools/testing/selftests/kvm/lib/kvm_util.c
index 524ef97d634bf..0b2256ea65ff9 100644
--- a/tools/testing/selftests/kvm/lib/kvm_util.c
+++ b/tools/testing/selftests/kvm/lib/kvm_util.c
@@ -1305,27 +1305,20 @@ void vm_guest_mem_fallocate(struct kvm_vm *vm, u64 base, u64 size,
bool punch_hole)
{
const int mode = FALLOC_FL_KEEP_SIZE | (punch_hole ? FALLOC_FL_PUNCH_HOLE : 0);
- struct userspace_mem_region *region;
u64 end = base + size;
- gpa_t gpa, len;
off_t fd_offset;
- int ret;
+ int fd, ret;
+ size_t len;
+ gpa_t gpa;
for (gpa = base; gpa < end; gpa += len) {
- u64 offset;
-
- region = userspace_mem_region_find(vm, gpa, gpa);
- TEST_ASSERT(region && region->region.flags & KVM_MEM_GUEST_MEMFD,
- "Private memory region not found for GPA 0x%lx", gpa);
+ fd = kvm_gpa_to_guest_memfd(vm, gpa, &fd_offset, &len);
+ len = min(end - gpa, len);
- offset = gpa - region->region.guest_phys_addr;
- fd_offset = region->region.guest_memfd_offset + offset;
- len = min_t(u64, end - gpa, region->region.memory_size - offset);
-
- ret = fallocate(region->region.guest_memfd, mode, fd_offset, len);
+ ret = fallocate(fd, mode, fd_offset, len);
TEST_ASSERT(!ret, "fallocate() failed to %s at %lx (len = %lu), fd = %d, mode = %x, offset = %lx",
punch_hole ? "punch hole" : "allocate", gpa, len,
- region->region.guest_memfd, mode, fd_offset);
+ fd, mode, fd_offset);
}
}
@@ -1662,6 +1655,22 @@ void *addr_gpa2alias(struct kvm_vm *vm, gpa_t gpa)
return (void *) ((uintptr_t) region->host_alias + offset);
}
+int kvm_gpa_to_guest_memfd(struct kvm_vm *vm, gpa_t gpa, off_t *fd_offset,
+ size_t *nr_bytes)
+{
+ struct userspace_mem_region *region;
+ gpa_t gpa_offset;
+
+ region = userspace_mem_region_find(vm, gpa, gpa);
+ TEST_ASSERT(region && region->region.flags & KVM_MEM_GUEST_MEMFD,
+ "guest_memfd memory region not found for GPA 0x%lx", gpa);
+
+ gpa_offset = gpa - region->region.guest_phys_addr;
+ *fd_offset = region->region.guest_memfd_offset + gpa_offset;
+ *nr_bytes = region->region.memory_size - gpa_offset;
+ return region->region.guest_memfd;
+}
+
/* Create an interrupt controller chip for the specified VM. */
void vm_create_irqchip(struct kvm_vm *vm)
{
--
2.55.0.rc0.738.g0c8ab3ebcc-goog
^ permalink raw reply related
page: next (older) | prev (newer) | latest
- recent:[subjects (threaded)|topics (new)|topics (active)]
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox