Add "real-time scheduling" monitor, which validates that SCHED_RR and
SCHED_FIFO tasks are scheduled before tasks with normal and extensible
scheduling policies

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Juri Lelli <juri.lelli@redhat.com>
Cc: Vincent Guittot <vincent.guittot@linaro.org>
Cc: Dietmar Eggemann <dietmar.eggemann@arm.com>
Cc: Ben Segall <bsegall@google.com>
Cc: Mel Gorman <mgorman@suse.de>
Cc: Valentin Schneider <vschneid@redhat.com>
---
 Documentation/trace/rv/monitor_sched.rst |  19 ++++
 kernel/trace/rv/Kconfig                  |   1 +
 kernel/trace/rv/Makefile                 |   1 +
 kernel/trace/rv/monitors/rts/Kconfig     |  17 +++
 kernel/trace/rv/monitors/rts/rts.c       | 131 +++++++++++++++++++++++
 kernel/trace/rv/monitors/rts/rts.h       | 126 ++++++++++++++++++++++
 kernel/trace/rv/monitors/rts/rts_trace.h |  15 +++
 tools/verification/models/sched/rts.ltl  |   5 +
 8 files changed, 315 insertions(+)
 create mode 100644 kernel/trace/rv/monitors/rts/Kconfig
 create mode 100644 kernel/trace/rv/monitors/rts/rts.c
 create mode 100644 kernel/trace/rv/monitors/rts/rts.h
 create mode 100644 kernel/trace/rv/monitors/rts/rts_trace.h
 create mode 100644 tools/verification/models/sched/rts.ltl

diff --git a/Documentation/trace/rv/monitor_sched.rst b/Documentation/trace/rv/monitor_sched.rst
index 3f8381ad9ec7..2f9d62a1af1f 100644
--- a/Documentation/trace/rv/monitor_sched.rst
+++ b/Documentation/trace/rv/monitor_sched.rst
@@ -396,6 +396,25 @@ preemption is always disabled. On non- ``PREEMPT_RT`` kernels, the interrupts
 might invoke a softirq to set ``need_resched`` and wake up a task. This is
 another special case that is currently not supported by the monitor.
 
+Monitor rts
+-----------
+
+The real-time scheduling monitor validates that tasks with real-time scheduling
+policies (`SCHED_FIFO` and `SCHED_RR`) are always scheduled before tasks with
+normal and extensible scheduling policies (`SCHED_OTHER`, `SCHED_BATCH`,
+`SCHED_IDLE`, `SCHED_EXT`):
+
+.. literalinclude:: ../../../tools/verification/models/sched/rts.ltl
+
+Note that this monitor may report errors if real-time throttling or fair
+deadline server is enabled. These mechanisms prevent real-time tasks from
+monopolying the CPU by giving tasks with normal and extensible scheduling
+policies a chance to run. They give system administrators a chance to kill a
+misbehaved real-time task. However, they violate the scheduling priorities and
+may cause latency to well-behaved real-time tasks. Thus, if you see errors from
+this monitor, consider disabling real-time throttling and the fair deadline
+server.
+
 References
 ----------
 
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 951c2e0cda25..3992ff6ac8b1 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -62,6 +62,7 @@ source "kernel/trace/rv/monitors/sts/Kconfig"
 source "kernel/trace/rv/monitors/nrp/Kconfig"
 source "kernel/trace/rv/monitors/sssw/Kconfig"
 source "kernel/trace/rv/monitors/opid/Kconfig"
+source "kernel/trace/rv/monitors/rts/Kconfig"
 # Add new sched monitors here
 
 source "kernel/trace/rv/monitors/rtapp/Kconfig"
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index 750e4ad6fa0f..d7bfc7ae6677 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -17,6 +17,7 @@ obj-$(CONFIG_RV_MON_STS) += monitors/sts/sts.o
 obj-$(CONFIG_RV_MON_NRP) += monitors/nrp/nrp.o
 obj-$(CONFIG_RV_MON_SSSW) += monitors/sssw/sssw.o
 obj-$(CONFIG_RV_MON_OPID) += monitors/opid/opid.o
