Contributors: 5
Author Tokens Token Proportion Commits Commit Proportion
Daniel Bristot de Oliveira 206 93.64% 2 25.00%
Gabriele Monaco 10 4.55% 3 37.50%
Nam Cao 2 0.91% 1 12.50%
Greg Kroah-Hartman 1 0.45% 1 12.50%
Yu Liao 1 0.45% 1 12.50%
Total 220 8 


/* 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/
 *
 * For further information, see:
 *   Documentation/trace/rv/da_monitor_synthesis.rst
 */

#include <rv/automata.h>
#include <linux/rv.h>
#include <linux/bug.h>
#include <linux/sched.h>

#ifdef CONFIG_RV_REACTORS

#define DECLARE_RV_REACTING_HELPERS(name, type)							\
static void cond_react_##name(type curr_state, type event)					\
{												\
	if (!rv_reacting_on() || !rv_##name.react)						\
		return;										\
	rv_##name.react("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));				\
}

#else /* CONFIG_RV_REACTOR */

#define DECLARE_RV_REACTING_HELPERS(name, type)							\
static void cond_react_##name(type curr_state, type event)					\
{												\
	return;											\
}
#endif

/*
 * Generic helpers for all types of deterministic automata monitors.
 */
#define DECLARE_DA_MON_GENERIC_HELPERS(name, type)						\
												\
DECLARE_RV_REACTING_HELPERS(name, type)								\
												\
/*												\
 * 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_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->curr_state = model_get_initial_state_##name();					\
	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)						\
{												\
	/* 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;										\
}

/*
 * Event handler for implicit monitors. Implicit monitor is the one which the
 * handler does not need to specify which da_monitor to manipulate. Examples
 * of implicit monitor are the per_cpu or the global ones.
 *
 * Retry in case there is a race between getting and setting the next state,
 * warn and reset the monitor if it runs out of retries. The monitor should be
 * able to handle various orders.
 */
#define DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type)					\
												\
static inline bool										\
da_event_##name(struct da_monitor *da_mon, enum events_##name event)				\
{												\
	enum states_##name curr_state, next_state;						\
												\
	curr_state = READ_ONCE(da_mon->curr_state);						\
	for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) {					\
		next_state = model_get_next_state_##name(curr_state, event);			\
		if (next_state == INVALID_STATE) {						\
			cond_react_##name(curr_state, event);					\
			trace_error_##name(model_get_state_name_##name(curr_state),		\
					   model_get_event_name_##name(event));			\
			return false;								\
		}										\
		if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) {	\
			trace_event_##name(model_get_state_name_##name(curr_state),		\
					   model_get_event_name_##name(event),			\
					   model_get_state_name_##name(next_state),		\
					   model_is_final_state_##name(next_state));		\
			return true;								\
		}										\
	}											\
												\
	trace_rv_retries_error(#name, model_get_event_name_##name(event));			\
	pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS)					\
		" retries reached for event %s, resetting monitor %s",				\
		model_get_event_name_##name(event), #name);					\
	return false;										\
}												\

/*
 * Event handler for per_task monitors.
 *
 * Retry in case there is a race between getting and setting the next state,
 * warn and reset the monitor if it runs out of retries. The monitor should be
 * able to handle various orders.
 */
#define DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type)					\
												\
static inline bool da_event_##name(struct da_monitor *da_mon, struct task_struct *tsk,		\
				   enum events_##name event)					\
{												\
	enum states_##name curr_state, next_state;						\
												\
	curr_state = READ_ONCE(da_mon->curr_state);						\
	for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) {					\
		next_state = model_get_next_state_##name(curr_state, event);			\
		if (next_state == INVALID_STATE) {						\
			cond_react_##name(curr_state, event);					\
			trace_error_##name(tsk->pid,						\
					   model_get_state_name_##name(curr_state),		\
					   model_get_event_name_##name(event));			\
			return false;								\
		}										\
		if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) {	\
			trace_event_##name(tsk->pid,						\
					   model_get_state_name_##name(curr_state),		\
					   model_get_event_name_##name(event),			\
					   model_get_state_name_##name(next_state),		\
					   model_is_final_state_##name(next_state));		\
			return true;								\
		}										\
	}											\
												\
	trace_rv_retries_error(#name, model_get_event_name_##name(event));			\
	pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS)					\
		" retries reached for event %s, resetting monitor %s",				\
		model_get_event_name_##name(event), #name);					\
	return false;										\
}

