Skip to content

Commit d57aff2

Browse files
Daniel Bristot de Oliveirarostedt
Daniel Bristot de Oliveira
authored and
rostedt
committed
Documentation/rv: Add deterministic automata monitor synthesis documentation
Add the da_monitor_synthesis.rst introduces some concepts behind the Deterministic Automata (DA) monitor synthesis and interface. Link: https://lkml.kernel.org/r/7873bdb7b2e5d2bc0b2eb6ca0b324af9a0ba27a0.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 24bce20 commit d57aff2

File tree

5 files changed

+157
-0
lines changed

5 files changed

+157
-0
lines changed

‎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.

‎Documentation/trace/rv/index.rst

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,4 @@ Runtime Verification
88

99
runtime-verification.rst
1010
deterministic_automata.rst
11+
da_monitor_synthesis.rst

‎include/rv/da_monitor.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,9 @@
66
* with automata models in C generated by the dot2k tool.
77
*
88
* The dot2k tool is available at tools/verification/dot2k/
9+
*
10+
* For further information, see:
11+
* Documentation/trace/rv/da_monitor_synthesis.rst
912
*/
1013

1114
#include <rv/automata.h>

‎tools/verification/dot2/dot2k

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,9 @@
44
# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
55
#
66
# dot2k: transform dot files into a monitor for the Linux kernel.
7+
#
8+
# For further information, see:
9+
# Documentation/trace/rv/da_monitor_synthesis.rst
710

811
if __name__ == '__main__':
912
from dot2.dot2k import dot2k

‎tools/verification/dot2/dot2k.py

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,9 @@
44
# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
55
#
66
# dot2k: transform dot files into a monitor for the Linux kernel.
7+
#
8+
# For further information, see:
9+
# Documentation/trace/rv/da_monitor_synthesis.rst
710

811
from dot2.dot2c import Dot2c
912
import platform

0 commit comments

Comments
 (0)