Skip to content

Commit 10bde81

Browse files
Daniel Bristot de Oliveirarostedt
Daniel Bristot de Oliveira
authored and
rostedt
committed
rv/monitor: Add the wip monitor
The wakeup in preemptive (wip) monitor verifies if the wakeup events always take place with preemption disabled: | | v #==================# H preemptive H <+ #==================# | | | | preempt_disable | preempt_enable v | sched_waking +------------------+ | +--------------- | | | | | non_preemptive | | +--------------> | | -+ +------------------+ The wakeup event always takes place with preemption disabled because of the scheduler synchronization. However, because the preempt_count and its trace event are not atomic with regard to interrupts, some inconsistencies might happen. The documentation illustrates one of these cases. Link: https://lkml.kernel.org/r/c98ca678df81115fddc04921b3c79720c836b18f.1659052063.git.bristot@kernel.org Cc: Wim Van Sebroeck <[email protected]> Cc: Guenter Roeck <[email protected]> Cc: Jonathan Corbet <[email protected]> Cc: Ingo Molnar <[email protected]> Cc: Thomas Gleixner <[email protected]> Cc: Peter Zijlstra <[email protected]> Cc: Will Deacon <[email protected]> Cc: Catalin Marinas <[email protected]> Cc: Marco Elver <[email protected]> Cc: Dmitry Vyukov <[email protected]> Cc: "Paul E. McKenney" <[email protected]> Cc: Shuah Khan <[email protected]> Cc: Gabriele Paoloni <[email protected]> Cc: Juri Lelli <[email protected]> Cc: Clark Williams <[email protected]> Cc: Tao Zhou <[email protected]> Cc: Randy Dunlap <[email protected]> Cc: [email protected] Cc: [email protected] Cc: [email protected] Signed-off-by: Daniel Bristot de Oliveira <[email protected]> Signed-off-by: Steven Rostedt (Google) <[email protected]>
1 parent 8812d21 commit 10bde81

File tree

7 files changed

+111
-36
lines changed

7 files changed

+111
-36
lines changed

‎Documentation/trace/rv/index.rst

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,4 @@ Runtime Verification
1010
deterministic_automata.rst
1111
da_monitor_synthesis.rst
1212
da_monitor_instrumentation.rst
13+
monitor_wip.rst

‎Documentation/trace/rv/monitor_wip.rst

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
Monitor wip
2+
===========
3+
4+
- Name: wip - wakeup in preemptive
5+
- Type: per-cpu deterministic automaton
6+
- Author: Daniel Bristot de Oliveira <[email protected]>
7+
8+
Description
9+
-----------
10+
11+
The wakeup in preemptive (wip) monitor is a sample per-cpu monitor
12+
that verifies if the wakeup events always take place with
13+
preemption disabled::
14+
15+
|
16+
|
17+
v
18+
#==================#
19+
H preemptive H <+
20+
#==================# |
21+
| |
22+
| preempt_disable | preempt_enable
23+
v |
24+
sched_waking +------------------+ |
25+
+--------------- | | |
26+
| | non_preemptive | |
27+
+--------------> | | -+
28+
+------------------+
29+
30+
The wakeup event always takes place with preemption disabled because
31+
of the scheduler synchronization. However, because the preempt_count
32+
and its trace event are not atomic with regard to interrupts, some
33+
inconsistencies might happen. For example::
34+
35+
preempt_disable() {
36+
__preempt_count_add(1)
37+
-------> smp_apic_timer_interrupt() {
38+
preempt_disable()
39+
do not trace (preempt count >= 1)
40+
41+
wake up a thread
42+
43+
preempt_enable()
44+
do not trace (preempt count >= 1)
45+
}
46+
<------
47+
trace_preempt_disable();
48+
}
49+
50+
This problem was reported and discussed here:
51+
https://lore.kernel.org/r/[email protected]/
52+
53+
Specification
54+
-------------
55+
Grapviz Dot file in tools/verification/models/wip.dot

‎include/trace/events/rv.h

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,16 @@ DECLARE_EVENT_CLASS(error_da_monitor,
5656
__entry->event,
5757
__entry->state)
5858
);
59+
60+
#ifdef CONFIG_RV_MON_WIP
61+
DEFINE_EVENT(event_da_monitor, event_wip,
62+
TP_PROTO(char *state, char *event, char *next_state, bool final_state),
63+
TP_ARGS(state, event, next_state, final_state));
64+
65+
DEFINE_EVENT(error_da_monitor, error_wip,
66+
TP_PROTO(char *state, char *event),
67+
TP_ARGS(state, event));
68+
#endif /* CONFIG_RV_MON_WIP */
5969
#endif /* CONFIG_DA_MON_EVENTS_IMPLICIT */
6070

6171
#ifdef CONFIG_DA_MON_EVENTS_ID

‎kernel/trace/rv/Kconfig

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,19 @@ menuconfig RV
2525
For further information, see:
2626
Documentation/trace/rv/runtime-verification.rst
2727

