Add support for per-cpu run-time verification linear temporal logic
monitors. This is analogous to deterministic automaton per-cpu monitors.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 include/linux/rv.h         |  1 +
 include/rv/ltl_monitor.h   | 32 ++++++++++++++++++++++++++
 kernel/trace/rv/Kconfig    |  4 ++++
 kernel/trace/rv/rv_trace.h | 47 ++++++++++++++++++++++++++++++++++++++
 4 files changed, 84 insertions(+)

diff --git a/include/linux/rv.h b/include/linux/rv.h
index 175438a22641..a41ae5980099 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -29,6 +29,7 @@ struct da_monitor {
 #ifdef CONFIG_RV_LTL_MONITOR
 
 #define LTL_TASK_MONITOR 0
+#define LTL_CPU_MONITOR 1
 /*
  * In the future, if the number of atomic propositions or the size of Buchi
  * automaton is larger, we can switch to dynamic allocation. For now, the code
diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h
index 466155fd53e6..29bbf86d1a52 100644
--- a/include/rv/ltl_monitor.h
+++ b/include/rv/ltl_monitor.h
@@ -23,12 +23,21 @@
 
 typedef struct task_struct *monitor_target;
 
+#elif LTL_MONITOR_TYPE == LTL_CPU_MONITOR
+
+#define TARGET_PRINT_FORMAT "%u"
+#define TARGET_PRINT_ARGS(cpu) cpu
+
+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);
+
 static void rv_cond_react(monitor_target target)
 {
 	if (!rv_reacting_on() || !RV_MONITOR_NAME.react)
@@ -54,6 +63,13 @@ static struct ltl_monitor *ltl_get_monitor(monitor_target target)
 {
 	return &target->rv[ltl_monitor_slot].ltl_mon;
 }
+#elif LTL_MONITOR_TYPE == LTL_CPU_MONITOR
+static struct ltl_monitor *ltl_get_monitor(unsigned int cpu)
+{
+	static DEFINE_PER_CPU(struct ltl_monitor, ltl_monitor);
+
+	return per_cpu_ptr(&ltl_monitor, cpu);
+}
 #endif
 
 static void ltl_target_init(monitor_target target, bool target_creation)
@@ -108,6 +124,22 @@ static void ltl_monitor_destroy(void)
 	rv_put_task_monitor_slot(ltl_monitor_slot);
 	ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
 }
+
+#elif LTL_MONITOR_TYPE == LTL_CPU_MONITOR
+
+static int ltl_monitor_init(void)
+{
+	unsigned int cpu;
+
+	for_each_possible_cpu(cpu)
+		ltl_target_init(cpu, false);
+	return 0;
+}
+
+static void ltl_monitor_destroy(void)
+{
+}
+
 #endif
 
 static void ltl_illegal_state(monitor_target target, struct ltl_monitor *mon)
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 5b4be87ba59d..951c2e0cda25 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -16,6 +16,10 @@ config DA_MON_EVENTS_ID
 	select RV_MON_MAINTENANCE_EVENTS
 	bool
 
+config LTL_MON_EVENTS_IMPLICIT
+	select RV_MON_EVENTS
+	bool
+
 config LTL_MON_EVENTS_ID
 	select RV_MON_EVENTS
 	bool
diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index 4a6faddac614..f9e5fd044c45 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -177,6 +177,53 @@ DECLARE_EVENT_CLASS(error_ltl_monitor_id,
 #include <monitors/pagefault/pagefault_trace.h>
 #include <monitors/sleep/sleep_trace.h>
 // Add new monitors based on CONFIG_LTL_MON_EVENTS_ID here
+
+#ifdef CONFIG_LTL_MON_EVENTS_IMPLICIT
+DECLARE_EVENT_CLASS(event_ltl_monitor,
+
+	TP_PROTO(unsigned int cpu, char *states, char *atoms, char *next),
+
+	TP_ARGS(cpu, states, atoms, next),
+
+	TP_STRUCT__entry(
+		__field(unsigned int, cpu)
+		__string(states, states)
+		__string(atoms, atoms)
+		__string(next, next)
+	),
+
+	TP_fast_assign(
+		__entry->cpu = cpu;
+		__assign_str(states);
+		__assign_str(atoms);
+		__assign_str(next);
+	),
+
+	TP_printk("cpu%u: (%s) x (%s) -> (%s)", __entry->cpu,
+		  __get_str(states), __get_str(atoms), __get_str(next))
+);
+
+DECLARE_EVENT_CLASS(error_ltl_monitor,
+
+	TP_PROTO(unsigned int cpu),
+
+	TP_ARGS(cpu),
+
+	TP_STRUCT__entry(
+		__field(unsigned int, cpu)
+	),
+
+	TP_fast_assign(
+		__entry->cpu = cpu;
+	),
+
+	TP_printk("cpu%u: violation detected", __entry->cpu)
+);
+#include <monitors/rts/rts_trace.h>
+// Add new monitors based on CONFIG_LTL_MON_EVENTS_IMPLICIT here
+
+#endif /* CONFIG_LTL_MON_EVENTS_IMPLICIT */
+
 #endif /* CONFIG_LTL_MON_EVENTS_ID */
 
 #ifdef CONFIG_RV_MON_MAINTENANCE_EVENTS
-- 
2.39.5

On Wed, 2025-07-30 at 14:45 +0200, Nam Cao wrote:
> Add support for per-cpu run-time verification linear temporal logic
> monitors. This is analogous to deterministic automaton per-cpu
> monitors.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---
> 
> diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
> index 4a6faddac614..f9e5fd044c45 100644
> --- a/kernel/trace/rv/rv_trace.h
> +++ b/kernel/trace/rv/rv_trace.h
> @@ -177,6 +177,53 @@ DECLARE_EVENT_CLASS(error_ltl_monitor_id,
>  #include <monitors/pagefault/pagefault_trace.h>
>  #include <monitors/sleep/sleep_trace.h>
>  // Add new monitors based on CONFIG_LTL_MON_EVENTS_ID here
> +
> +#ifdef CONFIG_LTL_MON_EVENTS_IMPLICIT
> +DECLARE_EVENT_CLASS(event_ltl_monitor,
> +
> +	TP_PROTO(unsigned int cpu, char *states, char *atoms, char
> *next),
> +

You don't really need to follow to the ID/IMPLICIT convention here.

These LTL per-cpu monitors are, in fact, not implicit since they do
have an id (the CPU), implicit makes sense with the current
implementation of da_get_monitor that uses the current CPU (doesn't
have to stay that way, but there was no need to change so far).

If you don't want to get rid of the task's comm in the tracepoint (and
unify both with an integer id, like with DA), I'd suggest you use
different names like CONFIG_LTL_MON_EVENTS_TASK (in fact that doesn't
just have an ID) and CONFIG_LTL_MON_EVENTS_CPU (or even
CONFIG_LTL_MON_EVENTS_ID, for this it actually makes sense).

I'd prefer it as general as possible to ease new monitor types, but to
be real picky the LTLs per-task are not ID and the per-cpu are not
IMPLICIT.

The id field is what the rv userspace tool uses to differentiate
monitor types, by the way.


> +#endif /* CONFIG_LTL_MON_EVENTS_IMPLICIT */
> +
>  #endif /* CONFIG_LTL_MON_EVENTS_ID */

Also, I'm not sure if that was intended, but
CONFIG_LTL_MON_EVENTS_IMPLICIT gets compiled only with
CONFIG_LTL_MON_EVENTS_ID.

Thanks,
Gabriele

On Thu, Jul 31, 2025 at 10:02:19AM +0200, Gabriele Monaco wrote:
> You don't really need to follow to the ID/IMPLICIT convention here.
> 
> These LTL per-cpu monitors are, in fact, not implicit since they do
> have an id (the CPU), implicit makes sense with the current
> implementation of da_get_monitor that uses the current CPU (doesn't
> have to stay that way, but there was no need to change so far).
> 
> If you don't want to get rid of the task's comm in the tracepoint (and
> unify both with an integer id, like with DA), I'd suggest you use
> different names like CONFIG_LTL_MON_EVENTS_TASK (in fact that doesn't
> just have an ID) and CONFIG_LTL_MON_EVENTS_CPU (or even
> CONFIG_LTL_MON_EVENTS_ID, for this it actually makes sense).
> 
> I'd prefer it as general as possible to ease new monitor types, but to
> be real picky the LTLs per-task are not ID and the per-cpu are not
> IMPLICIT.
> 
> The id field is what the rv userspace tool uses to differentiate
> monitor types, by the way.

Ah, these names didn't make sense to me. But DA use them, so I was
"whatever".

Thanks for the explanation, let's use the _CPU names instead.

> > +#endif /* CONFIG_LTL_MON_EVENTS_IMPLICIT */
> > +
> >  #endif /* CONFIG_LTL_MON_EVENTS_ID */
> 
> Also, I'm not sure if that was intended, but
> CONFIG_LTL_MON_EVENTS_IMPLICIT gets compiled only with
> CONFIG_LTL_MON_EVENTS_ID.

That was certainly not intended.

Nam