/*
 * Functions to define, init and get a global monitor.
 */
#define DECLARE_DA_MON_INIT_GLOBAL(name, type)							\
												\
/*												\
 * global monitor (a single variable)								\
 */												\
static struct da_monitor da_mon_##name;								\
												\
/*												\
 * da_get_monitor_##name - return the global monitor address					\
 */												\
static struct da_monitor *da_get_monitor_##name(void)						\
{												\
	return &da_mon_##name;									\
}												\
												\
/*												\
 * da_monitor_reset_all_##name - reset the single monitor					\
 */												\
static void da_monitor_reset_all_##name(void)							\
{												\
	da_monitor_reset_##name(da_get_monitor_##name());					\
}												\
												\
/*												\
 * da_monitor_init_##name - initialize a monitor						\
 */												\
static inline int da_monitor_init_##name(void)							\
{												\
	da_monitor_reset_all_##name();								\
	return 0;										\
}												\
												\
/*												\
 * da_monitor_destroy_##name - destroy the monitor						\
 */												\
static inline void da_monitor_destroy_##name(void)						\
{												\
	return;											\
}

/*
 * Functions to define, init and get a per-cpu monitor.
 */
#define DECLARE_DA_MON_INIT_PER_CPU(name, type)							\
												\
/*												\
 * per-cpu monitor variables									\
 */												\
