diff mbox series

[RFC,9/9] rv: Add srs per-task monitor

Message ID 20250404084512.98552-20-gmonaco@redhat.com (mailing list archive)
State New
Headers show
Series [RFC,1/9] tools/rv: Do not skip idle in trace | expand

Commit Message

Gabriele Monaco April 4, 2025, 8:45 a.m. UTC
Add a per-task monitor for task switches as part of the sched model:

* srs:
    Monitor to describe conditions for different types of task switch.
    This monitor enforces rules such as preempt after setting need
    for reschedule and suspend after setting a task to sleepable.

This new monitor implies the previously introduced snroc (set non
runnable on its own context), so replace that monitor with srs.

Cc: Ingo Molnar <mingo@redhat.com>
Cc: Peter Zijlstra <peterz@infradead.org>
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
---
 Documentation/trace/rv/monitor_sched.rst      | 169 +++++++++++++++---
 kernel/trace/rv/Kconfig                       |   2 +-
 kernel/trace/rv/Makefile                      |   2 +-
 kernel/trace/rv/monitors/snroc/snroc.c        |  85 ---------
 kernel/trace/rv/monitors/snroc/snroc.h        |  47 -----
 .../trace/rv/monitors/{snroc => srs}/Kconfig  |   8 +-
 kernel/trace/rv/monitors/srs/srs.c            | 135 ++++++++++++++
 kernel/trace/rv/monitors/srs/srs.h            |  87 +++++++++
 .../{snroc/snroc_trace.h => srs/srs_trace.h}  |   8 +-
 kernel/trace/rv/rv_trace.h                    |   2 +-
 tools/verification/models/sched/snroc.dot     |  18 --
 tools/verification/models/sched/srs.dot       |  61 +++++++
 12 files changed, 443 insertions(+), 181 deletions(-)
 delete mode 100644 kernel/trace/rv/monitors/snroc/snroc.c
 delete mode 100644 kernel/trace/rv/monitors/snroc/snroc.h
 rename kernel/trace/rv/monitors/{snroc => srs}/Kconfig (52%)
 create mode 100644 kernel/trace/rv/monitors/srs/srs.c
 create mode 100644 kernel/trace/rv/monitors/srs/srs.h
 rename kernel/trace/rv/monitors/{snroc/snroc_trace.h => srs/srs_trace.h} (67%)
 delete mode 100644 tools/verification/models/sched/snroc.dot
 create mode 100644 tools/verification/models/sched/srs.dot
diff mbox series

Patch

diff --git a/Documentation/trace/rv/monitor_sched.rst b/Documentation/trace/rv/monitor_sched.rst
index 641e70e359aaa..c1516b71b8e73 100644
--- a/Documentation/trace/rv/monitor_sched.rst
+++ b/Documentation/trace/rv/monitor_sched.rst
@@ -61,27 +61,6 @@  happen only in thread context::
                                             |
                        scheduling_context  -+
 
-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::
-
-                        |
-                        |
-                        v
-                      +------------------+
-                      |  other_context   | <+
-                      +------------------+  |
-                        |                   |
-                        | sched_switch_in   | sched_switch_out
-                        v                   |
-    sched_set_state                         |
-  +------------------                       |
-  |                       own_context       |
-  +----------------->                      -+
-
 Monitor scpd
 ~~~~~~~~~~~~
 
@@ -193,6 +172,154 @@  real task switch occurs::
   +-------------- |                    | <-------------+
                   +--------------------+
 
