ha_monitor.h

/* SPDX-License-Identifier: GPL-2.0 */
/*
 * Copyright (C) 2025-2028 Red Hat, Inc. Gabriele Monaco <[email protected]>
 *
 * Hybrid automata (HA) monitor functions, to be used together
 * with automata models in C generated by the rvgen tool.
 *
 * This type of monitors extends the Deterministic automata (DA) class by
 * adding a set of environment variables (e.g. clocks) that can be used to
 * constraint the valid transitions.
 *
 * The rvgen tool is available at tools/verification/rvgen/
 *
 * For further information, see:
 *   Documentation/trace/rv/monitor_synthesis.rst
 */

#ifndef _RV_HA_MONITOR_H
#define _RV_HA_MONITOR_H

#include <rv/automata.h>

#ifndef da_id_type
#define da_id_type int
#endif

static inline void ha_monitor_init_env(struct da_monitor *da_mon);
static inline void ha_monitor_reset_env(struct da_monitor *da_mon);
static inline void ha_setup_timer(struct ha_monitor *ha_mon);
static inline bool ha_cancel_timer(struct ha_monitor *ha_mon);
static bool ha_monitor_handle_constraint(struct da_monitor *da_mon,
					 enum states curr_state,
					 enum events event,
					 enum states next_state,
					 da_id_type id);
#define da_monitor_event_hook ha_monitor_handle_constraint
#define da_monitor_init_hook ha_monitor_init_env
#define da_monitor_reset_hook ha_monitor_reset_env

#include <rv/da_monitor.h>
#include <linux/seq_buf.h>

/* This simplifies things since da_mon and ha_mon coexist in the same union */
_Static_assert(offsetof(struct ha_monitor, da_mon) == 0,
	       "da_mon must be the first element in an ha_mon!");
#define to_ha_monitor(da) container_of(da, struct ha_monitor, da_mon)

#define ENV_MAX CONCATENATE(env_max_, MONITOR_NAME)
#define ENV_MAX_STORED CONCATENATE(env_max_stored_, MONITOR_NAME)
#define envs CONCATENATE(envs_, MONITOR_NAME)

/* Environment storage before being reset */
#define ENV_INVALID_VALUE U64_MAX
/* Error with no event occurs only on timeouts */
#define EVENT_NONE EVENT_MAX
#define EVENT_NONE_LBL "none"
#define ENV_BUFFER_SIZE 64

#ifdef CONFIG_RV_REACTORS

/*
 * ha_react - trigger the reaction after a failed environment constraint
 *
 * The transition from curr_state with event is otherwise valid, but the
 * environment constraint is false. This function can be called also with no
 * event from a timer (state constraints only).
 */
static void ha_react(enum states curr_state, enum events event, char *env)
{
	rv_react(&rv_this,
		 "rv: monitor %s does not allow event %s on state %s with env %s\n",
		 __stringify(MONITOR_NAME),
		 event == EVENT_NONE ? EVENT_NONE_LBL : model_get_event_name(event),
		 model_get_state_name(curr_state), env);
}

#else /* CONFIG_RV_REACTOR */

static void ha_react(enum states curr_state, enum events event, char *env) { }
#endif

/*
 * model_get_state_name - return the (string) name of the given state
 */
static char *model_get_env_name(enum envs env)
{
	if ((env < 0) || (env >= ENV_MAX))
		return "INVALID";

	return RV_AUTOMATON_NAME.env_names[env];
}

/*
 * Monitors requiring a timer implementation need to request it explicitly.
 */
#ifndef HA_TIMER_TYPE
#define HA_TIMER_TYPE HA_TIMER_NONE
#endif

#if HA_TIMER_TYPE == HA_TIMER_WHEEL
static void ha_monitor_timer_callback(struct timer_list *timer);
#elif HA_TIMER_TYPE == HA_TIMER_HRTIMER
static enum hrtimer_restart ha_monitor_timer_callback(struct hrtimer *hrtimer);
#endif

/*
 * ktime_get_ns is expensive, since we usually don't require precise accounting
 * of changes within the same event, cache the current time at the beginning of
 * the constraint handler and use the cache for subsequent calls.
 * Monitors without ns clocks automatically skip this.
 */
#ifdef HA_CLK_NS
#define ha_get_ns() ktime_get_ns()
#else
#define ha_get_ns() 0
#endif /* HA_CLK_NS */

