| Message ID | f57547af5e8c836f5c548f624e61f3e0002ce0b4.1744355018.git.namcao@linutronix.de (mailing list archive) |
|---|---|
| State | New |
| Headers | show |
| Series | RV: Linear temporal logic monitors for RT application | expand |
On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote: > Userspace real-time applications may have design flaws that they > raise > page faults in real-time threads, and thus have unexpected latencies. > > Add an linear temporal logic monitor to detect this scenario. > > 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 > --- > kernel/trace/rv/Kconfig | 1 + > kernel/trace/rv/Makefile | 1 + > kernel/trace/rv/monitors/pagefault/Kconfig | 11 +++ > .../trace/rv/monitors/pagefault/pagefault.c | 83 > +++++++++++++++++++ > .../trace/rv/monitors/pagefault/pagefault.h | 57 +++++++++++++ > .../rv/monitors/pagefault/pagefault_trace.h | 14 ++++ > kernel/trace/rv/rv_trace.h | 1 + > tools/verification/models/rtapp/pagefault.ltl | 1 + > 8 files changed, 169 insertions(+) > create mode 100644 kernel/trace/rv/monitors/pagefault/Kconfig > create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault.c > create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault.h > create mode 100644 > kernel/trace/rv/monitors/pagefault/pagefault_trace.h > create mode 100644 tools/verification/models/rtapp/pagefault.ltl > > diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig > index 5c407d291661..6f86d8501e87 100644 > --- a/kernel/trace/rv/Kconfig > +++ b/kernel/trace/rv/Kconfig > @@ -42,6 +42,7 @@ source "kernel/trace/rv/monitors/scpd/Kconfig" > source "kernel/trace/rv/monitors/snep/Kconfig" > source "kernel/trace/rv/monitors/sncid/Kconfig" > source "kernel/trace/rv/monitors/rtapp/Kconfig" > +source "kernel/trace/rv/monitors/pagefault/Kconfig" > # Add new monitors here > > config RV_REACTORS > diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile > index 9b28c2419995..353ecf939d0e 100644 > --- a/kernel/trace/rv/Makefile > +++ b/kernel/trace/rv/Makefile > @@ -13,6 +13,7 @@ obj-$(CONFIG_RV_MON_SCPD) += monitors/scpd/scpd.o > obj-$(CONFIG_RV_MON_SNEP) += monitors/snep/snep.o > obj-$(CONFIG_RV_MON_SNCID) += monitors/sncid/sncid.o > obj-$(CONFIG_RV_MON_RTAPP) += monitors/rtapp/rtapp.o > +obj-$(CONFIG_RV_MON_PAGEFAULT) += monitors/pagefault/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/pagefault/Kconfig > b/kernel/trace/rv/monitors/pagefault/Kconfig > new file mode 100644 > index 000000000000..b31dee208459 > --- /dev/null > +++ b/kernel/trace/rv/monitors/pagefault/Kconfig > @@ -0,0 +1,11 @@ > +# SPDX-License-Identifier: GPL-2.0-only > +# > +config RV_MON_PAGEFAULT > + depends on RV > + select RV_LTL_MONITOR > + depends on RV_MON_RTAPP > + default y > + select LTL_MON_EVENTS_ID > + bool "pagefault monitor" > + help > + Monitor that real-time tasks do not raise page faults > diff --git a/kernel/trace/rv/monitors/pagefault/pagefault.c > b/kernel/trace/rv/monitors/pagefault/pagefault.c > new file mode 100644 > index 000000000000..9f7a4cba39a1 > --- /dev/null > +++ b/kernel/trace/rv/monitors/pagefault/pagefault.c > @@ -0,0 +1,83 @@ > +// SPDX-License-Identifier: GPL-2.0 > +#include <linux/ftrace.h> > +#include <linux/tracepoint.h> > +#include <linux/kernel.h> > +#include <linux/module.h> > +#include <linux/init.h> > +#include <linux/rv.h> > +#include <rv/instrumentation.h> > + > +#define MODULE_NAME "pagefault" > + > +#include <rv_trace.h> > +#include <trace/events/exceptions.h> > +#include <monitors/rtapp/rtapp.h> > + > +#include "pagefault.h" > +#include <rv/ltl_monitor.h> > + > +static void ltl_atoms_fetch(struct task_struct *task, struct > ltl_monitor *mon) > +{ > + ltl_atom_set(mon, LTL_RT, rt_task(task)); > +} > + > +static void ltl_atoms_init(struct task_struct *task, struct > ltl_monitor *mon, bool task_creation) > +{ > + if (task_creation) > + ltl_atom_set(mon, LTL_PAGEFAULT, false); > +} > + > +static void handle_page_fault(void *data, unsigned long address, > struct pt_regs *regs, > + unsigned long error_code) > +{ > + ltl_atom_pulse(current, LTL_PAGEFAULT, true); > +} > + > +static int enable_pagefault(void) > +{ > + int retval; > + > + retval = ltl_monitor_init(); > + if (retval) > + return retval; > + > + rv_attach_trace_probe("pagefault", page_fault_kernel, > handle_page_fault); > + rv_attach_trace_probe("pagefault", page_fault_user, > handle_page_fault); > + > + return 0; > +} > + > +static void disable_pagefault(void) > +{ > + rv_pagefault.enabled = 0; > + > + rv_detach_trace_probe("rtapp_pagefault", page_fault_kernel, > handle_page_fault); > + rv_detach_trace_probe("rtapp_pagefault", page_fault_user, > handle_page_fault); > + > + ltl_monitor_destroy(); > +} > + > +static struct rv_monitor rv_pagefault = { > + .name = "pagefault", > + .description = "Monitor that RT tasks do not raise page > faults", > + .enable = enable_pagefault, > + .disable = disable_pagefault, > +}; > + > +static int __init register_pagefault(void) > +{ > + rv_register_monitor(&rv_pagefault, &rv_rtapp); > + return 0; Any reason why you aren't returning the error value from the monitor registration? Other than that, the monitor seems neat and reasonably easy to generate. May not be necessary in this series, but try to keep compatibility with the userspace RV tool as well, you need to have some special case in its tracing components because fields are not matching: # rv mon sleep -t rcuc/11-108 [011] event <CANT FIND FIELD final_state> (null) x (null) -> (null) Y rcuc/11-108 [011] event <CANT FIND FIELD final_state> (null) x (null) -> (null) Y ktimers/11-109 [011] event <CANT FIND FIELD final_state> (null) x (null) -> (null) Y Thanks, Gabriele
On Tue, Apr 15, 2025 at 02:31:43PM +0200, Gabriele Monaco wrote: > On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote: > > +static int __init register_pagefault(void) > > +{ > > + rv_register_monitor(&rv_pagefault, &rv_rtapp); > > + return 0; > > Any reason why you aren't returning the error value from the monitor > registration? Copy-paste from dot2k :P > Other than that, the monitor seems neat and reasonably easy to > generate. > > May not be necessary in this series, but try to keep compatibility with > the userspace RV tool as well, you need to have some special case in > its tracing components because fields are not matching: > # rv mon sleep -t > rcuc/11-108 [011] event <CANT FIND FIELD final_state> > (null) x (null) -> (null) Y > rcuc/11-108 [011] event <CANT FIND FIELD final_state> > (null) x (null) -> (null) Y > ktimers/11-109 [011] event <CANT FIND FIELD final_state> > (null) x (null) -> (null) Y I have this userspace RV tool in my "later" TODO list, if that's okay. Honestly, I haven't looked at what it does yet. perf already does what I need. Best regards, Nam
On Tue, 2025-04-15 at 14:38 +0200, Nam Cao wrote: > On Tue, Apr 15, 2025 at 02:31:43PM +0200, Gabriele Monaco wrote: > > On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote: > > > +static int __init register_pagefault(void) > > > +{ > > > + rv_register_monitor(&rv_pagefault, &rv_rtapp); > > > + return 0; > > > > Any reason why you aren't returning the error value from the > > monitor > > registration? > > Copy-paste from dot2k :P Mmh, you're right! All other monitors are broken in this sense.. > > > Other than that, the monitor seems neat and reasonably easy to > > generate. > > > > May not be necessary in this series, but try to keep compatibility > > with > > the userspace RV tool as well, you need to have some special case > > in > > its tracing components because fields are not matching: > > # rv mon sleep -t > > rcuc/11-108 [011] event <CANT FIND FIELD > > final_state> > > (null) x (null) -> (null) Y > > rcuc/11-108 [011] event <CANT FIND FIELD > > final_state> > > (null) x (null) -> (null) Y > > ktimers/11-109 [011] event <CANT FIND FIELD > > final_state> > > (null) x (null) -> (null) Y > > I have this userspace RV tool in my "later" TODO list, if that's > okay. > > Honestly, I haven't looked at what it does yet. perf already does > what I > need. Yeah, no rush, the tool is mostly for enabling the monitor and reactors in a single command, the rest (tracing) you can already do with perf, trace-cmd and friends, after enabling the monitor manually, of course. We may even consider integrating RV in other tools instead of maintaining a separate one, but that's for another day. Thanks, Gabriele
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index 5c407d291661..6f86d8501e87 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -42,6 +42,7 @@ source "kernel/trace/rv/monitors/scpd/Kconfig" source "kernel/trace/rv/monitors/snep/Kconfig" source "kernel/trace/rv/monitors/sncid/Kconfig" source "kernel/trace/rv/monitors/rtapp/Kconfig" +source "kernel/trace/rv/monitors/pagefault/Kconfig" # Add new monitors here config RV_REACTORS diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile index 9b28c2419995..353ecf939d0e 100644 --- a/kernel/trace/rv/Makefile +++ b/kernel/trace/rv/Makefile @@ -13,6 +13,7 @@ obj-$(CONFIG_RV_MON_SCPD) += monitors/scpd/scpd.o obj-$(CONFIG_RV_MON_SNEP) += monitors/snep/snep.o obj-$(CONFIG_RV_MON_SNCID) += monitors/sncid/sncid.o obj-$(CONFIG_RV_MON_RTAPP) += monitors/rtapp/rtapp.o +obj-$(CONFIG_RV_MON_PAGEFAULT) += monitors/pagefault/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/pagefault/Kconfig b/kernel/trace/rv/monitors/pagefault/Kconfig new file mode 100644 index 000000000000..b31dee208459 --- /dev/null +++ b/kernel/trace/rv/monitors/pagefault/Kconfig @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_PAGEFAULT + depends on RV + select RV_LTL_MONITOR + depends on RV_MON_RTAPP + default y + select LTL_MON_EVENTS_ID + bool "pagefault monitor" + help + Monitor that real-time tasks do not raise page faults diff --git a/kernel/trace/rv/monitors/pagefault/pagefault.c b/kernel/trace/rv/monitors/pagefault/pagefault.c new file mode 100644 index 000000000000..9f7a4cba39a1 --- /dev/null +++ b/kernel/trace/rv/monitors/pagefault/pagefault.c @@ -0,0 +1,83 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/ftrace.h> +#include <linux/tracepoint.h> +#include <linux/kernel.h> +#include <linux/module.h> +#include <linux/init.h> +#include <linux/rv.h> +#include <rv/instrumentation.h> + +#define MODULE_NAME "pagefault" + +#include <rv_trace.h> +#include <trace/events/exceptions.h> +#include <monitors/rtapp/rtapp.h> + +#include "pagefault.h" +#include <rv/ltl_monitor.h> + +static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon) +{ + ltl_atom_set(mon, LTL_RT, rt_task(task)); +} + +static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation) +{ + if (task_creation) + ltl_atom_set(mon, LTL_PAGEFAULT, false); +} + +static void handle_page_fault(void *data, unsigned long address, struct pt_regs *regs, + unsigned long error_code) +{ + ltl_atom_pulse(current, LTL_PAGEFAULT, true); +} + +static int enable_pagefault(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("pagefault", page_fault_kernel, handle_page_fault); + rv_attach_trace_probe("pagefault", page_fault_user, handle_page_fault); + + return 0; +} + +static void disable_pagefault(void) +{ + rv_pagefault.enabled = 0; + + rv_detach_trace_probe("rtapp_pagefault", page_fault_kernel, handle_page_fault); + rv_detach_trace_probe("rtapp_pagefault", page_fault_user, handle_page_fault); + + ltl_monitor_destroy(); +} + +static struct rv_monitor rv_pagefault = { + .name = "pagefault", + .description = "Monitor that RT tasks do not raise page faults", + .enable = enable_pagefault, + .disable = disable_pagefault, +}; + +static int __init register_pagefault(void) +{ + rv_register_monitor(&rv_pagefault, &rv_rtapp); + return 0; +} + +static void __exit unregister_pagefault(void) +{ + rv_unregister_monitor(&rv_pagefault); +} + +module_init(register_pagefault); +module_exit(unregister_pagefault); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Nam Cao <namcao@linutronix.de>"); +MODULE_DESCRIPTION("pagefault: Monitor that RT tasks do not raise page faults"); diff --git a/kernel/trace/rv/monitors/pagefault/pagefault.h b/kernel/trace/rv/monitors/pagefault/pagefault.h new file mode 100644 index 000000000000..f4535c83f7d1 --- /dev/null +++ b/kernel/trace/rv/monitors/pagefault/pagefault.h @@ -0,0 +1,57 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +#include <linux/rv.h> + +#define MONITOR_NAME pagefault + +enum ltl_atom { + LTL_PAGEFAULT, + LTL_RT, + LTL_NUM_ATOM +}; +static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); + +static const char *ltl_atom_str(enum ltl_atom atom) +{ + static const char *const names[] = { + "p", + "r", + }; + + return names[atom]; +} + +enum ltl_buchi_state { + S0, + RV_NUM_BA_STATES +}; +static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); + +static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) +{ + bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms); + bool val3 = !pagefault; + bool rt = test_bit(LTL_RT, mon->atoms); + bool val1 = !rt; + bool val4 = val1 || val3; + + if (val4) + __set_bit(S0, mon->states); +} + +static void +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) +{ + bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms); + bool val3 = !pagefault; + bool rt = test_bit(LTL_RT, mon->atoms); + bool val1 = !rt; + bool val4 = val1 || val3; + + switch (state) { + case S0: + if (val4) + __set_bit(S0, next); + break; + } +} diff --git a/kernel/trace/rv/monitors/pagefault/pagefault_trace.h b/kernel/trace/rv/monitors/pagefault/pagefault_trace.h new file mode 100644 index 000000000000..fe1f82597b1a --- /dev/null +++ b/kernel/trace/rv/monitors/pagefault/pagefault_trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_PAGEFAULT +DEFINE_EVENT(event_ltl_monitor_id, event_pagefault, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_ltl_monitor_id, error_pagefault, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_PAGEFAULT */ diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h index f9fb848bae91..02c906c9745b 100644 --- a/kernel/trace/rv/rv_trace.h +++ b/kernel/trace/rv/rv_trace.h @@ -172,6 +172,7 @@ TRACE_EVENT(error_ltl_monitor_id, TP_printk("%s[%d]: violation detected", __get_str(comm), __entry->pid) ); +#include <monitors/pagefault/pagefault_trace.h> // Add new monitors based on CONFIG_LTL_MON_EVENTS_ID here #endif /* CONFIG_LTL_MON_EVENTS_ID */ #endif /* _TRACE_RV_H */ diff --git a/tools/verification/models/rtapp/pagefault.ltl b/tools/verification/models/rtapp/pagefault.ltl new file mode 100644 index 000000000000..d7ce62102733 --- /dev/null +++ b/tools/verification/models/rtapp/pagefault.ltl @@ -0,0 +1 @@ +RULE = always (RT imply not PAGEFAULT)
Userspace real-time applications may have design flaws that they raise page faults in real-time threads, and thus have unexpected latencies. Add an linear temporal logic monitor to detect this scenario. 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 --- kernel/trace/rv/Kconfig | 1 + kernel/trace/rv/Makefile | 1 + kernel/trace/rv/monitors/pagefault/Kconfig | 11 +++ .../trace/rv/monitors/pagefault/pagefault.c | 83 +++++++++++++++++++ .../trace/rv/monitors/pagefault/pagefault.h | 57 +++++++++++++ .../rv/monitors/pagefault/pagefault_trace.h | 14 ++++ kernel/trace/rv/rv_trace.h | 1 + tools/verification/models/rtapp/pagefault.ltl | 1 + 8 files changed, 169 insertions(+) create mode 100644 kernel/trace/rv/monitors/pagefault/Kconfig create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault.c create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault.h create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault_trace.h create mode 100644 tools/verification/models/rtapp/pagefault.ltl