+Monitor srs
+-----------
+
+The switch after resched or sleep (srs) monitor describes conditions for
+different types of task switch. This is a complex model, below we are going to
+explain it step by step. Unfortunately splitting this into smaller monitor is
+not trivial due to some shared events such as ``switch_in``::
+
+                                                      set_runnable
+                                  |                        wakeup +---+
+                                  |                   switch_vain |   |
+                                  v                               |   v      wakeup
+                         #================================================#  set_runnable
+      switch_in          H                                                H <----------+
+    +------------------> H                    running                     H            |
+    |                    H                                                H -----+     |
+    |                    #================================================#      |     |
+    |                         |        |                |         ^    ^         |     |
+    |                         |  switch_yield      need_resched   |    |         |     |
+    |                         |        |      need_resched_lazy   |    |         |     |
+    |                set_sleepable     v                |         |    |         |     |
+    |                         |      +-------------+    |         |    |         |     |
+    |                +--------+----> |  preempted  | ---+- switch_in   |         |     |
+    |                |        |      +-------------+    |              |         |     |
+    |        switch_preempt   |        |                |              |         |     |
+    |        switch_yield     |   need_resched          |   +- switch_vain       |     |
+    |                |        |        v                |   |                    |     |
+    |                |        |      +-------------+    |   |                    |     |
+    |  need_resched -+--------+----> | resched_out |    |   |                    |     |
+    |  |             |        |      +-------------+    |   |                    |     |
+    |  |             |        |        |                |   |     need_resched   |     |
+    |  |             |        |    switch_in            |   |     wakeup         |     |
+    |  |             |        |        v                v   |     set_runnable   |     |
+    |  |             |        |      +--------------------------+ -------+       |     |
+    |  |             |        |      |                          |        |       |     |
+    |  |             +--------+----- |       rescheduling       | <------+       |     |
+    |  |                      |      |                          |                |     |
+    |  |                      |      +--------------------------+ -----------+   |     |
+    |  |                      |        |           ^ wakeup                  |   |     |
+    |  |                      |  set_sleepable   set_runnable                |   |     |
+    |  |                      |        v           |                         |   |     |
+    |  |   +------------------+----- +---------------------------+           |   |     |
+    |  |   |                  |      |                           |           |   |     |
+ +--+--+---+------------------+----> |     resched_sleepable     | ---+      |   |     |
+ |  |  |   |                  |      |                           |    |      |   |     |
+ |  |  |   |    +-------------+----> +---------------------------+    |      |   |     |
+ |  |  |   |    |             |        |           ^      |           |      |   |     |
+ |  |  |   |    |             |  switch_preempt    | need_resched     |      |   |     |
+ |  |  |   |    |             |        |           | set_sleepable    |      |   |     |
+ |  |  |   |    |             |        v           +------+           |      |   |     |
+ |  |  |   |    |             |       +---------------------------+ --+------+---+-----+--+
+ |  |  |   |    |             |       |    preempted_sleepable    |   |      |   |     |  |
+ |  |  |   |    |             |       +---------------------------+ --+------+---+--+  |  |
+ |  |  |   |    |             |         |             ^               |      |   |  |  |  |
+ |  |  |   |    |             |     switch_in   switch_preempt        |      |   |  |  |  |
+ |  |  |   |    |             |         v             |          switch_vain |   |  |  |  |
+ |  |  |   |    |             |        +-------------------------+    |      |   |  |  |  |
+ |  |  |   |    |             +------> |                         | <--+      |   |  |  |  |
+ |  |  |   |    |                      |        sleepable        |           |   |  |  |  |
+ |  |  |   |    +- need_resched------- |                         | ----------+---+--+--+  |
+ |  |  |   |       need_resched_lazy   +-------------------------+           |   |  |     |
+ |  |  |   |                              |      ^      |          switch_block  |  |     |
+ |  |  |   |                              |      | set_sleepable             |   |  |     |
+ |  |  |   |                      switch_block   | switch_vain    +----------+   |  |     |
+ |  |  |   |                    switch_suspend   +------+         |              |  |     |
+ |  |  |   |                              v                       v              |  |     |
+ |  |  |   |   switch_block          +-----------------------------+  switch_block  |     |
+ |  |  |   +-switch_suspend--------> |          sleeping           | <-----------+  |     |
+ |  |  |                             +-----------------------------+                |     |
+ |  |  |                               | wakeup                                     |     |
+ |  |  |                               v                                            |     |
+ |  |  +- need_resched ------------- +-------------+  wakeup                        |     |
+ |  |                                |   waking    | <------------------------------+     |
+ |  +------------------------------- +-------------+                                      |
+ |                                                                                        |
+ |                         +-----------------------+                                      |
+ +----- switch_in -------- | resched_out_sleepable | <-- sched_need_resched --------------+
+                           +-----------------------+
+
+Types of switches:
+
+* ``switch_in``:
+  a non running task is scheduled in, this leads to ``running`` if the task is
+  runnable and ``sleepable`` if the task was preempted before sleeping.
+* ``switch_suspend``:
+  a task puts itself to sleep, this can happen only after explicitly setting
+  the task to ``sleepable``. After a task is suspended, it needs to be woken up
+  (``waking`` state) before being switched in again. The task can be set to
+  ``resched_sleepable`` via a ``need_resched`` but not preempted, in which case it
+  is equivalent to ``sleepable``.
+  Setting the task's state to ``sleepable`` can be reverted before switching if it
+  is woken up or set to runnable.
+* ``switch_blocked``:
+  a special case of a ``switch_suspend`` where the task is waiting on a
+  sleeping RT lock (``PREEMPT_RT`` only), it is common to see wakeup and set
+  state events racing with each other and this leads the model to perceive this
+  type of switch when the task is not set to sleepable. This is a limitation of
+  the model in SMP system and workarounds may require to slow down the
+  scheduler.
+* ``switch_yield``:
+  a task explicitly calls the scheduler, this looks like a preemption as the
+  task is still runnable but the ``need_resched`` flag is not set. It can
+  happen after a ``yield`` system call or from the idle task.
+* ``switch_preempt``:
+  a task is ``preempted``, this can happen after the need for ``rescheduling``
+  has been set, also in its ``lazy`` flavour. ``need_resched`` can be set as a
+  flag to the task or in the per-core preemption count, either of them can
+  trigger a preemption.
+  The task was previously running and can be switched in directly, but it is
+  possible that a task is preempted after it sets itself as ``sleepable``
+  (``preempted_sleepable``), in this condition, once the task is switched back
+  in, it will not be ``running`` but continue its sleeping process in
+  ``sleepable``.
+* ``switch_vain``:
+  a task goes through the scheduler but it is picked as the next task to run,
+  hence no real task switch occurs. Since we run the scheduler, this clears the
+  need to reschedule.
+
+The ``resched_out`` state (``resched_out_sleepable`` if the task is sleepable)
+is a special case reached if the ``need_resched`` is set after picking the next
+task but before switching. In this case, the previous task is switched out
+normally but once it switches in, it can be preempted in ``rescheduling``. This
+can happen, for instance, when a task disables migration and we do a
+dequeue/enqueue before actually switching out.
+
+This monitor has several events that can race with each other, for instance if
+running from multiple CPUs (e.g. ``need_resched`` and ``wakeup`` can occur from
+a remote CPU), we need to account for them in any possible order.
+
+This monitor allows set state (runnable or sleepable) only in states
+``running``, ``rescheduling``, ``resched_sleepable``, and ``sleepable``, and
+not for states where the task is ``sleeping`` or ``preempted``. This implies
+the set state event occurs only in the task's context::
+
+                        |
+                        |
+                        v
+                      +------------------+
+                      |  other_context   | <+
+                      +------------------+  |
+                        |                   |
+                        | switch_in         | switch_out
+                        v                   |
+    sched_set_state                         |
+  +------------------                       |
+  |                       own_context       |
+  +----------------->                      -+
+
 References
 ----------
 
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index a53a3eca9616d..f296095f1df28 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -29,11 +29,11 @@  source "kernel/trace/rv/monitors/wip/Kconfig"
 source "kernel/trace/rv/monitors/wwnr/Kconfig"
 source "kernel/trace/rv/monitors/sched/Kconfig"
 source "kernel/trace/rv/monitors/sco/Kconfig"