/* Should be supplied by the monitor */
static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs env, u64 time_ns);
static bool ha_verify_constraint(struct ha_monitor *ha_mon,
				 enum states curr_state,
				 enum events event,
				 enum states next_state,
				 u64 time_ns);

/*
 * ha_monitor_reset_all_stored - reset all environment variables in the monitor
 */
static inline void ha_monitor_reset_all_stored(struct ha_monitor *ha_mon)
{
	for (int i = 0; i < ENV_MAX_STORED; i++)
		WRITE_ONCE(ha_mon->env_store[i], ENV_INVALID_VALUE);
}

/*
 * ha_monitor_init_env - setup timer and reset all environment
 *
 * Called from a hook in the DA start functions, it supplies the da_mon
 * corresponding to the current ha_mon.
 * Not all hybrid automata require the timer, still set it for simplicity.
 */
static inline void ha_monitor_init_env(struct da_monitor *da_mon)
{
	struct ha_monitor *ha_mon = to_ha_monitor(da_mon);

	ha_monitor_reset_all_stored(ha_mon);
	ha_setup_timer(ha_mon);
}

/*
 * ha_monitor_reset_env - stop timer and reset all environment
 *
 * Called from a hook in the DA reset functions, it supplies the da_mon
 * corresponding to the current ha_mon.
 * Not all hybrid automata require the timer, still clear it for simplicity.
 */
static inline void ha_monitor_reset_env(struct da_monitor *da_mon)
{
	struct ha_monitor *ha_mon = to_ha_monitor(da_mon);

	/* Initialisation resets the monitor before initialising the timer */
	if (likely(da_monitoring(da_mon)))
		ha_cancel_timer(ha_mon);
}

/*
 * ha_monitor_env_invalid - return true if env has not been initialised
 */
static inline bool ha_monitor_env_invalid(struct ha_monitor *ha_mon, enum envs env)
{
	return READ_ONCE(ha_mon->env_store[env]) == ENV_INVALID_VALUE;
}

static inline void ha_get_env_string(struct seq_buf *s,
				     struct ha_monitor *ha_mon, u64 time_ns)
{
	const char *format_str = "%s=%llu";

	for (int i = 0; i < ENV_MAX; i++) {
		seq_buf_printf(s, format_str, model_get_env_name(i),
			       ha_get_env(ha_mon, i, time_ns));
		format_str = ",%s=%llu";
	}
}

#if RV_MON_TYPE == RV_MON_GLOBAL || RV_MON_TYPE == RV_MON_PER_CPU
static inline void ha_trace_error_env(struct ha_monitor *ha_mon,
				      char *curr_state, char *event, char *env,
				      da_id_type id)
{
	CONCATENATE(trace_error_env_, MONITOR_NAME)(curr_state, event, env);
}
#elif RV_MON_TYPE == RV_MON_PER_TASK || RV_MON_TYPE == RV_MON_PER_OBJ

#define ha_get_target(ha_mon) da_get_target(&ha_mon->da_mon)

static inline void ha_trace_error_env(struct ha_monitor *ha_mon,
				      char *curr_state, char *event, char *env,
				      da_id_type id)
{
	CONCATENATE(trace_error_env_, MONITOR_NAME)(id, curr_state, event, env);
}
#endif /* RV_MON_TYPE */

/*
 * ha_get_monitor - return the current monitor
 */
#define ha_get_monitor(...) to_ha_monitor(da_get_monitor(__VA_ARGS__))

/*
 * ha_monitor_handle_constraint - handle the constraint on the current transition
 *
 * If the monitor implementation defines a constraint in the transition from
 * curr_state to event, react and trace appropriately as well as return false.
 * This function is called from the hook in the DA event handle function and
 * triggers a failure in the monitor.
 */
static bool ha_monitor_handle_constraint(struct da_monitor *da_mon,
					 enum states curr_state,
					 enum events event,
					 enum states next_state,
					 da_id_type id)
{
	struct ha_monitor *ha_mon = to_ha_monitor(da_mon);
	u64 time_ns = ha_get_ns();
	DECLARE_SEQ_BUF(env_string, ENV_BUFFER_SIZE);

	if (ha_verify_constraint(ha_mon, curr_state, event, next_state, time_ns))
		return true;

	ha_get_env_string(&env_string, ha_mon, time_ns);
	ha_react(curr_state, event, env_string.buffer);
	ha_trace_error_env(ha_mon,
			   model_get_state_name(curr_state),
			   model_get_event_name(event),
			   env_string.buffer, id);
	return false;
}

