tjh.dev
Linux kernel mirror (for testing)
git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
kernel
os
linux
rv: Add scpd, snep and sncid per-cpu monitors
Add 3 per-cpu monitors as part of the sched model:
* scpd: schedule called with preemption disabled
Monitor to ensure schedule is called with preemption disabled
* snep: schedule does not enable preempt
Monitor to ensure schedule does not enable preempt
* sncid: schedule not called with interrupt disabled
Monitor to ensure schedule is not called with interrupt disabled
To: Ingo Molnar <mingo@redhat.com>
To: Peter Zijlstra <peterz@infradead.org>
Cc: Juri Lelli <juri.lelli@redhat.com>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: John Kacur <jkacur@redhat.com>
Cc: Clark Williams <williams@redhat.com>
Link: https://lore.kernel.org/20250305140406.350227-6-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
authored by
Gabriele Monaco
and committed by
Steven Rostedt (Google)
fbe6c09b
93bac9cf
+588
+3
kernel/trace/rv/Kconfig
+3
kernel/trace/rv/Kconfig
···
31
31
source "kernel/trace/rv/monitors/tss/Kconfig"
32
32
source "kernel/trace/rv/monitors/sco/Kconfig"
33
33
source "kernel/trace/rv/monitors/snroc/Kconfig"
34
+
source "kernel/trace/rv/monitors/scpd/Kconfig"
35
+
source "kernel/trace/rv/monitors/snep/Kconfig"
36
+
source "kernel/trace/rv/monitors/sncid/Kconfig"
34
37
# Add new monitors here
35
38
36
39
config RV_REACTORS
+3
kernel/trace/rv/Makefile
+3
kernel/trace/rv/Makefile
···
9
9
obj-$(CONFIG_RV_MON_TSS) += monitors/tss/tss.o
10
10
obj-$(CONFIG_RV_MON_SCO) += monitors/sco/sco.o
11
11
obj-$(CONFIG_RV_MON_SNROC) += monitors/snroc/snroc.o
12
+
obj-$(CONFIG_RV_MON_SCPD) += monitors/scpd/scpd.o
13
+
obj-$(CONFIG_RV_MON_SNEP) += monitors/snep/snep.o
14
+
obj-$(CONFIG_RV_MON_SNCID) += monitors/sncid/sncid.o
12
15
# Add new monitors here
13
16
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
14
17
obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
+15
kernel/trace/rv/monitors/scpd/Kconfig
+15
kernel/trace/rv/monitors/scpd/Kconfig
···
1
+
# SPDX-License-Identifier: GPL-2.0-only
2
+
#
3
+
config RV_MON_SCPD
4
+
depends on RV
5
+
depends on PREEMPT_TRACER
6
+
depends on RV_MON_SCHED
7
+
default y
8
+
select DA_MON_EVENTS_IMPLICIT
9
+
bool "scpd monitor"
10
+
help
11
+
Monitor to ensure schedule is called with preemption disabled.
12
+
This monitor is part of the sched monitors collection.
13
+
14
+
For further information, see:
15
+
Documentation/trace/rv/monitor_sched.rst
+96
kernel/trace/rv/monitors/scpd/scpd.c
+96
kernel/trace/rv/monitors/scpd/scpd.c
···
1
+
// SPDX-License-Identifier: GPL-2.0
2
+
#include <linux/ftrace.h>
3
+
#include <linux/tracepoint.h>
4
+
#include <linux/kernel.h>
5
+
#include <linux/module.h>
6
+
#include <linux/init.h>
7
+
#include <linux/rv.h>
8
+
#include <rv/instrumentation.h>
9
+
#include <rv/da_monitor.h>
10
+
11
+
#define MODULE_NAME "scpd"
12
+
13
+
#include <trace/events/sched.h>
14
+
#include <trace/events/preemptirq.h>
15
+
#include <rv_trace.h>
16
+
#include <monitors/sched/sched.h>
17
+
18
+
#include "scpd.h"
19
+
20
+
static struct rv_monitor rv_scpd;
21
+
DECLARE_DA_MON_PER_CPU(scpd, unsigned char);
22
+
23
+
static void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
24
+
{
25
+
da_handle_event_scpd(preempt_disable_scpd);
26
+
}
27
+
28
+
static void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
29
+
{
30
+
da_handle_start_event_scpd(preempt_enable_scpd);
31
+
}
32
+
33
+
static void handle_schedule_entry(void *data, bool preempt, unsigned long ip)
34
+
{
35
+
da_handle_event_scpd(schedule_entry_scpd);
36
+
}
37
+
38
+
static void handle_schedule_exit(void *data, bool is_switch, unsigned long ip)
39
+
{
40
+
da_handle_event_scpd(schedule_exit_scpd);
41
+
}
42
+
43
+
static int enable_scpd(void)
44
+
{
45
+
int retval;
46
+
47
+
retval = da_monitor_init_scpd();
48
+
if (retval)
49
+
return retval;
50
+
51
+
rv_attach_trace_probe("scpd", preempt_disable, handle_preempt_disable);
52
+
rv_attach_trace_probe("scpd", preempt_enable, handle_preempt_enable);
53
+
rv_attach_trace_probe("scpd", sched_entry_tp, handle_schedule_entry);
54
+
rv_attach_trace_probe("scpd", sched_exit_tp, handle_schedule_exit);
55
+
56
+
return 0;
57
+
}
58
+
59
+
static void disable_scpd(void)
60
+
{
61
+
rv_scpd.enabled = 0;
62
+
63
+
rv_detach_trace_probe("scpd", preempt_disable, handle_preempt_disable);
64
+
rv_detach_trace_probe("scpd", preempt_enable, handle_preempt_enable);
65
+
rv_detach_trace_probe("scpd", sched_entry_tp, handle_schedule_entry);
66
+
rv_detach_trace_probe("scpd", sched_exit_tp, handle_schedule_exit);
67
+
68
+
da_monitor_destroy_scpd();
69
+
}
70
+
71
+
static struct rv_monitor rv_scpd = {
72
+
.name = "scpd",
73
+
.description = "schedule called with preemption disabled.",
74
+
.enable = enable_scpd,
75
+
.disable = disable_scpd,
76
+
.reset = da_monitor_reset_all_scpd,
77
+
.enabled = 0,
78
+
};
79
+
80
+
static int __init register_scpd(void)
81
+
{
82
+
rv_register_monitor(&rv_scpd, &rv_sched);
83
+
return 0;
84
+
}
85
+
86
+
static void __exit unregister_scpd(void)
87
+
{
88
+
rv_unregister_monitor(&rv_scpd);
89
+
}
90
+
91
+
module_init(register_scpd);
92
+
module_exit(unregister_scpd);
93
+
94
+
MODULE_LICENSE("GPL");
95
+
MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
96
+
MODULE_DESCRIPTION("scpd: schedule called with preemption disabled.");
+49
kernel/trace/rv/monitors/scpd/scpd.h
+49
kernel/trace/rv/monitors/scpd/scpd.h
···
1
+
/* SPDX-License-Identifier: GPL-2.0 */
2
+
/*
3
+
* Automatically generated C representation of scpd automaton
4
+
* For further information about this format, see kernel documentation:
5
+
* Documentation/trace/rv/deterministic_automata.rst
6
+
*/
7
+
8
+
enum states_scpd {
9
+
cant_sched_scpd = 0,
10
+
can_sched_scpd,
11
+
state_max_scpd
12
+
};
13
+
14
+
#define INVALID_STATE state_max_scpd
15
+
16
+
enum events_scpd {
17
+
preempt_disable_scpd = 0,
18
+
preempt_enable_scpd,
19
+
schedule_entry_scpd,
20
+
schedule_exit_scpd,
21
+
event_max_scpd
22
+
};
23
+
24
+
struct automaton_scpd {
25
+
char *state_names[state_max_scpd];
26
+
char *event_names[event_max_scpd];
27
+
unsigned char function[state_max_scpd][event_max_scpd];
28
+
unsigned char initial_state;
29
+
bool final_states[state_max_scpd];
30
+
};
31
+
32
+
static const struct automaton_scpd automaton_scpd = {
33
+
.state_names = {
34
+
"cant_sched",
35
+
"can_sched"
36
+
},
37
+
.event_names = {
38
+
"preempt_disable",
39
+
"preempt_enable",
40
+
"schedule_entry",
41
+
"schedule_exit"
42
+
},
43
+
.function = {
44
+
{ can_sched_scpd, INVALID_STATE, INVALID_STATE, INVALID_STATE },
45
+
{ INVALID_STATE, cant_sched_scpd, can_sched_scpd, can_sched_scpd },
46
+
},
47
+
.initial_state = cant_sched_scpd,
48
+
.final_states = { 1, 0 },
49
+
};
+15
kernel/trace/rv/monitors/scpd/scpd_trace.h
+15
kernel/trace/rv/monitors/scpd/scpd_trace.h
···
1
+
/* SPDX-License-Identifier: GPL-2.0 */
2
+
3
+
/*
4
+
* Snippet to be included in rv_trace.h
5
+
*/
6
+
7
+
#ifdef CONFIG_RV_MON_SCPD
8
+
DEFINE_EVENT(event_da_monitor, event_scpd,
9
+
TP_PROTO(char *state, char *event, char *next_state, bool final_state),
10
+
TP_ARGS(state, event, next_state, final_state));
11
+
12
+
DEFINE_EVENT(error_da_monitor, error_scpd,
13
+
TP_PROTO(char *state, char *event),
14
+
TP_ARGS(state, event));
15
+
#endif /* CONFIG_RV_MON_SCPD */
+15
kernel/trace/rv/monitors/sncid/Kconfig
+15
kernel/trace/rv/monitors/sncid/Kconfig
···
1
+
# SPDX-License-Identifier: GPL-2.0-only
2
+
#
3
+
config RV_MON_SNCID
4
+
depends on RV
5
+
depends on IRQSOFF_TRACER
6
+
depends on RV_MON_SCHED
7
+
default y
8
+
select DA_MON_EVENTS_IMPLICIT
9
+
bool "sncid monitor"
10
+
help
11
+
Monitor to ensure schedule is not called with interrupt disabled.
12
+
This monitor is part of the sched monitors collection.
13
+
14
+
For further information, see:
15
+
Documentation/trace/rv/monitor_sched.rst
+96
kernel/trace/rv/monitors/sncid/sncid.c
+96
kernel/trace/rv/monitors/sncid/sncid.c
···
1
+
// SPDX-License-Identifier: GPL-2.0
2
+
#include <linux/ftrace.h>
3
+
#include <linux/tracepoint.h>
4
+
#include <linux/kernel.h>
5
+
#include <linux/module.h>
6
+
#include <linux/init.h>
7
+
#include <linux/rv.h>
8
+
#include <rv/instrumentation.h>
9
+
#include <rv/da_monitor.h>
10
+
11
+
#define MODULE_NAME "sncid"
12
+
13
+
#include <trace/events/sched.h>
14
+
#include <trace/events/preemptirq.h>
15
+
#include <rv_trace.h>
16
+
#include <monitors/sched/sched.h>
17
+
18
+
#include "sncid.h"
19
+
20
+
static struct rv_monitor rv_sncid;
21
+
DECLARE_DA_MON_PER_CPU(sncid, unsigned char);
22
+
23
+
static void handle_irq_disable(void *data, unsigned long ip, unsigned long parent_ip)
24
+
{
25
+
da_handle_event_sncid(irq_disable_sncid);
26
+
}
27
+
28
+
static void handle_irq_enable(void *data, unsigned long ip, unsigned long parent_ip)
29
+
{
30
+
da_handle_start_event_sncid(irq_enable_sncid);
31
+
}
32
+
33
+
static void handle_schedule_entry(void *data, bool preempt, unsigned long ip)
34
+
{
35
+
da_handle_start_event_sncid(schedule_entry_sncid);
36
+
}
37
+
38
+
static void handle_schedule_exit(void *data, bool is_switch, unsigned long ip)
39
+
{
40
+
da_handle_start_event_sncid(schedule_exit_sncid);
41
+
}
42
+
43
+
static int enable_sncid(void)
44
+
{
45
+
int retval;
46
+
47
+
retval = da_monitor_init_sncid();
48
+
if (retval)
49
+
return retval;
50
+
51
+
rv_attach_trace_probe("sncid", irq_disable, handle_irq_disable);
52
+
rv_attach_trace_probe("sncid", irq_enable, handle_irq_enable);
53
+
rv_attach_trace_probe("sncid", sched_entry_tp, handle_schedule_entry);
54
+
rv_attach_trace_probe("sncid", sched_exit_tp, handle_schedule_exit);
55
+
56
+
return 0;
57
+
}
58
+
59
+
static void disable_sncid(void)
60
+
{
61
+
rv_sncid.enabled = 0;
62
+
63
+
rv_detach_trace_probe("sncid", irq_disable, handle_irq_disable);
64
+
rv_detach_trace_probe("sncid", irq_enable, handle_irq_enable);
65
+
rv_detach_trace_probe("sncid", sched_entry_tp, handle_schedule_entry);
66
+
rv_detach_trace_probe("sncid", sched_exit_tp, handle_schedule_exit);
67
+
68
+
da_monitor_destroy_sncid();
69
+
}
70
+
71
+
static struct rv_monitor rv_sncid = {
72
+
.name = "sncid",
73
+
.description = "schedule not called with interrupt disabled.",
74
+
.enable = enable_sncid,
75
+
.disable = disable_sncid,
76
+
.reset = da_monitor_reset_all_sncid,
77
+
.enabled = 0,
78
+
};
79
+
80
+
static int __init register_sncid(void)
81
+
{
82
+
rv_register_monitor(&rv_sncid, &rv_sched);
83
+
return 0;
84
+
}
85
+
86
+
static void __exit unregister_sncid(void)
87
+
{
88
+
rv_unregister_monitor(&rv_sncid);
89
+
}
90
+
91
+
module_init(register_sncid);
92
+
module_exit(unregister_sncid);
93
+
94
+
MODULE_LICENSE("GPL");
95
+
MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
96
+
MODULE_DESCRIPTION("sncid: schedule not called with interrupt disabled.");
+49
kernel/trace/rv/monitors/sncid/sncid.h
+49
kernel/trace/rv/monitors/sncid/sncid.h
···
1
+
/* SPDX-License-Identifier: GPL-2.0 */
2
+
/*
3
+
* Automatically generated C representation of sncid automaton
4
+
* For further information about this format, see kernel documentation:
5
+
* Documentation/trace/rv/deterministic_automata.rst
6
+
*/
7
+
8
+
enum states_sncid {
9
+
can_sched_sncid = 0,
10
+
cant_sched_sncid,
11
+
state_max_sncid
12
+
};
13
+
14
+
#define INVALID_STATE state_max_sncid
15
+
16
+
enum events_sncid {
17
+
irq_disable_sncid = 0,
18
+
irq_enable_sncid,
19
+
schedule_entry_sncid,
20
+
schedule_exit_sncid,
21
+
event_max_sncid
22
+
};
23
+
24
+
struct automaton_sncid {
25
+
char *state_names[state_max_sncid];
26
+
char *event_names[event_max_sncid];
27
+
unsigned char function[state_max_sncid][event_max_sncid];
28
+
unsigned char initial_state;
29
+
bool final_states[state_max_sncid];
30
+
};
31
+
32
+
static const struct automaton_sncid automaton_sncid = {
33
+
.state_names = {
34
+
"can_sched",
35
+
"cant_sched"
36
+
},
37
+
.event_names = {
38
+
"irq_disable",
39
+
"irq_enable",
40
+
"schedule_entry",
41
+
"schedule_exit"
42
+
},
43
+
.function = {
44
+
{ cant_sched_sncid, INVALID_STATE, can_sched_sncid, can_sched_sncid },
45
+
{ INVALID_STATE, can_sched_sncid, INVALID_STATE, INVALID_STATE },
46
+
},
47
+
.initial_state = can_sched_sncid,
48
+
.final_states = { 1, 0 },
49
+
};
+15
kernel/trace/rv/monitors/sncid/sncid_trace.h
+15
kernel/trace/rv/monitors/sncid/sncid_trace.h
···
1
+
/* SPDX-License-Identifier: GPL-2.0 */
2
+
3
+
/*
4
+
* Snippet to be included in rv_trace.h
5
+
*/
6
+
7
+
#ifdef CONFIG_RV_MON_SNCID
8
+
DEFINE_EVENT(event_da_monitor, event_sncid,
9
+
TP_PROTO(char *state, char *event, char *next_state, bool final_state),
10
+
TP_ARGS(state, event, next_state, final_state));
11
+
12
+
DEFINE_EVENT(error_da_monitor, error_sncid,
13
+
TP_PROTO(char *state, char *event),
14
+
TP_ARGS(state, event));
15
+
#endif /* CONFIG_RV_MON_SNCID */
+15
kernel/trace/rv/monitors/snep/Kconfig
+15
kernel/trace/rv/monitors/snep/Kconfig
···
1
+
# SPDX-License-Identifier: GPL-2.0-only
2
+
#
3
+
config RV_MON_SNEP
4
+
depends on RV
5
+
depends on PREEMPT_TRACER
6
+
depends on RV_MON_SCHED
7
+
default y
8
+
select DA_MON_EVENTS_IMPLICIT
9
+
bool "snep monitor"
10
+
help
11
+
Monitor to ensure schedule does not enable preempt.
12
+
This monitor is part of the sched monitors collection.
13
+
14
+
For further information, see:
15
+
Documentation/trace/rv/monitor_sched.rst
+96
kernel/trace/rv/monitors/snep/snep.c
+96
kernel/trace/rv/monitors/snep/snep.c
···
1
+
// SPDX-License-Identifier: GPL-2.0
2
+
#include <linux/ftrace.h>
3
+
#include <linux/tracepoint.h>
4
+
#include <linux/kernel.h>
5
+
#include <linux/module.h>
6
+
#include <linux/init.h>
7
+
#include <linux/rv.h>
8
+
#include <rv/instrumentation.h>
9
+
#include <rv/da_monitor.h>
10
+
11
+
#define MODULE_NAME "snep"
12
+
13
+
#include <trace/events/sched.h>
14
+
#include <trace/events/preemptirq.h>
15
+
#include <rv_trace.h>
16
+
#include <monitors/sched/sched.h>
17
+
18
+
#include "snep.h"
19
+
20
+
static struct rv_monitor rv_snep;
21
+
DECLARE_DA_MON_PER_CPU(snep, unsigned char);
22
+
23
+
static void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
24
+
{
25
+
da_handle_start_event_snep(preempt_disable_snep);
26
+
}
27
+
28
+
static void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
29
+
{
30
+
da_handle_start_event_snep(preempt_enable_snep);
31
+
}
32
+
33
+
static void handle_schedule_entry(void *data, bool preempt, unsigned long ip)
34
+
{
35
+
da_handle_event_snep(schedule_entry_snep);
36
+
}
37
+
38
+
static void handle_schedule_exit(void *data, bool is_switch, unsigned long ip)
39
+
{
40
+
da_handle_start_event_snep(schedule_exit_snep);
41
+
}
42
+
43
+
static int enable_snep(void)
44
+
{
45
+
int retval;
46
+
47
+
retval = da_monitor_init_snep();
48
+
if (retval)
49
+
return retval;
50
+
51
+
rv_attach_trace_probe("snep", preempt_disable, handle_preempt_disable);
52
+
rv_attach_trace_probe("snep", preempt_enable, handle_preempt_enable);
53
+
rv_attach_trace_probe("snep", sched_entry_tp, handle_schedule_entry);
54
+
rv_attach_trace_probe("snep", sched_exit_tp, handle_schedule_exit);
55
+
56
+
return 0;
57
+
}
58
+
59
+
static void disable_snep(void)
60
+
{
61
+
rv_snep.enabled = 0;
62
+
63
+
rv_detach_trace_probe("snep", preempt_disable, handle_preempt_disable);
64
+
rv_detach_trace_probe("snep", preempt_enable, handle_preempt_enable);
65
+
rv_detach_trace_probe("snep", sched_entry_tp, handle_schedule_entry);
66
+
rv_detach_trace_probe("snep", sched_exit_tp, handle_schedule_exit);
67
+
68
+
da_monitor_destroy_snep();
69
+
}
70
+
71
+
static struct rv_monitor rv_snep = {
72
+
.name = "snep",
73
+
.description = "schedule does not enable preempt.",
74
+
.enable = enable_snep,
75
+
.disable = disable_snep,
76
+
.reset = da_monitor_reset_all_snep,
77
+
.enabled = 0,
78
+
};
79
+
80
+
static int __init register_snep(void)
81
+
{
82
+
rv_register_monitor(&rv_snep, &rv_sched);
83
+
return 0;
84
+
}
85
+
86
+
static void __exit unregister_snep(void)
87
+
{
88
+
rv_unregister_monitor(&rv_snep);
89
+
}
90
+
91
+
module_init(register_snep);
92
+
module_exit(unregister_snep);
93
+
94
+
MODULE_LICENSE("GPL");
95
+
MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
96
+
MODULE_DESCRIPTION("snep: schedule does not enable preempt.");
+49
kernel/trace/rv/monitors/snep/snep.h
+49
kernel/trace/rv/monitors/snep/snep.h
···
1
+
/* SPDX-License-Identifier: GPL-2.0 */
2
+
/*
3
+
* Automatically generated C representation of snep automaton
4
+
* For further information about this format, see kernel documentation:
5
+
* Documentation/trace/rv/deterministic_automata.rst
6
+
*/
7
+
8
+
enum states_snep {
9
+
non_scheduling_context_snep = 0,
10
+
scheduling_contex_snep,
11
+
state_max_snep
12
+
};
13
+
14
+
#define INVALID_STATE state_max_snep
15
+
16
+
enum events_snep {
17
+
preempt_disable_snep = 0,
18
+
preempt_enable_snep,
19
+
schedule_entry_snep,
20
+
schedule_exit_snep,
21
+
event_max_snep
22
+
};
23
+
24
+
struct automaton_snep {
25
+
char *state_names[state_max_snep];
26
+
char *event_names[event_max_snep];
27
+
unsigned char function[state_max_snep][event_max_snep];
28
+
unsigned char initial_state;
29
+
bool final_states[state_max_snep];
30
+
};
31
+
32
+
static const struct automaton_snep automaton_snep = {
33
+
.state_names = {
34
+
"non_scheduling_context",
35
+
"scheduling_contex"
36
+
},
37
+
.event_names = {
38
+
"preempt_disable",
39
+
"preempt_enable",
40
+
"schedule_entry",
41
+
"schedule_exit"
42
+
},
43
+
.function = {
44
+
{ non_scheduling_context_snep, non_scheduling_context_snep, scheduling_contex_snep, INVALID_STATE },
45
+
{ INVALID_STATE, INVALID_STATE, INVALID_STATE, non_scheduling_context_snep },
46
+
},
47
+
.initial_state = non_scheduling_context_snep,
48
+
.final_states = { 1, 0 },
49
+
};
+15
kernel/trace/rv/monitors/snep/snep_trace.h
+15
kernel/trace/rv/monitors/snep/snep_trace.h
···
1
+
/* SPDX-License-Identifier: GPL-2.0 */
2
+
3
+
/*
4
+
* Snippet to be included in rv_trace.h
5
+
*/
6
+
7
+
#ifdef CONFIG_RV_MON_SNEP
8
+
DEFINE_EVENT(event_da_monitor, event_snep,
9
+
TP_PROTO(char *state, char *event, char *next_state, bool final_state),
10
+
TP_ARGS(state, event, next_state, final_state));
11
+
12
+
DEFINE_EVENT(error_da_monitor, error_snep,
13
+
TP_PROTO(char *state, char *event),
14
+
TP_ARGS(state, event));
15
+
#endif /* CONFIG_RV_MON_SNEP */
+3
kernel/trace/rv/rv_trace.h
+3
kernel/trace/rv/rv_trace.h
···
60
60
#include <monitors/wip/wip_trace.h>
61
61
#include <monitors/tss/tss_trace.h>
62
62
#include <monitors/sco/sco_trace.h>
63
+
#include <monitors/scpd/scpd_trace.h>
64
+
#include <monitors/snep/snep_trace.h>
65
+
#include <monitors/sncid/sncid_trace.h>
63
66
// Add new monitors based on CONFIG_DA_MON_EVENTS_IMPLICIT here
64
67
65
68
#endif /* CONFIG_DA_MON_EVENTS_IMPLICIT */
+18
tools/verification/models/sched/scpd.dot
+18
tools/verification/models/sched/scpd.dot
···
1
+
digraph state_automaton {
2
+
center = true;
3
+
size = "7,11";
4
+
{node [shape = plaintext] "can_sched"};
5
+
{node [shape = plaintext, style=invis, label=""] "__init_cant_sched"};
6
+
{node [shape = ellipse] "cant_sched"};
7
+
{node [shape = plaintext] "cant_sched"};
8
+
"__init_cant_sched" -> "cant_sched";
9
+
"can_sched" [label = "can_sched"];
10
+
"can_sched" -> "can_sched" [ label = "schedule_entry\nschedule_exit" ];
11
+
"can_sched" -> "cant_sched" [ label = "preempt_enable" ];
12
+
"cant_sched" [label = "cant_sched", color = green3];
13
+
"cant_sched" -> "can_sched" [ label = "preempt_disable" ];
14
+
{ rank = min ;
15
+
"__init_cant_sched";
16
+
"cant_sched";
17
+
}
18
+
}
+18
tools/verification/models/sched/sncid.dot
+18
tools/verification/models/sched/sncid.dot
···
1
+
digraph state_automaton {
2
+
center = true;
3
+
size = "7,11";
4
+
{node [shape = plaintext, style=invis, label=""] "__init_can_sched"};
5
+
{node [shape = ellipse] "can_sched"};
6
+
{node [shape = plaintext] "can_sched"};
7
+
{node [shape = plaintext] "cant_sched"};
8
+
"__init_can_sched" -> "can_sched";
9
+
"can_sched" [label = "can_sched", color = green3];
10
+
"can_sched" -> "can_sched" [ label = "schedule_entry\nschedule_exit" ];
11
+
"can_sched" -> "cant_sched" [ label = "irq_disable" ];
12
+
"cant_sched" [label = "cant_sched"];
13
+
"cant_sched" -> "can_sched" [ label = "irq_enable" ];
14
+
{ rank = min ;
15
+
"__init_can_sched";
16
+
"can_sched";
17
+
}
18
+
}
+18
tools/verification/models/sched/snep.dot
+18
tools/verification/models/sched/snep.dot
···
1
+
digraph state_automaton {
2
+
center = true;
3
+
size = "7,11";
4
+
{node [shape = plaintext, style=invis, label=""] "__init_non_scheduling_context"};
5
+
{node [shape = ellipse] "non_scheduling_context"};
6
+
{node [shape = plaintext] "non_scheduling_context"};
7
+
{node [shape = plaintext] "scheduling_contex"};
8
+
"__init_non_scheduling_context" -> "non_scheduling_context";
9
+
"non_scheduling_context" [label = "non_scheduling_context", color = green3];
10
+
"non_scheduling_context" -> "non_scheduling_context" [ label = "preempt_disable\npreempt_enable" ];
11
+
"non_scheduling_context" -> "scheduling_contex" [ label = "schedule_entry" ];
12
+
"scheduling_contex" [label = "scheduling_contex"];
13
+
"scheduling_contex" -> "non_scheduling_context" [ label = "schedule_exit" ];
14
+
{ rank = min ;
15
+
"__init_non_scheduling_context";
16
+
"non_scheduling_context";
17
+
}
18
+
}