Lines Matching +full:realm +full:-
16 of the monitor (per-cpu monitor, per-task monitor, and so on), the helper
21 Linux +----- RV Monitor ----------------------------------+ Formal
22 Realm | | Realm
23 +-------------------+ +----------------+ +-----------------+
25 | Tracing | -> | Instance(s) | <- | Model |
27 +-------------------+ +----------------+ +-----------------+
30 | +----------+ |
32 | +--+--+--+-+ |
34 | | | +-> trace output ? |
35 +------------------------|--|----------------------+
36 | +----> panic ?
37 +-------> <user-specified>
40 --------------------
50 -----
56 [1] into a per-cpu monitor with the following command::
58 $ rvgen monitor -c da -s wip.dot -t per_cpu
62 - wip.h: the wip model in C
63 - wip.c: the RV monitor
71 $ rvgen monitor -c ltl -s pagefault.ltl -t per_task
75 - pagefault.h: The Buchi automaton (the non-deterministic state machine to
77 - pagefault.c: The skeleton for the RV monitor
80 --------------------
84 - `rv/da_monitor.h` for deterministic automaton monitor
85 - `rv/ltl_monitor` for linear temporal logic monitor
91 3-fold:
93 - Reduce the code duplication;
94 - Facilitate the bug fix/improvement;
95 - Avoid the case of developers changing the core of the monitor code to
96 manipulate the model in a (let's say) non-standard way.
103 - ``#define DECLARE_DA_MON_GLOBAL(name, type)``
104 - ``#define DECLARE_DA_MON_PER_CPU(name, type)``
105 - ``#define DECLARE_DA_MON_PER_TASK(name, type)``
108 the second for monitors with per-cpu instances, and the third with per-task
117 is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::
167 implementation of the Buchi automaton - a non-deterministic state machine that
204 This LTL states that a real-time task does not raise page faults. For this
258 -------------