Something went wrong. Try again.
(I'm so sorry!) Linux kernel mirror (for testing) git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551/* 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);}/* * 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;}static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon){ hrtimer_cancel(&ha_mon->hrtimer);}#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;}static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon) { }#endif
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)#ifdef RV_MON_OPS_INIT#undef RV_MON_OPS_INIT#endif
#if RV_MON_TYPE == RV_MON_PER_TASK#define RV_MON_OPS_INIT() { \ .rv_this = &rv_this, \ .is_per_task = true, \ .task_slot = &task_mon_slot, \ .task_reset = da_reset, \}#else#define RV_MON_OPS_INIT() { \ .rv_this = &rv_this, \ .monitor_init = ha_monitor_init, \ .monitor_destroy = ha_monitor_destroy, \}#endif /* RV_MON_TYPE */#endif /* CONFIG_RV_MONITORS_KUNIT_TEST */
#endif