-source "kernel/trace/rv/monitors/snroc/Kconfig"
 source "kernel/trace/rv/monitors/scpd/Kconfig"
 source "kernel/trace/rv/monitors/snep/Kconfig"
 source "kernel/trace/rv/monitors/sncid/Kconfig"
 source "kernel/trace/rv/monitors/sts/Kconfig"
+source "kernel/trace/rv/monitors/srs/Kconfig"
 # Add new monitors here
 
 config RV_REACTORS
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index c609b72275cb8..5aba1d85ad662 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -7,11 +7,11 @@  obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o
 obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o
 obj-$(CONFIG_RV_MON_SCHED) += monitors/sched/sched.o
 obj-$(CONFIG_RV_MON_SCO) += monitors/sco/sco.o
-obj-$(CONFIG_RV_MON_SNROC) += monitors/snroc/snroc.o
 obj-$(CONFIG_RV_MON_SCPD) += monitors/scpd/scpd.o
 obj-$(CONFIG_RV_MON_SNEP) += monitors/snep/snep.o
 obj-$(CONFIG_RV_MON_SNCID) += monitors/sncid/sncid.o
 obj-$(CONFIG_RV_MON_STS) += monitors/sts/sts.o
+obj-$(CONFIG_RV_MON_SRS) += monitors/srs/srs.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/snroc/snroc.c b/kernel/trace/rv/monitors/snroc/snroc.c
deleted file mode 100644
index bb1f60d552960..0000000000000
--- a/kernel/trace/rv/monitors/snroc/snroc.c
+++ /dev/null
@@ -1,85 +0,0 @@ 
-// 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>
-#include <rv/da_monitor.h>
-
-#define MODULE_NAME "snroc"
-
-#include <trace/events/sched.h>
-#include <rv_trace.h>
-#include <monitors/sched/sched.h>
-
-#include "snroc.h"
-
-static struct rv_monitor rv_snroc;
-DECLARE_DA_MON_PER_TASK(snroc, unsigned char);
-
-static void handle_sched_set_state(void *data, struct task_struct *tsk, int state)
-{
-	da_handle_event_snroc(tsk, sched_set_state_snroc);
-}
-
-static void handle_sched_switch(void *data, bool preempt,
-				struct task_struct *prev,
-				struct task_struct *next,
-				unsigned int prev_state)
-{
-	da_handle_start_event_snroc(prev, sched_switch_out_snroc);
-	da_handle_event_snroc(next, sched_switch_in_snroc);
-}
-
-static int enable_snroc(void)
-{
-	int retval;
-
-	retval = da_monitor_init_snroc();
-	if (retval)
-		return retval;
-
-	rv_attach_trace_probe("snroc", sched_set_state_tp, handle_sched_set_state);
-	rv_attach_trace_probe("snroc", sched_switch, handle_sched_switch);
-
-	return 0;
-}
-
-static void disable_snroc(void)
-{
-	rv_snroc.enabled = 0;
-
-	rv_detach_trace_probe("snroc", sched_set_state_tp, handle_sched_set_state);
-	rv_detach_trace_probe("snroc", sched_switch, handle_sched_switch);
-
-	da_monitor_destroy_snroc();
-}
-
-static struct rv_monitor rv_snroc = {
-	.name = "snroc",
-	.description = "set non runnable on its own context.",
-	.enable = enable_snroc,
-	.disable = disable_snroc,
-	.reset = da_monitor_reset_all_snroc,
-	.enabled = 0,
-};
-
-static int __init register_snroc(void)
-{
-	rv_register_monitor(&rv_snroc, &rv_sched);
-	return 0;
-}
-
-static void __exit unregister_snroc(void)
-{
-	rv_unregister_monitor(&rv_snroc);
-}
-
-module_init(register_snroc);
-module_exit(unregister_snroc);
-
-MODULE_LICENSE("GPL");
-MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
-MODULE_DESCRIPTION("snroc: set non runnable on its own context.");
diff --git a/kernel/trace/rv/monitors/snroc/snroc.h b/kernel/trace/rv/monitors/snroc/snroc.h
deleted file mode 100644
index c3650a2b1b107..0000000000000
--- a/kernel/trace/rv/monitors/snroc/snroc.h
+++ /dev/null
@@ -1,47 +0,0 @@ 
-/* SPDX-License-Identifier: GPL-2.0 */
-/*
- * Automatically generated C representation of snroc automaton
- * For further information about this format, see kernel documentation:
- *   Documentation/trace/rv/deterministic_automata.rst
- */
-
-enum states_snroc {
-	other_context_snroc = 0,
-	own_context_snroc,
-	state_max_snroc
-};
-
-#define INVALID_STATE state_max_snroc
-
-enum events_snroc {
-	sched_set_state_snroc = 0,
-	sched_switch_in_snroc,
-	sched_switch_out_snroc,
-	event_max_snroc
-};
-
-struct automaton_snroc {
-	char *state_names[state_max_snroc];
-	char *event_names[event_max_snroc];
-	unsigned char function[state_max_snroc][event_max_snroc];
-	unsigned char initial_state;
-	bool final_states[state_max_snroc];
-};
-
-static const struct automaton_snroc automaton_snroc = {
-	.state_names = {
-		"other_context",
-		"own_context"
-	},
-	.event_names = {
-		"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 },
-	},
-	.initial_state = other_context_snroc,
-	.final_states = { 1, 0 },
-};
diff --git a/kernel/trace/rv/monitors/snroc/Kconfig b/kernel/trace/rv/monitors/srs/Kconfig
similarity index 52%
rename from kernel/trace/rv/monitors/snroc/Kconfig
rename to kernel/trace/rv/monitors/srs/Kconfig
index 6e4365a2fea3b..a5b3998b32328 100644
--- a/kernel/trace/rv/monitors/snroc/Kconfig
+++ b/kernel/trace/rv/monitors/srs/Kconfig
@@ -1,13 +1,15 @@ 
 # SPDX-License-Identifier: GPL-2.0-only
 #
