Skip to content

Commit 965a9d7

Browse files
committed
Merge tag 'trace-v6.0' of git://git.kernel.org/pub/scm/linux/kernel/git/rostedt/linux-trace
Pull tracing updates from Steven Rostedt: - Runtime verification infrastructure This is the biggest change here. It introduces the runtime verification that is necessary for running Linux on safety critical systems. It allows for deterministic automata models to be inserted into the kernel that will attach to tracepoints, where the information on these tracepoints will move the model from state to state. If a state is encountered that does not belong to the model, it will then activate a given reactor, that could just inform the user or even panic the kernel (for which safety critical systems will detect and can recover from). - Two monitor models are also added: Wakeup In Preemptive (WIP - not to be confused with "work in progress"), and Wakeup While Not Running (WWNR). - Added __vstring() helper to the TRACE_EVENT() macro to replace several vsnprintf() usages that were all doing it wrong. - eprobes now can have their event autogenerated when the event name is left off. - The rest is various cleanups and fixes. * tag 'trace-v6.0' of git://git.kernel.org/pub/scm/linux/kernel/git/rostedt/linux-trace: (50 commits) rv: Unlock on error path in rv_unregister_reactor() tracing: Use alignof__(struct {type b;}) instead of offsetof() tracing/eprobe: Show syntax error logs in error_log file scripts/tracing: Fix typo 'the the' in comment tracepoints: It is CONFIG_TRACEPOINTS not CONFIG_TRACEPOINT tracing: Use free_trace_buffer() in allocate_trace_buffers() tracing: Use a struct alignof to determine trace event field alignment rv/reactor: Add the panic reactor rv/reactor: Add the printk reactor rv/monitor: Add the wwnr monitor rv/monitor: Add the wip monitor rv/monitor: Add the wip monitor skeleton created by dot2k Documentation/rv: Add deterministic automata instrumentation documentation Documentation/rv: Add deterministic automata monitor synthesis documentation tools/rv: Add dot2k Documentation/rv: Add deterministic automaton documentation tools/rv: Add dot2c Documentation/rv: Add a basic documentation rv/include: Add instrumentation helper functions rv/include: Add deterministic automata monitor definition via C macros ...
2 parents 29b1d46 + f1a15b9 commit 965a9d7

File tree

86 files changed

+4808
-172
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

86 files changed

+4808
-172
lines changed

Documentation/trace/index.rst

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,3 +32,4 @@ Linux Tracing Technologies
3232
sys-t
3333
coresight/index
3434
user_events
35+
rv/index

Documentation/trace/kprobetrace.rst

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -28,10 +28,10 @@ Synopsis of kprobe_events
2828
-------------------------
2929
::
3030

31-
p[:[GRP/]EVENT] [MOD:]SYM[+offs]|MEMADDR [FETCHARGS] : Set a probe
32-
r[MAXACTIVE][:[GRP/]EVENT] [MOD:]SYM[+0] [FETCHARGS] : Set a return probe
33-
p:[GRP/]EVENT] [MOD:]SYM[+0]%return [FETCHARGS] : Set a return probe
34-
-:[GRP/]EVENT : Clear a probe
31+
p[:[GRP/][EVENT]] [MOD:]SYM[+offs]|MEMADDR [FETCHARGS] : Set a probe
32+
r[MAXACTIVE][:[GRP/][EVENT]] [MOD:]SYM[+0] [FETCHARGS] : Set a return probe
33+
p[:[GRP/][EVENT]] [MOD:]SYM[+0]%return [FETCHARGS] : Set a return probe
34+
-:[GRP/][EVENT] : Clear a probe
3535

