From ff4e233d8ab70fe6ae460ecc8c0e5b24dd0fedb0 Mon Sep 17 00:00:00 2001 From: Nam Cao Date: Wed, 9 Jul 2025 21:21:15 +0200 Subject: rv: Let the reactors take care of buffers Each RV monitor has one static buffer to send to the reactors. If multiple errors are detected simultaneously, the one buffer could be overwritten. Instead, leave it to the reactors to handle buffering. Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/linux/rv.h | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'include/linux/rv.h') diff --git a/include/linux/rv.h b/include/linux/rv.h index 3452b5e4b29e..9428e62eb8e9 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -38,7 +38,7 @@ union rv_task_monitor { struct rv_reactor { const char *name; const char *description; - void (*react)(char *msg); + __printf(1, 2) void (*react)(const char *msg, ...); }; #endif @@ -50,7 +50,7 @@ struct rv_monitor { void (*disable)(void); void (*reset)(void); #ifdef CONFIG_RV_REACTORS - void (*react)(char *msg); + __printf(1, 2) void (*react)(const char *msg, ...); #endif }; @@ -64,6 +64,11 @@ void rv_put_task_monitor_slot(int slot); bool rv_reacting_on(void); int rv_unregister_reactor(struct rv_reactor *reactor); int rv_register_reactor(struct rv_reactor *reactor); +#else +static inline bool rv_reacting_on(void) +{ + return false; +} #endif /* CONFIG_RV_REACTORS */ #endif /* CONFIG_RV */ -- cgit v1.2.3 From a9769a5b987838f03f3dd57b097794cd4c691098 Mon Sep 17 00:00:00 2001 From: Nam Cao Date: Wed, 9 Jul 2025 21:21:17 +0200 Subject: rv: Add support for LTL monitors While attempting to implement DA monitors for some complex specifications, deterministic automaton is found to be inappropriate as the specification language. The automaton is complicated, hard to understand, and error-prone. For these cases, linear temporal logic is more suitable as the specification language. Add support for linear temporal logic runtime verification monitor. Cc: John Ogness Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Cc: Gabriele Monaco Link: https://lore.kernel.org/d366c1fed60ed4e8f6451f3c15a99755f2740b5f.1752088709.git.namcao@linutronix.de Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/linux/rv.h | 63 ++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 59 insertions(+), 4 deletions(-) (limited to 'include/linux/rv.h') diff --git a/include/linux/rv.h b/include/linux/rv.h index 9428e62eb8e9..1d5579f9b75a 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -10,6 +10,10 @@ #define MAX_DA_NAME_LEN 32 #ifdef CONFIG_RV +#include +#include +#include + /* * Deterministic automaton per-object variables. */ @@ -18,6 +22,59 @@ struct da_monitor { unsigned int curr_state; }; +#ifdef CONFIG_RV_LTL_MONITOR + +/* + * In the future, if the number of atomic propositions or the size of Buchi + * automaton is larger, we can switch to dynamic allocation. For now, the code + * is simpler this way. + */ +#define RV_MAX_LTL_ATOM 32 +#define RV_MAX_BA_STATES 32 + +/** + * struct ltl_monitor - A linear temporal logic runtime verification monitor + * @states: States in the Buchi automaton. As Buchi automaton is a + * non-deterministic state machine, the monitor can be in multiple + * states simultaneously. This is a bitmask of all possible states. + * If this is zero, that means either: + * - The monitor has not started yet (e.g. because not all + * atomic propositions are known). + * - There is no possible state to be in. In other words, a + * violation of the LTL property is detected. + * @atoms: The values of atomic propositions. + * @unknown_atoms: Atomic propositions which are still unknown. + */ +struct ltl_monitor { + DECLARE_BITMAP(states, RV_MAX_BA_STATES); + DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM); + DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM); +}; + +static inline bool rv_ltl_valid_state(struct ltl_monitor *mon) +{ + for (int i = 0; i < ARRAY_SIZE(mon->states); ++i) { + if (mon->states[i]) + return true; + } + return false; +} + +static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon) +{ + for (int i = 0; i < ARRAY_SIZE(mon->unknown_atoms); ++i) { + if (mon->unknown_atoms[i]) + return false; + } + return true; +} + +#else + +struct ltl_monitor {}; + +#endif /* CONFIG_RV_LTL_MONITOR */ + /* * Per-task RV monitors count. Nowadays fixed in RV_PER_TASK_MONITORS. * If we find justification for more monitors, we can think about @@ -27,11 +84,9 @@ struct da_monitor { #define RV_PER_TASK_MONITORS 1 #define RV_PER_TASK_MONITOR_INIT (RV_PER_TASK_MONITORS) -/* - * Futher monitor types are expected, so make this a union. - */ union rv_task_monitor { - struct da_monitor da_mon; + struct da_monitor da_mon; + struct ltl_monitor ltl_mon; }; #ifdef CONFIG_RV_REACTORS -- cgit v1.2.3 From fac5493251a680cb74343895d0e76843624a90d8 Mon Sep 17 00:00:00 2001 From: Nam Cao Date: Wed, 9 Jul 2025 21:21:23 +0200 Subject: rv: Allow to configure the number of per-task monitor Now that there are 2 monitors for real-time applications, users may want to enable both of them simultaneously. Make the number of per-task monitor configurable. Default it to 2 for now. Cc: John Ogness Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/93e83313fc4ba7f6e66f4abe80ca5f5494d658d0.1752088709.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/linux/rv.h | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) (limited to 'include/linux/rv.h') diff --git a/include/linux/rv.h b/include/linux/rv.h index 1d5579f9b75a..97baf58d88b2 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -75,14 +75,7 @@ struct ltl_monitor {}; #endif /* CONFIG_RV_LTL_MONITOR */ -/* - * Per-task RV monitors count. Nowadays fixed in RV_PER_TASK_MONITORS. - * If we find justification for more monitors, we can think about - * adding more or developing a dynamic method. So far, none of - * these are justified. - */ -#define RV_PER_TASK_MONITORS 1 -#define RV_PER_TASK_MONITOR_INIT (RV_PER_TASK_MONITORS) +#define RV_PER_TASK_MONITOR_INIT (CONFIG_RV_PER_TASK_MONITORS) union rv_task_monitor { struct da_monitor da_mon; -- cgit v1.2.3 From 24cbfe18d55a6866bc2e27fda74306f4a1b5cb01 Mon Sep 17 00:00:00 2001 From: Nam Cao Date: Thu, 24 Jul 2025 19:33:27 +0200 Subject: rv: Merge struct rv_monitor_def into struct rv_monitor Each struct rv_monitor has a unique struct rv_monitor_def associated with it. struct rv_monitor is statically allocated, while struct rv_monitor_def is dynamically allocated. This makes the code more complicated than it should be: - Lookup is required to get the associated rv_monitor_def from rv_monitor - Dynamic memory allocation is required for rv_monitor_def. This is harder to get right compared to static memory. For instance, there is an existing mistake: rv_unregister_monitor() does not free the memory allocated by rv_register_monitor(). This is fortunately not a real memory leak problem, as rv_unregister_monitor() is never called. Simplify and merge rv_monitor_def into rv_monitor. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/194449c00f87945c207aab4c96920c75796a4f53.1753378331.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/linux/rv.h | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'include/linux/rv.h') diff --git a/include/linux/rv.h b/include/linux/rv.h index 97baf58d88b2..dba53aecdfab 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -7,6 +7,9 @@ #ifndef _LINUX_RV_H #define _LINUX_RV_H +#include +#include + #define MAX_DA_NAME_LEN 32 #ifdef CONFIG_RV @@ -98,8 +101,13 @@ struct rv_monitor { void (*disable)(void); void (*reset)(void); #ifdef CONFIG_RV_REACTORS + struct rv_reactor_def *rdef; __printf(1, 2) void (*react)(const char *msg, ...); + bool reacting; #endif + struct list_head list; + struct rv_monitor *parent; + struct dentry *root_d; }; bool rv_monitoring_on(void); -- cgit v1.2.3 From 3d3c376118b5f7ed7723c2b4fd7a0a1c1893d63e Mon Sep 17 00:00:00 2001 From: Nam Cao Date: Thu, 24 Jul 2025 19:33:28 +0200 Subject: rv: Merge struct rv_reactor_def into struct rv_reactor Each struct rv_reactor has a unique struct rv_reactor_def associated with it. struct rv_reactor is statically allocated, while struct rv_reactor_def is dynamically allocated. This makes the code more complicated than it should be: - Lookup is required to get the associated rv_reactor_def from rv_reactor - Dynamic memory allocation is required for rv_reactor_def. This is harder to get right compared to static memory. For instance, there is an existing mistake: rv_unregister_reactor() does not free the memory allocated by rv_register_reactor(). This is fortunately not a real memory leak problem as rv_unregister_reactor() is never called. Simplify and merge rv_reactor_def into rv_reactor. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/71cb91c86cd40df5b8c492b788787f2a73c3eaa3.1753378331.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/linux/rv.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'include/linux/rv.h') diff --git a/include/linux/rv.h b/include/linux/rv.h index dba53aecdfab..c22c9b8c1567 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -90,6 +90,9 @@ struct rv_reactor { const char *name; const char *description; __printf(1, 2) void (*react)(const char *msg, ...); + struct list_head list; + /* protected by the monitor interface lock */ + int counter; }; #endif @@ -101,7 +104,7 @@ struct rv_monitor { void (*disable)(void); void (*reset)(void); #ifdef CONFIG_RV_REACTORS - struct rv_reactor_def *rdef; + struct rv_reactor *reactor; __printf(1, 2) void (*react)(const char *msg, ...); bool reacting; #endif -- cgit v1.2.3 From 3d3800b4f7f4b1472a0ec2cffd535c05603f8f60 Mon Sep 17 00:00:00 2001 From: Nam Cao Date: Thu, 24 Jul 2025 19:33:29 +0200 Subject: rv: Remove rv_reactor's reference counter rv_reactor has a reference counter to ensure it is not removed while monitors are still using it. However, this is futile, as __exit functions are not expected to fail and will proceed normally despite rv_unregister_reactor() returning an error. At the moment, reactors do not support being built as modules, therefore they are never removed and the reference counters are not necessary. If we support building RV reactors as modules in the future, kernel module's centralized facilities such as try_module_get(), module_put() or MODULE_SOFTDEP should be used instead of this custom implementation. Remove this reference counter. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/bb946398436a5e17fb0f5b842ef3313c02291852.1753378331.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/linux/rv.h | 2 -- 1 file changed, 2 deletions(-) (limited to 'include/linux/rv.h') diff --git a/include/linux/rv.h b/include/linux/rv.h index c22c9b8c1567..2f867d6f72ba 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -91,8 +91,6 @@ struct rv_reactor { const char *description; __printf(1, 2) void (*react)(const char *msg, ...); struct list_head list; - /* protected by the monitor interface lock */ - int counter; }; #endif -- cgit v1.2.3 From b8a7fba39cd49eab343bfe561d85bb5dc57541af Mon Sep 17 00:00:00 2001 From: Nam Cao Date: Thu, 24 Jul 2025 19:33:30 +0200 Subject: rv: Remove struct rv_monitor::reacting The field 'reacting' in struct rv_monitor is set but never used. Delete it. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/a6c16f845d2f1a09c4d0934ab83f3cb14478a71d.1753378331.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/linux/rv.h | 1 - 1 file changed, 1 deletion(-) (limited to 'include/linux/rv.h') diff --git a/include/linux/rv.h b/include/linux/rv.h index 2f867d6f72ba..80731242fe60 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -104,7 +104,6 @@ struct rv_monitor { #ifdef CONFIG_RV_REACTORS struct rv_reactor *reactor; __printf(1, 2) void (*react)(const char *msg, ...); - bool reacting; #endif struct list_head list; struct rv_monitor *parent; -- cgit v1.2.3 From 9d475d80c93735f0f336b34a8e2c22beea6145ab Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 28 Jul 2025 15:50:17 +0200 Subject: rv: Retry when da monitor detects race conditions DA monitor can be accessed from multiple cores simultaneously, this is likely, for instance when dealing with per-task monitors reacting on events that do not always occur on the CPU where the task is running. This can cause race conditions where two events change the next state and we see inconsistent values. E.g.: [62] event_srs: 27: sleepable x sched_wakeup -> running (final) [63] event_srs: 27: sleepable x sched_set_state_sleepable -> sleepable [63] error_srs: 27: event sched_switch_suspend not expected in the state running In this case the monitor fails because the event on CPU 62 wins against the one on CPU 63, although the correct state should have been sleepable, since the task get suspended. Detect if the current state was modified by using try_cmpxchg while storing the next value. If it was, try again reading the current state. After a maximum number of failed retries, react by calling a special tracepoint, print on the console and reset the monitor. Remove the functions da_monitor_curr_state() and da_monitor_set_state() as they only hide the underlying implementation in this case. Monitors where this type of condition can occur must be able to account for racing events in any possible order, as we cannot know the winner. Cc: Ingo Molnar Cc: Masami Hiramatsu Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Cc: Peter Zijlstra Link: https://lore.kernel.org/20250728135022.255578-6-gmonaco@redhat.com Signed-off-by: Gabriele Monaco Reviewed-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/linux/rv.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'include/linux/rv.h') diff --git a/include/linux/rv.h b/include/linux/rv.h index 80731242fe60..14410a42faef 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -10,7 +10,8 @@ #include #include -#define MAX_DA_NAME_LEN 32 +#define MAX_DA_NAME_LEN 32 +#define MAX_DA_RETRY_RACING_EVENTS 3 #ifdef CONFIG_RV #include -- cgit v1.2.3