Linux Documentation
 help / color / mirror / Atom feed
* [PATCH 06/10] rv: Add enqueue/dequeue to snroc monitor
       [not found] <20260929124908.177676-1-gmonaco@redhat.com>
@ 2026-09-29 12:49 ` Gabriele Monaco
  2026-09-29 12:49 ` [PATCH 07/10] rv: Add throttle deadline monitor Gabriele Monaco
  2026-09-29 12:49 ` [PATCH 08/10] rv: Add dl_server specific monitors Gabriele Monaco
  2 siblings, 0 replies; 3+ messages in thread
From: Gabriele Monaco @ 2026-09-29 12:49 UTC (permalink / raw)
  To: linux-kernel, linux-trace-kernel, Steven Rostedt, Gabriele Monaco,
	Jonathan Corbet, Masami Hiramatsu, linux-doc
  Cc: Nam Cao, Wen Yang, Juri Lelli

The snroc monitor is a simple monitor that validates set_state occurs
only when a task is running. This implicitly validates switch in and out
follow one another.

Add enqueue/dequeue to validate they also follow one another without
duplicated events. Although they are not necessary to define the
task context, adding the check here saves from adding another simple
per-task monitor, which would require another slot in the task struct.

Reviewed-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
---
 Documentation/trace/rv/monitor_sched.rst  | 39 ++++++++++++-------
 kernel/trace/rv/monitors/snroc/snroc.c    | 18 ++++++++-
 kernel/trace/rv/monitors/snroc/snroc.h    | 46 ++++++++++++++++++++---
 tools/verification/models/sched/snroc.dot | 30 ++++++++++-----
 4 files changed, 101 insertions(+), 32 deletions(-)

diff --git a/Documentation/trace/rv/monitor_sched.rst b/Documentation/trace/rv/monitor_sched.rst
index d3ba7edc202f..6afddedfb202 100644
--- a/Documentation/trace/rv/monitor_sched.rst
+++ b/Documentation/trace/rv/monitor_sched.rst
@@ -66,21 +66,32 @@ Monitor snroc
 
 The set non runnable on its own context (snroc) monitor ensures changes in a
 task state happens only in the respective task's context. This is a per-task
-monitor::
+monitor.
+The monitor also includes enqueue/dequeue events to validate they alternate
+each other without duplication. Although they are not necessary to define the
+context, adding the check here saves from adding another simple per-task monitor::
+
+              |
+              |
+              v
+         #===============================================================#
+ +------ H                           enqueued                            H <--+
+ |       #===============================================================#    |
+ |         |                  ^                       sched_set_state         |
+ |  sched_switch_in   sched_switch_out                +--------------+        |
+ |         v                  |                       v              |        |
+ |      +-----------------------+   sched_dequeue    +-------------------+    |
+ |      |                       | -----------------> |                   |    |
+ |      |     own_context       |                    | dequeued_running  |    |
+ |      |                       | <----------------- |                   |    |
+ |      +-----------------------+   sched_enqueue    +-------------------+    |
+ |          ^   |           |                                                 |
+ |          +---+           | sched_switch_out                                |
+ |    sched_set_state       v                                                 |
+ |                      +-------------------------------------+               |
+ +--------------------> |              dequeued               | --------------+
+       sched_dequeue    +-------------------------------------+  sched_enqueue
 
-                        |
-                        |
-                        v
-                      +------------------+
-                      |  other_context   | <+
-                      +------------------+  |
-                        |                   |
-                        | sched_switch_in   | sched_switch_out
-                        v                   |
-    sched_set_state                         |
-  +------------------                       |
-  |                       own_context       |
-  +----------------->                      -+
 
 Monitor scpd
 ~~~~~~~~~~~~
diff --git a/kernel/trace/rv/monitors/snroc/snroc.c b/kernel/trace/rv/monitors/snroc/snroc.c
index f168b1a4b12c..87f87f479d18 100644
--- a/kernel/trace/rv/monitors/snroc/snroc.c
+++ b/kernel/trace/rv/monitors/snroc/snroc.c
@@ -17,6 +17,16 @@
 #include "snroc.h"
 #include <rv/da_monitor.h>
 
+static void handle_sched_dequeue(void *data, struct task_struct *tsk, int cpu)
+{
+	da_handle_event(tsk, sched_dequeue_snroc);
+}
+
+static void handle_sched_enqueue(void *data, struct task_struct *tsk, int cpu)
+{
+	da_handle_event(tsk, sched_enqueue_snroc);
+}
+
 static void handle_sched_set_state(void *data, struct task_struct *tsk, int state)
 {
 	da_handle_event(tsk, sched_set_state_snroc);
@@ -27,8 +37,8 @@ static void handle_sched_switch(void *data, bool preempt,
 				struct task_struct *next,
 				unsigned int prev_state)
 {
-	da_handle_start_event(prev, sched_switch_out_snroc);
-	da_handle_event(next, sched_switch_in_snroc);
+	da_handle_event(prev, sched_switch_out_snroc);
+	da_handle_start_run_event(next, sched_switch_in_snroc);
 }
 
 static int enable_snroc(void)
@@ -39,6 +49,8 @@ static int enable_snroc(void)
 	if (retval)
 		return retval;
 
+	rv_attach_trace_probe("snroc", sched_dequeue_tp, handle_sched_dequeue);
+	rv_attach_trace_probe("snroc", sched_enqueue_tp, handle_sched_enqueue);
 	rv_attach_trace_probe("snroc", sched_set_state_tp, handle_sched_set_state);
 	rv_attach_trace_probe("snroc", sched_switch, handle_sched_switch);
 
@@ -49,6 +61,8 @@ static void disable_snroc(void)
 {
 	rv_this.enabled = 0;
 
+	rv_detach_trace_probe("snroc", sched_dequeue_tp, handle_sched_dequeue);
+	rv_detach_trace_probe("snroc", sched_enqueue_tp, handle_sched_enqueue);
 	rv_detach_trace_probe("snroc", sched_set_state_tp, handle_sched_set_state);
 	rv_detach_trace_probe("snroc", sched_switch, handle_sched_switch);
 
diff --git a/kernel/trace/rv/monitors/snroc/snroc.h b/kernel/trace/rv/monitors/snroc/snroc.h
index 88b7328ad31a..b5b8c508cd11 100644
--- a/kernel/trace/rv/monitors/snroc/snroc.h
+++ b/kernel/trace/rv/monitors/snroc/snroc.h
@@ -8,7 +8,9 @@
 #define MONITOR_NAME snroc
 
 enum states_snroc {
-	other_context_snroc,
+	enqueued_snroc,
+	dequeued_snroc,
+	dequeued_running_snroc,
 	own_context_snroc,
 	state_max_snroc,
 };
@@ -16,6 +18,8 @@ enum states_snroc {
 #define INVALID_STATE state_max_snroc
 
 enum events_snroc {
+	sched_dequeue_snroc,
+	sched_enqueue_snroc,
 	sched_set_state_snroc,
 	sched_switch_in_snroc,
 	sched_switch_out_snroc,
@@ -32,18 +36,48 @@ struct automaton_snroc {
 
 static const struct automaton_snroc automaton_snroc = {
 	.state_names = {
-		"other_context",
+		"enqueued",
+		"dequeued",
+		"dequeued_running",
 		"own_context",
 	},
 	.event_names = {
+		"sched_dequeue",
+		"sched_enqueue",
 		"sched_set_state",
 		"sched_switch_in",
 		"sched_switch_out",
 	},
 	.function = {
-		{      INVALID_STATE,  own_context_snroc,       INVALID_STATE },
-		{  own_context_snroc,      INVALID_STATE, other_context_snroc },
+		{
+			dequeued_snroc,
+			INVALID_STATE,
+			INVALID_STATE,
+			own_context_snroc,
+			INVALID_STATE,
+		},
+		{
+			INVALID_STATE,
+			enqueued_snroc,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+		},
+		{
+			INVALID_STATE,
+			own_context_snroc,
+			dequeued_running_snroc,
+			INVALID_STATE,
+			dequeued_snroc,
+		},
+		{
+			dequeued_running_snroc,
+			INVALID_STATE,
+			own_context_snroc,
+			INVALID_STATE,
+			enqueued_snroc,
+		},
 	},
-	.initial_state = other_context_snroc,
-	.final_states = { 1, 0 },
+	.initial_state = enqueued_snroc,
+	.final_states = { 1, 0, 0, 0 },
 };
diff --git a/tools/verification/models/sched/snroc.dot b/tools/verification/models/sched/snroc.dot
index 8b71c32d4dca..b32e9adfb383 100644
--- a/tools/verification/models/sched/snroc.dot
+++ b/tools/verification/models/sched/snroc.dot
@@ -1,18 +1,28 @@
 digraph state_automaton {
 	center = true;
 	size = "7,11";
-	{node [shape = plaintext, style=invis, label=""] "__init_other_context"};
-	{node [shape = ellipse] "other_context"};
-	{node [shape = plaintext] "other_context"};
-	{node [shape = plaintext] "own_context"};
-	"__init_other_context" -> "other_context";
-	"other_context" [label = "other_context", color = green3];
-	"other_context" -> "own_context" [ label = "sched_switch_in" ];
+	{node [shape = circle] "dequeued"};
+	{node [shape = circle] "dequeued_running"};
+	{node [shape = plaintext, style=invis, label=""] "__init_enqueued"};
+	{node [shape = doublecircle] "enqueued"};
+	{node [shape = circle] "enqueued"};
+	{node [shape = circle] "own_context"};
+	"__init_enqueued" -> "enqueued";
+	"dequeued" [label = "dequeued"];
+	"dequeued" -> "enqueued" [ label = "sched_enqueue" ];
+	"dequeued_running" [label = "dequeued_running"];
+	"dequeued_running" -> "dequeued" [ label = "sched_switch_out" ];
+	"dequeued_running" -> "dequeued_running" [ label = "sched_set_state" ];
+	"dequeued_running" -> "own_context" [ label = "sched_enqueue" ];
+	"enqueued" [label = "enqueued", color = green3];
+	"enqueued" -> "dequeued" [ label = "sched_dequeue" ];
+	"enqueued" -> "own_context" [ label = "sched_switch_in" ];
 	"own_context" [label = "own_context"];
-	"own_context" -> "other_context" [ label = "sched_switch_out" ];
+	"own_context" -> "dequeued_running" [ label = "sched_dequeue" ];
+	"own_context" -> "enqueued" [ label = "sched_switch_out" ];
 	"own_context" -> "own_context" [ label = "sched_set_state" ];
 	{ rank = min ;
-		"__init_other_context";
-		"other_context";
+		"__init_enqueued";
+		"enqueued";
 	}
 }
-- 
2.55.0


^ permalink raw reply related	[flat|nested] 3+ messages in thread

* [PATCH 07/10] rv: Add throttle deadline monitor
       [not found] <20260929124908.177676-1-gmonaco@redhat.com>
  2026-09-29 12:49 ` [PATCH 06/10] rv: Add enqueue/dequeue to snroc monitor Gabriele Monaco
