On Wed, 2025-08-06 at 10:01 +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 <[email protected]> > --- > v2: Rename "implicit" to "cpu"
Looks good to me. Reviewed-by: Gabriele Monaco <[email protected]> Thanks, Gabriele > --- > include/rv/ltl_monitor.h | 32 ++++++++++++++++++++++++++ > kernel/trace/rv/Kconfig | 4 ++++ > kernel/trace/rv/rv_trace.h | 46 > ++++++++++++++++++++++++++++++++++++++ > 3 files changed, 82 insertions(+) > > diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h > index 9dabc5b133a3..4ad08b5b9f2d 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 == RV_MON_PER_CPU > + > +#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 == RV_MON_PER_CPU > +static struct ltl_monitor *ltl_get_monitor(unsigned int cpu) > +{ > + static DEFINE_PER_CPU(struct ltl_monitor, ltl_monitor); > + > + return per_cpu_ptr(<l_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 == RV_MON_PER_CPU > + > +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..7ef89006ed50 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_CPU > + 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..bf7cca6579ec 100644 > --- a/kernel/trace/rv/rv_trace.h > +++ b/kernel/trace/rv/rv_trace.h > @@ -177,8 +177,54 @@ 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 > + > #endif /* CONFIG_LTL_MON_EVENTS_ID */ > > +#ifdef CONFIG_LTL_MON_EVENTS_CPU > +DECLARE_EVENT_CLASS(event_ltl_monitor_cpu, > + > + 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_cpu, > + > + 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) > +); > +// Add new monitors based on CONFIG_LTL_MON_EVENTS_CPU here > + > +#endif /* CONFIG_LTL_MON_EVENTS_CPU */ > + > #ifdef CONFIG_RV_MON_MAINTENANCE_EVENTS > /* Tracepoint useful for monitors development, currenly only used in > DA */ > TRACE_EVENT(rv_retries_error,