-config RV_MON_SNROC
+config RV_MON_SRS
 	depends on RV
 	depends on RV_MON_SCHED
 	default y
 	select DA_MON_EVENTS_ID
-	bool "snroc monitor"
+	bool "srs monitor"
 	help
-	  Monitor to ensure sched_set_state happens only in the respective task's context.
+	  Monitor to describe conditions for different types of task switch.
+	  This monitor enforces rules such as preempt after setting need
+	  for reschedule and suspend after setting a task to sleepable.
 	  This monitor is part of the sched monitors collection.
 
 	  For further information, see:
diff --git a/kernel/trace/rv/monitors/srs/srs.c b/kernel/trace/rv/monitors/srs/srs.c
new file mode 100644
index 0000000000000..3ea7419581e06
--- /dev/null
+++ b/kernel/trace/rv/monitors/srs/srs.c
@@ -0,0 +1,135 @@ 
+// 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>
+#include <rv/da_monitor.h>
+
+#define MODULE_NAME "srs"
+
+#include <trace/events/sched.h>
+#include <rv_trace.h>
+#include <monitors/sched/sched.h>
+
+#include "srs.h"
+
+static struct rv_monitor rv_srs;
+DECLARE_DA_MON_PER_TASK(srs, unsigned char);
+
+static void handle_sched_need_resched(void *data, struct task_struct *tsk, int cpu, int tif)
+{
+	if (tif == TIF_NEED_RESCHED)
+		da_handle_event_srs(tsk, sched_need_resched_srs);
+	else
+		da_handle_event_srs(tsk, sched_need_resched_lazy_srs);
+}
+
+static void handle_schedule_entry(void *data, bool preempt, unsigned long ip)
+{
+	/* special case from preempt_enable */
+	if (preempt && unlikely(!tif_need_resched() && test_preempt_need_resched()))
+		da_handle_event_srs(current, sched_need_resched_srs);
+}
+
+static void handle_sched_set_state(void *data, struct task_struct *tsk, int state)
+{
+	if (state == TASK_RUNNING)
+		da_handle_event_srs(tsk, sched_set_state_runnable_srs);
+	else
+		da_handle_event_srs(tsk, sched_set_state_sleepable_srs);
+}
+
+static void handle_sched_switch(void *data, bool preempt,
+				struct task_struct *prev,
+				struct task_struct *next,
+				unsigned int prev_state)
+{
+	if (preempt)
+		da_handle_event_srs(prev, sched_switch_preempt_srs);
+	else if (prev_state == TASK_RUNNING)
+		da_handle_start_run_event_srs(prev, sched_switch_yield_srs);
+	else if (prev_state == TASK_RTLOCK_WAIT)
+		/* special case of sleeping task with racy conditions */
+		da_handle_event_srs(prev, sched_switch_blocking_srs);
+	else
+		da_handle_event_srs(prev, sched_switch_suspend_srs);
+	/* switch in also leads to sleepable or rescheduling */
+	if (task_is_running(next) && !test_tsk_thread_flag(next, TIF_NEED_RESCHED))
+		da_handle_start_event_srs(next, sched_switch_in_srs);
+	else
+		da_handle_event_srs(next, sched_switch_in_srs);
+}
+
+static void handle_sched_switch_vain(void *data, bool preempt,
+				     struct task_struct *tsk,
+				     unsigned int tsk_state)
+{
+	da_handle_event_srs(tsk, sched_switch_vain_srs);
+}
+
+static void handle_sched_wakeup(void *data, struct task_struct *p)
+{
+	da_handle_event_srs(p, sched_wakeup_srs);
+}
+
+static int enable_srs(void)
+{
+	int retval;
+
+	retval = da_monitor_init_srs();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("srs", sched_set_need_resched_tp, handle_sched_need_resched);
+	rv_attach_trace_probe("srs", sched_set_state_tp, handle_sched_set_state);
+	rv_attach_trace_probe("srs", sched_switch, handle_sched_switch);
+	rv_attach_trace_probe("srs", sched_switch_vain_tp, handle_sched_switch_vain);
+	rv_attach_trace_probe("srs", sched_wakeup, handle_sched_wakeup);
+	rv_attach_trace_probe("srs", sched_entry_tp, handle_schedule_entry);
+
+	return 0;
+}
+
+static void disable_srs(void)
+{
+	rv_srs.enabled = 0;
+
+	rv_detach_trace_probe("srs", sched_set_need_resched_tp, handle_sched_need_resched);
+	rv_detach_trace_probe("srs", sched_set_state_tp, handle_sched_set_state);
+	rv_detach_trace_probe("srs", sched_switch, handle_sched_switch);
+	rv_detach_trace_probe("srs", sched_switch_vain_tp, handle_sched_switch_vain);
+	rv_detach_trace_probe("srs", sched_wakeup, handle_sched_wakeup);
+	rv_detach_trace_probe("srs", sched_entry_tp, handle_schedule_entry);
+
+	da_monitor_destroy_srs();
+}
+
+static struct rv_monitor rv_srs = {
+	.name = "srs",
+	.description = "switch after resched or sleep.",
+	.enable = enable_srs,
+	.disable = disable_srs,
+	.reset = da_monitor_reset_all_srs,
+	.enabled = 0,
+};
+
+static int __init register_srs(void)
+{
+	rv_register_monitor(&rv_srs, &rv_sched);
+	return 0;
+}
+
+static void __exit unregister_srs(void)
+{
+	rv_unregister_monitor(&rv_srs);
+}
+
+module_init(register_srs);
+module_exit(unregister_srs);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
+MODULE_DESCRIPTION("srs: switch after resched or sleep.");
diff --git a/kernel/trace/rv/monitors/srs/srs.h b/kernel/trace/rv/monitors/srs/srs.h
new file mode 100644
index 0000000000000..ce2005880a105
--- /dev/null
+++ b/kernel/trace/rv/monitors/srs/srs.h
@@ -0,0 +1,87 @@ 
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of srs automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+enum states_srs {
+	running_srs = 0,
+	preempted_srs,
+	preempted_sleepable_srs,
+	resched_out_srs,
+	resched_out_sleepable_srs,
+	resched_sleepable_srs,
+	rescheduling_srs,
+	sleepable_srs,
+	sleeping_srs,
+	waking_srs,
+	state_max_srs
+};
+
+#define INVALID_STATE state_max_srs
+
+enum events_srs {
+	sched_need_resched_srs = 0,
+	sched_need_resched_lazy_srs,
+	sched_set_state_runnable_srs,
+	sched_set_state_sleepable_srs,
+	sched_switch_blocking_srs,
+	sched_switch_in_srs,
+	sched_switch_preempt_srs,
+	sched_switch_suspend_srs,
+	sched_switch_vain_srs,
+	sched_switch_yield_srs,
+	sched_wakeup_srs,
+	event_max_srs
+};
+
+struct automaton_srs {
+	char *state_names[state_max_srs];
+	char *event_names[event_max_srs];
+	unsigned char function[state_max_srs][event_max_srs];
+	unsigned char initial_state;
+	bool final_states[state_max_srs];
+};
+
+static const struct automaton_srs automaton_srs = {
+	.state_names = {
+		"running",
+		"preempted",
+		"preempted_sleepable",
+		"resched_out",
+		"resched_out_sleepable",
+		"resched_sleepable",
+		"rescheduling",
+		"sleepable",
+		"sleeping",
+		"waking"
+	},
+	.event_names = {
+		"sched_need_resched",
+		"sched_need_resched_lazy",
+		"sched_set_state_runnable",
+		"sched_set_state_sleepable",
+		"sched_switch_blocking",
+		"sched_switch_in",
+		"sched_switch_preempt",
+		"sched_switch_suspend",
+		"sched_switch_vain",
+		"sched_switch_yield",
+		"sched_wakeup"
+	},
+	.function = {
+		{          rescheduling_srs,          rescheduling_srs,               running_srs,             sleepable_srs,              sleeping_srs,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,               running_srs,             preempted_srs,               running_srs },
+		{           resched_out_srs,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,               running_srs,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE },
+		{ resched_out_sleepable_srs,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             sleepable_srs,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,                waking_srs },
+		{             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,          rescheduling_srs,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE },
+		{             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,     resched_sleepable_srs,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE },
+		{     resched_sleepable_srs,             INVALID_STATE,          rescheduling_srs,     resched_sleepable_srs,              sleeping_srs,             INVALID_STATE,   preempted_sleepable_srs,              sleeping_srs,             sleepable_srs,             INVALID_STATE,          rescheduling_srs },
+		{          rescheduling_srs,             INVALID_STATE,          rescheduling_srs,     resched_sleepable_srs,              sleeping_srs,             INVALID_STATE,             preempted_srs,             INVALID_STATE,               running_srs,             preempted_srs,          rescheduling_srs },
+		{     resched_sleepable_srs,     resched_sleepable_srs,               running_srs,             sleepable_srs,              sleeping_srs,             INVALID_STATE,   preempted_sleepable_srs,              sleeping_srs,             sleepable_srs,             INVALID_STATE,               running_srs },
+		{             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,                waking_srs },
+		{           resched_out_srs,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,               running_srs,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE,             INVALID_STATE },
+	},
+	.initial_state = running_srs,
+	.final_states = { 1, 0, 0, 0, 0, 0, 0, 0, 0, 0 },
+};
diff --git a/kernel/trace/rv/monitors/snroc/snroc_trace.h b/kernel/trace/rv/monitors/srs/srs_trace.h
similarity index 67%
rename from kernel/trace/rv/monitors/snroc/snroc_trace.h
rename to kernel/trace/rv/monitors/srs/srs_trace.h
index 50114cef51229..fd033de926542 100644
--- a/kernel/trace/rv/monitors/snroc/snroc_trace.h
+++ b/kernel/trace/rv/monitors/srs/srs_trace.h
@@ -4,12 +4,12 @@ 
  * Snippet to be included in rv_trace.h
  */
 
