Lines Matching refs:monitor
8 The formal representation needs to be then *synthesized* into a *monitor*
10 *monitor* connects to the system via an *instrumentation* that converts
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
39 DA monitor synthesis
42 The synthesis of automata-based models into the Linux *RV monitor* abstraction
44 contains a set of macros that automatically generate the monitor's code.
51 a kernel monitor in C.
54 [1] into a per-cpu monitor with the following command::
61 - wip.c: the RV monitor
63 The wip.c file contains the monitor declaration and the starting point for
72 The benefits of the usage of macro for monitor synthesis are 3-fold as it:
76 - Avoids the case of developers changing the core of the monitor code
79 This initial implementation presents three different types of monitor instances:
85 The first declares the functions for a global deterministic automata monitor,
89 In all cases, the 'name' argument is a string that identifies the monitor, and
95 is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::
99 The monitor is executed by sending events to be processed via the functions
107 the event will be processed if the monitor is processing events.
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
118 monitor can start monitoring and monitor the current event.
121 "sched_waking" should be sent to monitor, respectively, via [2]::
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.
136 With the monitor synthesis in place using the rv/da_monitor.h and
145 [2] dot2k appends the monitor's name suffix to the events enums to