* [PATCH 01/10] rv: Add #undef TRACE_INCLUDE_FILE
2025-03-11 17:05 [PATCH 00/10] RV: Linear temporal logic monitors for RT application Nam Cao
@ 2025-03-11 17:05 ` Nam Cao
2025-03-11 17:05 ` [PATCH 02/10] rv: Let the reactors take care of buffers Nam Cao
` (8 subsequent siblings)
9 siblings, 0 replies; 23+ messages in thread
From: Nam Cao @ 2025-03-11 17:05 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, john.ogness, linux-trace-kernel,
linux-kernel
Cc: Nam Cao
Without "#undef TRACE_INCLUDE_FILE", there could be a build error due to
TRACE_INCLUDE_FILE being redefined. Therefore add it.
Also fix a typo while at it.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
kernel/trace/rv/rv_trace.h | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index 5e65097423ba..96264233cac5 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -123,8 +123,9 @@ DECLARE_EVENT_CLASS(error_da_monitor_id,
#endif /* CONFIG_DA_MON_EVENTS_ID */
#endif /* _TRACE_RV_H */
-/* This part ust be outside protection */
+/* This part must be outside protection */
#undef TRACE_INCLUDE_PATH
#define TRACE_INCLUDE_PATH .
+#undef TRACE_INCLUDE_FILE
#define TRACE_INCLUDE_FILE rv_trace
#include <trace/define_trace.h>
--
2.39.5
^ permalink raw reply related [flat|nested] 23+ messages in thread* [PATCH 02/10] rv: Let the reactors take care of buffers
2025-03-11 17:05 [PATCH 00/10] RV: Linear temporal logic monitors for RT application Nam Cao
2025-03-11 17:05 ` [PATCH 01/10] rv: Add #undef TRACE_INCLUDE_FILE Nam Cao
@ 2025-03-11 17:05 ` Nam Cao
2025-03-12 7:58 ` Gabriele Monaco
` (2 more replies)
2025-03-11 17:05 ` [PATCH 03/10] rv: Add infrastructure for linear temporal logic monitor Nam Cao
` (7 subsequent siblings)
9 siblings, 3 replies; 23+ messages in thread
From: Nam Cao @ 2025-03-11 17:05 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, john.ogness, linux-trace-kernel,
linux-kernel
Cc: Nam Cao, Petr Mladek, Sergey Senozhatsky
Each RV monitor has one static buffer to send to the reactors. If multiple
errors are detected at the same time, the one buffer could be overwritten.
Instead, leave it to the reactors to handle buffering.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Petr Mladek <pmladek@suse.com>
Cc: John Ogness <john.ogness@linutronix.de>
Cc: Sergey Senozhatsky <senozhatsky@chromium.org>
---
include/linux/printk.h | 1 +
include/linux/rv.h | 11 +++---
include/rv/da_monitor.h | 61 ++++++--------------------------
kernel/printk/internal.h | 1 -
kernel/trace/rv/reactor_panic.c | 7 +---
kernel/trace/rv/reactor_printk.c | 8 +++--
kernel/trace/rv/rv_reactors.c | 2 +-
7 files changed, 26 insertions(+), 65 deletions(-)
diff --git a/include/linux/printk.h b/include/linux/printk.h
index 4217a9f412b2..11e49b299312 100644
--- a/include/linux/printk.h
+++ b/include/linux/printk.h
@@ -154,6 +154,7 @@ int vprintk_emit(int facility, int level,
asmlinkage __printf(1, 0)
int vprintk(const char *fmt, va_list args);
+__printf(1, 0) int vprintk_deferred(const char *fmt, va_list args);
asmlinkage __printf(1, 2) __cold
int _printk(const char *fmt, ...);
diff --git a/include/linux/rv.h b/include/linux/rv.h
index 8883b41d88ec..5482651ed020 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);
+ void (*react)(const char *msg, ...);
};
#endif
@@ -49,9 +49,7 @@ struct rv_monitor {
int (*enable)(void);
void (*disable)(void);
void (*reset)(void);
-#ifdef CONFIG_RV_REACTORS
- void (*react)(char *msg);
-#endif
+ void (*react)(const char *msg, ...);
};
bool rv_monitoring_on(void);
@@ -64,6 +62,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 */
diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
index 510c88bfabd4..c55d45544a16 100644
--- a/include/rv/da_monitor.h
+++ b/include/rv/da_monitor.h
@@ -16,58 +16,11 @@
#include <linux/bug.h>
#include <linux/sched.h>
-#ifdef CONFIG_RV_REACTORS
-
-#define DECLARE_RV_REACTING_HELPERS(name, type) \
-static char REACT_MSG_##name[1024]; \
- \
-static inline char *format_react_msg_##name(type curr_state, type event) \
-{ \
- snprintf(REACT_MSG_##name, 1024, \
- "rv: monitor %s does not allow event %s on state %s\n", \
- #name, \
- model_get_event_name_##name(event), \
- model_get_state_name_##name(curr_state)); \
- return REACT_MSG_##name; \
-} \
- \
-static void cond_react_##name(char *msg) \
-{ \
- if (rv_##name.react) \
- rv_##name.react(msg); \
-} \
- \
-static bool rv_reacting_on_##name(void) \
-{ \
- return rv_reacting_on(); \
-}
-
-#else /* CONFIG_RV_REACTOR */
-
-#define DECLARE_RV_REACTING_HELPERS(name, type) \
-static inline char *format_react_msg_##name(type curr_state, type event) \
-{ \
- return NULL; \
-} \
- \
-static void cond_react_##name(char *msg) \
-{ \
- return; \
-} \
- \
-static bool rv_reacting_on_##name(void) \
-{ \
- return 0; \
-}
-#endif
-
/*
* Generic helpers for all types of deterministic automata monitors.
*/
#define DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
\
-DECLARE_RV_REACTING_HELPERS(name, type) \
- \
/* \
* da_monitor_reset_##name - reset a monitor and setting it to init state \
*/ \
@@ -170,8 +123,11 @@ da_event_##name(struct da_monitor *da_mon, enum events_##name event) \
return true; \
} \
\
- if (rv_reacting_on_##name()) \
- cond_react_##name(format_react_msg_##name(curr_state, event)); \
+ if (rv_reacting_on() && rv_##name.react) \
+ rv_##name.react("rv: monitor %s does not allow event %s on state %s\n", \
+ #name, \
+ model_get_event_name_##name(event), \
+ model_get_state_name_##name(curr_state)); \
\
trace_error_##name(model_get_state_name_##name(curr_state), \
model_get_event_name_##name(event)); \
@@ -202,8 +158,11 @@ static inline bool da_event_##name(struct da_monitor *da_mon, struct task_struct
return true; \
} \
\
- if (rv_reacting_on_##name()) \
- cond_react_##name(format_react_msg_##name(curr_state, event)); \
+ if (rv_reacting_on() && rv_##name.react) \
+ rv_##name.react("rv: monitor %s does not allow event %s on state %s\n", \
+ #name, \
+ model_get_event_name_##name(event), \
+ model_get_state_name_##name(curr_state)); \
\
trace_error_##name(tsk->pid, \
model_get_state_name_##name(curr_state), \
diff --git a/kernel/printk/internal.h b/kernel/printk/internal.h
index a91bdf802967..28afdeb58412 100644
--- a/kernel/printk/internal.h
+++ b/kernel/printk/internal.h
@@ -71,7 +71,6 @@ int vprintk_store(int facility, int level,
const char *fmt, va_list args);
__printf(1, 0) int vprintk_default(const char *fmt, va_list args);
-__printf(1, 0) int vprintk_deferred(const char *fmt, va_list args);
void __printk_safe_enter(void);
void __printk_safe_exit(void);
diff --git a/kernel/trace/rv/reactor_panic.c b/kernel/trace/rv/reactor_panic.c
index 0186ff4cbd0b..4addabc9bcf1 100644
--- a/kernel/trace/rv/reactor_panic.c
+++ b/kernel/trace/rv/reactor_panic.c
@@ -13,15 +13,10 @@
#include <linux/init.h>
#include <linux/rv.h>
-static void rv_panic_reaction(char *msg)
-{
- panic(msg);
-}
-
static struct rv_reactor rv_panic = {
.name = "panic",
.description = "panic the system if an exception is found.",
- .react = rv_panic_reaction
+ .react = panic
};
static int __init register_react_panic(void)
diff --git a/kernel/trace/rv/reactor_printk.c b/kernel/trace/rv/reactor_printk.c
index 178759dbf89f..a15db3fc8b82 100644
--- a/kernel/trace/rv/reactor_printk.c
+++ b/kernel/trace/rv/reactor_printk.c
@@ -12,9 +12,13 @@
#include <linux/init.h>
#include <linux/rv.h>
-static void rv_printk_reaction(char *msg)
+static void rv_printk_reaction(const char *msg, ...)
{
- printk_deferred(msg);
+ va_list args;
+
+ va_start(args, msg);
+ vprintk_deferred(msg, args);
+ va_end(args);
}
static struct rv_reactor rv_printk = {
diff --git a/kernel/trace/rv/rv_reactors.c b/kernel/trace/rv/rv_reactors.c
index 7b49cbe388d4..885661fe2b6e 100644
--- a/kernel/trace/rv/rv_reactors.c
+++ b/kernel/trace/rv/rv_reactors.c
@@ -468,7 +468,7 @@ void reactor_cleanup_monitor(struct rv_monitor_def *mdef)
/*
* Nop reactor register
*/
-static void rv_nop_reaction(char *msg)
+static void rv_nop_reaction(const char *msg, ...)
{
}
--
2.39.5
^ permalink raw reply related [flat|nested] 23+ messages in thread* Re: [PATCH 02/10] rv: Let the reactors take care of buffers
2025-03-11 17:05 ` [PATCH 02/10] rv: Let the reactors take care of buffers Nam Cao
@ 2025-03-12 7:58 ` Gabriele Monaco
2025-03-13 8:16 ` Nam Cao
2025-03-13 16:07 ` kernel test robot
2025-03-13 16:07 ` kernel test robot
2 siblings, 1 reply; 23+ messages in thread
From: Gabriele Monaco @ 2025-03-12 7:58 UTC (permalink / raw)
To: Nam Cao, Steven Rostedt, john.ogness, linux-trace-kernel,
linux-kernel
Cc: Petr Mladek, Sergey Senozhatsky
On Tue, 2025-03-11 at 18:05 +0100, Nam Cao wrote:
> Each RV monitor has one static buffer to send to the reactors. If
> multiple
> errors are detected at the same time, the one buffer could be
> overwritten.
>
> Instead, leave it to the reactors to handle buffering.
>
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
> Cc: Petr Mladek <pmladek@suse.com>
> Cc: John Ogness <john.ogness@linutronix.de>
> Cc: Sergey Senozhatsky <senozhatsky@chromium.org>
> ---
> include/linux/printk.h | 1 +
> include/linux/rv.h | 11 +++---
> include/rv/da_monitor.h | 61 ++++++------------------------
> --
> kernel/printk/internal.h | 1 -
> kernel/trace/rv/reactor_panic.c | 7 +---
> kernel/trace/rv/reactor_printk.c | 8 +++--
> kernel/trace/rv/rv_reactors.c | 2 +-
> 7 files changed, 26 insertions(+), 65 deletions(-)
>
> diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
> index 510c88bfabd4..c55d45544a16 100644
> --- a/include/rv/da_monitor.h
> +++ b/include/rv/da_monitor.h
> @@ -16,58 +16,11 @@
> #include <linux/bug.h>
> #include <linux/sched.h>
>
> -#ifdef CONFIG_RV_REACTORS
> -
> -#define DECLARE_RV_REACTING_HELPERS(name,
> type) \
> -static char
> REACT_MSG_##name[1024]; \
> -
> \
> -static inline char *format_react_msg_##name(type curr_state, type
> event) \
> -
> { \
> - snprintf(REACT_MSG_##name,
> 1024, \
> - "rv: monitor %s does not allow event %s on state
> %s\n", \
> -
> #name, \
> -
> model_get_event_name_##name(event), \
> -
> model_get_state_name_##name(curr_state)); \
> - return
> REACT_MSG_##name; \
> -
> } \
> -
> \
> -static void cond_react_##name(char
> *msg) \
> -
> { \
> - if
> (rv_##name.react) \
> -
> rv_##name.react(msg); \
> -
> } \
> -
> \
> -static bool
> rv_reacting_on_##name(void) \
> -
> { \
> - return
> rv_reacting_on(); \
> -}
> -
> -#else /* CONFIG_RV_REACTOR */
> -
> -#define DECLARE_RV_REACTING_HELPERS(name,
> type) \
> -static inline char *format_react_msg_##name(type curr_state, type
> event) \
> -
> { \
> - return
> NULL; \
> -
> } \
> -
> \
> -static void cond_react_##name(char
> *msg) \
> -
> { \
> -
> return; \
> -
> } \
> -
> \
> -static bool
> rv_reacting_on_##name(void) \
> -
> { \
> - return
> 0; \
> -}
> -#endif
> -
I don't think you need to remove those helper functions, why not just
having format_react_msg_ prepare the arguments for react?
cond_react might be mildly useful also for ltl, we may think about
putting it somewhere else and/or refactoring it a bit to include
reacting_on (which is indeed global and doesn't require a per-monitor
wrapper).
> /*
> * Generic helpers for all types of deterministic automata monitors.
> */
> #define DECLARE_DA_MON_GENERIC_HELPERS(name,
> type) \
>
> \
> -DECLARE_RV_REACTING_HELPERS(name,
> type) \
> -
> \
> /*
> \
> * da_monitor_reset_##name - reset a monitor and setting it to init
> state \
>
> */ \
> @@ -170,8 +123,11 @@ da_event_##name(struct da_monitor *da_mon, enum
> events_##name event) \
> return
> true; \
> }
> \
>
> \
> - if
> (rv_reacting_on_##name()) \
> -
> cond_react_##name(format_react_msg_##name(curr_state, event)); \
> + if (rv_reacting_on() &&
> rv_##name.react) \
> + rv_##name.react("rv: monitor %s does not allow event
> %s on state %s\n", \
> + #name,
> \
> + model_get_event_name_##name(event),
> \
> + model_get_state_name_##name(curr_sta
> te)); \
>
> \
> trace_error_##name(model_get_state_name_##name(curr_state),
> \
>
> model_get_event_name_##name(event)); \
> @@ -202,8 +158,11 @@ static inline bool da_event_##name(struct
> da_monitor *da_mon, struct task_struct
> return
> true; \
> }
> \
>
> \
> - if
> (rv_reacting_on_##name()) \
> -
> cond_react_##name(format_react_msg_##name(curr_state, event)); \
> + if (rv_reacting_on() &&
> rv_##name.react) \
> + rv_##name.react("rv: monitor %s does not allow event
> %s on state %s\n", \
> + #name,
> \
> + model_get_event_name_##name(event),
> \
> + model_get_state_name_##name(curr_sta
> te)); \
>
> \
> trace_error_##name(tsk-
> >pid, \
>
> model_get_state_name_##name(curr_state), \
> diff --git a/kernel/printk/internal.h b/kernel/printk/internal.h
> index a91bdf802967..28afdeb58412 100644
> --- a/kernel/printk/internal.h
> +++ b/kernel/printk/internal.h
> @@ -71,7 +71,6 @@ int vprintk_store(int facility, int level,
> const char *fmt, va_list args);
>
> __printf(1, 0) int vprintk_default(const char *fmt, va_list args);
> -__printf(1, 0) int vprintk_deferred(const char *fmt, va_list args);
>
> void __printk_safe_enter(void);
> void __printk_safe_exit(void);
> diff --git a/kernel/trace/rv/reactor_panic.c
> b/kernel/trace/rv/reactor_panic.c
> index 0186ff4cbd0b..4addabc9bcf1 100644
> --- a/kernel/trace/rv/reactor_panic.c
> +++ b/kernel/trace/rv/reactor_panic.c
> @@ -13,15 +13,10 @@
> #include <linux/init.h>
> #include <linux/rv.h>
>
> -static void rv_panic_reaction(char *msg)
> -{
> - panic(msg);
> -}
> -
> static struct rv_reactor rv_panic = {
> .name = "panic",
> .description = "panic the system if an exception is found.",
> - .react = rv_panic_reaction
> + .react = panic
> };
For the sake of verbosity, I would still keep a wrapper function around
panic, just to show directly from this file how should a react()
function look like, as well as allowing future modifications, if
needed. Not that the additional function call would be much of a
problem during panic, I believe.
Good improvement overall, thanks.
Gabriele
>
> static int __init register_react_panic(void)
> diff --git a/kernel/trace/rv/reactor_printk.c
> b/kernel/trace/rv/reactor_printk.c
> index 178759dbf89f..a15db3fc8b82 100644
> --- a/kernel/trace/rv/reactor_printk.c
> +++ b/kernel/trace/rv/reactor_printk.c
> @@ -12,9 +12,13 @@
> #include <linux/init.h>
> #include <linux/rv.h>
>
> -static void rv_printk_reaction(char *msg)
> +static void rv_printk_reaction(const char *msg, ...)
> {
> - printk_deferred(msg);
> + va_list args;
> +
> + va_start(args, msg);
> + vprintk_deferred(msg, args);
> + va_end(args);
> }
>
> static struct rv_reactor rv_printk = {
> diff --git a/kernel/trace/rv/rv_reactors.c
> b/kernel/trace/rv/rv_reactors.c
> index 7b49cbe388d4..885661fe2b6e 100644
> --- a/kernel/trace/rv/rv_reactors.c
> +++ b/kernel/trace/rv/rv_reactors.c
> @@ -468,7 +468,7 @@ void reactor_cleanup_monitor(struct
> rv_monitor_def *mdef)
> /*
> * Nop reactor register
> */
> -static void rv_nop_reaction(char *msg)
> +static void rv_nop_reaction(const char *msg, ...)
> {
> }
>
^ permalink raw reply [flat|nested] 23+ messages in thread* Re: [PATCH 02/10] rv: Let the reactors take care of buffers
2025-03-12 7:58 ` Gabriele Monaco
@ 2025-03-13 8:16 ` Nam Cao
2025-03-13 11:39 ` Gabriele Monaco
0 siblings, 1 reply; 23+ messages in thread
From: Nam Cao @ 2025-03-13 8:16 UTC (permalink / raw)
To: Gabriele Monaco
Cc: Steven Rostedt, john.ogness, linux-trace-kernel, linux-kernel,
Petr Mladek, Sergey Senozhatsky
Hi Gabriele,
On Wed, Mar 12, 2025 at 08:58:56AM +0100, Gabriele Monaco wrote:
> On Tue, 2025-03-11 at 18:05 +0100, Nam Cao wrote:
> > diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
> > index 510c88bfabd4..c55d45544a16 100644
> > --- a/include/rv/da_monitor.h
> > +++ b/include/rv/da_monitor.h
> > @@ -16,58 +16,11 @@
> > #include <linux/bug.h>
> > #include <linux/sched.h>
> >
> > -#ifdef CONFIG_RV_REACTORS
> > -
> > -#define DECLARE_RV_REACTING_HELPERS(name,
> > type) \
> > -static char
> > REACT_MSG_##name[1024]; \
> > -
> > \
> > -static inline char *format_react_msg_##name(type curr_state, type
> > event) \
> > -
> > { \
> > - snprintf(REACT_MSG_##name,
> > 1024, \
> > - "rv: monitor %s does not allow event %s on state
> > %s\n", \
> > -
> > #name, \
> > -
> > model_get_event_name_##name(event), \
> > -
> > model_get_state_name_##name(curr_state)); \
> > - return
> > REACT_MSG_##name; \
> > -
> > } \
> > -
> > \
> > -static void cond_react_##name(char
> > *msg) \
> > -
> > { \
> > - if
> > (rv_##name.react) \
> > -
> > rv_##name.react(msg); \
> > -
> > } \
> > -
> > \
> > -static bool
> > rv_reacting_on_##name(void) \
> > -
> > { \
> > - return
> > rv_reacting_on(); \
> > -}
> > -
> > -#else /* CONFIG_RV_REACTOR */
> > -
> > -#define DECLARE_RV_REACTING_HELPERS(name,
> > type) \
> > -static inline char *format_react_msg_##name(type curr_state, type
> > event) \
> > -
> > { \
> > - return
> > NULL; \
> > -
> > } \
> > -
> > \
> > -static void cond_react_##name(char
> > *msg) \
> > -
> > { \
> > -
> > return; \
> > -
> > } \
> > -
> > \
> > -static bool
> > rv_reacting_on_##name(void) \
> > -
> > { \
> > - return
> > 0; \
> > -}
> > -#endif
> > -
>
> I don't think you need to remove those helper functions, why not just
> having format_react_msg_ prepare the arguments for react?
I'm not sure what you mean. Making format_react_msg_* a macro that is
preprocessed into arguments? Then make cond_react_*() a variadic function,
so that we can "pass" format_react_msg_* to it?
Going that way would also need a vreact() variant, as cond_react_*() cannot
pass on the variadic arguments to react().
Instead, is it cleaner to do the below?
diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
index 510c88bfabd4..e185ebf894a4 100644
--- a/include/rv/da_monitor.h
+++ b/include/rv/da_monitor.h
@@ -19,22 +19,14 @@
#ifdef CONFIG_RV_REACTORS
#define DECLARE_RV_REACTING_HELPERS(name, type) \
-static char REACT_MSG_##name[1024]; \
- \
-static inline char *format_react_msg_##name(type curr_state, type event) \
-{ \
- snprintf(REACT_MSG_##name, 1024, \
- "rv: monitor %s does not allow event %s on state %s\n", \
- #name, \
- model_get_event_name_##name(event), \
- model_get_state_name_##name(curr_state)); \
- return REACT_MSG_##name; \
-} \
- \
-static void cond_react_##name(char *msg) \
+static void cond_react_##name(type curr_state, type event) \
{ \
- if (rv_##name.react) \
- rv_##name.react(msg); \
+ if (!rv_##name.react) \
+ return; \
+ rv_##name.react("rv: monitor %s does not allow event %s on state %s\n", \
+ #name, \
+ model_get_event_name_##name(event), \
+ model_get_state_name_##name(curr_state)); \
} \
\
static bool rv_reacting_on_##name(void) \
@@ -45,12 +37,7 @@ static bool rv_reacting_on_##name(void) \
#else /* CONFIG_RV_REACTOR */
#define DECLARE_RV_REACTING_HELPERS(name, type) \
-static inline char *format_react_msg_##name(type curr_state, type event) \
-{ \
- return NULL; \
-} \
- \
-static void cond_react_##name(char *msg) \
+static void cond_react_##name(type curr_state, type event) \
{ \
return; \
} \
@@ -171,7 +158,7 @@ da_event_##name(struct da_monitor *da_mon, enum events_##name event) \
} \
\
if (rv_reacting_on_##name()) \
- cond_react_##name(format_react_msg_##name(curr_state, event)); \
+ cond_react_##name(curr_state, event); \
\
trace_error_##name(model_get_state_name_##name(curr_state), \
model_get_event_name_##name(event)); \
@@ -203,7 +190,7 @@ static inline bool da_event_##name(struct da_monitor *da_mon, struct task_struct
} \
\
if (rv_reacting_on_##name()) \
- cond_react_##name(format_react_msg_##name(curr_state, event)); \
+ cond_react_##name(curr_state, event); \
\
trace_error_##name(tsk->pid, \
model_get_state_name_##name(curr_state), \
Best regards,
Nam
^ permalink raw reply related [flat|nested] 23+ messages in thread* Re: [PATCH 02/10] rv: Let the reactors take care of buffers
2025-03-13 8:16 ` Nam Cao
@ 2025-03-13 11:39 ` Gabriele Monaco
0 siblings, 0 replies; 23+ messages in thread
From: Gabriele Monaco @ 2025-03-13 11:39 UTC (permalink / raw)
To: Nam Cao
Cc: Steven Rostedt, john.ogness, linux-trace-kernel, linux-kernel,
Petr Mladek, Sergey Senozhatsky
On Thu, 2025-03-13 at 09:16 +0100, Nam Cao wrote:
> Hi Gabriele,
>
> On Wed, Mar 12, 2025 at 08:58:56AM +0100, Gabriele Monaco wrote:
> > On Tue, 2025-03-11 at 18:05 +0100, Nam Cao wrote:
> > > diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
> > > index 510c88bfabd4..c55d45544a16 100644
> > > --- a/include/rv/da_monitor.h
> > > +++ b/include/rv/da_monitor.h
> > > @@ -16,58 +16,11 @@
> > > #include <linux/bug.h>
> > > #include <linux/sched.h>
> > >
> > > -#ifdef CONFIG_RV_REACTORS
> > > -
> > > -#define DECLARE_RV_REACTING_HELPERS(name,
> > > type) \
> > > -static char
> > > REACT_MSG_##name[1024];
> > > \
> > > -
> > >
> > > \
> > > -static inline char *format_react_msg_##name(type curr_state,
> > > type
> > > event) \
> > > -
> > > {
> > > \
> > > - snprintf(REACT_MSG_##name,
> > > 1024, \
> > > - "rv: monitor %s does not allow event %s on
> > > state
> > > %s\n", \
> > > -
> > > #name,
> > > \
> > > -
> > > model_get_event_name_##name(event),
> > > \
> > > -
> > > model_get_state_name_##name(curr_state));
> > > \
> > > - return
> > > REACT_MSG_##name;
> > > \
> > > -
> > > }
> > > \
> > > -
> > >
> > > \
> > > -static void cond_react_##name(char
> > > *msg) \
> > > -
> > > {
> > > \
> > > - if
> > > (rv_##name.react)
> > > \
> > > -
> > > rv_##name.react(msg);
> > > \
> > > -
> > > }
> > > \
> > > -
> > >
> > > \
> > > -static bool
> > > rv_reacting_on_##name(void)
> > > \
> > > -
> > > {
> > > \
> > > - return
> > > rv_reacting_on();
> > > \
> > > -}
> > > -
> > > -#else /* CONFIG_RV_REACTOR */
> > > -
> > > -#define DECLARE_RV_REACTING_HELPERS(name,
> > > type) \
> > > -static inline char *format_react_msg_##name(type curr_state,
> > > type
> > > event) \
> > > -
> > > {
> > > \
> > > - return
> > > NULL;
> > > \
> > > -
> > > }
> > > \
> > > -
> > >
> > > \
> > > -static void cond_react_##name(char
> > > *msg) \
> > > -
> > > {
> > > \
> > > -
> > > return;
> > > \
> > > -
> > > }
> > > \
> > > -
> > >
> > > \
> > > -static bool
> > > rv_reacting_on_##name(void)
> > > \
> > > -
> > > {
> > > \
> > > - return
> > > 0;
> > > \
> > > -}
> > > -#endif
> > > -
> >
> > I don't think you need to remove those helper functions, why not
> > just
> > having format_react_msg_ prepare the arguments for react?
>
> I'm not sure what you mean. Making format_react_msg_* a macro that is
> preprocessed into arguments? Then make cond_react_*() a variadic
> function,
> so that we can "pass" format_react_msg_* to it?
>
> Going that way would also need a vreact() variant, as cond_react_*()
> cannot
> pass on the variadic arguments to react().
>
> Instead, is it cleaner to do the below?
Hi Nam,
you're right, I got a bit confused, all I meant was to find a way not
to repeat the arguments for implicit and per-task monitors.
What you propose seems perfect to me.
Also for the sake of simplifying things, a bit like you started, we
could have the reacting_on() check inside cond_react and drop the per-
monitor function. I believe the initial idea was to have a reacting_on
toggle for each monitor but since it isn't the case, we don't really
need it.
Thanks,
Gabriele
>
> diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
> index 510c88bfabd4..e185ebf894a4 100644
> --- a/include/rv/da_monitor.h
> +++ b/include/rv/da_monitor.h
> @@ -19,22 +19,14 @@
> #ifdef CONFIG_RV_REACTORS
>
> #define DECLARE_RV_REACTING_HELPERS(name,
> type) \
> -static char
> REACT_MSG_##name[1024]; \
> -
> \
> -static inline char *format_react_msg_##name(type curr_state, type
> event) \
> -
> { \
> - snprintf(REACT_MSG_##name,
> 1024, \
> - "rv: monitor %s does not allow event %s on state
> %s\n", \
> -
> #name, \
> -
> model_get_event_name_##name(event), \
> -
> model_get_state_name_##name(curr_state)); \
> - return
> REACT_MSG_##name; \
> -
> } \
> -
> \
> -static void cond_react_##name(char
> *msg) \
> +static void cond_react_##name(type curr_state, type
> event) \
> {
> \
> - if
> (rv_##name.react) \
> -
> rv_##name.react(msg); \
> + if
> (!rv_##name.react) \
> + return;
> \
> + rv_##name.react("rv: monitor %s does not allow event %s on
> state %s\n", \
> + #name,
> \
> + model_get_event_name_##name(event),
> \
> + model_get_state_name_##name(curr_state));
> \
> }
> \
>
> \
> static bool
> rv_reacting_on_##name(void) \
> @@ -45,12 +37,7 @@ static bool
> rv_reacting_on_##name(void) \
> #else /* CONFIG_RV_REACTOR */
>
> #define DECLARE_RV_REACTING_HELPERS(name,
> type) \
> -static inline char *format_react_msg_##name(type curr_state, type
> event) \
> -
> { \
> - return
> NULL; \
> -
> } \
> -
> \
> -static void cond_react_##name(char
> *msg) \
> +static void cond_react_##name(type curr_state, type
> event) \
> {
> \
> return;
> \
> }
> \
> @@ -171,7 +158,7 @@ da_event_##name(struct da_monitor *da_mon, enum
> events_##name event) \
> }
> \
>
> \
> if
> (rv_reacting_on_##name()) \
> -
> cond_react_##name(format_react_msg_##name(curr_state, event)); \
> + cond_react_##name(curr_state,
> event); \
>
> \
> trace_error_##name(model_get_state_name_##name(curr_state),
> \
>
> model_get_event_name_##name(event)); \
> @@ -203,7 +190,7 @@ static inline bool da_event_##name(struct
> da_monitor *da_mon, struct task_struct
> }
> \
>
> \
> if
> (rv_reacting_on_##name()) \
> -
> cond_react_##name(format_react_msg_##name(curr_state, event)); \
> + cond_react_##name(curr_state,
> event); \
>
> \
> trace_error_##name(tsk-
> >pid, \
>
> model_get_state_name_##name(curr_state), \
>
> Best regards,
> Nam
>
^ permalink raw reply [flat|nested] 23+ messages in thread
* Re: [PATCH 02/10] rv: Let the reactors take care of buffers
2025-03-11 17:05 ` [PATCH 02/10] rv: Let the reactors take care of buffers Nam Cao
2025-03-12 7:58 ` Gabriele Monaco
@ 2025-03-13 16:07 ` kernel test robot
2025-03-13 16:07 ` kernel test robot
2 siblings, 0 replies; 23+ messages in thread
From: kernel test robot @ 2025-03-13 16:07 UTC (permalink / raw)
To: Nam Cao, Steven Rostedt, Gabriele Monaco, john.ogness,
linux-trace-kernel, linux-kernel
Cc: llvm, oe-kbuild-all, Nam Cao, Petr Mladek, Sergey Senozhatsky
Hi Nam,
kernel test robot noticed the following build warnings:
[auto build test WARNING on trace/for-next]
[also build test WARNING on tip/x86/core tip/x86/mm linus/master v6.14-rc6 next-20250313]
[If your patch is applied to the wrong git tree, kindly drop us a note.
And when submitting patch, we suggest to use '--base' as documented in
https://git-scm.com/docs/git-format-patch#_base_tree_information]
url: https://github.com/intel-lab-lkp/linux/commits/Nam-Cao/rv-Add-undef-TRACE_INCLUDE_FILE/20250312-011043
base: https://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace for-next
patch link: https://lore.kernel.org/r/90868f1dd49680ec63c961ec8c72ceb64f1af091.1741708239.git.namcao%40linutronix.de
patch subject: [PATCH 02/10] rv: Let the reactors take care of buffers
config: sh-allmodconfig (https://download.01.org/0day-ci/archive/20250313/202503132340.zzBclxPj-lkp@intel.com/config)
compiler: sh4-linux-gcc (GCC) 14.2.0
reproduce (this is a W=1 build): (https://download.01.org/0day-ci/archive/20250313/202503132340.zzBclxPj-lkp@intel.com/reproduce)
If you fix the issue in a separate patch/commit (i.e. not just a new version of
the same patch/commit), kindly add following tags
| Reported-by: kernel test robot <lkp@intel.com>
| Closes: https://lore.kernel.org/oe-kbuild-all/202503132340.zzBclxPj-lkp@intel.com/
All warnings (new ones prefixed by >>):
>> kernel/trace/rv/reactor_panic.c:19:18: warning: initialization left-hand side might be a candidate for a format attribute [-Wsuggest-attribute=format]
19 | .react = panic
| ^~~~~
vim +19 kernel/trace/rv/reactor_panic.c
15
16 static struct rv_reactor rv_panic = {
17 .name = "panic",
18 .description = "panic the system if an exception is found.",
> 19 .react = panic
20 };
21
--
0-DAY CI Kernel Test Service
https://github.com/intel/lkp-tests/wiki
^ permalink raw reply [flat|nested] 23+ messages in thread* Re: [PATCH 02/10] rv: Let the reactors take care of buffers
2025-03-11 17:05 ` [PATCH 02/10] rv: Let the reactors take care of buffers Nam Cao
2025-03-12 7:58 ` Gabriele Monaco
2025-03-13 16:07 ` kernel test robot
@ 2025-03-13 16:07 ` kernel test robot
2 siblings, 0 replies; 23+ messages in thread
From: kernel test robot @ 2025-03-13 16:07 UTC (permalink / raw)
To: Nam Cao, Steven Rostedt, Gabriele Monaco, john.ogness,
linux-trace-kernel, linux-kernel
Cc: llvm, oe-kbuild-all, Nam Cao, Petr Mladek, Sergey Senozhatsky
Hi Nam,
kernel test robot noticed the following build errors:
[auto build test ERROR on trace/for-next]
[also build test ERROR on tip/x86/core tip/x86/mm linus/master v6.14-rc6 next-20250313]
[If your patch is applied to the wrong git tree, kindly drop us a note.
And when submitting patch, we suggest to use '--base' as documented in
https://git-scm.com/docs/git-format-patch#_base_tree_information]
url: https://github.com/intel-lab-lkp/linux/commits/Nam-Cao/rv-Add-undef-TRACE_INCLUDE_FILE/20250312-011043
base: https://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace for-next
patch link: https://lore.kernel.org/r/90868f1dd49680ec63c961ec8c72ceb64f1af091.1741708239.git.namcao%40linutronix.de
patch subject: [PATCH 02/10] rv: Let the reactors take care of buffers
config: parisc-randconfig-002-20250313 (https://download.01.org/0day-ci/archive/20250313/202503132350.aM5NZ6Vh-lkp@intel.com/config)
compiler: hppa-linux-gcc (GCC) 14.2.0
reproduce (this is a W=1 build): (https://download.01.org/0day-ci/archive/20250313/202503132350.aM5NZ6Vh-lkp@intel.com/reproduce)
If you fix the issue in a separate patch/commit (i.e. not just a new version of
the same patch/commit), kindly add following tags
| Reported-by: kernel test robot <lkp@intel.com>
| Closes: https://lore.kernel.org/oe-kbuild-all/202503132350.aM5NZ6Vh-lkp@intel.com/
All errors (new ones prefixed by >>):
kernel/trace/rv/reactor_printk.c: In function 'rv_printk_reaction':
>> kernel/trace/rv/reactor_printk.c:20:9: error: implicit declaration of function 'vprintk_deferred'; did you mean '_printk_deferred'? [-Wimplicit-function-declaration]
20 | vprintk_deferred(msg, args);
| ^~~~~~~~~~~~~~~~
| _printk_deferred
vim +20 kernel/trace/rv/reactor_printk.c
14
15 static void rv_printk_reaction(const char *msg, ...)
16 {
17 va_list args;
18
19 va_start(args, msg);
> 20 vprintk_deferred(msg, args);
21 va_end(args);
22 }
23
--
0-DAY CI Kernel Test Service
https://github.com/intel/lkp-tests/wiki
^ permalink raw reply [flat|nested] 23+ messages in thread
* [PATCH 03/10] rv: Add infrastructure for linear temporal logic monitor
2025-03-11 17:05 [PATCH 00/10] RV: Linear temporal logic monitors for RT application Nam Cao
2025-03-11 17:05 ` [PATCH 01/10] rv: Add #undef TRACE_INCLUDE_FILE Nam Cao
2025-03-11 17:05 ` [PATCH 02/10] rv: Let the reactors take care of buffers Nam Cao
@ 2025-03-11 17:05 ` Nam Cao
2025-03-12 6:47 ` Gabriele Monaco
2025-03-11 17:05 ` [PATCH 04/10] rv: Add rtapp_block monitor Nam Cao
` (6 subsequent siblings)
9 siblings, 1 reply; 23+ messages in thread
From: Nam Cao @ 2025-03-11 17:05 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, john.ogness, linux-trace-kernel,
linux-kernel
Cc: Nam Cao
Prepare the infrastructure for linear temporal logic monitors:
- add scripts for generating the monitors
- implement data structures
For details, see:
Documentation/trace/rv/linear_temporal_logic.rst
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
.../trace/rv/linear_temporal_logic.rst | 73 +++
include/linux/rv.h | 26 +-
kernel/fork.c | 5 +-
tools/verification/ltl2ba/.gitignore | 3 +
tools/verification/ltl2ba/generate.py | 154 +++++
tools/verification/ltl2ba/ltl.py | 556 ++++++++++++++++++
tools/verification/ltl2ba/template.c | 131 +++++
tools/verification/ltl2ba/template.h | 157 +++++
8 files changed, 1097 insertions(+), 8 deletions(-)
create mode 100644 Documentation/trace/rv/linear_temporal_logic.rst
create mode 100644 tools/verification/ltl2ba/.gitignore
create mode 100755 tools/verification/ltl2ba/generate.py
create mode 100644 tools/verification/ltl2ba/ltl.py
create mode 100644 tools/verification/ltl2ba/template.c
create mode 100644 tools/verification/ltl2ba/template.h
diff --git a/Documentation/trace/rv/linear_temporal_logic.rst b/Documentation/trace/rv/linear_temporal_logic.rst
new file mode 100644
index 000000000000..9b0ce6a143ec
--- /dev/null
+++ b/Documentation/trace/rv/linear_temporal_logic.rst
@@ -0,0 +1,73 @@
+Introduction
+============
+
+Deterministic automaton runtime verification monitor is a verification technique which checks that
+the kernel follows a specification in the form of deterministic automaton (DA). It does so by using
+tracepoints to monitor the kernel's execution trace, and verifying that the execution trace
+sastifies the specification.
+
+However, 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.
+
+Thus, RV monitors based on linear temporal logic (LTL for short) are introduced. This type of
+monitor uses LTL as specification, instead of DA. For some cases, writing the specification as LTL
+is more concise and intuitive.
+
+Documents regarding LTL are widely available on the internet, this document will not go into
+details.
+
+Grammar
+========
+
+Unlike some existing syntax, kernel's implementation of LTL is more verbose. This is motivated by
+considering that the people who read the LTL specifications may not be well-versed in LTL.
+
+Grammar:
+ ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
+
+Operands (opd):
+ true, false, user-defined names consisting of upper-case characters, digits, and underscore.
+
+Unary Operators (unop):
+ always
+ eventually
+ not
+
+Binary Operators (binop):
+ until
+ and
+ or
+ imply
+ equivalent
+
+This grammar is ambiguous: operator precedence is not defined. Parentheses must be used.
+
+Monitor synthesis
+=================
+
+To synthesize an LTL into a kernel monitor, conversion scripts are provided:
+`tools/verification/ltl2ba`. The specification needs to be provided as a file, and it must have a
+"RULE = LTL" assignment, which specifies the LTL property to verify. For example:
+
+ .. code-block::
+
+ RULE = always (ACQUIRE imply ((not KILLED and not CRASHED) until RELEASE))
+
+The LTL can be broken down if required using sub-expressions. For example, the above is equivalent
+to:
+
+ .. code-block::
+
+ RULE = always (ACQUIRE imply (ALIVE until RELEASE))
+ ALIVE = not KILLED and not CRASHED
+
+The ltl file can be converted into C code:
+
+ .. code-block::
+
+ .tools/verification/ltl2ba/generate.py -l <ltl file> -n <model name> -o <output diretory>
+
+The above command generates `ba.c` and `ba.h`, the Buchi automaton that verifies the LTL property.
+The Buchi automaton needs to be manually glued to the kernel. Please see the comments in `ba.h` for
+further details.
diff --git a/include/linux/rv.h b/include/linux/rv.h
index 5482651ed020..6de4f93b390e 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -10,6 +10,8 @@
#define MAX_DA_NAME_LEN 24
#ifdef CONFIG_RV
+#include <linux/types.h>
+
/*
* Deterministic automaton per-object variables.
*/
@@ -18,6 +20,24 @@ struct da_monitor {
unsigned int curr_state;
};
+enum ltl_truth_value {
+ LTL_FALSE,
+ LTL_TRUE,
+ LTL_UNDETERMINED,
+};
+
+/*
+ * In the future, if the number of atomic propositions or the custom data size is larger, we can
+ * switch to dynamic allocation. For now, the code is simpler this way.
+ */
+#define RV_MAX_LTL_ATOM 10
+#define RV_MAX_DATA_SIZE 16
+struct ltl_monitor {
+ unsigned int state;
+ enum ltl_truth_value atoms[RV_MAX_LTL_ATOM];
+ u8 data[RV_MAX_DATA_SIZE];
+};
+
/*
* 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 +47,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
diff --git a/kernel/fork.c b/kernel/fork.c
index 735405a9c5f3..5d6c1caca702 100644
--- a/kernel/fork.c
+++ b/kernel/fork.c
@@ -2127,10 +2127,7 @@ static void copy_oom_score_adj(u64 clone_flags, struct task_struct *tsk)
#ifdef CONFIG_RV
static void rv_task_fork(struct task_struct *p)
{
- int i;
-
- for (i = 0; i < RV_PER_TASK_MONITORS; i++)
- p->rv[i].da_mon.monitoring = false;
+ memset(p->rv, 0, sizeof(p->rv));
}
#else
#define rv_task_fork(p) do {} while (0)
diff --git a/tools/verification/ltl2ba/.gitignore b/tools/verification/ltl2ba/.gitignore
new file mode 100644
index 000000000000..9c47b9724860
--- /dev/null
+++ b/tools/verification/ltl2ba/.gitignore
@@ -0,0 +1,3 @@
+__pycache__/
+parsetab.py
+parser.out
diff --git a/tools/verification/ltl2ba/generate.py b/tools/verification/ltl2ba/generate.py
new file mode 100755
index 000000000000..52d5b3618e64
--- /dev/null
+++ b/tools/verification/ltl2ba/generate.py
@@ -0,0 +1,154 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+
+import argparse
+import ntpath
+import os
+import platform
+from pathlib import Path
+import sys
+import ltl
+
+parser = argparse.ArgumentParser(description='transform ltl file into kernel rv monitor')
+parser.add_argument('-l', "--ltl", dest="ltl", required=True)
+parser.add_argument('-n', "--model_name", dest="model_name", required=True)
+parser.add_argument('-o', "--outdir", dest="outdir", required=True)
+params = parser.parse_args()
+
+with open(params.ltl) as f:
+ atoms, graph = ltl.create_graph(f.read())
+states = []
+transitions = []
+init_conditions = []
+
+COLUMN_LIMIT = 100
+
+def build_condition_string(node: ltl.GraphNode):
+ if not node.labels:
+ return "(true)"
+
+ result = "("
+
+ first = True
+ for l in sorted(node.labels):
+ if not first:
+ result += " && "
+ result += '(' + l + ')'
+ first = False
+
+ result += ")"
+
+ return result
+
+def build_states() -> str:
+ states = ''
+ for node in graph:
+ states += "\t%s,\n" % node.name
+ return states
+
+def build_atoms() -> str:
+ global atoms
+ s = ''
+ for a in sorted(atoms):
+ s += "\t%s,\n" % a
+ return s
+
+def build_transitions() -> list[str]:
+ transitions = []
+ for node in graph:
+ transitions.append("\tcase %s:\n" % node.name)
+
+ result = ""
+ first = True
+ for o in sorted(node.outgoing):
+ if first:
+ result += "\t\tif "
+ cursor = 19
+ else:
+ result += "\t\telse if "
+ cursor = 24
+
+ condition = build_condition_string(o)
+
+ while len(condition) + cursor > COLUMN_LIMIT:
+ i = condition[:COLUMN_LIMIT - cursor].rfind(' ')
+ result += condition[:i]
+ if cursor == 19:
+ result += '\n\t\t '
+ elif cursor == 24:
+ result += '\t\t\t\t'
+ else:
+ raise ValueError()
+ condition = condition[i + 1:]
+
+ result += condition
+
+ result += '\n'
+ result += ("\t\t\tmon->state = %s;\n" % o.name)
+ first = False
+ result += "\t\telse\n\t\t\tillegal_state(task, mon);\n"
+ result += "\t\tbreak;\n"
+ transitions.append(result)
+ return transitions
+
+def build_initial_conditions() -> str:
+ result = ""
+ first = True
+
+ for node in graph:
+ if not node.init:
+ continue
+
+ if not first:
+ result += "\telse if "
+ cursor = 16
+ else:
+ result += "\tif "
+ cursor = 11
+
+ condition = build_condition_string(node)
+ while len(condition) + cursor > COLUMN_LIMIT:
+ i = condition[:COLUMN_LIMIT - cursor].rfind(' ')
+ result += condition[:i]
+ if cursor == 16:
+ result += '\n\t\t'
+ elif cursor == 11:
+ result += '\n\t '
+ else:
+ raise ValueError()
+ condition = condition[i + 1:]
+
+ result += condition
+ result += '\n'
+ result += ("\t\tmon->state = %s;\n" % node.name)
+ first = False
+ result += "\telse\n\t\tillegal_state(task, mon);\n"
+ return result
+
+template = Path(__file__).with_name('template.h')
+out = os.path.join(params.outdir, "ba.h")
+with template.open() as template, open(out, "w") as file:
+ for line in template:
+ if line == "%%ATOM_LIST%%\n":
+ file.write(build_atoms())
+ else:
+ line = line.replace("%%MODEL_NAME%%", params.model_name)
+ file.write(line)
+
+template = Path(__file__).with_name('template.c')
+out = os.path.join(params.outdir, "ba.c")
+with template.open() as template, open(out, "w") as file:
+ for line in template:
+ if line == "%%STATE_LIST%%\n":
+ file.write(build_states())
+ elif line == "%%BUCHI_START%%\n":
+ file.write(build_initial_conditions())
+ elif line == "%%BUCHI_TRANSITIONS%%\n":
+ for t in build_transitions():
+ file.write(t)
+ elif line == "%%ERROR_MESSAGE%%\n":
+ file.write(build_error_message())
+ else:
+ line = line.replace("%%MODEL_NAME%%", params.model_name)
+ line = line.replace("%%LTL%%", params.ltl)
+ file.write(line)
diff --git a/tools/verification/ltl2ba/ltl.py b/tools/verification/ltl2ba/ltl.py
new file mode 100644
index 000000000000..aa3a11d78a8e
--- /dev/null
+++ b/tools/verification/ltl2ba/ltl.py
@@ -0,0 +1,556 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Implementation based on
+# Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996).
+# Simple On-the-fly Automatic Verification of Linear Temporal Logic.
+# https://doi.org/10.1007/978-0-387-34892-6_1
+# With extra optimizations
+
+from ply.lex import lex
+from ply.yacc import yacc
+
+# Grammar:
+# ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
+#
+# Operands (opd):
+# true, false, user-defined names
+#
+# Unary Operators (unop):
+# always
+# eventually
+# not
+#
+# Binary Operators (binop):
+# until
+# and
+# or
+# imply
+# equivalent
+
+tokens = (
+ 'AND',
+ 'OR',
+ 'IMPLY',
+ 'UNTIL',
+ 'ALWAYS',
+ 'EVENTUALLY',
+ '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_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 ValueError("Illegal character '%s'" % t.value[0])
+
+lexer = lex()
+
+_new_name_counter = 0
+def new_name():
+ global _new_name_counter
+
+ _new_name_counter += 1
+
+ return "S" + str(_new_name_counter)
+
+class GraphNode:
+ def __init__(self, name: str, incoming: set['GraphNode'], new, old, _next):
+ self.init = False
+ self.outgoing = set()
+ self.labels = set()
+ self.incoming = incoming
+ self.name = name
+ self.new = new.copy()
+ self.old = old.copy()
+ self.next = _next.copy()
+
+ def expand(self, node_set):
+ if not self.new:
+ for nd in node_set:
+ if nd.old == self.old and nd.next == self.next:
+ nd.incoming |= self.incoming
+ for i in self.incoming:
+ i.outgoing.add(nd)
+ return node_set
+
+ new_current_node = GraphNode(new_name(), {self}, self.next, set(), set())
+ return new_current_node.expand({self} | node_set)
+ n = self.new.pop()
+ return n.expand(self, node_set)
+
+ def __lt__(self, other):
+ return self.name < other.name
+
+class ASTNode:
+ def __init__(self,op):
+ self.op = op
+
+ def __hash__(self):
+ return hash(self.op)
+
+ def __str__(self):
+ return str(self.op)
+
+ def __eq__(self, other):
+ return self is other
+
+ def __iter__(self):
+ yield self
+ yield from self.op
+
+ def negate(self):
+ self.op = self.op.negate()
+ return self
+
+ def expand(self, node, node_set):
+ return self.op.expand(self, node, node_set)
+
+ def normalize(self):
+ # Get rid of:
+ # - ALWAYS
+ # - EVENTUALLY
+ # - IMPLY
+ # And move all the NOT to be inside
+ self.op = self.op.normalize()
+ return self
+
+class BinaryOp:
+ op_str = "not_supported"
+
+ def __init__(self, left: ASTNode, right: ASTNode):
+ self.left = left
+ self.right = right
+
+ def __str__(self):
+ return "(%s %s %s)" % (self.left, self.op_str, self.right)
+
+ def __hash__(self):
+ return hash((self.left, self.right))
+
+ def __iter__(self):
+ yield from self.left
+ yield from self.right
+
+ def normalize(self):
+ raise NotImplemented
+
+ def negate(self):
+ raise NotImplemented
+
+ def _is_temporal(self):
+ raise NotImplemented
+
+ def is_temporal(self):
+ if self.left.op.is_temporal():
+ return True
+ if self.right.op.is_temporal():
+ return True
+ return self._is_temporal()
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ raise NotImplemented
+
+class AndOp(BinaryOp):
+ op_str = '&&'
+
+ def __init__(self, left, right):
+ super().__init__(left, right)
+
+ def normalize(self):
+ return self
+
+ def negate(self):
+ return OrOp(self.left.negate(), self.right.negate())
+
+ def _is_temporal(self):
+ return False
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ if not n.op.is_temporal():
+ node.old.add(n)
+ return node.expand(node_set)
+
+ tmp = GraphNode(node.name, node.incoming,
+ node.new | ({n.op.left, n.op.right} - node.old),
+ node.old | {n},
+ node.next)
+ return tmp.expand(node_set)
+
+class OrOp(BinaryOp):
+ op_str = '||'
+
+ def __init__(self, left, right):
+ super().__init__(left, right)
+
+ def normalize(self):
+ return self
+
+ def negate(self):
+ return AndOp(self.left.negate(), self.right.negate())
+
+ def _is_temporal(self):
+ return False
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ if not n.op.is_temporal():
+ node.old |= {n}
+ return node.expand(node_set)
+
+ node1 = GraphNode(new_name(), node.incoming,
+ node.new | ({n.op.left} - node.old),
+ node.old | {n},
+ node.next)
+ node2 = GraphNode(new_name(), node.incoming,
+ node.new | ({n.op.right} - node.old),
+ node.old | {n},
+ node.next)
+ return node2.expand(node1.expand(node_set))
+
+class UntilOp(BinaryOp):
+ def __init__(self, left, right):
+ super().__init__(left, right)
+
+ def normalize(self):
+ return self
+
+ def negate(self):
+ return VOp(self.left.negate(), self.right.negate())
+
+ def _is_temporal(self):
+ return True
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ node1 = GraphNode(new_name(), node.incoming,
+ node.new | ({n.op.left} - node.old),
+ node.old | {n},
+ node.next | {n})
+ node2 = GraphNode(new_name(), node.incoming,
+ node.new | ({n.op.right} - node.old),
+ node.old | {n},
+ node.next)
+ return node2.expand(node1.expand(node_set))
+
+class VOp(BinaryOp):
+ def __init__(self, left, right):
+ super().__init__(left, right)
+
+ def normalize(self):
+ return self
+
+ def negate(self):
+ return UntilOp(self.left.negate(), self.right.negate())
+
+ def _is_temporal(self):
+ return True
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ node1 = GraphNode(new_name(), node.incoming,
+ node.new | ({n.op.right} - node.old),
+ node.old | {n},
+ node.next | {n})
+ node2 = GraphNode(new_name(), node.incoming,
+ node.new | ({n.op.left, n.op.right} - node.old),
+ node.old | {n},
+ node.next)
+ return node2.expand(node1.expand(node_set))
+
+class ImplyOp(BinaryOp):
+ def __init__(self, left, right):
+ super().__init__(left, right)
+
+ def normalize(self):
+ # P -> Q === !P | Q
+ return OrOp(self.left.negate(), self.right)
+
+ def _is_temporal(self):
+ return False
+
+ def negate():
+ # !(P -> Q) === !(!P | Q) === P & !Q
+ return AndOp(self.left, self.right.negate())
+
+class UnaryOp:
+ def __init__(self, child: ASTNode):
+ self.child = child
+
+ def __iter__(self):
+ yield from self.child
+
+ def __hash__(self):
+ return hash(self.child)
+
+ def normalize(self):
+ raise NotImplemented
+
+ def _is_temporal(self):
+ raise NotImplemented
+
+ def is_temporal(self):
+ if self.child.op.is_temporal():
+ return True
+ return self._is_temporal()
+
+ def negate(self):
+ raise NotImplemented
+
+class EventuallyOp(UnaryOp):
+ def __init__(self, child):
+ super().__init__(child)
+
+ def __str__(self):
+ return "eventually " + str(self.child)
+
+ def normalize(self):
+ # <>F == true U F
+ return UntilOp(Literal(True), self.right)
+
+ def _is_temporal(self):
+ return True
+
+ def negate(self):
+ # !<>F == [](!F)
+ return AlwaysOp(self.right.negate()).normalize()
+
+class AlwaysOp(UnaryOp):
+ def __init__(self, child):
+ super().__init__(child)
+
+ def normalize(self):
+ #[]F === !(true U !F) == false V F
+ new = ASTNode(Literal(False))
+ return VOp(new, self.child)
+
+ def _is_temporal(self):
+ return True
+
+ def negate(self):
+ # ![]F == <>(!F)
+ return EventuallyOp(self.left, self.right.negate()).normalize()
+
+class NotOp(UnaryOp):
+ def __init__(self, child):
+ super().__init__(child)
+
+ def __str__(self):
+ return "!" + str(self.child)
+
+ def normalize(self):
+ return self.child.op.negate()
+
+ def negate(self):
+ return self.child.op
+
+ def _is_temporal(self):
+ return False
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ for f in node.old:
+ if n.op.child is f:
+ return node_set
+ node.old |= {n}
+ return node.expand(node_set)
+
+class Variable:
+ def __init__(self, name: str):
+ self.name = name
+
+ def __str__(self):
+ return "mon->atoms[%s]" % self.name
+
+ def __hash__(self):
+ return hash(self.name)
+
+ def __iter__(self):
+ yield from ()
+
+ def negate(self):
+ new = ASTNode(self)
+ return NotOp(new)
+
+ def normalize(self):
+ return self
+
+ def is_temporal(self):
+ return False
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ for f in node.old:
+ if isinstance(f, NotOp) and f.op.child is n:
+ return node_set
+ node.old |= {n}
+ return node.expand(node_set)
+
+class Literal:
+ def __init__(self, value: bool):
+ self.value = value
+
+ def __iter__(self):
+ yield from ()
+
+ def __hash__(self):
+ return hash(self.value)
+
+ def __str__(self):
+ if self.value:
+ return "true"
+ return "false"
+
+ def negate(self):
+ self.value = not self.value
+ return self
+
+ def normalize(self):
+ return self
+
+ def is_temporal(self):
+ return False
+
+ @staticmethod
+ def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
+ if not n.op.value:
+ return node_set
+ 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
+ | NOT ltl
+ '''
+ if p[1] == "always":
+ op = AlwaysOp(p[2])
+ if p[1] == "eventually":
+ op = EventuallyOp(p[2])
+ if p[1] == "not":
+ op = NotOp(p[2])
+
+ 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 ValueError("Invalid binary operator: %s" % p[2])
+
+ p[0] = ASTNode(op)
+
+parser = yacc()
+
+def parse_ltl(s: str) -> ASTNode:
+ spec = parser.parse(s)
+
+ for assign in spec:
+ if assign[0] == "RULE":
+ rule = assign[1]
+
+ for assign in spec:
+ if assign[0] == "RULE":
+ continue
+
+ subexpr = assign[0]
+ for node in rule:
+ if isinstance(node.op, Variable) and node.op.name == subexpr:
+ node.op = assign[1].op
+
+ return rule
+
+def create_graph(s: str):
+ atoms = set()
+
+ x = parse_ltl(s)
+ for c in x:
+ c.normalize()
+ if isinstance(c.op, Variable):
+ atoms.add(c.op.name)
+
+ init = GraphNode("init", set(), set(), set(), set())
+ head = GraphNode("first", {init}, {x}, set(), set())
+ graph = head.expand(set())
+
+ for node in graph:
+ for incoming in node.incoming:
+ if incoming.name == "init":
+ node.init = True
+ for o in node.old:
+ if not o.op.is_temporal():
+ node.labels.add(str(o))
+
+ return atoms, sorted(graph)
diff --git a/tools/verification/ltl2ba/template.c b/tools/verification/ltl2ba/template.c
new file mode 100644
index 000000000000..31c5a209d71d
--- /dev/null
+++ b/tools/verification/ltl2ba/template.c
@@ -0,0 +1,131 @@
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * This file is generated, do not edit.
+ */
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+#include <trace/events/task.h>
+#include <trace/events/sched.h>
+
+#include "ba.h"
+
+static_assert(NUM_ATOM <= RV_MAX_LTL_ATOM);
+
+enum buchi_state {
+ INIT,
+%%STATE_LIST%%
+ DEAD,
+};
+
+int rv_%%MODEL_NAME%%_task_slot = RV_PER_TASK_MONITOR_INIT;
+
+static void init_monitor(struct task_struct *task)
+{
+ struct ltl_monitor *mon = rv_%%MODEL_NAME%%_get_monitor(task);
+
+ for (int i = 0; i < NUM_ATOM; ++i)
+ mon->atoms[i] = LTL_UNDETERMINED;
+ mon->state = INIT;
+}
+
+static void handle_task_newtask(void *data, struct task_struct *task, unsigned long flags)
+{
+ struct ltl_monitor *mon = rv_%%MODEL_NAME%%_get_monitor(task);
+
+ init_monitor(task);
+
+ rv_%%MODEL_NAME%%_atoms_init(task, mon);
+ rv_%%MODEL_NAME%%_atoms_fetch(task, mon);
+}
+
+int rv_%%MODEL_NAME%%_init(size_t data_size)
+{
+ struct task_struct *g, *p;
+ int ret, cpu;
+
+ if (WARN_ON(data_size > RV_MAX_DATA_SIZE))
+ return -EINVAL;
+
+ ret = rv_get_task_monitor_slot();
+ if (ret < 0)
+ return ret;
+
+ rv_%%MODEL_NAME%%_task_slot = ret;
+
+ rv_attach_trace_probe("%%MODEL_NAME%%", task_newtask, handle_task_newtask);
+
+ read_lock(&tasklist_lock);
+
+ for_each_process_thread(g, p)
+ init_monitor(p);
+
+ for_each_present_cpu(cpu)
+ init_monitor(idle_task(cpu));
+
+ read_unlock(&tasklist_lock);
+
+ return 0;
+}
+
+void rv_%%MODEL_NAME%%_destroy(void)
+{
+ rv_put_task_monitor_slot(rv_%%MODEL_NAME%%_task_slot);
+ rv_%%MODEL_NAME%%_task_slot = RV_PER_TASK_MONITOR_INIT;
+
+ rv_detach_trace_probe("%%MODEL_NAME%%", task_newtask, handle_task_newtask);
+}
+
+static void illegal_state(struct task_struct *task, struct ltl_monitor *mon)
+{
+ mon->state = INIT;
+ rv_%%MODEL_NAME%%_error(task, mon);
+}
+
+static void rv_%%MODEL_NAME%%_attempt_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+ int i;
+
+ mon = rv_%%MODEL_NAME%%_get_monitor(task);
+
+ rv_%%MODEL_NAME%%_atoms_fetch(task, mon);
+
+ for (i = 0; i < NUM_ATOM; ++i) {
+ if (mon->atoms[i] == LTL_UNDETERMINED)
+ return;
+ }
+
+%%BUCHI_START%%
+}
+
+static void rv_%%MODEL_NAME%%_step(struct task_struct *task, struct ltl_monitor *mon)
+{
+ switch (mon->state) {
+%%BUCHI_TRANSITIONS%%
+ case DEAD:
+ case INIT:
+ break;
+ default:
+ WARN_ON_ONCE(1);
+ }
+}
+
+void rv_%%MODEL_NAME%%_atom_update(struct task_struct *task, unsigned int atom, bool value)
+{
+ struct ltl_monitor *mon = rv_%%MODEL_NAME%%_get_monitor(task);
+
+ rv_%%MODEL_NAME%%_atom_set(mon, atom, value);
+
+ if (mon->state == DEAD)
+ return;
+
+ if (mon->state == INIT)
+ rv_%%MODEL_NAME%%_attempt_start(task, mon);
+ if (mon->state == INIT)
+ return;
+
+ mon->atoms[atom] = value;
+
+ rv_%%MODEL_NAME%%_atoms_fetch(task, mon);
+
+ rv_%%MODEL_NAME%%_step(task, mon);
+}
diff --git a/tools/verification/ltl2ba/template.h b/tools/verification/ltl2ba/template.h
new file mode 100644
index 000000000000..65d342891e70
--- /dev/null
+++ b/tools/verification/ltl2ba/template.h
@@ -0,0 +1,157 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * This file is generated, do not edit.
+ *
+ * This file includes necessary functions to glue the Buchi automaton and the kernel together.
+ * Some of these functions must be manually implemented (look for "Must be implemented", or just
+ * let the compiler tells you).
+ *
+ * Essentially, you need to manually define the meaning of the atomic propositions in the LTL
+ * property. The primary function for that is rv_%%MODEL_NAME%%_atom_update(), which can be called
+ * in tracepoints' handlers for example. In some specific cases where
+ * rv_%%MODEL_NAME%%_atom_update() is not convenient, rv_%%MODEL_NAME%%_atoms_fetch() can be used.
+ *
+ * rv_%%MODEL_NAME%%_init()/rv_%%MODEL_NAME%%_destroy() must be called while enabling/disabling
+ * the monitor.
+ *
+ * If the fields in struct ltl_monitor is not enough, extra custom data can be used. See
+ * rv_%%MODEL_NAME%%_get_data().
+ */
+
+#include <linux/sched.h>
+
+enum %%MODEL_NAME%%_atom {
+%%ATOM_LIST%%
+ NUM_ATOM
+};
+
+/**
+ * rv_%%MODEL_NAME%%_init
+ * @data_size: required custom data size, can be zero
+ *
+ * Must be called while enabling the monitor
+ */
+int rv_%%MODEL_NAME%%_init(size_t data_size);
+
+/**
+ * rv_%%MODEL_NAME%%_destroy
+ *
+ * must be called while disabling the monitor
+ */
+void rv_%%MODEL_NAME%%_destroy(void);
+
+/**
+ * rv_%%MODEL_NAME%%_error - report violation of the LTL property
+ * @task: the task violating the LTL property
+ * @mon: the LTL monitor
+ *
+ * Must be implemented. This function should invoke the RV reactor and the monitor's tracepoints.
+ */
+void rv_%%MODEL_NAME%%_error(struct task_struct *task, struct ltl_monitor *mon);
+
+extern int rv_%%MODEL_NAME%%_task_slot;
+
+/**
+ * rv_%%MODEL_NAME%%_get_monitor - get the struct ltl_monitor of a task
+ */
+static inline struct ltl_monitor *rv_%%MODEL_NAME%%_get_monitor(struct task_struct *task)
+{
+ return &task->rv[rv_%%MODEL_NAME%%_task_slot].ltl_mon;
+}
+
+/**
+ * rv_%%MODEL_NAME%%_atoms_init - initialize the atomic propositions
+ * @task: the task
+ * @mon: the LTL monitor
+ *
+ * Must be implemented. This function is called during task creation, and should initialize all
+ * atomic propositions. rv_%%MODEL_NAME%%_atom_set() should be used to implement this function.
+ *
+ * This function does not have to initialize atomic propositions that are updated by
+ * rv_%%MODEL_NAME%%_atoms_fetch(), because the two functions are called together.
+ */
+void rv_%%MODEL_NAME%%_atoms_init(struct task_struct *task, struct ltl_monitor *mon);
+
+/**
+ * rv_%%MODEL_NAME%%_atoms_fetch - fetch the atomic propositions
+ * @task: the task
+ * @mon: the LTL monitor
+ *
+ * Must be implemented. This function is called anytime the Buchi automaton is triggered. Its
+ * intended purpose is to update the atomic propositions which are expensive to trace and can be
+ * easily read from @task. rv_%%MODEL_NAME%%_atom_set() should be used to implement this function.
+ *
+ * Using this function may cause incorrect verification result if it is important for the LTL that
+ * the atomic propositions must be updated at the correct time. Therefore, if it is possible,
+ * updating atomic propositions should be done with rv_%%MODEL_NAME%%_atom_update() instead.
+ *
+ * An example where this function is useful is with the LTL property:
+ * always (RT imply not PAGEFAULT)
+ * (a realtime task does not raise page faults)
+ *
+ * In this example, adding tracepoints to track RT is complicated, because it is changed in
+ * differrent places (mutex's priority boosting, sched_setscheduler). Furthermore, for this LTL
+ * property, we don't care exactly when RT changes, as long as we have its correct value when
+ * PAGEFAULT==true. Therefore, it is better to update RT in rv_%%MODEL_NAME%%_atoms_fetch(), as it
+ * can easily be retrieved from task_struct.
+ *
+ * This function can be empty.
+ */
+void rv_%%MODEL_NAME%%_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon);
+
+/**
+ * rv_%%MODEL_NAME%%_atom_update - update an atomic proposition
+ * @task: the task
+ * @atom: the atomic proposition, one of enum %%MODEL_NAME%%_atom
+ * @value: the new value for @atom
+ *
+ * Update an atomic proposition and trigger the Buchi atomaton to check for violation of the LTL
+ * property. This function can be called in tracepoints' handler, for example.
+ */
+void rv_%%MODEL_NAME%%_atom_update(struct task_struct *task, unsigned int atom, bool value);
+
+/**
+ * rv_%%MODEL_NAME%%_atom_get - get an atomic proposition
+ * @mon: the monitor
+ * @atom: the atomic proposition, one of enum %%MODEL_NAME%%_atom
+ *
+ * Returns the value of an atomic proposition.
+ */
+static inline
+enum ltl_truth_value rv_%%MODEL_NAME%%_atom_get(struct ltl_monitor *mon, unsigned int atom)
+{
+ return mon->atoms[atom];
+}
+
+/**
+ * rv_%%MODEL_NAME%%_atom_set - set an atomic proposition
+ * @mon: the monitor
+ * @atom: the atomic proposition, one of enum %%MODEL_NAME%%_atom
+ * @value: the new value for @atom
+ *
+ * Update an atomic proposition without triggering the Buchi automaton. This can be useful to
+ * implement rv_%%MODEL_NAME%%_atoms_fetch() and rv_%%MODEL_NAME%%_atoms_init().
+ *
+ * Another use case for this function is when multiple atomic propositions change at the same time,
+ * because calling rv_%%MODEL_NAME%%_atom_update() (and thus triggering the Buchi automaton)
+ * multiple times may be incorrect. In that case, rv_%%MODEL_NAME%%_atom_set() can be used to avoid
+ * triggering the Buchi automaton, and rv_%%MODEL_NAME%%_atom_update() is only used for the last
+ * atomic proposition.
+ */
+static inline
+void rv_%%MODEL_NAME%%_atom_set(struct ltl_monitor *mon, unsigned int atom, bool value)
+{
+ mon->atoms[atom] = value;
+}
+
+/**
+ * rv_%%MODEL_NAME%%_get_data - get the custom data of this monitor.
+ * @mon: the monitor
+ *
+ * If this function is used, rv_%%MODEL_NAME%%_init() must have been called with a positive
+ * data_size.
+ */
+static inline void *rv_%%MODEL_NAME%%_get_data(struct ltl_monitor *mon)
+{
+ return &mon->data;
+}
--
2.39.5
^ permalink raw reply related [flat|nested] 23+ messages in thread* Re: [PATCH 03/10] rv: Add infrastructure for linear temporal logic monitor
2025-03-11 17:05 ` [PATCH 03/10] rv: Add infrastructure for linear temporal logic monitor Nam Cao
@ 2025-03-12 6:47 ` Gabriele Monaco
2025-03-12 9:56 ` Steven Rostedt
2025-03-12 14:29 ` Nam Cao
0 siblings, 2 replies; 23+ messages in thread
From: Gabriele Monaco @ 2025-03-12 6:47 UTC (permalink / raw)
To: Nam Cao, Steven Rostedt, john.ogness, linux-trace-kernel,
linux-kernel
On Tue, 2025-03-11 at 18:05 +0100, Nam Cao wrote:
> Prepare the infrastructure for linear temporal logic monitors:
>
> - add scripts for generating the monitors
> - implement data structures
>
> For details, see:
> Documentation/trace/rv/linear_temporal_logic.rst
>
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
Thanks for this. It's great to have a new type of monitor!
I'll play with this a bit more, but please see my initial comments.
> .../trace/rv/linear_temporal_logic.rst | 73 +++
> include/linux/rv.h | 26 +-
> kernel/fork.c | 5 +-
> tools/verification/ltl2ba/.gitignore | 3 +
> tools/verification/ltl2ba/generate.py | 154 +++++
> tools/verification/ltl2ba/ltl.py | 556
> ++++++++++++++++++
> tools/verification/ltl2ba/template.c | 131 +++++
> tools/verification/ltl2ba/template.h | 157 +++++
> 8 files changed, 1097 insertions(+), 8 deletions(-)
> create mode 100644 Documentation/trace/rv/linear_temporal_logic.rst
> create mode 100644 tools/verification/ltl2ba/.gitignore
> create mode 100755 tools/verification/ltl2ba/generate.py
> create mode 100644 tools/verification/ltl2ba/ltl.py
> create mode 100644 tools/verification/ltl2ba/template.c
> create mode 100644 tools/verification/ltl2ba/template.h
>
> diff --git a/Documentation/trace/rv/linear_temporal_logic.rst
> b/Documentation/trace/rv/linear_temporal_logic.rst
> new file mode 100644
> index 000000000000..9b0ce6a143ec
> --- /dev/null
> +++ b/Documentation/trace/rv/linear_temporal_logic.rst
> [...]
>
> diff --git a/include/linux/rv.h b/include/linux/rv.h
> index 5482651ed020..6de4f93b390e 100644
> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -10,6 +10,8 @@
> #define MAX_DA_NAME_LEN 24
>
> #ifdef CONFIG_RV
> +#include <linux/types.h>
> +
> /*
> * Deterministic automaton per-object variables.
> */
> @@ -18,6 +20,24 @@ struct da_monitor {
> unsigned int curr_state;
> };
>
> +enum ltl_truth_value {
> + LTL_FALSE,
> + LTL_TRUE,
> + LTL_UNDETERMINED,
> +};
> +
> +/*
> + * In the future, if the number of atomic propositions or the custom
> data size is larger, we can
> + * switch to dynamic allocation. For now, the code is simpler this
> way.
> + */
> +#define RV_MAX_LTL_ATOM 10
> +#define RV_MAX_DATA_SIZE 16
> +struct ltl_monitor {
> + unsigned int state;
> + enum ltl_truth_value atoms[RV_MAX_LTL_ATOM];
> + u8 data[RV_MAX_DATA_SIZE];
> +};
> +
> /*
> * 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 +47,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;
> };
This adds quite some memory overhead if we have multiple per-task
monitors (we might in the future) and we don't use this ltl monitors.
What about keeping it conditionally compiled out?
You could define the struct only if e.g. CONFIG_RV_LTL_MONITORS is set,
select it with any LTL monitor via Kconfig, then glue it somehow to
have it readable.
>
> #ifdef CONFIG_RV_REACTORS
> diff --git a/kernel/fork.c b/kernel/fork.c
> index 735405a9c5f3..5d6c1caca702 100644
> --- a/kernel/fork.c
> +++ b/kernel/fork.c
> @@ -2127,10 +2127,7 @@ static void copy_oom_score_adj(u64
> clone_flags, struct task_struct *tsk)
> #ifdef CONFIG_RV
> static void rv_task_fork(struct task_struct *p)
> {
> - int i;
> -
> - for (i = 0; i < RV_PER_TASK_MONITORS; i++)
> - p->rv[i].da_mon.monitoring = false;
> + memset(p->rv, 0, sizeof(p->rv));
> }
> #else
> #define rv_task_fork(p) do {} while (0)
> diff --git a/tools/verification/ltl2ba/.gitignore
> b/tools/verification/ltl2ba/.gitignore
> new file mode 100644
> index 000000000000..9c47b9724860
> --- /dev/null
> +++ b/tools/verification/ltl2ba/.gitignore
> @@ -0,0 +1,3 @@
> +__pycache__/
> +parsetab.py
> +parser.out
> diff --git a/tools/verification/ltl2ba/generate.py
> b/tools/verification/ltl2ba/generate.py
> new file mode 100755
> index 000000000000..52d5b3618e64
> --- /dev/null
> +++ b/tools/verification/ltl2ba/generate.py
You may want to rename this script to something more unique, just in
case one day we decide to make it possible to install this generator on
the system (like dot2k/dot2c).
>
> diff --git a/tools/verification/ltl2ba/ltl.py
> b/tools/verification/ltl2ba/ltl.py
> new file mode 100644
> index 000000000000..aa3a11d78a8e
> --- /dev/null
> +++ b/tools/verification/ltl2ba/ltl.py
>
> diff --git a/tools/verification/ltl2ba/template.c
> b/tools/verification/ltl2ba/template.c
> new file mode 100644
> index 000000000000..31c5a209d71d
> --- /dev/null
> +++ b/tools/verification/ltl2ba/template.c
> diff --git a/tools/verification/ltl2ba/template.h
> b/tools/verification/ltl2ba/template.h
> new file mode 100644
> index 000000000000..65d342891e70
> --- /dev/null
> +++ b/tools/verification/ltl2ba/template.h
> @@ -0,0 +1,157 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/*
> + * This file is generated, do not edit.
> + *
> + * This file includes necessary functions to glue the Buchi
> automaton and the kernel together.
> + * Some of these functions must be manually implemented (look for
> "Must be implemented", or just
> + * let the compiler tells you).
> + *
> + * Essentially, you need to manually define the meaning of the
> atomic propositions in the LTL
> + * property. The primary function for that is
> rv_%%MODEL_NAME%%_atom_update(), which can be called
> + * in tracepoints' handlers for example. In some specific cases
> where
> + * rv_%%MODEL_NAME%%_atom_update() is not convenient,
> rv_%%MODEL_NAME%%_atoms_fetch() can be used.
> + *
> + * rv_%%MODEL_NAME%%_init()/rv_%%MODEL_NAME%%_destroy() must be
> called while enabling/disabling
> + * the monitor.
> + *
> + * If the fields in struct ltl_monitor is not enough, extra custom
> data can be used. See
> + * rv_%%MODEL_NAME%%_get_data().
> + */
> +
> +#include <linux/sched.h>
> +
> +enum %%MODEL_NAME%%_atom {
> +%%ATOM_LIST%%
> + NUM_ATOM
> +};
> +
> +/**
> + * rv_%%MODEL_NAME%%_init
> + * @data_size: required custom data size, can be zero
> + *
> + * Must be called while enabling the monitor
> + */
> +int rv_%%MODEL_NAME%%_init(size_t data_size);
> +
> +/**
> + * rv_%%MODEL_NAME%%_destroy
> + *
> + * must be called while disabling the monitor
> + */
> +void rv_%%MODEL_NAME%%_destroy(void);
> +
> +/**
> + * rv_%%MODEL_NAME%%_error - report violation of the LTL property
> + * @task: the task violating the LTL property
> + * @mon: the LTL monitor
> + *
> + * Must be implemented. This function should invoke the RV reactor
> and the monitor's tracepoints.
> + */
> +void rv_%%MODEL_NAME%%_error(struct task_struct *task, struct
> ltl_monitor *mon);
> +
> +extern int rv_%%MODEL_NAME%%_task_slot;
> +
> +/**
> + * rv_%%MODEL_NAME%%_get_monitor - get the struct ltl_monitor of a
> task
> + */
> +static inline struct ltl_monitor
> *rv_%%MODEL_NAME%%_get_monitor(struct task_struct *task)
> +{
> + return &task->rv[rv_%%MODEL_NAME%%_task_slot].ltl_mon;
> +}
> +
> +/**
> + * rv_%%MODEL_NAME%%_atoms_init - initialize the atomic propositions
> + * @task: the task
> + * @mon: the LTL monitor
> + *
> + * Must be implemented. This function is called during task
> creation, and should initialize all
> + * atomic propositions. rv_%%MODEL_NAME%%_atom_set() should be used
> to implement this function.
> + *
> + * This function does not have to initialize atomic propositions
> that are updated by
> + * rv_%%MODEL_NAME%%_atoms_fetch(), because the two functions are
> called together.
> + */
> +void rv_%%MODEL_NAME%%_atoms_init(struct task_struct *task, struct
> ltl_monitor *mon);
> +
> +/**
> + * rv_%%MODEL_NAME%%_atoms_fetch - fetch the atomic propositions
> + * @task: the task
> + * @mon: the LTL monitor
> + *
> + * Must be implemented. This function is called anytime the Buchi
> automaton is triggered. Its
> + * intended purpose is to update the atomic propositions which are
> expensive to trace and can be
> + * easily read from @task. rv_%%MODEL_NAME%%_atom_set() should be
> used to implement this function.
> + *
> + * Using this function may cause incorrect verification result if it
> is important for the LTL that
> + * the atomic propositions must be updated at the correct time.
> Therefore, if it is possible,
> + * updating atomic propositions should be done with
> rv_%%MODEL_NAME%%_atom_update() instead.
> + *
> + * An example where this function is useful is with the LTL
> property:
> + * always (RT imply not PAGEFAULT)
> + * (a realtime task does not raise page faults)
> + *
> + * In this example, adding tracepoints to track RT is complicated,
> because it is changed in
> + * differrent places (mutex's priority boosting,
> sched_setscheduler). Furthermore, for this LTL
> + * property, we don't care exactly when RT changes, as long as we
> have its correct value when
> + * PAGEFAULT==true. Therefore, it is better to update RT in
> rv_%%MODEL_NAME%%_atoms_fetch(), as it
> + * can easily be retrieved from task_struct.
> + *
> + * This function can be empty.
> + */
> +void rv_%%MODEL_NAME%%_atoms_fetch(struct task_struct *task, struct
> ltl_monitor *mon);
> +
> +/**
> + * rv_%%MODEL_NAME%%_atom_update - update an atomic proposition
> + * @task: the task
> + * @atom: the atomic proposition, one of enum
> %%MODEL_NAME%%_atom
> + * @value: the new value for @atom
> + *
> + * Update an atomic proposition and trigger the Buchi atomaton to
> check for violation of the LTL
> + * property. This function can be called in tracepoints' handler,
> for example.
> + */
> +void rv_%%MODEL_NAME%%_atom_update(struct task_struct *task,
> unsigned int atom, bool value);
> +
> +/**
> + * rv_%%MODEL_NAME%%_atom_get - get an atomic proposition
> + * @mon: the monitor
> + * @atom: the atomic proposition, one of enum
> %%MODEL_NAME%%_atom
> + *
> + * Returns the value of an atomic proposition.
> + */
> +static inline
> +enum ltl_truth_value rv_%%MODEL_NAME%%_atom_get(struct ltl_monitor
> *mon, unsigned int atom)
> +{
> + return mon->atoms[atom];
> +}
> +
> +/**
> + * rv_%%MODEL_NAME%%_atom_set - set an atomic proposition
> + * @mon: the monitor
> + * @atom: the atomic proposition, one of enum
> %%MODEL_NAME%%_atom
> + * @value: the new value for @atom
> + *
> + * Update an atomic proposition without triggering the Buchi
> automaton. This can be useful to
> + * implement rv_%%MODEL_NAME%%_atoms_fetch() and
> rv_%%MODEL_NAME%%_atoms_init().
> + *
> + * Another use case for this function is when multiple atomic
> propositions change at the same time,
> + * because calling rv_%%MODEL_NAME%%_atom_update() (and thus
> triggering the Buchi automaton)
> + * multiple times may be incorrect. In that case,
> rv_%%MODEL_NAME%%_atom_set() can be used to avoid
> + * triggering the Buchi automaton, and
> rv_%%MODEL_NAME%%_atom_update() is only used for the last
> + * atomic proposition.
> + */
> +static inline
> +void rv_%%MODEL_NAME%%_atom_set(struct ltl_monitor *mon, unsigned
> int atom, bool value)
> +{
> + mon->atoms[atom] = value;
> +}
> +
> +/**
> + * rv_%%MODEL_NAME%%_get_data - get the custom data of this monitor.
> + * @mon: the monitor
> + *
> + * If this function is used, rv_%%MODEL_NAME%%_init() must have been
> called with a positive
> + * data_size.
> + */
> +static inline void *rv_%%MODEL_NAME%%_get_data(struct ltl_monitor
> *mon)
> +{
> + return &mon->data;
> +}
Do we need all those functions defined here? We could have them
generated by the pre-processor just like with DA monitors.
Having a ltl_monitor.h defining all common utility functions and
variables (here I'm assuming most are, indeed, common) may save a lot
of maintenance.
Also I would rearrange monitors sources a bit differently, like putting
everything that doesn't need manual intervention (states and atoms
lists) in the header, remaining functions that may need tracepoint
wiring or more complex stuff can stay in a single c file, a bit like
current da monitors.
I see there seems to be more manual work in the main C file (e.g.
rtapp_block.c), but I think it would look cleaner if all other code was
generated by the preprocessor in a common header and all lists/inlined
functions created by the script stay in a separate header (why not call
it rtapp_block.h?).
What do you think?
Thanks,
Gabriele
^ permalink raw reply [flat|nested] 23+ messages in thread* Re: [PATCH 03/10] rv: Add infrastructure for linear temporal logic monitor
2025-03-12 6:47 ` Gabriele Monaco
@ 2025-03-12 9:56 ` Steven Rostedt
2025-03-12 14:29 ` Nam Cao
1 sibling, 0 replies; 23+ messages in thread
From: Steven Rostedt @ 2025-03-12 9:56 UTC (permalink / raw)
To: Gabriele Monaco; +Cc: Nam Cao, john.ogness, linux-trace-kernel, linux-kernel
On Wed, 12 Mar 2025 07:47:50 +0100
Gabriele Monaco <gmonaco@redhat.com> wrote:
> -/*
> > - * 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;
> > };
>
> This adds quite some memory overhead if we have multiple per-task
> monitors (we might in the future) and we don't use this ltl monitors.
> What about keeping it conditionally compiled out?
> You could define the struct only if e.g. CONFIG_RV_LTL_MONITORS is set,
> select it with any LTL monitor via Kconfig, then glue it somehow to
> have it readable.
One thing to do if you compile it out, make it a stub structure, so you
don't need to add #ifdef into the union.
struct ltl_monitor { int unused; };
Or something like that.
-- Steve
^ permalink raw reply [flat|nested] 23+ messages in thread* Re: [PATCH 03/10] rv: Add infrastructure for linear temporal logic monitor
2025-03-12 6:47 ` Gabriele Monaco
2025-03-12 9:56 ` Steven Rostedt
@ 2025-03-12 14:29 ` Nam Cao
1 sibling, 0 replies; 23+ messages in thread
From: Nam Cao @ 2025-03-12 14:29 UTC (permalink / raw)
To: Gabriele Monaco
Cc: Steven Rostedt, john.ogness, linux-trace-kernel, linux-kernel
On Wed, Mar 12, 2025 at 07:47:50AM +0100, Gabriele Monaco wrote:
> On Tue, 2025-03-11 at 18:05 +0100, Nam Cao wrote:
> > -/*
> > - * 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;
> > };
>
> This adds quite some memory overhead if we have multiple per-task
> monitors (we might in the future) and we don't use this ltl monitors.
> What about keeping it conditionally compiled out?
> You could define the struct only if e.g. CONFIG_RV_LTL_MONITORS is set,
> select it with any LTL monitor via Kconfig, then glue it somehow to
> have it readable.
Good point.
> > diff --git a/tools/verification/ltl2ba/generate.py
> > b/tools/verification/ltl2ba/generate.py
> > new file mode 100755
> > index 000000000000..52d5b3618e64
> > --- /dev/null
> > +++ b/tools/verification/ltl2ba/generate.py
>
> You may want to rename this script to something more unique, just in
> case one day we decide to make it possible to install this generator on
> the system (like dot2k/dot2c).
Acked. Inspired by the dot2k name, maybe something like ltl2k.
> > + * rv_%%MODEL_NAME%%_get_data - get the custom data of this monitor.
> > + * @mon: the monitor
> > + *
> > + * If this function is used, rv_%%MODEL_NAME%%_init() must have been
> > called with a positive
> > + * data_size.
> > + */
> > +static inline void *rv_%%MODEL_NAME%%_get_data(struct ltl_monitor
> > *mon)
> > +{
> > + return &mon->data;
> > +}
>
> Do we need all those functions defined here? We could have them
> generated by the pre-processor just like with DA monitors.
>
> Having a ltl_monitor.h defining all common utility functions and
> variables (here I'm assuming most are, indeed, common) may save a lot
> of maintenance.
I avoided macros like with DA monitors, they are hard to grep. But your
point on maintenance is true from my experience working on this series..
Pre-processor it is then.
> Also I would rearrange monitors sources a bit differently, like putting
> everything that doesn't need manual intervention (states and atoms
> lists) in the header, remaining functions that may need tracepoint
> wiring or more complex stuff can stay in a single c file, a bit like
> current da monitors.
>
> I see there seems to be more manual work in the main C file (e.g.
> rtapp_block.c), but I think it would look cleaner if all other code was
> generated by the preprocessor in a common header and all lists/inlined
> functions created by the script stay in a separate header (why not call
> it rtapp_block.h?).
>
> What do you think?
Sounds better, let me give me a try.
Thanks so much for the suggestions,
Nam
^ permalink raw reply [flat|nested] 23+ messages in thread
* [PATCH 04/10] rv: Add rtapp_block monitor
2025-03-11 17:05 [PATCH 00/10] RV: Linear temporal logic monitors for RT application Nam Cao
` (2 preceding siblings ...)
2025-03-11 17:05 ` [PATCH 03/10] rv: Add infrastructure for linear temporal logic monitor Nam Cao
@ 2025-03-11 17:05 ` Nam Cao
2025-03-12 7:34 ` Gabriele Monaco
2025-03-13 15:15 ` kernel test robot
2025-03-11 17:05 ` [PATCH 05/10] x86/tracing: Remove redundant trace_pagefault_key Nam Cao
` (5 subsequent siblings)
9 siblings, 2 replies; 23+ messages in thread
From: Nam Cao @ 2025-03-11 17:05 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, john.ogness, linux-trace-kernel,
linux-kernel
Cc: Nam Cao, Peter Zijlstra, Ingo Molnar, Will Deacon, Boqun Feng,
Waiman Long
Add an RV monitor to detect realtime tasks getting blocked. For the full
description, see Documentation/trace/rv/monitor_rtapp_block.rst.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Will Deacon <will@kernel.org>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Waiman Long <longman@redhat.com>
---
.../trace/rv/monitor_rtapp_block.rst | 34 +++
include/trace/events/lock.h | 12 +
kernel/locking/rtmutex.c | 4 +
kernel/trace/rv/Kconfig | 12 +-
kernel/trace/rv/Makefile | 2 +
kernel/trace/rv/monitors/rtapp_block/ba.c | 146 +++++++++++
kernel/trace/rv/monitors/rtapp_block/ba.h | 166 +++++++++++++
kernel/trace/rv/monitors/rtapp_block/ltl | 9 +
.../rv/monitors/rtapp_block/rtapp_block.c | 232 ++++++++++++++++++
kernel/trace/rv/rv_trace.h | 44 ++++
lib/Kconfig.debug | 3 +
11 files changed, 663 insertions(+), 1 deletion(-)
create mode 100644 Documentation/trace/rv/monitor_rtapp_block.rst
create mode 100644 kernel/trace/rv/monitors/rtapp_block/ba.c
create mode 100644 kernel/trace/rv/monitors/rtapp_block/ba.h
create mode 100644 kernel/trace/rv/monitors/rtapp_block/ltl
create mode 100644 kernel/trace/rv/monitors/rtapp_block/rtapp_block.c
diff --git a/Documentation/trace/rv/monitor_rtapp_block.rst b/Documentation/trace/rv/monitor_rtapp_block.rst
new file mode 100644
index 000000000000..9cabbe66fa4a
--- /dev/null
+++ b/Documentation/trace/rv/monitor_rtapp_block.rst
@@ -0,0 +1,34 @@
+Monitor rtapp_block
+=======================
+
+- Name: rtapp_block - real time applications are undesirably blocked
+- Type: per-task linear temporal logic monitor
+- Author: Nam Cao <namcao@linutronix.de>
+
+Introduction
+------------
+
+Real time threads could be blocked and fail to finish their execution timely. For instance, they
+need to access shared resources which are already acquired by other threads. Or they could be
+waiting for non-realtime threads to signal them to proceed: as the non-realtime threads are not
+prioritized by the scheduler, the execution of realtime threads could be delayed indefinitely.
+These scenarios are often unintentional, and cause unexpected latency to the realtime application.
+
+The rtapp_block monitor reports this type of scenario, by monitoring for:
+
+ * Realtime threads going to sleep without explicitly asking for it (namely, with nanosleep
+ syscall).
+ * Realtime threads are woken up by non-realtime threads.
+
+How to fix the monitor's warnings?
+----------------------------------
+
+There is no single answer, the solution needs to be evaluated depending on the specific cases.
+
+If the realtime thread is blocked trying to take a `pthread_mutex_t` which is already taken by a
+non-realtime thread, the solution could be enabling priority inheritance for the mutex, so that the
+blocking non-realtime thread would be priority-boosted to run at realtime priority.
+
+If realtime thread needs to wait for non-realtime thread to signal it to proceed, perhaps the design
+needs to be reconsidered to remove this dependency. Often, the work executed by the realtime thread
+needs not to be realtime at all.
diff --git a/include/trace/events/lock.h b/include/trace/events/lock.h
index 8e89baa3775f..d4b32194d47f 100644
--- a/include/trace/events/lock.h
+++ b/include/trace/events/lock.h
@@ -138,6 +138,18 @@ TRACE_EVENT(contention_end,
TP_printk("%p (ret=%d)", __entry->lock_addr, __entry->ret)
);
+#ifdef CONFIG_TRACE_RT_MUTEX_WAKE_WAITER
+DECLARE_TRACE(rt_mutex_wake_waiter_begin,
+ TP_PROTO(struct task_struct *task),
+ TP_ARGS(task))
+DECLARE_TRACE(rt_mutex_wake_waiter_end,
+ TP_PROTO(struct task_struct *task),
+ TP_ARGS(task))
+#else
+#define trace_rt_mutex_wake_waiter_begin(...)
+#define trace_rt_mutex_wake_waiter_end(...)
+#endif /* CONFIG_TRACE_RT_MUTEX */
+
#endif /* _TRACE_LOCK_H */
/* This part must be outside protection */
diff --git a/kernel/locking/rtmutex.c b/kernel/locking/rtmutex.c
index 4a8df1800cbb..fc9cf4a2cf75 100644
--- a/kernel/locking/rtmutex.c
+++ b/kernel/locking/rtmutex.c
@@ -561,6 +561,8 @@ static __always_inline void rt_mutex_wake_q_add(struct rt_wake_q_head *wqh,
static __always_inline void rt_mutex_wake_up_q(struct rt_wake_q_head *wqh)
{
+ trace_rt_mutex_wake_waiter_begin(current);
+
if (IS_ENABLED(CONFIG_PREEMPT_RT) && wqh->rtlock_task) {
wake_up_state(wqh->rtlock_task, TASK_RTLOCK_WAIT);
put_task_struct(wqh->rtlock_task);
@@ -572,6 +574,8 @@ static __always_inline void rt_mutex_wake_up_q(struct rt_wake_q_head *wqh)
/* Pairs with preempt_disable() in mark_wakeup_next_waiter() */
preempt_enable();
+
+ trace_rt_mutex_wake_waiter_end(current);
}
/*
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 8226352a0062..d65bf9bda2f2 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -13,7 +13,7 @@ config DA_MON_EVENTS_ID
menuconfig RV
bool "Runtime Verification"
- depends on TRACING
+ select TRACING
help
Enable the kernel runtime verification infrastructure. RV is a
lightweight (yet rigorous) method that complements classical
@@ -29,6 +29,16 @@ source "kernel/trace/rv/monitors/wip/Kconfig"
source "kernel/trace/rv/monitors/wwnr/Kconfig"
# Add new monitors here
+config RV_MON_RTAPP_BLOCK
+ depends on RV
+ select DA_MON_EVENTS
+ select TRACE_IRQFLAGS
+ select TRACE_RT_MUTEX_WAKE_WAITER
+ bool "rtapp_block monitor"
+ help
+ Enable rtapp_wakeup which monitors that realtime tasks are not blocked.
+ For details, see Documentation/trace/rv/monitor_rtapp_block.rst.
+
config RV_REACTORS
bool "Runtime verification reactors"
default y
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index 188b64668e1f..6570a3116127 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -5,6 +5,8 @@ ccflags-y += -I $(src) # needed for trace events
obj-$(CONFIG_RV) += rv.o
obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o
obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o
+obj-$(CONFIG_RV_MON_RTAPP_BLOCK) += monitors/rtapp_block/ba.o \
+ monitors/rtapp_block/rtapp_block.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_block/ba.c b/kernel/trace/rv/monitors/rtapp_block/ba.c
new file mode 100644
index 000000000000..5e99f79d5e74
--- /dev/null
+++ b/kernel/trace/rv/monitors/rtapp_block/ba.c
@@ -0,0 +1,146 @@
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * This file is generated, do not edit.
+ */
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+#include <trace/events/task.h>
+#include <trace/events/sched.h>
+
+#include "ba.h"
+
+static_assert(NUM_ATOM <= RV_MAX_LTL_ATOM);
+
+enum buchi_state {
+ INIT,
+ S3,
+ DEAD,
+};
+
+int rv_rtapp_block_task_slot = RV_PER_TASK_MONITOR_INIT;
+
+static void init_monitor(struct task_struct *task)
+{
+ struct ltl_monitor *mon = rv_rtapp_block_get_monitor(task);
+
+ for (int i = 0; i < NUM_ATOM; ++i)
+ mon->atoms[i] = LTL_UNDETERMINED;
+ mon->state = INIT;
+}
+
+static void handle_task_newtask(void *data, struct task_struct *task, unsigned long flags)
+{
+ struct ltl_monitor *mon = rv_rtapp_block_get_monitor(task);
+
+ init_monitor(task);
+
+ rv_rtapp_block_atoms_init(task, mon);
+ rv_rtapp_block_atoms_fetch(task, mon);
+}
+
+int rv_rtapp_block_init(size_t data_size)
+{
+ struct task_struct *g, *p;
+ int ret, cpu;
+
+ if (WARN_ON(data_size > RV_MAX_DATA_SIZE))
+ return -EINVAL;
+
+ ret = rv_get_task_monitor_slot();
+ if (ret < 0)
+ return ret;
+
+ rv_rtapp_block_task_slot = ret;
+
+ rv_attach_trace_probe("rtapp_block", task_newtask, handle_task_newtask);
+
+ read_lock(&tasklist_lock);
+
+ for_each_process_thread(g, p)
+ init_monitor(p);
+
+ for_each_present_cpu(cpu)
+ init_monitor(idle_task(cpu));
+
+ read_unlock(&tasklist_lock);
+
+ return 0;
+}
+
+void rv_rtapp_block_destroy(void)
+{
+ rv_put_task_monitor_slot(rv_rtapp_block_task_slot);
+ rv_rtapp_block_task_slot = RV_PER_TASK_MONITOR_INIT;
+
+ rv_detach_trace_probe("rtapp_block", task_newtask, handle_task_newtask);
+}
+
+static void illegal_state(struct task_struct *task, struct ltl_monitor *mon)
+{
+ mon->state = INIT;
+ rv_rtapp_block_error(task, mon);
+}
+
+static void rv_rtapp_block_attempt_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+ int i;
+
+ mon = rv_rtapp_block_get_monitor(task);
+
+ rv_rtapp_block_atoms_fetch(task, mon);
+
+ for (i = 0; i < NUM_ATOM; ++i) {
+ if (mon->atoms[i] == LTL_UNDETERMINED)
+ return;
+ }
+
+ if (((!mon->atoms[WAKEUP_RT_TASK] || (mon->atoms[RT] || (mon->atoms[RT_MUTEX_WAKING_WAITER]
+ || (mon->atoms[STOPPING_WOKEN_TASK] || (mon->atoms[WOKEN_TASK_IS_MIGRATION] ||
+ mon->atoms[WOKEN_TASK_IS_RCU])))))) && (((!mon->atoms[USER_TASK] || !mon->atoms[RT]) ||
+ (!mon->atoms[SLEEP] || (mon->atoms[DO_NANOSLEEP] || mon->atoms[FUTEX_LOCK_WITH_PI])))))
+ mon->state = S3;
+ else
+ illegal_state(task, mon);
+}
+
+static void rv_rtapp_block_step(struct task_struct *task, struct ltl_monitor *mon)
+{
+ switch (mon->state) {
+ case S3:
+ if (((!mon->atoms[WAKEUP_RT_TASK] || (mon->atoms[RT] ||
+ (mon->atoms[RT_MUTEX_WAKING_WAITER] || (mon->atoms[STOPPING_WOKEN_TASK] ||
+ (mon->atoms[WOKEN_TASK_IS_MIGRATION] || mon->atoms[WOKEN_TASK_IS_RCU])))))) &&
+ (((!mon->atoms[USER_TASK] || !mon->atoms[RT]) || (!mon->atoms[SLEEP] ||
+ (mon->atoms[DO_NANOSLEEP] || mon->atoms[FUTEX_LOCK_WITH_PI])))))
+ mon->state = S3;
+ else
+ illegal_state(task, mon);
+ break;
+ case DEAD:
+ case INIT:
+ break;
+ default:
+ WARN_ON_ONCE(1);
+ }
+}
+
+void rv_rtapp_block_atom_update(struct task_struct *task, unsigned int atom, bool value)
+{
+ struct ltl_monitor *mon = rv_rtapp_block_get_monitor(task);
+
+ rv_rtapp_block_atom_set(mon, atom, value);
+
+ if (mon->state == DEAD)
+ return;
+
+ if (mon->state == INIT)
+ rv_rtapp_block_attempt_start(task, mon);
+ if (mon->state == INIT)
+ return;
+
+ mon->atoms[atom] = value;
+
+ rv_rtapp_block_atoms_fetch(task, mon);
+
+ rv_rtapp_block_step(task, mon);
+}
diff --git a/kernel/trace/rv/monitors/rtapp_block/ba.h b/kernel/trace/rv/monitors/rtapp_block/ba.h
new file mode 100644
index 000000000000..c1ba88f6779a
--- /dev/null
+++ b/kernel/trace/rv/monitors/rtapp_block/ba.h
@@ -0,0 +1,166 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * This file is generated, do not edit.
+ *
+ * This file includes necessary functions to glue the Buchi automaton and the kernel together.
+ * Some of these functions must be manually implemented (look for "Must be implemented", or just
+ * let the compiler tells you).
+ *
+ * Essentially, you need to manually define the meaning of the atomic propositions in the LTL
+ * property. The primary function for that is rv_rtapp_block_atom_update(), which can be called
+ * in tracepoints' handlers for example. In some specific cases where
+ * rv_rtapp_block_atom_update() is not convenient, rv_rtapp_block_atoms_fetch() can be used.
+ *
+ * rv_rtapp_block_init()/rv_rtapp_block_destroy() must be called while enabling/disabling
+ * the monitor.
+ *
+ * If the fields in struct ltl_monitor is not enough, extra custom data can be used. See
+ * rv_rtapp_block_get_data().
+ */
+
+#include <linux/sched.h>
+
+enum rtapp_block_atom {
+ DO_NANOSLEEP,
+ FUTEX_LOCK_WITH_PI,
+ RT,
+ RT_MUTEX_WAKING_WAITER,
+ SLEEP,
+ STOPPING_WOKEN_TASK,
+ USER_TASK,
+ WAKEUP_RT_TASK,
+ WOKEN_TASK_IS_MIGRATION,
+ WOKEN_TASK_IS_RCU,
+ NUM_ATOM
+};
+
+/**
+ * rv_rtapp_block_init
+ * @data_size: required custom data size, can be zero
+ *
+ * Must be called while enabling the monitor
+ */
+int rv_rtapp_block_init(size_t data_size);
+
+/**
+ * rv_rtapp_block_destroy
+ *
+ * must be called while disabling the monitor
+ */
+void rv_rtapp_block_destroy(void);
+
+/**
+ * rv_rtapp_block_error - report violation of the LTL property
+ * @task: the task violating the LTL property
+ * @mon: the LTL monitor
+ *
+ * Must be implemented. This function should invoke the RV reactor and the monitor's tracepoints.
+ */
+void rv_rtapp_block_error(struct task_struct *task, struct ltl_monitor *mon);
+
+extern int rv_rtapp_block_task_slot;
+
+/**
+ * rv_rtapp_block_get_monitor - get the struct ltl_monitor of a task
+ */
+static inline struct ltl_monitor *rv_rtapp_block_get_monitor(struct task_struct *task)
+{
+ return &task->rv[rv_rtapp_block_task_slot].ltl_mon;
+}
+
+/**
+ * rv_rtapp_block_atoms_init - initialize the atomic propositions
+ * @task: the task
+ * @mon: the LTL monitor
+ *
+ * Must be implemented. This function is called during task creation, and should initialize all
+ * atomic propositions. rv_rtapp_block_atom_set() should be used to implement this function.
+ *
+ * This function does not have to initialize atomic propositions that are updated by
+ * rv_rtapp_block_atoms_fetch(), because the two functions are called together.
+ */
+void rv_rtapp_block_atoms_init(struct task_struct *task, struct ltl_monitor *mon);
+
+/**
+ * rv_rtapp_block_atoms_fetch - fetch the atomic propositions
+ * @task: the task
+ * @mon: the LTL monitor
+ *
+ * Must be implemented. This function is called anytime the Buchi automaton is triggered. Its
+ * intended purpose is to update the atomic propositions which are expensive to trace and can be
+ * easily read from @task. rv_rtapp_block_atom_set() should be used to implement this function.
+ *
+ * Using this function may cause incorrect verification result if it is important for the LTL that
+ * the atomic propositions must be updated at the correct time. Therefore, if it is possible,
+ * updating atomic propositions should be done with rv_rtapp_block_atom_update() instead.
+ *
+ * An example where this function is useful is with the LTL property:
+ * always (RT imply not PAGEFAULT)
+ * (a realtime task does not raise page faults)
+ *
+ * In this example, adding tracepoints to track RT is complicated, because it is changed in
+ * differrent places (mutex's priority boosting, sched_setscheduler). Furthermore, for this LTL
+ * property, we don't care exactly when RT changes, as long as we have its correct value when
+ * PAGEFAULT==true. Therefore, it is better to update RT in rv_rtapp_block_atoms_fetch(), as it
+ * can easily be retrieved from task_struct.
+ *
+ * This function can be empty.
+ */
+void rv_rtapp_block_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon);
+
+/**
+ * rv_rtapp_block_atom_update - update an atomic proposition
+ * @task: the task
+ * @atom: the atomic proposition, one of enum rtapp_block_atom
+ * @value: the new value for @atom
+ *
+ * Update an atomic proposition and trigger the Buchi atomaton to check for violation of the LTL
+ * property. This function can be called in tracepoints' handler, for example.
+ */
+void rv_rtapp_block_atom_update(struct task_struct *task, unsigned int atom, bool value);
+
+/**
+ * rv_rtapp_block_atom_get - get an atomic proposition
+ * @mon: the monitor
+ * @atom: the atomic proposition, one of enum rtapp_block_atom
+ *
+ * Returns the value of an atomic proposition.
+ */
+static inline
+enum ltl_truth_value rv_rtapp_block_atom_get(struct ltl_monitor *mon, unsigned int atom)
+{
+ return mon->atoms[atom];
+}
+
+/**
+ * rv_rtapp_block_atom_set - set an atomic proposition
+ * @mon: the monitor
+ * @atom: the atomic proposition, one of enum rtapp_block_atom
+ * @value: the new value for @atom
+ *
+ * Update an atomic proposition without triggering the Buchi automaton. This can be useful to
+ * implement rv_rtapp_block_atoms_fetch() and rv_rtapp_block_atoms_init().
+ *
+ * Another use case for this function is when multiple atomic propositions change at the same time,
+ * because calling rv_rtapp_block_atom_update() (and thus triggering the Buchi automaton)
+ * multiple times may be incorrect. In that case, rv_rtapp_block_atom_set() can be used to avoid
+ * triggering the Buchi automaton, and rv_rtapp_block_atom_update() is only used for the last
+ * atomic proposition.
+ */
+static inline
+void rv_rtapp_block_atom_set(struct ltl_monitor *mon, unsigned int atom, bool value)
+{
+ mon->atoms[atom] = value;
+}
+
+/**
+ * rv_rtapp_block_get_data - get the custom data of this monitor.
+ * @mon: the monitor
+ *
+ * If this function is used, rv_rtapp_block_init() must have been called with a positive
+ * data_size.
+ */
+static inline void *rv_rtapp_block_get_data(struct ltl_monitor *mon)
+{
+ return &mon->data;
+}
diff --git a/kernel/trace/rv/monitors/rtapp_block/ltl b/kernel/trace/rv/monitors/rtapp_block/ltl
new file mode 100644
index 000000000000..781f0144a222
--- /dev/null
+++ b/kernel/trace/rv/monitors/rtapp_block/ltl
@@ -0,0 +1,9 @@
+RULE = always (WAKEUP_RT_TASK imply (RT or WAKEUP_WHITELIST))
+ and always ((USER_TASK and RT) imply (SLEEP imply INTENTIONAL_SLEEP))
+
+INTENTIONAL_SLEEP = DO_NANOSLEEP or FUTEX_LOCK_WITH_PI
+
+WAKEUP_WHITELIST = RT_MUTEX_WAKING_WAITER
+ or STOPPING_WOKEN_TASK
+ or WOKEN_TASK_IS_MIGRATION
+ or WOKEN_TASK_IS_RCU
diff --git a/kernel/trace/rv/monitors/rtapp_block/rtapp_block.c b/kernel/trace/rv/monitors/rtapp_block/rtapp_block.c
new file mode 100644
index 000000000000..3f5b1efb7af0
--- /dev/null
+++ b/kernel/trace/rv/monitors/rtapp_block/rtapp_block.c
@@ -0,0 +1,232 @@
+// 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/sched/rt.h>
+#include <linux/preempt.h>
+#include <linux/rv.h>
+
+#include <uapi/linux/futex.h>
+#include <trace/events/syscalls.h>
+#include <trace/events/sched.h>
+#include <trace/events/task.h>
+#include <trace/events/lock.h>
+#include <trace/events/preemptirq.h>
+
+#include <rv_trace.h>
+#include <rv/instrumentation.h>
+
+
+#include "ba.h"
+
+struct rtapp_block_data {
+ struct task_struct *woken_task;
+ struct task_struct *stopping_task;
+};
+
+static void handle_sys_enter(void *data, struct pt_regs *regs, long id)
+{
+ unsigned long args[6];
+ int op, cmd;
+
+ switch (id) {
+ case __NR_nanosleep:
+ case __NR_clock_nanosleep:
+#ifdef __NR_clock_nanosleep_time64
+ case __NR_clock_nanosleep_time64:
+#endif
+ rv_rtapp_block_atom_update(current, DO_NANOSLEEP, true);
+ break;
+
+ case __NR_futex:
+#ifdef __NR_futex_time64
+ case __NR_futex_time64:
+#endif
+ syscall_get_arguments(current, regs, args);
+ op = args[1];
+ cmd = op & FUTEX_CMD_MASK;
+
+ if (cmd == FUTEX_LOCK_PI || cmd == FUTEX_LOCK_PI2)
+ rv_rtapp_block_atom_update(current, FUTEX_LOCK_WITH_PI, true);
+ break;
+ }
+}
+
+static void handle_sys_exit(void *data, struct pt_regs *regs, long ret)
+{
+ struct ltl_monitor *mon = rv_rtapp_block_get_monitor(current);
+
+ rv_rtapp_block_atom_set(mon, FUTEX_LOCK_WITH_PI, false);
+ rv_rtapp_block_atom_update(current, DO_NANOSLEEP, false);
+}
+
+static void handle_sched_switch(void *data, bool preempt, struct task_struct *prev,
+ struct task_struct *next, unsigned int prev_state)
+{
+ if (prev_state & TASK_INTERRUPTIBLE)
+ rv_rtapp_block_atom_update(prev, SLEEP, true);
+ rv_rtapp_block_atom_update(next, SLEEP, false);
+}
+
+void rv_rtapp_block_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+ rv_rtapp_block_atom_set(mon, RT, rt_task(task));
+ rv_rtapp_block_atom_set(mon, USER_TASK, !(task->flags & PF_KTHREAD));
+}
+
+void rv_rtapp_block_atoms_init(struct task_struct *task, struct ltl_monitor *mon)
+{
+ rv_rtapp_block_atom_set(mon, SLEEP, false);
+ rv_rtapp_block_atom_set(mon, DO_NANOSLEEP, false);
+ rv_rtapp_block_atom_set(mon, FUTEX_LOCK_PI, false);
+ rv_rtapp_block_atom_set(mon, WAKEUP_RT_TASK, false);
+ rv_rtapp_block_atom_set(mon, RT_MUTEX_WAKING_WAITER, false);
+ rv_rtapp_block_atom_set(mon, STOPPING_WOKEN_TASK, false);
+ rv_rtapp_block_atom_set(mon, WOKEN_TASK_IS_MIGRATION, false);
+ rv_rtapp_block_atom_set(mon, WOKEN_TASK_IS_RCU, false);
+}
+
+static void handle_rt_mutex_wake_waiter_begin(void *, struct task_struct *task)
+{
+ rv_rtapp_block_atom_update(task, RT_MUTEX_WAKING_WAITER, true);
+}
+
+static void handle_rt_mutex_wake_waiter_end(void *, struct task_struct *task)
+{
+ rv_rtapp_block_atom_update(task, RT_MUTEX_WAKING_WAITER, false);
+}
+
+static void handle_sched_kthread_stop(void *, struct task_struct *task)
+{
+ struct ltl_monitor *mon = rv_rtapp_block_get_monitor(current);
+ struct rtapp_block_data *data = rv_rtapp_block_get_data(mon);
+
+ data->stopping_task = task;
+}
+
+static void handle_sched_kthread_stop_ret(void *, int)
+{
+ struct ltl_monitor *mon = rv_rtapp_block_get_monitor(current);
+ struct rtapp_block_data *data = rv_rtapp_block_get_data(mon);
+
+ data->stopping_task = NULL;
+}
+
+static void handle_sched_wakeup(void *, struct task_struct *task)
+{
+ struct ltl_monitor *mon = rv_rtapp_block_get_monitor(current);
+ struct rtapp_block_data *data = rv_rtapp_block_get_data(mon);
+
+ if (!in_task())
+ return;
+
+ if (this_cpu_read(hardirq_context))
+ return;
+
+ if (!rt_task(task))
+ return;
+
+ data->woken_task = task;
+
+ if (!strncmp(task->comm, "migration/", strlen("migration/")))
+ rv_rtapp_block_atom_set(mon, WOKEN_TASK_IS_MIGRATION, true);
+ if (!strcmp(task->comm, "rcu_preempt"))
+ rv_rtapp_block_atom_set(mon, WOKEN_TASK_IS_RCU, true);
+ if (data->stopping_task == data->woken_task)
+ rv_rtapp_block_atom_set(mon, STOPPING_WOKEN_TASK, true);
+
+ rv_rtapp_block_atom_update(current, WAKEUP_RT_TASK, true);
+
+ rv_rtapp_block_atom_set(mon, WOKEN_TASK_IS_MIGRATION, false);
+ rv_rtapp_block_atom_set(mon, WOKEN_TASK_IS_RCU, false);
+ rv_rtapp_block_atom_set(mon, STOPPING_WOKEN_TASK, false);
+ rv_rtapp_block_atom_update(current, WAKEUP_RT_TASK, false);
+}
+
+static int enable_rtapp_block(void)
+{
+ int ret;
+
+ ret = rv_rtapp_block_init(sizeof(struct rtapp_block_data));
+
+ if (ret)
+ return ret;
+
+ rv_attach_trace_probe("rtapp_block", sched_wakeup, handle_sched_wakeup);
+ rv_attach_trace_probe("rtapp_block", rt_mutex_wake_waiter_begin,
+ handle_rt_mutex_wake_waiter_begin);
+ rv_attach_trace_probe("rtapp_block", rt_mutex_wake_waiter_end,
+ handle_rt_mutex_wake_waiter_end);
+ rv_attach_trace_probe("rtapp_block", sched_kthread_stop, handle_sched_kthread_stop);
+ rv_attach_trace_probe("rtapp_block", sched_kthread_stop_ret, handle_sched_kthread_stop_ret);
+ rv_attach_trace_probe("rtapp_block", sys_enter, handle_sys_enter);
+ rv_attach_trace_probe("rtapp_block", sys_exit, handle_sys_exit);
+ rv_attach_trace_probe("rtapp_block", sched_switch, handle_sched_switch);
+
+ return 0;
+}
+
+static void disable_rtapp_block(void)
+{
+ rv_detach_trace_probe("rtapp_block", sched_wakeup, handle_sched_wakeup);
+ rv_detach_trace_probe("rtapp_block", rt_mutex_wake_waiter_begin,
+ handle_rt_mutex_wake_waiter_begin);
+ rv_detach_trace_probe("rtapp_block", rt_mutex_wake_waiter_end,
+ handle_rt_mutex_wake_waiter_end);
+ rv_detach_trace_probe("rtapp_block", sched_kthread_stop, handle_sched_kthread_stop);
+ rv_detach_trace_probe("rtapp_block", sched_kthread_stop_ret, handle_sched_kthread_stop_ret);
+ rv_detach_trace_probe("rtapp_block", sys_enter, handle_sys_enter);
+ rv_detach_trace_probe("rtapp_block", sys_exit, handle_sys_exit);
+ rv_detach_trace_probe("rtapp_block", sched_switch, handle_sched_switch);
+
+ rv_rtapp_block_destroy();
+}
+
+static struct rv_monitor rv_rtapp_block = {
+ .name = "rtapp_block",
+ .description = "Monitor that RT tasks are not blocked by non-RT tasks",
+ .enable = enable_rtapp_block,
+ .disable = disable_rtapp_block,
+};
+
+void rv_rtapp_block_error(struct task_struct *task, struct ltl_monitor *mon)
+{
+ struct rtapp_block_data *data = rv_rtapp_block_get_data(mon);
+ struct task_struct *woken = data->woken_task;
+
+ bool sleep = rv_rtapp_block_atom_get(mon, SLEEP);
+
+ if (sleep)
+ trace_rtapp_block_sleep_error(task);
+ else
+ trace_rtapp_block_wakeup_error(task, woken);
+
+#ifdef CONFIG_RV_REACTORS
+ if (!rv_rtapp_block.react)
+ return;
+
+ if (sleep) {
+ rv_rtapp_block.react("rv: %s[%d](RT) is blocked\n", task->comm, task->pid);
+ } else {
+ rv_rtapp_block.react("rv: %s[%d](RT) was blocked %s[%d](non-RT)\n",
+ woken->comm, woken->pid,
+ task->comm, task->pid);
+ }
+#endif
+}
+
+static int __init register_rtapp_block(void)
+{
+ rv_register_monitor(&rv_rtapp_block);
+ return 0;
+}
+
+static void __exit unregister_rtapp_block(void)
+{
+ rv_unregister_monitor(&rv_rtapp_block);
+}
+
+module_init(register_rtapp_block);
+module_exit(unregister_rtapp_block);
diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index 96264233cac5..79a7388b5c55 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -121,6 +121,50 @@ DECLARE_EVENT_CLASS(error_da_monitor_id,
// Add new monitors based on CONFIG_DA_MON_EVENTS_ID here
#endif /* CONFIG_DA_MON_EVENTS_ID */
+#ifdef CONFIG_RV_MON_RTAPP_BLOCK
+TRACE_EVENT(rtapp_block_wakeup_error,
+
+ TP_PROTO(struct task_struct *task, struct task_struct *woken),
+
+ TP_ARGS(task, woken),
+
+ TP_STRUCT__entry(
+ __string(comm, task->comm)
+ __string(woken_comm, woken->comm)
+ __field(pid_t, pid)
+ __field(pid_t, woken_pid)
+ ),
+
+ TP_fast_assign(
+ __assign_str(comm);
+ __assign_str(woken_comm);
+ __entry->pid = task->pid;
+ __entry->woken_pid = woken->pid;
+ ),
+
+ TP_printk("rv: %s[%d](RT) was blocked by %s[%d](non-RT)\n",
+ __get_str(woken_comm), __entry->woken_pid,
+ __get_str(comm), __entry->pid)
+);
+TRACE_EVENT(rtapp_block_sleep_error,
+
+ TP_PROTO(struct task_struct *task),
+
+ TP_ARGS(task),
+
+ TP_STRUCT__entry(
+ __string(comm, task->comm)
+ __field(pid_t, pid)
+ ),
+
+ TP_fast_assign(
+ __assign_str(comm);
+ __entry->pid = task->pid;
+ ),
+
+ TP_printk("rv: %s[%d](RT) is blocked\n", __get_str(comm), __entry->pid)
+);
+#endif
#endif /* _TRACE_RV_H */
/* This part must be outside protection */
diff --git a/lib/Kconfig.debug b/lib/Kconfig.debug
index 1af972a92d06..942318ef3f62 100644
--- a/lib/Kconfig.debug
+++ b/lib/Kconfig.debug
@@ -1638,6 +1638,9 @@ config TRACE_IRQFLAGS
Enables hooks to interrupt enabling and disabling for
either tracing or lock debugging.
+config TRACE_RT_MUTEX_WAKE_WAITER
+ bool
+
config TRACE_IRQFLAGS_NMI
def_bool y
depends on TRACE_IRQFLAGS
--
2.39.5
^ permalink raw reply related [flat|nested] 23+ messages in thread* Re: [PATCH 04/10] rv: Add rtapp_block monitor
2025-03-11 17:05 ` [PATCH 04/10] rv: Add rtapp_block monitor Nam Cao
@ 2025-03-12 7:34 ` Gabriele Monaco
2025-03-13 15:15 ` kernel test robot
1 sibling, 0 replies; 23+ messages in thread
From: Gabriele Monaco @ 2025-03-12 7:34 UTC (permalink / raw)
To: Nam Cao, Steven Rostedt, john.ogness, linux-trace-kernel,
linux-kernel
Cc: Peter Zijlstra, Ingo Molnar, Will Deacon, Boqun Feng, Waiman Long
On Tue, 2025-03-11 at 18:05 +0100, Nam Cao wrote:
> Add an RV monitor to detect realtime tasks getting blocked. For the
> full
> description, see Documentation/trace/rv/monitor_rtapp_block.rst.
>
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
> Cc: Peter Zijlstra <peterz@infradead.org>
> Cc: Ingo Molnar <mingo@redhat.com>
> Cc: Will Deacon <will@kernel.org>
> Cc: Boqun Feng <boqun.feng@gmail.com>
> Cc: Waiman Long <longman@redhat.com>
> ---
> .../trace/rv/monitor_rtapp_block.rst | 34 +++
> include/trace/events/lock.h | 12 +
> kernel/locking/rtmutex.c | 4 +
> kernel/trace/rv/Kconfig | 12 +-
> kernel/trace/rv/Makefile | 2 +
> kernel/trace/rv/monitors/rtapp_block/ba.c | 146 +++++++++++
> kernel/trace/rv/monitors/rtapp_block/ba.h | 166 +++++++++++++
> kernel/trace/rv/monitors/rtapp_block/ltl | 9 +
> .../rv/monitors/rtapp_block/rtapp_block.c | 232
> ++++++++++++++++++
I see the creation of this type of monitor requires a bit more steps,
but are you considering automatic generation of Kconfig and
rtapp_block.c ?
We could reuse (export) some code from dot2k for that since the
skeleton could be the same.
Not needed for this series but it would be very nice to experiment
further.
I see the tracepoint generation is a bit complicated to generalise.
Da monitors currently don't give much data, besides pointing to what
failed in the model. If the user wants more, they can enable the
triggering tracepoints (e.g. I want to see the exact details of a
context switch, I enable that in the trace).
I get it isn't the quickest thing to do but makes the monitors very
general. Do you think something like this could be done here too?
Perhaps storing possible error messages in the monitor's header file
(like the state names in a da monitor).
> kernel/trace/rv/rv_trace.h | 44 ++++
> lib/Kconfig.debug | 3 +
> 11 files changed, 663 insertions(+), 1 deletion(-)
> create mode 100644 Documentation/trace/rv/monitor_rtapp_block.rst
> create mode 100644 kernel/trace/rv/monitors/rtapp_block/ba.c
> create mode 100644 kernel/trace/rv/monitors/rtapp_block/ba.h
> create mode 100644 kernel/trace/rv/monitors/rtapp_block/ltl
> create mode 100644
> kernel/trace/rv/monitors/rtapp_block/rtapp_block.c
>
> diff --git a/Documentation/trace/rv/monitor_rtapp_block.rst
> b/Documentation/trace/rv/monitor_rtapp_block.rst
> new file mode 100644
> index 000000000000..9cabbe66fa4a
> --- /dev/null
> +++ b/Documentation/trace/rv/monitor_rtapp_block.rst
> @@ -0,0 +1,34 @@
> +Monitor rtapp_block
> +=======================
> +
> +- Name: rtapp_block - real time applications are undesirably blocked
> +- Type: per-task linear temporal logic monitor
> +- Author: Nam Cao <namcao@linutronix.de>
> +
> +Introduction
> +------------
> +
> +Real time threads could be blocked and fail to finish their
> execution timely. For instance, they
> +need to access shared resources which are already acquired by other
> threads. Or they could be
> +waiting for non-realtime threads to signal them to proceed: as the
> non-realtime threads are not
> +prioritized by the scheduler, the execution of realtime threads
> could be delayed indefinitely.
> +These scenarios are often unintentional, and cause unexpected
> latency to the realtime application.
> +
> +The rtapp_block monitor reports this type of scenario, by monitoring
> for:
> +
> + * Realtime threads going to sleep without explicitly asking for it
> (namely, with nanosleep
> + syscall).
> + * Realtime threads are woken up by non-realtime threads.
> +
> +How to fix the monitor's warnings?
> +----------------------------------
> +
> +There is no single answer, the solution needs to be evaluated
> depending on the specific cases.
> +
> +If the realtime thread is blocked trying to take a `pthread_mutex_t`
> which is already taken by a
> +non-realtime thread, the solution could be enabling priority
> inheritance for the mutex, so that the
> +blocking non-realtime thread would be priority-boosted to run at
> realtime priority.
> +
> +If realtime thread needs to wait for non-realtime thread to signal
> it to proceed, perhaps the design
> +needs to be reconsidered to remove this dependency. Often, the work
> executed by the realtime thread
> +needs not to be realtime at all.
> diff --git a/include/trace/events/lock.h
> b/include/trace/events/lock.h
> index 8e89baa3775f..d4b32194d47f 100644
> --- a/include/trace/events/lock.h
> +++ b/include/trace/events/lock.h
> @@ -138,6 +138,18 @@ TRACE_EVENT(contention_end,
> TP_printk("%p (ret=%d)", __entry->lock_addr, __entry->ret)
> );
>
> +#ifdef CONFIG_TRACE_RT_MUTEX_WAKE_WAITER
> +DECLARE_TRACE(rt_mutex_wake_waiter_begin,
> + TP_PROTO(struct task_struct *task),
> + TP_ARGS(task))
> +DECLARE_TRACE(rt_mutex_wake_waiter_end,
> + TP_PROTO(struct task_struct *task),
> + TP_ARGS(task))
> +#else
> +#define trace_rt_mutex_wake_waiter_begin(...)
> +#define trace_rt_mutex_wake_waiter_end(...)
> +#endif /* CONFIG_TRACE_RT_MUTEX */
> +
> #endif /* _TRACE_LOCK_H */
>
> /* This part must be outside protection */
> diff --git a/kernel/locking/rtmutex.c b/kernel/locking/rtmutex.c
> index 4a8df1800cbb..fc9cf4a2cf75 100644
> --- a/kernel/locking/rtmutex.c
> +++ b/kernel/locking/rtmutex.c
> [...]
> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
> index 8226352a0062..d65bf9bda2f2 100644
> --- a/kernel/trace/rv/Kconfig
> +++ b/kernel/trace/rv/Kconfig
> [...]
> diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
> index 188b64668e1f..6570a3116127 100644
> --- a/kernel/trace/rv/Makefile
> +++ b/kernel/trace/rv/Makefile
> [...]
> diff --git a/kernel/trace/rv/monitors/rtapp_block/ba.c
> b/kernel/trace/rv/monitors/rtapp_block/ba.c
> new file mode 100644
> index 000000000000..5e99f79d5e74
> --- /dev/null
> +++ b/kernel/trace/rv/monitors/rtapp_block/ba.c
> @@ -0,0 +1,146 @@
> [...]
> diff --git a/kernel/trace/rv/monitors/rtapp_block/ba.h
> b/kernel/trace/rv/monitors/rtapp_block/ba.h
> new file mode 100644
> index 000000000000..c1ba88f6779a
> --- /dev/null
> +++ b/kernel/trace/rv/monitors/rtapp_block/ba.h
> @@ -0,0 +1,166 @@
> [...]
> +
> +/**
> + * rv_rtapp_block_atoms_fetch - fetch the atomic propositions
> + * @task: the task
> + * @mon: the LTL monitor
> + *
> + * Must be implemented. This function is called anytime the Buchi
> automaton is triggered. Its
> + * intended purpose is to update the atomic propositions which are
> expensive to trace and can be
> + * easily read from @task. rv_rtapp_block_atom_set() should be used
> to implement this function.
> + *
> + * Using this function may cause incorrect verification result if it
> is important for the LTL that
> + * the atomic propositions must be updated at the correct time.
> Therefore, if it is possible,
> + * updating atomic propositions should be done with
> rv_rtapp_block_atom_update() instead.
> + *
> + * An example where this function is useful is with the LTL
> property:
> + * always (RT imply not PAGEFAULT)
> + * (a realtime task does not raise page faults)
> + *
> + * In this example, adding tracepoints to track RT is complicated,
> because it is changed in
> + * differrent places (mutex's priority boosting,
> sched_setscheduler). Furthermore, for this LTL
> + * property, we don't care exactly when RT changes, as long as we
> have its correct value when
> + * PAGEFAULT==true. Therefore, it is better to update RT in
> rv_rtapp_block_atoms_fetch(), as it
> + * can easily be retrieved from task_struct.
> + *
> + * This function can be empty.
Personal preference, but what about having the examples only in the
docs and point to those from here? Just to keep the code a bit slimmer.
> + */
> +void rv_rtapp_block_atoms_fetch(struct task_struct *task, struct
> ltl_monitor *mon);
> +
> +/**
> + * rv_rtapp_block_atom_update - update an atomic proposition
> + * @task: the task
> + * @atom: the atomic proposition, one of enum rtapp_block_atom
> + * @value: the new value for @atom
> + *
> + * Update an atomic proposition and trigger the Buchi atomaton to
> check for violation of the LTL
> + * property. This function can be called in tracepoints' handler,
> for example.
> + */
> +void rv_rtapp_block_atom_update(struct task_struct *task, unsigned
> int atom, bool value);
> +
> +/**
> + * rv_rtapp_block_atom_get - get an atomic proposition
> + * @mon: the monitor
> + * @atom: the atomic proposition, one of enum rtapp_block_atom
> + *
> + * Returns the value of an atomic proposition.
> + */
> +static inline
> +enum ltl_truth_value rv_rtapp_block_atom_get(struct ltl_monitor
> *mon, unsigned int atom)
> +{
> + return mon->atoms[atom];
> +}
> +
> +/**
> + * rv_rtapp_block_atom_set - set an atomic proposition
> + * @mon: the monitor
> + * @atom: the atomic proposition, one of enum rtapp_block_atom
> + * @value: the new value for @atom
> + *
> + * Update an atomic proposition without triggering the Buchi
> automaton. This can be useful to
> + * implement rv_rtapp_block_atoms_fetch() and
> rv_rtapp_block_atoms_init().
> + *
> + * Another use case for this function is when multiple atomic
> propositions change at the same time,
> + * because calling rv_rtapp_block_atom_update() (and thus triggering
> the Buchi automaton)
> + * multiple times may be incorrect. In that case,
> rv_rtapp_block_atom_set() can be used to avoid
> + * triggering the Buchi automaton, and rv_rtapp_block_atom_update()
> is only used for the last
> + * atomic proposition.
> + */
> +static inline
> +void rv_rtapp_block_atom_set(struct ltl_monitor *mon, unsigned int
> atom, bool value)
> +{
> + mon->atoms[atom] = value;
> +}
> +
> +/**
> + * rv_rtapp_block_get_data - get the custom data of this monitor.
> + * @mon: the monitor
> + *
> + * If this function is used, rv_rtapp_block_init() must have been
> called with a positive
> + * data_size.
> + */
> +static inline void *rv_rtapp_block_get_data(struct ltl_monitor *mon)
> +{
> + return &mon->data;
> +}
> diff --git a/kernel/trace/rv/monitors/rtapp_block/ltl
> b/kernel/trace/rv/monitors/rtapp_block/ltl
> new file mode 100644
> index 000000000000..781f0144a222
> --- /dev/null
> +++ b/kernel/trace/rv/monitors/rtapp_block/ltl
> @@ -0,0 +1,9 @@
> +RULE = always (WAKEUP_RT_TASK imply (RT or WAKEUP_WHITELIST))
> + and always ((USER_TASK and RT) imply (SLEEP imply
> INTENTIONAL_SLEEP))
> +
> +INTENTIONAL_SLEEP = DO_NANOSLEEP or FUTEX_LOCK_WITH_PI
> +
> +WAKEUP_WHITELIST = RT_MUTEX_WAKING_WAITER
> + or STOPPING_WOKEN_TASK
> + or WOKEN_TASK_IS_MIGRATION
> + or WOKEN_TASK_IS_RCU
> diff --git a/kernel/trace/rv/monitors/rtapp_block/rtapp_block.c
> b/kernel/trace/rv/monitors/rtapp_block/rtapp_block.c
> new file mode 100644
> index 000000000000..3f5b1efb7af0
I'm wondering if it would be cleaner to keep the specifications under tools/
(just like the dot files for da monitors).
Nevertheless we should be consistent with what we choose.
Thanks,
Gabriele
> --- /dev/null
> +++ b/kernel/trace/rv/monitors/rtapp_block/rtapp_block.c
> [...]
> diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
> index 96264233cac5..79a7388b5c55 100644
> --- a/kernel/trace/rv/rv_trace.h
> +++ b/kernel/trace/rv/rv_trace.h
> [...]
> diff --git a/lib/Kconfig.debug b/lib/Kconfig.debug
> index 1af972a92d06..942318ef3f62 100644
> --- a/lib/Kconfig.debug
> +++ b/lib/Kconfig.debug
> @@ -1638,6 +1638,9 @@ config TRACE_IRQFLAGS
> Enables hooks to interrupt enabling and disabling for
> either tracing or lock debugging.
>
> +config TRACE_RT_MUTEX_WAKE_WAITER
> + bool
> +
> config TRACE_IRQFLAGS_NMI
> def_bool y
> depends on TRACE_IRQFLAGS
^ permalink raw reply [flat|nested] 23+ messages in thread* Re: [PATCH 04/10] rv: Add rtapp_block monitor
2025-03-11 17:05 ` [PATCH 04/10] rv: Add rtapp_block monitor Nam Cao
2025-03-12 7:34 ` Gabriele Monaco
@ 2025-03-13 15:15 ` kernel test robot
1 sibling, 0 replies; 23+ messages in thread
From: kernel test robot @ 2025-03-13 15:15 UTC (permalink / raw)
To: Nam Cao, Steven Rostedt, Gabriele Monaco, john.ogness,
linux-trace-kernel, linux-kernel
Cc: llvm, oe-kbuild-all, Nam Cao, Peter Zijlstra, Ingo Molnar,
Will Deacon, Boqun Feng, Waiman Long
Hi Nam,
kernel test robot noticed the following build warnings:
[auto build test WARNING on trace/for-next]
[also build test WARNING on tip/x86/core tip/x86/mm linus/master v6.14-rc6 next-20250313]
[If your patch is applied to the wrong git tree, kindly drop us a note.
And when submitting patch, we suggest to use '--base' as documented in
https://git-scm.com/docs/git-format-patch#_base_tree_information]
url: https://github.com/intel-lab-lkp/linux/commits/Nam-Cao/rv-Add-undef-TRACE_INCLUDE_FILE/20250312-011043
base: https://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace for-next
patch link: https://lore.kernel.org/r/c8a1658c6da343b6055cbfcd6ee5ddea48335d31.1741708239.git.namcao%40linutronix.de
patch subject: [PATCH 04/10] rv: Add rtapp_block monitor
config: hexagon-allyesconfig (https://download.01.org/0day-ci/archive/20250313/202503132244.Azu340js-lkp@intel.com/config)
compiler: clang version 18.1.8 (https://github.com/llvm/llvm-project 3b5b5c1ec4a3095ab096dd780e84d7ab81f3d7ff)
reproduce (this is a W=1 build): (https://download.01.org/0day-ci/archive/20250313/202503132244.Azu340js-lkp@intel.com/reproduce)
If you fix the issue in a separate patch/commit (i.e. not just a new version of
the same patch/commit), kindly add following tags
| Reported-by: kernel test robot <lkp@intel.com>
| Closes: https://lore.kernel.org/oe-kbuild-all/202503132244.Azu340js-lkp@intel.com/
All warnings (new ones prefixed by >>):
>> kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:91:53: warning: omitting the parameter name in a function definition is a C23 extension [-Wc23-extensions]
91 | static void handle_rt_mutex_wake_waiter_begin(void *, struct task_struct *task)
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:96:51: warning: omitting the parameter name in a function definition is a C23 extension [-Wc23-extensions]
96 | static void handle_rt_mutex_wake_waiter_end(void *, struct task_struct *task)
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:101:45: warning: omitting the parameter name in a function definition is a C23 extension [-Wc23-extensions]
101 | static void handle_sched_kthread_stop(void *, struct task_struct *task)
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:109:49: warning: omitting the parameter name in a function definition is a C23 extension [-Wc23-extensions]
109 | static void handle_sched_kthread_stop_ret(void *, int)
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:109:54: warning: omitting the parameter name in a function definition is a C23 extension [-Wc23-extensions]
109 | static void handle_sched_kthread_stop_ret(void *, int)
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:117:39: warning: omitting the parameter name in a function definition is a C23 extension [-Wc23-extensions]
117 | static void handle_sched_wakeup(void *, struct task_struct *task)
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:164:2: error: call to undeclared function 'check_trace_callback_type_sys_enter'; ISO C99 and later do not support implicit function declarations [-Wimplicit-function-declaration]
164 | rv_attach_trace_probe("rtapp_block", sys_enter, handle_sys_enter);
| ^
include/rv/instrumentation.h:18:3: note: expanded from macro 'rv_attach_trace_probe'
18 | check_trace_callback_type_##tp(rv_handler); \
| ^
<scratch space>:8:1: note: expanded from here
8 | check_trace_callback_type_sys_enter
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:164:2: error: call to undeclared function 'register_trace_sys_enter'; ISO C99 and later do not support implicit function declarations [-Wimplicit-function-declaration]
include/rv/instrumentation.h:19:13: note: expanded from macro 'rv_attach_trace_probe'
19 | WARN_ONCE(register_trace_##tp(rv_handler, NULL), \
| ^
<scratch space>:9:1: note: expanded from here
9 | register_trace_sys_enter
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:165:2: error: call to undeclared function 'check_trace_callback_type_sys_exit'; ISO C99 and later do not support implicit function declarations [-Wimplicit-function-declaration]
165 | rv_attach_trace_probe("rtapp_block", sys_exit, handle_sys_exit);
| ^
include/rv/instrumentation.h:18:3: note: expanded from macro 'rv_attach_trace_probe'
18 | check_trace_callback_type_##tp(rv_handler); \
| ^
<scratch space>:14:1: note: expanded from here
14 | check_trace_callback_type_sys_exit
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:165:2: error: call to undeclared function 'register_trace_sys_exit'; ISO C99 and later do not support implicit function declarations [-Wimplicit-function-declaration]
include/rv/instrumentation.h:19:13: note: expanded from macro 'rv_attach_trace_probe'
19 | WARN_ONCE(register_trace_##tp(rv_handler, NULL), \
| ^
<scratch space>:15:1: note: expanded from here
15 | register_trace_sys_exit
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:165:2: note: did you mean 'register_ftrace_direct'?
include/rv/instrumentation.h:19:13: note: expanded from macro 'rv_attach_trace_probe'
19 | WARN_ONCE(register_trace_##tp(rv_handler, NULL), \
| ^
<scratch space>:15:1: note: expanded from here
15 | register_trace_sys_exit
| ^
include/linux/ftrace.h:535:19: note: 'register_ftrace_direct' declared here
535 | static inline int register_ftrace_direct(struct ftrace_ops *ops, unsigned long addr)
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:180:2: error: call to undeclared function 'unregister_trace_sys_enter'; ISO C99 and later do not support implicit function declarations [-Wimplicit-function-declaration]
180 | rv_detach_trace_probe("rtapp_block", sys_enter, handle_sys_enter);
| ^
include/rv/instrumentation.h:28:3: note: expanded from macro 'rv_detach_trace_probe'
28 | unregister_trace_##tp(rv_handler, NULL); \
| ^
<scratch space>:29:1: note: expanded from here
29 | unregister_trace_sys_enter
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:181:2: error: call to undeclared function 'unregister_trace_sys_exit'; ISO C99 and later do not support implicit function declarations [-Wimplicit-function-declaration]
181 | rv_detach_trace_probe("rtapp_block", sys_exit, handle_sys_exit);
| ^
include/rv/instrumentation.h:28:3: note: expanded from macro 'rv_detach_trace_probe'
28 | unregister_trace_##tp(rv_handler, NULL); \
| ^
<scratch space>:30:1: note: expanded from here
30 | unregister_trace_sys_exit
| ^
kernel/trace/rv/monitors/rtapp_block/rtapp_block.c:181:2: note: did you mean 'unregister_ftrace_direct'?
include/rv/instrumentation.h:28:3: note: expanded from macro 'rv_detach_trace_probe'
28 | unregister_trace_##tp(rv_handler, NULL); \
| ^
<scratch space>:30:1: note: expanded from here
30 | unregister_trace_sys_exit
| ^
include/linux/ftrace.h:539:19: note: 'unregister_ftrace_direct' declared here
539 | static inline int unregister_ftrace_direct(struct ftrace_ops *ops, unsigned long addr,
| ^
6 warnings and 6 errors generated.
vim +91 kernel/trace/rv/monitors/rtapp_block/rtapp_block.c
90
> 91 static void handle_rt_mutex_wake_waiter_begin(void *, struct task_struct *task)
92 {
93 rv_rtapp_block_atom_update(task, RT_MUTEX_WAKING_WAITER, true);
94 }
95
--
0-DAY CI Kernel Test Service
https://github.com/intel/lkp-tests/wiki
^ permalink raw reply [flat|nested] 23+ messages in thread
* [PATCH 05/10] x86/tracing: Remove redundant trace_pagefault_key
2025-03-11 17:05 [PATCH 00/10] RV: Linear temporal logic monitors for RT application Nam Cao
` (3 preceding siblings ...)
2025-03-11 17:05 ` [PATCH 04/10] rv: Add rtapp_block monitor Nam Cao
@ 2025-03-11 17:05 ` Nam Cao
2025-03-11 17:05 ` [PATCH 06/10] x86/tracing: Move page fault trace points to generic Nam Cao
` (4 subsequent siblings)
9 siblings, 0 replies; 23+ messages in thread
From: Nam Cao @ 2025-03-11 17:05 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, john.ogness, linux-trace-kernel,
linux-kernel
Cc: Nam Cao, Thomas Gleixner, Ingo Molnar, Borislav Petkov,
Dave Hansen, x86, H . Peter Anvin, Andy Lutomirski,
Peter Zijlstra
trace_pagefault_key is used to determine whether the tracepoints are
registered and whether to call trace functions. However, tracepoints
already have this functionality built-in.
Remove this redundant key.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Borislav Petkov <bp@alien8.de>
Cc: Dave Hansen <dave.hansen@linux.intel.com>
Cc: x86@kernel.org
Cc: H. Peter Anvin <hpa@zytor.com>
Cc: Andy Lutomirski <luto@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
---
arch/x86/include/asm/trace/common.h | 12 ------------
arch/x86/include/asm/trace/exceptions.h | 18 ++++++------------
arch/x86/include/asm/trace/irq_vectors.h | 1 -
arch/x86/kernel/tracepoint.c | 21 ---------------------
arch/x86/mm/fault.c | 3 ---
5 files changed, 6 insertions(+), 49 deletions(-)
delete mode 100644 arch/x86/include/asm/trace/common.h
delete mode 100644 arch/x86/kernel/tracepoint.c
diff --git a/arch/x86/include/asm/trace/common.h b/arch/x86/include/asm/trace/common.h
deleted file mode 100644
index f0f9bcdb74d9..000000000000
--- a/arch/x86/include/asm/trace/common.h
+++ /dev/null
@@ -1,12 +0,0 @@
-#ifndef _ASM_TRACE_COMMON_H
-#define _ASM_TRACE_COMMON_H
-
-#ifdef CONFIG_TRACING
-DECLARE_STATIC_KEY_FALSE(trace_pagefault_key);
-#define trace_pagefault_enabled() \
- static_branch_unlikely(&trace_pagefault_key)
-#else
-static inline bool trace_pagefault_enabled(void) { return false; }
-#endif
-
-#endif
diff --git a/arch/x86/include/asm/trace/exceptions.h b/arch/x86/include/asm/trace/exceptions.h
index 6b1e87194809..34bc8214a2d7 100644
--- a/arch/x86/include/asm/trace/exceptions.h
+++ b/arch/x86/include/asm/trace/exceptions.h
@@ -6,10 +6,6 @@
#define _TRACE_PAGE_FAULT_H
#include <linux/tracepoint.h>
-#include <asm/trace/common.h>
-
-extern int trace_pagefault_reg(void);
-extern void trace_pagefault_unreg(void);
DECLARE_EVENT_CLASS(x86_exceptions,
@@ -34,15 +30,13 @@ DECLARE_EVENT_CLASS(x86_exceptions,
(void *)__entry->address, (void *)__entry->ip,
__entry->error_code) );
-#define DEFINE_PAGE_FAULT_EVENT(name) \
-DEFINE_EVENT_FN(x86_exceptions, name, \
- TP_PROTO(unsigned long address, struct pt_regs *regs, \
- unsigned long error_code), \
- TP_ARGS(address, regs, error_code), \
- trace_pagefault_reg, trace_pagefault_unreg);
+DEFINE_EVENT(x86_exceptions, page_fault_user,
+ TP_PROTO(unsigned long address, struct pt_regs *regs, unsigned long error_code),
+ TP_ARGS(address, regs, error_code));
-DEFINE_PAGE_FAULT_EVENT(page_fault_user);
-DEFINE_PAGE_FAULT_EVENT(page_fault_kernel);
+DEFINE_EVENT(x86_exceptions, page_fault_kernel,
+ TP_PROTO(unsigned long address, struct pt_regs *regs, unsigned long error_code),
+ TP_ARGS(address, regs, error_code));
#undef TRACE_INCLUDE_PATH
#undef TRACE_INCLUDE_FILE
diff --git a/arch/x86/include/asm/trace/irq_vectors.h b/arch/x86/include/asm/trace/irq_vectors.h
index 88e7f0f3bf62..7408bebdfde0 100644
--- a/arch/x86/include/asm/trace/irq_vectors.h
+++ b/arch/x86/include/asm/trace/irq_vectors.h
@@ -6,7 +6,6 @@
#define _TRACE_IRQ_VECTORS_H
#include <linux/tracepoint.h>
-#include <asm/trace/common.h>
#ifdef CONFIG_X86_LOCAL_APIC
diff --git a/arch/x86/kernel/tracepoint.c b/arch/x86/kernel/tracepoint.c
deleted file mode 100644
index 03ae1caaa878..000000000000
--- a/arch/x86/kernel/tracepoint.c
+++ /dev/null
@@ -1,21 +0,0 @@
-// SPDX-License-Identifier: GPL-2.0
-/*
- * Copyright (C) 2013 Seiji Aguchi <seiji.aguchi@hds.com>
- */
-#include <linux/jump_label.h>
-#include <linux/atomic.h>
-
-#include <asm/trace/exceptions.h>
-
-DEFINE_STATIC_KEY_FALSE(trace_pagefault_key);
-
-int trace_pagefault_reg(void)
-{
- static_branch_inc(&trace_pagefault_key);
- return 0;
-}
-
-void trace_pagefault_unreg(void)
-{
- static_branch_dec(&trace_pagefault_key);
-}
diff --git a/arch/x86/mm/fault.c b/arch/x86/mm/fault.c
index 296d294142c8..7e3e51fa1f95 100644
--- a/arch/x86/mm/fault.c
+++ b/arch/x86/mm/fault.c
@@ -1455,9 +1455,6 @@ static __always_inline void
trace_page_fault_entries(struct pt_regs *regs, unsigned long error_code,
unsigned long address)
{
- if (!trace_pagefault_enabled())
- return;
-
if (user_mode(regs))
trace_page_fault_user(address, regs, error_code);
else
--
2.39.5
^ permalink raw reply related [flat|nested] 23+ messages in thread* [PATCH 06/10] x86/tracing: Move page fault trace points to generic
2025-03-11 17:05 [PATCH 00/10] RV: Linear temporal logic monitors for RT application Nam Cao
` (4 preceding siblings ...)
2025-03-11 17:05 ` [PATCH 05/10] x86/tracing: Remove redundant trace_pagefault_key Nam Cao
@ 2025-03-11 17:05 ` Nam Cao
2025-03-11 17:05 ` [PATCH 07/10] arm64: mm: Add page fault trace points Nam Cao
` (3 subsequent siblings)
9 siblings, 0 replies; 23+ messages in thread
From: Nam Cao @ 2025-03-11 17:05 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, john.ogness, linux-trace-kernel,
linux-kernel
Cc: Nam Cao, Thomas Gleixner, Ingo Molnar, Borislav Petkov,
Dave Hansen, x86, H. Peter Anvin, Andy Lutomirski, Peter Zijlstra
Page fault trace points are interesting for other architectures as well.
Move them to be generic.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Borislav Petkov <bp@alien8.de>
Cc: Dave Hansen <dave.hansen@linux.intel.com>
Cc: x86@kernel.org
Cc: "H. Peter Anvin" <hpa@zytor.com>
Cc: Andy Lutomirski <luto@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
---
arch/x86/mm/fault.c | 2 +-
.../asm/trace => include/trace/events}/exceptions.h | 13 ++++---------
2 files changed, 5 insertions(+), 10 deletions(-)
rename {arch/x86/include/asm/trace => include/trace/events}/exceptions.h (79%)
diff --git a/arch/x86/mm/fault.c b/arch/x86/mm/fault.c
index 7e3e51fa1f95..ad4cb1502316 100644
--- a/arch/x86/mm/fault.c
+++ b/arch/x86/mm/fault.c
@@ -38,7 +38,7 @@
#include <asm/sev.h> /* snp_dump_hva_rmpentry() */
#define CREATE_TRACE_POINTS
-#include <asm/trace/exceptions.h>
+#include <trace/events/exceptions.h>
/*
* Returns 0 if mmiotrace is disabled, or if the fault is not
diff --git a/arch/x86/include/asm/trace/exceptions.h b/include/trace/events/exceptions.h
similarity index 79%
rename from arch/x86/include/asm/trace/exceptions.h
rename to include/trace/events/exceptions.h
index 34bc8214a2d7..a631f8de8917 100644
--- a/arch/x86/include/asm/trace/exceptions.h
+++ b/include/trace/events/exceptions.h
@@ -7,7 +7,7 @@
#include <linux/tracepoint.h>
-DECLARE_EVENT_CLASS(x86_exceptions,
+DECLARE_EVENT_CLASS(exceptions,
TP_PROTO(unsigned long address, struct pt_regs *regs,
unsigned long error_code),
@@ -22,7 +22,7 @@ DECLARE_EVENT_CLASS(x86_exceptions,
TP_fast_assign(
__entry->address = address;
- __entry->ip = regs->ip;
+ __entry->ip = instruction_pointer(regs);
__entry->error_code = error_code;
),
@@ -30,18 +30,13 @@ DECLARE_EVENT_CLASS(x86_exceptions,
(void *)__entry->address, (void *)__entry->ip,
__entry->error_code) );
-DEFINE_EVENT(x86_exceptions, page_fault_user,
+DEFINE_EVENT(exceptions, page_fault_user,
TP_PROTO(unsigned long address, struct pt_regs *regs, unsigned long error_code),
TP_ARGS(address, regs, error_code));
-
-DEFINE_EVENT(x86_exceptions, page_fault_kernel,
+DEFINE_EVENT(exceptions, page_fault_kernel,
TP_PROTO(unsigned long address, struct pt_regs *regs, unsigned long error_code),
TP_ARGS(address, regs, error_code));
-#undef TRACE_INCLUDE_PATH
-#undef TRACE_INCLUDE_FILE
-#define TRACE_INCLUDE_PATH .
-#define TRACE_INCLUDE_FILE exceptions
#endif /* _TRACE_PAGE_FAULT_H */
/* This part must be outside protection */
--
2.39.5
^ permalink raw reply related [flat|nested] 23+ messages in thread* [PATCH 07/10] arm64: mm: Add page fault trace points
2025-03-11 17:05 [PATCH 00/10] RV: Linear temporal logic monitors for RT application Nam Cao
` (5 preceding siblings ...)
2025-03-11 17:05 ` [PATCH 06/10] x86/tracing: Move page fault trace points to generic Nam Cao
@ 2025-03-11 17:05 ` Nam Cao
2025-03-11 17:05 ` [PATCH 08/10] riscv: " Nam Cao
` (2 subsequent siblings)
9 siblings, 0 replies; 23+ messages in thread
From: Nam Cao @ 2025-03-11 17:05 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, john.ogness, linux-trace-kernel,
linux-kernel
Cc: Nam Cao, Catalin Marinas, Will Deacon, linux-arm-kernel
Add page fault trace points, which are useful to implement RV monitor which
watches page faults.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Catalin Marinas <catalin.marinas@arm.com>
Cc: Will Deacon <will@kernel.org>
Cc: linux-arm-kernel@lists.infradead.org
---
arch/arm64/mm/fault.c | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/arch/arm64/mm/fault.c b/arch/arm64/mm/fault.c
index ef63651099a9..e3f096b0dffd 100644
--- a/arch/arm64/mm/fault.c
+++ b/arch/arm64/mm/fault.c
@@ -44,6 +44,9 @@
#include <asm/tlbflush.h>
#include <asm/traps.h>
+#define CREATE_TRACE_POINTS
+#include <trace/events/exceptions.h>
+
struct fault_info {
int (*fn)(unsigned long far, unsigned long esr,
struct pt_regs *regs);
@@ -559,6 +562,11 @@ static int __kprobes do_page_fault(unsigned long far, unsigned long esr,
if (kprobe_page_fault(regs, esr))
return 0;
+ if (user_mode(regs))
+ trace_page_fault_user(addr, regs, esr);
+ else
+ trace_page_fault_kernel(addr, regs, esr);
+
/*
* If we're in an interrupt or have no user context, we must not take
* the fault.
--
2.39.5
^ permalink raw reply related [flat|nested] 23+ messages in thread* [PATCH 08/10] riscv: mm: Add page fault trace points
2025-03-11 17:05 [PATCH 00/10] RV: Linear temporal logic monitors for RT application Nam Cao
` (6 preceding siblings ...)
2025-03-11 17:05 ` [PATCH 07/10] arm64: mm: Add page fault trace points Nam Cao
@ 2025-03-11 17:05 ` Nam Cao
2025-04-02 7:35 ` Alexandre Ghiti
2025-03-11 17:05 ` [PATCH 09/10] rv: Add rtapp_pagefault monitor Nam Cao
2025-03-11 17:05 ` [PATCH 10/10] rv: raise the number of per-task monitor to 2 Nam Cao
9 siblings, 1 reply; 23+ messages in thread
From: Nam Cao @ 2025-03-11 17:05 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, john.ogness, linux-trace-kernel,
linux-kernel
Cc: Nam Cao, Paul Walmsley, Palmer Dabbelt, Albert Ou,
Alexandre Ghiti, linux-riscv
Add page fault trace points, which are useful to implement RV monitor that
watches page faults.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Paul Walmsley <paul.walmsley@sifive.com>
Cc: Palmer Dabbelt <palmer@dabbelt.com>
Cc: Albert Ou <aou@eecs.berkeley.edu>
Cc: Alexandre Ghiti <alex@ghiti.fr>
Cc: linux-riscv@lists.infradead.org
---
arch/riscv/mm/fault.c | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/arch/riscv/mm/fault.c b/arch/riscv/mm/fault.c
index 0194324a0c50..04ed6f8acae4 100644
--- a/arch/riscv/mm/fault.c
+++ b/arch/riscv/mm/fault.c
@@ -20,6 +20,9 @@
#include <asm/ptrace.h>
#include <asm/tlbflush.h>
+#define CREATE_TRACE_POINTS
+#include <trace/events/exceptions.h>
+
#include "../kernel/head.h"
static void show_pte(unsigned long addr)
@@ -291,6 +294,11 @@ void handle_page_fault(struct pt_regs *regs)
if (kprobe_page_fault(regs, cause))
return;
+ if (user_mode(regs))
+ trace_page_fault_user(addr, regs, cause);
+ else
+ trace_page_fault_kernel(addr, regs, cause);
+
/*
* Fault-in kernel-space virtual memory on-demand.
* The 'reference' page table is init_mm.pgd.
--
2.39.5
^ permalink raw reply related [flat|nested] 23+ messages in thread* Re: [PATCH 08/10] riscv: mm: Add page fault trace points
2025-03-11 17:05 ` [PATCH 08/10] riscv: " Nam Cao
@ 2025-04-02 7:35 ` Alexandre Ghiti
0 siblings, 0 replies; 23+ messages in thread
From: Alexandre Ghiti @ 2025-04-02 7:35 UTC (permalink / raw)
To: Nam Cao, Steven Rostedt, Gabriele Monaco, john.ogness,
linux-trace-kernel, linux-kernel
Cc: Paul Walmsley, Palmer Dabbelt, Albert Ou, linux-riscv
Hi Nam,
On 11/03/2025 18:05, Nam Cao wrote:
> Add page fault trace points, which are useful to implement RV monitor that
> watches page faults.
>
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
> Cc: Paul Walmsley <paul.walmsley@sifive.com>
> Cc: Palmer Dabbelt <palmer@dabbelt.com>
> Cc: Albert Ou <aou@eecs.berkeley.edu>
> Cc: Alexandre Ghiti <alex@ghiti.fr>
> Cc: linux-riscv@lists.infradead.org
> ---
> arch/riscv/mm/fault.c | 8 ++++++++
> 1 file changed, 8 insertions(+)
>
> diff --git a/arch/riscv/mm/fault.c b/arch/riscv/mm/fault.c
> index 0194324a0c50..04ed6f8acae4 100644
> --- a/arch/riscv/mm/fault.c
> +++ b/arch/riscv/mm/fault.c
> @@ -20,6 +20,9 @@
> #include <asm/ptrace.h>
> #include <asm/tlbflush.h>
>
> +#define CREATE_TRACE_POINTS
> +#include <trace/events/exceptions.h>
> +
> #include "../kernel/head.h"
>
> static void show_pte(unsigned long addr)
> @@ -291,6 +294,11 @@ void handle_page_fault(struct pt_regs *regs)
> if (kprobe_page_fault(regs, cause))
> return;
>
> + if (user_mode(regs))
> + trace_page_fault_user(addr, regs, cause);
> + else
> + trace_page_fault_kernel(addr, regs, cause);
> +
> /*
> * Fault-in kernel-space virtual memory on-demand.
> * The 'reference' page table is init_mm.pgd.
For this riscv part, you can add:
Acked-by: Alexandre Ghiti <alexghiti@rivosinc.com>
Thanks,
Alex
^ permalink raw reply [flat|nested] 23+ messages in thread
* [PATCH 09/10] rv: Add rtapp_pagefault monitor
2025-03-11 17:05 [PATCH 00/10] RV: Linear temporal logic monitors for RT application Nam Cao
` (7 preceding siblings ...)
2025-03-11 17:05 ` [PATCH 08/10] riscv: " Nam Cao
@ 2025-03-11 17:05 ` Nam Cao
2025-03-11 17:05 ` [PATCH 10/10] rv: raise the number of per-task monitor to 2 Nam Cao
9 siblings, 0 replies; 23+ messages in thread
From: Nam Cao @ 2025-03-11 17:05 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, john.ogness, linux-trace-kernel,
linux-kernel
Cc: Nam Cao, Catalin Marinas, Will Deacon, Paul Walmsley,
Palmer Dabbelt, Albert Ou, Alexandre Ghiti, Thomas Gleixner,
Ingo Molnar, Borislav Petkov, Dave Hansen, x86, H . Peter Anvin,
Andy Lutomirski, Peter Zijlstra, linux-arm-kernel, linux-riscv
Real time applications can have unexpected latency due to page faults.
Add an RV LTL monitor to detect such cases. For complete description, see
Documentation/trace/rv/monitor_rtapp_pagefault.rst.
The document is mostly from:
https://www.linutronix.de/blog/A-Checklist-for-Real-Time-Applications-in-Linux
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Catalin Marinas <catalin.marinas@arm.com>
Cc: Will Deacon <will@kernel.org>
Cc: Paul Walmsley <paul.walmsley@sifive.com>
Cc: Palmer Dabbelt <palmer@dabbelt.com>
Cc: Albert Ou <aou@eecs.berkeley.edu>
Cc: Alexandre Ghiti <alex@ghiti.fr>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Borislav Petkov <bp@alien8.de>
Cc: Dave Hansen <dave.hansen@linux.intel.com>
Cc: x86@kernel.org
Cc: H. Peter Anvin <hpa@zytor.com>
Cc: Andy Lutomirski <luto@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: linux-arm-kernel@lists.infradead.org
Cc: linux-riscv@lists.infradead.org
---
.../trace/rv/monitor_rtapp_pagefault.rst | 36 ++++
kernel/trace/rv/Kconfig | 8 +
kernel/trace/rv/Makefile | 2 +
kernel/trace/rv/monitors/rtapp_pagefault/ba.c | 139 +++++++++++++++
kernel/trace/rv/monitors/rtapp_pagefault/ba.h | 158 ++++++++++++++++++
kernel/trace/rv/monitors/rtapp_pagefault/ltl | 1 +
.../rtapp_pagefault/rtapp_pagefault.c | 84 ++++++++++
kernel/trace/rv/rv_trace.h | 20 +++
8 files changed, 448 insertions(+)
create mode 100644 Documentation/trace/rv/monitor_rtapp_pagefault.rst
create mode 100644 kernel/trace/rv/monitors/rtapp_pagefault/ba.c
create mode 100644 kernel/trace/rv/monitors/rtapp_pagefault/ba.h
create mode 100644 kernel/trace/rv/monitors/rtapp_pagefault/ltl
create mode 100644 kernel/trace/rv/monitors/rtapp_pagefault/rtapp_pagefault.c
diff --git a/Documentation/trace/rv/monitor_rtapp_pagefault.rst b/Documentation/trace/rv/monitor_rtapp_pagefault.rst
new file mode 100644
index 000000000000..0ee223d83d09
--- /dev/null
+++ b/Documentation/trace/rv/monitor_rtapp_pagefault.rst
@@ -0,0 +1,36 @@
+Monitor rtapp_pagefault
+=======================
+
+- Name: rtapp_pagefault - realtime applications raising page faults
+- Type: per-task linear temporal logic monitor
+- Author: Nam Cao <namcao@linutronix.de>
+
+Introduction
+------------
+
+One of the most devastating situations for a real-time application is the need to assign or "page
+in" memory. This can be due to the over-commitment behavior of Linux when accessing allocated or
+reserved memory for the first time. Or it can be paging in disk data (such as text segments) when
+calling functions for the first time. Whatever the case, it must be avoided in order to meet
+response requirements.
+
+The monitor reports these situation where real-time applications raise page faults.
+
+How to fix the monitor's warnings?
+----------------------------------
+
+The first thing a real-time application needs to do is configure glibc to use a single
+non-shrinkable heap for the application. This guarantees that a pool of readily accessible physical
+RAM can be made available to the real-time application. This is accomplished using the mallopt(3)
+function (M_MMAP_MAX=0, M_ARENA_MAX=1, M_TRIM_THRESHOLD=-1).
+
+Next, all allocated and mapped virtual memory must be assigned to physical RAM and locked so that it
+cannot be reclaimed for other purposes. This is accomplished using the mlockall(2) function
+(MCL_CURRENT | MCL_FUTURE).
+
+Finally, the amounts of stack and heap needed during the lifetime of the real-time application must
+be allocated and written to in order to trigger heap and stack assignments to physical RAM. This is
+known as pre-faulting and is usually accomplished by memsetting a large buffer within a stack frame
+and allocating, memsetting, and freeing a large heap buffer.
+
+Pitfall: Keep in mind that each thread will have its own stack.
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index d65bf9bda2f2..2822af1b2b4d 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -39,6 +39,14 @@ config RV_MON_RTAPP_BLOCK
Enable rtapp_wakeup which monitors that realtime tasks are not blocked.
For details, see Documentation/trace/rv/monitor_rtapp_block.rst.
+config RV_MON_RTAPP_PAGEFAULT
+ depends on RV
+ select DA_MON_EVENTS
+ bool "rtapp_pagefault monitor"
+ help
+ Enable rtapp_pagefault which monitors that real-time tasks do not raise page faults.
+ See Documentation/trace/rv/monitor_rtapp_pagefault.rst for full details.
+
config RV_REACTORS
bool "Runtime verification reactors"
default y
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index 6570a3116127..7f21a679ad70 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -7,6 +7,8 @@ obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o
obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o
obj-$(CONFIG_RV_MON_RTAPP_BLOCK) += monitors/rtapp_block/ba.o \
monitors/rtapp_block/rtapp_block.o
+obj-$(CONFIG_RV_MON_RTAPP_PAGEFAULT) += monitors/rtapp_pagefault/ba.o \
+ monitors/rtapp_pagefault/rtapp_pagefault.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_pagefault/ba.c b/kernel/trace/rv/monitors/rtapp_pagefault/ba.c
new file mode 100644
index 000000000000..6f6322717854
--- /dev/null
+++ b/kernel/trace/rv/monitors/rtapp_pagefault/ba.c
@@ -0,0 +1,139 @@
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * This file is generated, do not edit.
+ */
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+#include <trace/events/task.h>
+#include <trace/events/sched.h>
+
+#include "ba.h"
+
+static_assert(NUM_ATOM <= RV_MAX_LTL_ATOM);
+
+enum buchi_state {
+ INIT,
+ S1,
+ DEAD,
+};
+
+int rv_rtapp_pagefault_task_slot = RV_PER_TASK_MONITOR_INIT;
+
+static void init_monitor(struct task_struct *task)
+{
+ struct ltl_monitor *mon = rv_rtapp_pagefault_get_monitor(task);
+
+ for (int i = 0; i < NUM_ATOM; ++i)
+ mon->atoms[i] = LTL_UNDETERMINED;
+ mon->state = INIT;
+}
+
+static void handle_task_newtask(void *data, struct task_struct *task, unsigned long flags)
+{
+ struct ltl_monitor *mon = rv_rtapp_pagefault_get_monitor(task);
+
+ init_monitor(task);
+
+ rv_rtapp_pagefault_atoms_init(task, mon);
+ rv_rtapp_pagefault_atoms_fetch(task, mon);
+}
+
+int rv_rtapp_pagefault_init(size_t data_size)
+{
+ struct task_struct *g, *p;
+ int ret, cpu;
+
+ if (WARN_ON(data_size > RV_MAX_DATA_SIZE))
+ return -EINVAL;
+
+ ret = rv_get_task_monitor_slot();
+ if (ret < 0)
+ return ret;
+
+ rv_rtapp_pagefault_task_slot = ret;
+
+ rv_attach_trace_probe("rtapp_pagefault", task_newtask, handle_task_newtask);
+
+ read_lock(&tasklist_lock);
+
+ for_each_process_thread(g, p)
+ init_monitor(p);
+
+ for_each_present_cpu(cpu)
+ init_monitor(idle_task(cpu));
+
+ read_unlock(&tasklist_lock);
+
+ return 0;
+}
+
+void rv_rtapp_pagefault_destroy(void)
+{
+ rv_put_task_monitor_slot(rv_rtapp_pagefault_task_slot);
+ rv_rtapp_pagefault_task_slot = RV_PER_TASK_MONITOR_INIT;
+
+ rv_detach_trace_probe("rtapp_pagefault", task_newtask, handle_task_newtask);
+}
+
+static void illegal_state(struct task_struct *task, struct ltl_monitor *mon)
+{
+ mon->state = INIT;
+ rv_rtapp_pagefault_error(task, mon);
+}
+
+static void rv_rtapp_pagefault_attempt_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+ int i;
+
+ mon = rv_rtapp_pagefault_get_monitor(task);
+
+ rv_rtapp_pagefault_atoms_fetch(task, mon);
+
+ for (i = 0; i < NUM_ATOM; ++i) {
+ if (mon->atoms[i] == LTL_UNDETERMINED)
+ return;
+ }
+
+ if (((!mon->atoms[RT] || !mon->atoms[PAGEFAULT])))
+ mon->state = S1;
+ else
+ illegal_state(task, mon);
+}
+
+static void rv_rtapp_pagefault_step(struct task_struct *task, struct ltl_monitor *mon)
+{
+ switch (mon->state) {
+ case S1:
+ if (((!mon->atoms[RT] || !mon->atoms[PAGEFAULT])))
+ mon->state = S1;
+ else
+ illegal_state(task, mon);
+ break;
+ case DEAD:
+ case INIT:
+ break;
+ default:
+ WARN_ON_ONCE(1);
+ }
+}
+
+void rv_rtapp_pagefault_atom_update(struct task_struct *task, unsigned int atom, bool value)
+{
+ struct ltl_monitor *mon = rv_rtapp_pagefault_get_monitor(task);
+
+ rv_rtapp_pagefault_atom_set(mon, atom, value);
+
+ if (mon->state == DEAD)
+ return;
+
+ if (mon->state == INIT)
+ rv_rtapp_pagefault_attempt_start(task, mon);
+ if (mon->state == INIT)
+ return;
+
+ mon->atoms[atom] = value;
+
+ rv_rtapp_pagefault_atoms_fetch(task, mon);
+
+ rv_rtapp_pagefault_step(task, mon);
+}
diff --git a/kernel/trace/rv/monitors/rtapp_pagefault/ba.h b/kernel/trace/rv/monitors/rtapp_pagefault/ba.h
new file mode 100644
index 000000000000..eec2068c1419
--- /dev/null
+++ b/kernel/trace/rv/monitors/rtapp_pagefault/ba.h
@@ -0,0 +1,158 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * This file is generated, do not edit.
+ *
+ * This file includes necessary functions to glue the Buchi automaton and the kernel together.
+ * Some of these functions must be manually implemented (look for "Must be implemented", or just
+ * let the compiler tells you).
+ *
+ * Essentially, you need to manually define the meaning of the atomic propositions in the LTL
+ * property. The primary function for that is rv_rtapp_pagefault_atom_update(), which can be called
+ * in tracepoints' handlers for example. In some specific cases where
+ * rv_rtapp_pagefault_atom_update() is not convenient, rv_rtapp_pagefault_atoms_fetch() can be used.
+ *
+ * rv_rtapp_pagefault_init()/rv_rtapp_pagefault_destroy() must be called while enabling/disabling
+ * the monitor.
+ *
+ * If the fields in struct ltl_monitor is not enough, extra custom data can be used. See
+ * rv_rtapp_pagefault_get_data().
+ */
+
+#include <linux/sched.h>
+
+enum rtapp_pagefault_atom {
+ PAGEFAULT,
+ RT,
+ NUM_ATOM
+};
+
+/**
+ * rv_rtapp_pagefault_init
+ * @data_size: required custom data size, can be zero
+ *
+ * Must be called while enabling the monitor
+ */
+int rv_rtapp_pagefault_init(size_t data_size);
+
+/**
+ * rv_rtapp_pagefault_destroy
+ *
+ * must be called while disabling the monitor
+ */
+void rv_rtapp_pagefault_destroy(void);
+
+/**
+ * rv_rtapp_pagefault_error - report violation of the LTL property
+ * @task: the task violating the LTL property
+ * @mon: the LTL monitor
+ *
+ * Must be implemented. This function should invoke the RV reactor and the monitor's tracepoints.
+ */
+void rv_rtapp_pagefault_error(struct task_struct *task, struct ltl_monitor *mon);
+
+extern int rv_rtapp_pagefault_task_slot;
+
+/**
+ * rv_rtapp_pagefault_get_monitor - get the struct ltl_monitor of a task
+ */
+static inline struct ltl_monitor *rv_rtapp_pagefault_get_monitor(struct task_struct *task)
+{
+ return &task->rv[rv_rtapp_pagefault_task_slot].ltl_mon;
+}
+
+/**
+ * rv_rtapp_pagefault_atoms_init - initialize the atomic propositions
+ * @task: the task
+ * @mon: the LTL monitor
+ *
+ * Must be implemented. This function is called during task creation, and should initialize all
+ * atomic propositions. rv_rtapp_pagefault_atom_set() should be used to implement this function.
+ *
+ * This function does not have to initialize atomic propositions that are updated by
+ * rv_rtapp_pagefault_atoms_fetch(), because the two functions are called together.
+ */
+void rv_rtapp_pagefault_atoms_init(struct task_struct *task, struct ltl_monitor *mon);
+
+/**
+ * rv_rtapp_pagefault_atoms_fetch - fetch the atomic propositions
+ * @task: the task
+ * @mon: the LTL monitor
+ *
+ * Must be implemented. This function is called anytime the Buchi automaton is triggered. Its
+ * intended purpose is to update the atomic propositions which are expensive to trace and can be
+ * easily read from @task. rv_rtapp_pagefault_atom_set() should be used to implement this function.
+ *
+ * Using this function may cause incorrect verification result if it is important for the LTL that
+ * the atomic propositions must be updated at the correct time. Therefore, if it is possible,
+ * updating atomic propositions should be done with rv_rtapp_pagefault_atom_update() instead.
+ *
+ * An example where this function is useful is with the LTL property:
+ * always (RT imply not PAGEFAULT)
+ * (a realtime task does not raise page faults)
+ *
+ * In this example, adding tracepoints to track RT is complicated, because it is changed in
+ * differrent places (mutex's priority boosting, sched_setscheduler). Furthermore, for this LTL
+ * property, we don't care exactly when RT changes, as long as we have its correct value when
+ * PAGEFAULT==true. Therefore, it is better to update RT in rv_rtapp_pagefault_atoms_fetch(), as it
+ * can easily be retrieved from task_struct.
+ *
+ * This function can be empty.
+ */
+void rv_rtapp_pagefault_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon);
+
+/**
+ * rv_rtapp_pagefault_atom_update - update an atomic proposition
+ * @task: the task
+ * @atom: the atomic proposition, one of enum rtapp_pagefault_atom
+ * @value: the new value for @atom
+ *
+ * Update an atomic proposition and trigger the Buchi atomaton to check for violation of the LTL
+ * property. This function can be called in tracepoints' handler, for example.
+ */
+void rv_rtapp_pagefault_atom_update(struct task_struct *task, unsigned int atom, bool value);
+
+/**
+ * rv_rtapp_pagefault_atom_get - get an atomic proposition
+ * @mon: the monitor
+ * @atom: the atomic proposition, one of enum rtapp_pagefault_atom
+ *
+ * Returns the value of an atomic proposition.
+ */
+static inline
+enum ltl_truth_value rv_rtapp_pagefault_atom_get(struct ltl_monitor *mon, unsigned int atom)
+{
+ return mon->atoms[atom];
+}
+
+/**
+ * rv_rtapp_pagefault_atom_set - set an atomic proposition
+ * @mon: the monitor
+ * @atom: the atomic proposition, one of enum rtapp_pagefault_atom
+ * @value: the new value for @atom
+ *
+ * Update an atomic proposition without triggering the Buchi automaton. This can be useful to
+ * implement rv_rtapp_pagefault_atoms_fetch() and rv_rtapp_pagefault_atoms_init().
+ *
+ * Another use case for this function is when multiple atomic propositions change at the same time,
+ * because calling rv_rtapp_pagefault_atom_update() (and thus triggering the Buchi automaton)
+ * multiple times may be incorrect. In that case, rv_rtapp_pagefault_atom_set() can be used to avoid
+ * triggering the Buchi automaton, and rv_rtapp_pagefault_atom_update() is only used for the last
+ * atomic proposition.
+ */
+static inline
+void rv_rtapp_pagefault_atom_set(struct ltl_monitor *mon, unsigned int atom, bool value)
+{
+ mon->atoms[atom] = value;
+}
+
+/**
+ * rv_rtapp_pagefault_get_data - get the custom data of this monitor.
+ * @mon: the monitor
+ *
+ * If this function is used, rv_rtapp_pagefault_init() must have been called with a positive
+ * data_size.
+ */
+static inline void *rv_rtapp_pagefault_get_data(struct ltl_monitor *mon)
+{
+ return &mon->data;
+}
diff --git a/kernel/trace/rv/monitors/rtapp_pagefault/ltl b/kernel/trace/rv/monitors/rtapp_pagefault/ltl
new file mode 100644
index 000000000000..d7ce62102733
--- /dev/null
+++ b/kernel/trace/rv/monitors/rtapp_pagefault/ltl
@@ -0,0 +1 @@
+RULE = always (RT imply not PAGEFAULT)
diff --git a/kernel/trace/rv/monitors/rtapp_pagefault/rtapp_pagefault.c b/kernel/trace/rv/monitors/rtapp_pagefault/rtapp_pagefault.c
new file mode 100644
index 000000000000..32aaae9fea46
--- /dev/null
+++ b/kernel/trace/rv/monitors/rtapp_pagefault/rtapp_pagefault.c
@@ -0,0 +1,84 @@
+// 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>
+#include <linux/sched/rt.h>
+#include <trace/events/sched.h>
+#include <trace/events/exceptions.h>
+#include <rv_trace.h>
+
+#include "ba.h"
+
+static void handle_page_fault(void *data, unsigned long address, struct pt_regs *regs,
+ unsigned long error_code)
+{
+ rv_rtapp_pagefault_atom_update(current, PAGEFAULT, true);
+ rv_rtapp_pagefault_atom_update(current, PAGEFAULT, false);
+}
+
+void rv_rtapp_pagefault_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+ rv_rtapp_pagefault_atom_set(mon, RT, rt_task(task));
+}
+
+void rv_rtapp_pagefault_atoms_init(struct task_struct *task, struct ltl_monitor *mon)
+{
+ rv_rtapp_pagefault_atom_set(mon, PAGEFAULT, false);
+}
+
+static int enable_rtapp_pagefault(void)
+{
+ int ret;
+
+ ret = rv_rtapp_pagefault_init(0);
+ if (ret)
+ return ret;
+
+ rv_attach_trace_probe("rtapp_pagefault", page_fault_kernel, handle_page_fault);
+ rv_attach_trace_probe("rtapp_pagefault", page_fault_user, handle_page_fault);
+
+ return 0;
+}
+
+static void disable_rtapp_pagefault(void)
+{
+ rv_detach_trace_probe("rtapp_pagefault", page_fault_kernel, handle_page_fault);
+ rv_detach_trace_probe("rtapp_pagefault", page_fault_user, handle_page_fault);
+
+ rv_rtapp_pagefault_destroy();
+}
+
+static struct rv_monitor rv_rtapp_pagefault = {
+ .name = "rtapp_pagefault",
+ .description = "monitor RT tasks do not page fault",
+ .enable = enable_rtapp_pagefault,
+ .disable = disable_rtapp_pagefault,
+};
+
+void rv_rtapp_pagefault_error(struct task_struct *task, struct ltl_monitor *mon)
+{
+ trace_rtapp_pagefault_error(task);
+#ifdef CONFIG_RV_REACTORS
+ if (rv_rtapp_pagefault.react)
+ rv_rtapp_pagefault.react("rv: %s[%d](RT) raises a page fault\n",
+ task->comm, task->pid);
+#endif
+}
+
+static int __init register_rtapp_pagefault(void)
+{
+ rv_register_monitor(&rv_rtapp_pagefault);
+ return 0;
+}
+
+static void __exit unregister_rtapp_pagefault(void)
+{
+ rv_unregister_monitor(&rv_rtapp_pagefault);
+}
+
+module_init(register_rtapp_pagefault);
+module_exit(unregister_rtapp_pagefault);
diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index 79a7388b5c55..560581d7edcb 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -165,6 +165,26 @@ TRACE_EVENT(rtapp_block_sleep_error,
TP_printk("rv: %s[%d](RT) is blocked\n", __get_str(comm), __entry->pid)
);
#endif
+#ifdef CONFIG_RV_MON_RTAPP_PAGEFAULT
+TRACE_EVENT(rtapp_pagefault_error,
+
+ TP_PROTO(struct task_struct *task),
+
+ TP_ARGS(task),
+
+ TP_STRUCT__entry(
+ __string(comm, task->comm)
+ __field(pid_t, pid)
+ ),
+
+ TP_fast_assign(
+ __assign_str(comm);
+ __entry->pid = task->pid;
+ ),
+
+ TP_printk("rv: %s[%d](RT) raises a page fault", __get_str(comm), __entry->pid)
+);
+#endif
#endif /* _TRACE_RV_H */
/* This part must be outside protection */
--
2.39.5
^ permalink raw reply related [flat|nested] 23+ messages in thread* [PATCH 10/10] rv: raise the number of per-task monitor to 2
2025-03-11 17:05 [PATCH 00/10] RV: Linear temporal logic monitors for RT application Nam Cao
` (8 preceding siblings ...)
2025-03-11 17:05 ` [PATCH 09/10] rv: Add rtapp_pagefault monitor Nam Cao
@ 2025-03-11 17:05 ` Nam Cao
2025-03-12 6:57 ` Gabriele Monaco
9 siblings, 1 reply; 23+ messages in thread
From: Nam Cao @ 2025-03-11 17:05 UTC (permalink / raw)
To: Steven Rostedt, Gabriele Monaco, john.ogness, linux-trace-kernel,
linux-kernel
Cc: Nam Cao
There are 2 monitors to check realtime applications. Users may want to
enable them both.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
include/linux/rv.h | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/include/linux/rv.h b/include/linux/rv.h
index 6de4f93b390e..224c2194f582 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -44,7 +44,7 @@ struct ltl_monitor {
* adding more or developing a dynamic method. So far, none of
* these are justified.
*/
-#define RV_PER_TASK_MONITORS 1
+#define RV_PER_TASK_MONITORS 2
#define RV_PER_TASK_MONITOR_INIT (RV_PER_TASK_MONITORS)
union rv_task_monitor {
--
2.39.5
^ permalink raw reply related [flat|nested] 23+ messages in thread* Re: [PATCH 10/10] rv: raise the number of per-task monitor to 2
2025-03-11 17:05 ` [PATCH 10/10] rv: raise the number of per-task monitor to 2 Nam Cao
@ 2025-03-12 6:57 ` Gabriele Monaco
0 siblings, 0 replies; 23+ messages in thread
From: Gabriele Monaco @ 2025-03-12 6:57 UTC (permalink / raw)
To: Nam Cao; +Cc: Steven Rostedt, john.ogness, linux-trace-kernel, linux-kernel
On Tue, 2025-03-11 at 18:05 +0100, Nam Cao wrote:
> There are 2 monitors to check realtime applications. Users may want
> to
> enable them both.
>
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
> include/linux/rv.h | 2 +-
> 1 file changed, 1 insertion(+), 1 deletion(-)
>
> diff --git a/include/linux/rv.h b/include/linux/rv.h
> index 6de4f93b390e..224c2194f582 100644
> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -44,7 +44,7 @@ struct ltl_monitor {
> * adding more or developing a dynamic method. So far, none of
> * these are justified.
> */
> -#define RV_PER_TASK_MONITORS 1
> +#define RV_PER_TASK_MONITORS 2
> #define RV_PER_TASK_MONITOR_INIT (RV_PER_TASK_MONITORS)
>
> union rv_task_monitor {
I was thinking this value could be defined in Kconfig. Here you are
adding two monitors that belong with each other, that would fit nicely
with nested monitors [1] (patch waiting for final Ack).
Your monitor (let's call it rtapp) would require 2 slots and you could
enforce that in Kconfig.
Of course you don't have to add it to this series, but just as a heads up.
Cheers,
Gabriele
[1] - https://lore.kernel.org/lkml/20250218123121.253551-5-gmonaco@redhat.com/
^ permalink raw reply [flat|nested] 23+ messages in thread