@ 2026-09-29 12:49 ` Gabriele Monaco
  2026-09-29 12:49 ` [PATCH 08/10] rv: Add dl_server specific monitors Gabriele Monaco
  2 siblings, 0 replies; 3+ messages in thread
From: Gabriele Monaco @ 2026-09-29 12:49 UTC (permalink / raw)
  To: linux-kernel, linux-trace-kernel, Steven Rostedt, Gabriele Monaco,
	Jonathan Corbet, Masami Hiramatsu, linux-doc
  Cc: Nam Cao, Wen Yang, Juri Lelli

Add a monitor to validate the behaviour of the deadline scheduler.

* throttle:
    validate dl entities are throttled when they use up their runtime

Reviewed-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
---
 Documentation/trace/rv/monitor_deadline.rst   |  74 +++++
 kernel/trace/rv/Kconfig                       |   1 +
 kernel/trace/rv/Makefile                      |   1 +
 kernel/trace/rv/monitors/throttle/Kconfig     |  15 +
 kernel/trace/rv/monitors/throttle/throttle.c  | 285 ++++++++++++++++++
 kernel/trace/rv/monitors/throttle/throttle.h  | 116 +++++++
 .../rv/monitors/throttle/throttle_trace.h     |  19 ++
 kernel/trace/rv/rv_trace.h                    |   1 +
 .../verification/models/deadline/throttle.dot |  44 +++
 9 files changed, 556 insertions(+)
 create mode 100644 kernel/trace/rv/monitors/throttle/Kconfig
 create mode 100644 kernel/trace/rv/monitors/throttle/throttle.c
 create mode 100644 kernel/trace/rv/monitors/throttle/throttle.h
 create mode 100644 kernel/trace/rv/monitors/throttle/throttle_trace.h
 create mode 100644 tools/verification/models/deadline/throttle.dot

diff --git a/Documentation/trace/rv/monitor_deadline.rst b/Documentation/trace/rv/monitor_deadline.rst
index 84506ed1e293..e88f631d8387 100644
--- a/Documentation/trace/rv/monitor_deadline.rst
+++ b/Documentation/trace/rv/monitor_deadline.rst
@@ -82,3 +82,77 @@ server can run from sleeping without being ready::
  +--------------+ <---------+                                        ^
         |                                                            |
         +------ dl_throttle;is_constr_dl == 1 || is_defer == 1 ------+
