Documentation/trace/rv/monitor_synthesis.rst

Source file repositories/reference/linux-study-clean/Documentation/trace/rv/monitor_synthesis.rst

File Facts

System
Linux kernel
Corpus path
Documentation/trace/rv/monitor_synthesis.rst
Extension
.rst
Size
14941 bytes
Lines
383
Domain
Support Tooling And Documentation
Bucket
Documentation
Inferred role
Support Tooling And Documentation: documentation
Status
atlas-only

Why This File Exists

Repository support layer: documentation, build tooling, samples, user-space helper tools, generated initramfs support, licenses, and validation utilities.

Dependency Surface

Detected Declarations

Annotated Snippet

Runtime Verification Monitor Synthesis
======================================

The starting point for the application of runtime verification (RV) techniques
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>

RV monitor synthesis
--------------------

The synthesis of a specification into the Linux *RV monitor* abstraction is
automated by the rvgen tool and the header file containing common code for
creating monitors. The header files are:

  * rv/da_monitor.h for deterministic automaton monitor.
  * rv/ltl_monitor.h for linear temporal logic monitor.
  * rv/ha_monitor.h for hybrid automaton monitor.

rvgen
-----

The rvgen utility converts a specification into the C presentation 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::

  $ rvgen monitor -c da -s 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.

Similarly, a linear temporal logic monitor can be generated with the following
command::

Annotation

Implementation Notes