[PATCH 2/5] rv/ltl: Support per-cpu monitors

[Nam Cao]

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 <nam...@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