Skip to content

Commit ff0aaf6

Browse files
Daniel Bristot de Oliveirarostedt
Daniel Bristot de Oliveira
authored and
rostedt
committed
Documentation/rv: Add a basic documentation
Add the runtime-verification.rst document, explaining the basics of RV and how to use the interface. Link: https://lkml.kernel.org/r/4be7d1a88ab1e2eb0767521e1ab52a149a154bc4.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 cc8e71c commit ff0aaf6

5 files changed

Lines changed: 247 additions & 0 deletions

File tree

‎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/rv/index.rst‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
====================
2+
Runtime Verification
3+
====================
4+
5+
.. toctree::
6+
:maxdepth: 2
7+
:glob:
8+
9+
runtime-verification.rst

‎Documentation/trace/rv/runtime-verification.rst‎

Lines changed: 231 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,231 @@
1+
====================
2+
Runtime Verification
3+
====================
4+
5+
Runtime Verification (RV) is a lightweight (yet rigorous) method that
6+
complements classical exhaustive verification techniques (such as *model
7+
checking* and *theorem proving*) with a more practical approach for complex
8+
systems.
9+
10+
Instead of relying on a fine-grained model of a system (e.g., a
11+
re-implementation a instruction level), RV works by analyzing the trace of the
12+
system's actual execution, comparing it against a formal specification of
13+
the system behavior.
14+
15+
The main advantage is that RV can give precise information on the runtime
16+
behavior of the monitored system, without the pitfalls of developing models
17+
that require a re-implementation of the entire system in a modeling language.
18+
Moreover, given an efficient monitoring method, it is possible execute an
19+
*online* verification of a system, enabling the *reaction* for unexpected
20+
events, avoiding, for example, the propagation of a failure on safety-critical
21+
systems.
22+
23+
Runtime Monitors and Reactors
24+
=============================
25+
26+
A monitor is the central part of the runtime verification of a system. The
27+
monitor stands in between the formal specification of the desired (or
28+
undesired) behavior, and the trace of the actual system.
29+
30+
In Linux terms, the runtime verification monitors are encapsulated inside the
31+
*RV monitor* abstraction. A *RV monitor* includes a reference model of the
32+
system, a set of instances of the monitor (per-cpu monitor, per-task monitor,
33+
and so on), and the helper functions that glue the monitor to the system via
34+
trace, as depicted bellow::
35+
36+
Linux +---- RV Monitor ----------------------------------+ Formal
37+
Realm | | Realm
38+
+-------------------+ +----------------+ +-----------------+
39+
| Linux kernel | | Monitor | | Reference |
40+
| Tracing | -> | Instance(s) | <- | Model |
41+
| (instrumentation) | | (verification) | | (specification) |
42+
+-------------------+ +----------------+ +-----------------+
43+
| | |
44+
| V |
45+
| +----------+ |
46+
| | Reaction | |
47+
| +--+--+--+-+ |
48+
| | | | |
49+
| | | +-> trace output ? |
50+
+------------------------|--|----------------------+
51+
| +----> panic ?
52+
+-------> <user-specified>
53+
54+
In addition to the verification and monitoring of the system, a monitor can
55+
react to an unexpected event. The forms of reaction can vary from logging the
56+
event occurrence to the enforcement of the correct behavior to the extreme
57+
action of taking a system down to avoid the propagation of a failure.
58+
59+
In Linux terms, a *reactor* is an reaction method available for *RV monitors*.
60+
By default, all monitors should provide a trace output of their actions,
61+
which is already a reaction. In addition, other reactions will be available
62+
so the user can enable them as needed.
63+
64+
For further information about the principles of runtime verification and
65+
RV applied to Linux:
66+
67+
Bartocci, Ezio, et al. *Introduction to runtime verification.* In: Lectures on
68+
Runtime Verification. Springer, Cham, 2018. p. 1-33.
69+
70+
Falcone, Ylies, et al. *A taxonomy for classifying runtime verification tools.*
71+
In: International Conference on Runtime Verification. Springer, Cham, 2018. p.
72+
241-262.
73+
74+
De Oliveira, Daniel Bristot. *Automata-based formal analysis and
75+
verification of the real-time Linux kernel.* Ph.D. Thesis, 2020.
76+
77+
Online RV monitors
78+
==================
79+
80+
Monitors can be classified as *offline* and *online* monitors. *Offline*
81+
monitor process the traces generated by a system after the events, generally by
82+
reading the trace execution from a permanent storage system. *Online* monitors
83+
process the trace during the execution of the system. Online monitors are said
84+
to be *synchronous* if the processing of an event is attached to the system
85+
execution, blocking the system during the event monitoring. On the other hand,
86+
an *asynchronous* monitor has its execution detached from the system. Each type
87+
of monitor has a set of advantages. For example, *offline* monitors can be
88+
executed on different machines but require operations to save the log to a
89+
file. In contrast, *synchronous online* method can react at the exact moment
90+
a violation occurs.
91+
92+
Another important aspect regarding monitors is the overhead associated with the
93+
event analysis. If the system generates events at a frequency higher than the
94+
monitor's ability to process them in the same system, only the *offline*
95+
methods are viable. On the other hand, if the tracing of the events incurs
96+
on higher overhead than the simple handling of an event by a monitor, then a
97+
*synchronous online* monitors will incur on lower overhead.
98+
99+
Indeed, the research presented in:
100+
101+
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva.
102+
*Efficient formal verification for the Linux kernel.* In: International
103+
Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
104+
p. 315-332.
105+
106+
Shows that for Deterministic Automata models, the synchronous processing of
107+
events in-kernel causes lower overhead than saving the same events to the trace
108+
buffer, not even considering collecting the trace for user-space analysis.
109+
This motivated the development of an in-kernel interface for online monitors.
110+
111+
For further information about modeling of Linux kernel behavior using automata,
112+
see:
113+
114+
De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *A thread
115+
synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems
116+
Architecture, 2020, 107: 101729.
117+
118+
The user interface
119+
==================
120+
121+
The user interface resembles the tracing interface (on purpose). It is
122+
currently at "/sys/kernel/tracing/rv/".
123+
124+
The following files/folders are currently available:
125+
126+
**available_monitors**
127+
128+
- Reading list the available monitors, one per line
129+
130+
For example::
131+
132+
# cat available_monitors
133+
wip
134+
wwnr
135+
136+
**available_reactors**
137+
138+
- Reading shows the available reactors, one per line.
139+
140+
For example::
141+
142+
# cat available_reactors
143+
nop
144+
panic
145+
printk
146+
147+
**enabled_monitors**:
148+
149+
- Reading lists the enabled monitors, one per line
150+
- Writing to it enables a given monitor
151+
- Writing a monitor name with a '!' prefix disables it
152+
- Truncating the file disables all enabled monitors
153+
154+
For example::
155+
156+
# cat enabled_monitors
157+
# echo wip > enabled_monitors
158+
# echo wwnr >> enabled_monitors
159+
# cat enabled_monitors
160+
wip
161+
wwnr
162+
# echo '!wip' >> enabled_monitors
163+
# cat enabled_monitors
164+
wwnr
165+
# echo > enabled_monitors
166+
# cat enabled_monitors
167+
#
168+
169+
Note that it is possible to enable more than one monitor concurrently.
170+
171+
**monitoring_on**
172+
173+
This is an on/off general switcher for monitoring. It resembles the
174+
"tracing_on" switcher in the trace interface.
175+
176+
- Writing "0" stops the monitoring
177+
- Writing "1" continues the monitoring
178+
- Reading returns the current status of the monitoring
179+
180+
Note that it does not disable enabled monitors but stop the per-entity
181+
monitors monitoring the events received from the system.
182+
183+
**reacting_on**
184+
185+
- Writing "0" prevents reactions for happening
186+
- Writing "1" enable reactions
187+
- Reading returns the current status of the reaction
188+
189+
**monitors/**
190+
191+
Each monitor will have its own directory inside "monitors/". There the
192+
monitor-specific files will be presented. The "monitors/" directory resembles
193+
the "events" directory on tracefs.
194+
195+
For example::
196+
197+
# cd monitors/wip/
198+
# ls
199+
desc enable
200+
# cat desc
201+
wakeup in preemptive per-cpu testing monitor.
202+
# cat enable
203+
0
204+
205+
**monitors/MONITOR/desc**
206+
207+
- Reading shows a description of the monitor *MONITOR*
208+
209+
**monitors/MONITOR/enable**
210+
211+
- Writing "0" disables the *MONITOR*
212+
- Writing "1" enables the *MONITOR*
213+
- Reading return the current status of the *MONITOR*
214+
215+
**monitors/MONITOR/reactors**
216+
217+
- List available reactors, with the select reaction for the given *MONITOR*
218+
inside "[]". The default one is the nop (no operation) reactor.
219+
- Writing the name of a reactor enables it to the given MONITOR.
220+
221+
For example::
222+
223+
# cat monitors/wip/reactors
224+
[nop]
225+
panic
226+
printk
227+
# echo panic > monitors/wip/reactors
228+
# cat monitors/wip/reactors
229+
nop
230+
[panic]
231+
printk

‎kernel/trace/rv/Kconfig‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,9 @@ menuconfig RV
2222
actual execution, comparing it against a formal specification of
2323
the system behavior.
2424

25+
For further information, see:
26+
Documentation/trace/rv/runtime-verification.rst
27+
2528
config RV_REACTORS
2629
bool "Runtime verification reactors"
2730
default y

‎kernel/trace/rv/rv.c‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -133,6 +133,9 @@
133133
* auto-generated wakeup in preemptive monitor.
134134
* # cat enable
135135
* 0
136+
*
137+
* For further information, see:
138+
* Documentation/trace/rv/runtime-verification.rst
136139
*/
137140

138141
#include <linux/kernel.h>

0 commit comments

Comments
 (0)