1 Deterministic Automata Monitor Synthesis 1 Deterministic Automata Monitor Synthesis
2 ======================================== 2 ========================================
3 3
4 The starting point for the application of runt 4 The starting point for the application of runtime verification (RV) techniques
5 is the *specification* or *modeling* of the de 5 is the *specification* or *modeling* of the desired (or undesired) behavior
6 of the system under scrutiny. 6 of the system under scrutiny.
7 7
8 The formal representation needs to be then *sy 8 The formal representation needs to be then *synthesized* into a *monitor*
9 that can then be used in the analysis of the t 9 that can then be used in the analysis of the trace of the system. The
10 *monitor* connects to the system via an *instr 10 *monitor* connects to the system via an *instrumentation* that converts
11 the events from the *system* to the events of 11 the events from the *system* to the events of the *specification*.
12 12
13 13
14 In Linux terms, the runtime verification monit 14 In Linux terms, the runtime verification monitors are encapsulated inside
15 the *RV monitor* abstraction. The RV monitor i 15 the *RV monitor* abstraction. The RV monitor includes a set of instances
16 of the monitor (per-cpu monitor, per-task moni 16 of the monitor (per-cpu monitor, per-task monitor, and so on), the helper
17 functions that glue the monitor to the system 17 functions that glue the monitor to the system reference model, and the
18 trace output as a reaction to event parsing an 18 trace output as a reaction to event parsing and exceptions, as depicted
19 below:: 19 below::
20 20
21 Linux +----- RV Monitor -------------------- 21 Linux +----- RV Monitor ----------------------------------+ Formal
22 Realm | 22 Realm | | Realm
23 +-------------------+ +----------------+ 23 +-------------------+ +----------------+ +-----------------+
24 | Linux kernel | | Monitor | 24 | Linux kernel | | Monitor | | Reference |
25 | Tracing | -> | Instance(s) | 25 | Tracing | -> | Instance(s) | <- | Model |
26 | (instrumentation) | | (verification) | 26 | (instrumentation) | | (verification) | | (specification) |
27 +-------------------+ +----------------+ 27 +-------------------+ +----------------+ +-----------------+
28 | | 28 | | |
29 | V 29 | V |
30 | +----------+ 30 | +----------+ |
31 | | Reaction | 31 | | Reaction | |
32 | +--+--+--+-+ 32 | +--+--+--+-+ |
33 | | | | 33 | | | | |
34 | | | +-> tr 34 | | | +-> trace output ? |
35 +------------------------|--|-------- 35 +------------------------|--|----------------------+
36 | +----> pa 36 | +----> panic ?
37 +-------> <u 37 +-------> <user-specified>
38 38
39 DA monitor synthesis 39 DA monitor synthesis
40 -------------------- 40 --------------------
41 41
42 The synthesis of automata-based models into th 42 The synthesis of automata-based models into the Linux *RV monitor* abstraction
43 is automated by the dot2k tool and the rv/da_m 43 is automated by the dot2k tool and the rv/da_monitor.h header file that
44 contains a set of macros that automatically ge 44 contains a set of macros that automatically generate the monitor's code.
45 45
46 dot2k 46 dot2k
47 ----- 47 -----
48 48
49 The dot2k utility leverages dot2c by convertin 49 The dot2k utility leverages dot2c by converting an automaton model in
50 the DOT format into the C representation [1] a 50 the DOT format into the C representation [1] and creating the skeleton of
51 a kernel monitor in C. 51 a kernel monitor in C.
52 52
53 For example, it is possible to transform the w 53 For example, it is possible to transform the wip.dot model present in
54 [1] into a per-cpu monitor with the following 54 [1] into a per-cpu monitor with the following command::
55 55
56 $ dot2k -d wip.dot -t per_cpu 56 $ dot2k -d wip.dot -t per_cpu
57 57
58 This will create a directory named wip/ with t 58 This will create a directory named wip/ with the following files:
59 59
60 - wip.h: the wip model in C 60 - wip.h: the wip model in C
61 - wip.c: the RV monitor 61 - wip.c: the RV monitor
62 62
63 The wip.c file contains the monitor declaratio 63 The wip.c file contains the monitor declaration and the starting point for
64 the system instrumentation. 64 the system instrumentation.
65 65
66 Monitor macros 66 Monitor macros
67 -------------- 67 --------------
68 68
69 The rv/da_monitor.h enables automatic code gen 69 The rv/da_monitor.h enables automatic code generation for the *Monitor
70 Instance(s)* using C macros. 70 Instance(s)* using C macros.
71 71
72 The benefits of the usage of macro for monitor 72 The benefits of the usage of macro for monitor synthesis are 3-fold as it:
73 73
74 - Reduces the code duplication; 74 - Reduces the code duplication;
75 - Facilitates the bug fix/improvement; 75 - Facilitates the bug fix/improvement;
76 - Avoids the case of developers changing the c 76 - Avoids the case of developers changing the core of the monitor code
77 to manipulate the model in a (let's say) non 77 to manipulate the model in a (let's say) non-standard way.
78 78
79 This initial implementation presents three dif 79 This initial implementation presents three different types of monitor instances:
80 80
81 - ``#define DECLARE_DA_MON_GLOBAL(name, type)` 81 - ``#define DECLARE_DA_MON_GLOBAL(name, type)``
82 - ``#define DECLARE_DA_MON_PER_CPU(name, type) 82 - ``#define DECLARE_DA_MON_PER_CPU(name, type)``
83 - ``#define DECLARE_DA_MON_PER_TASK(name, type 83 - ``#define DECLARE_DA_MON_PER_TASK(name, type)``
84 84
85 The first declares the functions for a global 85 The first declares the functions for a global deterministic automata monitor,
86 the second for monitors with per-cpu instances 86 the second for monitors with per-cpu instances, and the third with per-task
87 instances. 87 instances.
88 88
89 In all cases, the 'name' argument is a string 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 d 90 the 'type' argument is the data type used by dot2k on the representation of
91 the model in C. 91 the model in C.
92 92
93 For example, the wip model with two states and 93 For example, the wip model with two states and three events can be
94 stored in an 'unsigned char' type. Considering 94 stored in an 'unsigned char' type. Considering that the preemption control
95 is a per-cpu behavior, the monitor declaration 95 is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::
96 96
97 DECLARE_DA_MON_PER_CPU(wip, unsigned char); 97 DECLARE_DA_MON_PER_CPU(wip, unsigned char);
98 98
99 The monitor is executed by sending events to b 99 The monitor is executed by sending events to be processed via the functions
100 presented below:: 100 presented below::
101 101
102 da_handle_event_$(MONITOR_NAME)($(event from 102 da_handle_event_$(MONITOR_NAME)($(event from event enum));
103 da_handle_start_event_$(MONITOR_NAME)($(even 103 da_handle_start_event_$(MONITOR_NAME)($(event from event enum));
104 da_handle_start_run_event_$(MONITOR_NAME)($( 104 da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum));
105 105
106 The function ``da_handle_event_$(MONITOR_NAME) 106 The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where
107 the event will be processed if the monitor is 107 the event will be processed if the monitor is processing events.
108 108
109 When a monitor is enabled, it is placed in the 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 syst 110 However, the monitor does not know if the system is in the *initial state*.
111 111
112 The ``da_handle_start_event_$(MONITOR_NAME)()` 112 The ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the
113 monitor that the system is returning to the in 113 monitor that the system is returning to the initial state, so the monitor can
114 start monitoring the next event. 114 start monitoring the next event.
115 115
116 The ``da_handle_start_run_event_$(MONITOR_NAME 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 117 the monitor that the system is known to be in the initial state, so the
118 monitor can start monitoring and monitor the c 118 monitor can start monitoring and monitor the current event.
119 119
120 Using the wip model as example, the events "pr 120 Using the wip model as example, the events "preempt_disable" and
121 "sched_waking" should be sent to monitor, resp 121 "sched_waking" should be sent to monitor, respectively, via [2]::
122 122
123 da_handle_event_wip(preempt_disable_wip); 123 da_handle_event_wip(preempt_disable_wip);
124 da_handle_event_wip(sched_waking_wip); 124 da_handle_event_wip(sched_waking_wip);
125 125
126 While the event "preempt_enabled" will use:: 126 While the event "preempt_enabled" will use::
127 127
128 da_handle_start_event_wip(preempt_enable_wip 128 da_handle_start_event_wip(preempt_enable_wip);
129 129
130 To notify the monitor that the system will be 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 syn 131 so the system and the monitor should be in sync.
132 132
133 Final remarks 133 Final remarks
134 ------------- 134 -------------
135 135
136 With the monitor synthesis in place using the 136 With the monitor synthesis in place using the rv/da_monitor.h and
137 dot2k, the developer's work should be limited 137 dot2k, the developer's work should be limited to the instrumentation
138 of the system, increasing the confidence in th 138 of the system, increasing the confidence in the overall approach.
139 139
140 [1] For details about deterministic automata f 140 [1] For details about deterministic automata format and the translation
141 from one representation to another, see:: 141 from one representation to another, see::
142 142
143 Documentation/trace/rv/deterministic_automat 143 Documentation/trace/rv/deterministic_automata.rst
144 144
145 [2] dot2k appends the monitor's name suffix to 145 [2] dot2k appends the monitor's name suffix to the events enums to
146 avoid conflicting variables when exporting the 146 avoid conflicting variables when exporting the global vmlinux.h
147 use by BPF programs. 147 use by BPF programs.
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.