@@ -150,3 +150,121 @@ is applied::
  +--------------+ <- dl_server_idle     sched_switch_suspend         ^
         |                                                            |
         +------ dl_throttle;is_constr_dl == 1 || is_defer == 1 ------+
+
+Monitor boost
+~~~~~~~~~~~~~
+
+The boost monitor ensures tasks associated to a server (e.g. fair tasks) run
+either independently or boosted in a timely manner.
+Unlike other models, the ``running`` state (and the ``switch_in/out`` events)
+indicates that any fair task is running, this needs to happen within a
+threshold that depends on server deadline and remaining runtime, whenever a
+task is ready.
+
+The following chart is simplified to avoid confusion, several less important
+self-loops on states have been removed and event names have been simplified:
+
+* ``idle`` (``dl_server_idle``) occurs when the CPU runs the idle task.
+* ``start/stop`` (``dl_server_start/stop``) start and stop the server.
+* ``switch`` (``sched_switch_in/out``) represented as a double arrow to
+  indicate both edges are present: ``ready -- switch_in -> running`` and
+  ``running -- switch_out -> ready``. As stated above this fires when any fair
+  task starts or stops to running.
+* ``resume/resume_throttle``: a fair task woke up, potentially when the server
+  is throttled (no runtime left), this event is especially frequent on self
+  loops (no state change during a wakeup) but is removed here for clarity.
+* arrows merge with an ``x`` sign to indicate they are the same event going to
+  the same state (but with different origins, e.g. ``{idle/throttled} -- stop
+  -> stopped``). The ``+`` sign indicates standard crossings or corners.
+
+Refer to the dot file for the full specification::
+
+                      |
+                      v
+                #===============#        stop;reset(clk)
+                H               H <---------------+
+  +------------>H    stopped    H                 |
+  |             H               H                 |
+  |             #===============#                 |
+  |                 ^          |                  |
+  |                 |          |                  |      replenish;reset(clk)
+  |               stop         |                  |                    +--+
+  |                 |     start;reset(clk)        +-----------------+  |  |
+  |                 |          v                                    |  |  v
+  |                +---------------+ <---------- switch --------> +---------+
+  |   +- resume -> |     ready     |                              |         |
+  |   |            |               | -replenish;reset(clk)        | running |
+  |   |  +- idle - | clk < thesh() |   |                          |         |
+  |   |  |         +---------------+ <-+        +---------------- +---------+
+  |   |  |         |  ^                         |                   ^    |
+  |   |  |         |  |                       throttle              |    |
+  |   |  |         |  |replenish;reset(clk)     |                   |    |
+  |   |  |  throttle  |                         |   replenish;reset(clk) |
+  |   |  |         |  |                         |                   |    |
+  |   |  |         v  |                         v                   |    |
+  |   |  |   +---------+    switch    +-------------------+         |    |
+  x---+--+-- |         | <----------> | throttled_running | --------+    |
+  |   |  |   |throttled|              +-------------------+              |
+  |   |  |   |         | -----+            |                             |
+  |   |  |   +---------+      |            |                             |
+  |   |  |      ^             |            |                             |
+  |   |  | resume_throttle    |            |                             |
+ stop |  |      |             |            |                             |
+  |   |  v      |             |            |                             |
+  |   +---------+ <-----------x--- idle ---x-----------------------------+
+  |   |         |
+  +-- |  idle   | <--+
+      |         |    | replenish;reset(clk)
+      +---------+ ---+
+
+Monitor laxity
+~~~~~~~~~~~~~~
+
+The laxity monitor ensure deferrable servers go to a zero-laxity wait unless
+already running and run in starvation cases. The model can stay in the
+zero-laxity wait only for up to a period, then the server either prepares to
+stop (after ``idle_wait``) or prepares to boost a task (``running``). Boosting
+(``sched_switch_in``) is only allowed in the ``running`` state.
+``dl_replenish_running`` should not be allowed in ``running``, but can happen
+as soon as the server started, the model allows this only within a short
+threshold::
+
+                                                  |
+ +---- dl_server_stop -----+                      |
+ |                         v                      v
+ |            #=======================================#
+ |   +------- H                stopped                H
+ |   |        #=======================================#
+ |   |          |                             ^
+ |   |  dl_server_start_running;        dl_server_stop
+ |   |        reset(clk)                      |
+ |   |          v                             |     dl_replenish_running;
+ |   |     +-------------------------------------+     clk < REPLENISH_NS
+ |   |     |                                     | -------------+
+ |   |     |              running                |              |
+ |   |     |                                     | <------------+
+ |   |     +-------------------------------------+
+ |   |       |                  ^              ^
+ |   |  dl_throttle    dl_replenish_running    |
+ |   |       v                  |              |
+ |   |   +-------------------+ -+              |
+ |   |   |  replenish_wait   |                 |   dl_replenish_idle;reset(clk)
+ |   |   | clk < period_ns() | ----------------+------------------------------+
+ |   |   +-------------------+                 |                              |
+ |   |                   |                     |                              |
+ |   |         dl_replenish;reset(clk)         | dl_replenish_running         |
+ |   |                   v                     |                              |
+ | dl_server_start;    +--------------------------+   dl_replenish;reset(clk) |
+ |   reset(clk)        |     zero_laxity_wait     | -------------+            |
+ |   |                 |     clk < period_ns()    |              |            |
+ |   +---------------> |                          | <------------+            |
+ |                     +--------------------------+                           |
+ |                               |              ^                             |
+ |  dl_replenish_idle;reset(clk) |      dl_replenish;reset(clk)               |
+ |                               v              |                             |
+ |                  +------------------------+  |                             |
+ +----------------- |        idle_wait       | -+                             |
+                    |   clk < period_ns()    |                                |
+                    +------------------------+ <------------------------------+
+                         ^     dl_replenish_idle;reset(clk)
+                         +-------------+

