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).
Also adapt the set_state handler prototypes to the tracepoint change.
Cc: Ingo Molnar <mi...@redhat.com>
Cc: Peter Zijlstra <pet...@infradead.org>
Signed-off-by: Gabriele Monaco <gmon...@redhat.com>
---
Documentation/trace/rv/monitor_sched.rst | 32 ++++++++++++-----------
kernel/trace/rv/monitors/snroc/snroc.c | 12 ++++++++-
kernel/trace/rv/monitors/snroc/snroc.h | 8 +++---
tools/verification/models/sched/snroc.dot | 2 +-
4 files changed, 34 insertions(+), 20 deletions(-)
diff --git a/Documentation/trace/rv/monitor_sched.rst
b/Documentation/trace/rv/monitor_sched.rst
index 6f76bba94d9f..5cb58ac441d8 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 540e686e699f..11a56b58665e 100644
--- a/kernel/trace/rv/monitors/snroc/snroc.c
+++ b/kernel/trace/rv/monitors/snroc/snroc.c
@@ -19,7 +19,8 @@
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)
+static void handle_sched_set_state(void *data, struct task_struct *tsk,
+ int state, bool from_signal)
{
da_handle_event_snroc(tsk, sched_set_state_snroc);
}
@@ -33,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;
@@ -43,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;
}
@@ -53,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 c3650a2b1b10..d6de40e15ae1 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,11 +37,12 @@ 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 },
- { own_context_snroc, INVALID_STATE, other_context_snroc },
+ { INVALID_STATE, own_context_snroc,
INVALID_STATE, INVALID_STATE },
+ { own_context_snroc, INVALID_STATE,
other_context_snroc, own_context_snroc },
},
.initial_state = other_context_snroc,
.final_states = { 1, 0 },
diff --git a/tools/verification/models/sched/snroc.dot
b/tools/verification/models/sched/snroc.dot
index 8b71c32d4dca..5b1a787d0350 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.49.0
