trace/rv/da_monitor_synthesis.rst

16 of the monitor (per-cpu monitor, per-task monitor, and so on), the helper
21  Linux  +----- RV Monitor ----------------------------------+ Formal
23   +-------------------+     +----------------+     +-----------------+
25   |     Tracing       |  -> |   Instance(s)  | <-  |       Model     |
27   +-------------------+     +----------------+     +-----------------+
30          |                     +----------+                 |
32          |                     +--+--+--+-+                 |
34          |                        |  |  +-> trace output ?  |
35          +------------------------|--|----------------------+
36                                   |  +----> panic ?
37                                   +-------> <user-specified>
40 --------------------
42 The synthesis of automata-based models into the Linux *RV monitor* abstraction
47 -----
54 [1] into a per-cpu monitor with the following command::
56   $ dot2k -d wip.dot -t per_cpu
60 - wip.h: the wip model in C
61 - wip.c: the RV monitor
67 --------------
72 The benefits of the usage of macro for monitor synthesis are 3-fold as it:
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.
79 This initial implementation presents three different types of monitor instances:
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)``
86 the second for monitors with per-cpu instances, and the third with per-task
93 For example, the wip model with two states and three events can be
95 is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::
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*.
113 monitor that the system is returning to the initial state, so the monitor can
117 the monitor that the system is known to be in the initial state, so the
130 To notify the monitor that the system will be returning to the initial state,
134 -------------