Skip to content

Commit b6172b5

Browse files
Daniel Bristot de Oliveirarostedt
authored andcommitted
Documentation/rv: Add deterministic automata instrumentation documentation
Add the da_monitor_instrumentation.rst. It describes the basics of RV monitor instrumentation. Link: https://lkml.kernel.org/r/0557d5c68e2fc252f2643c2cc5295a67e2b73277.1659052063.git.bristot@kernel.org Cc: Wim Van Sebroeck <wim@linux-watchdog.org> Cc: Guenter Roeck <linux@roeck-us.net> Cc: Jonathan Corbet <corbet@lwn.net> Cc: Ingo Molnar <mingo@redhat.com> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Will Deacon <will@kernel.org> Cc: Catalin Marinas <catalin.marinas@arm.com> Cc: Marco Elver <elver@google.com> Cc: Dmitry Vyukov <dvyukov@google.com> Cc: "Paul E. McKenney" <paulmck@kernel.org> Cc: Shuah Khan <skhan@linuxfoundation.org> Cc: Gabriele Paoloni <gpaoloni@redhat.com> Cc: Juri Lelli <juri.lelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: Tao Zhou <tao.zhou@linux.dev> Cc: Randy Dunlap <rdunlap@infradead.org> Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
1 parent d57aff2 commit b6172b5

2 files changed

Lines changed: 172 additions & 0 deletions

File tree

Lines changed: 171 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,171 @@
1+
Deterministic Automata Instrumentation
2+
======================================
3+
4+
The RV monitor file created by dot2k, with the name "$MODEL_NAME.c"
5+
includes a section dedicated to instrumentation.
6+
7+
In the example of the wip.dot monitor created on [1], it will look like::
8+
9+
/*
10+
* This is the instrumentation part of the monitor.
11+
*
12+
* This is the section where manual work is required. Here the kernel events
13+
* are translated into model's event.
14+
*
15+
*/
16+
static void handle_preempt_disable(void *data, /* XXX: fill header */)
17+
{
18+
da_handle_event_wip(preempt_disable_wip);
19+
}
20+
21+
static void handle_preempt_enable(void *data, /* XXX: fill header */)
22+
{
23+
da_handle_event_wip(preempt_enable_wip);
24+
}
25+
26+
static void handle_sched_waking(void *data, /* XXX: fill header */)
27+
{
28+
da_handle_event_wip(sched_waking_wip);
29+
}
30+
31+
static int enable_wip(void)
32+
{
33+
int retval;
34+
35+
retval = da_monitor_init_wip();
36+
if (retval)
37+
return retval;
38+
39+
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
40+
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
41+
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
42+
43+
return 0;
44+
}
45+
46+
The comment at the top of the section explains the general idea: the
47+
instrumentation section translates *kernel events* into the *model's
48+
event*.
49+
50+
Tracing callback functions
51+
--------------------------
52+
53+
The first three functions are the starting point of the callback *handler
54+
functions* for each of the three events from the wip model. The developer
55+
does not necessarily need to use them: they are just starting points.
56+
57+
Using the example of::
58+
59+
void handle_preempt_disable(void *data, /* XXX: fill header */)
60+
{
61+
da_handle_event_wip(preempt_disable_wip);
62+
}
63+
64+
The preempt_disable event from the model connects directly to the
65+
preemptirq:preempt_disable. The preemptirq:preempt_disable event
66+
has the following signature, from include/trace/events/preemptirq.h::
67+
68+
TP_PROTO(unsigned long ip, unsigned long parent_ip)
69+
70+
Hence, the handle_preempt_disable() function will look like::
71+
72+
void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
73+
74+
In this case, the kernel event translates one to one with the automata
75+
event, and indeed, no other change is required for this function.
76+
77+
The next handler function, handle_preempt_enable() has the same argument
78+
list from the handle_preempt_disable(). The difference is that the
79+
preempt_enable event will be used to synchronize the system to the model.
80+
81+
Initially, the *model* is placed in the initial state. However, the *system*
82+
might or might not be in the initial state. The monitor cannot start
83+
processing events until it knows that the system has reached the initial state.
84+
Otherwise, the monitor and the system could be out-of-sync.
85+
86+
Looking at the automata definition, it is possible to see that the system
87+
and the model are expected to return to the initial state after the
88+
preempt_enable execution. Hence, it can be used to synchronize the
89+
system and the model at the initialization of the monitoring section.
90+
91+
The start is informed via a special handle function, the
92+
"da_handle_start_event_$(MONITOR_NAME)(event)", in this case::
93+
94+
da_handle_start_event_wip(preempt_enable_wip);
95+
96+
So, the callback function will look like::
97+
98+
void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
99+
{
100+
da_handle_start_event_wip(preempt_enable_wip);
101+
}
102+
103+
Finally, the "handle_sched_waking()" will look like::
104+
105+
void handle_sched_waking(void *data, struct task_struct *task)
106+
{
107+
da_handle_event_wip(sched_waking_wip);
108+
}
109+
110+
And the explanation is left for the reader as an exercise.
111+
112+
enable and disable functions
113+
----------------------------
114+
115+
dot2k automatically creates two special functions::
116+
117+
enable_$(MONITOR_NAME)()
118+
disable_$(MONITOR_NAME)()
119+
120+
These functions are called when the monitor is enabled and disabled,
121+
respectively.
122+
123+
They should be used to *attach* and *detach* the instrumentation to the running
124+
system. The developer must add to the relative function all that is needed to
125+
*attach* and *detach* its monitor to the system.
126+
127+
For the wip case, these functions were named::
128+
129+
enable_wip()
130+
disable_wip()
131+
132+
But no change was required because: by default, these functions *attach* and
133+
*detach* the tracepoints_to_attach, which was enough for this case.
134+
135+
Instrumentation helpers
136+
-----------------------
137+
138+
To complete the instrumentation, the *handler functions* need to be attached to a
139+
kernel event, at the monitoring enable phase.
140+
141+
The RV interface also facilitates this step. For example, the macro "rv_attach_trace_probe()"
142+
is used to connect the wip model events to the relative kernel event. dot2k automatically
143+
adds "rv_attach_trace_probe()" function call for each model event in the enable phase, as
144+
a suggestion.
145+
146+
For example, from the wip sample model::
147+
148+
static int enable_wip(void)
149+
{
150+
int retval;
151+
152+
retval = da_monitor_init_wip();
153+
if (retval)
154+
return retval;
155+
156+
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
157+
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
158+
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
159+
160+
return 0;
161+
}
162+
163+
The probes then need to be detached at the disable phase.
164+
165+
[1] The wip model is presented in::
166+
167+
Documentation/trace/rv/deterministic_automata.rst
168+
169+
The wip monitor is presented in::
170+
171+
Documentation/trace/rv/da_monitor_synthesis.rst

Documentation/trace/rv/index.rst

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ Runtime Verification
99
runtime-verification.rst
1010
deterministic_automata.rst
1111
da_monitor_synthesis.rst
12+
da_monitor_instrumentation.rst

0 commit comments

Comments
 (0)