+
+Monitor throttle
+~~~~~~~~~~~~~~~~
+
+The throttle monitor ensures deadline entities are throttled when they use up
+their runtime. Deadline tasks can be only ``running``, ``preempted`` and
+``throttled``, the runtime is enforced only in ``running`` based on an internal
+clock and the runtime value in the deadline entity.
+On systems with CPU frequency scaling or turbo boost, deadline tasks can run
+longer than their runtime as this is scaled according to the frequency. In this
+scenario, the monitor allows to skip the runtime check with the module
+parameter ``throttle.skip_runtime_check``.
+
+Servers can be also in the ``armed`` state, which represents when the
+server is consuming bandwidth in background (e.g. idle or normal tasks are
+running without any boost). From this state the server can be throttled but it
+can also use more runtime than available. A server is considered ``running``
+when it's actively boosting a task, only there the runtime is enforced. The
+server is preempted if the running task is not in the server's runqueue (e.g. a
+FIFO task for the fair server).
+Events like ``dl_armed`` and ``sched_switch_in`` can occur sequentially for
+servers since they are related to the current task (e.g. a 2 fair tasks can be
+switched in sequentially, that corresponds to multiple ``dl_armed``).
+
+Any task or server in the ``throttled`` state must leave it shortly, e.g.
+become ``preempted``::
+
+                                     |
+                                     |
+      dl_replenish;reset(clk)        v
+              sched_switch_in   #=========================# sched_switch_in;
+               +--------------- H                         H   reset(clk)
+               |                H                         H <----------------+
+               +--------------> H         running         H                  |
+    dl_throttle;reset(clk)      H clk < runtime_left_ns() H                  |
+   +--------------------------- H                         H sched_switch_out |
+   |       +------------------> H                         H -------------+   |
+   | dl_replenish;reset(clk)    #=========================#              |   |
+   |       |                         |             ^                     |   |
+   v       |                  dl_defer_arm         |                     |   |
+ +-------------------------+         |             |                     |   |
+ |       throttled         |         |    sched_switch_in;reset(clk)     |   |
+ | clk < THROTTLED_TIME_NS |         v             |                     |   |
+ +-------------------------+        +----------------+                   |   |
+   |    |                           |                | sched_switch_out  |   |
+   |    |               +---------- |                | -------------+    |   |
+   |    |          dl_replenish     |     armed      |              |    |   |
+   |    |          dl_defer_arm     |                | <--------+   |    |   |
+   |    |               +---------> |                | dl_defer_arm |    |   |
+   |    |                           +----------------+          |   |    |   |
+   |    |                            |         ^                |   |    |   |
+   |    |                        dl_throttle  dl_replenish      |   |    |   |
+   |    |                            v         |                |   |    |   |
+   |    |     dl_defer_arm  +-------------------+               |   v    v   |
+   |    |       +---------- |                   |             +--------------+
+   |    |       |           |                   |             |              |
+   |    |       +---------> |  armed_throttled  |             |  preempted   |
+   |    |                   |                   |             |              |
+   |    +-----------------> |                   |             +--------------+
+   |          dl_defer_arm  +-------------------+   sched_switch_out ^   |  ^
+   |                            |              ^        dl_replenish |   |  |
+   |                  sched_switch_out    dl_defer_arm          +----+   |  |
+   |                            v              |                         |  |
+   |       sched_switch_out  +-----------------------+                   |  |
+   |         +-------------- |                       | dl_throttle;      |  |
+   |         |               |                       |  is_constr_dl==1  |  |
+   |         +-------------> |  preempted_throttled  | <-----------------+  |
+   |                         |                       |                      |
+   +-----------------------> |                       | -- dl_replenish -----+
+         sched_switch_out    +-----------------------+
+
+The value of ``runtime_left_ns()`` is directly read from the deadline entity
+and updated as the task runs. It is increased by 1 tick to account for the
+maximum delay to throttle (not valid if ``sched_feat(HRTICK_DL)`` is active).
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index efa930f94ea4..cdb851c7cceb 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -82,6 +82,7 @@ source "kernel/trace/rv/monitors/wakeup/Kconfig"
 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"
 # Add new deadline monitors here
 
 # Add new monitors here
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index cdbf68c84f5a..1387082dc490 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -21,6 +21,7 @@ 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_WAKEUP) += monitors/wakeup/wakeup.o
+obj-$(CONFIG_RV_MON_THROTTLE) += monitors/throttle/throttle.o
 # Add new monitors here
 obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
 obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
