Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) client-ip=2620:137:e000::1:20;
Date:   Wed, 20 Jul 2022 16:06:06 -0400
From:   Steven Rostedt <rostedt@goodmis.org>
To:     Daniel Bristot de Oliveira <bristot@kernel.org>
Cc:     Wim Van Sebroeck <wim@linux-watchdog.org>,
        Guenter Roeck <linux@roeck-us.net>,
        Jonathan Corbet <corbet@lwn.net>,
        Ingo Molnar <mingo@redhat.com>,
        Thomas Gleixner <tglx@linutronix.de>,
        Peter Zijlstra <peterz@infradead.org>,
        Will Deacon <will@kernel.org>,
        Catalin Marinas <catalin.marinas@arm.com>,
        Marco Elver <elver@google.com>,
        Dmitry Vyukov <dvyukov@google.com>,
        "Paul E. McKenney" <paulmck@kernel.org>,
        Shuah Khan <skhan@linuxfoundation.org>,
        Gabriele Paoloni <gpaoloni@redhat.com>,
        Juri Lelli <juri.lelli@redhat.com>,
        Clark Williams <williams@redhat.com>,
        Tao Zhou <tao.zhou@linux.dev>,
        Randy Dunlap <rdunlap@infradead.org>,
        linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org,
        linux-trace-devel@vger.kernel.org
Subject: Re: [PATCH V6 04/16] rv/include: Add deterministic automata monitor
 definition via C macros
Message-ID: <20220720160606.3e672b55@gandalf.local.home>
In-Reply-To: <9ffc05b67fff087413143a420373731e0e34eef4.1658244826.git.bristot@kernel.org>
References: <cover.1658244826.git.bristot@kernel.org>
        <9ffc05b67fff087413143a420373731e0e34eef4.1658244826.git.bristot@kernel.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Precedence: bulk

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);