static DEFINE_PER_CPU(struct da_monitor, da_mon_##name);					\
												\
/*												\
 * da_get_monitor_##name - return current CPU monitor address					\
 */												\
static struct da_monitor *da_get_monitor_##name(void)						\
{												\
	return this_cpu_ptr(&da_mon_##name);							\
}												\
												\
/*												\
 * da_monitor_reset_all_##name - reset all CPUs' monitor					\
 */												\
static void da_monitor_reset_all_##name(void)							\
{												\
	struct da_monitor *da_mon;								\
	int cpu;										\
	for_each_cpu(cpu, cpu_online_mask) {							\
		da_mon = per_cpu_ptr(&da_mon_##name, cpu);					\
		da_monitor_reset_##name(da_mon);						\
	}											\
}												\
												\
/*												\
 * da_monitor_init_##name - initialize all CPUs' monitor					\
 */												\
static inline int da_monitor_init_##name(void)							\
{												\
	da_monitor_reset_all_##name();								\
	return 0;										\
}												\
												\
/*												\
 * da_monitor_destroy_##name - destroy the monitor						\
 */												\
static inline void da_monitor_destroy_##name(void)						\
{												\
	return;											\
}

/*
 * Functions to define, init and get a per-task monitor.
 */
#define DECLARE_DA_MON_INIT_PER_TASK(name, type)						\
												\
/*												\
 * The per-task monitor is stored a vector in the task struct. This variable			\
 * stores the position on the vector reserved for this monitor.					\
 */												\
static int task_mon_slot_##name = RV_PER_TASK_MONITOR_INIT;					\
												\
/*												\
 * da_get_monitor_##name - return the monitor in the allocated slot for tsk 			\
 */												\
static inline struct da_monitor *da_get_monitor_##name(struct task_struct *tsk)			\
{												\
	return &tsk->rv[task_mon_slot_##name].da_mon;						\
}												\
												\
static void da_monitor_reset_all_##name(void)							\
{												\
	struct task_struct *g, *p;								\
	int cpu;										\
												\
	read_lock(&tasklist_lock);								\
	for_each_process_thread(g, p)								\
		da_monitor_reset_##name(da_get_monitor_##name(p));				\
	for_each_present_cpu(cpu)								\
		da_monitor_reset_##name(da_get_monitor_##name(idle_task(cpu)));			\
	read_unlock(&tasklist_lock);								\
}												\
												\
/*												\
 * da_monitor_init_##name - initialize the per-task monitor					\
 *												\
 * Try to allocate a slot in the task's vector of monitors. If there				\
 * is an available slot, use it and reset all task's monitor.					\
 */												\
static int da_monitor_init_##name(void)								\
{												\
	int slot;										\
												\
	slot = rv_get_task_monitor_slot();							\
	if (slot < 0 || slot >= RV_PER_TASK_MONITOR_INIT)					\
		return slot;									\
												\
	task_mon_slot_##name = slot;								\
												\
	da_monitor_reset_all_##name();								\
	return 0;										\
}												\
												\
/*												\
 * da_monitor_destroy_##name - return the allocated slot					\
 */												\
static inline void da_monitor_destroy_##name(void)						\
{												\
	if (task_mon_slot_##name == RV_PER_TASK_MONITOR_INIT) {					\
		WARN_ONCE(1, "Disabling a disabled monitor: " #name);				\
		return;										\
	}											\
	rv_put_task_monitor_slot(task_mon_slot_##name);						\
	task_mon_slot_##name = RV_PER_TASK_MONITOR_INIT;					\
	return;											\
}

/*
 * Handle event for implicit monitor: da_get_monitor_##name() will figure out
 * the monitor.
 */
#define DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)					\
												\
static inline void __da_handle_event_##name(struct da_monitor *da_mon,				\
					    enum events_##name event)				\
{												\
	bool retval;										\
												\
	retval = da_event_##name(da_mon, event);						\
	if (!retval)										\
		da_monitor_reset_##name(da_mon);						\
}												\
												\
/*												\
 * da_handle_event_##name - handle an event							\
 */												\
static inline void da_handle_event_##name(enum events_##name event)				\
{												\
	struct da_monitor *da_mon = da_get_monitor_##name();					\
	bool retval;										\
												\
	retval = da_monitor_handling_event_##name(da_mon);					\
	if (!retval)										\
		return;										\
												\
	__da_handle_event_##name(da_mon, event);						\
}												\
												\
/*												\
 * da_handle_start_event_##name - start monitoring or handle event				\
 *												\
 * This function is used to notify the monitor that the system is returning			\
 * to the initial state, so the monitor can start monitoring in the next event.			\
 * Thus:											\
 *												\
 * If the monitor already started, handle the event.						\
 * If the monitor did not start yet, start the monitor but skip the event.			\
 */												\
static inline bool da_handle_start_event_##name(enum events_##name event)			\
{												\
	struct da_monitor *da_mon;								\
												\
	if (!da_monitor_enabled_##name())							\
		return 0;									\
												\
	da_mon = da_get_monitor_##name();							\
												\
	if (unlikely(!da_monitoring_##name(da_mon))) {						\
		da_monitor_start_##name(da_mon);						\
		return 0;									\
	}											\
												\
	__da_handle_event_##name(da_mon, event);						\
												\
	return 1;										\
}												\
												\
/*												\
 * da_handle_start_run_event_##name - start monitoring and handle event				\
 *												\
 * This function is used to notify the monitor that the system is in the			\
 * initial state, so the monitor can start monitoring and handling event.			\
 */												\
static inline bool da_handle_start_run_event_##name(enum events_##name event)			\
{												\
	struct da_monitor *da_mon;								\
												\
	if (!da_monitor_enabled_##name())							\
		return 0;									\
												\
	da_mon = da_get_monitor_##name();							\
												\
	if (unlikely(!da_monitoring_##name(da_mon)))						\
		da_monitor_start_##name(da_mon);						\
												\
	__da_handle_event_##name(da_mon, event);						\
												\
	return 1;										\
}

/*
 * Handle event for per task.
 */
#define DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type)					\
												\
static inline void										\
__da_handle_event_##name(struct da_monitor *da_mon, struct task_struct *tsk,			\
			 enum events_##name event)						\
{												\
	bool retval;										\
												\
	retval = da_event_##name(da_mon, tsk, event);						\
	if (!retval)										\
		da_monitor_reset_##name(da_mon);						\
}												\
												\
/*												\
 * da_handle_event_##name - handle an event							\
 */												\
static inline void										\
da_handle_event_##name(struct task_struct *tsk, enum events_##name event)			\
{												\
	struct da_monitor *da_mon = da_get_monitor_##name(tsk);					\
	bool retval;										\
												\
	retval = da_monitor_handling_event_##name(da_mon);					\
	if (!retval)										\
		return;										\
												\
	__da_handle_event_##name(da_mon, tsk, event);						\
}												\
												\
/*												\
 * da_handle_start_event_##name - start monitoring or handle event				\
 *												\
 * This function is used to notify the monitor that the system is returning			\
 * to the initial state, so the monitor can start monitoring in the next event.			\
 * Thus:											\
 *												\
 * If the monitor already started, handle the event.						\
 * If the monitor did not start yet, start the monitor but skip the event.			\
 */												\
static inline bool										\
da_handle_start_event_##name(struct task_struct *tsk, enum events_##name event)			\
{												\
	struct da_monitor *da_mon;								\
												\
	if (!da_monitor_enabled_##name())							\
		return 0;									\
												\
	da_mon = da_get_monitor_##name(tsk);							\
												\
	if (unlikely(!da_monitoring_##name(da_mon))) {						\
		da_monitor_start_##name(da_mon);						\
		return 0;									\
	}											\
												\
	__da_handle_event_##name(da_mon, tsk, event);						\
												\
	return 1;										\
}												\
												\
/*												\
 * da_handle_start_run_event_##name - start monitoring and handle event				\
 *												\
 * This function is used to notify the monitor that the system is in the			\
 * initial state, so the monitor can start monitoring and handling event.			\
 */												\
static inline bool										\
da_handle_start_run_event_##name(struct task_struct *tsk, enum events_##name event)		\
{												\
	struct da_monitor *da_mon;								\
												\
	if (!da_monitor_enabled_##name())							\
		return 0;									\
												\
	da_mon = da_get_monitor_##name(tsk);							\
												\
	if (unlikely(!da_monitoring_##name(da_mon)))						\
		da_monitor_start_##name(da_mon);						\
												\
	__da_handle_event_##name(da_mon, tsk, event);						\
												\
	return 1;										\
}

/*
 * Entry point for the global monitor.
 */
#define DECLARE_DA_MON_GLOBAL(name, type)							\
												\
DECLARE_AUTOMATA_HELPERS(name, type)								\
DECLARE_DA_MON_GENERIC_HELPERS(name, type)							\
DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type)						\
DECLARE_DA_MON_INIT_GLOBAL(name, type)								\
DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)

/*
 * Entry point for the per-cpu monitor.
 */
#define DECLARE_DA_MON_PER_CPU(name, type)							\
												\
DECLARE_AUTOMATA_HELPERS(name, type)								\
DECLARE_DA_MON_GENERIC_HELPERS(name, type)							\
DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type)						\
DECLARE_DA_MON_INIT_PER_CPU(name, type)								\
DECLARE_DA_MON_MONITOR_HANDLER_IMPLICIT(name, type)

/*
 * Entry point for the per-task monitor.
 */
#define DECLARE_DA_MON_PER_TASK(name, type)							\
												\
DECLARE_AUTOMATA_HELPERS(name, type)								\
DECLARE_DA_MON_GENERIC_HELPERS(name, type)							\
DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type)						\
DECLARE_DA_MON_INIT_PER_TASK(name, type)							\
DECLARE_DA_MON_MONITOR_HANDLER_PER_TASK(name, type)