On Tue, 19 Jul 2022 19:27:09 +0200
Daniel Bristot de Oliveira <bristot@xxxxxxxxxx> wrote:
> diff --git a/include/linux/rv.h b/include/linux/rv.h
> index 4f5b70eee557..31d8b2614eae 100644
> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -7,6 +7,8 @@
> #ifndef _LINUX_RV_H
> #define _LINUX_RV_H
>
> +#define MAX_DA_NAME_LEN 24
> +
> struct rv_reactor {
> char *name;
> char *description;
> diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
> new file mode 100644
> index 000000000000..ef7ee3ffcad6
> --- /dev/null
> +++ b/include/rv/da_monitor.h
> @@ -0,0 +1,507 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/*
> + * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@xxxxxxxxxx>
> + *
> + * Deterministic automata (DA) monitor functions, to be used together
> + * with automata models in C generated by the dot2k tool.
> + *
> + * The dot2k tool is available at tools/verification/dot2k/
> + */
> +
> +#include <rv/automata.h>
> +#include <linux/rv.h>
> +#include <linux/bug.h>
> +
> +/*
> + * Generic helpers for all types of deterministic automata monitors.
> + */
> +#define DECLARE_DA_MON_GENERIC_HELPERS(name, type) \
> + \
> +static char REACT_MSG[1024]; \
> + \
> +static inline char *format_react_msg(type curr_state, type event) \
You probably want to call this format_react_msg_##name() too.
> +{ \
> + snprintf(REACT_MSG, 1024, \
> + "rv: monitor %s does not allow event %s on state %s\n", \
> + #name, \
> + model_get_event_name_##name(event), \
> + model_get_state_name_##name(curr_state)); \
> + return REACT_MSG; \
> +} \
> + \
> +static void cond_react(char *msg) \
And this cond_react_##name() as well. Otherwise you can have issues with
the same function being used by multiple monitors. What if two are declared
in the same file? This will fail to build.
> +{ \
> + if (rv_##name.react) \
> + rv_##name.react(msg); \
> +} \
> + \
> +/* \
> + * da_monitor_reset_##name - reset a monitor and setting it to init state \
> + */ \
> +static inline void da_monitor_reset_##name(struct da_monitor *da_mon) \
> +{ \
> + da_mon->monitoring = 0; \
> + da_mon->curr_state = model_get_initial_state_##name(); \
> +} \
> + \
> +/* \
> + * da_monitor_curr_state_##name - return the current state \
> + */ \
> +static inline type da_monitor_curr_state_##name(struct da_monitor *da_mon) \
> +{ \
> + return da_mon->curr_state; \
> +} \
> + \
> +/* \
> + * da_monitor_set_state_##name - set the new current state \
> + */ \
> +static inline void \
> +da_monitor_set_state_##name(struct da_monitor *da_mon, enum states_##name state) \
> +{ \
> + da_mon->curr_state = state; \
> +} \
> + \
> +/* \
> + * da_monitor_start_##name - start monitoring \
> + * \
> + * The monitor will ignore all events until monitoring is set to true. This \
> + * function needs to be called to tell the monitor to start monitoring. \
> + */ \
> +static inline void da_monitor_start_##name(struct da_monitor *da_mon) \
> +{ \
> + da_mon->monitoring = 1; \
> +} \
> + \
> +/* \
> + * da_monitoring_##name - returns true if the monitor is processing events \
> + */ \
> +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) \
> +{ \
Should we add a:
smp_rmb();
here? And then a smp_wmb() where these switches get updated?
I guess how critical is it that these turn off immediately after the switch
is flipped?
> + /* 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()) \
> + return 0; \
> + \
> + /* monitor is actually monitoring */ \
> + if (unlikely(!da_monitoring_##name(da_mon))) \
> + return 0; \
> + \
> + return 1; \
> +}
> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
> index 3eb5d48ab4f6..0123bdf7052a 100644
> --- a/kernel/trace/rv/Kconfig
> +++ b/kernel/trace/rv/Kconfig
> @@ -1,5 +1,19 @@
> # SPDX-License-Identifier: GPL-2.0-only
> #
> +config DA_MON_EVENTS
> + default n
> + bool
> +
> +config DA_MON_EVENTS_IMPLICIT
> + select DA_MON_EVENTS
> + default n
> + bool
> +
> +config DA_MON_EVENTS_ID
> + select DA_MON_EVENTS
> + default n
> + bool
The "default n" are not needed. The default is 'n' without it.
-- Steve
> +
> menuconfig RV
> bool "Runtime Verification"
> depends on TRACING
> diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c
> index eb835777a59b..00183e056dfd 100644
> --- a/kernel/trace/rv/rv.c
> +++ b/kernel/trace/rv/rv.c
> @@ -141,6 +141,11 @@
> #include <linux/slab.h>
> #include <rv/rv.h>
>
> +#ifdef CONFIG_DA_MON_EVENTS
> +#define CREATE_TRACE_POINTS
> +#include <trace/events/rv.h>
> +#endif
> +
> #include "rv.h"
>
> DEFINE_MUTEX(rv_interface_lock);
