The snroc monitor ensures changes in a task state happens only in the
respective task's context. This is the only monitor enforcing a task
is to be switched in after being switched out, and vice-versa.
Although this is a trivial claim, it is useful to complete other claims
on when scheduling is possible while keeping models simple.
Add the sched_switch_vain event to the model, enforcing that a vain
switch doesn't change the context but can only occur while a task is
running (e.g. a call to schedule that re-selects the current task).
Cc: Ingo Molnar <mingo@xxxxxxxxxx>
Cc: Peter Zijlstra <peterz@xxxxxxxxxxxxx>
Signed-off-by: Gabriele Monaco <gmonaco@xxxxxxxxxx>
---
Documentation/trace/rv/monitor_sched.rst | 32 ++++++++++++-----------
kernel/trace/rv/monitors/snroc/snroc.c | 9 +++++++
kernel/trace/rv/monitors/snroc/snroc.h | 8 ++++--
tools/verification/models/sched/snroc.dot | 2 +-
4 files changed, 33 insertions(+), 18 deletions(-)
diff --git a/Documentation/trace/rv/monitor_sched.rst b/Documentation/trace/rv/monitor_sched.rst
index 6f76bba94d9fb..5cb58ac441d83 100644
--- a/Documentation/trace/rv/monitor_sched.rst
+++ b/Documentation/trace/rv/monitor_sched.rst
@@ -89,21 +89,23 @@ 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. A task is in its own context after switching in and leaves the context
+when switched out, a vain switch maintains the context::
+
+ |
+ |
+ v
+ +------------------+
+ | other_context | <+
+ +------------------+ |
+ | |
+ | sched_switch_in | sched_switch_out
+ v |
+ sched_set_state |
+ sched_switch_vain |
+ +-------------------- own_context |
+ | |
+ +-------------------> -+
Monitor scpd
~~~~~~~~~~~~
diff --git a/kernel/trace/rv/monitors/snroc/snroc.c b/kernel/trace/rv/monitors/snroc/snroc.c
index 2651f589d1554..11a56b58665e7 100644
--- a/kernel/trace/rv/monitors/snroc/snroc.c
+++ b/kernel/trace/rv/monitors/snroc/snroc.c
@@ -34,6 +34,13 @@ static void handle_sched_switch(void *data, bool preempt,
da_handle_event_snroc(next, sched_switch_in_snroc);
}
+static void handle_sched_switch_vain(void *data, bool preempt,
+ struct task_struct *tsk,
+ unsigned int tsk_state)
+{
+ da_handle_event_snroc(tsk, sched_switch_vain_snroc);
+}
+
static int enable_snroc(void)
{
int retval;
@@ -44,6 +51,7 @@ static int enable_snroc(void)
rv_attach_trace_probe("snroc", sched_set_state_tp, handle_sched_set_state);
rv_attach_trace_probe("snroc", sched_switch, handle_sched_switch);
+ rv_attach_trace_probe("snroc", sched_switch_vain_tp, handle_sched_switch_vain);
return 0;
}
@@ -54,6 +62,7 @@ static void disable_snroc(void)
rv_detach_trace_probe("snroc", sched_set_state_tp, handle_sched_set_state);
rv_detach_trace_probe("snroc", sched_switch, handle_sched_switch);
+ rv_detach_trace_probe("snroc", sched_switch_vain_tp, handle_sched_switch_vain);
da_monitor_destroy_snroc();
}
diff --git a/kernel/trace/rv/monitors/snroc/snroc.h b/kernel/trace/rv/monitors/snroc/snroc.h
index be46f7b9ebb87..064d98fb9796d 100644
--- a/kernel/trace/rv/monitors/snroc/snroc.h
+++ b/kernel/trace/rv/monitors/snroc/snroc.h
@@ -17,6 +17,7 @@ enum events_snroc {
sched_set_state_snroc = 0,
sched_switch_in_snroc,
sched_switch_out_snroc,
+ sched_switch_vain_snroc,
event_max_snroc
};
@@ -36,18 +37,21 @@ static const struct automaton_snroc automaton_snroc = {
.event_names = {
"sched_set_state",
"sched_switch_in",
- "sched_switch_out"
+ "sched_switch_out",
+ "sched_switch_vain"
},
.function = {
{
INVALID_STATE,
own_context_snroc,
+ INVALID_STATE,
INVALID_STATE
},
{
own_context_snroc,
INVALID_STATE,
- other_context_snroc
+ other_context_snroc,
+ own_context_snroc
},
},
.initial_state = other_context_snroc,
diff --git a/tools/verification/models/sched/snroc.dot b/tools/verification/models/sched/snroc.dot
index 8b71c32d4dca4..5b1a787d0350b 100644
--- a/tools/verification/models/sched/snroc.dot
+++ b/tools/verification/models/sched/snroc.dot
@@ -10,7 +10,7 @@ digraph state_automaton {
"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" ];
+ "own_context" -> "own_context" [ label = "sched_set_state\nsched_switch_vain" ];
{ rank = min ;
"__init_other_context";
"other_context";
--
2.50.1