@@ -82,6 +82,8 @@ source "kernel/trace/rv/monitors/stall/Kconfig"
 source "kernel/trace/rv/monitors/deadline/Kconfig"
 source "kernel/trace/rv/monitors/nomiss/Kconfig"
 source "kernel/trace/rv/monitors/throttle/Kconfig"
+source "kernel/trace/rv/monitors/boost/Kconfig"
+source "kernel/trace/rv/monitors/laxity/Kconfig"
 # Add new deadline monitors here
 
 # Add new monitors here

@@ -21,6 +21,8 @@ obj-$(CONFIG_RV_MON_STALL) += monitors/stall/stall.o
 obj-$(CONFIG_RV_MON_DEADLINE) += monitors/deadline/deadline.o
 obj-$(CONFIG_RV_MON_NOMISS) += monitors/nomiss/nomiss.o
 obj-$(CONFIG_RV_MON_THROTTLE) += monitors/throttle/throttle.o
+obj-$(CONFIG_RV_MON_BOOST) += monitors/boost/boost.o
+obj-$(CONFIG_RV_MON_LAXITY) += monitors/laxity/laxity.o
 # Add new monitors here
 obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
 obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o

@@ -0,0 +1,15 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_BOOST
+	depends on RV
+	depends on RV_MON_DEADLINE
+	default y
+	select HA_MON_EVENTS_ID
+	bool "boost monitor"
+	help
+	  Monitor to ensure tasks associated to a server (e.g. fair tasks) run
+	  either independently or boosted in a timely manner.
+	  This monitor is part of the deadline monitors collection.
+
+	  For further information, see:
+	    Documentation/trace/rv/monitor_deadline.rst