static inline void __ha_monitor_timer_callback(struct ha_monitor *ha_mon)
{
	enum states curr_state = READ_ONCE(ha_mon->da_mon.curr_state);
	DECLARE_SEQ_BUF(env_string, ENV_BUFFER_SIZE);
	u64 time_ns = ha_get_ns();

	ha_get_env_string(&env_string, ha_mon, time_ns);
	ha_react(curr_state, EVENT_NONE, env_string.buffer);
	ha_trace_error_env(ha_mon, model_get_state_name(curr_state),
			   EVENT_NONE_LBL, env_string.buffer,
			   da_get_id(&ha_mon->da_mon));

	da_monitor_reset(&ha_mon->da_mon);
}

/*
 * The clock variables have 2 different representations in the env_store:
 * - The guard representation is the timestamp of the last reset
 * - The invariant representation is the timestamp when the invariant expires
 * As the representations are incompatible, care must be taken when switching
 * between them: the invariant representation can only be used when starting a
 * timer when the previous representation was guard (e.g. no other invariant
 * started since the last reset operation).
 * Likewise, switching from invariant to guard representation without a reset
 * can be done only by subtracting the exact value used to start the invariant.
 *
 * Reading the environment variable (ha_get_clk) also reflects this difference
 * any reads in states that have an invariant return the (possibly negative)
 * time since expiration, other reads return the time since last reset.
 */

/*
 * Helper functions for env variables describing clocks with ns granularity
 */
static inline u64 ha_get_clk_ns(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
{
	return time_ns - READ_ONCE(ha_mon->env_store[env]);
}
static inline void ha_reset_clk_ns(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
{
	WRITE_ONCE(ha_mon->env_store[env], time_ns);
}
static inline void ha_set_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
				       u64 value, u64 time_ns)
{
	WRITE_ONCE(ha_mon->env_store[env], time_ns + value);
}
static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon,
					 enum envs env, u64 time_ns)
{
	return READ_ONCE(ha_mon->env_store[env]) >= time_ns;
}
/*
 * ha_invariant_passed_ns - prepare the invariant and return the time since reset
 */
static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env,
				   u64 expire, u64 time_ns)
{
	u64 passed = 0;

	if (env < 0 || env >= ENV_MAX_STORED)
		return 0;
	if (ha_monitor_env_invalid(ha_mon, env))
		return 0;
	passed = ha_get_env(ha_mon, env, time_ns);
	ha_set_invariant_ns(ha_mon, env, expire - passed, time_ns);
	return passed;
}

/*
 * Helper functions for env variables describing clocks with jiffy granularity
 */
static inline u64 ha_get_clk_jiffy(struct ha_monitor *ha_mon, enum envs env)
{
	return get_jiffies_64() - READ_ONCE(ha_mon->env_store[env]);
}
static inline void ha_reset_clk_jiffy(struct ha_monitor *ha_mon, enum envs env)
{
	WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64());
}
static inline void ha_set_invariant_jiffy(struct ha_monitor *ha_mon,
					  enum envs env, u64 value)
{
	WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64() + value);
}
static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon,
					    enum envs env, u64 time_ns)
{
	return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64());

}
/*
 * ha_invariant_passed_jiffy - prepare the invariant and return the time since reset
 */
static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env,
				      u64 expire, u64 time_ns)
{
	u64 passed = 0;

	if (env < 0 || env >= ENV_MAX_STORED)
		return 0;
	if (ha_monitor_env_invalid(ha_mon, env))
		return 0;
	passed = ha_get_env(ha_mon, env, time_ns);
	ha_set_invariant_jiffy(ha_mon, env, expire - passed);
	return passed;
}

/*
 * Retrieve the last reset time (guard representation) from the invariant
 * representation (expiration).
 * It the caller's responsibility to make sure the storage was actually in the
 * invariant representation (e.g. the current state has an invariant).
 * The provided value must be the same used when starting the invariant.
 *
 * This function's access to the storage is NOT atomic, due to the rarity when
 * this is used. If a monitor allows writes concurrent to this, likely
 * other things are broken and need rethinking the model or additional locking.
 */
