Documentation/trace/rv/da_monitor_synthesis.rst

   1 Deterministic Automata Monitor Synthesis
   2 ========================================
   3
   4 The starting point for the application of runtime verification (RV) techniques
   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.