28+
config RV_MON_WIP
29+
depends on RV
30+
depends on PREEMPT_TRACER
31+
select DA_MON_EVENTS_IMPLICIT
32+
bool "wip monitor"
33+
help
34+
Enable wip (wakeup in preemptive) sample monitor that illustrates
35+
the usage of per-cpu monitors, and one limitation of the
36+
preempt_disable/enable events.
37+
38+
For further information, see:
39+
Documentation/trace/rv/monitor_wip.rst
40+
2841
config RV_REACTORS
2942
bool "Runtime verification reactors"
3043
default y

‎kernel/trace/rv/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,3 +2,4 @@
22

33
obj-$(CONFIG_RV) += rv.o
44
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
5+
obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o

‎kernel/trace/rv/monitors/wip/wip.c

Lines changed: 15 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -10,44 +10,26 @@
1010

1111
#define MODULE_NAME "wip"
1212

13-
/*
14-
* XXX: include required tracepoint headers, e.g.,
15-
* #include <linux/trace/events/sched.h>
16-
*/
1713
#include <trace/events/rv.h>
14+
#include <trace/events/sched.h>
15+
#include <trace/events/preemptirq.h>
1816

19-
/*
20-
* This is the self-generated part of the monitor. Generally, there is no need
21-
* to touch this section.
22-
*/
2317
#include "wip.h"
2418

25-
/*
26-
* Declare the deterministic automata monitor.
27-
*
28-
* The rv monitor reference is needed for the monitor declaration.
29-
*/
3019
struct rv_monitor rv_wip;
3120
DECLARE_DA_MON_PER_CPU(wip, unsigned char);
3221

33-
/*
34-
* This is the instrumentation part of the monitor.
35-
*
36-
* This is the section where manual work is required. Here the kernel events
37-
* are translated into model's event.
38-
*
39-
*/
40-
static void handle_preempt_disable(void *data, /* XXX: fill header */)
22+
static void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
4123
{
4224
da_handle_event_wip(preempt_disable_wip);
4325
}
4426

45-
static void handle_preempt_enable(void *data, /* XXX: fill header */)
27+
static void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
4628
{
47-
da_handle_event_wip(preempt_enable_wip);
29+
da_handle_start_event_wip(preempt_enable_wip);
4830
}
4931

50-
static void handle_sched_waking(void *data, /* XXX: fill header */)
32+
static void handle_sched_waking(void *data, struct task_struct *task)
5133
{
5234
da_handle_event_wip(sched_waking_wip);
5335
}
@@ -60,9 +42,9 @@ static int enable_wip(void)
6042
if (retval)
6143
return retval;
6244

63-
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
64-
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
65-
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
45+
rv_attach_trace_probe("wip", preempt_enable, handle_preempt_enable);
46+
rv_attach_trace_probe("wip", sched_waking, handle_sched_waking);
47+
rv_attach_trace_probe("wip", preempt_disable, handle_preempt_disable);
6648

6749
return 0;
6850
}
@@ -71,19 +53,16 @@ static void disable_wip(void)
7153
{
7254
rv_wip.enabled = 0;
7355

74-
rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
75-
rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
76-
rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
56+
rv_detach_trace_probe("wip", preempt_disable, handle_preempt_disable);
57+
rv_detach_trace_probe("wip", preempt_enable, handle_preempt_enable);
58+
rv_detach_trace_probe("wip", sched_waking, handle_sched_waking);
7759

7860
da_monitor_destroy_wip();
7961
}
8062

81-
/*
82-
* This is the monitor register section.
83-
*/
8463
struct rv_monitor rv_wip = {
8564
.name = "wip",
86-
.description = "auto-generated wip",
65+
.description = "wakeup in preemptive per-cpu testing monitor.",
8766
.enable = enable_wip,
8867
.disable = disable_wip,
8968
.reset = da_monitor_reset_all_wip,
@@ -105,5 +84,5 @@ module_init(register_wip);
10584
module_exit(unregister_wip);
10685

10786
MODULE_LICENSE("GPL");
108-
MODULE_AUTHOR("dot2k: auto-generated");
109-
MODULE_DESCRIPTION("wip");
87+
MODULE_AUTHOR("Daniel Bristot de Oliveira <[email protected]>");
88+
MODULE_DESCRIPTION("wip: wakeup in preemptive - per-cpu sample monitor.");

‎tools/verification/models/wip.dot

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
digraph state_automaton {
2+
{node [shape = circle] "non_preemptive"};
3+
{node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
4+
{node [shape = doublecircle] "preemptive"};
5+
{node [shape = circle] "preemptive"};
6+
"__init_preemptive" -> "preemptive";
7+
"non_preemptive" [label = "non_preemptive"];
8+
"non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
9+
"non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
10+
"preemptive" [label = "preemptive"];
11+
"preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
12+
{ rank = min ;
13+
"__init_preemptive";
14+
"preemptive";
15+
}
16+
}

0 commit comments

Comments
 (0)