/* SPDX-License-Identifier: GPL-2.0 */ /* * Copyright (C) 2025-2028 Red Hat, Inc. Gabriele Monaco * * 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 #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 #include /* 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