0001 Deterministic Automata Monitor Synthesis
0002 ========================================
0003
0004 The starting point for the application of runtime verification (RV) technics
0005 is the *specification* or *modeling* of the desired (or undesired) behavior
0006 of the system under scrutiny.
0007
0008 The formal representation needs to be then *synthesized* into a *monitor*
0009 that can then be used in the analysis of the trace of the system. The
0010 *monitor* connects to the system via an *instrumentation* that converts
0011 the events from the *system* to the events of the *specification*.
0012
0013
0014 In Linux terms, the runtime verification monitors are encapsulated inside
0015 the *RV monitor* abstraction. The RV monitor includes a set of instances
0016 of the monitor (per-cpu monitor, per-task monitor, and so on), the helper
0017 functions that glue the monitor to the system reference model, and the
0018 trace output as a reaction to event parsing and exceptions, as depicted
0019 below::
0020
0021 Linux +----- RV Monitor ----------------------------------+ Formal
0022 Realm | | Realm
0023 +-------------------+ +----------------+ +-----------------+
0024 | Linux kernel | | Monitor | | Reference |
0025 | Tracing | -> | Instance(s) | <- | Model |
0026 | (instrumentation) | | (verification) | | (specification) |
0027 +-------------------+ +----------------+ +-----------------+
0028 | | |
0029 | V |
0030 | +----------+ |
0031 | | Reaction | |
0032 | +--+--+--+-+ |
0033 | | | | |
0034 | | | +-> trace output ? |
0035 +------------------------|--|----------------------+
0036 | +----> panic ?
0037 +-------> <user-specified>
0038
0039 DA monitor synthesis
0040 --------------------
0041
0042 The synthesis of automata-based models into the Linux *RV monitor* abstraction
0043 is automated by the dot2k tool and the rv/da_monitor.h header file that
0044 contains a set of macros that automatically generate the monitor's code.
0045
0046 dot2k
0047 -----
0048
0049 The dot2k utility leverages dot2c by converting an automaton model in
0050 the DOT format into the C representation [1] and creating the skeleton of
0051 a kernel monitor in C.
0052
0053 For example, it is possible to transform the wip.dot model present in
0054 [1] into a per-cpu monitor with the following command::
0055
0056 $ dot2k -d wip.dot -t per_cpu
0057
0058 This will create a directory named wip/ with the following files:
0059
0060 - wip.h: the wip model in C
0061 - wip.c: the RV monitor
0062
0063 The wip.c file contains the monitor declaration and the starting point for
0064 the system instrumentation.
0065
0066 Monitor macros
0067 --------------
0068
0069 The rv/da_monitor.h enables automatic code generation for the *Monitor
0070 Instance(s)* using C macros.
0071
0072 The benefits of the usage of macro for monitor synthesis are 3-fold as it:
0073
0074 - Reduces the code duplication;
0075 - Facilitates the bug fix/improvement;
0076 - Avoids the case of developers changing the core of the monitor code
0077 to manipulate the model in a (let's say) non-standard way.
0078
0079 This initial implementation presents three different types of monitor instances:
0080
0081 - ``#define DECLARE_DA_MON_GLOBAL(name, type)``
0082 - ``#define DECLARE_DA_MON_PER_CPU(name, type)``
0083 - ``#define DECLARE_DA_MON_PER_TASK(name, type)``
0084
0085 The first declares the functions for a global deterministic automata monitor,
0086 the second for monitors with per-cpu instances, and the third with per-task
0087 instances.
0088
0089 In all cases, the 'name' argument is a string that identifies the monitor, and
0090 the 'type' argument is the data type used by dot2k on the representation of
0091 the model in C.
0092
0093 For example, the wip model with two states and three events can be
0094 stored in an 'unsigned char' type. Considering that the preemption control
0095 is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::
0096
0097 DECLARE_DA_MON_PER_CPU(wip, unsigned char);
0098
0099 The monitor is executed by sending events to be processed via the functions
0100 presented below::
0101
0102 da_handle_event_$(MONITOR_NAME)($(event from event enum));
0103 da_handle_start_event_$(MONITOR_NAME)($(event from event enum));
0104 da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum));
0105
0106 The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where
0107 the event will be processed if the monitor is processing events.
0108
0109 When a monitor is enabled, it is placed in the initial state of the automata.
0110 However, the monitor does not know if the system is in the *initial state*.
0111
0112 The ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the
0113 monitor that the system is returning to the initial state, so the monitor can
0114 start monitoring the next event.
0115
0116 The ``da_handle_start_run_event_$(MONITOR_NAME)()`` function is used to notify
0117 the monitor that the system is known to be in the initial state, so the
0118 monitor can start monitoring and monitor the current event.
0119
0120 Using the wip model as example, the events "preempt_disable" and
0121 "sched_waking" should be sent to monitor, respectively, via [2]::
0122
0123 da_handle_event_wip(preempt_disable_wip);
0124 da_handle_event_wip(sched_waking_wip);
0125
0126 While the event "preempt_enabled" will use::
0127
0128 da_handle_start_event_wip(preempt_enable_wip);
0129
0130 To notify the monitor that the system will be returning to the initial state,
0131 so the system and the monitor should be in sync.
0132
0133 Final remarks
0134 -------------
0135
0136 With the monitor synthesis in place using the rv/da_monitor.h and
0137 dot2k, the developer's work should be limited to the instrumentation
0138 of the system, increasing the confidence in the overall approach.
0139
0140 [1] For details about deterministic automata format and the translation
0141 from one representation to another, see::
0142
0143 Documentation/trace/rv/deterministic_automata.rst
0144
0145 [2] dot2k appends the monitor's name suffix to the events enums to
0146 avoid conflicting variables when exporting the global vmlinux.h
0147 use by BPF programs.
