Re: [PATCH V6 04/16] rv/include: Add deterministic automata monitor definition via C macros

[Steven Rostedt <rostedt@goodmis.org>]

On Tue, 19 Jul 2022 19:27:09 +0200
Daniel Bristot de Oliveira <bristot@kernel.org> 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@kernel.org>
> + *
> + * 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);