+obj-$(CONFIG_RV_MON_RTS) += monitors/rts/rts.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/rts/Kconfig b/kernel/trace/rv/monitors/rts/Kconfig
new file mode 100644
index 000000000000..1b780bce6133
--- /dev/null
+++ b/kernel/trace/rv/monitors/rts/Kconfig
@@ -0,0 +1,17 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_RTS
+	depends on RV
+	select RV_LTL_MONITOR
+	depends on RV_MON_SCHED
+	default y
+	select LTL_MON_EVENTS_IMPLICIT
+	bool "rts monitor"
+	help
+	  Add support for RTS (real-time scheduling) monitor which validates
+	  that real-time-priority tasks are scheduled before SCHED_OTHER tasks.
+
+	  This monitor may report an error if RT throttling or deadline server
+	  is enabled.
+
+	  Say Y if you are debugging or testing a real-time system.
diff --git a/kernel/trace/rv/monitors/rts/rts.c b/kernel/trace/rv/monitors/rts/rts.c
new file mode 100644
index 000000000000..e23563c47eb1
--- /dev/null
+++ b/kernel/trace/rv/monitors/rts/rts.c
@@ -0,0 +1,131 @@
+// 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 <linux/sched/deadline.h>
+#include <linux/sched/rt.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "rts"
+
+#include <trace/events/sched.h>
+#include <rv_trace.h>
+#include <monitors/sched/sched.h>
+
+#include "rts.h"
+#include <rv/ltl_monitor.h>
+
+static DEFINE_PER_CPU(unsigned int, nr_queued);
+
+static void ltl_atoms_fetch(unsigned int cpu, struct ltl_monitor *mon)
+{
+}
+
+static void ltl_atoms_init(unsigned int cpu, struct ltl_monitor *mon,
+			   bool target_creation)
+{
+	ltl_atom_set(mon, LTL_SCHED_SWITCH, false);
+	ltl_atom_set(mon, LTL_SCHED_SWITCH_DL, false);
+	ltl_atom_set(mon, LTL_SCHED_SWITCH_RT, false);
+
+	/*
+	 * This may not be accurate, there may be enqueued RT tasks. But that's
+	 * okay, the worst we get is a false negative. It will be accurate as
+	 * soon as the CPU no longer has any queued RT task.
+	 */
+	ltl_atom_set(mon, LTL_RT_TASK_ENQUEUED, false);
+}
+
+static void handle_enqueue_task_rt(void *data, int cpu, struct task_struct *task)
+{
+	unsigned int *queued = per_cpu_ptr(&nr_queued, cpu);
+
+	(*queued)++;
+	ltl_atom_update(cpu, LTL_RT_TASK_ENQUEUED, true);
+}
+
+static void handle_dequeue_task_rt(void *data, int cpu, struct task_struct *task)
+{
+	unsigned int *queued = per_cpu_ptr(&nr_queued, cpu);
+
+	/*
+	 * This may not be accurate for a short time after the monitor is
+	 * enabled, because there may be enqueued RT tasks which are not counted
+	 * torward nr_queued. But that's okay, the worst we get is a false
+	 * negative. nr_queued will be accurate as soon as the CPU no longer has
+	 * any queued RT task.
+	 */
+	if (*queued)
+		(*queued)--;
+	if (!*queued)
+		ltl_atom_update(cpu, LTL_RT_TASK_ENQUEUED, false);
+}
+
+static void handle_sched_switch(void *data, bool preempt, struct task_struct *prev,
+				struct task_struct *next, unsigned int prev_state)
+{
+	unsigned int cpu = smp_processor_id();
+	struct ltl_monitor *mon = ltl_get_monitor(cpu);
+
+	ltl_atom_set(mon, LTL_SCHED_SWITCH_RT, rt_task(next));
+	ltl_atom_set(mon, LTL_SCHED_SWITCH_DL, dl_task(next));
+	ltl_atom_update(cpu, LTL_SCHED_SWITCH, true);
+
+	ltl_atom_set(mon, LTL_SCHED_SWITCH_RT, false);
+	ltl_atom_set(mon, LTL_SCHED_SWITCH_DL, false);
+	ltl_atom_update(cpu, LTL_SCHED_SWITCH, false);
+}
+
+static int enable_rts(void)
+{
+	int retval;
+
+	retval = ltl_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("rts", enqueue_task_rt_tp, handle_enqueue_task_rt);
+	rv_attach_trace_probe("rts", dequeue_task_rt_tp, handle_dequeue_task_rt);
+	rv_attach_trace_probe("rts", sched_switch, handle_sched_switch);
+
+	return 0;
+}
+
+static void disable_rts(void)
+{
+	rv_detach_trace_probe("rts", enqueue_task_rt_tp, handle_enqueue_task_rt);
+	rv_detach_trace_probe("rts", dequeue_task_rt_tp, handle_dequeue_task_rt);
+	rv_detach_trace_probe("rts", sched_switch, handle_sched_switch);
+
+	ltl_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_rts = {
+	.name = "rts",
+	.description = "Validate that real-time tasks are scheduled before lower-priority tasks",
+	.enable = enable_rts,
+	.disable = disable_rts,
+};
+
+static int __init register_rts(void)
+{
+	return rv_register_monitor(&rv_rts, &rv_sched);
+}
+
+static void __exit unregister_rts(void)
+{
+	rv_unregister_monitor(&rv_rts);
+}
+
+module_init(register_rts);
+module_exit(unregister_rts);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Nam Cao <namcao@linutronix.de>");
+MODULE_DESCRIPTION("rts: Validate that real-time tasks are scheduled before lower-priority tasks");
diff --git a/kernel/trace/rv/monitors/rts/rts.h b/kernel/trace/rv/monitors/rts/rts.h
new file mode 100644
index 000000000000..9fbf0d97c1a7
--- /dev/null
+++ b/kernel/trace/rv/monitors/rts/rts.h
@@ -0,0 +1,126 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * C implementation of Buchi automaton, automatically generated by
+ * tools/verification/rvgen from the linear temporal logic specification.
+ * For further information, see kernel documentation:
+ *   Documentation/trace/rv/linear_temporal_logic.rst
+ */
+
+#include <linux/rv.h>
+
+#define MONITOR_NAME rts
+
+#define LTL_MONITOR_TYPE LTL_CPU_MONITOR
+
+enum ltl_atom {
+	LTL_RT_TASK_ENQUEUED,
+	LTL_SCHED_SWITCH,
+	LTL_SCHED_SWITCH_DL,
+	LTL_SCHED_SWITCH_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[] = {
+		"rt_ta_en",
+		"sc_sw",
+		"sc_sw_dl",
+		"sc_sw_rt",
+	};
+
+	return names[atom];
+}
+
+enum ltl_buchi_state {
+	S0,
+	S1,
+	S2,
+	S3,
+	S4,
+	RV_NUM_BA_STATES
+};
+static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
+
+static void ltl_start(unsigned int cpu, struct ltl_monitor *mon)
+{
+	bool sched_switch_rt = test_bit(LTL_SCHED_SWITCH_RT, mon->atoms);
+	bool sched_switch_dl = test_bit(LTL_SCHED_SWITCH_DL, mon->atoms);
+	bool sched_switch = test_bit(LTL_SCHED_SWITCH, mon->atoms);
+	bool rt_task_enqueued = test_bit(LTL_RT_TASK_ENQUEUED, mon->atoms);
+	bool val13 = !rt_task_enqueued;
+	bool val8 = sched_switch_dl || val13;
+	bool val9 = sched_switch_rt || val8;
+	bool val6 = !sched_switch;
+	bool val1 = !rt_task_enqueued;
+
+	if (val1)
+		__set_bit(S0, mon->states);
+	if (val6)
+		__set_bit(S1, mon->states);
+	if (val9)
+		__set_bit(S4, mon->states);
+}
+
+static void
+ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
+{
+	bool sched_switch_rt = test_bit(LTL_SCHED_SWITCH_RT, mon->atoms);
+	bool sched_switch_dl = test_bit(LTL_SCHED_SWITCH_DL, mon->atoms);
+	bool sched_switch = test_bit(LTL_SCHED_SWITCH, mon->atoms);
+	bool rt_task_enqueued = test_bit(LTL_RT_TASK_ENQUEUED, mon->atoms);
+	bool val13 = !rt_task_enqueued;
+	bool val8 = sched_switch_dl || val13;
+	bool val9 = sched_switch_rt || val8;
+	bool val6 = !sched_switch;
+	bool val1 = !rt_task_enqueued;
+
+	switch (state) {
+	case S0:
+		if (val1)
+			__set_bit(S0, next);
+		if (val6)
+			__set_bit(S1, next);
+		if (val9)
+			__set_bit(S4, next);
+		break;
+	case S1:
+		if (val6)
+			__set_bit(S1, next);
+		if (val1 && val6)
+			__set_bit(S2, next);
+		if (val1 && val9)
+			__set_bit(S3, next);
+		if (val9)
+			__set_bit(S4, next);
+		break;
+	case S2:
+		if (val6)
+			__set_bit(S1, next);
+		if (val1 && val6)
+			__set_bit(S2, next);
+		if (val1 && val9)
+			__set_bit(S3, next);
+		if (val9)
+			__set_bit(S4, next);
+		break;
+	case S3:
+		if (val1)
+			__set_bit(S0, next);
+		if (val6)
+			__set_bit(S1, next);
+		if (val9)
+			__set_bit(S4, next);
+		break;
+	case S4:
+		if (val1)
+			__set_bit(S0, next);
+		if (val6)
+			__set_bit(S1, next);
+		if (val9)
+			__set_bit(S4, next);
+		break;
+	}
+}
diff --git a/kernel/trace/rv/monitors/rts/rts_trace.h b/kernel/trace/rv/monitors/rts/rts_trace.h
new file mode 100644
index 000000000000..0ac9e112a8b0
--- /dev/null
+++ b/kernel/trace/rv/monitors/rts/rts_trace.h
@@ -0,0 +1,15 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_RTS
+DEFINE_EVENT(event_ltl_monitor, event_rts,
+	TP_PROTO(unsigned int cpu, char *states, char *atoms, char *next),
+	TP_ARGS(cpu, states, atoms, next));
+
+DEFINE_EVENT(error_ltl_monitor, error_rts,
+	TP_PROTO(unsigned int cpu),
+	TP_ARGS(cpu));
+#endif /* CONFIG_RV_MON_RTS */
diff --git a/tools/verification/models/sched/rts.ltl b/tools/verification/models/sched/rts.ltl
new file mode 100644
index 000000000000..90872bca46b1
--- /dev/null
+++ b/tools/verification/models/sched/rts.ltl
@@ -0,0 +1,5 @@
+RULE = always (RT_TASK_ENQUEUED imply SCHEDULE_RT_NEXT)
+
+SCHEDULE_RT_NEXT = (not SCHED_SWITCH) until (SCHED_SWITCH_RT or EXCEPTIONS)
+
+EXCEPTIONS = SCHED_SWITCH_DL or not RT_TASK_ENQUEUED
-- 
2.39.5

On Wed, 2025-07-30 at 14:45 +0200, Nam Cao wrote:
> Add "real-time scheduling" monitor, which validates that SCHED_RR and
> SCHED_FIFO tasks are scheduled before tasks with normal and
> extensible
> scheduling policies
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>

Hello Nam,

I just built and booted up the monitor in a VM (virtme-ng), the
configuration has preemptirq tracepoints and all monitors so far (as we
have seen earlier, it doesn't build if rtapp monitors are not there
because of the circular dependency in the tracepoints).

All I did was to enable the monitor and printk reactor, but I get a
whole lot of errors (as in, I need to quit the VM for it to stop):

[ 1537.699834] rv: rts: 7: violation detected
[ 1537.699930] rv: rts: 3: violation detected
[ 1537.701827] rv: rts: 6: violation detected
[ 1537.704894] rv: rts: 0: violation detected
[ 1537.704925] rv: rts: 0: violation detected
[ 1537.704988] rv: rts: 3: violation detected
[ 1537.705019] rv: rts: 3: violation detected
[ 1537.705998] rv: rts: 0: violation detected
[ 1537.706024] rv: rts: 0: violation detected
[ 1537.709875] rv: rts: 6: violation detected
[ 1537.709921] rv: rts: 6: violation detected
[ 1537.711241] rv: rts: 6: violation detected

Curiously enough, I only see those CPUs (0, 3, 6 and 7).
Other runs have different CPUs but always a small subset (e.g. 10-15,
6-7 only 2).
It doesn't always occur but enabling/disabling the monitor might help
triggering it.

Any idea what is happening?

Thanks,
Gabriele

> ---
> Cc: Ingo Molnar <mingo@redhat.com>
> Cc: Peter Zijlstra <peterz@infradead.org>
> Cc: Juri Lelli <juri.lelli@redhat.com>
> Cc: Vincent Guittot <vincent.guittot@linaro.org>
> Cc: Dietmar Eggemann <dietmar.eggemann@arm.com>
> Cc: Ben Segall <bsegall@google.com>
> Cc: Mel Gorman <mgorman@suse.de>
> Cc: Valentin Schneider <vschneid@redhat.com>
> ---
>  Documentation/trace/rv/monitor_sched.rst |  19 ++++
>  kernel/trace/rv/Kconfig                  |   1 +
>  kernel/trace/rv/Makefile                 |   1 +
>  kernel/trace/rv/monitors/rts/Kconfig     |  17 +++
>  kernel/trace/rv/monitors/rts/rts.c       | 131
> +++++++++++++++++++++++
>  kernel/trace/rv/monitors/rts/rts.h       | 126
> ++++++++++++++++++++++
>  kernel/trace/rv/monitors/rts/rts_trace.h |  15 +++
>  tools/verification/models/sched/rts.ltl  |   5 +
>  8 files changed, 315 insertions(+)
>  create mode 100644 kernel/trace/rv/monitors/rts/Kconfig
>  create mode 100644 kernel/trace/rv/monitors/rts/rts.c
>  create mode 100644 kernel/trace/rv/monitors/rts/rts.h
>  create mode 100644 kernel/trace/rv/monitors/rts/rts_trace.h
>  create mode 100644 tools/verification/models/sched/rts.ltl
> 
> diff --git a/Documentation/trace/rv/monitor_sched.rst
> b/Documentation/trace/rv/monitor_sched.rst
> index 3f8381ad9ec7..2f9d62a1af1f 100644
> --- a/Documentation/trace/rv/monitor_sched.rst
> +++ b/Documentation/trace/rv/monitor_sched.rst
> @@ -396,6 +396,25 @@ preemption is always disabled. On non-
> ``PREEMPT_RT`` kernels, the interrupts
>  might invoke a softirq to set ``need_resched`` and wake up a task.
> This is
>  another special case that is currently not supported by the monitor.
>  
> +Monitor rts
> +-----------
> +
> +The real-time scheduling monitor validates that tasks with real-time
> scheduling
> +policies (`SCHED_FIFO` and `SCHED_RR`) are always scheduled before
> tasks with
> +normal and extensible scheduling policies (`SCHED_OTHER`,
> `SCHED_BATCH`,
> +`SCHED_IDLE`, `SCHED_EXT`):
> +
> +.. literalinclude:: ../../../tools/verification/models/sched/rts.ltl
> +
> +Note that this monitor may report errors if real-time throttling or
> fair
> +deadline server is enabled. These mechanisms prevent real-time tasks
> from
> +monopolying the CPU by giving tasks with normal and extensible
> scheduling
> +policies a chance to run. They give system administrators a chance
> to kill a
> +misbehaved real-time task. However, they violate the scheduling
> priorities and
> +may cause latency to well-behaved real-time tasks. Thus, if you see
> errors from
> +this monitor, consider disabling real-time throttling and the fair
> deadline
> +server.
> +
>  References
>  ----------
>  
> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
> index 951c2e0cda25..3992ff6ac8b1 100644
> --- a/kernel/trace/rv/Kconfig
> +++ b/kernel/trace/rv/Kconfig
> @@ -62,6 +62,7 @@ source "kernel/trace/rv/monitors/sts/Kconfig"
>  source "kernel/trace/rv/monitors/nrp/Kconfig"
>  source "kernel/trace/rv/monitors/sssw/Kconfig"
>  source "kernel/trace/rv/monitors/opid/Kconfig"
> +source "kernel/trace/rv/monitors/rts/Kconfig"
>  # Add new sched monitors here
>  
>  source "kernel/trace/rv/monitors/rtapp/Kconfig"
> diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
> index 750e4ad6fa0f..d7bfc7ae6677 100644
> --- a/kernel/trace/rv/Makefile
> +++ b/kernel/trace/rv/Makefile
> @@ -17,6 +17,7 @@ obj-$(CONFIG_RV_MON_STS) += monitors/sts/sts.o
>  obj-$(CONFIG_RV_MON_NRP) += monitors/nrp/nrp.o
>  obj-$(CONFIG_RV_MON_SSSW) += monitors/sssw/sssw.o
>  obj-$(CONFIG_RV_MON_OPID) += monitors/opid/opid.o
> +obj-$(CONFIG_RV_MON_RTS) += monitors/rts/rts.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/rts/Kconfig
> b/kernel/trace/rv/monitors/rts/Kconfig
> new file mode 100644
> index 000000000000..1b780bce6133
> --- /dev/null
> +++ b/kernel/trace/rv/monitors/rts/Kconfig
> @@ -0,0 +1,17 @@
> +# SPDX-License-Identifier: GPL-2.0-only
> +#
> +config RV_MON_RTS
> +	depends on RV
> +	select RV_LTL_MONITOR
> +	depends on RV_MON_SCHED
> +	default y
> +	select LTL_MON_EVENTS_IMPLICIT
> +	bool "rts monitor"
> +	help
> +	  Add support for RTS (real-time scheduling) monitor which
> validates
> +	  that real-time-priority tasks are scheduled before
> SCHED_OTHER tasks.
> +
> +	  This monitor may report an error if RT throttling or
> deadline server
> +	  is enabled.
> +
> +	  Say Y if you are debugging or testing a real-time system.
> diff --git a/kernel/trace/rv/monitors/rts/rts.c
> b/kernel/trace/rv/monitors/rts/rts.c
> new file mode 100644
> index 000000000000..e23563c47eb1
> --- /dev/null
> +++ b/kernel/trace/rv/monitors/rts/rts.c
> @@ -0,0 +1,131 @@
> +// 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 <linux/sched/deadline.h>
> +#include <linux/sched/rt.h>
> +#include <rv/instrumentation.h>
> +
> +#define MODULE_NAME "rts"
> +
> +#include <trace/events/sched.h>
> +#include <rv_trace.h>
> +#include <monitors/sched/sched.h>
> +
> +#include "rts.h"
> +#include <rv/ltl_monitor.h>
> +
> +static DEFINE_PER_CPU(unsigned int, nr_queued);
> +
> +static void ltl_atoms_fetch(unsigned int cpu, struct ltl_monitor
> *mon)
> +{
> +}
> +
> +static void ltl_atoms_init(unsigned int cpu, struct ltl_monitor
> *mon,
> +			   bool target_creation)
> +{
> +	ltl_atom_set(mon, LTL_SCHED_SWITCH, false);
> +	ltl_atom_set(mon, LTL_SCHED_SWITCH_DL, false);
> +	ltl_atom_set(mon, LTL_SCHED_SWITCH_RT, false);
> +
> +	/*
> +	 * This may not be accurate, there may be enqueued RT tasks.
> But that's
> +	 * okay, the worst we get is a false negative. It will be
> accurate as
> +	 * soon as the CPU no longer has any queued RT task.
> +	 */
> +	ltl_atom_set(mon, LTL_RT_TASK_ENQUEUED, false);
> +}
> +
> +static void handle_enqueue_task_rt(void *data, int cpu, struct
> task_struct *task)
> +{
> +	unsigned int *queued = per_cpu_ptr(&nr_queued, cpu);
> +
> +	(*queued)++;
> +	ltl_atom_update(cpu, LTL_RT_TASK_ENQUEUED, true);
> +}
> +
> +static void handle_dequeue_task_rt(void *data, int cpu, struct
> task_struct *task)
> +{
> +	unsigned int *queued = per_cpu_ptr(&nr_queued, cpu);
> +
> +	/*
> +	 * This may not be accurate for a short time after the
> monitor is
> +	 * enabled, because there may be enqueued RT tasks which are
> not counted
> +	 * torward nr_queued. But that's okay, the worst we get is a
> false
> +	 * negative. nr_queued will be accurate as soon as the CPU
> no longer has
> +	 * any queued RT task.
> +	 */
> +	if (*queued)
> +		(*queued)--;
> +	if (!*queued)
> +		ltl_atom_update(cpu, LTL_RT_TASK_ENQUEUED, false);
> +}
> +
> +static void handle_sched_switch(void *data, bool preempt, struct
> task_struct *prev,
> +				struct task_struct *next, unsigned
> int prev_state)
> +{
> +	unsigned int cpu = smp_processor_id();
> +	struct ltl_monitor *mon = ltl_get_monitor(cpu);
> +
> +	ltl_atom_set(mon, LTL_SCHED_SWITCH_RT, rt_task(next));
> +	ltl_atom_set(mon, LTL_SCHED_SWITCH_DL, dl_task(next));
> +	ltl_atom_update(cpu, LTL_SCHED_SWITCH, true);
> +
> +	ltl_atom_set(mon, LTL_SCHED_SWITCH_RT, false);
> +	ltl_atom_set(mon, LTL_SCHED_SWITCH_DL, false);
> +	ltl_atom_update(cpu, LTL_SCHED_SWITCH, false);
> +}
> +
> +static int enable_rts(void)
> +{
> +	int retval;
> +
> +	retval = ltl_monitor_init();
> +	if (retval)
> +		return retval;
> +
> +	rv_attach_trace_probe("rts", enqueue_task_rt_tp,
> handle_enqueue_task_rt);
> +	rv_attach_trace_probe("rts", dequeue_task_rt_tp,
> handle_dequeue_task_rt);
> +	rv_attach_trace_probe("rts", sched_switch,
> handle_sched_switch);
> +
> +	return 0;
> +}
> +
> +static void disable_rts(void)
> +{
> +	rv_detach_trace_probe("rts", enqueue_task_rt_tp,
> handle_enqueue_task_rt);
> +	rv_detach_trace_probe("rts", dequeue_task_rt_tp,
> handle_dequeue_task_rt);
> +	rv_detach_trace_probe("rts", sched_switch,
> handle_sched_switch);
> +
> +	ltl_monitor_destroy();
> +}
> +
> +/*
> + * This is the monitor register section.
> + */
> +static struct rv_monitor rv_rts = {
> +	.name = "rts",
> +	.description = "Validate that real-time tasks are scheduled
> before lower-priority tasks",
> +	.enable = enable_rts,
> +	.disable = disable_rts,
> +};
> +
> +static int __init register_rts(void)
> +{
> +	return rv_register_monitor(&rv_rts, &rv_sched);
> +}
> +
> +static void __exit unregister_rts(void)
> +{
> +	rv_unregister_monitor(&rv_rts);
> +}
> +
> +module_init(register_rts);
> +module_exit(unregister_rts);
> +
> +MODULE_LICENSE("GPL");
> +MODULE_AUTHOR("Nam Cao <namcao@linutronix.de>");
> +MODULE_DESCRIPTION("rts: Validate that real-time tasks are scheduled
> before lower-priority tasks");
> diff --git a/kernel/trace/rv/monitors/rts/rts.h
> b/kernel/trace/rv/monitors/rts/rts.h
> new file mode 100644
> index 000000000000..9fbf0d97c1a7
> --- /dev/null
> +++ b/kernel/trace/rv/monitors/rts/rts.h
> @@ -0,0 +1,126 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +
> +/*
> + * C implementation of Buchi automaton, automatically generated by
> + * tools/verification/rvgen from the linear temporal logic
> specification.
> + * For further information, see kernel documentation:
> + *   Documentation/trace/rv/linear_temporal_logic.rst
> + */
> +
> +#include <linux/rv.h>
> +
> +#define MONITOR_NAME rts
> +
> +#define LTL_MONITOR_TYPE LTL_CPU_MONITOR
> +
> +enum ltl_atom {
> +	LTL_RT_TASK_ENQUEUED,
> +	LTL_SCHED_SWITCH,
> +	LTL_SCHED_SWITCH_DL,
> +	LTL_SCHED_SWITCH_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[] = {
> +		"rt_ta_en",
> +		"sc_sw",
> +		"sc_sw_dl",
> +		"sc_sw_rt",
> +	};
> +
> +	return names[atom];
> +}
> +
> +enum ltl_buchi_state {
> +	S0,
> +	S1,
> +	S2,
> +	S3,
> +	S4,
> +	RV_NUM_BA_STATES
> +};
> +static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
> +
> +static void ltl_start(unsigned int cpu, struct ltl_monitor *mon)
> +{
> +	bool sched_switch_rt = test_bit(LTL_SCHED_SWITCH_RT, mon-
> >atoms);
> +	bool sched_switch_dl = test_bit(LTL_SCHED_SWITCH_DL, mon-
> >atoms);
> +	bool sched_switch = test_bit(LTL_SCHED_SWITCH, mon->atoms);
> +	bool rt_task_enqueued = test_bit(LTL_RT_TASK_ENQUEUED, mon-
> >atoms);
> +	bool val13 = !rt_task_enqueued;
> +	bool val8 = sched_switch_dl || val13;
> +	bool val9 = sched_switch_rt || val8;
> +	bool val6 = !sched_switch;
> +	bool val1 = !rt_task_enqueued;
> +
> +	if (val1)
> +		__set_bit(S0, mon->states);
> +	if (val6)
> +		__set_bit(S1, mon->states);
> +	if (val9)
> +		__set_bit(S4, mon->states);
> +}
> +
> +static void
> +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int
> state, unsigned long *next)
> +{
> +	bool sched_switch_rt = test_bit(LTL_SCHED_SWITCH_RT, mon-
> >atoms);
> +	bool sched_switch_dl = test_bit(LTL_SCHED_SWITCH_DL, mon-
> >atoms);
> +	bool sched_switch = test_bit(LTL_SCHED_SWITCH, mon->atoms);
> +	bool rt_task_enqueued = test_bit(LTL_RT_TASK_ENQUEUED, mon-
> >atoms);
> +	bool val13 = !rt_task_enqueued;
> +	bool val8 = sched_switch_dl || val13;
> +	bool val9 = sched_switch_rt || val8;
> +	bool val6 = !sched_switch;
> +	bool val1 = !rt_task_enqueued;
> +
> +	switch (state) {
> +	case S0:
> +		if (val1)
> +			__set_bit(S0, next);
> +		if (val6)
> +			__set_bit(S1, next);
> +		if (val9)
> +			__set_bit(S4, next);
> +		break;
> +	case S1:
> +		if (val6)
> +			__set_bit(S1, next);
> +		if (val1 && val6)
> +			__set_bit(S2, next);
> +		if (val1 && val9)
> +			__set_bit(S3, next);
> +		if (val9)
> +			__set_bit(S4, next);
> +		break;
> +	case S2:
> +		if (val6)
> +			__set_bit(S1, next);
> +		if (val1 && val6)
> +			__set_bit(S2, next);
> +		if (val1 && val9)
> +			__set_bit(S3, next);
> +		if (val9)
> +			__set_bit(S4, next);
> +		break;
> +	case S3:
> +		if (val1)
> +			__set_bit(S0, next);
> +		if (val6)
> +			__set_bit(S1, next);
> +		if (val9)
> +			__set_bit(S4, next);
> +		break;
> +	case S4:
> +		if (val1)
> +			__set_bit(S0, next);
> +		if (val6)
> +			__set_bit(S1, next);
> +		if (val9)
> +			__set_bit(S4, next);
> +		break;
> +	}
> +}
> diff --git a/kernel/trace/rv/monitors/rts/rts_trace.h
> b/kernel/trace/rv/monitors/rts/rts_trace.h
> new file mode 100644
> index 000000000000..0ac9e112a8b0
> --- /dev/null
> +++ b/kernel/trace/rv/monitors/rts/rts_trace.h
> @@ -0,0 +1,15 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +
> +/*
> + * Snippet to be included in rv_trace.h
> + */
> +
> +#ifdef CONFIG_RV_MON_RTS
> +DEFINE_EVENT(event_ltl_monitor, event_rts,
> +	TP_PROTO(unsigned int cpu, char *states, char *atoms, char
> *next),
> +	TP_ARGS(cpu, states, atoms, next));
> +
> +DEFINE_EVENT(error_ltl_monitor, error_rts,
> +	TP_PROTO(unsigned int cpu),
> +	TP_ARGS(cpu));
> +#endif /* CONFIG_RV_MON_RTS */
> diff --git a/tools/verification/models/sched/rts.ltl
> b/tools/verification/models/sched/rts.ltl
> new file mode 100644
> index 000000000000..90872bca46b1
> --- /dev/null
> +++ b/tools/verification/models/sched/rts.ltl
> @@ -0,0 +1,5 @@
> +RULE = always (RT_TASK_ENQUEUED imply SCHEDULE_RT_NEXT)
> +
> +SCHEDULE_RT_NEXT = (not SCHED_SWITCH) until (SCHED_SWITCH_RT or
> EXCEPTIONS)
> +
> +EXCEPTIONS = SCHED_SWITCH_DL or not RT_TASK_ENQUEUED

On Tue, Aug 05, 2025 at 10:40:30AM +0200, Gabriele Monaco wrote:
> Hello Nam,
> 
> I just built and booted up the monitor in a VM (virtme-ng), the
> configuration has preemptirq tracepoints and all monitors so far (as we
> have seen earlier, it doesn't build if rtapp monitors are not there
> because of the circular dependency in the tracepoints).
> 
> All I did was to enable the monitor and printk reactor, but I get a
> whole lot of errors (as in, I need to quit the VM for it to stop):
> 
> [ 1537.699834] rv: rts: 7: violation detected
> [ 1537.699930] rv: rts: 3: violation detected
> [ 1537.701827] rv: rts: 6: violation detected
> [ 1537.704894] rv: rts: 0: violation detected
> [ 1537.704925] rv: rts: 0: violation detected
> [ 1537.704988] rv: rts: 3: violation detected
> [ 1537.705019] rv: rts: 3: violation detected
> [ 1537.705998] rv: rts: 0: violation detected
> [ 1537.706024] rv: rts: 0: violation detected
> [ 1537.709875] rv: rts: 6: violation detected
> [ 1537.709921] rv: rts: 6: violation detected
> [ 1537.711241] rv: rts: 6: violation detected
> 
> Curiously enough, I only see those CPUs (0, 3, 6 and 7).
> Other runs have different CPUs but always a small subset (e.g. 10-15,
> 6-7 only 2).
> It doesn't always occur but enabling/disabling the monitor might help
> triggering it.
> 
> Any idea what is happening?

Thanks for the report. I can reproduce the issue.

Looking at the tracepoints, it makes sense why the monitor complains, some
RT tasks are enqueued but are not dequeued. Then a sched_switch happens
which switches to a non-RT task.

Most likely the dequeue tracepoint misses some cases, let me investigate..

Nam

On Tue, Aug 05, 2025 at 02:22:17PM +0200, Nam Cao wrote:
> On Tue, Aug 05, 2025 at 10:40:30AM +0200, Gabriele Monaco wrote:
> > Hello Nam,
> > 
> > I just built and booted up the monitor in a VM (virtme-ng), the
> > configuration has preemptirq tracepoints and all monitors so far (as we
> > have seen earlier, it doesn't build if rtapp monitors are not there
> > because of the circular dependency in the tracepoints).
> > 
> > All I did was to enable the monitor and printk reactor, but I get a
> > whole lot of errors (as in, I need to quit the VM for it to stop):
> > 
> > [ 1537.699834] rv: rts: 7: violation detected
> > [ 1537.699930] rv: rts: 3: violation detected
> > [ 1537.701827] rv: rts: 6: violation detected
> > [ 1537.704894] rv: rts: 0: violation detected
> > [ 1537.704925] rv: rts: 0: violation detected
> > [ 1537.704988] rv: rts: 3: violation detected
> > [ 1537.705019] rv: rts: 3: violation detected
> > [ 1537.705998] rv: rts: 0: violation detected
> > [ 1537.706024] rv: rts: 0: violation detected
> > [ 1537.709875] rv: rts: 6: violation detected
> > [ 1537.709921] rv: rts: 6: violation detected
> > [ 1537.711241] rv: rts: 6: violation detected
> > 
> > Curiously enough, I only see those CPUs (0, 3, 6 and 7).
> > Other runs have different CPUs but always a small subset (e.g. 10-15,
> > 6-7 only 2).
> > It doesn't always occur but enabling/disabling the monitor might help
> > triggering it.
> > 
> > Any idea what is happening?

There are two issues:

  - When the monitor is disabled then enabled, the number of queued task
    does not reset. The monitor may mistakenly thinks there are queued RT
    tasks, but there aren't.

  - The enqueue tracepoint is registered before the dequeue tracepoint.
    Therefore there may be a enqueue followed by a dequeue, but the monitor
    missed the latter.

The first issue can be fixed by reseting the queued task number at
enabling.

For the second issue, LTL monitors need something similar to
da_monitor_enabled_##name(void). But a quick workaround is reordering the
tracepoint registerations.

So with the below diff, I no longer see the issue.

Thanks again for noticing this!

Nam

diff --git a/kernel/trace/rv/monitors/rts/rts.c b/kernel/trace/rv/monitors/rts/rts.c
index 473004b673c5..3ddbf09db0dd 100644
--- a/kernel/trace/rv/monitors/rts/rts.c
+++ b/kernel/trace/rv/monitors/rts/rts.c
@@ -81,14 +81,21 @@ static void handle_sched_switch(void *data, bool preempt, struct task_struct *pr
 
 static int enable_rts(void)
 {
+	unsigned int cpu;
 	int retval;
 
 	retval = ltl_monitor_init();
 	if (retval)
 		return retval;
 
-	rv_attach_trace_probe("rts", enqueue_task_rt_tp, handle_enqueue_task_rt);
+	for_each_possible_cpu(cpu) {
+		unsigned int *queued = per_cpu_ptr(&nr_queued, cpu);
+
+		*queued = 0;
+	}
+
 	rv_attach_trace_probe("rts", dequeue_task_rt_tp, handle_dequeue_task_rt);
+	rv_attach_trace_probe("rts", enqueue_task_rt_tp, handle_enqueue_task_rt);
 	rv_attach_trace_probe("rts", sched_switch, handle_sched_switch);
 
 	return 0;

On Tue, 2025-08-05 at 17:45 +0200, Nam Cao wrote:
> On Tue, Aug 05, 2025 at 02:22:17PM +0200, Nam Cao wrote:
> > On Tue, Aug 05, 2025 at 10:40:30AM +0200, Gabriele Monaco wrote:
> > > Hello Nam,
> > > 
> > > I just built and booted up the monitor in a VM (virtme-ng), the
> > > configuration has preemptirq tracepoints and all monitors so far
> > > (as we
> > > have seen earlier, it doesn't build if rtapp monitors are not
> > > there
> > > because of the circular dependency in the tracepoints).
> > > 
> > > All I did was to enable the monitor and printk reactor, but I get
> > > a
> > > whole lot of errors (as in, I need to quit the VM for it to
> > > stop):
> > > 
> > > [ 1537.699834] rv: rts: 7: violation detected
> > > [ 1537.699930] rv: rts: 3: violation detected
> > > [ 1537.701827] rv: rts: 6: violation detected
> > > [ 1537.704894] rv: rts: 0: violation detected
> > > [ 1537.704925] rv: rts: 0: violation detected
> > > [ 1537.704988] rv: rts: 3: violation detected
> > > [ 1537.705019] rv: rts: 3: violation detected
> > > [ 1537.705998] rv: rts: 0: violation detected
> > > [ 1537.706024] rv: rts: 0: violation detected
> > > [ 1537.709875] rv: rts: 6: violation detected
> > > [ 1537.709921] rv: rts: 6: violation detected
> > > [ 1537.711241] rv: rts: 6: violation detected
> > > 
> > > Curiously enough, I only see those CPUs (0, 3, 6 and 7).
> > > Other runs have different CPUs but always a small subset (e.g.
> > > 10-15,
> > > 6-7 only 2).
> > > It doesn't always occur but enabling/disabling the monitor might
> > > help
> > > triggering it.
> > > 
> > > Any idea what is happening?
> 
> There are two issues:
> 
>   - When the monitor is disabled then enabled, the number of queued
> task does not reset. The monitor may mistakenly thinks there are
> queued RT tasks, but there aren't.
> 
>   - The enqueue tracepoint is registered before the dequeue
> tracepoint.
>     Therefore there may be a enqueue followed by a dequeue, but the
> monitor missed the latter.
> 
> The first issue can be fixed by reseting the queued task number at
> enabling.

Mmh good catch, indeed you have a counter separated from the LTL thing
here.

> 
> For the second issue, LTL monitors need something similar to
> da_monitor_enabled_##name(void). But a quick workaround is reordering
> the tracepoint registerations.

I didn't make it on time before your V2, I assume you solved already so
you might ignore this.

You kinda have something like the da_monitor_enabled: the
rv_ltl_all_atoms_known

I wonder if you could define LTL_RT_TASK_ENQUEUED only when you
actually know it (or are reasonably sure based on your internal
counter). Or at least not set all atoms until the monitor is fully set
up.

Anyway reordering the tracepoints registration is likely necessary
whatever you do, but I'm afraid a problem like this can occur pretty
often with this type of monitors.

Thanks,
Gabriele

> 
> So with the below diff, I no longer see the issue.
> 
> Thanks again for noticing this!
> 
> Nam
> 
> diff --git a/kernel/trace/rv/monitors/rts/rts.c
> b/kernel/trace/rv/monitors/rts/rts.c
> index 473004b673c5..3ddbf09db0dd 100644
> --- a/kernel/trace/rv/monitors/rts/rts.c
> +++ b/kernel/trace/rv/monitors/rts/rts.c
> @@ -81,14 +81,21 @@ static void handle_sched_switch(void *data, bool
> preempt, struct task_struct *pr
>  
>  static int enable_rts(void)
>  {
> +	unsigned int cpu;
>  	int retval;
>  
>  	retval = ltl_monitor_init();
>  	if (retval)
>  		return retval;
>  
> -	rv_attach_trace_probe("rts", enqueue_task_rt_tp,
> handle_enqueue_task_rt);
> +	for_each_possible_cpu(cpu) {
> +		unsigned int *queued = per_cpu_ptr(&nr_queued, cpu);
> +
> +		*queued = 0;
> +	}
> +
>  	rv_attach_trace_probe("rts", dequeue_task_rt_tp,
> handle_dequeue_task_rt);
> +	rv_attach_trace_probe("rts", enqueue_task_rt_tp,
> handle_enqueue_task_rt);
>  	rv_attach_trace_probe("rts", sched_switch,
> handle_sched_switch);
>  
>  	return 0;

On Wed, Aug 06, 2025 at 10:15:48AM +0200, Gabriele Monaco wrote:
> I didn't make it on time before your V2, I assume you solved already so
> you might ignore this.
> 
> You kinda have something like the da_monitor_enabled: the
> rv_ltl_all_atoms_known
> 
> I wonder if you could define LTL_RT_TASK_ENQUEUED only when you
> actually know it (or are reasonably sure based on your internal
> counter). Or at least not set all atoms until the monitor is fully set
> up.

The rv_ltl_all_atoms_known() thingy is for situation where relevant
tracepoints have not been hit yet.

This case is slightly different, the tracepoint has been hit. And it is not
clear how to implement the "reasonably sure based on your internal counter"
part.

> Anyway reordering the tracepoints registration is likely necessary
> whatever you do, but I'm afraid a problem like this can occur pretty
> often with this type of monitors.

What I have in v2 is a workaround only, by reordering the tracepoint
registrations.

The root problem is not specific to this monitor, but all LTL monitors. My
idea for the real fix is the untested patch below. I will send it
separately. It is not urgent, so I can wait for your DA macro removal patch
to be merged first.

As I'm sending the patch to you, I realized that the patch effectively
nullifies ltl_atoms_init(). So I will need to fix that up..

Nam

commit 7fbb9a99f1a95e5149d476fa3d83a60be1a9a579
Author: Nam Cao <namcao@linutronix.de>
Date:   Tue Aug 5 22:47:49 2025 +0200

    rv: Share the da_monitor_enabled_##name() function with LTL
    
    The LTL monitors also need the functionality that
    da_monitor_enabled_##name() offers.
    
    This is useful to prevent the automaton from being executed before the
    monitor is completely enabled, preventing the situation where the
    monitors run before all tracepoints are registered. This situation can
    cause a false positive error, because the monitors do not see some
    events and do not validate properly.
    
    Pull da_monitor_enabled_##name() to be in the common header, and use
    it for both LTL and DA.
    
    Signed-off-by: Nam Cao <namcao@linutronix.de>

diff --git a/include/linux/rv.h b/include/linux/rv.h
index 1aa01d98e390..8a885b3665a8 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -119,6 +119,14 @@ int rv_register_monitor(struct rv_monitor *monitor, struct rv_monitor *parent);
 int rv_get_task_monitor_slot(void);
 void rv_put_task_monitor_slot(int slot);
 
+static inline bool rv_monitor_enabled(struct rv_monitor *monitor)
+{
+	if (unlikely(!rv_monitoring_on()))
+		return 0;
+
+	return likely(monitor->enabled);
+}
+
 #ifdef CONFIG_RV_REACTORS
 bool rv_reacting_on(void);
 int rv_unregister_reactor(struct rv_reactor *reactor);
diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
index 17fa4f6e5ea6..92b8a8c0b9b7 100644
--- a/include/rv/da_monitor.h
+++ b/include/rv/da_monitor.h
@@ -74,29 +74,12 @@ static inline bool da_monitoring_##name(struct da_monitor *da_mon)				\
 	return da_mon->monitoring;								\
 }												\
 												\
-/*												\
- * da_monitor_enabled_##name - checks if the monitor is enabled					\
- */												\
-static inline bool da_monitor_enabled_##name(void)						\
-{												\
-	/* global switch */									\
-	if (unlikely(!rv_monitoring_on()))							\
-		return 0;									\
-												\
-	/* monitor enabled */									\
-	if (unlikely(!rv_##name.enabled))							\
-		return 0;									\
-												\
-	return 1;										\
-}												\
-												\
 /*												\
  * da_monitor_handling_event_##name - checks if the monitor is ready to handle events		\
  */												\
 static inline bool da_monitor_handling_event_##name(struct da_monitor *da_mon)			\
 {												\
-												\
-	if (!da_monitor_enabled_##name())							\
+	if (!rv_monitor_enabled(&rv_##name))							\
 		return 0;									\
 												\
 	/* monitor is actually monitoring */							\
@@ -390,7 +373,7 @@ static inline bool da_handle_start_event_##name(enum events_##name event)			\
 {												\
 	struct da_monitor *da_mon;								\
 												\
-	if (!da_monitor_enabled_##name())							\
+	if (!rv_monitor_enabled(&rv_##name))							\
 		return 0;									\
 												\
 	da_mon = da_get_monitor_##name();							\
@@ -415,7 +398,7 @@ static inline bool da_handle_start_run_event_##name(enum events_##name event)
 {												\
 	struct da_monitor *da_mon;								\
 												\
-	if (!da_monitor_enabled_##name())							\
+	if (!rv_monitor_enabled(&rv_##name))				\
 		return 0;									\
 												\
 	da_mon = da_get_monitor_##name();							\
@@ -475,7 +458,7 @@ da_handle_start_event_##name(struct task_struct *tsk, enum events_##name event)
 {												\
 	struct da_monitor *da_mon;								\
 												\
-	if (!da_monitor_enabled_##name())							\
+	if (!rv_monitor_enabled(&rv_##name))							\
 		return 0;									\
 												\
 	da_mon = da_get_monitor_##name(tsk);							\
@@ -501,7 +484,7 @@ da_handle_start_run_event_##name(struct task_struct *tsk, enum events_##name eve
 {												\
 	struct da_monitor *da_mon;								\
 												\
-	if (!da_monitor_enabled_##name())							\
+	if (!rv_monitor_enabled(&rv_##name))							\
 		return 0;									\
 												\
 	da_mon = da_get_monitor_##name(tsk);							\
diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h
index 29bbf86d1a52..85a3d07a0303 100644
--- a/include/rv/ltl_monitor.h
+++ b/include/rv/ltl_monitor.h
@@ -16,6 +16,8 @@
 #error "Please include $(MODEL_NAME).h generated by rvgen"
 #endif
 
+#define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME)
+
 #if LTL_MONITOR_TYPE == LTL_TASK_MONITOR
 
 #define TARGET_PRINT_FORMAT "%s[%d]"
@@ -33,7 +35,6 @@ typedef unsigned int monitor_target;
 #endif
 
 #ifdef CONFIG_RV_REACTORS
-#define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME)
 static struct rv_monitor RV_MONITOR_NAME;
 
 static struct ltl_monitor *ltl_get_monitor(monitor_target target);
@@ -156,6 +157,9 @@ static void ltl_attempt_start(monitor_target target, struct ltl_monitor *mon)
 
 static inline void ltl_atom_set(struct ltl_monitor *mon, enum ltl_atom atom, bool value)
 {
+	if (!rv_monitor_enabled(&RV_MONITOR_NAME))
+		return;
+
 	__clear_bit(atom, mon->unknown_atoms);
 	if (value)
 		__set_bit(atom, mon->atoms);

On Wed, 2025-08-06 at 10:46 +0200, Nam Cao wrote:
> On Wed, Aug 06, 2025 at 10:15:48AM +0200, Gabriele Monaco wrote:
> > I didn't make it on time before your V2, I assume you solved
> > already so
> > you might ignore this.
> > 
> > You kinda have something like the da_monitor_enabled: the
> > rv_ltl_all_atoms_known
> > 
> > I wonder if you could define LTL_RT_TASK_ENQUEUED only when you
> > actually know it (or are reasonably sure based on your internal
> > counter). Or at least not set all atoms until the monitor is fully
> > set
> > up.
> 
> The rv_ltl_all_atoms_known() thingy is for situation where relevant
> tracepoints have not been hit yet.
> 
> This case is slightly different, the tracepoint has been hit. And it
> is not clear how to implement the "reasonably sure based on your
> internal counter" part.
> 
> > Anyway reordering the tracepoints registration is likely necessary
> > whatever you do, but I'm afraid a problem like this can occur
> > pretty
> > often with this type of monitors.
> 
> What I have in v2 is a workaround only, by reordering the tracepoint
> registrations.
> 
> The root problem is not specific to this monitor, but all LTL
> monitors. My idea for the real fix is the untested patch below. I
> will send it separately. It is not urgent, so I can wait for your DA
> macro removal patch to be merged first.
> 

Alright, I get it, let's continue with the workaround for now, I'm
going to have a look at your V2.

Thanks,
Gabriele

> As I'm sending the patch to you, I realized that the patch
> effectively nullifies ltl_atoms_init(). So I will need to fix that
> up..
> 
> Nam
> 
> commit 7fbb9a99f1a95e5149d476fa3d83a60be1a9a579
> Author: Nam Cao <namcao@linutronix.de>
> Date:   Tue Aug 5 22:47:49 2025 +0200
> 
>     rv: Share the da_monitor_enabled_##name() function with LTL
>     
>     The LTL monitors also need the functionality that
>     da_monitor_enabled_##name() offers.
>     
>     This is useful to prevent the automaton from being executed
> before the
>     monitor is completely enabled, preventing the situation where the
>     monitors run before all tracepoints are registered. This
> situation can
>     cause a false positive error, because the monitors do not see
> some
>     events and do not validate properly.
>     
>     Pull da_monitor_enabled_##name() to be in the common header, and
> use
>     it for both LTL and DA.
>     
>     Signed-off-by: Nam Cao <namcao@linutronix.de>
> 
> diff --git a/include/linux/rv.h b/include/linux/rv.h
> index 1aa01d98e390..8a885b3665a8 100644
> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -119,6 +119,14 @@ int rv_register_monitor(struct rv_monitor
> *monitor, struct rv_monitor *parent);
>  int rv_get_task_monitor_slot(void);
>  void rv_put_task_monitor_slot(int slot);
>  
> +static inline bool rv_monitor_enabled(struct rv_monitor *monitor)
> +{
> +	if (unlikely(!rv_monitoring_on()))
> +		return 0;
> +
> +	return likely(monitor->enabled);
> +}
> +
>  #ifdef CONFIG_RV_REACTORS
>  bool rv_reacting_on(void);
>  int rv_unregister_reactor(struct rv_reactor *reactor);
> diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
> index 17fa4f6e5ea6..92b8a8c0b9b7 100644
> --- a/include/rv/da_monitor.h
> +++ b/include/rv/da_monitor.h
> @@ -74,29 +74,12 @@ static inline bool da_monitoring_##name(struct
> da_monitor *da_mon)				\
>  	return da_mon-
> >monitoring;								\
>  }								
> 				\
>  								
> 				\
> -
> /*												\
> - * da_monitor_enabled_##name - checks if the monitor is
> enabled					\
> -
> */												\
> -static inline bool
> da_monitor_enabled_##name(void)						\
> -
> {												\
> -	/* global switch
> */									\
> -	if
> (unlikely(!rv_monitoring_on()))							\
> -		return
> 0;									\
> -
> 												\
> -	/* monitor enabled
> */									\
> -	if
> (unlikely(!rv_##name.enabled))							\
> -		return
> 0;									\
> -
> 												\
> -	return
> 1;										\
> -
> }												\
> -
> 												\
>  /*								
> 				\
>   * da_monitor_handling_event_##name - checks if the monitor is ready
> to handle events		\
>  
> */												\
>  static inline bool da_monitor_handling_event_##name(struct
> da_monitor *da_mon)			\
>  {								
> 				\
> -
> 												\
> -	if
> (!da_monitor_enabled_##name())							\
> +	if
> (!rv_monitor_enabled(&rv_##name))							\
>  		return
> 0;									\
>  								
> 				\
>  	/* monitor is actually monitoring
> */							\
> @@ -390,7 +373,7 @@ static inline bool
> da_handle_start_event_##name(enum events_##name
> event)			\
>  {								
> 				\
>  	struct da_monitor
> *da_mon;								\
>  								
> 				\
> -	if
> (!da_monitor_enabled_##name())							\
> +	if
> (!rv_monitor_enabled(&rv_##name))							\
>  		return
> 0;									\
>  								
> 				\
>  	da_mon =
> da_get_monitor_##name();							\
> @@ -415,7 +398,7 @@ static inline bool
> da_handle_start_run_event_##name(enum events_##name event)
>  {								
> 				\
>  	struct da_monitor
> *da_mon;								\
>  								
> 				\
> -	if
> (!da_monitor_enabled_##name())							\
> +	if
> (!rv_monitor_enabled(&rv_##name))				\
>  		return
> 0;									\
>  								
> 				\
>  	da_mon =
> da_get_monitor_##name();							\
> @@ -475,7 +458,7 @@ da_handle_start_event_##name(struct task_struct
> *tsk, enum events_##name event)
>  {								
> 				\
>  	struct da_monitor
> *da_mon;								\
>  								
> 				\
> -	if
> (!da_monitor_enabled_##name())							\
> +	if
> (!rv_monitor_enabled(&rv_##name))							\
>  		return
> 0;									\
>  								
> 				\
>  	da_mon =
> da_get_monitor_##name(tsk);							\
> @@ -501,7 +484,7 @@ da_handle_start_run_event_##name(struct
> task_struct *tsk, enum events_##name eve
>  {								
> 				\
>  	struct da_monitor
> *da_mon;								\
>  								
> 				\
> -	if
> (!da_monitor_enabled_##name())							\
> +	if
> (!rv_monitor_enabled(&rv_##name))							\
>  		return
> 0;									\
>  								
> 				\
>  	da_mon =
> da_get_monitor_##name(tsk);							\
> diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h
> index 29bbf86d1a52..85a3d07a0303 100644
> --- a/include/rv/ltl_monitor.h
> +++ b/include/rv/ltl_monitor.h
> @@ -16,6 +16,8 @@
>  #error "Please include $(MODEL_NAME).h generated by rvgen"
>  #endif
>  
> +#define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME)
> +
>  #if LTL_MONITOR_TYPE == LTL_TASK_MONITOR
>  
>  #define TARGET_PRINT_FORMAT "%s[%d]"
> @@ -33,7 +35,6 @@ typedef unsigned int monitor_target;
>  #endif
>  
>  #ifdef CONFIG_RV_REACTORS
> -#define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME)
>  static struct rv_monitor RV_MONITOR_NAME;
>  
>  static struct ltl_monitor *ltl_get_monitor(monitor_target target);
> @@ -156,6 +157,9 @@ static void ltl_attempt_start(monitor_target
> target, struct ltl_monitor *mon)
>  
>  static inline void ltl_atom_set(struct ltl_monitor *mon, enum
> ltl_atom atom, bool value)
>  {
> +	if (!rv_monitor_enabled(&RV_MONITOR_NAME))
> +		return;
> +
>  	__clear_bit(atom, mon->unknown_atoms);
>  	if (value)
>  		__set_bit(atom, mon->atoms);

On Wed, 2025-07-30 at 14:45 +0200, Nam Cao wrote:
> Add "real-time scheduling" monitor, which validates that SCHED_RR and
> SCHED_FIFO tasks are scheduled before tasks with normal and
> extensible
> scheduling policies
> 

Looks a very interesting monitor!
A few questions:

I assume this works with rt-throttle because it implies a dequeue,
right?
And you probably won't see that without explicit tracepoints..

> +	/*
> +	 * This may not be accurate, there may be enqueued RT tasks.
> But
> that's
> +	 * okay, the worst we get is a false negative. It will be
> accurate
> as
> +	 * soon as the CPU no longer has any queued RT task.
> +	 */
> +	ltl_atom_set(mon, LTL_RT_TASK_ENQUEUED, false);
> 

As far as I understand here the monitor would just miss RT tasks
already running but would perfectly enforce the ones starting after
initialisation, right?

> +RULE = always (RT_TASK_ENQUEUED imply SCHEDULE_RT_NEXT)
> +
> +SCHEDULE_RT_NEXT = (not SCHED_SWITCH) until (SCHED_SWITCH_RT or
> EXCEPTIONS)
> +
> +EXCEPTIONS = SCHED_SWITCH_DL or not RT_TASK_ENQUEUED

This monitor allows non-RT tasks to run indefinitely before the switch,
only when it happens, RT must run, right?
Not sure you can do much about it though. (without falling into the
need resched rabbithole I was trying to untangle)

Thanks,
Gabriele

On Thu, Jul 31, 2025 at 09:47:10AM +0200, Gabriele Monaco wrote:
> On Wed, 2025-07-30 at 14:45 +0200, Nam Cao wrote:
> > Add "real-time scheduling" monitor, which validates that SCHED_RR and
> > SCHED_FIFO tasks are scheduled before tasks with normal and
> > extensible
> > scheduling policies
> > 
> 
> Looks a very interesting monitor!
> A few questions:
> 
> I assume this works with rt-throttle because it implies a dequeue,
> right?
> And you probably won't see that without explicit tracepoints..

It does work properly with rt-throttling:
	root@yellow:~# ./rt-loop
	[   74.357730] sched: RT throttling activated
	[   74.357745] rv: rts: 0: violation detected

Looking at rt-throlling code, it does not dequeue tasks, only does
	rt_rq->rt_throttled = 1;
	rt_rq->rt_queued = 0;

so we are fine.

> > +	/*
> > +	 * This may not be accurate, there may be enqueued RT tasks.
> > But
> > that's
> > +	 * okay, the worst we get is a false negative. It will be
> > accurate
> > as
> > +	 * soon as the CPU no longer has any queued RT task.
> > +	 */
> > +	ltl_atom_set(mon, LTL_RT_TASK_ENQUEUED, false);
> > 
> 
> As far as I understand here the monitor would just miss RT tasks
> already running but would perfectly enforce the ones starting after
> initialisation, right?

Not exactly. What could happen is that:

 - RT task A already running

 - monitor enabled. The monitor isn't aware of task A, therefore it allows
   sched_switch to switch to non-RT task.

 - RT task B is queued. The monitor now knows at least one RT task is
   enqueued, so it disallows sched_switch to switch to non-RT.

 - RT task A is dequeued. However, the monitor does not differentiate task
   A and task B, therefore I thinks the only enqueued RT task is now gone.

 - So now we have task B started after the monitor, but the monitor does
   not check it.

The monitor will become accurate once the CPU has no enqueued RT task,
which should happen quite quickly on a sane setup where RT tasks do not
monopoly the CPU.

The monitor could be changed to be accurate from the get-go, by looking at
how many enqueued RT tasks are present. I *think* rt_rq->rt_nr_running
works. But I think the current implementation is fine, so not worth
thinking too much about it.

> > +RULE = always (RT_TASK_ENQUEUED imply SCHEDULE_RT_NEXT)
> > +
> > +SCHEDULE_RT_NEXT = (not SCHED_SWITCH) until (SCHED_SWITCH_RT or
> > EXCEPTIONS)
> > +
> > +EXCEPTIONS = SCHED_SWITCH_DL or not RT_TASK_ENQUEUED
> 
> This monitor allows non-RT tasks to run indefinitely before the switch,
> only when it happens, RT must run, right?

Yes.

> Not sure you can do much about it though. (without falling into the
> need resched rabbithole I was trying to untangle)

I would need to look into scheduler code, maybe we could check that the
next scheduler tick implies a sched_switch. Another day.

Nam

On Fri, 2025-08-01 at 09:58 +0200, Nam Cao wrote:
> On Thu, Jul 31, 2025 at 09:47:10AM +0200, Gabriele Monaco wrote:
> > On Wed, 2025-07-30 at 14:45 +0200, Nam Cao wrote:
> > > Add "real-time scheduling" monitor, which validates that SCHED_RR
> > > and SCHED_FIFO tasks are scheduled before tasks with normal and
> > > extensible scheduling policies
> > 
> > Looks a very interesting monitor!
> > A few questions:
> > 
> > I assume this works with rt-throttle because it implies a dequeue,
> > right?
> > And you probably won't see that without explicit tracepoints..
> 
> It does work properly with rt-throttling:
> 	root@yellow:~# ./rt-loop
> 	[   74.357730] sched: RT throttling activated
> 	[   74.357745] rv: rts: 0: violation detected
> 
> Looking at rt-throlling code, it does not dequeue tasks, only does
> 	rt_rq->rt_throttled = 1;
> 	rt_rq->rt_queued = 0;
> 
> so we are fine.

Wait, by /works properly/ you mean it reports a violation. I just
noticed you mention it in the description.

It's reasonable to request RT throttling disabled on sanely configured
RT systems. But throttling is a /valid/ kernel feature, I get you mark
it as /unwanted/ though.

I guess if that's the case, this monitor doesn't belong in the sched
collection because it's meant to validate the kernel behaviour, not its
configuration for a specific purpose (RT).
Isn't it better off with the rtapp ones (which validate the system
configuration to run in an RT scenario).

Does it make sense to you?

> > 
> > As far as I understand here the monitor would just miss RT tasks
> > already running but would perfectly enforce the ones starting after
> > initialisation, right?
> 
> Not exactly. What could happen is that:
> 
>  - RT task A already running
> 
>  - monitor enabled. The monitor isn't aware of task A, therefore it
> allows
>    sched_switch to switch to non-RT task.
> 
>  - RT task B is queued. The monitor now knows at least one RT task is
>    enqueued, so it disallows sched_switch to switch to non-RT.
> 
>  - RT task A is dequeued. However, the monitor does not differentiate
> task
>    A and task B, therefore I thinks the only enqueued RT task is now
> gone.
> 
>  - So now we have task B started after the monitor, but the monitor
> does not check it.
> 
> The monitor will become accurate once the CPU has no enqueued RT
> task, which should happen quite quickly on a sane setup where RT
> tasks do not monopoly the CPU.
> 
> The monitor could be changed to be accurate from the get-go, by
> looking at how many enqueued RT tasks are present. I *think* rt_rq-
> >rt_nr_running works. But I think the current implementation is
> fine, so not worth thinking too much about it.

Yeah if it's something quickly reached it shouldn't be a problem, also
rt throttle would run in case there's an RT monopoly and you'd see a
violation already.

> > 
> > Not sure you can do much about it though. (without falling into the
> > need resched rabbithole I was trying to untangle)
> 
> I would need to look into scheduler code, maybe we could check that
> the next scheduler tick implies a sched_switch. Another day.

Agree, the monitor looks good for now.
I still want to give it a run when I have a bit more time, besides with
RT throttle, can the monitor really fail on a working system?

Thanks,
Gabriele

Gabriele Monaco <gmonaco@redhat.com> writes:
> Wait, by /works properly/ you mean it reports a violation. I just
> noticed you mention it in the description.
>
> It's reasonable to request RT throttling disabled on sanely configured
> RT systems. But throttling is a /valid/ kernel feature, I get you mark
> it as /unwanted/ though.

True.

> I guess if that's the case, this monitor doesn't belong in the sched
> collection because it's meant to validate the kernel behaviour, not its
> configuration for a specific purpose (RT).
> Isn't it better off with the rtapp ones (which validate the system
> configuration to run in an RT scenario).
>
> Does it make sense to you?

Yeah I was a bit unsure where to put this monitor. But under rtapp makes
sense, if you prefer it there.

> I still want to give it a run when I have a bit more time, besides with
> RT throttle, can the monitor really fail on a working system?

RT throttling and fair deadline server are the only two known mechanisms
which would fail the monitor.

In the future, there may also be sched_ext deadline server:
https://lore.kernel.org/all/20250702232944.3221001-1-joelagnelf@nvidia.com/#t

They exist for good reasons, but they are also a problem to real-time
tasks. I am posting this monitor because we did a cyclic test the other
day and observed some big latencies, and we had no idea why. It turned
out it was the fair deadline server. So we need this monitor to tell us
if some similar mechanisms exist or will appear in the future.

If you try the monitor and see problems, let me know. Most likely it
would be a flaw in the monitor, but there is also a chance there is
another throttling mechanism we are not yet aware of.

Nam