/* SPDX-License-Identifier: GPL-2.0 *//* * Copyright (C) 2025-2028 Red Hat, Inc. Gabriele Monaco <gmonaco@redhat.com> * * 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 inline void ha_cancel_timer_sync(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#define da_monitor_sync_hook() synchronize_rcu() #if !defined(HA_SKIP_AUTO_CLEANUP) && RV_MON_TYPE == RV_MON_PER_TASK/* * Automatic cleanup handlers for per-task HA monitors, only skip if you know * what you are doing (e.g. you want to implement cleanup manually in another * handler doing more things). */static void ha_handle_sched_process_exit(void *data, struct task_struct *p,					 bool group_dead); #define ha_monitor_enable_hook()                                             \	rv_attach_trace_probe(__stringify(MONITOR_NAME), sched_process_exit, \			      ha_handle_sched_process_exit)#define ha_monitor_disable_hook()                                            \	rv_detach_trace_probe(__stringify(MONITOR_NAME), sched_process_exit, \			      ha_handle_sched_process_exit)#else#define ha_monitor_enable_hook() ((void)0)#define ha_monitor_disable_hook() ((void)0)#endif #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_WHEELstatic void ha_monitor_timer_callback(struct timer_list *timer);#elif HA_TIMER_TYPE == HA_TIMER_HRTIMERstatic 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 */ static bool ha_mon_destroying; static int ha_monitor_init(void){	int ret; 	WRITE_ONCE(ha_mon_destroying, false);	ret = da_monitor_init();	if (ret == 0)		ha_monitor_enable_hook();	return ret;} static void ha_monitor_destroy(void){	WRITE_ONCE(ha_mon_destroying, true);	ha_monitor_disable_hook();	da_monitor_destroy();} /* 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. * Monitors that never started have their timer uninitialized, do not stop those. */static inline void ha_monitor_reset_env(struct da_monitor *da_mon){	struct ha_monitor *ha_mon = to_ha_monitor(da_mon); 	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_CPUstatic 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);} #if !defined(HA_SKIP_AUTO_CLEANUP) && RV_MON_TYPE == RV_MON_PER_TASKstatic void ha_handle_sched_process_exit(void *data, struct task_struct *p,					 bool group_dead){	struct da_monitor *da_mon = da_get_monitor(p); 	if (likely(da_monitoring(da_mon))) {		da_monitor_reset(da_mon);		ha_cancel_timer_sync(to_ha_monitor(da_mon));	}}#endif #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;} /* * __ha_monitor_timer_callback - generic callback representation * * This callback runs in an RCU read-side critical section to allow the * destruction sequence to easily synchronize_rcu() with all pending timers * after asynchronously disabling them. The ha_mon_destroying check ensures * any callback entering the RCU section after synchronize_rcu() completes * will see the flag and bail out immediately. */static inline void __ha_monitor_timer_callback(struct ha_monitor *ha_mon){	DECLARE_SEQ_BUF(env_string, ENV_BUFFER_SIZE);	enum states curr_state;	u64 time_ns; 	guard(rcu)();	if (unlikely(READ_ONCE(ha_mon_destroying)))		return;	/* Ensure consistent curr_state if we race with da_monitor_reset */	curr_state = smp_load_acquire(&ha_mon->da_mon.curr_state);	if (unlikely(!da_monitor_handling_event(&ha_mon->da_mon)))		return; 	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 store the time epoch - the timestamp when the clock was last reset. * They are read by subtracting the time epoch from the current time. */ /* * 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 bool ha_check_invariant_ns(struct ha_monitor *ha_mon, enum envs env,					 u64 time_ns, u64 expire_ns){	return READ_ONCE(ha_mon->env_store[env]) >= time_ns - expire_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 time_ns){	if (env < 0 || env >= ENV_MAX_STORED)		return 0;	if (ha_monitor_env_invalid(ha_mon, env))		return 0;	return ha_get_env(ha_mon, env, time_ns);} /* * 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 bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon, enum envs env,					    u64 time_ns, u64 expire_jiffy){	return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64() - expire_jiffy);}/* * 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 time_ns){	if (env < 0 || env >= ENV_MAX_STORED)		return 0;	if (ha_monitor_env_invalid(ha_mon, env))		return 0;	return ha_get_env(ha_mon, env, time_ns);} /* * 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, 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, 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);}static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon){	timer_delete_sync(&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, 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, time_ns); 	ha_start_timer_ns(ha_mon, ENV_MAX_STORED,			  jiffies_to_nsecs(expire - passed), time_ns);}

Lines 1–500 of 550. Load more