1Deterministic Automata Monitor Synthesis
2========================================
3
4The starting point for the application of runtime verification (RV) technics
5is the *specification* or *modeling* of the desired (or undesired) behavior
6of the system under scrutiny.
7
8The formal representation needs to be then *synthesized* into a *monitor*
9that 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
11the events from the *system* to the events of the *specification*.
12
13
14In Linux terms, the runtime verification monitors are encapsulated inside
15the *RV monitor* abstraction. The RV monitor includes a set of instances
16of the monitor (per-cpu monitor, per-task monitor, and so on), the helper
17functions that glue the monitor to the system reference model, and the
18trace output as a reaction to event parsing and exceptions, as depicted
19below::
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
39DA monitor synthesis
40--------------------
41
42The synthesis of automata-based models into the Linux *RV monitor* abstraction
43is automated by the dot2k tool and the rv/da_monitor.h header file that
44contains a set of macros that automatically generate the monitor's code.
45
46dot2k
47-----
48
49The dot2k utility leverages dot2c by converting an automaton model in
50the DOT format into the C representation [1] and creating the skeleton of
51a kernel monitor in C.
52
53For 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
58This 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
63The wip.c file contains the monitor declaration and the starting point for
64the system instrumentation.
65
66Monitor macros
67--------------
68
69The rv/da_monitor.h enables automatic code generation for the *Monitor
70Instance(s)* using C macros.
71
72The 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
79This 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
85The first declares the functions for a global deterministic automata monitor,
86the second for monitors with per-cpu instances, and the third with per-task
87instances.
88
89In all cases, the 'name' argument is a string that identifies the monitor, and
90the 'type' argument is the data type used by dot2k on the representation of
91the model in C.
92
93For example, the wip model with two states and three events can be
94stored in an 'unsigned char' type. Considering that the preemption control
95is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::
96
97  DECLARE_DA_MON_PER_CPU(wip, unsigned char);
98
99The monitor is executed by sending events to be processed via the functions
100presented 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
106The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where
107the event will be processed if the monitor is processing events.
108
109When a monitor is enabled, it is placed in the initial state of the automata.
110However, the monitor does not know if the system is in the *initial state*.
111
112The ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the
113monitor that the system is returning to the initial state, so the monitor can
114start monitoring the next event.
115
116The ``da_handle_start_run_event_$(MONITOR_NAME)()`` function is used to notify
117the monitor that the system is known to be in the initial state, so the
118monitor can start monitoring and monitor the current event.
119
120Using 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
126While the event "preempt_enabled" will use::
127
128  da_handle_start_event_wip(preempt_enable_wip);
129
130To notify the monitor that the system will be returning to the initial state,
131so the system and the monitor should be in sync.
132
133Final remarks
134-------------
135
136With the monitor synthesis in place using the rv/da_monitor.h and
137dot2k, the developer's work should be limited to the instrumentation
138of the system, increasing the confidence in the overall approach.
139
140[1] For details about deterministic automata format and the translation
141from 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
146avoid conflicting variables when exporting the global vmlinux.h
147use by BPF programs.
148