@@ -0,0 +1,232 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "boost"
+
+#include <trace/events/sched.h>
+#include <rv_trace.h>
+
+#define RV_MON_TYPE RV_MON_PER_OBJ
+#define DA_SKIP_AUTO_ALLOC
+#define HA_TIMER_TYPE HA_TIMER_WHEEL
+typedef struct sched_dl_entity *monitor_target;
+#include "boost.h"
+#include <rv/ha_monitor.h>
+#include <monitors/deadline/deadline.h>
+
+static inline u64 server_threshold_ns(struct ha_monitor *ha_mon)
+{
+	struct sched_dl_entity *dl_se = ha_get_target(ha_mon);
+
+	return dl_se->dl_deadline + TICK_NSEC - dl_se->runtime;
+}
+
+static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_boost env, u64 time_ns)
+{
+	if (env == clk_boost)
+		return ha_get_clk_ns(ha_mon, env, time_ns);
+	return ENV_INVALID_VALUE;
+}
+
+static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_boost env, u64 time_ns)
+{
+	if (env == clk_boost)
+		ha_reset_clk_ns(ha_mon, env, time_ns);
+}
+
+static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
+					enum states curr_state, enum events event,
+					enum states next_state, u64 time_ns)
+{
+	if (curr_state == ready_boost)
+		return ha_check_invariant_ns(ha_mon, clk_boost, time_ns);
+	return true;
+}
+
+static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
+				    enum states curr_state, enum events event,
+				    enum states next_state, u64 time_ns)
+{
+	bool res = true;
+
+	if (curr_state == idle_boost && event == dl_replenish_boost)
+		ha_reset_env(ha_mon, clk_boost, time_ns);
+	else if (curr_state == ready_boost && event == dl_replenish_boost)
+		ha_reset_env(ha_mon, clk_boost, time_ns);
+	else if (curr_state == running_boost && event == dl_replenish_boost)
+		ha_reset_env(ha_mon, clk_boost, time_ns);
+	else if (curr_state == stopped_boost && event == dl_server_start_boost)
+		ha_reset_env(ha_mon, clk_boost, time_ns);
+	else if (curr_state == throttled_boost && event == dl_replenish_boost)
+		ha_reset_env(ha_mon, clk_boost, time_ns);
+	else if (curr_state == throttled_running_boost && event == dl_replenish_boost)
+		ha_reset_env(ha_mon, clk_boost, time_ns);
+	return res;
+}
+
+static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
+				       enum states curr_state, enum events event,
+				       enum states next_state, u64 time_ns)
+{
+	if (next_state == curr_state && event != dl_replenish_boost)
+		return;
+	if (next_state == ready_boost)
+		ha_start_timer_ns(ha_mon, clk_boost, server_threshold_ns(ha_mon), time_ns);
+	else if (curr_state == ready_boost)
+		ha_cancel_timer(ha_mon);
+}
+
+static bool ha_verify_constraint(struct ha_monitor *ha_mon,
+				 enum states curr_state, enum events event,
+				 enum states next_state, u64 time_ns)
+{
+	if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
+		return false;
+
+	if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
+		return false;
+
+	ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);
+
+	return true;
+}
+
+static void handle_dl_replenish(void *data, struct sched_dl_entity *dl_se, int cpu)
+{
+	da_handle_event(EXPAND_ID(dl_se, cpu), dl_replenish_boost);
+}
+
+static void handle_sched_switch(void *data, bool preempt,
+				struct task_struct *prev,
+				struct task_struct *next,
+				unsigned int prev_state)
+{
+	struct sched_dl_entity *dl_se = get_fair_server(next);
+	int cpu = task_cpu(next);
+
+	/*
+	 * The server is available in next only if the next task is boosted,
+	 * otherwise we need to retrieve it.
+	 * This monitor considers switch in/out whenever a task related to the
+	 * server (i.e. fair) is scheduled in or out, boosted or not.
+	 * Any switch to the same policy is ignored.
+	 * PI boosted tasks are not considered fair.
+	 */
+	if (!dl_se || (next->policy == prev->policy && !is_idle_task(next) &&
+		    !is_idle_task(prev)))
+		return;
+	if (is_idle_task(next))
+		da_handle_event(EXPAND_ID(dl_se, cpu), dl_server_idle_boost);
+	else if (next->policy == SCHED_NORMAL && !rt_or_dl_task(next))
+		da_handle_event(EXPAND_ID(dl_se, cpu), sched_switch_in_boost);
+	else if (prev->policy == SCHED_NORMAL && !is_idle_task(prev))
+		da_handle_event(EXPAND_ID(dl_se, cpu), sched_switch_out_boost);
+}
+
+static void handle_sched_enqueue(void *data, struct task_struct *tsk, int cpu)
+{
+	struct sched_dl_entity *dl_se = get_fair_server(tsk);
+
+	if (dl_se && tsk->policy == SCHED_NORMAL) {
+		da_handle_event(EXPAND_ID(dl_se, cpu),
+				dl_se->runtime > 0 ?
+					dl_server_resume_boost :
+					dl_server_resume_throttled_boost);
+	}
+}
+
+static void handle_sched_dequeue(void *data, struct task_struct *tsk, int cpu)
+{
+	struct sched_dl_entity *dl_se = get_fair_server(tsk);
+
+	/*
+	 * A dequeue is counted as switching out only in case of a change in
+	 * scheduler where the task is moved to another scheduler's runqueue.
+	 */
+	if (dl_se && tsk->policy == SCHED_NORMAL && task_is_running(tsk) && sched_task_on_rq(tsk))
+		da_handle_event(EXPAND_ID(dl_se, cpu), sched_switch_out_boost);
+}
+
+static void handle_dl_server_start(void *data, struct sched_dl_entity *dl_se, int cpu)
+{
+	da_handle_event(EXPAND_ID(dl_se, cpu), dl_server_start_boost);
+}
+
+static void handle_dl_server_stop(void *data, struct sched_dl_entity *dl_se, int cpu)
+{
+	da_handle_start_event(EXPAND_ID(dl_se, cpu), dl_server_stop_boost);
+}
+
+static void handle_dl_throttle(void *data, struct sched_dl_entity *dl_se, int cpu)
+{
+	da_handle_event(EXPAND_ID(dl_se, cpu), dl_throttle_boost);
+}
+
+static int enable_boost(void)
+{
+	int retval;
+
+	retval = da_monitor_init();
+	if (retval)
+		return retval;
+
+	retval = init_storage(true);
+	if (retval)
+		return retval;
+	rv_attach_trace_probe("boost", sched_dl_replenish_tp, handle_dl_replenish);
+	rv_attach_trace_probe("boost", sched_dl_server_start_tp, handle_dl_server_start);
+	rv_attach_trace_probe("boost", sched_dl_server_stop_tp, handle_dl_server_stop);
+	rv_attach_trace_probe("boost", sched_dl_throttle_tp, handle_dl_throttle);
+	rv_attach_trace_probe("boost", sched_enqueue_tp, handle_sched_enqueue);
+	rv_attach_trace_probe("boost", sched_dequeue_tp, handle_sched_dequeue);
+	rv_attach_trace_probe("boost", sched_switch, handle_sched_switch);
+
+	return 0;
+}
+
+static void disable_boost(void)
+{
+	rv_this.enabled = 0;
+
+	rv_detach_trace_probe("boost", sched_dl_replenish_tp, handle_dl_replenish);
+	rv_detach_trace_probe("boost", sched_dl_server_start_tp, handle_dl_server_start);
+	rv_detach_trace_probe("boost", sched_dl_server_stop_tp, handle_dl_server_stop);
+	rv_detach_trace_probe("boost", sched_dl_throttle_tp, handle_dl_throttle);
+	rv_detach_trace_probe("boost", sched_enqueue_tp, handle_sched_enqueue);
+	rv_detach_trace_probe("boost", sched_dequeue_tp, handle_sched_dequeue);
+	rv_detach_trace_probe("boost", sched_switch, handle_sched_switch);
+
+	da_monitor_destroy();
+}
+
+static struct rv_monitor rv_this = {
+	.name = "boost",
+	.description = "fair tasks run either independently or boosted.",
+	.enable = enable_boost,
+	.disable = disable_boost,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_boost(void)
+{
+	return rv_register_monitor(&rv_this, &rv_deadline);
+}
+
+static void __exit unregister_boost(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_boost);
+module_exit(unregister_boost);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
+MODULE_DESCRIPTION("boost: fair tasks run either independently or boosted.");

@@ -0,0 +1,146 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of boost automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME boost
+
+enum states_boost {
+	stopped_boost,
+	idle_boost,
+	ready_boost,
+	running_boost,
+	throttled_boost,
+	throttled_running_boost,
+	state_max_boost,
+};
+
+#define INVALID_STATE state_max_boost
+
+enum events_boost {
+	dl_replenish_boost,
+	dl_server_idle_boost,
+	dl_server_resume_boost,
+	dl_server_resume_throttled_boost,
+	dl_server_start_boost,
+	dl_server_stop_boost,
+	dl_throttle_boost,
+	sched_switch_in_boost,
+	sched_switch_out_boost,
+	event_max_boost,
+};
+
+enum envs_boost {
+	clk_boost,
+	env_max_boost,
+	env_max_stored_boost = env_max_boost,
+};
+
+_Static_assert(env_max_stored_boost <= MAX_HA_ENV_LEN, "Not enough slots");
+#define HA_CLK_NS
+
+struct automaton_boost {
+	char *state_names[state_max_boost];
+	char *event_names[event_max_boost];
+	char *env_names[env_max_boost];
+	unsigned char function[state_max_boost][event_max_boost];
+	unsigned char initial_state;
+	bool final_states[state_max_boost];
+};
+
+static const struct automaton_boost automaton_boost = {
+	.state_names = {
+		"stopped",
+		"idle",
+		"ready",
+		"running",
+		"throttled",
+		"throttled_running",
+	},
+	.event_names = {
+		"dl_replenish",
+		"dl_server_idle",
+		"dl_server_resume",
+		"dl_server_resume_throttled",
+		"dl_server_start",
+		"dl_server_stop",
+		"dl_throttle",
+		"sched_switch_in",
+		"sched_switch_out",
+	},
+	.env_names = {
+		"clk",
+	},
+	.function = {
+		{
+			INVALID_STATE,
+			stopped_boost,
+			stopped_boost,
+			stopped_boost,
+			ready_boost,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			stopped_boost,
+		},
+		{
+			idle_boost,
+			idle_boost,
+			ready_boost,
+			throttled_boost,
+			INVALID_STATE,
+			stopped_boost,
+			idle_boost,
+			INVALID_STATE,
+			INVALID_STATE,
+		},
+		{
+			ready_boost,
+			idle_boost,
+			ready_boost,
+			ready_boost,
+			INVALID_STATE,
+			stopped_boost,
+			throttled_boost,
+			running_boost,
+			ready_boost,
+		},
+		{
+			running_boost,
+			idle_boost,
+			running_boost,
+			running_boost,
+			INVALID_STATE,
+			stopped_boost,
+			throttled_running_boost,
+			INVALID_STATE,
+			ready_boost,
+		},
+		{
+			ready_boost,
+			idle_boost,
+			INVALID_STATE,
+			throttled_boost,
+			INVALID_STATE,
+			stopped_boost,
+			throttled_boost,
+			throttled_running_boost,
+			INVALID_STATE,
+		},
+		{
+			running_boost,
+			idle_boost,
+			INVALID_STATE,
+			throttled_running_boost,
+			INVALID_STATE,
+			INVALID_STATE,
+			throttled_running_boost,
+			INVALID_STATE,
+			throttled_boost,
+		},
+	},
+	.initial_state = stopped_boost,
+	.final_states = { 1, 0, 0, 0, 0, 0 },
+};

@@ -0,0 +1,19 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_BOOST
+DEFINE_EVENT(event_da_monitor_id, event_boost,
+	     TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state),
+	     TP_ARGS(id, state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor_id, error_boost,
+	     TP_PROTO(int id, char *state, char *event),
+	     TP_ARGS(id, state, event));
+
+DEFINE_EVENT(error_env_da_monitor_id, error_env_boost,
+	     TP_PROTO(int id, char *state, char *event, char *env),
+	     TP_ARGS(id, state, event, env));
+#endif /* CONFIG_RV_MON_BOOST */

@@ -0,0 +1,14 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_LAXITY
+	depends on RV
+	depends on RV_MON_DEADLINE
+	default y
+	select HA_MON_EVENTS_ID
+	bool "laxity monitor"
+	help
+	  Monitor to ensure deferrable servers go to a zero-laxity wait unless
+	  already running and run in starvation cases.
+
+	  For further information, see:
+	    Documentation/trace/rv/monitor_deadline.rst

@@ -0,0 +1,248 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "laxity"
+
+#include <trace/events/sched.h>
+#include <rv_trace.h>
+
+#define RV_MON_TYPE RV_MON_PER_OBJ
+#define HA_TIMER_TYPE HA_TIMER_WHEEL
+/* The start condition is on server_stop, allocation likely fails on PREEMPT_RT */
+#define DA_SKIP_AUTO_ALLOC
+typedef struct sched_dl_entity *monitor_target;
+#include "laxity.h"
+#include <rv/ha_monitor.h>
+#include <monitors/deadline/deadline.h>
+
+/* allow replenish when running only right after server start */
+#define REPLENISH_NS TICK_NSEC
+
+static inline u64 period_ns(struct ha_monitor *ha_mon)
+{
+	return ha_get_target(ha_mon)->dl_period + TICK_NSEC;
+}
+
+static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_laxity env, u64 time_ns)
+{
+	if (env == clk_laxity)
+		return ha_get_clk_ns(ha_mon, env, time_ns);
+	return ENV_INVALID_VALUE;
+}
+
+static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_laxity env, u64 time_ns)
+{
+	if (env == clk_laxity)
+		ha_reset_clk_ns(ha_mon, env, time_ns);
+}
+
+static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
+					enum states curr_state, enum events event,
+					enum states next_state, u64 time_ns)
+{
+	if (curr_state == idle_wait_laxity)
+		return ha_check_invariant_ns(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == replenish_wait_laxity)
+		return ha_check_invariant_ns(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == zero_laxity_wait_laxity)
+		return ha_check_invariant_ns(ha_mon, clk_laxity, time_ns);
+	return true;
+}
+
+static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
+					enum states curr_state, enum events event,
+					enum states next_state, u64 time_ns)
+{
+	if (curr_state == next_state)
+		return;
+	if (curr_state == zero_laxity_wait_laxity)
+		ha_inv_to_guard(ha_mon, clk_laxity, period_ns(ha_mon), time_ns);
+}
+
+static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
+				    enum states curr_state, enum events event,
+				    enum states next_state, u64 time_ns)
+{
+	bool res = true;
+
+	if (curr_state == idle_wait_laxity && event == dl_replenish_idle_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == idle_wait_laxity && event == dl_replenish_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == replenish_wait_laxity && event == dl_replenish_running_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == replenish_wait_laxity && event == dl_replenish_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == replenish_wait_laxity && event == dl_replenish_idle_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == running_laxity && event == dl_throttle_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == running_laxity && event == dl_replenish_running_laxity)
+		res = ha_monitor_env_invalid(ha_mon, clk_laxity) ||
+		      ha_get_env(ha_mon, clk_laxity, time_ns) < REPLENISH_NS;
+	else if (curr_state == stopped_laxity && event == dl_server_start_running_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == stopped_laxity && event == dl_server_start_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == zero_laxity_wait_laxity && event == dl_replenish_idle_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == zero_laxity_wait_laxity && event == dl_replenish_running_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == zero_laxity_wait_laxity && event == dl_replenish_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	return res;
+}
+
+static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
+				       enum states curr_state, enum events event,
+				       enum states next_state, u64 time_ns)
+{
+	if (next_state == curr_state && event != dl_replenish_laxity &&
+	    event != dl_replenish_idle_laxity)
+		return;
+	if (next_state == idle_wait_laxity)
+		ha_start_timer_ns(ha_mon, clk_laxity, period_ns(ha_mon), time_ns);
+	else if (next_state == replenish_wait_laxity)
+		ha_start_timer_ns(ha_mon, clk_laxity, period_ns(ha_mon), time_ns);
+	else if (next_state == zero_laxity_wait_laxity)
+		ha_start_timer_ns(ha_mon, clk_laxity, period_ns(ha_mon), time_ns);
+	else if (curr_state == idle_wait_laxity)
+		ha_cancel_timer(ha_mon);
+	else if (curr_state == replenish_wait_laxity)
+		ha_cancel_timer(ha_mon);
+	else if (curr_state == zero_laxity_wait_laxity)
+		ha_cancel_timer(ha_mon);
+}
+
+static bool ha_verify_constraint(struct ha_monitor *ha_mon,
+				 enum states curr_state, enum events event,
+				 enum states next_state, u64 time_ns)
+{
+	if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
+		return false;
+
+	ha_convert_inv_guard(ha_mon, curr_state, event, next_state, time_ns);
+
+	if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
+		return false;
+
+	ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);
+
+	return true;
+}
+
+static void handle_dl_replenish(void *data, struct sched_dl_entity *dl_se, int cpu)
+{
+	/* Special replenish happening after throttle, ignore it */
+	if (dl_se->dl_defer_running && dl_se->dl_throttled)
+		return;
+	if (dl_se->dl_defer_running)
+		da_handle_event(EXPAND_ID(dl_se, cpu), dl_replenish_running_laxity);
+	else if (idle_cpu(cpu))
+		da_handle_event(EXPAND_ID(dl_se, cpu), dl_replenish_idle_laxity);
+	else
+		da_handle_event(EXPAND_ID(dl_se, cpu), dl_replenish_laxity);
+}
+
+static void handle_dl_server_start(void *data, struct sched_dl_entity *dl_se, int cpu)
+{
+	if (dl_se->dl_defer_running)
+		da_handle_event(EXPAND_ID(dl_se, cpu), dl_server_start_running_laxity);
+	else
+		da_handle_event(EXPAND_ID(dl_se, cpu), dl_server_start_laxity);
+}
+
+static void handle_dl_server_stop(void *data, struct sched_dl_entity *dl_se, int cpu)
+{
+	da_handle_start_event(EXPAND_ID(dl_se, cpu), dl_server_stop_laxity);
+}
+
+static void handle_dl_throttle(void *data, struct sched_dl_entity *dl_se, int cpu)
+{
+	da_handle_event(EXPAND_ID(dl_se, cpu), dl_throttle_laxity);
+}
+
+static void handle_sched_switch(void *data, bool preempt,
+				struct task_struct *prev,
+				struct task_struct *next,
+				unsigned int prev_state)
+{
+	if (next->dl_server)
+		da_handle_event(EXPAND_ID(next->dl_server, task_cpu(next)),
+				sched_switch_in_laxity);
+}
+
+static void handle_sched_enqueue(void *data, struct task_struct *tsk, int cpu)
+{
+	struct sched_dl_entity *dl_se = get_fair_server(tsk);
+
+	if (dl_se && tsk->policy == SCHED_NORMAL)
+		da_handle_event(EXPAND_ID(dl_se, cpu), dl_server_resume_laxity);
+}
+
+static int enable_laxity(void)
+{
+	int retval;
+
+	retval = da_monitor_init();
+	if (retval)
+		return retval;
+
+	retval = init_storage(true);
+	if (retval)
+		return retval;
+	rv_attach_trace_probe("laxity", sched_dl_replenish_tp, handle_dl_replenish);
+	rv_attach_trace_probe("laxity", sched_dl_server_start_tp, handle_dl_server_start);
+	rv_attach_trace_probe("laxity", sched_dl_server_stop_tp, handle_dl_server_stop);
+	rv_attach_trace_probe("laxity", sched_dl_throttle_tp, handle_dl_throttle);
+	rv_attach_trace_probe("laxity", sched_switch, handle_sched_switch);
+	rv_attach_trace_probe("laxity", sched_enqueue_tp, handle_sched_enqueue);
+
+	return 0;
+}
+
+static void disable_laxity(void)
+{
+	rv_this.enabled = 0;
+
+	rv_detach_trace_probe("laxity", sched_dl_replenish_tp, handle_dl_replenish);
+	rv_detach_trace_probe("laxity", sched_dl_server_start_tp, handle_dl_server_start);
+	rv_detach_trace_probe("laxity", sched_dl_server_stop_tp, handle_dl_server_stop);
+	rv_detach_trace_probe("laxity", sched_dl_throttle_tp, handle_dl_throttle);
+	rv_detach_trace_probe("laxity", sched_switch, handle_sched_switch);
+	rv_detach_trace_probe("laxity", sched_enqueue_tp, handle_sched_enqueue);
+
+	da_monitor_destroy();
+}
+
+static struct rv_monitor rv_this = {
+	.name = "laxity",
+	.description = "deferrable servers wait for zero-laxity and run.",
+	.enable = enable_laxity,
+	.disable = disable_laxity,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_laxity(void)
+{
+	return rv_register_monitor(&rv_this, &rv_deadline);
+}
+
+static void __exit unregister_laxity(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_laxity);
+module_exit(unregister_laxity);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
+MODULE_DESCRIPTION("laxity: deferrable servers wait for zero-laxity and run.");

@@ -0,0 +1,133 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of laxity automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME laxity
+
+enum states_laxity {
+	stopped_laxity,
+	idle_wait_laxity,
+	replenish_wait_laxity,
+	running_laxity,
+	zero_laxity_wait_laxity,
+	state_max_laxity,
+};
+
+#define INVALID_STATE state_max_laxity
+
+enum events_laxity {
+	dl_replenish_laxity,
+	dl_replenish_idle_laxity,
+	dl_replenish_running_laxity,
+	dl_server_resume_laxity,
+	dl_server_start_laxity,
+	dl_server_start_running_laxity,
+	dl_server_stop_laxity,
+	dl_throttle_laxity,
+	sched_switch_in_laxity,
+	event_max_laxity,
+};
+
+enum envs_laxity {
+	clk_laxity,
+	env_max_laxity,
+	env_max_stored_laxity = env_max_laxity,
+};
+
+_Static_assert(env_max_stored_laxity <= MAX_HA_ENV_LEN, "Not enough slots");
+#define HA_CLK_NS
+
+struct automaton_laxity {
+	char *state_names[state_max_laxity];
+	char *event_names[event_max_laxity];
+	char *env_names[env_max_laxity];
+	unsigned char function[state_max_laxity][event_max_laxity];
+	unsigned char initial_state;
+	bool final_states[state_max_laxity];
+};
+
+static const struct automaton_laxity automaton_laxity = {
+	.state_names = {
+		"stopped",
+		"idle_wait",
+		"replenish_wait",
+		"running",
+		"zero_laxity_wait",
+	},
+	.event_names = {
+		"dl_replenish",
+		"dl_replenish_idle",
+		"dl_replenish_running",
+		"dl_server_resume",
+		"dl_server_start",
+		"dl_server_start_running",
+		"dl_server_stop",
+		"dl_throttle",
+		"sched_switch_in",
+	},
+	.env_names = {
+		"clk",
+	},
+	.function = {
+		{
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			stopped_laxity,
+			zero_laxity_wait_laxity,
+			running_laxity,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+		},
+		{
+			zero_laxity_wait_laxity,
+			idle_wait_laxity,
+			INVALID_STATE,
+			zero_laxity_wait_laxity,
+			INVALID_STATE,
+			INVALID_STATE,
+			stopped_laxity,
+			INVALID_STATE,
+			INVALID_STATE,
+		},
+		{
+			zero_laxity_wait_laxity,
+			idle_wait_laxity,
+			running_laxity,
+			replenish_wait_laxity,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+		},
+		{
+			INVALID_STATE,
+			INVALID_STATE,
+			running_laxity,
+			running_laxity,
+			INVALID_STATE,
+			INVALID_STATE,
+			stopped_laxity,
+			replenish_wait_laxity,
+			running_laxity,
+		},
+		{
+			zero_laxity_wait_laxity,
+			idle_wait_laxity,
+			running_laxity,
+			zero_laxity_wait_laxity,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+		},
+	},
+	.initial_state = stopped_laxity,
+	.final_states = { 1, 0, 0, 0, 0 },
+};

@@ -0,0 +1,19 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_LAXITY
+DEFINE_EVENT(event_da_monitor_id, event_laxity,
+	     TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state),
+	     TP_ARGS(id, state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor_id, error_laxity,
+	     TP_PROTO(int id, char *state, char *event),
+	     TP_ARGS(id, state, event));
+
+DEFINE_EVENT(error_env_da_monitor_id, error_env_laxity,
+	     TP_PROTO(int id, char *state, char *event, char *env),
+	     TP_ARGS(id, state, event, env));
+#endif /* CONFIG_RV_MON_LAXITY */

@@ -190,6 +190,8 @@ DECLARE_EVENT_CLASS(error_env_da_monitor_id,
 #include <monitors/stall/stall_trace.h>
 #include <monitors/nomiss/nomiss_trace.h>
 #include <monitors/throttle/throttle_trace.h>
+#include <monitors/boost/boost_trace.h>
+#include <monitors/laxity/laxity_trace.h>
 // Add new monitors based on CONFIG_HA_MON_EVENTS_ID here
 
 #endif

@@ -0,0 +1,48 @@
+digraph state_automaton {
+	center = true;
+	size = "7,11";
+	{node [shape = circle] "idle"};
+	{node [shape = circle] "ready"};
+	{node [shape = circle] "running"};
+	{node [shape = plaintext, style=invis, label=""] "__init_stopped"};
+	{node [shape = doublecircle] "stopped"};
+	{node [shape = circle] "stopped"};
+	{node [shape = circle] "throttled"};
+	{node [shape = circle] "throttled_running"};
+	"__init_stopped" -> "stopped";
+	"idle" [label = "idle"];
+	"idle" -> "idle" [ label = "dl_server_idle\ndl_replenish;reset(clk)\ndl_throttle" ];
+	"idle" -> "ready" [ label = "dl_server_resume" ];
+	"idle" -> "stopped" [ label = "dl_server_stop" ];
+	"idle" -> "throttled" [ label = "dl_server_resume_throttled" ];
+	"ready" [label = "ready\nclk < server_threshold_ns()"];
+	"ready" -> "idle" [ label = "dl_server_idle" ];
+	"ready" -> "ready" [ label = "sched_switch_out\ndl_server_resume_throttled\ndl_server_resume\ndl_replenish;reset(clk)" ];
+	"ready" -> "running" [ label = "sched_switch_in" ];
+	"ready" -> "stopped" [ label = "dl_server_stop" ];
+	"ready" -> "throttled" [ label = "dl_throttle" ];
+	"running" [label = "running"];
+	"running" -> "idle" [ label = "dl_server_idle" ];
+	"running" -> "ready" [ label = "sched_switch_out" ];
+	"running" -> "running" [ label = "dl_server_resume_throttled\ndl_server_resume\ndl_replenish;reset(clk)" ];
+	"running" -> "stopped" [ label = "dl_server_stop" ];
+	"running" -> "throttled_running" [ label = "dl_throttle" ];
+	"stopped" [label = "stopped", color = green3];
+	"stopped" -> "ready" [ label = "dl_server_start;reset(clk)" ];
+	"stopped" -> "stopped" [ label = "dl_server_idle\nsched_switch_out\ndl_server_resume\ndl_server_resume_throttled" ];
+	"throttled" [label = "throttled"];
+	"throttled" -> "idle" [ label = "dl_server_idle" ];
+	"throttled" -> "ready" [ label = "dl_replenish;reset(clk)" ];
+	"throttled" -> "stopped" [ label = "dl_server_stop" ];
+	"throttled" -> "throttled" [ label = "dl_throttle\ndl_server_resume_throttled" ];
+	"throttled" -> "throttled_running" [ label = "sched_switch_in" ];
+	"throttled_running" [label = "throttled_running"];
+	"throttled_running" -> "idle" [ label = "dl_server_idle" ];
+	"throttled_running" -> "running" [ label = "dl_replenish;reset(clk)" ];
+	"throttled_running" -> "throttled" [ label = "sched_switch_out" ];
+	"throttled_running" -> "throttled_running" [ label = "dl_throttle\ndl_server_resume_throttled" ];
+	{ rank = min ;
+		"__init_stopped";
+		"stopped";
+	}
+}