3636
GRP : Group name. If omitted, use "kprobes" for it.
3737
EVENT : Event name. If omitted, the event name is generated
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
Lines changed: 147 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,147 @@
1+
Deterministic Automata Monitor Synthesis
2+
========================================
3+
4+
The starting point for the application of runtime verification (RV) technics
5+
is the *specification* or *modeling* of the desired (or undesired) behavior
6+
of the system under scrutiny.
7+
8+
The formal representation needs to be then *synthesized* into a *monitor*
9+
that can then be used in the analysis of the trace of the system. The
10+
*monitor* connects to the system via an *instrumentation* that converts
11+
the events from the *system* to the events of the *specification*.
12+
13+
14+
In Linux terms, the runtime verification monitors are encapsulated inside
15+
the *RV monitor* abstraction. The RV monitor includes a set of instances
16+
of the monitor (per-cpu monitor, per-task monitor, and so on), the helper
17+
functions that glue the monitor to the system reference model, and the
18+
trace output as a reaction to event parsing and exceptions, as depicted
19+
below::
20+
21+
Linux +----- RV Monitor ----------------------------------+ Formal
22+
Realm | | Realm
23+
+-------------------+ +----------------+ +-----------------+
24+
| Linux kernel | | Monitor | | Reference |
25+
| Tracing | -> | Instance(s) | <- | Model |
26+
| (instrumentation) | | (verification) | | (specification) |
27+
+-------------------+ +----------------+ +-----------------+
28+
| | |
29+
| V |
30+
| +----------+ |
31+
| | Reaction | |
32+
| +--+--+--+-+ |
33+
| | | | |
34+
| | | +-> trace output ? |
35+
+------------------------|--|----------------------+
36+
| +----> panic ?
37+
+-------> <user-specified>
38+
39+
DA monitor synthesis
40+
--------------------
41+
42+
The synthesis of automata-based models into the Linux *RV monitor* abstraction
43+
is automated by the dot2k tool and the rv/da_monitor.h header file that
44+
contains a set of macros that automatically generate the monitor's code.
45+
46+
dot2k
47+
-----
48+
49+
The dot2k utility leverages dot2c by converting an automaton model in
50+
the DOT format into the C representation [1] and creating the skeleton of
51+
a kernel monitor in C.
52+
53+
For example, it is possible to transform the wip.dot model present in
54+
[1] into a per-cpu monitor with the following command::
55+
56+
$ dot2k -d wip.dot -t per_cpu
57+
58+
This will create a directory named wip/ with the following files:
59+
60+
- wip.h: the wip model in C
61+
- wip.c: the RV monitor
62+
63+
The wip.c file contains the monitor declaration and the starting point for
64+
the system instrumentation.
65+
66+
Monitor macros
67+
--------------
68+
69+
The rv/da_monitor.h enables automatic code generation for the *Monitor
70+
Instance(s)* using C macros.
71+
72+
The benefits of the usage of macro for monitor synthesis are 3-fold as it:
73+
74+
- Reduces the code duplication;
75+
- Facilitates the bug fix/improvement;
76+
- Avoids the case of developers changing the core of the monitor code
77+
to manipulate the model in a (let's say) non-standard way.
78+
79+
This initial implementation presents three different types of monitor instances:
80+
81+
- ``#define DECLARE_DA_MON_GLOBAL(name, type)``
82+
- ``#define DECLARE_DA_MON_PER_CPU(name, type)``
83+
- ``#define DECLARE_DA_MON_PER_TASK(name, type)``
84+
85+
The first declares the functions for a global deterministic automata monitor,
86+
the second for monitors with per-cpu instances, and the third with per-task
87+
instances.
88+
89+
In all cases, the 'name' argument is a string that identifies the monitor, and
90+
the 'type' argument is the data type used by dot2k on the representation of
91+
the model in C.
92+
93+
For example, the wip model with two states and three events can be
94+
stored in an 'unsigned char' type. Considering that the preemption control
95+
is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::
96+
97+
DECLARE_DA_MON_PER_CPU(wip, unsigned char);
98+
99+
The monitor is executed by sending events to be processed via the functions
100+
presented below::
101+
102+
da_handle_event_$(MONITOR_NAME)($(event from event enum));
103+
da_handle_start_event_$(MONITOR_NAME)($(event from event enum));
104+
da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum));
105+
106+
The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where
107+
the event will be processed if the monitor is processing events.
108+
109+
When a monitor is enabled, it is placed in the initial state of the automata.
110+
However, the monitor does not know if the system is in the *initial state*.
111+
112+
The ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the
113+
monitor that the system is returning to the initial state, so the monitor can
114+
start monitoring the next event.
115+
116+
The ``da_handle_start_run_event_$(MONITOR_NAME)()`` function is used to notify
117+
the monitor that the system is known to be in the initial state, so the
118+
monitor can start monitoring and monitor the current event.
119+
120+
Using the wip model as example, the events "preempt_disable" and
121+
"sched_waking" should be sent to monitor, respectively, via [2]::
122+
123+
da_handle_event_wip(preempt_disable_wip);
124+
da_handle_event_wip(sched_waking_wip);
125+
126+
While the event "preempt_enabled" will use::
127+
128+
da_handle_start_event_wip(preempt_enable_wip);
129+
130+
To notify the monitor that the system will be returning to the initial state,
131+
so the system and the monitor should be in sync.
132+
133+
Final remarks
134+
-------------
135+
136+
With the monitor synthesis in place using the rv/da_monitor.h and
137+
dot2k, the developer's work should be limited to the instrumentation
138+
of the system, increasing the confidence in the overall approach.
139+
140+
[1] For details about deterministic automata format and the translation
141+
from one representation to another, see::
142+
143+
Documentation/trace/rv/deterministic_automata.rst
144+
145+
[2] dot2k appends the monitor's name suffix to the events enums to
146+
avoid conflicting variables when exporting the global vmlinux.h
147+
use by BPF programs.

0 commit comments

Comments
 (0)