sphinx.addnodesdocument)}( rawsourcechildren]( translations LanguagesNode)}(hhh](h pending_xref)}(hhh]docutils.nodesTextChinese (Simplified)}parenthsba attributes}(ids]classes]names]dupnames]backrefs] refdomainstdreftypedoc reftarget./translations/zh_CN/trace/rv/monitor_synthesismodnameN classnameN refexplicitutagnamehhh ubh)}(hhh]hChinese (Traditional)}hh2sbah}(h]h ]h"]h$]h&] refdomainh)reftypeh+ reftarget./translations/zh_TW/trace/rv/monitor_synthesismodnameN classnameN refexplicituh1hhh ubh)}(hhh]hItalian}hhFsbah}(h]h ]h"]h$]h&] refdomainh)reftypeh+ reftarget./translations/it_IT/trace/rv/monitor_synthesismodnameN classnameN refexplicituh1hhh ubh)}(hhh]hJapanese}hhZsbah}(h]h ]h"]h$]h&] refdomainh)reftypeh+ reftarget./translations/ja_JP/trace/rv/monitor_synthesismodnameN classnameN refexplicituh1hhh ubh)}(hhh]hKorean}hhnsbah}(h]h ]h"]h$]h&] refdomainh)reftypeh+ reftarget./translations/ko_KR/trace/rv/monitor_synthesismodnameN classnameN refexplicituh1hhh ubh)}(hhh]hPortuguese (Brazilian)}hhsbah}(h]h ]h"]h$]h&] refdomainh)reftypeh+ reftarget./translations/pt_BR/trace/rv/monitor_synthesismodnameN classnameN refexplicituh1hhh ubh)}(hhh]hSpanish}hhsbah}(h]h ]h"]h$]h&] refdomainh)reftypeh+ reftarget./translations/sp_SP/trace/rv/monitor_synthesismodnameN classnameN refexplicituh1hhh ubeh}(h]h ]h"]h$]h&]current_languageEnglishuh1h hh _documenthsourceNlineNubhsection)}(hhh](htitle)}(h&Runtime Verification Monitor Synthesish]h&Runtime Verification Monitor Synthesis}(hhhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhhhH/var/lib/git/docbuild/linux/Documentation/trace/rv/monitor_synthesis.rsthKubh paragraph)}(hThe starting point for the application of runtime verification (RV) techniques is the *specification* or *modeling* of the desired (or undesired) behavior of the system under scrutiny.h](hVThe starting point for the application of runtime verification (RV) techniques is the }(hhhhhNhNubhemphasis)}(h*specification*h]h specification}(hhhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhubh or }(hhhhhNhNubh)}(h *modeling*h]hmodeling}(hhhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhubhE of the desired (or undesired) behavior of the system under scrutiny.}(hhhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhhhhubh)}(hXThe formal representation needs to be then *synthesized* into a *monitor* that can then be used in the analysis of the trace of the system. The *monitor* connects to the system via an *instrumentation* that converts the events from the *system* to the events of the *specification*.h](h+The formal representation needs to be then }(hjhhhNhNubh)}(h *synthesized*h]h synthesized}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhjubh into a }(hjhhhNhNubh)}(h *monitor*h]hmonitor}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhjubhG that can then be used in the analysis of the trace of the system. The }(hjhhhNhNubh)}(h *monitor*h]hmonitor}(hj-hhhNhNubah}(h]h ]h"]h$]h&]uh1hhjubh connects to the system via an }(hjhhhNhNubh)}(h*instrumentation*h]hinstrumentation}(hj?hhhNhNubah}(h]h ]h"]h$]h&]uh1hhjubh# that converts the events from the }(hjhhhNhNubh)}(h*system*h]hsystem}(hjQhhhNhNubah}(h]h ]h"]h$]h&]uh1hhjubh to the events of the }(hjhhhNhNubh)}(h*specification*h]h specification}(hjchhhNhNubah}(h]h ]h"]h$]h&]uh1hhjubh.}(hjhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhhhhubh)}(hXsIn Linux terms, the runtime verification monitors are encapsulated inside the *RV monitor* abstraction. The RV monitor includes a set of instances of the monitor (per-cpu monitor, per-task monitor, and so on), the helper functions that glue the monitor to the system reference model, and the trace output as a reaction to event parsing and exceptions, as depicted below::h](hNIn Linux terms, the runtime verification monitors are encapsulated inside the }(hj{hhhNhNubh)}(h *RV monitor*h]h RV monitor}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhj{ubhX abstraction. The RV monitor includes a set of instances of the monitor (per-cpu monitor, per-task monitor, and so on), the helper functions that glue the monitor to the system reference model, and the trace output as a reaction to event parsing and exceptions, as depicted below:}(hj{hhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhhhhubh literal_block)}(hX<Linux +---- RV Monitor ----------------------------------+ Formal Realm | | Realm +-------------------+ +----------------+ +-----------------+ | Linux kernel | | Monitor | | Reference | | Tracing | -> | Instance(s) | <- | Model | | (instrumentation) | | (verification) | | (specification) | +-------------------+ +----------------+ +-----------------+ | | | | V | | +----------+ | | | Reaction | | | +--+--+--+-+ | | | | | | | | | +-> trace output ? | +------------------------|--|----------------------+ | +----> panic ? +-------> h]hX<Linux +---- RV Monitor ----------------------------------+ Formal Realm | | Realm +-------------------+ +----------------+ +-----------------+ | Linux kernel | | Monitor | | Reference | | Tracing | -> | Instance(s) | <- | Model | | (instrumentation) | | (verification) | | (specification) | +-------------------+ +----------------+ +-----------------+ | | | | V | | +----------+ | | | Reaction | | | +--+--+--+-+ | | | | | | | | | +-> trace output ? | +------------------------|--|----------------------+ | +----> panic ? +-------> }hjsbah}(h]h ]h"]h$]h&] xml:spacepreserveuh1jhhhKhhhhubh)}(hhh](h)}(hRV monitor synthesish]hRV monitor synthesis}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhjhhhhhK(ubh)}(hThe synthesis of a specification into the Linux *RV monitor* abstraction is automated by the rvgen tool and the header file containing common code for creating monitors. The header files are:h](h0The synthesis of a specification into the Linux }(hjhhhNhNubh)}(h *RV monitor*h]h RV monitor}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhjubh abstraction is automated by the rvgen tool and the header file containing common code for creating monitors. The header files are:}(hjhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhK*hjhhubh block_quote)}(h* rv/da_monitor.h for deterministic automaton monitor. * rv/ltl_monitor.h for linear temporal logic monitor. * rv/ha_monitor.h for hybrid automaton monitor. h]h bullet_list)}(hhh](h list_item)}(h4rv/da_monitor.h for deterministic automaton monitor.h]h)}(hjh]h4rv/da_monitor.h for deterministic automaton monitor.}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhK.hjubah}(h]h ]h"]h$]h&]uh1jhjubj)}(h3rv/ltl_monitor.h for linear temporal logic monitor.h]h)}(hjh]h3rv/ltl_monitor.h for linear temporal logic monitor.}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhK/hjubah}(h]h ]h"]h$]h&]uh1jhjubj)}(h.rv/ha_monitor.h for hybrid automaton monitor. h]h)}(h-rv/ha_monitor.h for hybrid automaton monitor.h]h-rv/ha_monitor.h for hybrid automaton monitor.}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhK0hjubah}(h]h ]h"]h$]h&]uh1jhjubeh}(h]h ]h"]h$]h&]bullet*uh1jhhhK.hjubah}(h]h ]h"]h$]h&]uh1jhhhK.hjhhubeh}(h]rv-monitor-synthesisah ]h"]rv monitor synthesisah$]h&]uh1hhhhhhhhK(ubh)}(hhh](h)}(hrvgenh]hrvgen}(hjJhhhNhNubah}(h]h ]h"]h$]h&]uh1hhjGhhhhhK3ubh)}(hvThe rvgen utility converts a specification into the C presentation and creating the skeleton of a kernel monitor in C.h]hvThe rvgen utility converts a specification into the C presentation and creating the skeleton of a kernel monitor in C.}(hjXhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhK5hjGhhubh)}(h}For example, it is possible to transform the wip.dot model present in [1] into a per-cpu monitor with the following command::h]h|For example, it is possible to transform the wip.dot model present in [1] into a per-cpu monitor with the following command:}(hjfhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhK8hjGhhubj)}(h+$ rvgen monitor -c da -s wip.dot -t per_cpuh]h+$ rvgen monitor -c da -s wip.dot -t per_cpu}hjtsbah}(h]h ]h"]h$]h&]jjuh1jhhhK;hjGhhubh)}(hAThis will create a directory named wip/ with the following files:h]hAThis will create a directory named wip/ with the following files:}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhK=hjGhhubj)}(hhh](j)}(hwip.h: the wip model in Ch]h)}(hjh]hwip.h: the wip model in C}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhK?hjubah}(h]h ]h"]h$]h&]uh1jhjhhhhhNubj)}(hwip.c: the RV monitor h]h)}(hwip.c: the RV monitorh]hwip.c: the RV monitor}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhK@hjubah}(h]h ]h"]h$]h&]uh1jhjhhhhhNubeh}(h]h ]h"]h$]h&]j7-uh1jhhhK?hjGhhubh)}(hfThe wip.c file contains the monitor declaration and the starting point for the system instrumentation.h]hfThe wip.c file contains the monitor declaration and the starting point for the system instrumentation.}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKBhjGhhubh)}(hXSimilarly, a linear temporal logic monitor can be generated with the following command::h]hWSimilarly, a linear temporal logic monitor can be generated with the following command:}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKEhjGhhubj)}(h3$ rvgen monitor -c ltl -s pagefault.ltl -t per_taskh]h3$ rvgen monitor -c ltl -s pagefault.ltl -t per_task}hjsbah}(h]h ]h"]h$]h&]jjuh1jhhhKHhjGhhubh)}(h)This generates pagefault/ directory with:h]h)This generates pagefault/ directory with:}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKJhjGhhubj)}(hhh](j)}(hbpagefault.h: The Buchi automaton (the non-deterministic state machine to verify the specification)h]h)}(hbpagefault.h: The Buchi automaton (the non-deterministic state machine to verify the specification)h]hbpagefault.h: The Buchi automaton (the non-deterministic state machine to verify the specification)}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKLhjubah}(h]h ]h"]h$]h&]uh1jhjhhhhhNubj)}(h-pagefault.c: The skeleton for the RV monitor h]h)}(h,pagefault.c: The skeleton for the RV monitorh]h,pagefault.c: The skeleton for the RV monitor}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKNhjubah}(h]h ]h"]h$]h&]uh1jhjhhhhhNubeh}(h]h ]h"]h$]h&]j7juh1jhhhKLhjGhhubeh}(h]rvgenah ]h"]rvgenah$]h&]uh1hhhhhhhhK3ubh)}(hhh](h)}(hMonitor header filesh]hMonitor header files}(hjEhhhNhNubah}(h]h ]h"]h$]h&]uh1hhjBhhhhhKQubh)}(hThe header files:h]hThe header files:}(hjShhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKShjBhhubj)}(hhh](j)}(h5`rv/da_monitor.h` for deterministic automaton monitorh]h)}(hjfh](htitle_reference)}(h`rv/da_monitor.h`h]hrv/da_monitor.h}(hjmhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjhubh$ for deterministic automaton monitor}(hjhhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKUhjdubah}(h]h ]h"]h$]h&]uh1jhjahhhhhNubj)}(h3`rv/ltl_monitor` for linear temporal logic monitor h]h)}(h2`rv/ltl_monitor` for linear temporal logic monitorh](jl)}(h`rv/ltl_monitor`h]hrv/ltl_monitor}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubh" for linear temporal logic monitor}(hjhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKVhjubah}(h]h ]h"]h$]h&]uh1jhjahhhhhNubeh}(h]h ]h"]h$]h&]j7juh1jhhhKUhjBhhubh)}(hRinclude common macros and static functions for implementing *Monitor Instance(s)*.h](hhhhhhKdubh)}(hPThis initial implementation presents three different types of monitor instances:h]hPThis initial implementation presents three different types of monitor instances:}(hjOhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKfhj>hhubj)}(hhh](j)}(h%``#define RV_MON_TYPE RV_MON_GLOBAL``h]h)}(hjbh]hliteral)}(hjbh]h!#define RV_MON_TYPE RV_MON_GLOBAL}(hjihhhNhNubah}(h]h ]h"]h$]h&]uh1jghjdubah}(h]h ]h"]h$]h&]uh1hhhhKhhj`ubah}(h]h ]h"]h$]h&]uh1jhj]hhhhhNubj)}(h&``#define RV_MON_TYPE RV_MON_PER_CPU``h]h)}(hjh]jh)}(hjh]h"#define RV_MON_TYPE RV_MON_PER_CPU}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jghjubah}(h]h ]h"]h$]h&]uh1hhhhKihjubah}(h]h ]h"]h$]h&]uh1jhj]hhhhhNubj)}(h(``#define RV_MON_TYPE RV_MON_PER_TASK`` h]h)}(h'``#define RV_MON_TYPE RV_MON_PER_TASK``h]jh)}(hjh]h##define RV_MON_TYPE RV_MON_PER_TASK}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jghjubah}(h]h ]h"]h$]h&]uh1hhhhKjhjubah}(h]h ]h"]h$]h&]uh1jhj]hhhhhNubeh}(h]h ]h"]h$]h&]j7juh1jhhhKhhj>hhubh)}(hThe first sets up functions declaration for a global deterministic automata monitor, the second for monitors with per-cpu instances, and the third with per-task instances.h]hThe first sets up functions declaration for a global deterministic automata monitor, the second for monitors with per-cpu instances, and the third with per-task instances.}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKlhj>hhubh)}(hIn all cases, the C file must include the $(MODEL_NAME).h file (generated by `rvgen`), for example, to define the per-cpu 'wip' monitor, the `wip.c` source file must include::h](hMIn all cases, the C file must include the $(MODEL_NAME).h file (generated by }(hjhhhNhNubjl)}(h`rvgen`h]hrvgen}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubh=), for example, to define the per-cpu ‘wip’ monitor, the }(hjhhhNhNubjl)}(h`wip.c`h]hwip.c}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubh source file must include:}(hjhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKphj>hhubj)}(hN#define RV_MON_TYPE RV_MON_PER_CPU #include "wip.h" #include h]hN#define RV_MON_TYPE RV_MON_PER_CPU #include "wip.h" #include }hj sbah}(h]h ]h"]h$]h&]jjuh1jhhhKthj>hhubh)}(h]The monitor is executed by sending events to be processed via the functions presented below::h]h\The monitor is executed by sending events to be processed via the functions presented below:}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKxhj>hhubj)}(hda_handle_event($(event from event enum)); da_handle_start_event($(event from event enum)); da_handle_start_run_event($(event from event enum));h]hda_handle_event($(event from event enum)); da_handle_start_event($(event from event enum)); da_handle_start_run_event($(event from event enum));}hj%sbah}(h]h ]h"]h$]h&]jjuh1jhhhK{hj>hhubh)}(h}The function ``da_handle_event()`` is the regular case where the event will be processed if the monitor is processing events.h](h The function }(hj3hhhNhNubjh)}(h``da_handle_event()``h]hda_handle_event()}(hj;hhhNhNubah}(h]h ]h"]h$]h&]uh1jghj3ubh[ is the regular case where the event will be processed if the monitor is processing events.}(hj3hhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhj>hhubh)}(hWhen a monitor is enabled, it is placed in the initial state of the automata. However, the monitor does not know if the system is in the *initial state*.h](hWhen a monitor is enabled, it is placed in the initial state of the automata. However, the monitor does not know if the system is in the }(hjShhhNhNubh)}(h*initial state*h]h initial state}(hj[hhhNhNubah}(h]h ]h"]h$]h&]uh1hhjSubh.}(hjShhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhj>hhubh)}(hThe ``da_handle_start_event()`` function is used to notify the monitor that the system is returning to the initial state, so the monitor can start monitoring the next event.h](hThe }(hjshhhNhNubjh)}(h``da_handle_start_event()``h]hda_handle_start_event()}(hj{hhhNhNubah}(h]h ]h"]h$]h&]uh1jghjsubh function is used to notify the monitor that the system is returning to the initial state, so the monitor can start monitoring the next event.}(hjshhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhj>hhubh)}(hThe ``da_handle_start_run_event()`` function is used to notify the monitor that the system is known to be in the initial state, so the monitor can start monitoring and monitor the current event.h](hThe }(hjhhhNhNubjh)}(h``da_handle_start_run_event()``h]hda_handle_start_run_event()}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jghjubh function is used to notify the monitor that the system is known to be in the initial state, so the monitor can start monitoring and monitor the current event.}(hjhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhj>hhubh)}(hUsing the wip model as example, the events "preempt_disable" and "sched_waking" should be sent to monitor, respectively, via [2]::h]hUsing the wip model as example, the events “preempt_disable” and “sched_waking” should be sent to monitor, respectively, via [2]:}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKhj>hhubj)}(hHda_handle_event(preempt_disable_wip); da_handle_event(sched_waking_wip);h]hHda_handle_event(preempt_disable_wip); da_handle_event(sched_waking_wip);}hjsbah}(h]h ]h"]h$]h&]jjuh1jhhhKhj>hhubh)}(h,While the event "preempt_enabled" will use::h]h/While the event “preempt_enabled” will use:}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKhj>hhubj)}(h*da_handle_start_event(preempt_enable_wip);h]h*da_handle_start_event(preempt_enable_wip);}hjsbah}(h]h ]h"]h$]h&]jjuh1jhhhKhj>hhubh)}(h~To notify the monitor that the system will be returning to the initial state, so the system and the monitor should be in sync.h]h~To notify the monitor that the system will be returning to the initial state, so the system and the monitor should be in sync.}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKhj>hhubeh}(h]rv-da-monitor-hah ]h"]rv/da_monitor.hah$]h&]uh1hhjBhhhhhKdubh)}(hhh](h)}(hrv/ltl_monitor.hh]hrv/ltl_monitor.h}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhjhhhhhKubh)}(hThis file must be combined with the $(MODEL_NAME).h file (generated by `rvgen`) to be complete. For example, for the `pagefault` monitor, the `pagefault.c` source file must include::h](hGThis file must be combined with the $(MODEL_NAME).h file (generated by }(hjhhhNhNubjl)}(h`rvgen`h]hrvgen}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubh') to be complete. For example, for the }(hjhhhNhNubjl)}(h `pagefault`h]h pagefault}(hj,hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubh monitor, the }(hjhhhNhNubjl)}(h `pagefault.c`h]h pagefault.c}(hj>hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubh source file must include:}(hjhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhjhhubj)}(h2#include "pagefault.h" #include h]h2#include "pagefault.h" #include }hjVsbah}(h]h ]h"]h$]h&]jjuh1jhhhKhjhhubh)}(hC(the skeleton monitor file generated by `rvgen` already does this).h](h((the skeleton monitor file generated by }(hjdhhhNhNubjl)}(h`rvgen`h]hrvgen}(hjlhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjdubh already does this).}(hjdhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhjhhubh)}(hXg`$(MODEL_NAME).h` (`pagefault.h` in the above example) includes the implementation of the Buchi automaton - a non-deterministic state machine that verifies the LTL specification. While `rv/ltl_monitor.h` includes the common helper functions to interact with the Buchi automaton and to implement an RV monitor. An important definition in `$(MODEL_NAME).h` is::h](jl)}(h`$(MODEL_NAME).h`h]h$(MODEL_NAME).h}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubh (}(hjhhhNhNubjl)}(h `pagefault.h`h]h pagefault.h}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubh in the above example) includes the implementation of the Buchi automaton - a non-deterministic state machine that verifies the LTL specification. While }(hjhhhNhNubjl)}(h`rv/ltl_monitor.h`h]hrv/ltl_monitor.h}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubh includes the common helper functions to interact with the Buchi automaton and to implement an RV monitor. An important definition in }(hjhhhNhNubjl)}(h`$(MODEL_NAME).h`h]h$(MODEL_NAME).h}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubh is:}(hjhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhjhhubj)}(hvenum ltl_atom { LTL_$(FIRST_ATOMIC_PROPOSITION), LTL_$(SECOND_ATOMIC_PROPOSITION), ... LTL_NUM_ATOM };h]hvenum ltl_atom { LTL_$(FIRST_ATOMIC_PROPOSITION), LTL_$(SECOND_ATOMIC_PROPOSITION), ... LTL_NUM_ATOM };}hjsbah}(h]h ]h"]h$]h&]jjuh1jhhhKhjhhubh)}(hwhich is the list of atomic propositions present in the LTL specification (prefixed with "LTL\_" to avoid name collision). This `enum` is passed to the functions interacting with the Buchi automaton.h](hwhich is the list of atomic propositions present in the LTL specification (prefixed with “LTL_” to avoid name collision). This }(hjhhhNhNubjl)}(h`enum`h]henum}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubhA is passed to the functions interacting with the Buchi automaton.}(hjhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhjhhubh)}(hX*While generating code, `rvgen` cannot understand the meaning of the atomic propositions. Thus, that task is left for manual work. The recommended practice is adding tracepoints to places where the atomic propositions change; and in the tracepoints' handlers: the Buchi automaton is executed using::h](hWhile generating code, }(hjhhhNhNubjl)}(h`rvgen`h]hrvgen}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubhX  cannot understand the meaning of the atomic propositions. Thus, that task is left for manual work. The recommended practice is adding tracepoints to places where the atomic propositions change; and in the tracepoints’ handlers: the Buchi automaton is executed using:}(hjhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhjhhubj)}(hNvoid ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)h]hNvoid ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)}hj$sbah}(h]h ]h"]h$]h&]jjuh1jhhhKhjhhubh)}(hwhich tells the Buchi automaton that the atomic proposition `atom` is now `value`. The Buchi automaton checks whether the LTL specification is still satisfied, and invokes the monitor's error tracepoint and the reactor if violation is detected.h](hhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubh everywhere.}(hjhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhjhhubh)}(hFor atomic propositions which act like events, they usually need to be set (or cleared) and then immediately cleared (or set). A convenient function is provided::h]hFor atomic propositions which act like events, they usually need to be set (or cleared) and then immediately cleared (or set). A convenient function is provided:}(hjVhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKhjhhubj)}(hMvoid ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)h]hMvoid ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)}hjdsbah}(h]h ]h"]h$]h&]jjuh1jhhhKhjhhubh)}(hwhich is equivalent to::h]hwhich is equivalent to:}(hjrhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKhjhhubj)}(hHltl_atom_update(task, atom, value); ltl_atom_update(task, atom, !value);h]hHltl_atom_update(task, atom, value); ltl_atom_update(task, atom, !value);}hjsbah}(h]h ]h"]h$]h&]jjuh1jhhhKhjhhubh)}(hSTo initialize the atomic propositions, the following function must be implemented::h]hRTo initialize the atomic propositions, the following function must be implemented:}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKhjhhubj)}(hUltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)h]hUltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)}hjsbah}(h]h ]h"]h$]h&]jjuh1jhhhKhjhhubh)}(hThis function is called for all running tasks when the monitor is enabled. It is also called for new tasks created after the enabling the monitor. It should initialize as many atomic propositions as possible, for example::h]hThis function is called for all running tasks when the monitor is enabled. It is also called for new tasks created after the enabling the monitor. It should initialize as many atomic propositions as possible, for example:}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhKhjhhubj)}(hvoid ltl_atom_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation) { ltl_atom_set(mon, LTL_RT, rt_task(task)); if (task_creation) ltl_atom_set(mon, LTL_PAGEFAULT, false); }h]hvoid ltl_atom_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation) { ltl_atom_set(mon, LTL_RT, rt_task(task)); if (task_creation) ltl_atom_set(mon, LTL_PAGEFAULT, false); }}hjsbah}(h]h ]h"]h$]h&]jjuh1jhhhKhjhhubh)}(hXAtomic propositions not initialized by `ltl_atom_init()` will stay in the unknown state until relevant tracepoints are hit, which can take some time. As monitoring for a task cannot be done until all atomic propositions is known for the task, the monitor may need some time to start validating tasks which have been running before the monitor is enabled. Therefore, it is recommended to start the tasks of interest after enabling the monitor.h](h'Atomic propositions not initialized by }(hjhhhNhNubjl)}(h`ltl_atom_init()`h]hltl_atom_init()}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1jkhjubhX will stay in the unknown state until relevant tracepoints are hit, which can take some time. As monitoring for a task cannot be done until all atomic propositions is known for the task, the monitor may need some time to start validating tasks which have been running before the monitor is enabled. Therefore, it is recommended to start the tasks of interest after enabling the monitor.}(hjhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhKhjhhubeh}(h]rv-ltl-monitor-hah ]h"]rv/ltl_monitor.hah$]h&]uh1hhjBhhhhhKubh)}(hhh](h)}(hrv/ha_monitor.hh]hrv/ha_monitor.h}(hjhhhNhNubah}(h]h ]h"]h$]h&]uh1hhjhhhhhMubh)}(hThe implementation of hybrid automaton monitors derives directly from the deterministic automaton one. Despite using a different header (``ha_monitor.h``) the functions to handle events are the same (e.g. ``da_handle_event``).h](hThe implementation of hybrid automaton monitors derives directly from the deterministic automaton one. Despite using a different header (}(hjhhhNhNubjh)}(h``ha_monitor.h``h]h ha_monitor.h}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jghjubh4) the functions to handle events are the same (e.g. }(hjhhhNhNubjh)}(h``da_handle_event``h]hda_handle_event}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jghjubh).}(hjhhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhMhjhhubh)}(hAdditionally, the `rvgen` tool populates skeletons for the ``ha_verify_constraint``, ``ha_get_env`` and ``ha_reset_env`` based on the monitor specification in the monitor source file.h](hAdditionally, the }(hj1 hhhNhNubjl)}(h`rvgen`h]hrvgen}(hj9 hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj1 ubh" tool populates skeletons for the }(hj1 hhhNhNubjh)}(h``ha_verify_constraint``h]hha_verify_constraint}(hjK hhhNhNubah}(h]h ]h"]h$]h&]uh1jghj1 ubh, }(hj1 hhhNhNubjh)}(h``ha_get_env``h]h ha_get_env}(hj] hhhNhNubah}(h]h ]h"]h$]h&]uh1jghj1 ubh and }(hj1 hhhNhNubjh)}(h``ha_reset_env``h]h ha_reset_env}(hjo hhhNhNubah}(h]h ]h"]h$]h&]uh1jghj1 ubh? based on the monitor specification in the monitor source file.}(hj1 hhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhMhjhhubh)}(hJ``ha_verify_constraint`` is typically ready as it is generated by `rvgen`:h](jh)}(h``ha_verify_constraint``h]hha_verify_constraint}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jghj ubh* is typically ready as it is generated by }(hj hhhNhNubjl)}(h`rvgen`h]hrvgen}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj ubh:}(hj hhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhM hjhhubj)}(hhh](j)}(hcstandard constraints on edges are turned into the form:: res = ha_get_env(ha_mon, ENV) < VALUE; h](h)}(h8standard constraints on edges are turned into the form::h]h7standard constraints on edges are turned into the form:}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhMhj ubj)}(h&res = ha_get_env(ha_mon, ENV) < VALUE;h]h&res = ha_get_env(ha_mon, ENV) < VALUE;}hj sbah}(h]h ]h"]h$]h&]jjuh1jhhhMhj ubeh}(h]h ]h"]h$]h&]uh1jhj hhhhhNubj)}(hKreset constraints are turned into the form:: ha_reset_env(ha_mon, ENV); h](h)}(h,reset constraints are turned into the form::h]h+reset constraints are turned into the form:}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhMhj ubj)}(hha_reset_env(ha_mon, ENV);h]hha_reset_env(ha_mon, ENV);}hj sbah}(h]h ]h"]h$]h&]jjuh1jhhhMhj ubeh}(h]h ]h"]h$]h&]uh1jhj hhhhhNubj)}(hXconstraints on the state are implemented using timers - armed before entering the state - cancelled while entering any other state - untouched if the state does not change as a result of the event - checked if the timer expired but the callback did not run - available implementation are `HA_TIMER_HRTIMER` and `HA_TIMER_WHEEL` - hrtimers are more precise but may have higher overhead - select by defining `HA_TIMER_TYPE` before including the header:: #define HA_TIMER_TYPE HA_TIMER_HRTIMER h](h)}(h5constraints on the state are implemented using timersh]h5constraints on the state are implemented using timers}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhMhj ubj)}(hhh](j)}(h armed before entering the state h]h)}(harmed before entering the stateh]harmed before entering the state}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhMhj ubah}(h]h ]h"]h$]h&]uh1jhj ubj)}(h)cancelled while entering any other state h]h)}(h(cancelled while entering any other stateh]h(cancelled while entering any other state}(hj5 hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhMhj1 ubah}(h]h ]h"]h$]h&]uh1jhj ubj)}(h@untouched if the state does not change as a result of the event h]h)}(h?untouched if the state does not change as a result of the eventh]h?untouched if the state does not change as a result of the event}(hjM hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhMhjI ubah}(h]h ]h"]h$]h&]uh1jhj ubj)}(h:checked if the timer expired but the callback did not run h]h)}(h9checked if the timer expired but the callback did not runh]h9checked if the timer expired but the callback did not run}(hje hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhMhja ubah}(h]h ]h"]h$]h&]uh1jhj ubj)}(havailable implementation are `HA_TIMER_HRTIMER` and `HA_TIMER_WHEEL` - hrtimers are more precise but may have higher overhead - select by defining `HA_TIMER_TYPE` before including the header:: #define HA_TIMER_TYPE HA_TIMER_HRTIMER h](h)}(hDavailable implementation are `HA_TIMER_HRTIMER` and `HA_TIMER_WHEEL`h](havailable implementation are }(hj} hhhNhNubjl)}(h`HA_TIMER_HRTIMER`h]hHA_TIMER_HRTIMER}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj} ubh and }(hj} hhhNhNubjl)}(h`HA_TIMER_WHEEL`h]hHA_TIMER_WHEEL}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj} ubeh}(h]h ]h"]h$]h&]uh1hhhhM hjy ubj)}(hhh](j)}(h7hrtimers are more precise but may have higher overhead h]h)}(h6hrtimers are more precise but may have higher overheadh]h6hrtimers are more precise but may have higher overhead}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhM"hj ubah}(h]h ]h"]h$]h&]uh1jhj ubj)}(hiselect by defining `HA_TIMER_TYPE` before including the header:: #define HA_TIMER_TYPE HA_TIMER_HRTIMER h](h)}(h@select by defining `HA_TIMER_TYPE` before including the header::h](hselect by defining }(hj hhhNhNubjl)}(h`HA_TIMER_TYPE`h]h HA_TIMER_TYPE}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj ubh before including the header:}(hj hhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhM$hj ubj)}(h&#define HA_TIMER_TYPE HA_TIMER_HRTIMERh]h&#define HA_TIMER_TYPE HA_TIMER_HRTIMER}hj sbah}(h]h ]h"]h$]h&]jjuh1jhhhM&hj ubeh}(h]h ]h"]h$]h&]uh1jhj ubeh}(h]h ]h"]h$]h&]j7juh1jhhhM"hjy ubeh}(h]h ]h"]h$]h&]uh1jhj ubeh}(h]h ]h"]h$]h&]j7juh1jhhhMhj ubeh}(h]h ]h"]h$]h&]uh1jhj hhhNhNubeh}(h]h ]h"]h$]h&]j7j8uh1jhhhMhjhhubh)}(h6Constraint values can be specified in different forms:h]h6Constraint values can be specified in different forms:}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhM(hjhhubj)}(hhh](j)}(h_literal value (with optional unit). E.g.:: preemptive == 0 clk < 100ns threshold <= 10j h](h)}(h*literal value (with optional unit). E.g.::h]h)literal value (with optional unit). E.g.:}(hj1 hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhM*hj- ubj)}(h,preemptive == 0 clk < 100ns threshold <= 10jh]h,preemptive == 0 clk < 100ns threshold <= 10j}hj? sbah}(h]h ]h"]h$]h&]jjuh1jhhhM,hj- ubeh}(h]h ]h"]h$]h&]uh1jhj* hhhhhNubj)}(h:constant value (uppercase string). E.g.:: clk < MAX_NS h](h)}(h)constant value (uppercase string). E.g.::h]h(constant value (uppercase string). E.g.:}(hjW hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhM0hjS ubj)}(h clk < MAX_NSh]h clk < MAX_NS}hje sbah}(h]h ]h"]h$]h&]jjuh1jhhhM2hjS ubeh}(h]h ]h"]h$]h&]uh1jhj* hhhhhNubj)}(hAparameter (lowercase string). E.g.:: clk <= threshold_jiffies h](h)}(h$parameter (lowercase string). E.g.::h]h#parameter (lowercase string). E.g.:}(hj} hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhM4hjy ubj)}(hclk <= threshold_jiffiesh]hclk <= threshold_jiffies}hj sbah}(h]h ]h"]h$]h&]jjuh1jhhhM6hjy ubeh}(h]h ]h"]h$]h&]uh1jhj* hhhhhNubj)}(hDmacro (uppercase string with parentheses). E.g.:: clk < MAX_NS() h](h)}(h1macro (uppercase string with parentheses). E.g.::h]h0macro (uppercase string with parentheses). E.g.:}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhM8hj ubj)}(hclk < MAX_NS()h]hclk < MAX_NS()}hj sbah}(h]h ]h"]h$]h&]jjuh1jhhhM:hj ubeh}(h]h ]h"]h$]h&]uh1jhj* hhhhhNubj)}(hSfunction (lowercase string with parentheses). E.g.:: clk <= threshold_jiffies() h](h)}(h4function (lowercase string with parentheses). E.g.::h]h3function (lowercase string with parentheses). E.g.:}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhM<hj ubj)}(hclk <= threshold_jiffies()h]hclk <= threshold_jiffies()}hj sbah}(h]h ]h"]h$]h&]jjuh1jhhhM>hj ubeh}(h]h ]h"]h$]h&]uh1jhj* hhhhhNubeh}(h]h ]h"]h$]h&]j7j8uh1jhhhM*hjhhubh)}(hX}In all cases, `rvgen` will try to understand the type of the environment variable from the name or unit. For instance, constants or parameters terminating with ``_NS`` or ``_jiffies`` are intended as clocks with ns and jiffy granularity, respectively. Literals with measure unit `j` are jiffies and if a time unit is specified (`ns` to `s`), `rvgen` will convert the value to `ns`.h](hIn all cases, }(hj hhhNhNubjl)}(h`rvgen`h]hrvgen}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj ubh will try to understand the type of the environment variable from the name or unit. For instance, constants or parameters terminating with }(hj hhhNhNubjh)}(h``_NS``h]h_NS}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jghj ubh or }(hj hhhNhNubjh)}(h ``_jiffies``h]h_jiffies}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jghj ubh` are intended as clocks with ns and jiffy granularity, respectively. Literals with measure unit }(hj hhhNhNubjl)}(h`j`h]hj}(hj/ hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj ubh. are jiffies and if a time unit is specified (}(hj hhhNhNubjl)}(h`ns`h]hns}(hjA hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj ubh to }(hj hhhNhNubjl)}(h`s`h]hs}(hjS hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj ubh), }(hj hhhNhNubjl)}(h`rvgen`h]hrvgen}(hje hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj ubh will convert the value to }(hj hhhNhNubjl)}(h`ns`h]hns}(hjw hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj ubh.}(hj hhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhM@hjhhubh)}(hXConstants need to be defined by the user (but unlike the name, they don't necessarily need to be defined as constants). Parameters get converted to module parameters and the user needs to provide a default value. Also function and macros are defined by the user, by default they get as an argument the ``ha_monitor``, a common usage would be to get the required value from the target, e.g. the task in per-task monitors, using the helper ``ha_get_target(ha_mon)``.h](hX0Constants need to be defined by the user (but unlike the name, they don’t necessarily need to be defined as constants). Parameters get converted to module parameters and the user needs to provide a default value. Also function and macros are defined by the user, by default they get as an argument the }(hj hhhNhNubjh)}(h``ha_monitor``h]h ha_monitor}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jghj ubhz, a common usage would be to get the required value from the target, e.g. the task in per-task monitors, using the helper }(hj hhhNhNubjh)}(h``ha_get_target(ha_mon)``h]hha_get_target(ha_mon)}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jghj ubh.}(hj hhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhMFhjhhubh)}(hXvIf `rvgen` determines that the variable is a clock, it provides the getter and resetter based on the unit. Otherwise, the user needs to provide an appropriate definition. Typically non-clock environment variables are not reset. In such case only the getter skeleton will be present in the file generated by `rvgen`. For instance, the getter for preemptive can be filled as::h](hIf }(hj hhhNhNubjl)}(h`rvgen`h]hrvgen}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj ubhX) determines that the variable is a clock, it provides the getter and resetter based on the unit. Otherwise, the user needs to provide an appropriate definition. Typically non-clock environment variables are not reset. In such case only the getter skeleton will be present in the file generated by }(hj hhhNhNubjl)}(h`rvgen`h]hrvgen}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj ubh;. For instance, the getter for preemptive can be filled as:}(hj hhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhMNhjhhubj)}(hstatic u64 ha_get_env(struct ha_monitor *ha_mon, enum envs env) { if (env == preemptible) return preempt_count() == 0; return ENV_INVALID_VALUE; }h]hstatic u64 ha_get_env(struct ha_monitor *ha_mon, enum envs env) { if (env == preemptible) return preempt_count() == 0; return ENV_INVALID_VALUE; }}hj sbah}(h]h ]h"]h$]h&]jjuh1jhhhMUhjhhubh)}(hX]The function is supplied the ``ha_mon`` parameter in case some storage is required (as it is for clocks), but environment variables without reset do not require a storage and can ignore that argument. The number of environment variables requiring a storage is limited by ``MAX_HA_ENV_LEN``, however such limitation doesn't stand for other variables.h](hThe function is supplied the }(hj hhhNhNubjh)}(h ``ha_mon``h]hha_mon}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jghj ubh parameter in case some storage is required (as it is for clocks), but environment variables without reset do not require a storage and can ignore that argument. The number of environment variables requiring a storage is limited by }(hj hhhNhNubjh)}(h``MAX_HA_ENV_LEN``h]hMAX_HA_ENV_LEN}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jghj ubh>, however such limitation doesn’t stand for other variables.}(hj hhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhM\hjhhubh)}(hXFinally, constraints on states are only valid for clocks and only if the constraint is of the form `clk < N`. This is because such constraints are implemented with the expiration of a timer. Typically the clock variables are reset just before arming the timer, but this doesn't have to be the case and the available functions take care of it. It is a responsibility of per-task monitors to make sure no timer is left running when the task exits.h](hcFinally, constraints on states are only valid for clocks and only if the constraint is of the form }(hj3 hhhNhNubjl)}(h `clk < N`h]hclk < N}(hj; hhhNhNubah}(h]h ]h"]h$]h&]uh1jkhj3 ubhXS. This is because such constraints are implemented with the expiration of a timer. Typically the clock variables are reset just before arming the timer, but this doesn’t have to be the case and the available functions take care of it. It is a responsibility of per-task monitors to make sure no timer is left running when the task exits.}(hj3 hhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhMbhjhhubh)}(hXkBy default the generator implements timers with hrtimers (setting ``HA_TIMER_TYPE`` to ``HA_TIMER_HRTIMER``), this gives better responsiveness but higher overhead. The timer wheel (``HA_TIMER_WHEEL``) is a good alternative for monitors with several instances (e.g. per-task) that achieves lower overhead with increased latency, yet without compromising precision.h](hBBy default the generator implements timers with hrtimers (setting }(hjS hhhNhNubjh)}(h``HA_TIMER_TYPE``h]h HA_TIMER_TYPE}(hj[ hhhNhNubah}(h]h ]h"]h$]h&]uh1jghjS ubh to }(hjS hhhNhNubjh)}(h``HA_TIMER_HRTIMER``h]hHA_TIMER_HRTIMER}(hjm hhhNhNubah}(h]h ]h"]h$]h&]uh1jghjS ubhJ), this gives better responsiveness but higher overhead. The timer wheel (}(hjS hhhNhNubjh)}(h``HA_TIMER_WHEEL``h]hHA_TIMER_WHEEL}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1jghjS ubh) is a good alternative for monitors with several instances (e.g. per-task) that achieves lower overhead with increased latency, yet without compromising precision.}(hjS hhhNhNubeh}(h]h ]h"]h$]h&]uh1hhhhMjhjhhubeh}(h]rv-ha-monitor-hah ]h"]rv/ha_monitor.hah$]h&]uh1hhjBhhhhhMubeh}(h]monitor-header-filesah ]h"]monitor header filesah$]h&]uh1hhhhhhhhKQubh)}(hhh](h)}(h Final remarksh]h Final remarks}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhj hhhhhMqubh)}(hWith the monitor synthesis in place using the header files and rvgen, the developer's work should be limited to the instrumentation of the system, increasing the confidence in the overall approach.h]hWith the monitor synthesis in place using the header files and rvgen, the developer’s work should be limited to the instrumentation of the system, increasing the confidence in the overall approach.}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhMshj hhubh)}(hq[1] For details about deterministic automata format and the translation from one representation to another, see::h]hp[1] For details about deterministic automata format and the translation from one representation to another, see:}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhMwhj hhubj)}(h1Documentation/trace/rv/deterministic_automata.rsth]h1Documentation/trace/rv/deterministic_automata.rst}hj sbah}(h]h ]h"]h$]h&]jjuh1jhhhMzhj hhubh)}(h[2] rvgen appends the monitor's name suffix to the events enums to avoid conflicting variables when exporting the global vmlinux.h use by BPF programs.h]h[2] rvgen appends the monitor’s name suffix to the events enums to avoid conflicting variables when exporting the global vmlinux.h use by BPF programs.}(hj hhhNhNubah}(h]h ]h"]h$]h&]uh1hhhhM|hj hhubeh}(h] final-remarksah ]h"] final remarksah$]h&]uh1hhhhhhhhMqubeh}(h]&runtime-verification-monitor-synthesisah ]h"]&runtime verification monitor synthesisah$]h&]uh1hhhhhhhhKubeh}(h]h ]h"]h$]h&]sourcehuh1hcurrent_sourceN current_lineNsettingsdocutils.frontendValues)}(hN generatorN datestampN source_linkN source_urlN toc_backlinksentryfootnote_backlinksK sectnum_xformKstrip_commentsNstrip_elements_with_classesN strip_classesN report_levelK halt_levelKexit_status_levelKdebugNwarning_streamN tracebackinput_encoding utf-8-siginput_encoding_error_handlerstrictoutput_encodingutf-8output_encoding_error_handlerj#error_encodingutf-8error_encoding_error_handlerbackslashreplace language_codeenrecord_dependenciesNconfigN id_prefixhauto_id_prefixid dump_settingsNdump_internalsNdump_transformsNdump_pseudo_xmlNexpose_internalsNstrict_visitorN_disable_configN_sourcehʌ _destinationN _config_files]7/var/lib/git/docbuild/linux/Documentation/docutils.confafile_insertion_enabled raw_enabledKline_length_limitM'pep_referencesN pep_base_urlhttps://peps.python.org/pep_file_url_templatepep-%04drfc_referencesN rfc_base_url&https://datatracker.ietf.org/doc/html/ tab_widthKtrim_footnote_reference_spacesyntax_highlightlong smart_quotessmartquotes_locales]character_level_inline_markupdoctitle_xform docinfo_xformKsectsubtitle_xform image_loadinglinkembed_stylesheetcloak_email_addressessection_self_linkenvNubreporterNindirect_targets]substitution_defs}substitution_names}refnames}refids}nameids}(j j jDjAj?j<j j jjjjj j j j u nametypes}(j jDj?j jjj j uh}(j hjAjj<jGj jBjj>jjj jj j u footnote_refs} citation_refs} autofootnotes]autofootnote_refs]symbol_footnotes]symbol_footnote_refs] footnotes] citations]autofootnote_startKsymbol_footnote_startK id_counter collectionsCounter}Rparse_messages]transform_messages] transformerN include_log] decorationNhhub.