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>
---
kernel/trace/rv/Kconfig | 1 +
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/monitors/pagefault/Kconfig | 11 +++
.../trace/rv/monitors/pagefault/pagefault.c | 82 +++++++++++++++++++
.../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, 168 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..ff7df49871b2
--- /dev/null
+++ b/kernel/trace/rv/monitors/pagefault/pagefault.c
@@ -0,0 +1,82 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/init.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/rv.h>
+#include <linux/sched/deadline.h>
+#include <linux/sched/rt.h>
+#include <linux/tracepoint.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_or_dl_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("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_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);
+
+ 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)
+{
+ return rv_register_monitor(&rv_pagefault, &rv_rtapp);
+}
+
+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..94c0fe4fdaa5
--- /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[] = {
+ "pa",
+ "rt",
+ };
+
+ 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)
--
2.39.5
On Wed, 2025-04-23 at 08:50 +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>
> ---
> kernel/trace/rv/Kconfig | 1 +
> kernel/trace/rv/Makefile | 1 +
> kernel/trace/rv/monitors/pagefault/Kconfig | 11 +++
> .../trace/rv/monitors/pagefault/pagefault.c | 82
> +++++++++++++++++++
> .../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, 168 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..ff7df49871b2
> --- /dev/null
> +++ b/kernel/trace/rv/monitors/pagefault/pagefault.c
> @@ -0,0 +1,82 @@
> +// SPDX-License-Identifier: GPL-2.0
> +#include <linux/ftrace.h>
> +#include <linux/init.h>
> +#include <linux/kernel.h>
> +#include <linux/module.h>
> +#include <linux/rv.h>
> +#include <linux/sched/deadline.h>
> +#include <linux/sched/rt.h>
> +#include <linux/tracepoint.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_or_dl_task(task));
> +}
Mmh, you probably already considered that, so ignore my comment in that case.
I just realised this function would tell you a PI boosted task is an RT task,
is that acceptable in your model?
It's probably a configuration mistake on its own if an RT task following those
rules shares resources with non-RT tasks not following them, but if that's
something allowed, you may see this atom change more often than you'd like, not
sure if that can be something worth noting.
Perhaps you could add a comment saying that this is not a problem and why (e.g.
instead of using rt_or_dl_task_policy for the job).
What do you think?
Besides this detail, the monitor looks good to me
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Thanks,
Gabriele
On Wed, Apr 23, 2025 at 12:37:53PM +0200, Gabriele Monaco wrote:
> On Wed, 2025-04-23 at 08:50 +0200, Nam Cao wrote:
> > +static void ltl_atoms_fetch(struct task_struct *task, struct
> > ltl_monitor *mon)
> > +{
> > + ltl_atom_set(mon, LTL_RT, rt_or_dl_task(task));
> > +}
>
> Mmh, you probably already considered that, so ignore my comment in that case.
>
> I just realised this function would tell you a PI boosted task is an RT task,
> is that acceptable in your model?
Yes, that is intentional. A task being PI boosted means an "actual"
real-time task is waiting for it. Therefore the PI boosted task shouldn't
be delayed, otherwise the "actual" real-time task is delayed.
> It's probably a configuration mistake on its own if an RT task following those
> rules shares resources with non-RT tasks not following them,
non-RT tasks do not have to follow the rules all the time. But while
accessing resources shared with RT tasks, then yes the rules should be
obeyed.
> but if that's something allowed, you may see this atom change more often
> than you'd like, not sure if that can be something worth noting.
>
> Perhaps you could add a comment saying that this is not a problem and why (e.g.
> instead of using rt_or_dl_task_policy for the job).
Sure, a comment doesn't hurt.
> What do you think?
>
> Besides this detail, the monitor looks good to me
> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Thanks so much for the review!
Nam
© 2016 - 2025 Red Hat, Inc.