forked from Qortal/Brooklyn
You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
147 lines
5.9 KiB
147 lines
5.9 KiB
Deterministic Automata Monitor Synthesis |
|
======================================== |
|
|
|
The starting point for the application of runtime verification (RV) technics |
|
is the *specification* or *modeling* of the desired (or undesired) behavior |
|
of the system under scrutiny. |
|
|
|
The formal representation needs to be then *synthesized* into a *monitor* |
|
that can then be used in the analysis of the trace of the system. The |
|
*monitor* connects to the system via an *instrumentation* that converts |
|
the events from the *system* to the events of the *specification*. |
|
|
|
|
|
In Linux terms, the runtime verification monitors are encapsulated inside |
|
the *RV monitor* abstraction. The RV monitor includes a set of instances |
|
of the monitor (per-cpu monitor, per-task monitor, and so on), the helper |
|
functions that glue the monitor to the system reference model, and the |
|
trace output as a reaction to event parsing and exceptions, as depicted |
|
below:: |
|
|
|
Linux +----- RV Monitor ----------------------------------+ Formal |
|
Realm | | Realm |
|
+-------------------+ +----------------+ +-----------------+ |
|
| Linux kernel | | Monitor | | Reference | |
|
| Tracing | -> | Instance(s) | <- | Model | |
|
| (instrumentation) | | (verification) | | (specification) | |
|
+-------------------+ +----------------+ +-----------------+ |
|
| | | |
|
| V | |
|
| +----------+ | |
|
| | Reaction | | |
|
| +--+--+--+-+ | |
|
| | | | | |
|
| | | +-> trace output ? | |
|
+------------------------|--|----------------------+ |
|
| +----> panic ? |
|
+-------> <user-specified> |
|
|
|
DA monitor synthesis |
|
-------------------- |
|
|
|
The synthesis of automata-based models into the Linux *RV monitor* abstraction |
|
is automated by the dot2k tool and the rv/da_monitor.h header file that |
|
contains a set of macros that automatically generate the monitor's code. |
|
|
|
dot2k |
|
----- |
|
|
|
The dot2k utility leverages dot2c by converting an automaton model in |
|
the DOT format into the C representation [1] and creating the skeleton of |
|
a kernel monitor in C. |
|
|
|
For example, it is possible to transform the wip.dot model present in |
|
[1] into a per-cpu monitor with the following command:: |
|
|
|
$ dot2k -d wip.dot -t per_cpu |
|
|
|
This will create a directory named wip/ with the following files: |
|
|
|
- wip.h: the wip model in C |
|
- wip.c: the RV monitor |
|
|
|
The wip.c file contains the monitor declaration and the starting point for |
|
the system instrumentation. |
|
|
|
Monitor macros |
|
-------------- |
|
|
|
The rv/da_monitor.h enables automatic code generation for the *Monitor |
|
Instance(s)* using C macros. |
|
|
|
The benefits of the usage of macro for monitor synthesis are 3-fold as it: |
|
|
|
- Reduces the code duplication; |
|
- Facilitates the bug fix/improvement; |
|
- Avoids the case of developers changing the core of the monitor code |
|
to manipulate the model in a (let's say) non-standard way. |
|
|
|
This initial implementation presents three different types of monitor instances: |
|
|
|
- ``#define DECLARE_DA_MON_GLOBAL(name, type)`` |
|
- ``#define DECLARE_DA_MON_PER_CPU(name, type)`` |
|
- ``#define DECLARE_DA_MON_PER_TASK(name, type)`` |
|
|
|
The first declares the functions for a global deterministic automata monitor, |
|
the second for monitors with per-cpu instances, and the third with per-task |
|
instances. |
|
|
|
In all cases, the 'name' argument is a string that identifies the monitor, and |
|
the 'type' argument is the data type used by dot2k on the representation of |
|
the model in C. |
|
|
|
For example, the wip model with two states and three events can be |
|
stored in an 'unsigned char' type. Considering that the preemption control |
|
is a per-cpu behavior, the monitor declaration in the 'wip.c' file is:: |
|
|
|
DECLARE_DA_MON_PER_CPU(wip, unsigned char); |
|
|
|
The monitor is executed by sending events to be processed via the functions |
|
presented below:: |
|
|
|
da_handle_event_$(MONITOR_NAME)($(event from event enum)); |
|
da_handle_start_event_$(MONITOR_NAME)($(event from event enum)); |
|
da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum)); |
|
|
|
The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where |
|
the event will be processed if the monitor is processing events. |
|
|
|
When a monitor is enabled, it is placed in the initial state of the automata. |
|
However, the monitor does not know if the system is in the *initial state*. |
|
|
|
The ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the |
|
monitor that the system is returning to the initial state, so the monitor can |
|
start monitoring the next event. |
|
|
|
The ``da_handle_start_run_event_$(MONITOR_NAME)()`` function is used to notify |
|
the monitor that the system is known to be in the initial state, so the |
|
monitor can start monitoring and monitor the current event. |
|
|
|
Using the wip model as example, the events "preempt_disable" and |
|
"sched_waking" should be sent to monitor, respectively, via [2]:: |
|
|
|
da_handle_event_wip(preempt_disable_wip); |
|
da_handle_event_wip(sched_waking_wip); |
|
|
|
While the event "preempt_enabled" will use:: |
|
|
|
da_handle_start_event_wip(preempt_enable_wip); |
|
|
|
To notify the monitor that the system will be returning to the initial state, |
|
so the system and the monitor should be in sync. |
|
|
|
Final remarks |
|
------------- |
|
|
|
With the monitor synthesis in place using the rv/da_monitor.h and |
|
dot2k, the developer's work should be limited to the instrumentation |
|
of the system, increasing the confidence in the overall approach. |
|
|
|
[1] For details about deterministic automata format and the translation |
|
from one representation to another, see:: |
|
|
|
Documentation/trace/rv/deterministic_automata.rst |
|
|
|
[2] dot2k appends the monitor's name suffix to the events enums to |
|
avoid conflicting variables when exporting the global vmlinux.h |
|
use by BPF programs.
|
|
|