sched/cache: Keep nr_pref_llc_running in the runnable domain, to fix LLC mis-scheduling buggrafted

alb_break_llc() decides whether to break LLC preference during active
load balance. It does so by testing that every runnable fair task on the
source rq prefers its LLC:

	env->src_rq->nr_pref_llc_running == env->src_rq->cfs.h_nr_runnable

But the two counters cover different sets. nr_pref_llc_running is updated
in account_llc_enqueue()/account_llc_dequeue(), next to cfs_rq->nr_queued,
so it follows queued tasks. h_nr_runnable is updated in set_delayed()/
clear_delayed() and drops delay-dequeued tasks.

So under DELAY_DEQUEUE, a preferring task that goes to sleep stays counted
in nr_pref_llc_running while h_nr_runnable falls. The equality then breaks,
alb_break_llc() returns false, and active balance is free to pull a task
off its preferred LLC. Active balance only moves runnable tasks, and this
is the only LLC check it consults: once the stopper runs, LBF_ACTIVE_LB
skips the per-task test in can_migrate_task(). The runnable set is the one
we want.

Fix it on the counter side. A task should be counted in
nr_pref_llc_running exactly while it is both queued on its preferred LLC
(pref_llc_queued) and runnable (!sched_delayed). Define that membership
once in task_pref_llc_runnable(), and adjust the counter only through
pref_llc_running_inc()/pref_llc_running_dec() from the four sites that
change either input: account_llc_enqueue(), account_llc_dequeue(),
set_delayed() and clear_delayed(). Gating every update on the same
predicate keeps the delay, wake and dequeue paths from double-counting
or underflowing; see the comments at those sites for the ordering.

nr_llc_running and sd->llc_counts are not touched and stay on queued
semantics.

Fixes: 714059f79ff0 ("sched/cache: Handle moving single tasks to/from their preferred LLC")
Closes: https://lore.kernel.org/lkml/20260827135000.735138-1-zhanxusheng@xiaomi.com/
Reported-by: Zhan Xusheng <zhanxusheng@xiaomi.com>
Suggested-by: Chen Yu <yu.c.chen@intel.com>
Signed-off-by: Tim Chen <tim.c.chen@linux.intel.com>
Signed-off-by: Peter Zijlstra (Intel) <peterz@infradead.org>
Signed-off-by: Ingo Molnar <mingo@kernel.org>
Reviewed-by: Kayra Cizmeci <kayracizmeci@gmail.com>
Cc: <stable@kernel.org> # v7.2.x
Link: https://patch.msgid.link/06af61afedac32e6477f57feb4d658f6c411c3af.1790035273.git.tim.c.chen@linux.intel.com

6 files changed, 1849 insertions, 0 deletions