diff --git a/kernel/trace/rv/monitors/throttle/Kconfig b/kernel/trace/rv/monitors/throttle/Kconfig
new file mode 100644
index 000000000000..d9bd2dc903cd
--- /dev/null
+++ b/kernel/trace/rv/monitors/throttle/Kconfig
@@ -0,0 +1,15 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_THROTTLE
+	depends on RV
+	depends on HAVE_SYSCALL_TRACEPOINTS
+	depends on RV_MON_DEADLINE
+	default y
+	select HA_MON_EVENTS_ID
+	bool "throttle monitor"
+	help
+	  Monitor to ensure dl entities are throttled when they use up their runtime.
+	  This monitor is part of the deadline monitors collection.
+
+	  For further information, see:
+	    Documentation/trace/rv/monitor_deadline.rst
diff --git a/kernel/trace/rv/monitors/throttle/throttle.c b/kernel/trace/rv/monitors/throttle/throttle.c
new file mode 100644
index 000000000000..b22a2abe59fe
--- /dev/null
+++ b/kernel/trace/rv/monitors/throttle/throttle.c
@@ -0,0 +1,285 @@
+// 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 "throttle"
+
+#include <uapi/linux/sched/types.h>
+#include <trace/events/syscalls.h>
+#include <trace/events/sched.h>
+#include <trace/events/task.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 sched_switch, it's dangerous to allocate there */
+#define DA_SKIP_AUTO_ALLOC
+typedef struct sched_dl_entity *monitor_target;
+#include "throttle.h"
+#include <rv/ha_monitor.h>
+#include <monitors/deadline/deadline.h>
+
+#define THROTTLED_TIME_NS TICK_NSEC
+/* with sched_feat(HRTICK_DL) the threshold can be lower */
+#define RUNTIME_THRESH TICK_NSEC
+/*
+ * On systems with CPU frequency scaling or turbo boost, deadline tasks can run
+ * longer than their runtime as this is scaled according to the frequency. As a
+ * result, this constraint cannot work.
+ */
+static bool skip_runtime_check;
+module_param(skip_runtime_check, bool, 0644);
+
+static inline u64 runtime_left_ns(struct ha_monitor *ha_mon)
+{
+	return ha_get_target(ha_mon)->runtime + RUNTIME_THRESH;
+}
+
+static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_throttle env, u64 time_ns)
+{
+	if (env == clk_throttle)
+		return ha_get_clk_ns(ha_mon, env, time_ns);
+	else if (env == is_constr_dl_throttle)
+		return !dl_is_implicit(ha_get_target(ha_mon));
+	return ENV_INVALID_VALUE;
+}
+
+static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_throttle env, u64 time_ns)
+{
+	if (env == clk_throttle)
+		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 == running_throttle && !skip_runtime_check)
+		return ha_check_invariant_ns(ha_mon, clk_throttle, time_ns);
+	else if (curr_state == throttled_throttle)
+		return ha_check_invariant_ns(ha_mon, clk_throttle, 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 == armed_throttle && event == sched_switch_in_throttle)
+		ha_reset_env(ha_mon, clk_throttle, time_ns);
+	else if (curr_state == preempted_throttle && event == dl_throttle_throttle)
+		res = ha_get_env(ha_mon, is_constr_dl_throttle, time_ns) == 1ull;
+	else if (curr_state == preempted_throttle && event == sched_switch_in_throttle)
+		ha_reset_env(ha_mon, clk_throttle, time_ns);
+	else if (curr_state == running_throttle && event == dl_replenish_throttle)
+		ha_reset_env(ha_mon, clk_throttle, time_ns);
+	else if (curr_state == running_throttle && event == dl_throttle_throttle)
+		ha_reset_env(ha_mon, clk_throttle, time_ns);
+	else if (curr_state == throttled_throttle && event == dl_replenish_throttle)
+		ha_reset_env(ha_mon, clk_throttle, 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_throttle)
+		return;
+	if (next_state == running_throttle && !skip_runtime_check)
+		ha_start_timer_ns(ha_mon, clk_throttle, runtime_left_ns(ha_mon), time_ns);
+	else if (next_state == throttled_throttle)
+		ha_start_timer_ns(ha_mon, clk_throttle, THROTTLED_TIME_NS, time_ns);
+	else if (curr_state == running_throttle)
+		ha_cancel_timer(ha_mon);
+	else if (curr_state == throttled_throttle)
+		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, u8 type)
+{
+	if (is_supported_type(type))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_replenish_throttle);
+}
+
+static void handle_dl_throttle(void *data, struct sched_dl_entity *dl_se,
+			       int cpu, u8 type)
+{
+	if (is_supported_type(type))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_throttle_throttle);
+}
+
+static void handle_dl_server_stop(void *data, struct sched_dl_entity *dl_se,
+				  int cpu, u8 type)
+{
+	if (is_supported_type(type))
+		da_handle_start_run_event(EXPAND_ID(dl_se, cpu, type), sched_switch_out_throttle);
+}
+
+static inline void handle_server_switch(struct task_struct *next, int cpu, u8 type)
+{
+	struct sched_dl_entity *dl_se = get_server(next, type);
+
+	if (!dl_se)
+		return;
+	if (get_server_type(next) == type || is_idle_task(next))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_defer_arm_throttle);
+	else
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), sched_switch_out_throttle);
+}
+
+static void handle_sched_switch(void *data, bool preempt,
+				struct task_struct *prev,
+				struct task_struct *next,
+				unsigned int prev_state)
+{
+	int cpu = task_cpu(next);
+
+	if (prev->policy == SCHED_DEADLINE)
+		da_handle_event(EXPAND_ID_TASK(prev), sched_switch_out_throttle);
+	if (next->policy == SCHED_DEADLINE)
+		da_handle_start_event(EXPAND_ID_TASK(next), sched_switch_in_throttle);
+
+	/*
+	 * The server is available in next only if the next task is boosted,
+	 * otherwise we need to retrieve it.
+	 * Here the server continues in the state running/armed until actually
+	 * stopped, this works since we continue expecting a throttle.
+	 */
+	if (next->dl_server) {
+		da_handle_start_event(EXPAND_ID(next->dl_server, cpu,
+						get_server_type(next)),
+				      sched_switch_in_throttle);
+	} else {
+		handle_server_switch(next, cpu, DL_SERVER_FAIR);
+		if (IS_ENABLED(CONFIG_SCHED_CLASS_EXT))
+			handle_server_switch(next, cpu, DL_SERVER_EXT);
+	}
+}
+
+static void handle_sched_enqueue(void *data, struct task_struct *tsk, int cpu)
+{
+	struct sched_dl_entity *dl_se = NULL;
+	u8 type = get_server_type(tsk);
+
+	if (is_server_type(type))
+		dl_se = get_server(tsk, type);
+	/*
+	 * An enqueue is counted as server arming only in case of a change in
+	 * scheduler where the task is moved to another scheduler's runqueue.
+	 */
+	if (dl_se && task_is_running(tsk) && sched_task_on_rq(tsk))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_defer_arm_throttle);
+}
+
+static void handle_sys_enter(void *data, struct pt_regs *regs, long id)
+{
+	struct task_struct *p;
+	int new_policy = -1;
+	pid_t pid = 0;
+
+	new_policy = extract_params(regs, id, &pid);
+	if (new_policy < 0)
+		return;
+	guard(rcu)();
+	p = pid ? find_task_by_vpid(pid) : current;
+	if (unlikely(!p) || new_policy == p->policy)
+		return;
+
+	if (p->policy == SCHED_DEADLINE)
+		da_reset(EXPAND_ID_TASK(p));
+	else if (new_policy == SCHED_DEADLINE)
+		da_create_or_get(EXPAND_ID_TASK(p));
+}
+
+static int enable_throttle(void)
+{
+	int retval;
+
+	retval = ha_monitor_init();
+	if (retval)
+		return retval;
+
+	retval = init_storage(false);
+	if (retval)
+		return retval;
+	rv_attach_trace_probe("throttle", sched_dl_replenish_tp, handle_dl_replenish);
+	rv_attach_trace_probe("throttle", sched_dl_throttle_tp, handle_dl_throttle);
+	rv_attach_trace_probe("throttle", sched_enqueue_tp, handle_sched_enqueue);
+	rv_attach_trace_probe("throttle", sched_switch, handle_sched_switch);
+	if (!should_skip_syscall_handle())
+		rv_attach_trace_probe("throttle", sys_enter, handle_sys_enter);
+	rv_attach_trace_probe("throttle", task_newtask, handle_newtask);
+	rv_attach_trace_probe("throttle", sched_dl_server_stop_tp, handle_dl_server_stop);
+	rv_attach_trace_probe("throttle", sched_process_exit, handle_exit);
+
+	return 0;
+}
+
+static void disable_throttle(void)
+{
+	rv_this.enabled = 0;
+
+	/* Those are RCU writers, detach earlier hoping to close a bit faster */
+	rv_detach_trace_probe("throttle", task_newtask, handle_newtask);
+	rv_detach_trace_probe("throttle", sched_process_exit, handle_exit);
+	if (!should_skip_syscall_handle())
+		rv_detach_trace_probe("throttle", sys_enter, handle_sys_enter);
+
+	rv_detach_trace_probe("throttle", sched_dl_replenish_tp, handle_dl_replenish);
+	rv_detach_trace_probe("throttle", sched_dl_throttle_tp, handle_dl_throttle);
+	rv_detach_trace_probe("throttle", sched_dl_server_stop_tp, handle_dl_server_stop);
+	rv_detach_trace_probe("throttle", sched_enqueue_tp, handle_sched_enqueue);
+	rv_detach_trace_probe("throttle", sched_switch, handle_sched_switch);
+
+	ha_monitor_destroy();
+}
+
+static struct rv_monitor rv_this = {
+	.name = "throttle",
+	.description = "throttle dl entities when they use up their runtime.",
+	.enable = enable_throttle,
+	.disable = disable_throttle,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_throttle(void)
+{
+	return rv_register_monitor(&rv_this, &rv_deadline);
+}
+
+static void __exit unregister_throttle(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_throttle);
+module_exit(unregister_throttle);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
+MODULE_DESCRIPTION("throttle: throttle dl entities when they use up their runtime.");
diff --git a/kernel/trace/rv/monitors/throttle/throttle.h b/kernel/trace/rv/monitors/throttle/throttle.h
new file mode 100644
index 000000000000..3ab6d73280d2
--- /dev/null
+++ b/kernel/trace/rv/monitors/throttle/throttle.h
@@ -0,0 +1,116 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of throttle automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME throttle
+
+enum states_throttle {
+	running_throttle,
+	armed_throttle,
+	armed_throttled_throttle,
+	preempted_throttle,
+	preempted_throttled_throttle,
+	throttled_throttle,
+	state_max_throttle,
+};
+
+#define INVALID_STATE state_max_throttle
+
+enum events_throttle {
+	dl_defer_arm_throttle,
+	dl_replenish_throttle,
+	dl_throttle_throttle,
+	sched_switch_in_throttle,
+	sched_switch_out_throttle,
+	event_max_throttle,
+};
+
+enum envs_throttle {
+	clk_throttle,
+	is_constr_dl_throttle,
+	env_max_throttle,
+	env_max_stored_throttle = is_constr_dl_throttle,
+};
+
+_Static_assert(env_max_stored_throttle <= MAX_HA_ENV_LEN, "Not enough slots");
+#define HA_CLK_NS
+
+struct automaton_throttle {
+	char *state_names[state_max_throttle];
+	char *event_names[event_max_throttle];
+	char *env_names[env_max_throttle];
+	unsigned char function[state_max_throttle][event_max_throttle];
+	unsigned char initial_state;
+	bool final_states[state_max_throttle];
+};
+
+static const struct automaton_throttle automaton_throttle = {
+	.state_names = {
+		"running",
+		"armed",
+		"armed_throttled",
+		"preempted",
+		"preempted_throttled",
+		"throttled",
+	},
+	.event_names = {
+		"dl_defer_arm",
+		"dl_replenish",
+		"dl_throttle",
+		"sched_switch_in",
+		"sched_switch_out",
+	},
+	.env_names = {
+		"clk",
+		"is_constr_dl",
+	},
+	.function = {
+		{
+			armed_throttle,
+			running_throttle,
+			throttled_throttle,
+			running_throttle,
+			preempted_throttle,
+		},
+		{
+			armed_throttle,
+			armed_throttle,
+			armed_throttled_throttle,
+			running_throttle,
+			preempted_throttle,
+		},
+		{
+			armed_throttled_throttle,
+			armed_throttle,
+			INVALID_STATE,
+			INVALID_STATE,
+			preempted_throttled_throttle,
+		},
+		{
+			armed_throttle,
+			preempted_throttle,
+			preempted_throttled_throttle,
+			running_throttle,
+			preempted_throttle,
+		},
+		{
+			armed_throttled_throttle,
+			preempted_throttle,
+			INVALID_STATE,
+			INVALID_STATE,
+			preempted_throttled_throttle,
+		},
+		{
+			armed_throttled_throttle,
+			running_throttle,
+			INVALID_STATE,
+			INVALID_STATE,
+			preempted_throttled_throttle,
+		},
+	},
+	.initial_state = running_throttle,
+	.final_states = { 1, 0, 0, 0, 0, 0 },
+};
diff --git a/kernel/trace/rv/monitors/throttle/throttle_trace.h b/kernel/trace/rv/monitors/throttle/throttle_trace.h
new file mode 100644
index 000000000000..7e376d3aec60
--- /dev/null
+++ b/kernel/trace/rv/monitors/throttle/throttle_trace.h
@@ -0,0 +1,19 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_THROTTLE
+DEFINE_EVENT(event_da_monitor_id, event_throttle,
+	     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_throttle,
+	     TP_PROTO(int id, char *state, char *event),
+	     TP_ARGS(id, state, event));
+
+DEFINE_EVENT(error_env_da_monitor_id, error_env_throttle,
+	     TP_PROTO(int id, char *state, char *event, char *env),
+	     TP_ARGS(id, state, event, env));
+#endif /* CONFIG_RV_MON_THROTTLE */
diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index 2f8a932432c9..9896beae73af 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -189,6 +189,7 @@ 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>
 // Add new monitors based on CONFIG_HA_MON_EVENTS_ID here
 
 #endif
diff --git a/tools/verification/models/deadline/throttle.dot b/tools/verification/models/deadline/throttle.dot
new file mode 100644
index 000000000000..c24fc3f291a9
--- /dev/null
+++ b/tools/verification/models/deadline/throttle.dot
@@ -0,0 +1,44 @@
+digraph state_automaton {
+	center = true;
+	size = "7,11";
+	{node [shape = circle] "armed"};
+	{node [shape = circle] "armed_throttled"};
+	{node [shape = circle] "preempted"};
+	{node [shape = circle] "preempted_throttled"};
+	{node [shape = plaintext, style=invis, label=""] "__init_running"};
+	{node [shape = doublecircle] "running"};
+	{node [shape = circle] "running"};
+	{node [shape = circle] "throttled"};
+	"__init_running" -> "running";
+	"armed" [label = "armed"];
+	"armed" -> "armed" [ label = "dl_replenish\ndl_defer_arm" ];
+	"armed" -> "armed_throttled" [ label = "dl_throttle" ];
+	"armed" -> "preempted" [ label = "sched_switch_out" ];
+	"armed" -> "running" [ label = "sched_switch_in;reset(clk)" ];
+	"armed_throttled" [label = "armed_throttled"];
+	"armed_throttled" -> "armed" [ label = "dl_replenish" ];
+	"armed_throttled" -> "armed_throttled" [ label = "dl_defer_arm" ];
+	"armed_throttled" -> "preempted_throttled" [ label = "sched_switch_out" ];
+	"preempted" [label = "preempted"];
+	"preempted" -> "armed" [ label = "dl_defer_arm" ];
+	"preempted" -> "preempted" [ label = "dl_replenish\nsched_switch_out" ];
+	"preempted" -> "preempted_throttled" [ label = "dl_throttle;is_constr_dl == 1" ];
+	"preempted" -> "running" [ label = "sched_switch_in;reset(clk)" ];
+	"preempted_throttled" [label = "preempted_throttled"];
+	"preempted_throttled" -> "armed_throttled" [ label = "dl_defer_arm" ];
+	"preempted_throttled" -> "preempted" [ label = "dl_replenish" ];
+	"preempted_throttled" -> "preempted_throttled" [ label = "sched_switch_out" ];
+	"running" [label = "running\nclk < runtime_left_ns()", color = green3];
+	"running" -> "armed" [ label = "dl_defer_arm" ];
+	"running" -> "preempted" [ label = "sched_switch_out" ];
+	"running" -> "running" [ label = "dl_replenish;reset(clk)\nsched_switch_in" ];
+	"running" -> "throttled" [ label = "dl_throttle;reset(clk)" ];
+	"throttled" [label = "throttled\nclk < THROTTLED_TIME_NS"];
+	"throttled" -> "armed_throttled" [ label = "dl_defer_arm" ];
+	"throttled" -> "preempted_throttled" [ label = "sched_switch_out" ];
+	"throttled" -> "running" [ label = "dl_replenish;reset(clk)" ];
+	{ rank = min ;
+		"__init_running";
+		"running";
+	}
+}
-- 
2.55.0


^ permalink raw reply related	[flat|nested] 3+ messages in thread

* [PATCH 08/10] rv: Add dl_server specific monitors
       [not found] <20260929124908.177676-1-gmonaco@redhat.com>
  2026-09-29 12:49 ` [PATCH 06/10] rv: Add enqueue/dequeue to snroc monitor Gabriele Monaco
  2026-09-29 12:49 ` [PATCH 07/10] rv: Add throttle deadline monitor Gabriele Monaco
@ 2026-09-29 12:49 ` Gabriele Monaco
  2 siblings, 0 replies; 3+ messages in thread
From: Gabriele Monaco @ 2026-09-29 12:49 UTC (permalink / raw)
  To: linux-kernel, linux-trace-kernel, Steven Rostedt, Gabriele Monaco,
	Jonathan Corbet, Masami Hiramatsu, linux-doc
  Cc: Nam Cao, Juri Lelli, Wen Yang

Add monitors to validate the behaviour of the deadline server.

The currently implemented monitors are:
* boost
    fair tasks run either independently or boosted
* laxity
    deferrable servers wait for zero-laxity and run

Reviewed-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Juri Lelli <juri.lelli@redhat.com>
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
---
 Documentation/trace/rv/monitor_deadline.rst   | 127 ++++++++
 kernel/trace/rv/Kconfig                       |   2 +
 kernel/trace/rv/Makefile                      |   2 +
 kernel/trace/rv/monitors/boost/Kconfig        |  15 +
 kernel/trace/rv/monitors/boost/boost.c        | 276 ++++++++++++++++++
 kernel/trace/rv/monitors/boost/boost.h        | 146 +++++++++
 kernel/trace/rv/monitors/boost/boost_trace.h  |  19 ++
 kernel/trace/rv/monitors/laxity/Kconfig       |  14 +
 kernel/trace/rv/monitors/laxity/laxity.c      | 253 ++++++++++++++++
 kernel/trace/rv/monitors/laxity/laxity.h      | 133 +++++++++
 .../trace/rv/monitors/laxity/laxity_trace.h   |  19 ++
 kernel/trace/rv/rv_trace.h                    |   2 +
 tools/verification/models/deadline/boost.dot  |  48 +++
 tools/verification/models/deadline/laxity.dot |  36 +++
 14 files changed, 1092 insertions(+)
 create mode 100644 kernel/trace/rv/monitors/boost/Kconfig
 create mode 100644 kernel/trace/rv/monitors/boost/boost.c
 create mode 100644 kernel/trace/rv/monitors/boost/boost.h
 create mode 100644 kernel/trace/rv/monitors/boost/boost_trace.h
 create mode 100644 kernel/trace/rv/monitors/laxity/Kconfig
 create mode 100644 kernel/trace/rv/monitors/laxity/laxity.c
 create mode 100644 kernel/trace/rv/monitors/laxity/laxity.h
 create mode 100644 kernel/trace/rv/monitors/laxity/laxity_trace.h
 create mode 100644 tools/verification/models/deadline/boost.dot
 create mode 100644 tools/verification/models/deadline/laxity.dot

diff --git a/Documentation/trace/rv/monitor_deadline.rst b/Documentation/trace/rv/monitor_deadline.rst
index e88f631d8387..ce714bf6f9d9 100644
--- a/Documentation/trace/rv/monitor_deadline.rst
+++ b/Documentation/trace/rv/monitor_deadline.rst
@@ -156,3 +156,130 @@ become ``preempted``::
 The value of ``runtime_left_ns()`` is directly read from the deadline entity
 and updated as the task runs. It is increased by 1 tick to account for the
 maximum delay to throttle (not valid if ``sched_feat(HRTICK_DL)`` is active).
+
+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 (the server period ``T()``), 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``: a fair task woke up, this event is especially frequent on self
+  loops (no state change during a wakeup) but is removed here for clarity.
+  It's main purpose it's to capture the transition ``idle -> ready``.
+* ``resume_throttle``: a fair task woke up, potentially when the server
+  is going to be throttled (no runtime left). This is equivalent to ``resume``,
+  but it's going to be followed by throttle and the invariant in ``idle`` is
+  likely already invalid. It triggers also erroneously when the CPU is fully
+  idle, in that case the runtime is likely stale as it's still consumed by
+  idle, the event may not be followed by a throttle but the task is very likely
+  to run and the state machine is going to be fixed on the next replenish
+  (forced to happen within a period ``T()``).
+* 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 < T()   |   |                          |         |
+  |   |  |         +---------------+ <-+        +---------------- +---------+
+  |   |  |         |  ^                         |                   ^    |
+  |   |  |         |  |                       throttle;reset(clk)   |    |
+  |   |  |         |  |replenish;reset(clk)     |                   |    |
+  |   |  |  throttle; |                         |   replenish;reset(clk) |
+  |   |  |   reset()  |                         |                   |    |
+  |   |  |         v  |                         v                   |    |
+  |   |  |   +---------+    switch    +-------------------+         |    |
+  x---+--+-- |throttled| <----------> | throttled_running | --------+    |
+  |   |  |   |         |              |     clk < T()     |              |
+  |   |  |   |clk < T()| -----+       +-------------------+              |
+  |   |  |   +---------+      |            |                             |
+  |   |  |      ^             |            |                             |
+  |   |  | resume_throttle;   |            |                             |
+ stop |  |     reset(clk)     |            |                             |
+  |   |  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    |               dl_update
+ |   |       v            |                    |        dl_replenish;reset(clk)
+ |   |   +-------------------+                 |   dl_replenish_idle;reset(clk)
+ |   |   |  replenish_wait   |                 |                     |
+ |   |   | clk < period_ns() | ----------------+---------------------+--------+
+ |   |   +-------------------+                 |                     |        |
+ |   |                   |                     |                     |        |
+ |   |               dl_update                 |                     |        |
+ |   |         dl_replenish;reset(clk)     dl_replenish_running      |        |
+ |   |                   v                     |                     |        |
+ |   |                 +--------------------------+                  |        |
+ | dl_server_start;    |                          | <----------------+        |
+ |   reset(clk)        |     zero_laxity_wait     |                           |
+ |   |                 |     clk < period_ns()    | ------+ dl_replenish;     |
+ |   +---------------> |                          |       |    reset(clk)     |
+ |                     +--------------------------+ <-----+ dl_update         |
+ |                               |              ^                             |
+ |  dl_replenish_idle;reset(clk) |      dl_replenish;reset(clk)               |
+ |                               v            dl_update                       |
+ |                  +------------------------+  |                             |
+ +----------------- |        idle_wait       | -+                             |
+                    |   clk < period_ns()    |                                |
+                    +------------------------+ <-- dl_replenish_idle;reset(clk)
+                         ^             |
+                         +------dl_replenish_idle;reset(clk)
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index cdb851c7cceb..2f2d25bc972b 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -83,6 +83,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
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index 1387082dc490..81c557b26334 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -22,6 +22,8 @@ obj-$(CONFIG_RV_MON_DEADLINE) += monitors/deadline/deadline.o
 obj-$(CONFIG_RV_MON_NOMISS) += monitors/nomiss/nomiss.o
 obj-$(CONFIG_RV_MON_WAKEUP) += monitors/wakeup/wakeup.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
diff --git a/kernel/trace/rv/monitors/boost/Kconfig b/kernel/trace/rv/monitors/boost/Kconfig
new file mode 100644
index 000000000000..3fa121f77729
--- /dev/null
+++ b/kernel/trace/rv/monitors/boost/Kconfig
@@ -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
diff --git a/kernel/trace/rv/monitors/boost/boost.c b/kernel/trace/rv/monitors/boost/boost.c
new file mode 100644
index 000000000000..3533d23279ee
--- /dev/null
+++ b/kernel/trace/rv/monitors/boost/boost.c
@@ -0,0 +1,276 @@
+// 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 period_ns(struct ha_monitor *ha_mon)
+{
+	struct sched_dl_entity *dl_se = ha_get_target(ha_mon);
+
+	return dl_se->dl_period + TICK_NSEC;
+}
+
+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);
+	else if (curr_state == throttled_boost)
+		return ha_check_invariant_ns(ha_mon, clk_boost, time_ns);
+	else if (curr_state == throttled_running_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 == idle_boost && event == dl_server_resume_throttled_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 == ready_boost && event == dl_throttle_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 == running_boost && event == dl_throttle_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, period_ns(ha_mon), time_ns);
+	else if (next_state == throttled_boost)
+		ha_start_timer_ns(ha_mon, clk_boost, period_ns(ha_mon), time_ns);
+	else if (next_state == throttled_running_boost)
+		ha_start_timer_ns(ha_mon, clk_boost, period_ns(ha_mon), time_ns);
+	else if (curr_state == ready_boost)
+		ha_cancel_timer(ha_mon);
+	else if (curr_state == throttled_boost)
+		ha_cancel_timer(ha_mon);
+	else if (curr_state == throttled_running_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, u8 type)
+{
+	if (is_server_type(type))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_replenish_boost);
+}
+
+static inline void handle_server_switch(struct task_struct *next,
+					struct task_struct *prev, int cpu,
+					u8 type)
+{
+	struct sched_dl_entity *dl_se = get_server(next, type);
+
+	if (!dl_se)
+		return;
+	if (is_idle_task(next))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_server_idle_boost);
+	else if (get_server_type(next) == type && !rt_or_dl_task(next))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), sched_switch_in_boost);
+	else if (get_server_type(prev) == type && !is_idle_task(prev))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), sched_switch_out_boost);
+}
+
+static void handle_sched_switch(void *data, bool preempt,
+				struct task_struct *prev,
+				struct task_struct *next,
+				unsigned int prev_state)
+{
+	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 (get_server_type(next) == get_server_type(prev) &&
+	    !is_idle_task(next) && !is_idle_task(prev))
+		return;
+	handle_server_switch(next, prev, cpu, DL_SERVER_FAIR);
+	if (IS_ENABLED(CONFIG_SCHED_CLASS_EXT))
+		handle_server_switch(next, prev, cpu, DL_SERVER_EXT);
+}
+
+static void handle_sched_enqueue(void *data, struct task_struct *tsk, int cpu)
+{
+	struct sched_dl_entity *dl_se = NULL;
+	u8 type = get_server_type(tsk);
+
+	if (is_server_type(type))
+		dl_se = get_server(tsk, type);
+	if (dl_se) {
+		da_handle_event(EXPAND_ID(dl_se, cpu, type),
+				dl_se->runtime > 0 && !idle_cpu(cpu) ?
+					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 = NULL;
+	u8 type = get_server_type(tsk);
+
+	if (is_server_type(type))
+		dl_se = get_server(tsk, type);
+	/*
+	 * 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 && task_is_running(tsk) && sched_task_on_rq(tsk))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), sched_switch_out_boost);
+}
+
+static void handle_dl_server_start(void *data, struct sched_dl_entity *dl_se,
+				   int cpu, u8 type)
+{
+	if (is_server_type(type))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_server_start_boost);
+}
+
+static void handle_dl_server_stop(void *data, struct sched_dl_entity *dl_se,
+				  int cpu, u8 type)
+{
+	if (is_server_type(type))
+		da_handle_start_event(EXPAND_ID(dl_se, cpu, type), dl_server_stop_boost);
+}
+
+static void handle_dl_throttle(void *data, struct sched_dl_entity *dl_se,
+			       int cpu, u8 type)
+{
+	if (is_server_type(type))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_throttle_boost);
+}
+
+static int enable_boost(void)
+{
+	int retval;
+
+	retval = ha_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);
+
+	ha_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.");
diff --git a/kernel/trace/rv/monitors/boost/boost.h b/kernel/trace/rv/monitors/boost/boost.h
new file mode 100644
index 000000000000..e5ca85cc6620
--- /dev/null
+++ b/kernel/trace/rv/monitors/boost/boost.h
@@ -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,
+			throttled_boost,
+			throttled_boost,
+			INVALID_STATE,
+			stopped_boost,
+			throttled_boost,
+			throttled_running_boost,
+			throttled_boost,
+		},
+		{
+			running_boost,
+			idle_boost,
+			throttled_running_boost,
+			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 },
+};
diff --git a/kernel/trace/rv/monitors/boost/boost_trace.h b/kernel/trace/rv/monitors/boost/boost_trace.h
new file mode 100644
index 000000000000..7e422b0e586d
--- /dev/null
+++ b/kernel/trace/rv/monitors/boost/boost_trace.h
@@ -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 */
diff --git a/kernel/trace/rv/monitors/laxity/Kconfig b/kernel/trace/rv/monitors/laxity/Kconfig
new file mode 100644
index 000000000000..7ba69405d09b
--- /dev/null
+++ b/kernel/trace/rv/monitors/laxity/Kconfig
@@ -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
diff --git a/kernel/trace/rv/monitors/laxity/laxity.c b/kernel/trace/rv/monitors/laxity/laxity.c
new file mode 100644
index 000000000000..751d31822436
--- /dev/null
+++ b/kernel/trace/rv/monitors/laxity/laxity.c
@@ -0,0 +1,253 @@
+// 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 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_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == idle_wait_laxity && event == dl_replenish_idle_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 == replenish_wait_laxity && event == dl_replenish_running_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == running_laxity && event == dl_replenish_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == running_laxity && event == dl_replenish_idle_laxity)
+		ha_reset_env(ha_mon, clk_laxity, time_ns);
+	else if (curr_state == running_laxity && event == dl_replenish_running_laxity)
+		res = ha_get_env(ha_mon, clk_laxity, time_ns) < REPLENISH_NS;
+	else if (curr_state == running_laxity && event == dl_throttle_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 == stopped_laxity && event == dl_server_start_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);
+	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);
+	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;
+
+	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, u8 type)
+{
+	if (!is_server_type(type))
+		return;
+	/* 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, type), dl_replenish_running_laxity);
+	else if (idle_cpu(cpu))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_replenish_idle_laxity);
+	else
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_replenish_laxity);
+}
+
+static void handle_dl_server_start(void *data, struct sched_dl_entity *dl_se,
+				   int cpu, u8 type)
+{
+	if (!is_server_type(type))
+		return;
+	if (dl_se->dl_defer_running)
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_server_start_running_laxity);
+	else
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_server_start_laxity);
+}
+
+static void handle_dl_server_stop(void *data, struct sched_dl_entity *dl_se,
+				  int cpu, u8 type)
+{
+	if (is_server_type(type))
+		da_handle_start_event(EXPAND_ID(dl_se, cpu, type), dl_server_stop_laxity);
+}
+
+static void handle_dl_throttle(void *data, struct sched_dl_entity *dl_se,
+			       int cpu, u8 type)
+{
+	if (is_server_type(type))
+		da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_throttle_laxity);
+}
+
+static void handle_dl_update(void *data, struct sched_dl_entity *dl_se,
+			       int cpu, u8 type)
+{
+	if (!is_server_type(type) || idle_cpu(cpu) || dl_se->dl_defer_running)
+		return;
+	/* The idle flag can be cleared without passing from an actual replenish */
+	da_handle_event(EXPAND_ID(dl_se, cpu, type), dl_update_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)
+		return;
+	da_handle_event(EXPAND_ID(next->dl_server, task_cpu(next),
+				  get_server_type(next)),
+			sched_switch_in_laxity);
+}
+
+static int enable_laxity(void)
+{
+	int retval;
+
+	retval = ha_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_dl_update_tp, handle_dl_update);
+	rv_attach_trace_probe("laxity", sched_switch, handle_sched_switch);
+
+	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_dl_update_tp, handle_dl_update);
+	rv_detach_trace_probe("laxity", sched_switch, handle_sched_switch);
+
+	ha_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.");
diff --git a/kernel/trace/rv/monitors/laxity/laxity.h b/kernel/trace/rv/monitors/laxity/laxity.h
new file mode 100644
index 000000000000..69a818c0f6cf
--- /dev/null
+++ b/kernel/trace/rv/monitors/laxity/laxity.h
@@ -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_start_laxity,
+	dl_server_start_running_laxity,
+	dl_server_stop_laxity,
+	dl_throttle_laxity,
+	dl_update_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_start",
+		"dl_server_start_running",
+		"dl_server_stop",
+		"dl_throttle",
+		"dl_update",
+		"sched_switch_in",
+	},
+	.env_names = {
+		"clk",
+	},
+	.function = {
+		{
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			zero_laxity_wait_laxity,
+			running_laxity,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+		},
+		{
+			zero_laxity_wait_laxity,
+			idle_wait_laxity,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			stopped_laxity,
+			INVALID_STATE,
+			zero_laxity_wait_laxity,
+			INVALID_STATE,
+		},
+		{
+			zero_laxity_wait_laxity,
+			idle_wait_laxity,
+			running_laxity,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			zero_laxity_wait_laxity,
+			INVALID_STATE,
+		},
+		{
+			zero_laxity_wait_laxity,
+			zero_laxity_wait_laxity,
+			running_laxity,
+			INVALID_STATE,
+			INVALID_STATE,
+			stopped_laxity,
+			replenish_wait_laxity,
+			zero_laxity_wait_laxity,
+			running_laxity,
+		},
+		{
+			zero_laxity_wait_laxity,
+			idle_wait_laxity,
+			running_laxity,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			INVALID_STATE,
+			zero_laxity_wait_laxity,
+			INVALID_STATE,
+		},
+	},
+	.initial_state = stopped_laxity,
+	.final_states = { 1, 0, 0, 0, 0 },
+};
diff --git a/kernel/trace/rv/monitors/laxity/laxity_trace.h b/kernel/trace/rv/monitors/laxity/laxity_trace.h
new file mode 100644
index 000000000000..32580dba8f42
--- /dev/null
+++ b/kernel/trace/rv/monitors/laxity/laxity_trace.h
@@ -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 */
diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index 9896beae73af..ad4df55eb727 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -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
diff --git a/tools/verification/models/deadline/boost.dot b/tools/verification/models/deadline/boost.dot
new file mode 100644
index 000000000000..05a927b034d9
--- /dev/null
+++ b/tools/verification/models/deadline/boost.dot
@@ -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;reset(clk)" ];
+	"ready" [label = "ready\nclk < period_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;reset(clk)" ];
+	"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;reset(clk)" ];
+	"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\nclk < period_ns()"];
+	"throttled" -> "idle" [ label = "dl_server_idle" ];
+	"throttled" -> "ready" [ label = "dl_replenish;reset(clk)" ];
+	"throttled" -> "stopped" [ label = "dl_server_stop" ];
+	"throttled" -> "throttled" [ label = "dl_throttle\nsched_switch_out\ndl_server_resume_throttled\ndl_server_resume" ];
+	"throttled" -> "throttled_running" [ label = "sched_switch_in" ];
+	"throttled_running" [label = "throttled_running\nclk < period_ns()"];
+	"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\ndl_server_resume" ];
+	{ rank = min ;
+		"__init_stopped";
+		"stopped";
+	}
+}
diff --git a/tools/verification/models/deadline/laxity.dot b/tools/verification/models/deadline/laxity.dot
new file mode 100644
index 000000000000..e4fdabfe1743
--- /dev/null
+++ b/tools/verification/models/deadline/laxity.dot
@@ -0,0 +1,36 @@
+digraph state_automaton {
+	center = true;
+	size = "7,11";
+	{node [shape = circle] "idle_wait"};
+	{node [shape = circle] "replenish_wait"};
+	{node [shape = circle] "running"};
+	{node [shape = plaintext, style=invis, label=""] "__init_stopped"};
+	{node [shape = doublecircle] "stopped"};
+	{node [shape = circle] "stopped"};
+	{node [shape = circle] "zero_laxity_wait"};
+	"__init_stopped" -> "stopped";
+	"idle_wait" [label = "idle_wait\nclk < period_ns()"];
+	"idle_wait" -> "idle_wait" [ label = "dl_replenish_idle;reset(clk)" ];
+	"idle_wait" -> "stopped" [ label = "dl_server_stop" ];
+	"idle_wait" -> "zero_laxity_wait" [ label = "dl_replenish;reset(clk)\ndl_update" ];
+	"replenish_wait" [label = "replenish_wait\nclk < period_ns()"];
+	"replenish_wait" -> "idle_wait" [ label = "dl_replenish_idle;reset(clk)" ];
+	"replenish_wait" -> "running" [ label = "dl_replenish_running;reset(clk)" ];
+	"replenish_wait" -> "zero_laxity_wait" [ label = "dl_update\ndl_replenish;reset(clk)" ];
+	"running" [label = "running"];
+	"running" -> "replenish_wait" [ label = "dl_throttle;reset(clk)" ];
+	"running" -> "running" [ label = "sched_switch_in\ndl_replenish_running;clk < REPLENISH_NS" ];
+	"running" -> "stopped" [ label = "dl_server_stop" ];
+	"running" -> "zero_laxity_wait" [ label = "dl_replenish;reset(clk)\ndl_replenish_idle;reset(clk)\ndl_update" ];
+	"stopped" [label = "stopped", color = green3];
+	"stopped" -> "running" [ label = "dl_server_start_running;reset(clk)" ];
+	"stopped" -> "zero_laxity_wait" [ label = "dl_server_start;reset(clk)" ];
+	"zero_laxity_wait" [label = "zero_laxity_wait\nclk < period_ns()"];
+	"zero_laxity_wait" -> "idle_wait" [ label = "dl_replenish_idle;reset(clk)" ];
+	"zero_laxity_wait" -> "running" [ label = "dl_replenish_running;reset(clk)" ];
+	"zero_laxity_wait" -> "zero_laxity_wait" [ label = "dl_replenish;reset(clk)\ndl_update" ];
+	{ rank = min ;
+		"__init_stopped";
+		"stopped";
+	}
+}
-- 
2.55.0


^ permalink raw reply related	[flat|nested] 3+ messages in thread

end of thread, other threads:[~2026-09-29 12:50 UTC | newest]

Thread overview: 3+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
     [not found] <20260929124908.177676-1-gmonaco@redhat.com>
2026-09-29 12:49 ` [PATCH 06/10] rv: Add enqueue/dequeue to snroc monitor Gabriele Monaco
2026-09-29 12:49 ` [PATCH 07/10] rv: Add throttle deadline monitor Gabriele Monaco
2026-09-29 12:49 ` [PATCH 08/10] rv: Add dl_server specific monitors Gabriele Monaco

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox