From 4793e8a6e20e4c17ed4e755ea40e5912cc3539af Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 1 Jun 2026 17:38:28 +0200 Subject: [PATCH 01/17] rv: Fix __user specifier usage in extract_params() The attributes variables extracted from syscalls in the helper are both defined with the __user specifier although only the actual pointer to user data should be marked. Remove the __user specifier from attr. Reported-by: kernel test robot Closes: https://lore.kernel.org/oe-kbuild-all/202604150820.Ny143u6X-lkp@intel.com Fixes: b133207deb72 ("rv: Add nomiss deadline monitor") Reviewed-by: Wen Yang Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-2-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- kernel/trace/rv/monitors/deadline/deadline.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kernel/trace/rv/monitors/deadline/deadline.h b/kernel/trace/rv/monitors/deadline/deadline.h index 0bbfd2543329..78fca873d61e 100644 --- a/kernel/trace/rv/monitors/deadline/deadline.h +++ b/kernel/trace/rv/monitors/deadline/deadline.h @@ -95,7 +95,8 @@ static inline u8 get_server_type(struct task_struct *tsk) static inline int extract_params(struct pt_regs *regs, long id, pid_t *pid_out) { size_t size = offsetofend(struct sched_attr, sched_flags); - struct sched_attr __user *uattr, attr; + struct sched_attr __user *uattr; + struct sched_attr attr; int new_policy = -1, ret; unsigned long args[6]; From e32d7f404d7d9dac307c1cd9a1fe132fa62ab6d6 Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 1 Jun 2026 17:38:29 +0200 Subject: [PATCH 02/17] rv: Reset per-task DA monitors before releasing the slot Per-task monitors use task_mon_slot to determine which slot in the array to use for the monitor. During destruction, this slot is returned but this is done before resetting the monitor. As a result, the monitor's reset is in fact resetting a slot that is outside of the array (RV_PER_TASK_MONITOR_INIT). Release the slot only after the reset to avoid out-of-bound memory access. Fixes: f5587d1b6ec93 ("rv: Add Hybrid Automata monitor type") Cc: stable@vger.kernel.org Suggested-by: Wen Yang Reviewed-by: Wen Yang Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-3-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- include/rv/da_monitor.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h index 39765ff6f098..1459fb3dfee6 100644 --- a/include/rv/da_monitor.h +++ b/include/rv/da_monitor.h @@ -309,10 +309,11 @@ static inline void da_monitor_destroy(void) WARN_ONCE(1, "Disabling a disabled monitor: " __stringify(MONITOR_NAME)); return; } - rv_put_task_monitor_slot(task_mon_slot); - task_mon_slot = RV_PER_TASK_MONITOR_INIT; da_monitor_reset_all(); + + rv_put_task_monitor_slot(task_mon_slot); + task_mon_slot = RV_PER_TASK_MONITOR_INIT; } #elif RV_MON_TYPE == RV_MON_PER_OBJ From c3d016ea823a9941ab8cbcef01a500821ff0cf16 Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 1 Jun 2026 17:38:30 +0200 Subject: [PATCH 03/17] rv: Prevent in-flight per-task handlers from using invalid slots Per-task monitors use a slot in the task_struct->rv[] array and store that locally (e.g. task_mon_slot), this slot is returned during the destruction process but currently hanlers can be running while that slot is returning and this race may lead to accessing an invalid slot. Synchronise with all in-flight tracepoint handlers using tracepoint_synchronize_unregister() before returning the slot. Fixes: f5587d1b6ec9 ("rv: Add Hybrid Automata monitor type") Fixes: a9769a5b9878 ("rv: Add support for LTL monitors") Suggested-by: Wen Yang Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-4-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- include/rv/da_monitor.h | 4 ++++ include/rv/ltl_monitor.h | 1 + 2 files changed, 5 insertions(+) diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h index 1459fb3dfee6..cc97cc5dfbfd 100644 --- a/include/rv/da_monitor.h +++ b/include/rv/da_monitor.h @@ -302,6 +302,9 @@ static int da_monitor_init(void) /* * da_monitor_destroy - return the allocated slot + * + * Wait for all in-flight handlers before returning the slot to avoid + * out-of-bound accesses. */ static inline void da_monitor_destroy(void) { @@ -310,6 +313,7 @@ static inline void da_monitor_destroy(void) return; } + tracepoint_synchronize_unregister(); da_monitor_reset_all(); rv_put_task_monitor_slot(task_mon_slot); diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h index eff60cd61106..38e792401f76 100644 --- a/include/rv/ltl_monitor.h +++ b/include/rv/ltl_monitor.h @@ -77,6 +77,7 @@ static void ltl_monitor_destroy(void) { rv_detach_trace_probe(name, task_newtask, handle_task_newtask); + tracepoint_synchronize_unregister(); rv_put_task_monitor_slot(ltl_monitor_slot); ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT; } From 32171d828ab964dc1f05f2056a81477522a3361b Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 1 Jun 2026 17:38:31 +0200 Subject: [PATCH 04/17] rv: Ensure all pending probes terminate on per-obj monitor destroy The monitor disable/destroy sequence detaches all probes and resets the monitor's data, however it doesn't wait for pending probes. This is an issue with per-object monitors, which free the monitor storage. Call tracepoint_synchronize_unregister() to make sure to wait for all pending probes before destroying the monitor storage. Fixes: 4a24127bd6cb ("rv: Add support for per-object monitors in DA/HA") Reviewed-by: Wen Yang Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-5-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- include/rv/da_monitor.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h index cc97cc5dfbfd..a7e103654406 100644 --- a/include/rv/da_monitor.h +++ b/include/rv/da_monitor.h @@ -511,9 +511,10 @@ static inline void da_monitor_destroy(void) struct hlist_node *tmp; int bkt; + tracepoint_synchronize_unregister(); /* - * This function is called after all probes are disabled, we need only - * worry about concurrency against old events. + * This function is called after all probes are disabled and no longer + * pending, we can safely assume no concurrent user. */ synchronize_rcu(); hash_for_each_safe(da_monitor_ht, bkt, tmp, mon_storage, node) { From 2b9a8c27417eeef01967c6297def426a44776c04 Mon Sep 17 00:00:00 2001 From: Wen Yang Date: Mon, 1 Jun 2026 17:38:32 +0200 Subject: [PATCH 05/17] rv: Fix monitor start ordering and memory ordering for monitoring flag da_monitor_start() set monitoring=1 before calling da_monitor_init_hook(), may racing with the sched_switch handler: da_monitor_start() sched_switch handler ------------------------- --------------------------------- da_mon->monitoring = 1; if (da_monitoring(da_mon)) /* true */ ha_start_timer_ns(...); /* hrtimer->base == NULL, crash */ da_monitor_init_hook(da_mon); /* hrtimer_setup() sets base */ Fix the ordering and pair with release/acquire semantics: da_monitor_init_hook(da_mon); smp_store_release(&da_mon->monitoring, 1); /* da_monitor_start() */ return smp_load_acquire(&da_mon->monitoring); /* da_monitoring() */ On ARM64 a plain STR + LDR does not form a release-acquire pair, so the load can observe monitoring=1 while hrtimer->base is still NULL. The plain accesses are also data races under KCSAN. Use WRITE_ONCE for the monitoring=0 store in da_monitor_reset() to cover the reset path. Fixes: 792575348ff7 ("rv/include: Add deterministic automata monitor definition via C macros") Signed-off-by: Wen Yang Reviewed-by: Gabriele Monaco Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-6-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- include/rv/da_monitor.h | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h index a7e103654406..60dc39f2620a 100644 --- a/include/rv/da_monitor.h +++ b/include/rv/da_monitor.h @@ -82,7 +82,7 @@ static void react(enum states curr_state, enum events event) static inline void da_monitor_reset(struct da_monitor *da_mon) { da_monitor_reset_hook(da_mon); - da_mon->monitoring = 0; + WRITE_ONCE(da_mon->monitoring, 0); da_mon->curr_state = model_get_initial_state(); } @@ -95,8 +95,9 @@ static inline void da_monitor_reset(struct da_monitor *da_mon) static inline void da_monitor_start(struct da_monitor *da_mon) { da_mon->curr_state = model_get_initial_state(); - da_mon->monitoring = 1; da_monitor_init_hook(da_mon); + /* Pairs with smp_load_acquire in da_monitoring(). */ + smp_store_release(&da_mon->monitoring, 1); } /* @@ -104,7 +105,8 @@ static inline void da_monitor_start(struct da_monitor *da_mon) */ static inline bool da_monitoring(struct da_monitor *da_mon) { - return da_mon->monitoring; + /* Pairs with smp_store_release in da_monitor_start(). */ + return smp_load_acquire(&da_mon->monitoring); } /* From 713c9e1ea7623846f8e0bb657f1b9d211d1a61e6 Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 1 Jun 2026 17:38:33 +0200 Subject: [PATCH 06/17] rv: Do not rely on clean monitor when initialising HA Hybrid Automata monitors hook into the DA implementation when doing da_monitor_reset(). This function is called both on initialisation and teardown, HA monitors try to cancel a timer only when it's initialised relying on the da_mon->monitoring flag. This flag could however be corrupted during initialisation. This happens for instance on per-task monitors that share the same storage with different type of monitors like LTL or in case of races during a previous teardown. Stop relying on the monitoring flag during initialisation, assume that can have any value, so use a separate da_reset_state() skiping timer cancellation. New monitors (e.g. new tasks) are always zero-initialised so it is safe to rely on the monitoring flag for those. Reported-by: Wen Yang Closes: https://lore.kernel.org/lkml/d02c656aada7d071f083460a5c9a454363669b61.1778522945.git.wen.yang@linux.dev Suggested-by: Nam Cao Fixes: f5587d1b6ec9 ("rv: Add Hybrid Automata monitor type") Reviewed-by: Wen Yang Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-7-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- include/rv/da_monitor.h | 91 +++++++++++++++++++++++++++++++++-------- include/rv/ha_monitor.h | 2 +- 2 files changed, 76 insertions(+), 17 deletions(-) diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h index 60dc39f2620a..ec9bc88bd4c4 100644 --- a/include/rv/da_monitor.h +++ b/include/rv/da_monitor.h @@ -76,14 +76,22 @@ static void react(enum states curr_state, enum events event) model_get_state_name(curr_state)); } +/* + * da_monitor_reset_state - reset a monitor and setting it to init state + */ +static inline void da_monitor_reset_state(struct da_monitor *da_mon) +{ + WRITE_ONCE(da_mon->monitoring, 0); + da_mon->curr_state = model_get_initial_state(); +} + /* * da_monitor_reset - reset a monitor and setting it to init state */ static inline void da_monitor_reset(struct da_monitor *da_mon) { da_monitor_reset_hook(da_mon); - WRITE_ONCE(da_mon->monitoring, 0); - da_mon->curr_state = model_get_initial_state(); + da_monitor_reset_state(da_mon); } /* @@ -158,12 +166,28 @@ static struct da_monitor *da_get_monitor(void) return &DA_MON_NAME; } +/* + * __da_monitor_reset_all - reset the single monitor + */ +static void __da_monitor_reset_all(void (*reset)(struct da_monitor *)) +{ + reset(da_get_monitor()); +} + /* * da_monitor_reset_all - reset the single monitor */ static void da_monitor_reset_all(void) { - da_monitor_reset(da_get_monitor()); + __da_monitor_reset_all(da_monitor_reset); +} + +/* + * da_monitor_reset_state_all - reset the single monitor + */ +static inline void da_monitor_reset_state_all(void) +{ + __da_monitor_reset_all(da_monitor_reset_state); } /* @@ -171,7 +195,7 @@ static void da_monitor_reset_all(void) */ static inline int da_monitor_init(void) { - da_monitor_reset_all(); + da_monitor_reset_state_all(); return 0; } @@ -202,25 +226,41 @@ static struct da_monitor *da_get_monitor(void) } /* - * da_monitor_reset_all - reset all CPUs' monitor + * __da_monitor_reset_all - reset all CPUs' monitor */ -static void da_monitor_reset_all(void) +static void __da_monitor_reset_all(void (*reset)(struct da_monitor *)) { struct da_monitor *da_mon; int cpu; for_each_cpu(cpu, cpu_online_mask) { da_mon = per_cpu_ptr(&DA_MON_NAME, cpu); - da_monitor_reset(da_mon); + reset(da_mon); } } +/* + * da_monitor_reset_all - reset all CPUs' monitor + */ +static void da_monitor_reset_all(void) +{ + __da_monitor_reset_all(da_monitor_reset); +} + +/* + * da_monitor_reset_state_all - reset all CPUs' monitor + */ +static inline void da_monitor_reset_state_all(void) +{ + __da_monitor_reset_all(da_monitor_reset_state); +} + /* * da_monitor_init - initialize all CPUs' monitor */ static inline int da_monitor_init(void) { - da_monitor_reset_all(); + da_monitor_reset_state_all(); return 0; } @@ -269,19 +309,29 @@ static inline da_id_type da_get_id(struct da_monitor *da_mon) return da_get_target(da_mon)->pid; } -static void da_monitor_reset_all(void) +static void __da_monitor_reset_all(void (*reset)(struct da_monitor *)) { struct task_struct *g, *p; int cpu; read_lock(&tasklist_lock); for_each_process_thread(g, p) - da_monitor_reset(da_get_monitor(p)); + reset(da_get_monitor(p)); for_each_present_cpu(cpu) - da_monitor_reset(da_get_monitor(idle_task(cpu))); + reset(da_get_monitor(idle_task(cpu))); read_unlock(&tasklist_lock); } +static void da_monitor_reset_all(void) +{ + __da_monitor_reset_all(da_monitor_reset); +} + +static inline void da_monitor_reset_state_all(void) +{ + __da_monitor_reset_all(da_monitor_reset_state); +} + /* * da_monitor_init - initialize the per-task monitor * @@ -298,7 +348,7 @@ static int da_monitor_init(void) task_mon_slot = slot; - da_monitor_reset_all(); + da_monitor_reset_state_all(); return 0; } @@ -490,15 +540,24 @@ static inline void da_destroy_storage(da_id_type id) kfree_rcu(mon_storage, rcu); } -static void da_monitor_reset_all(void) +static void __da_monitor_reset_all(void (*reset)(struct da_monitor *)) { struct da_monitor_storage *mon_storage; int bkt; - rcu_read_lock(); + guard(rcu)(); hash_for_each_rcu(da_monitor_ht, bkt, mon_storage, node) - da_monitor_reset(&mon_storage->rv.da_mon); - rcu_read_unlock(); + reset(&mon_storage->rv.da_mon); +} + +static void da_monitor_reset_all(void) +{ + __da_monitor_reset_all(da_monitor_reset); +} + +static inline void da_monitor_reset_state_all(void) +{ + __da_monitor_reset_all(da_monitor_reset_state); } static inline int da_monitor_init(void) diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h index d59507e8cb30..bd87055567cc 100644 --- a/include/rv/ha_monitor.h +++ b/include/rv/ha_monitor.h @@ -153,12 +153,12 @@ static inline void ha_monitor_init_env(struct da_monitor *da_mon) * Called from a hook in the DA reset functions, it supplies the da_mon * corresponding to the current ha_mon. * Not all hybrid automata require the timer, still clear it for simplicity. + * Monitors that never started have their timer uninitialized, do not stop those. */ static inline void ha_monitor_reset_env(struct da_monitor *da_mon) { struct ha_monitor *ha_mon = to_ha_monitor(da_mon); - /* Initialisation resets the monitor before initialising the timer */ if (likely(da_monitoring(da_mon))) ha_cancel_timer(ha_mon); } From 700782ec8f6589c5792b323efd6e004dd183328b Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 1 Jun 2026 17:38:34 +0200 Subject: [PATCH 07/17] rv: Add automatic cleanup handlers for per-task HA monitors Hybrid automata monitors may start timers, depending on the model, these may remain active on an exiting task and cause false positives or even access freed memory. Add an enable/disable hook in the HA code, currently only populated by the per-task handler for registration and deregistration. This hooks to the sched_process_exit event and ensures the timer is stopped for every exiting task. The handler is enabled automatically but may be disabled, for instance if the monitor uses the event for another purpose (but should still manually ensure timers are stopped). Fixes: f5587d1b6ec9 ("rv: Add Hybrid Automata monitor type") Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-8-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- include/rv/ha_monitor.h | 60 +++++++++++++++++++ kernel/trace/rv/monitors/nomiss/nomiss.c | 4 +- kernel/trace/rv/monitors/opid/opid.c | 4 +- kernel/trace/rv/monitors/stall/stall.c | 4 +- .../rvgen/rvgen/templates/dot2k/main.c | 4 +- 5 files changed, 68 insertions(+), 8 deletions(-) diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h index bd87055567cc..4002b5247c46 100644 --- a/include/rv/ha_monitor.h +++ b/include/rv/ha_monitor.h @@ -28,6 +28,7 @@ static inline void ha_monitor_init_env(struct da_monitor *da_mon); static inline void ha_monitor_reset_env(struct da_monitor *da_mon); static inline void ha_setup_timer(struct ha_monitor *ha_mon); static inline bool ha_cancel_timer(struct ha_monitor *ha_mon); +static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon); static bool ha_monitor_handle_constraint(struct da_monitor *da_mon, enum states curr_state, enum events event, @@ -37,6 +38,26 @@ static bool ha_monitor_handle_constraint(struct da_monitor *da_mon, #define da_monitor_init_hook ha_monitor_init_env #define da_monitor_reset_hook ha_monitor_reset_env +#if !defined(HA_SKIP_AUTO_CLEANUP) && RV_MON_TYPE == RV_MON_PER_TASK +/* + * Automatic cleanup handlers for per-task HA monitors, only skip if you know + * what you are doing (e.g. you want to implement cleanup manually in another + * handler doing more things). + */ +static void ha_handle_sched_process_exit(void *data, struct task_struct *p, + bool group_dead); + +#define ha_monitor_enable_hook() \ + rv_attach_trace_probe(__stringify(MONITOR_NAME), sched_process_exit, \ + ha_handle_sched_process_exit) +#define ha_monitor_disable_hook() \ + rv_detach_trace_probe(__stringify(MONITOR_NAME), sched_process_exit, \ + ha_handle_sched_process_exit) +#else +#define ha_monitor_enable_hook() ((void)0) +#define ha_monitor_disable_hook() ((void)0) +#endif + #include #include @@ -115,6 +136,22 @@ static enum hrtimer_restart ha_monitor_timer_callback(struct hrtimer *hrtimer); #define ha_get_ns() 0 #endif /* HA_CLK_NS */ +static int ha_monitor_init(void) +{ + int ret; + + ret = da_monitor_init(); + if (ret == 0) + ha_monitor_enable_hook(); + return ret; +} + +static void ha_monitor_destroy(void) +{ + ha_monitor_disable_hook(); + da_monitor_destroy(); +} + /* Should be supplied by the monitor */ static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs env, u64 time_ns); static bool ha_verify_constraint(struct ha_monitor *ha_mon, @@ -200,6 +237,20 @@ static inline void ha_trace_error_env(struct ha_monitor *ha_mon, { CONCATENATE(trace_error_env_, MONITOR_NAME)(id, curr_state, event, env); } + +#if !defined(HA_SKIP_AUTO_CLEANUP) && RV_MON_TYPE == RV_MON_PER_TASK +static void ha_handle_sched_process_exit(void *data, struct task_struct *p, + bool group_dead) +{ + struct da_monitor *da_mon = da_get_monitor(p); + + if (likely(da_monitoring(da_mon))) { + da_monitor_reset(da_mon); + ha_cancel_timer_sync(to_ha_monitor(da_mon)); + } +} +#endif + #endif /* RV_MON_TYPE */ /* @@ -412,6 +463,10 @@ static inline bool ha_cancel_timer(struct ha_monitor *ha_mon) { return timer_delete(&ha_mon->timer); } +static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon) +{ + timer_delete_sync(&ha_mon->timer); +} #elif HA_TIMER_TYPE == HA_TIMER_HRTIMER /* * Helper functions to handle the monitor timer. @@ -463,6 +518,10 @@ static inline bool ha_cancel_timer(struct ha_monitor *ha_mon) { return hrtimer_try_to_cancel(&ha_mon->hrtimer) == 1; } +static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon) +{ + hrtimer_cancel(&ha_mon->hrtimer); +} #else /* HA_TIMER_NONE */ /* * Start function is intentionally not defined, monitors using timers must @@ -473,6 +532,7 @@ static inline bool ha_cancel_timer(struct ha_monitor *ha_mon) { return false; } +static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon) { } #endif #endif diff --git a/kernel/trace/rv/monitors/nomiss/nomiss.c b/kernel/trace/rv/monitors/nomiss/nomiss.c index 31f90f3638d8..8ead8783c29f 100644 --- a/kernel/trace/rv/monitors/nomiss/nomiss.c +++ b/kernel/trace/rv/monitors/nomiss/nomiss.c @@ -227,7 +227,7 @@ static int enable_nomiss(void) { int retval; - retval = da_monitor_init(); + retval = ha_monitor_init(); if (retval) return retval; @@ -263,7 +263,7 @@ static void disable_nomiss(void) rv_detach_trace_probe("nomiss", sched_switch, handle_sched_switch); rv_detach_trace_probe("nomiss", sched_wakeup, handle_sched_wakeup); - da_monitor_destroy(); + ha_monitor_destroy(); } static struct rv_monitor rv_this = { diff --git a/kernel/trace/rv/monitors/opid/opid.c b/kernel/trace/rv/monitors/opid/opid.c index 4594c7c46601..2922318c6112 100644 --- a/kernel/trace/rv/monitors/opid/opid.c +++ b/kernel/trace/rv/monitors/opid/opid.c @@ -73,7 +73,7 @@ static int enable_opid(void) { int retval; - retval = da_monitor_init(); + retval = ha_monitor_init(); if (retval) return retval; @@ -90,7 +90,7 @@ static void disable_opid(void) rv_detach_trace_probe("opid", sched_set_need_resched_tp, handle_sched_need_resched); rv_detach_trace_probe("opid", sched_waking, handle_sched_waking); - da_monitor_destroy(); + ha_monitor_destroy(); } /* diff --git a/kernel/trace/rv/monitors/stall/stall.c b/kernel/trace/rv/monitors/stall/stall.c index 9ccfda6b0e73..3c38fb1a0159 100644 --- a/kernel/trace/rv/monitors/stall/stall.c +++ b/kernel/trace/rv/monitors/stall/stall.c @@ -103,7 +103,7 @@ static int enable_stall(void) { int retval; - retval = da_monitor_init(); + retval = ha_monitor_init(); if (retval) return retval; @@ -120,7 +120,7 @@ static void disable_stall(void) rv_detach_trace_probe("stall", sched_switch, handle_sched_switch); rv_detach_trace_probe("stall", sched_wakeup, handle_sched_wakeup); - da_monitor_destroy(); + ha_monitor_destroy(); } static struct rv_monitor rv_this = { diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/main.c b/tools/verification/rvgen/rvgen/templates/dot2k/main.c index bf0999f6657a..889446760e3c 100644 --- a/tools/verification/rvgen/rvgen/templates/dot2k/main.c +++ b/tools/verification/rvgen/rvgen/templates/dot2k/main.c @@ -35,7 +35,7 @@ static int enable_%%MODEL_NAME%%(void) { int retval; - retval = da_monitor_init(); + retval = %%MONITOR_CLASS%%_monitor_init(); if (retval) return retval; @@ -50,7 +50,7 @@ static void disable_%%MODEL_NAME%%(void) %%TRACEPOINT_DETACH%% - da_monitor_destroy(); + %%MONITOR_CLASS%%_monitor_destroy(); } /* From 74e17bd6fc8ed7e30363bb78d4c50b38cfd71efe Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 1 Jun 2026 17:38:35 +0200 Subject: [PATCH 08/17] rv: Ensure synchronous cleanup for HA monitors HA monitors may start timers, all cleanup functions currently stop the timers asynchronously to avoid sleeping in the wrong context. Nothing makes sure running callbacks terminate on cleanup. Run the entire HA timer callback in an RCU read-side critical section, this way we can simply synchronize_rcu() with any pending timer and are sure any cleanup using kfree_rcu() runs after callbacks terminated. Additionally make sure any unlikely callback running late won't run any code if the monitor is marked as disabled or if destruction started. Use memory barriers to serialise with racing resets. Fixes: f5587d1b6ec9 ("rv: Add Hybrid Automata monitor type") Fixes: 4a24127bd6cb ("rv: Add support for per-object monitors in DA/HA") Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-9-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- include/rv/da_monitor.h | 19 ++++++++++++++++--- include/rv/ha_monitor.h | 27 +++++++++++++++++++++++++-- 2 files changed, 41 insertions(+), 5 deletions(-) diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h index ec9bc88bd4c4..1f440c7818e6 100644 --- a/include/rv/da_monitor.h +++ b/include/rv/da_monitor.h @@ -57,6 +57,15 @@ static struct rv_monitor rv_this; #define da_monitor_reset_hook(da_mon) #endif +/* + * Hook to allow the implementation of hybrid automata: define it with a + * function that waits for the termination of all monitors background + * activities (e.g. all timers). This hook can sleep. + */ +#ifndef da_monitor_sync_hook +#define da_monitor_sync_hook() +#endif + /* * Type for the target id, default to int but can be overridden. * A long type can work as hash table key (PER_OBJ) but will be downgraded to @@ -82,7 +91,8 @@ static void react(enum states curr_state, enum events event) static inline void da_monitor_reset_state(struct da_monitor *da_mon) { WRITE_ONCE(da_mon->monitoring, 0); - da_mon->curr_state = model_get_initial_state(); + /* Pair with load in __ha_monitor_timer_callback */ + smp_store_release(&da_mon->curr_state, model_get_initial_state()); } /* @@ -205,6 +215,7 @@ static inline int da_monitor_init(void) static inline void da_monitor_destroy(void) { da_monitor_reset_all(); + da_monitor_sync_hook(); } #elif RV_MON_TYPE == RV_MON_PER_CPU @@ -270,6 +281,7 @@ static inline int da_monitor_init(void) static inline void da_monitor_destroy(void) { da_monitor_reset_all(); + da_monitor_sync_hook(); } #elif RV_MON_TYPE == RV_MON_PER_TASK @@ -367,6 +379,7 @@ static inline void da_monitor_destroy(void) tracepoint_synchronize_unregister(); da_monitor_reset_all(); + da_monitor_sync_hook(); rv_put_task_monitor_slot(task_mon_slot); task_mon_slot = RV_PER_TASK_MONITOR_INIT; @@ -573,13 +586,13 @@ static inline void da_monitor_destroy(void) int bkt; tracepoint_synchronize_unregister(); + da_monitor_reset_all(); + da_monitor_sync_hook(); /* * This function is called after all probes are disabled and no longer * pending, we can safely assume no concurrent user. */ - synchronize_rcu(); hash_for_each_safe(da_monitor_ht, bkt, tmp, mon_storage, node) { - da_monitor_reset_hook(&mon_storage->rv.da_mon); hash_del_rcu(&mon_storage->node); kfree(mon_storage); } diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h index 4002b5247c46..28d3c74cabfc 100644 --- a/include/rv/ha_monitor.h +++ b/include/rv/ha_monitor.h @@ -37,6 +37,7 @@ static bool ha_monitor_handle_constraint(struct da_monitor *da_mon, #define da_monitor_event_hook ha_monitor_handle_constraint #define da_monitor_init_hook ha_monitor_init_env #define da_monitor_reset_hook ha_monitor_reset_env +#define da_monitor_sync_hook() synchronize_rcu() #if !defined(HA_SKIP_AUTO_CLEANUP) && RV_MON_TYPE == RV_MON_PER_TASK /* @@ -136,10 +137,13 @@ static enum hrtimer_restart ha_monitor_timer_callback(struct hrtimer *hrtimer); #define ha_get_ns() 0 #endif /* HA_CLK_NS */ +static bool ha_mon_destroying; + static int ha_monitor_init(void) { int ret; + WRITE_ONCE(ha_mon_destroying, false); ret = da_monitor_init(); if (ret == 0) ha_monitor_enable_hook(); @@ -148,6 +152,7 @@ static int ha_monitor_init(void) static void ha_monitor_destroy(void) { + WRITE_ONCE(ha_mon_destroying, true); ha_monitor_disable_hook(); da_monitor_destroy(); } @@ -288,12 +293,30 @@ static bool ha_monitor_handle_constraint(struct da_monitor *da_mon, return false; } +/* + * __ha_monitor_timer_callback - generic callback representation + * + * This callback runs in an RCU read-side critical section to allow the + * destruction sequence to easily synchronize_rcu() with all pending timers + * after asynchronously disabling them. The ha_mon_destroying check ensures + * any callback entering the RCU section after synchronize_rcu() completes + * will see the flag and bail out immediately. + */ static inline void __ha_monitor_timer_callback(struct ha_monitor *ha_mon) { - enum states curr_state = READ_ONCE(ha_mon->da_mon.curr_state); DECLARE_SEQ_BUF(env_string, ENV_BUFFER_SIZE); - u64 time_ns = ha_get_ns(); + enum states curr_state; + u64 time_ns; + guard(rcu)(); + if (unlikely(READ_ONCE(ha_mon_destroying))) + return; + /* Ensure consistent curr_state if we race with da_monitor_reset */ + curr_state = smp_load_acquire(&ha_mon->da_mon.curr_state); + if (unlikely(!da_monitor_handling_event(&ha_mon->da_mon))) + return; + + time_ns = ha_get_ns(); ha_get_env_string(&env_string, ha_mon, time_ns); ha_react(curr_state, EVENT_NONE, env_string.buffer); ha_trace_error_env(ha_mon, model_get_state_name(curr_state), From 7c147fae71f3b3542ba3292d2099ef7237cfc0da Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 1 Jun 2026 17:38:36 +0200 Subject: [PATCH 09/17] rv: Prevent task migration while handling per-CPU events Tracepoint handlers are fully preemptible after a46023d5616 ("tracing: Guard __DECLARE_TRACE() use of __DO_TRACE_CALL() with SRCU-fast"). When a per-CPU monitor handles an event, it retrieves the monitor state using a per-CPU pointer. If the event itself doesn't disable preemption, the task can migrate to a different CPU and we risk updating the wrong monitor. Mitigate this by explicitly disabling task migration before acquiring the monitor pointer. This cannot guarantee the monitor runs on the correct CPU but reduces the race condition window and prevents warnings. Reviewed-by: Wen Yang Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-10-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- include/rv/da_monitor.h | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h index 1f440c7818e6..34b8fba9ecd4 100644 --- a/include/rv/da_monitor.h +++ b/include/rv/da_monitor.h @@ -218,6 +218,10 @@ static inline void da_monitor_destroy(void) da_monitor_sync_hook(); } +#ifndef da_implicit_guard +#define da_implicit_guard() +#endif + #elif RV_MON_TYPE == RV_MON_PER_CPU /* * Functions to define, init and get a per-cpu monitor. @@ -284,6 +288,10 @@ static inline void da_monitor_destroy(void) da_monitor_sync_hook(); } +#ifndef da_implicit_guard +#define da_implicit_guard() guard(migrate)() +#endif + #elif RV_MON_TYPE == RV_MON_PER_TASK /* * Functions to define, init and get a per-task monitor. @@ -756,6 +764,7 @@ static inline bool __da_handle_start_run_event(struct da_monitor *da_mon, */ static inline void da_handle_event(enum events event) { + da_implicit_guard(); __da_handle_event(da_get_monitor(), event, 0); } @@ -771,6 +780,7 @@ static inline void da_handle_event(enum events event) */ static inline bool da_handle_start_event(enum events event) { + da_implicit_guard(); return __da_handle_start_event(da_get_monitor(), event, 0); } @@ -782,6 +792,7 @@ static inline bool da_handle_start_event(enum events event) */ static inline bool da_handle_start_run_event(enum events event) { + da_implicit_guard(); return __da_handle_start_run_event(da_get_monitor(), event, 0); } From d9022172c1abea9e220d13ee453813dafec5b9e4 Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 1 Jun 2026 17:38:37 +0200 Subject: [PATCH 10/17] rv: Use 0 to check preemption enabled in opid Tracepoint handlers no longer run with preemption disabled by default since a46023d5616 ("tracing: Guard __DECLARE_TRACE() use of __DO_TRACE_CALL() with SRCU-fast"), the opid monitor should now count 1 in the preemption count as preemption disabled. Change the rule for preempt_off to preempt > 0. Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-11-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- kernel/trace/rv/monitors/opid/opid.c | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/kernel/trace/rv/monitors/opid/opid.c b/kernel/trace/rv/monitors/opid/opid.c index 2922318c6112..3b6a85e815b8 100644 --- a/kernel/trace/rv/monitors/opid/opid.c +++ b/kernel/trace/rv/monitors/opid/opid.c @@ -22,14 +22,8 @@ static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_opid env, u64 time_ns if (env == irq_off_opid) return irqs_disabled(); else if (env == preempt_off_opid) { - /* - * If CONFIG_PREEMPTION is enabled, then the tracepoint itself disables - * preemption (adding one to the preempt_count). Since we are - * interested in the preempt_count at the time the tracepoint was - * hit, we consider 1 as still enabled. - */ if (IS_ENABLED(CONFIG_PREEMPTION)) - return (preempt_count() & PREEMPT_MASK) > 1; + return (preempt_count() & PREEMPT_MASK) > 0; return true; } return ENV_INVALID_VALUE; From 08904765bb941f98306ae6841c33cfd299343faf Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Thu, 4 Jun 2026 14:09:45 +0200 Subject: [PATCH 11/17] tools/rv: Ensure monitor name and desc are NUL-terminated ikm_fill_monitor_definition() copies monitor name and description with strncpy(), but does not guarantee NUL termination when source strings are equal to or longer than the destination buffers. Clamp copies to sizeof(dst) - 1 and explicitly append '\0' for both fields to keep them safe for later string operations. Suggested-by: unknownbbqrx Fixes: 6d60f89691fc9 ("tools/rv: Add in-kernel monitor interface") Link: https://lore.kernel.org/r/20260604120946.90302-2-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- tools/verification/rv/src/in_kernel.c | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/tools/verification/rv/src/in_kernel.c b/tools/verification/rv/src/in_kernel.c index 4bb746ea6e17..d324538249d3 100644 --- a/tools/verification/rv/src/in_kernel.c +++ b/tools/verification/rv/src/in_kernel.c @@ -215,10 +215,11 @@ static int ikm_fill_monitor_definition(char *name, struct monitor *ikm, char *co return -1; } - strncpy(ikm->name, nested_name, MAX_DA_NAME_LEN); + strncpy(ikm->name, nested_name, sizeof(ikm->name) - 1); + ikm->name[sizeof(ikm->name) - 1] = '\0'; ikm->enabled = enabled; - strncpy(ikm->desc, desc, MAX_DESCRIPTION); - + strncpy(ikm->desc, desc, sizeof(ikm->desc) - 1); + ikm->desc[sizeof(ikm->desc) - 1] = '\0'; free(desc); return 0; From a963fbf3166f2e178ac38b6c3c186a0c98092fb9 Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Thu, 14 May 2026 17:20:42 +0200 Subject: [PATCH 12/17] tools/rv: Fix substring match bug in monitor name search __ikm_find_monitor_name() relies on strstr() to find a monitor by name, which fails if the target monitor is a substring of a previously listed monitor. Fix it by tokenizing the available_monitors file and matching full tokens instead. Fixes: eba321a16fc6 ("tools/rv: Add support for nested monitors") Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260514152055.229162-2-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- tools/verification/rv/src/in_kernel.c | 50 ++++++++++++++------------- 1 file changed, 26 insertions(+), 24 deletions(-) diff --git a/tools/verification/rv/src/in_kernel.c b/tools/verification/rv/src/in_kernel.c index d324538249d3..95eac9ab1484 100644 --- a/tools/verification/rv/src/in_kernel.c +++ b/tools/verification/rv/src/in_kernel.c @@ -58,38 +58,40 @@ static int __ikm_read_enable(char *monitor_name) */ static int __ikm_find_monitor_name(char *monitor_name, char *out_name) { - char *available_monitors, container[MAX_DA_NAME_LEN+1], *cursor, *end; - int retval = 1; + char *available_monitors, *cursor, *line; + int len = strlen(monitor_name); + int found = 0; available_monitors = tracefs_instance_file_read(NULL, "rv/available_monitors", NULL); if (!available_monitors) return -1; - cursor = strstr(available_monitors, monitor_name); - if (!cursor) { - retval = 0; - goto out_free; + config_is_container = 0; + cursor = available_monitors; + while ((line = strsep(&cursor, "\n"))) { + char *colon = strchr(line, ':'); + + if (strcmp(line, monitor_name) && (!colon || strcmp(colon + 1, monitor_name))) + continue; + + strncpy(out_name, line, 2 * MAX_DA_NAME_LEN); + out_name[2 * MAX_DA_NAME_LEN - 1] = '\0'; + + if (colon) { + out_name[colon - line] = '/'; + } else { + /* If there are children, they are on the next line. */ + line = strsep(&cursor, "\n"); + if (line && !strncmp(line, monitor_name, len) && line[len] == ':') + config_is_container = 1; + } + + found = 1; + break; } - for (; cursor > available_monitors; cursor--) - if (*(cursor-1) == '\n') - break; - end = strstr(cursor, "\n"); - memcpy(out_name, cursor, end-cursor); - out_name[end-cursor] = '\0'; - - cursor = strstr(out_name, ":"); - if (cursor) - *cursor = '/'; - else { - sprintf(container, "%s:", monitor_name); - if (strstr(available_monitors, container)) - config_is_container = 1; - } - -out_free: free(available_monitors); - return retval; + return found; } /* From ba0247c5aa3fcb2890a92a97a88c70fe5ce704a6 Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Thu, 14 May 2026 17:20:43 +0200 Subject: [PATCH 13/17] tools/rv: Fix substring match when listing container monitors When listing monitors within a specific container (rv list ), the tool incorrectly matched monitors if the requested container name was only a prefix of the actual container (e.g., 'rv list sche' would incorrectly list monitors from 'sched:'). Fix this by ensuring the container name is an exact match and is immediately followed by the ':' separator. Fixes: eba321a16fc6 ("tools/rv: Add support for nested monitors") Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260514152055.229162-3-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- tools/verification/rv/src/in_kernel.c | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/tools/verification/rv/src/in_kernel.c b/tools/verification/rv/src/in_kernel.c index 95eac9ab1484..e4f35940374f 100644 --- a/tools/verification/rv/src/in_kernel.c +++ b/tools/verification/rv/src/in_kernel.c @@ -193,8 +193,12 @@ static int ikm_fill_monitor_definition(char *name, struct monitor *ikm, char *co nested_name = strstr(name, ":"); if (nested_name) { /* it belongs in container if it starts with "container:" */ - if (container && strstr(name, container) != name) - return 1; + if (container) { + int len = strlen(container); + + if (strncmp(name, container, len) || name[len] != ':') + return 1; + } *nested_name = '/'; ++nested_name; ikm->nested = 1; From 33ec2269a4155cad7e9e42c92327dcaa9aee59a7 Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Thu, 14 May 2026 17:20:45 +0200 Subject: [PATCH 14/17] tools/rv: Fix cleanup after failed trace setup Currently if ikm_setup_trace_instance() fails, the tool returns without any cleanup, if rv was called with both -t and -r, this means the reactor is not going to be cleared. Jump to the cleanup label to restore the reactor if necessary. Fixes: 6d60f89691fc9 ("tools/rv: Add in-kernel monitor interface") Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260514152055.229162-5-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- tools/verification/rv/src/in_kernel.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/verification/rv/src/in_kernel.c b/tools/verification/rv/src/in_kernel.c index e4f35940374f..e6dea4040f8f 100644 --- a/tools/verification/rv/src/in_kernel.c +++ b/tools/verification/rv/src/in_kernel.c @@ -810,7 +810,7 @@ int ikm_run_monitor(char *monitor_name, int argc, char **argv) if (config_trace) { inst = ikm_setup_trace_instance(nested_name); if (!inst) - return -1; + goto out_free_instance; } retval = ikm_enable(full_name); From 85339442de941e4d7ff5d53f51ae1413905e45ec Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 1 Jun 2026 17:38:38 +0200 Subject: [PATCH 15/17] verification/rvgen: Fix suffix strip in dot2k __start_to_invariant_check() and __get_constraint_env() parse the environment variable's name from sources that have it padded with the monitor name. This is removed using rstrip(), which is not meant to strip a substring but rather a set of characters. Use removesuffix() to actually get rid of the trailing _. Fixes: a82adadb16894 ("verification/rvgen: Add support for Hybrid Automata") Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-12-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/dot2k.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py index e6f476b903b0..110cfd69e53a 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -215,14 +215,14 @@ class ha2k(dot2k): 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.rstrip(f"_{self.name}") in self.envs + assert env.removesuffix(f"_{self.name}") in self.envs return env def __start_to_invariant_check(self, constr: str) -> str: # by default assume the timer has ns expiration env = self.__get_constraint_env(constr) clock_type = "ns" - if self.env_types.get(env.rstrip(f"_{self.name}")) == "j": + if self.env_types.get(env.removesuffix(f"_{self.name}")) == "j": clock_type = "jiffy" return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)" From 5f845ad706c0b394ae274e9a930044f78bef782e Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Thu, 14 May 2026 17:20:47 +0200 Subject: [PATCH 16/17] verification/rvgen: Fix options shared among commands After rvgen was refactored to use subparsers, the common options (-a and -D) were left in the main parser. This meant that they needed to be called /before/ the subcommand and using them without subcommand was allowed. This is not the original intent. rvgen -D "some description" container -n name Define the options as parent in the subparsers to allow them to be used from both subcommands together with other options. rvgen container -n name -D "some description" Fixes: 5270a0e3041c ("verification/dot2k: Replace is_container() hack with subparsers") Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260514152055.229162-7-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- tools/verification/rvgen/__main__.py | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py index 3be7f85fe37b..5c923dc10d0f 100644 --- a/tools/verification/rvgen/__main__.py +++ b/tools/verification/rvgen/__main__.py @@ -18,14 +18,16 @@ if __name__ == '__main__': import sys parser = argparse.ArgumentParser(description='Generate kernel rv monitor') - parser.add_argument("-D", "--description", dest="description", required=False) - parser.add_argument("-a", "--auto_patch", dest="auto_patch", + + parent_parser = argparse.ArgumentParser(add_help=False) + parent_parser.add_argument("-D", "--description", dest="description", required=False) + parent_parser.add_argument("-a", "--auto_patch", dest="auto_patch", action="store_true", required=False, help="Patch the kernel in place") subparsers = parser.add_subparsers(dest="subcmd", required=True) - monitor_parser = subparsers.add_parser("monitor") + monitor_parser = subparsers.add_parser("monitor", parents=[parent_parser]) monitor_parser.add_argument('-n', "--model_name", dest="model_name") monitor_parser.add_argument("-p", "--parent", dest="parent", required=False, help="Create a monitor nested to parent") @@ -36,7 +38,7 @@ if __name__ == '__main__': monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True, help=f"Available options: {', '.join(Monitor.monitor_types.keys())}") - container_parser = subparsers.add_parser("container") + container_parser = subparsers.add_parser("container", parents=[parent_parser]) container_parser.add_argument('-n', "--model_name", dest="model_name", required=True) params = parser.parse_args() From df996599cc69a9b74ff437c67751cf8a61f62e39 Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Thu, 14 May 2026 17:20:48 +0200 Subject: [PATCH 17/17] verification/rvgen: Fix ltl2k writing True as a literal The rvgen parser for LTL stores literal true values in the python representation (capitalised True), this doesn't build in C. The Literal class should already handle this case but ASTNode skips its strigification method and converts the value (true/false) directly. Fix by delegating ASTNode stringification to the Literal and Variable classes instead of bypassing them. Fixes: 97ffa4ce6ab32 ("verification/rvgen: Add support for linear temporal logic") Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260514152055.229162-8-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/ltl2ba.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py index 7f538598a868..016e7cf93bbb 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -122,10 +122,8 @@ class ASTNode: return self.op.expand(self, node, node_set) def __str__(self): - if isinstance(self.op, Literal): - return str(self.op.value) - if isinstance(self.op, Variable): - return self.op.name.lower() + if isinstance(self.op, (Literal, Variable)): + return str(self.op) return "val" + str(self.id) def normalize(self): @@ -382,6 +380,9 @@ class Variable: def __iter__(self): yield from () + def __str__(self): + return self.name.lower() + def negate(self): new = ASTNode(self) return NotOp(new)