static inline void ha_inv_to_guard(struct ha_monitor *ha_mon, enum envs env,
				   u64 value, u64 time_ns)
{
	WRITE_ONCE(ha_mon->env_store[env], READ_ONCE(ha_mon->env_store[env]) - value);
}

#if HA_TIMER_TYPE == HA_TIMER_WHEEL
/*
 * Helper functions to handle the monitor timer.
 * Not all monitors require a timer, in such case the timer will be set up but
 * never armed.
 * Timers start since the last reset of the supplied env or from now if env is
 * not an environment variable. If env was not initialised no timer starts.
 * Timers can expire on any CPU unless the monitor is per-cpu,
 * where we assume every event occurs on the local CPU.
 */
static void ha_monitor_timer_callback(struct timer_list *timer)
{
	struct ha_monitor *ha_mon = container_of(timer, struct ha_monitor, timer);

	__ha_monitor_timer_callback(ha_mon);
}
static inline void ha_setup_timer(struct ha_monitor *ha_mon)
{
	int mode = 0;

	if (RV_MON_TYPE == RV_MON_PER_CPU)
		mode |= TIMER_PINNED;
	timer_setup(&ha_mon->timer, ha_monitor_timer_callback, mode);
}
static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
					u64 expire, u64 time_ns)
{
	u64 passed = ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns);

	mod_timer(&ha_mon->timer, get_jiffies_64() + expire - passed);
}
static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
				     u64 expire, u64 time_ns)
{
	u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);

	ha_start_timer_jiffy(ha_mon, ENV_MAX_STORED,
			     nsecs_to_jiffies(expire - passed + TICK_NSEC - 1), time_ns);
}
/*
 * ha_cancel_timer - Cancel the timer
 *
 * Returns:
 *  *  1 when the timer was active
 *  *  0 when the timer was not active or running a callback
 */
static inline bool ha_cancel_timer(struct ha_monitor *ha_mon)
{
	return timer_delete(&ha_mon->timer);
}
#elif HA_TIMER_TYPE == HA_TIMER_HRTIMER
/*
 * Helper functions to handle the monitor timer.
 * Not all monitors require a timer, in such case the timer will be set up but
 * never armed.
 * Timers start since the last reset of the supplied env or from now if env is
 * not an environment variable. If env was not initialised no timer starts.
 * Timers can expire on any CPU unless the monitor is per-cpu,
 * where we assume every event occurs on the local CPU.
 */
static enum hrtimer_restart ha_monitor_timer_callback(struct hrtimer *hrtimer)
{
	struct ha_monitor *ha_mon = container_of(hrtimer, struct ha_monitor, hrtimer);

	__ha_monitor_timer_callback(ha_mon);
	return HRTIMER_NORESTART;
}
static inline void ha_setup_timer(struct ha_monitor *ha_mon)
{
	hrtimer_setup(&ha_mon->hrtimer, ha_monitor_timer_callback,
		      CLOCK_MONOTONIC, HRTIMER_MODE_REL_HARD);
}
static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
				     u64 expire, u64 time_ns)
{
	int mode = HRTIMER_MODE_REL_HARD;
	u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);

	if (RV_MON_TYPE == RV_MON_PER_CPU)
		mode |= HRTIMER_MODE_PINNED;
	hrtimer_start(&ha_mon->hrtimer, ns_to_ktime(expire - passed), mode);
}
static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
					u64 expire, u64 time_ns)
{
	u64 passed = ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns);

	ha_start_timer_ns(ha_mon, ENV_MAX_STORED,
			  jiffies_to_nsecs(expire - passed), time_ns);
}
/*
 * ha_cancel_timer - Cancel the timer
 *
 * Returns:
 *  *  1 when the timer was active
 *  *  0 when the timer was not active or running a callback
 */
static inline bool ha_cancel_timer(struct ha_monitor *ha_mon)
{
	return hrtimer_try_to_cancel(&ha_mon->hrtimer) == 1;
}
#else /* HA_TIMER_NONE */
/*
 * Start function is intentionally not defined, monitors using timers must
 * set HA_TIMER_TYPE to either HA_TIMER_WHEEL or HA_TIMER_HRTIMER.
 */
static inline void ha_setup_timer(struct ha_monitor *ha_mon) { }
static inline bool ha_cancel_timer(struct ha_monitor *ha_mon)
{
	return false;
}
#endif

#endif