diff --git a/include/rv/automata.h b/include/rv/automata.h
new file mode 100644
index 000000000..4a4eb40cf
--- /dev/null
+++ b/include/rv/automata.h
@@ -0,0 +1,81 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira  <bristot@kernel.org>
+ *
+ * Deterministic automata helper functions, to be used with the automata
+ * models in C generated by the dot2k tool.
+ */
+
+#ifndef _RV_AUTOMATA_H
+#define _RV_AUTOMATA_H
+
+#ifndef MONITOR_NAME
+#error "MONITOR_NAME macro is not defined. Did you include $(MODEL_NAME).h generated by rvgen?"
+#endif
+
+#define RV_AUTOMATON_NAME CONCATENATE(automaton_, MONITOR_NAME)
+#define EVENT_MAX CONCATENATE(event_max_, MONITOR_NAME)
+#define STATE_MAX CONCATENATE(state_max_, MONITOR_NAME)
+#define events CONCATENATE(events_, MONITOR_NAME)
+#define states CONCATENATE(states_, MONITOR_NAME)
+
+/*
+ * model_get_state_name - return the (string) name of the given state
+ */
+static char *model_get_state_name(enum states state)
+{
+	if ((state < 0) || (state >= STATE_MAX))
+		return "INVALID";
+
+	return RV_AUTOMATON_NAME.state_names[state];
+}
+
+/*
+ * model_get_event_name - return the (string) name of the given event
+ */
+static char *model_get_event_name(enum events event)
+{
+	if ((event < 0) || (event >= EVENT_MAX))
+		return "INVALID";
+
+	return RV_AUTOMATON_NAME.event_names[event];
+}
+
+/*
+ * model_get_initial_state - return the automaton's initial state
+ */
+static inline enum states model_get_initial_state(void)
+{
+	return RV_AUTOMATON_NAME.initial_state;
+}
+
+/*
+ * model_get_next_state - process an automaton event occurrence
+ *
+ * Given the current state (curr_state) and the event (event), returns
+ * the next state, or INVALID_STATE in case of error.
+ */
+static inline enum states model_get_next_state(enum states curr_state,
+					enum events event)
+{
+	if ((curr_state < 0) || (curr_state >= STATE_MAX))
+		return INVALID_STATE;
+
+	if ((event < 0) || (event >= EVENT_MAX))
+		return INVALID_STATE;
+
+	return RV_AUTOMATON_NAME.function[curr_state][event];
+}
+
+/*
+ * model_is_final_state - check if the given state is a final state
+ */
+static inline bool model_is_final_state(enum states state)
+{
+	if ((state < 0) || (state >= STATE_MAX))
+		return 0;
+
+	return RV_AUTOMATON_NAME.final_states[state];
+}
+
+#endif
diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h
new file mode 100644
index 000000000..6fc5ef814
--- /dev/null
+++ b/include/rv/da_monitor.h
@@ -0,0 +1,934 @@
+/* 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 rvgen tool.
+ *
+ * The rvgen tool is available at tools/verification/rvgen/
+ *
+ * For further information, see:
+ *   Documentation/trace/rv/monitor_synthesis.rst
+ */
+
+#ifndef _RV_DA_MONITOR_H
+#define _RV_DA_MONITOR_H
+
+#include <rv/automata.h>
+#include <linux/rv.h>
+#include <rv/kunit.h>
+#include <linux/stringify.h>
+#include <linux/bug.h>
+#include <linux/sched.h>
+#include <linux/slab.h>
+#include <linux/hashtable.h>
+
+/*
+ * Per-cpu variables require a unique name although static in some
+ * configurations (e.g. alpha modules).
+ */
+#define DA_MON_NAME CONCATENATE(da_mon_, MONITOR_NAME)
+
+static struct rv_monitor rv_this;
+
+/*
+ * Hook to allow the implementation of hybrid automata: define it with a
+ * function that takes curr_state, event and next_state and returns true if the
+ * environment constraints (e.g. timing) are satisfied, false otherwise.
+ */
+#ifndef da_monitor_event_hook
+#define da_monitor_event_hook(...) true
+#endif
+
+/*
+ * Hook to allow the implementation of hybrid automata: define it with a
+ * function that takes the da_monitor and performs further initialisation
+ * (e.g. reset set up timers).
+ */
+#ifndef da_monitor_init_hook
+#define da_monitor_init_hook(da_mon)
+#endif
+
+/*
+ * Hook to allow the implementation of hybrid automata: define it with a
+ * function that takes the da_monitor and performs further reset (e.g. reset
+ * all clocks).
+ */
+#ifndef da_monitor_reset_hook
+#define da_monitor_reset_hook(da_mon)
+#endif
+
+/*
+ * Hook to allow the implementation of hybrid automata: define it with a
+ * function that waits for the termination of all monitors background
+ * activities (e.g. all timers). This hook can sleep.
+ */
+#ifndef da_monitor_sync_hook
+#define da_monitor_sync_hook()
+#endif
+
+/*
+ * Type for the target id, default to int but can be overridden.
+ * A long type can work as hash table key (PER_OBJ) but will be downgraded to
+ * int in the event tracepoint.
+ * Unused for implicit monitors.
+ */
+#ifndef da_id_type
+#define da_id_type int
+#endif
+
+static void react(enum states curr_state, enum events event)
+{
+	rv_react(&rv_this,
+		 "rv: monitor %s does not allow event %s on state %s\n",
+		 __stringify(MONITOR_NAME),
+		 model_get_event_name(event),
+		 model_get_state_name(curr_state));
+}
+
+/*
+ * da_monitor_reset_state - reset a monitor and setting it to init state
+ */
+static inline void da_monitor_reset_state(struct da_monitor *da_mon)
+{
+	WRITE_ONCE(da_mon->monitoring, 0);
+	/* Pair with load in __ha_monitor_timer_callback */
+	smp_store_release(&da_mon->curr_state, model_get_initial_state());
+}
+
+/*
+ * da_monitor_reset - reset a monitor and setting it to init state
+ */
+static inline void da_monitor_reset(struct da_monitor *da_mon)
+{
+	da_monitor_reset_hook(da_mon);
+	da_monitor_reset_state(da_mon);
+}
+
+/*
+ * da_monitor_start - 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(struct da_monitor *da_mon)
+{
+	da_mon->curr_state = model_get_initial_state();
+	da_monitor_init_hook(da_mon);
+	/* Pairs with smp_load_acquire in da_monitoring(). */
+	smp_store_release(&da_mon->monitoring, 1);
+}
+
+/*
+ * da_monitoring - returns true if the monitor is processing events
+ */
+static inline bool da_monitoring(struct da_monitor *da_mon)
+{
+	/* Pairs with smp_store_release in da_monitor_start(). */
+	return smp_load_acquire(&da_mon->monitoring);
+}
+
+/*
+ * da_monitor_enabled - checks if the monitor is enabled
+ */
+static inline bool da_monitor_enabled(void)
+{
+	/* global switch */
+	if (unlikely(!rv_monitoring_on()))
+		return 0;
+
+	/* monitor enabled */
+	if (unlikely(!rv_this.enabled))
+		return 0;
+
+	return 1;
+}
+
+/*
+ * da_monitor_handling_event - checks if the monitor is ready to handle events
+ */
+static inline bool da_monitor_handling_event(struct da_monitor *da_mon)
+{
+	if (!da_monitor_enabled())
+		return 0;
+
+	/* monitor is actually monitoring */
+	if (unlikely(!da_monitoring(da_mon)))
+		return 0;
+
+	return 1;
+}
+
+#if RV_MON_TYPE == RV_MON_GLOBAL
+/*
+ * Functions to define, init and get a global monitor.
+ */
+
+/*
+ * global monitor (a single variable)
+ */
+static struct da_monitor DA_MON_NAME;
+
+/*
+ * da_get_monitor - return the global monitor address
+ */
+static struct da_monitor *da_get_monitor(void)
+{
+	return &DA_MON_NAME;
+}
+
+/*
+ * __da_monitor_reset_all - reset the single monitor
+ */
+static void __da_monitor_reset_all(void (*reset)(struct da_monitor *))
+{
+	reset(da_get_monitor());
+}
+
+/*
+ * da_monitor_reset_all - reset the single monitor
+ */
+static void da_monitor_reset_all(void)
+{
+	__da_monitor_reset_all(da_monitor_reset);
+}
+
+/*
+ * da_monitor_reset_state_all - reset the single monitor
+ */
+static inline void da_monitor_reset_state_all(void)
+{
+	__da_monitor_reset_all(da_monitor_reset_state);
+}
+
+/*
+ * da_monitor_init - initialize a monitor
+ */
+static inline int da_monitor_init(void)
+{
+	da_monitor_reset_state_all();
+	return 0;
+}
+
+/*
+ * da_monitor_destroy - destroy the monitor
+ */
+static inline void da_monitor_destroy(void)
+{
+	da_monitor_reset_all();
+	da_monitor_sync_hook();
+}
+
+#ifndef da_implicit_guard
+#define da_implicit_guard()
+#endif
+
+#elif RV_MON_TYPE == RV_MON_PER_CPU
+/*
+ * Functions to define, init and get a per-cpu monitor.
+ */
+
+/*
+ * per-cpu monitor variables
+ */
+static DEFINE_PER_CPU(struct da_monitor, DA_MON_NAME);
+
+/*
+ * da_get_monitor - return current CPU monitor address
+ */
+static struct da_monitor *da_get_monitor(void)
+{
+	return this_cpu_ptr(&DA_MON_NAME);
+}
+
+/*
+ * __da_monitor_reset_all - reset all CPUs' monitor
+ */
+static void __da_monitor_reset_all(void (*reset)(struct da_monitor *))
+{
+	struct da_monitor *da_mon;
+	int cpu;
+
+	for_each_cpu(cpu, cpu_online_mask) {
+		da_mon = per_cpu_ptr(&DA_MON_NAME, cpu);
+		reset(da_mon);
+	}
+}
+
+/*
+ * da_monitor_reset_all - reset all CPUs' monitor
+ */
+static void da_monitor_reset_all(void)
+{
+	__da_monitor_reset_all(da_monitor_reset);
+}
+
+/*
+ * da_monitor_reset_state_all - reset all CPUs' monitor
+ */
+static inline void da_monitor_reset_state_all(void)
+{
+	__da_monitor_reset_all(da_monitor_reset_state);
+}
+
+/*
+ * da_monitor_init - initialize all CPUs' monitor
+ */
+static inline int da_monitor_init(void)
+{
+	da_monitor_reset_state_all();
+	return 0;
+}
+
+/*
+ * da_monitor_destroy - destroy the monitor
+ */
+static inline void da_monitor_destroy(void)
+{
+	da_monitor_reset_all();
+	da_monitor_sync_hook();
+}
+
+#ifndef da_implicit_guard
+#define da_implicit_guard() guard(migrate)()
+#endif
+
+#elif RV_MON_TYPE == RV_MON_PER_TASK
+/*
+ * Functions to define, init and get a per-task monitor.
+ */
+
+/*
+ * 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 = RV_PER_TASK_MONITOR_INIT;
+
+/*
+ * da_get_monitor - return the monitor in the allocated slot for tsk
+ */
+static inline struct da_monitor *da_get_monitor(struct task_struct *tsk)
+{
+	return &tsk->rv[task_mon_slot].da_mon;
+}
+
+static inline void da_reset(struct task_struct *tsk)
+{
+	da_monitor_reset(da_get_monitor(tsk));
+}
+
+/*
+ * da_get_target - return the task associated to the monitor
+ */
+static inline struct task_struct *da_get_target(struct da_monitor *da_mon)
+{
+	return container_of(da_mon, struct task_struct, rv[task_mon_slot].da_mon);
+}
+
+/*
+ * da_get_id - return the id associated to the monitor
+ *
+ * For per-task monitors, the id is the task's PID.
+ */
+static inline da_id_type da_get_id(struct da_monitor *da_mon)
+{
+	return da_get_target(da_mon)->pid;
+}
+
+static void __da_monitor_reset_all(void (*reset)(struct da_monitor *))
+{
+	struct task_struct *g, *p;
+	int cpu;
+
+	scoped_guard(read_lock, &tasklist_lock) {
+		for_each_process_thread(g, p)
+			reset(da_get_monitor(p));
+	}
+	for_each_present_cpu(cpu)
+		reset(da_get_monitor(idle_task(cpu)));
+}
+
+static void da_monitor_reset_all(void)
+{
+	__da_monitor_reset_all(da_monitor_reset);
+}
+
+static inline void da_monitor_reset_state_all(void)
+{
+	__da_monitor_reset_all(da_monitor_reset_state);
+}
+
+/*
+ * da_monitor_init - 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(void)
+{
+	int slot;
+
+	slot = rv_get_task_monitor_slot();
+	if (slot < 0 || slot >= RV_PER_TASK_MONITOR_INIT)
+		return slot;
+
+	task_mon_slot = slot;
+
+	da_monitor_reset_state_all();
+	return 0;
+}
+
+/*
+ * da_monitor_destroy - return the allocated slot
+ *
+ * Wait for all in-flight handlers before returning the slot to avoid
+ * out-of-bound accesses.
+ */
+static inline void da_monitor_destroy(void)
+{
+	if (task_mon_slot == RV_PER_TASK_MONITOR_INIT) {
+		WARN_ONCE(1, "Disabling a disabled monitor: " __stringify(MONITOR_NAME));
+		return;
+	}
+
+	tracepoint_synchronize_unregister();
+	da_monitor_reset_all();
+	da_monitor_sync_hook();
+
+	rv_put_task_monitor_slot(task_mon_slot);
+	task_mon_slot = RV_PER_TASK_MONITOR_INIT;
+}
+
+#elif RV_MON_TYPE == RV_MON_PER_OBJ
+/*
+ * Functions to define, init and get a per-object monitor.
+ */
+
+struct da_monitor_storage {
+	da_id_type id;
+	monitor_target target;
+	union rv_task_monitor rv;
+	struct hlist_node node;
+	struct rcu_head rcu;
+};
+
+#ifndef DA_MONITOR_HT_BITS
+#define DA_MONITOR_HT_BITS 10
+#endif
+static DEFINE_HASHTABLE(da_monitor_ht, DA_MONITOR_HT_BITS);
+
+/*
+ * da_create_empty_storage - pre-allocate an empty storage
+ */
+static inline struct da_monitor_storage *da_create_empty_storage(da_id_type id)
+{
+	struct da_monitor_storage *mon_storage;
+
+	mon_storage = kmalloc_nolock(sizeof(struct da_monitor_storage),
+				     __GFP_ZERO, NUMA_NO_NODE);
+	if (!mon_storage)
+		return NULL;
+
+	hash_add_rcu(da_monitor_ht, &mon_storage->node, id);
+	mon_storage->id = id;
+	return mon_storage;
+}
+
+/*
+ * da_create_storage - create the per-object storage
+ *
+ * The caller is responsible to synchronise writers, either with locks or
+ * implicitly. For instance, if da_create_storage is only called from a single
+ * event for target (e.g. sched_switch), it's safe to call this without locks.
+ */
+static inline struct da_monitor *da_create_storage(da_id_type id,
+						   monitor_target target,
+						   struct da_monitor *da_mon)
+{
+	struct da_monitor_storage *mon_storage;
+
+	if (da_mon)
+		return da_mon;
+
+	mon_storage = da_create_empty_storage(id);
+	if (!mon_storage)
+		return NULL;
+
+	mon_storage->target = target;
+	return &mon_storage->rv.da_mon;
+}
+
+/*
+ * __da_get_mon_storage - get the monitor storage from the hash table
+ */
+static inline struct da_monitor_storage *__da_get_mon_storage(da_id_type id)
+{
+	struct da_monitor_storage *mon_storage;
+
+	lockdep_assert_in_rcu_read_lock();
+	hash_for_each_possible_rcu(da_monitor_ht, mon_storage, node, id) {
+		if (mon_storage->id == id)
+			return mon_storage;
+	}
+
+	return NULL;
+}
+
+/*
+ * da_get_monitor - return the monitor for target
+ */
+static struct da_monitor *da_get_monitor(da_id_type id, monitor_target target)
+{
+	struct da_monitor_storage *mon_storage;
+
+	mon_storage = __da_get_mon_storage(id);
+	return mon_storage ? &mon_storage->rv.da_mon : NULL;
+}
+
+/*
+ * da_get_target - return the object associated to the monitor
+ */
+static inline monitor_target da_get_target(struct da_monitor *da_mon)
+{
+	return container_of(da_mon, struct da_monitor_storage, rv.da_mon)->target;
+}
+
+/*
+ * da_get_id - return the id associated to the monitor
+ */
+static inline da_id_type da_get_id(struct da_monitor *da_mon)
+{
+	return container_of(da_mon, struct da_monitor_storage, rv.da_mon)->id;
+}
+
+/*
+ * da_create_or_get - create the per-object storage if not already there
+ *
+ * This needs a lookup so should be guarded by RCU, the condition is checked
+ * directly in da_create_storage()
+ */
+static inline void da_create_or_get(da_id_type id, monitor_target target)
+{
+	guard(rcu)();
+	da_create_storage(id, target, da_get_monitor(id, target));
+}
+
+/*
+ * da_fill_empty_storage - store the target in a pre-allocated storage
+ *
+ * Can be used as a substitute of da_create_storage when starting a monitor in
+ * an environment where allocation is unsafe.
+ */
+static inline struct da_monitor *da_fill_empty_storage(da_id_type id,
+						       monitor_target target,
+						       struct da_monitor *da_mon)
+{
+	if (unlikely(da_mon && !da_get_target(da_mon)))
+		container_of(da_mon, struct da_monitor_storage, rv.da_mon)->target = target;
+	return da_mon;
+}
+
+/*
+ * da_get_target_by_id - return the object associated to the id
+ */
+static inline monitor_target da_get_target_by_id(da_id_type id)
+{
+	struct da_monitor_storage *mon_storage;
+
+	guard(rcu)();
+	mon_storage = __da_get_mon_storage(id);
+
+	if (unlikely(!mon_storage))
+		return NULL;
+	return mon_storage->target;
+}
+
+/*
+ * da_destroy_storage - destroy the per-object storage
+ *
+ * The caller is responsible to synchronise writers, either with locks or
+ * implicitly. For instance, if da_destroy_storage is called at sched_exit and
+ * da_create_storage can never occur after that, it's safe to call this without
+ * locks.
+ * This function includes an RCU read-side critical section to synchronise
+ * against da_monitor_destroy().
+ */
+static inline void da_destroy_storage(da_id_type id)
+{
+	struct da_monitor_storage *mon_storage;
+
+	guard(rcu)();
+	mon_storage = __da_get_mon_storage(id);
+
+	if (!mon_storage)
+		return;
+	da_monitor_reset_hook(&mon_storage->rv.da_mon);
+	hash_del_rcu(&mon_storage->node);
+	kfree_rcu(mon_storage, rcu);
+}
+
+static void __da_monitor_reset_all(void (*reset)(struct da_monitor *))
+{
+	struct da_monitor_storage *mon_storage;
+	int bkt;
+
+	guard(rcu)();
+	hash_for_each_rcu(da_monitor_ht, bkt, mon_storage, node)
+		reset(&mon_storage->rv.da_mon);
+}
+
+static void da_monitor_reset_all(void)
+{
+	__da_monitor_reset_all(da_monitor_reset);
+}
+
+static inline void da_monitor_reset_state_all(void)
+{
+	__da_monitor_reset_all(da_monitor_reset_state);
+}
+
+static inline int da_monitor_init(void)
+{
+	hash_init(da_monitor_ht);
+	return 0;
+}
+
+static inline void da_monitor_destroy(void)
+{
+	struct da_monitor_storage *mon_storage;
+	struct hlist_node *tmp;
+	int bkt;
+
+	tracepoint_synchronize_unregister();
+	da_monitor_reset_all();
+	da_monitor_sync_hook();
+	/*
+	 * This function is called after all probes are disabled and no longer
+	 * pending, we can safely assume no concurrent user.
+	 */
+	hash_for_each_safe(da_monitor_ht, bkt, tmp, mon_storage, node) {
+		hash_del_rcu(&mon_storage->node);
+		kfree(mon_storage);
+	}
+}
+
+/*
+ * Allow the per-object monitors to run allocation manually, necessary if the
+ * start condition is in a context problematic for allocation (e.g. scheduling).
+ * In such case, if the storage was pre-allocated without a target, set it now.
+ */
+#ifdef DA_SKIP_AUTO_ALLOC
+#define da_prepare_storage da_fill_empty_storage
+#else
+#define da_prepare_storage da_create_storage
+#endif /* DA_SKIP_AUTO_ALLOC */
+
+#endif /* RV_MON_TYPE */
+
+#if RV_MON_TYPE == RV_MON_GLOBAL || RV_MON_TYPE == RV_MON_PER_CPU
+/*
+ * Trace events 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.
+ */
+
+static inline void da_trace_event(struct da_monitor *da_mon,
+				  char *curr_state, char *event,
+				  char *next_state, bool is_final,
+				  da_id_type id)
+{
+	CONCATENATE(trace_event_, MONITOR_NAME)(curr_state, event, next_state,
+						is_final);
+}
+
+static inline void da_trace_error(struct da_monitor *da_mon,
+				  char *curr_state, char *event,
+				  da_id_type id)
+{
+	CONCATENATE(trace_error_, MONITOR_NAME)(curr_state, event);
+}
+
+/*
+ * da_get_id - unused for implicit monitors
+ */
+static inline da_id_type da_get_id(struct da_monitor *da_mon)
+{
+	return 0;
+}
+
+#elif RV_MON_TYPE == RV_MON_PER_TASK || RV_MON_TYPE == RV_MON_PER_OBJ
+/*
+ * Trace events for per_task/per_object monitors, report the target id.
+ */
+
+static inline void da_trace_event(struct da_monitor *da_mon,
+				  char *curr_state, char *event,
+				  char *next_state, bool is_final,
+				  da_id_type id)
+{
+	CONCATENATE(trace_event_, MONITOR_NAME)(id, curr_state, event,
+						next_state, is_final);
+}
+
+static inline void da_trace_error(struct da_monitor *da_mon,
+				  char *curr_state, char *event,
+				  da_id_type id)
+{
+	CONCATENATE(trace_error_, MONITOR_NAME)(id, curr_state, event);
+}
+#endif /* RV_MON_TYPE */
+
+/*
+ * da_event - handle an event for the da_mon
+ *
+ * This function is valid for both implicit and id 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.
+ */
+static inline bool da_event(struct da_monitor *da_mon, enum events event, da_id_type id)
+{
+	enum states 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(curr_state, event);
+		if (next_state == INVALID_STATE) {
+			react(curr_state, event);
+			da_trace_error(da_mon, model_get_state_name(curr_state),
+				       model_get_event_name(event), id);
+			return false;
+		}
+		if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) {
+			if (!da_monitor_event_hook(da_mon, curr_state, event, next_state, id))
+				return false;
+			da_trace_event(da_mon, model_get_state_name(curr_state),
+				       model_get_event_name(event),
+				       model_get_state_name(next_state),
+				       model_is_final_state(next_state), id);
+			return true;
+		}
+	}
+
+	trace_rv_retries_error(__stringify(MONITOR_NAME), model_get_event_name(event));
+	pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS)
+		" retries reached for event %s, resetting monitor %s",
+		model_get_event_name(event), __stringify(MONITOR_NAME));
+	return false;
+}
+
+static inline void __da_handle_event_common(struct da_monitor *da_mon,
+					    enum events event, da_id_type id)
+{
+	if (!da_event(da_mon, event, id))
+		da_monitor_reset(da_mon);
+}
+
+static inline void __da_handle_event(struct da_monitor *da_mon,
+				     enum events event, da_id_type id)
+{
+	if (da_monitor_handling_event(da_mon))
+		__da_handle_event_common(da_mon, event, id);
+}
+
+static inline bool __da_handle_start_event(struct da_monitor *da_mon,
+					   enum events event, da_id_type id)
+{
+	if (!da_monitor_enabled())
+		return 0;
+	if (unlikely(!da_monitoring(da_mon))) {
+		da_monitor_start(da_mon);
+		return 0;
+	}
+
+	__da_handle_event_common(da_mon, event, id);
+
+	return 1;
+}
+
+static inline bool __da_handle_start_run_event(struct da_monitor *da_mon,
+					       enum events event, da_id_type id)
+{
+	if (!da_monitor_enabled())
+		return 0;
+	if (unlikely(!da_monitoring(da_mon)))
+		da_monitor_start(da_mon);
+
+	__da_handle_event_common(da_mon, event, id);
+
+	return 1;
+}
+
+#if RV_MON_TYPE == RV_MON_GLOBAL || RV_MON_TYPE == RV_MON_PER_CPU
+/*
+ * Handle event for implicit monitor: da_get_monitor() will figure out
+ * the monitor.
+ */
+
+/*
+ * da_handle_event - handle an event
+ */
+static inline void da_handle_event(enum events event)
+{
+	da_implicit_guard();
+	__da_handle_event(da_get_monitor(), event, 0);
+}
+
+/*
+ * da_handle_start_event - 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(enum events event)
+{
+	da_implicit_guard();
+	return __da_handle_start_event(da_get_monitor(), event, 0);
+}
+
+/*
+ * da_handle_start_run_event - 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(enum events event)
+{
+	da_implicit_guard();
+	return __da_handle_start_run_event(da_get_monitor(), event, 0);
+}
+
+#elif RV_MON_TYPE == RV_MON_PER_TASK
+/*
+ * Handle event for per task.
+ */
+
+/*
+ * da_handle_event - handle an event
+ */
+static inline void da_handle_event(struct task_struct *tsk, enum events event)
+{
+	__da_handle_event(da_get_monitor(tsk), event, tsk->pid);
+}
+
+/*
+ * da_handle_start_event - 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(struct task_struct *tsk,
+					 enum events event)
+{
+	return __da_handle_start_event(da_get_monitor(tsk), event, tsk->pid);
+}
+
+/*
+ * da_handle_start_run_event - 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(struct task_struct *tsk,
+					     enum events event)
+{
+	return __da_handle_start_run_event(da_get_monitor(tsk), event, tsk->pid);
+}
+
+#elif RV_MON_TYPE == RV_MON_PER_OBJ
+/*
+ * Handle event for per object.
+ */
+
+/*
+ * da_handle_event - handle an event
+ */
+static inline void da_handle_event(da_id_type id, monitor_target target, enum events event)
+{
+	struct da_monitor *da_mon;
+
+	guard(rcu)();
+	da_mon = da_get_monitor(id, target);
+	if (likely(da_mon))
+		__da_handle_event(da_mon, event, id);
+}
+
+/*
+ * da_handle_start_event - 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(da_id_type id, monitor_target target,
+					 enum events event)
+{
+	struct da_monitor *da_mon;
+
+	guard(rcu)();
+	da_mon = da_get_monitor(id, target);
+	da_mon = da_prepare_storage(id, target, da_mon);
+	if (unlikely(!da_mon))
+		return 0;
+	return __da_handle_start_event(da_mon, event, id);
+}
+
+/*
+ * da_handle_start_run_event - 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(da_id_type id, monitor_target target,
+					     enum events event)
+{
+	struct da_monitor *da_mon;
+
+	guard(rcu)();
+	da_mon = da_get_monitor(id, target);
+	da_mon = da_prepare_storage(id, target, da_mon);
+	if (unlikely(!da_mon))
+		return 0;
+	return __da_handle_start_run_event(da_mon, event, id);
+}
+
+static inline void da_reset(da_id_type id, monitor_target target)
+{
+	struct da_monitor *da_mon;
+
+	guard(rcu)();
+	da_mon = da_get_monitor(id, target);
+	if (likely(da_mon))
+		da_monitor_reset(da_mon);
+}
+#endif /* RV_MON_TYPE */
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+#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 = da_monitor_init,        \
+	.monitor_destroy = da_monitor_destroy,  \
+}
+#endif /* RV_MON_TYPE */
+#endif /* CONFIG_RV_MONITORS_KUNIT_TEST */
+
+#endif
diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h
new file mode 100644
index 000000000..6e1c7fe54
--- /dev/null
+++ b/include/rv/ha_monitor.h
@@ -0,0 +1,550 @@
+/* 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_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 */
+
+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_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);
+}
+
+#if !defined(HA_SKIP_AUTO_CLEANUP) && RV_MON_TYPE == RV_MON_PER_TASK
+static 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
diff --git a/include/rv/instrumentation.h b/include/rv/instrumentation.h
new file mode 100644
index 000000000..d4e7a02ed
--- /dev/null
+++ b/include/rv/instrumentation.h
@@ -0,0 +1,29 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+ *
+ * Helper functions to facilitate the instrumentation of auto-generated
+ * RV monitors create by dot2k.
+ *
+ * The dot2k tool is available at tools/verification/dot2/
+ */
+
+#include <linux/ftrace.h>
+
+/*
+ * rv_attach_trace_probe - check and attach a handler function to a tracepoint
+ */
+#define rv_attach_trace_probe(monitor, tp, rv_handler)					\
+	do {										\
+		check_trace_callback_type_##tp(rv_handler);				\
+		WARN_ONCE(register_trace_##tp(rv_handler, NULL),			\
+				"fail attaching " #monitor " " #tp "handler");		\
+	} while (0)
+
+/*
+ * rv_detach_trace_probe - detach a handler function to a tracepoint
+ */
+#define rv_detach_trace_probe(monitor, tp, rv_handler)					\
+	do {										\
+		unregister_trace_##tp(rv_handler, NULL);				\
+	} while (0)
diff --git a/include/rv/kunit.h b/include/rv/kunit.h
new file mode 100644
index 000000000..31e0b93c4
--- /dev/null
+++ b/include/rv/kunit.h
@@ -0,0 +1,73 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Copyright (C) 2026-2029 Red Hat, Inc. Gabriele Monaco <gmonaco@redhat.com>
+ *
+ * Declaration of wrappers to allow mocking core functionality, like current,
+ * and other testing utilities.
+ * Necessary only when mocking may be needed. If the RV KUnit test is
+ * enabled, the wrappers incur an additional function call overhead.
+ */
+
+#ifndef _RV_KUNIT_H
+#define _RV_KUNIT_H
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+
+#include <kunit/test.h>
+#include <kunit/test-bug.h>
+#include <linux/delay.h>
+
+int rv_set_testing(struct kunit_suite *suite);
+void rv_clear_testing(struct kunit_suite *suite);
+
+#define RV_KUNIT_MAX_MOCK_TASKS 8
+
+struct rv_kunit_ctx {
+	int reactions, expected;
+	int mock_task_count;
+	struct task_struct *mock_tasks[RV_KUNIT_MAX_MOCK_TASKS];
+};
+
+#define RV_KUNIT_EXPECT_REACTION(test, ctx)                             \
+	do {                                                            \
+		KUNIT_EXPECT_EQ(test, ctx->reactions, ++ctx->expected); \
+		if (ctx->reactions != ctx->expected)                    \
+			ctx->expected = ctx->reactions;                 \
+	} while (0)
+
+#define RV_KUNIT_EXPECT_NO_REACTION(test, ctx)                        \
+	do {                                                          \
+		KUNIT_EXPECT_EQ(test, ctx->reactions, ctx->expected); \
+		if (ctx->reactions != ctx->expected)                  \
+			ctx->expected = ctx->reactions;               \
+	} while (0)
+
+#define RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)                             \
+	for (int __done = ({ RV_KUNIT_EXPECT_NO_REACTION(test, ctx); 0; });  \
+	     !__done;                                                        \
+	     __done = ({ RV_KUNIT_EXPECT_REACTION(test, ctx); 1; }))
+
+struct rv_kunit_mon {
+	struct rv_monitor *rv_this;
+	int (*monitor_init)(void);
+	void (*monitor_destroy)(void);
+	bool is_per_task;
+	int *task_slot;
+	void (*task_reset)(struct task_struct *task);
+};
+
+void prepare_test(struct kunit *test, const struct rv_kunit_mon *mon);
+void teardown_test(void *arg);
+struct task_struct *rv_kunit_alloc_mock_task(struct kunit *test);
+
+void rv_mock_current(struct task_struct *tsk);
+struct task_struct *rv_get_mock_current(void);
+
+#define rv_get_current() (unlikely(kunit_get_current_test()) ? rv_get_mock_current() : current)
+
+#else /* !CONFIG_RV_MONITORS_KUNIT_TEST */
+
+#define rv_get_current() current
+
+#endif /* CONFIG_RV_MONITORS_KUNIT_TEST */
+#endif /* _RV_KUNIT_H */
diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h
new file mode 100644
index 000000000..e9fd8265a
--- /dev/null
+++ b/include/rv/ltl_monitor.h
@@ -0,0 +1,182 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/**
+ * This file must be combined with the $(MODEL_NAME).h file generated by
+ * tools/verification/rvgen.
+ */
+
+#include <linux/args.h>
+#include <linux/rv.h>
+#include <linux/stringify.h>
+#include <linux/seq_buf.h>
+#include <rv/instrumentation.h>
+#include <rv/kunit.h>
+#include <trace/events/task.h>
+#include <trace/events/sched.h>
+
+#ifndef MONITOR_NAME
+#error "Please include $(MODEL_NAME).h generated by rvgen"
+#endif
+
+static struct rv_monitor rv_this;
+
+static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon);
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation);
+
+static struct ltl_monitor *ltl_get_monitor(struct task_struct *task)
+{
+	return &task->rv[ltl_monitor_slot].ltl_mon;
+}
+
+static void ltl_task_init(struct task_struct *task, bool task_creation)
+{
+	struct ltl_monitor *mon = ltl_get_monitor(task);
+
+	memset(&mon->states, 0, sizeof(mon->states));
+
+	for (int i = 0; i < LTL_NUM_ATOM; ++i)
+		__set_bit(i, mon->unknown_atoms);
+
+	ltl_atoms_init(task, mon, task_creation);
+	ltl_atoms_fetch(task, mon);
+}
+
+static void handle_task_newtask(void *data, struct task_struct *task, u64 flags)
+{
+	ltl_task_init(task, true);
+}
+
+static int ltl_monitor_init(void)
+{
+	struct task_struct *g, *p;
+	int ret, cpu;
+
+	ret = rv_get_task_monitor_slot();
+	if (ret < 0)
+		return ret;
+
+	ltl_monitor_slot = ret;
+
+	rv_attach_trace_probe(name, task_newtask, handle_task_newtask);
+
+	read_lock(&tasklist_lock);
+
+	for_each_process_thread(g, p)
+		ltl_task_init(p, false);
+
+	for_each_present_cpu(cpu)
+		ltl_task_init(idle_task(cpu), false);
+
+	read_unlock(&tasklist_lock);
+
+	return 0;
+}
+
+static void ltl_monitor_destroy(void)
+{
+	rv_detach_trace_probe(name, task_newtask, handle_task_newtask);
+
+	tracepoint_synchronize_unregister();
+	rv_put_task_monitor_slot(ltl_monitor_slot);
+	ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
+}
+
+static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor *mon)
+{
+	CONCATENATE(trace_error_, MONITOR_NAME)(task);
+	rv_react(&rv_this, "rv: "__stringify(MONITOR_NAME)": %s[%d]: violation detected\n",
+		 task->comm, task->pid);
+}
+
+static void ltl_attempt_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+	if (rv_ltl_all_atoms_known(mon))
+		ltl_start(task, mon);
+}
+
+static inline void ltl_atom_set(struct ltl_monitor *mon, enum ltl_atom atom, bool value)
+{
+	__clear_bit(atom, mon->unknown_atoms);
+	if (value)
+		__set_bit(atom, mon->atoms);
+	else
+		__clear_bit(atom, mon->atoms);
+}
+
+static void
+ltl_trace_event(struct task_struct *task, struct ltl_monitor *mon, unsigned long *next_state)
+{
+	const char *format_str = "%s";
+	DECLARE_SEQ_BUF(atoms, 64);
+	char states[32], next[32];
+	int i;
+
+	if (!CONCATENATE(CONCATENATE(trace_event_, MONITOR_NAME), _enabled)())
+		return;
+
+	snprintf(states, sizeof(states), "%*pbl", RV_MAX_BA_STATES, mon->states);
+	snprintf(next, sizeof(next), "%*pbl", RV_MAX_BA_STATES, next_state);
+
+	for (i = 0; i < LTL_NUM_ATOM; ++i) {
+		if (test_bit(i, mon->atoms)) {
+			seq_buf_printf(&atoms, format_str, ltl_atom_str(i));
+			format_str = ",%s";
+		}
+	}
+
+	CONCATENATE(trace_event_, MONITOR_NAME)(task, states, atoms.buffer, next);
+}
+
+static void ltl_validate(struct task_struct *task, struct ltl_monitor *mon)
+{
+	DECLARE_BITMAP(next_states, RV_MAX_BA_STATES) = {0};
+
+	if (!rv_ltl_valid_state(mon))
+		return;
+
+	for (unsigned int i = 0; i < RV_NUM_BA_STATES; ++i) {
+		if (test_bit(i, mon->states))
+			ltl_possible_next_states(mon, i, next_states);
+	}
+
+	ltl_trace_event(task, mon, next_states);
+
+	memcpy(mon->states, next_states, sizeof(next_states));
+
+	if (!rv_ltl_valid_state(mon))
+		ltl_illegal_state(task, mon);
+}
+
+static void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)
+{
+	struct ltl_monitor *mon = ltl_get_monitor(task);
+
+	ltl_atom_set(mon, atom, value);
+	ltl_atoms_fetch(task, mon);
+
+	if (!rv_ltl_valid_state(mon)) {
+		ltl_attempt_start(task, mon);
+		return;
+	}
+
+	ltl_validate(task, mon);
+}
+
+static void __maybe_unused ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)
+{
+	struct ltl_monitor *mon = ltl_get_monitor(task);
+
+	ltl_atom_update(task, atom, value);
+
+	ltl_atom_set(mon, atom, !value);
+	ltl_validate(task, mon);
+}
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+#define RV_MON_OPS_INIT() {               \
+	.rv_this = &rv_this,              \
+	.is_per_task = true,              \
+	.task_slot = &ltl_monitor_slot,   \
+}
+#endif /* CONFIG_RV_MONITORS_KUNIT_TEST */