-#ifdef CONFIG_RV_MON_SNROC
-DEFINE_EVENT(event_da_monitor_id, event_snroc,
+#ifdef CONFIG_RV_MON_SRS
+DEFINE_EVENT(event_da_monitor_id, event_srs,
 	     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_snroc,
+DEFINE_EVENT(error_da_monitor_id, error_srs,
 	     TP_PROTO(int id, char *state, char *event),
 	     TP_ARGS(id, state, event));
-#endif /* CONFIG_RV_MON_SNROC */
+#endif /* CONFIG_RV_MON_SRS */
diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h
index a5e1c52e29926..f6ead55484751 100644
--- a/kernel/trace/rv/rv_trace.h
+++ b/kernel/trace/rv/rv_trace.h
@@ -123,7 +123,7 @@  DECLARE_EVENT_CLASS(error_da_monitor_id,
 );
 
 #include <monitors/wwnr/wwnr_trace.h>
-#include <monitors/snroc/snroc_trace.h>
+#include <monitors/srs/srs_trace.h>
 // Add new monitors based on CONFIG_DA_MON_EVENTS_ID here
 
 #endif /* CONFIG_DA_MON_EVENTS_ID */
diff --git a/tools/verification/models/sched/snroc.dot b/tools/verification/models/sched/snroc.dot
deleted file mode 100644
index 8b71c32d4dca4..0000000000000
--- a/tools/verification/models/sched/snroc.dot
+++ /dev/null
@@ -1,18 +0,0 @@ 
-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" ];
-	"own_context" [label = "own_context"];
-	"own_context" -> "other_context" [ label = "sched_switch_out" ];
-	"own_context" -> "own_context" [ label = "sched_set_state" ];
-	{ rank = min ;
-		"__init_other_context";
-		"other_context";
-	}
-}
diff --git a/tools/verification/models/sched/srs.dot b/tools/verification/models/sched/srs.dot
new file mode 100644
index 0000000000000..8926e1ab59d98
--- /dev/null
+++ b/tools/verification/models/sched/srs.dot
@@ -0,0 +1,61 @@ 
+digraph state_automaton {
+	center = true;
+	size = "7,11";
+	{node [shape = plaintext, style=invis, label=""] "__init_running"};
+	{node [shape = doublecircle] "running"};
+	{node [shape = circle] "preempted"};
+	{node [shape = circle] "preempted_sleepable"};
+	{node [shape = circle] "resched_out"};
+	{node [shape = circle] "resched_out_sleepable"};
+	{node [shape = circle] "resched_sleepable"};
+	{node [shape = circle] "rescheduling"};
+	{node [shape = circle] "running"};
+	{node [shape = circle] "sleepable"};
+	{node [shape = circle] "sleeping"};
+	{node [shape = circle] "waking"};
+	"__init_running" -> "running";
+	"preempted" [label = "preempted"];
+	"preempted" -> "resched_out" [ label = "sched_need_resched" ];
+	"preempted" -> "running" [ label = "sched_switch_in" ];
+	"preempted_sleepable" [label = "preempted_sleepable"];
+	"preempted_sleepable" -> "resched_out_sleepable" [ label = "sched_need_resched" ];
+	"preempted_sleepable" -> "sleepable" [ label = "sched_switch_in" ];
+	"preempted_sleepable" -> "waking" [ label = "sched_wakeup" ];
+	"resched_out" [label = "resched_out"];
+	"resched_out" -> "rescheduling" [ label = "sched_switch_in" ];
+	"resched_out_sleepable" [label = "resched_out_sleepable"];
+	"resched_out_sleepable" -> "resched_sleepable" [ label = "sched_switch_in" ];
+	"resched_sleepable" [label = "resched_sleepable"];
+	"resched_sleepable" -> "preempted_sleepable" [ label = "sched_switch_preempt" ];
+	"resched_sleepable" -> "resched_sleepable" [ label = "sched_need_resched\nsched_set_state_sleepable" ];
+	"resched_sleepable" -> "rescheduling" [ label = "sched_wakeup\nsched_set_state_runnable" ];
+	"resched_sleepable" -> "sleepable" [ label = "sched_switch_vain" ];
+	"resched_sleepable" -> "sleeping" [ label = "sched_switch_suspend\nsched_switch_blocking" ];
+	"rescheduling" [label = "rescheduling"];
+	"rescheduling" -> "preempted" [ label = "sched_switch_preempt\nsched_switch_yield" ];
+	"rescheduling" -> "resched_sleepable" [ label = "sched_set_state_sleepable" ];
+	"rescheduling" -> "rescheduling" [ label = "sched_need_resched\nsched_wakeup\nsched_set_state_runnable" ];
+	"rescheduling" -> "running" [ label = "sched_switch_vain" ];
+	"rescheduling" -> "sleeping" [ label = "sched_switch_blocking" ];
+	"running" [label = "running", color = green3];
+	"running" -> "preempted" [ label = "sched_switch_yield" ];
+	"running" -> "rescheduling" [ label = "sched_need_resched\nsched_need_resched_lazy" ];
+	"running" -> "running" [ label = "sched_set_state_runnable\nsched_wakeup\nsched_switch_vain" ];
+	"running" -> "sleepable" [ label = "sched_set_state_sleepable" ];
+	"running" -> "sleeping" [ label = "sched_switch_blocking" ];
+	"sleepable" [label = "sleepable"];
+	"sleepable" -> "preempted_sleepable" [ label = "sched_switch_preempt" ];
+	"sleepable" -> "resched_sleepable" [ label = "sched_need_resched\nsched_need_resched_lazy" ];
+	"sleepable" -> "running" [ label = "sched_set_state_runnable\nsched_wakeup" ];
+	"sleepable" -> "sleepable" [ label = "sched_set_state_sleepable\nsched_switch_vain" ];
+	"sleepable" -> "sleeping" [ label = "sched_switch_suspend\nsched_switch_blocking" ];
+	"sleeping" [label = "sleeping"];
+	"sleeping" -> "waking" [ label = "sched_wakeup" ];
+	"waking" [label = "waking"];
+	"waking" -> "resched_out" [ label = "sched_need_resched" ];
+	"waking" -> "running" [ label = "sched_switch_in" ];
+	{ rank = min ;
+		"__init_running";
+		"running";
+	}
+}