€•€ëŒsphinx.addnodes”Œdocument”“”)�”}”(Œ rawsource”Œ”Œchildren”]”(Œ translations”Œ LanguagesNode”“”)�”}”(hhh]”(hŒ pending_xref”“”)�”}”(hhh]”Œdocutils.nodes”ŒText”“”ŒChinese (Simplified)”…”�”}”Œparent”hsbaŒ attributes”}”(Œids”]”Œclasses”]”Œnames”]”Œdupnames”]”Œbackrefs”]”Œ refdomain”Œstd”Œreftype”Œdoc”Œ reftarget”Œ./translations/zh_CN/trace/rv/monitor_synthesis”Œmodname”NŒ classname”NŒ refexplicit”ˆuŒtagname”hhh ubh)�”}”(hhh]”hŒChinese (Traditional)”…”�”}”hh2sbah}”(h]”h ]”h"]”h$]”h&]”Œ refdomain”h)Œreftype”h+Œ reftarget”Œ./translations/zh_TW/trace/rv/monitor_synthesis”Œmodname”NŒ classname”NŒ refexplicit”ˆuh1hhh ubh)�”}”(hhh]”hŒItalian”…”�”}”hhFsbah}”(h]”h ]”h"]”h$]”h&]”Œ refdomain”h)Œreftype”h+Œ reftarget”Œ./translations/it_IT/trace/rv/monitor_synthesis”Œmodname”NŒ classname”NŒ refexplicit”ˆuh1hhh ubh)�”}”(hhh]”hŒJapanese”…”�”}”hhZsbah}”(h]”h ]”h"]”h$]”h&]”Œ refdomain”h)Œreftype”h+Œ reftarget”Œ./translations/ja_JP/trace/rv/monitor_synthesis”Œmodname”NŒ classname”NŒ refexplicit”ˆuh1hhh ubh)�”}”(hhh]”hŒKorean”…”�”}”hhnsbah}”(h]”h ]”h"]”h$]”h&]”Œ refdomain”h)Œreftype”h+Œ reftarget”Œ./translations/ko_KR/trace/rv/monitor_synthesis”Œmodname”NŒ classname”NŒ refexplicit”ˆuh1hhh ubh)�”}”(hhh]”hŒPortuguese (Brazilian)”…”�”}”hh‚sbah}”(h]”h ]”h"]”h$]”h&]”Œ refdomain”h)Œreftype”h+Œ reftarget”Œ./translations/pt_BR/trace/rv/monitor_synthesis”Œmodname”NŒ classname”NŒ refexplicit”ˆuh1hhh ubh)�”}”(hhh]”hŒSpanish”…”�”}”hh–sbah}”(h]”h ]”h"]”h$]”h&]”Œ refdomain”h)Œreftype”h+Œ reftarget”Œ./translations/sp_SP/trace/rv/monitor_synthesis”Œmodname”NŒ classname”NŒ refexplicit”ˆuh1hhh ubeh}”(h]”h ]”h"]”h$]”h&]”Œcurrent_language”ŒEnglish”uh1h hhŒ _document”hŒsource”NŒline”NubhŒsection”“”)�”}”(hhh]”(hŒtitle”“”)�”}”(hŒ&Runtime Verification Monitor Synthesis”h]”hŒ&Runtime Verification Monitor Synthesis”…”�”}”(hh¼h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hºhh·h²hh³ŒH/var/lib/git/docbuild/linux/Documentation/trace/rv/monitor_synthesis.rst”h´KubhŒ paragraph”“”)�”}”(hŒ¸The 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]”(hŒVThe starting point for the application of runtime verification (RV) techniques is the ”…”�”}”(hhÍh²hh³Nh´NubhŒemphasis”“”)�”}”(hŒ*specification*”h]”hŒ specification”…”�”}”(hh×h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hÕhhÍubhŒ or ”…”�”}”(hhÍh²hh³Nh´NubhÖ)�”}”(hŒ *modeling*”h]”hŒmodeling”…”�”}”(hhéh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hÕhhÍubhŒE of the desired (or undesired) behavior of the system under scrutiny.”…”�”}”(hhÍh²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Khh·h²hubhÌ)�”}”(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 ”…”�”}”(hjh²hh³Nh´NubhÖ)�”}”(hŒ *synthesized*”h]”hŒ synthesized”…”�”}”(hj h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hÕhjubhŒ into a ”…”�”}”(hjh²hh³Nh´NubhÖ)�”}”(hŒ *monitor*”h]”hŒmonitor”…”�”}”(hjh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hÕhjubhŒG that can then be used in the analysis of the trace of the system. The ”…”�”}”(hjh²hh³Nh´NubhÖ)�”}”(hŒ *monitor*”h]”hŒmonitor”…”�”}”(hj-h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hÕhjubhŒ connects to the system via an ”…”�”}”(hjh²hh³Nh´NubhÖ)�”}”(hŒ*instrumentation*”h]”hŒinstrumentation”…”�”}”(hj?h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hÕhjubhŒ# that converts the events from the ”…”�”}”(hjh²hh³Nh´NubhÖ)�”}”(hŒ*system*”h]”hŒsystem”…”�”}”(hjQh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hÕhjubhŒ to the events of the ”…”�”}”(hjh²hh³Nh´NubhÖ)�”}”(hŒ*specification*”h]”hŒ specification”…”�”}”(hjch²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hÕhjubhŒ.”…”�”}”(hjh²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Khh·h²hubhÌ)�”}”(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]”(hŒNIn Linux terms, the runtime verification monitors are encapsulated inside the ”…”�”}”(hj{h²hh³Nh´NubhÖ)�”}”(hŒ *RV monitor*”h]”hŒ RV monitor”…”�”}”(hjƒh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hÕhj{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{h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Khh·h²hubhŒ 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 ? +-------> ”…”�”}”hj�sbah}”(h]”h ]”h"]”h$]”h&]”Œ xml:space”Œpreserve”uh1j›h³hÊh´Khh·h²hubh¶)�”}”(hhh]”(h»)�”}”(hŒRV monitor synthesis”h]”hŒRV monitor synthesis”…”�”}”(hj°h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hºhj­h²hh³hÊh´K(ubhÌ)�”}”(hŒ¿The 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]”(hŒ0The synthesis of a specification into the Linux ”…”�”}”(hj¾h²hh³Nh´NubhÖ)�”}”(hŒ *RV monitor*”h]”hŒ RV monitor”…”�”}”(hjÆh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hÕhj¾ubhŒƒ abstraction is automated by the rvgen tool and the header file containing common code for creating monitors. The header files are:”…”�”}”(hj¾h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K*hj­h²hubhŒ 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”“”)�”}”(hŒ4rv/da_monitor.h for deterministic automaton monitor.”h]”hÌ)�”}”(hjíh]”hŒ4rv/da_monitor.h for deterministic automaton monitor.”…”�”}”(hjïh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K.hjëubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhjæubjê)�”}”(hŒ3rv/ltl_monitor.h for linear temporal logic monitor.”h]”hÌ)�”}”(hjh]”hŒ3rv/ltl_monitor.h for linear temporal logic monitor.”…”�”}”(hjh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K/hjubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhjæubjê)�”}”(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.”…”�”}”(hjh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K0hjubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhjæubeh}”(h]”h ]”h"]”h$]”h&]”Œbullet”Œ*”uh1jäh³hÊh´K.hjàubah}”(h]”h ]”h"]”h$]”h&]”uh1jÞh³hÊh´K.hj­h²hubeh}”(h]”Œrv-monitor-synthesis”ah ]”h"]”Œrv monitor synthesis”ah$]”h&]”uh1hµhh·h²hh³hÊh´K(ubh¶)�”}”(hhh]”(h»)�”}”(hŒrvgen”h]”hŒrvgen”…”�”}”(hjJh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hºhjGh²hh³hÊh´K3ubhÌ)�”}”(hŒvThe rvgen utility converts a specification into the C presentation and creating the skeleton of a kernel monitor in C.”h]”hŒvThe rvgen utility converts a specification into the C presentation and creating the skeleton of a kernel monitor in C.”…”�”}”(hjXh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K5hjGh²hubhÌ)�”}”(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:”…”�”}”(hjfh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K8hjGh²hubjœ)�”}”(hŒ+$ rvgen monitor -c da -s wip.dot -t per_cpu”h]”hŒ+$ rvgen monitor -c da -s wip.dot -t per_cpu”…”�”}”hjtsbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´K;hjGh²hubhÌ)�”}”(hŒAThis will create a directory named wip/ with the following files:”h]”hŒAThis will create a directory named wip/ with the following files:”…”�”}”(hj‚h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K=hjGh²hubjå)�”}”(hhh]”(jê)�”}”(hŒwip.h: the wip model in C”h]”hÌ)�”}”(hj•h]”hŒwip.h: the wip model in C”…”�”}”(hj—h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K?hj“ubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhj�h²hh³hÊh´Nubjê)�”}”(hŒwip.c: the RV monitor ”h]”hÌ)�”}”(hŒwip.c: the RV monitor”h]”hŒwip.c: the RV monitor”…”�”}”(hj®h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K@hjªubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhj�h²hh³hÊh´Nubeh}”(h]”h ]”h"]”h$]”h&]”j7Œ-”uh1jäh³hÊh´K?hjGh²hubhÌ)�”}”(hŒfThe wip.c file contains the monitor declaration and the starting point for the system instrumentation.”h]”hŒfThe wip.c file contains the monitor declaration and the starting point for the system instrumentation.”…”�”}”(hjÉh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´KBhjGh²hubhÌ)�”}”(hŒXSimilarly, a linear temporal logic monitor can be generated with the following command::”h]”hŒWSimilarly, a linear temporal logic monitor can be generated with the following command:”…”�”}”(hj×h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´KEhjGh²hubjœ)�”}”(hŒ3$ rvgen monitor -c ltl -s pagefault.ltl -t per_task”h]”hŒ3$ rvgen monitor -c ltl -s pagefault.ltl -t per_task”…”�”}”hjåsbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´KHhjGh²hubhÌ)�”}”(hŒ)This generates pagefault/ directory with:”h]”hŒ)This generates pagefault/ directory with:”…”�”}”(hjóh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´KJhjGh²hubjå)�”}”(hhh]”(jê)�”}”(hŒbpagefault.h: The Buchi automaton (the non-deterministic state machine to verify the specification)”h]”hÌ)�”}”(hŒbpagefault.h: The Buchi automaton (the non-deterministic state machine to verify the specification)”h]”hŒbpagefault.h: The Buchi automaton (the non-deterministic state machine to verify the specification)”…”�”}”(hjh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´KLhjubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhjh²hh³hÊh´Nubjê)�”}”(hŒ-pagefault.c: The skeleton for the RV monitor ”h]”hÌ)�”}”(hŒ,pagefault.c: The skeleton for the RV monitor”h]”hŒ,pagefault.c: The skeleton for the RV monitor”…”�”}”(hj h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´KNhjubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhjh²hh³hÊh´Nubeh}”(h]”h ]”h"]”h$]”h&]”j7jÈuh1jäh³hÊh´KLhjGh²hubeh}”(h]”Œrvgen”ah ]”h"]”Œrvgen”ah$]”h&]”uh1hµhh·h²hh³hÊh´K3ubh¶)�”}”(hhh]”(h»)�”}”(hŒMonitor header files”h]”hŒMonitor header files”…”�”}”(hjEh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hºhjBh²hh³hÊh´KQubhÌ)�”}”(hŒThe header files:”h]”hŒThe header files:”…”�”}”(hjSh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´KShjBh²hubjå)�”}”(hhh]”(jê)�”}”(hŒ5`rv/da_monitor.h` for deterministic automaton monitor”h]”hÌ)�”}”(hjfh]”(hŒtitle_reference”“”)�”}”(hŒ`rv/da_monitor.h`”h]”hŒrv/da_monitor.h”…”�”}”(hjmh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjhubhŒ$ for deterministic automaton monitor”…”�”}”(hjhh²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´KUhjdubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhjah²hh³hÊh´Nubjê)�”}”(hŒ3`rv/ltl_monitor` for linear temporal logic monitor ”h]”hÌ)�”}”(hŒ2`rv/ltl_monitor` for linear temporal logic monitor”h]”(jl)�”}”(hŒ`rv/ltl_monitor`”h]”hŒrv/ltl_monitor”…”�”}”(hj“h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhj�ubhŒ" for linear temporal logic monitor”…”�”}”(hj�h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´KVhj‹ubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhjah²hh³hÊh´Nubeh}”(h]”h ]”h"]”h$]”h&]”j7jÈuh1jäh³hÊh´KUhjBh²hubhÌ)�”}”(hŒRinclude common macros and static functions for implementing *Monitor Instance(s)*.”h]”(hŒh²hh³hÊh´KdubhÌ)�”}”(hŒPThis initial implementation presents three different types of monitor instances:”h]”hŒPThis initial implementation presents three different types of monitor instances:”…”�”}”(hjOh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Kfhj>h²hubjå)�”}”(hhh]”(jê)�”}”(hŒ%``#define RV_MON_TYPE RV_MON_GLOBAL``”h]”hÌ)�”}”(hjbh]”hŒliteral”“”)�”}”(hjbh]”hŒ!#define RV_MON_TYPE RV_MON_GLOBAL”…”�”}”(hjih²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghjdubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Khhj`ubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhj]h²hh³hÊh´Nubjê)�”}”(hŒ&``#define RV_MON_TYPE RV_MON_PER_CPU``”h]”hÌ)�”}”(hj„h]”jh)�”}”(hj„h]”hŒ"#define RV_MON_TYPE RV_MON_PER_CPU”…”�”}”(hj‰h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghj†ubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Kihj‚ubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhj]h²hh³hÊh´Nubjê)�”}”(hŒ(``#define RV_MON_TYPE RV_MON_PER_TASK`` ”h]”hÌ)�”}”(hŒ'``#define RV_MON_TYPE RV_MON_PER_TASK``”h]”jh)�”}”(hj¨h]”hŒ##define RV_MON_TYPE RV_MON_PER_TASK”…”�”}”(hjªh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghj¦ubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Kjhj¢ubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhj]h²hh³hÊh´Nubeh}”(h]”h ]”h"]”h$]”h&]”j7jÈuh1jäh³hÊh´Khhj>h²hubhÌ)�”}”(hŒ«The 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]”hŒ«The 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.”…”�”}”(hjÉh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Klhj>h²hubhÌ)�”}”(hŒ¯In 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]”(hŒMIn all cases, the C file must include the $(MODEL_NAME).h file (generated by ”…”�”}”(hj×h²hh³Nh´Nubjl)�”}”(hŒ`rvgen`”h]”hŒrvgen”…”�”}”(hjßh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhj×ubhŒ=), for example, to define the per-cpu ‘wip’ monitor, the ”…”�”}”(hj×h²hh³Nh´Nubjl)�”}”(hŒ`wip.c`”h]”hŒwip.c”…”�”}”(hjñh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhj×ubhŒ source file must include:”…”�”}”(hj×h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Kphj>h²hubjœ)�”}”(hŒN#define RV_MON_TYPE RV_MON_PER_CPU #include "wip.h" #include ”h]”hŒN#define RV_MON_TYPE RV_MON_PER_CPU #include "wip.h" #include ”…”�”}”hj sbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´Kthj>h²hubhÌ)�”}”(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:”…”�”}”(hjh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Kxhj>h²hubjœ)�”}”(hŒ�da_handle_event($(event from event enum)); da_handle_start_event($(event from event enum)); da_handle_start_run_event($(event from event enum));”h]”hŒ�da_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&]”j«j¬uh1j›h³hÊh´K{hj>h²hubhÌ)�”}”(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 ”…”�”}”(hj3h²hh³Nh´Nubjh)�”}”(hŒ``da_handle_event()``”h]”hŒda_handle_event()”…”�”}”(hj;h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghj3ubhŒ[ is the regular case where the event will be processed if the monitor is processing events.”…”�”}”(hj3h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Khj>h²hubhÌ)�”}”(hŒ™When 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]”(hŒ‰When 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 ”…”�”}”(hjSh²hh³Nh´NubhÖ)�”}”(hŒ*initial state*”h]”hŒ initial state”…”�”}”(hj[h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hÕhjSubhŒ.”…”�”}”(hjSh²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K‚hj>h²hubhÌ)�”}”(hŒ­The ``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]”(hŒThe ”…”�”}”(hjsh²hh³Nh´Nubjh)�”}”(hŒ``da_handle_start_event()``”h]”hŒda_handle_start_event()”…”�”}”(hj{h²hh³Nh´Nubah}”(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.”…”�”}”(hjsh²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K…hj>h²hubhÌ)�”}”(hŒÂThe ``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]”(hŒThe ”…”�”}”(hj“h²hh³Nh´Nubjh)�”}”(hŒ``da_handle_start_run_event()``”h]”hŒda_handle_start_run_event()”…”�”}”(hj›h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghj“ubhŒŸ 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.”…”�”}”(hj“h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K‰hj>h²hubhÌ)�”}”(hŒ‚Using the wip model as example, the events "preempt_disable" and "sched_waking" should be sent to monitor, respectively, via [2]::”h]”hŒ‰Using the wip model as example, the events “preempt_disableâ€� and “sched_wakingâ€� should be sent to monitor, respectively, via [2]:”…”�”}”(hj³h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K�hj>h²hubjœ)�”}”(hŒHda_handle_event(preempt_disable_wip); da_handle_event(sched_waking_wip);”h]”hŒHda_handle_event(preempt_disable_wip); da_handle_event(sched_waking_wip);”…”�”}”hjÁsbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´K�hj>h²hubhÌ)�”}”(hŒ,While the event "preempt_enabled" will use::”h]”hŒ/While the event “preempt_enabledâ€� will use:”…”�”}”(hjÏh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K“hj>h²hubjœ)�”}”(hŒ*da_handle_start_event(preempt_enable_wip);”h]”hŒ*da_handle_start_event(preempt_enable_wip);”…”�”}”hjÝsbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´K•hj>h²hubhÌ)�”}”(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.”…”�”}”(hjëh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K—hj>h²hubeh}”(h]”Œrv-da-monitor-h”ah ]”h"]”Œrv/da_monitor.h”ah$]”h&]”uh1hµhjBh²hh³hÊh´Kdubh¶)�”}”(hhh]”(h»)�”}”(hŒrv/ltl_monitor.h”h]”hŒrv/ltl_monitor.h”…”�”}”(hjh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hºhjh²hh³hÊh´K›ubhÌ)�”}”(hŒ¶This 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]”(hŒGThis file must be combined with the $(MODEL_NAME).h file (generated by ”…”�”}”(hjh²hh³Nh´Nubjl)�”}”(hŒ`rvgen`”h]”hŒrvgen”…”�”}”(hjh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjubhŒ') to be complete. For example, for the ”…”�”}”(hjh²hh³Nh´Nubjl)�”}”(hŒ `pagefault`”h]”hŒ pagefault”…”�”}”(hj,h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjubhŒ monitor, the ”…”�”}”(hjh²hh³Nh´Nubjl)�”}”(hŒ `pagefault.c`”h]”hŒ pagefault.c”…”�”}”(hj>h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjubhŒ source file must include:”…”�”}”(hjh²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Kœhjh²hubjœ)�”}”(hŒ2#include "pagefault.h" #include ”h]”hŒ2#include "pagefault.h" #include ”…”�”}”hjVsbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´K hjh²hubhÌ)�”}”(hŒC(the skeleton monitor file generated by `rvgen` already does this).”h]”(hŒ((the skeleton monitor file generated by ”…”�”}”(hjdh²hh³Nh´Nubjl)�”}”(hŒ`rvgen`”h]”hŒrvgen”…”�”}”(hjlh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjdubhŒ already does this).”…”�”}”(hjdh²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K£hjh²hubhÌ)�”}”(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”…”�”}”(hjˆh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhj„ubhŒ (”…”�”}”(hj„h²hh³Nh´Nubjl)�”}”(hŒ `pagefault.h`”h]”hŒ pagefault.h”…”�”}”(hjšh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhj„ubhŒ™ in the above example) includes the implementation of the Buchi automaton - a non-deterministic state machine that verifies the LTL specification. While ”…”�”}”(hj„h²hh³Nh´Nubjl)�”}”(hŒ`rv/ltl_monitor.h`”h]”hŒrv/ltl_monitor.h”…”�”}”(hj¬h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhj„ubhŒ† includes the common helper functions to interact with the Buchi automaton and to implement an RV monitor. An important definition in ”…”�”}”(hj„h²hh³Nh´Nubjl)�”}”(hŒ`$(MODEL_NAME).h`”h]”hŒ$(MODEL_NAME).h”…”�”}”(hj¾h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhj„ubhŒ is:”…”�”}”(hj„h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K¥hjh²hubjœ)�”}”(hŒvenum ltl_atom { LTL_$(FIRST_ATOMIC_PROPOSITION), LTL_$(SECOND_ATOMIC_PROPOSITION), ... LTL_NUM_ATOM };”h]”hŒvenum ltl_atom { LTL_$(FIRST_ATOMIC_PROPOSITION), LTL_$(SECOND_ATOMIC_PROPOSITION), ... LTL_NUM_ATOM };”…”�”}”hjÖsbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´K«hjh²hubhÌ)�”}”(hŒÇwhich 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]”(hŒ„which is the list of atomic propositions present in the LTL specification (prefixed with “LTL_â€� to avoid name collision). This ”…”�”}”(hjäh²hh³Nh´Nubjl)�”}”(hŒ`enum`”h]”hŒenum”…”�”}”(hjìh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjäubhŒA is passed to the functions interacting with the Buchi automaton.”…”�”}”(hjäh²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K²hjh²hubhÌ)�”}”(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]”(hŒWhile generating code, ”…”�”}”(hjh²hh³Nh´Nubjl)�”}”(hŒ`rvgen`”h]”hŒrvgen”…”�”}”(hj h²hh³Nh´Nubah}”(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:”…”�”}”(hjh²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´K¶hjh²hubjœ)�”}”(hŒNvoid ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)”h]”hŒNvoid ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)”…”�”}”hj$sbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´K»hjh²hubhÌ)�”}”(hŒôwhich 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]”(hŒh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjubhŒ everywhere.”…”�”}”(hjh²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´KÚhjh²hubhÌ)�”}”(hŒ¢For 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]”hŒ¡For 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:”…”�”}”(hjVh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´KÞhjh²hubjœ)�”}”(hŒMvoid ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)”h]”hŒMvoid ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)”…”�”}”hjdsbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´Kâhjh²hubhÌ)�”}”(hŒwhich is equivalent to::”h]”hŒwhich is equivalent to:”…”�”}”(hjrh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Kähjh²hubjœ)�”}”(hŒHltl_atom_update(task, atom, value); ltl_atom_update(task, atom, !value);”h]”hŒHltl_atom_update(task, atom, value); ltl_atom_update(task, atom, !value);”…”�”}”hj€sbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´Kæhjh²hubhÌ)�”}”(hŒSTo initialize the atomic propositions, the following function must be implemented::”h]”hŒRTo initialize the atomic propositions, the following function must be implemented:”…”�”}”(hjŽh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Kéhjh²hubjœ)�”}”(hŒUltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)”h]”hŒUltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)”…”�”}”hjœsbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´Kìhjh²hubhÌ)�”}”(hŒÞThis 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]”hŒÝThis 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:”…”�”}”(hjªh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Kîhjh²hubjœ)�”}”(hŒÓvoid 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]”hŒÓvoid 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); }”…”�”}”hj¸sbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´Kòhjh²hubhÌ)�”}”(hXºAtomic 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 ”…”�”}”(hjÆh²hh³Nh´Nubjl)�”}”(hŒ`ltl_atom_init()`”h]”hŒltl_atom_init()”…”�”}”(hjÎh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjÆubhX‚ 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.”…”�”}”(hjÆh²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Kùhjh²hubeh}”(h]”Œrv-ltl-monitor-h”ah ]”h"]”Œrv/ltl_monitor.h”ah$]”h&]”uh1hµhjBh²hh³hÊh´K›ubh¶)�”}”(hhh]”(h»)�”}”(hŒrv/ha_monitor.h”h]”hŒrv/ha_monitor.h”…”�”}”(hjñh²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hºhjîh²hh³hÊh´MubhÌ)�”}”(hŒâThe 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]”(hŒ‰The implementation of hybrid automaton monitors derives directly from the deterministic automaton one. Despite using a different header (”…”�”}”(hjÿh²hh³Nh´Nubjh)�”}”(hŒ``ha_monitor.h``”h]”hŒ ha_monitor.h”…”�”}”(hj h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghjÿubhŒ4) the functions to handle events are the same (e.g. ”…”�”}”(hjÿh²hh³Nh´Nubjh)�”}”(hŒ``da_handle_event``”h]”hŒda_handle_event”…”�”}”(hj h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghjÿubhŒ).”…”�”}”(hjÿh²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Mhjîh²hubhÌ)�”}”(hŒ·Additionally, 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]”(hŒAdditionally, the ”…”�”}”(hj1 h²hh³Nh´Nubjl)�”}”(hŒ`rvgen`”h]”hŒrvgen”…”�”}”(hj9 h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhj1 ubhŒ" tool populates skeletons for the ”…”�”}”(hj1 h²hh³Nh´Nubjh)�”}”(hŒ``ha_verify_constraint``”h]”hŒha_verify_constraint”…”�”}”(hjK h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghj1 ubhŒ, ”…”�”}”(hj1 h²hh³Nh´Nubjh)�”}”(hŒ``ha_get_env``”h]”hŒ ha_get_env”…”�”}”(hj] h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghj1 ubhŒ and ”…”�”}”(hj1 h²hh³Nh´Nubjh)�”}”(hŒ``ha_reset_env``”h]”hŒ ha_reset_env”…”�”}”(hjo h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghj1 ubhŒ? based on the monitor specification in the monitor source file.”…”�”}”(hj1 h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Mhjîh²hubhÌ)�”}”(hŒJ``ha_verify_constraint`` is typically ready as it is generated by `rvgen`:”h]”(jh)�”}”(hŒ``ha_verify_constraint``”h]”hŒha_verify_constraint”…”�”}”(hj‹ h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghj‡ ubhŒ* is typically ready as it is generated by ”…”�”}”(hj‡ h²hh³Nh´Nubjl)�”}”(hŒ`rvgen`”h]”hŒrvgen”…”�”}”(hj� h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhj‡ ubhŒ:”…”�”}”(hj‡ h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M hjîh²hubjå)�”}”(hhh]”(jê)�”}”(hŒcstandard constraints on edges are turned into the form:: res = ha_get_env(ha_mon, ENV) < VALUE; ”h]”(hÌ)�”}”(hŒ8standard constraints on edges are turned into the form::”h]”hŒ7standard constraints on edges are turned into the form:”…”�”}”(hj¼ h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Mhj¸ 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&]”j«j¬uh1j›h³hÊh´Mhj¸ ubeh}”(h]”h ]”h"]”h$]”h&]”uh1jéhjµ h²hh³hÊh´Nubjê)�”}”(hŒKreset 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â h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´MhjÞ ubjœ)�”}”(hŒha_reset_env(ha_mon, ENV);”h]”hŒha_reset_env(ha_mon, ENV);”…”�”}”hjð sbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´MhjÞ ubeh}”(h]”h ]”h"]”h$]”h&]”uh1jéhjµ h²hh³hÊh´Nubjê)�”}”(hXûconstraints 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Ì)�”}”(hŒ5constraints on the state are implemented using timers”h]”hŒ5constraints on the state are implemented using timers”…”�”}”(hj h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Mhj ubjå)�”}”(hhh]”(jê)�”}”(hŒ armed before entering the state ”h]”hÌ)�”}”(hŒarmed before entering the state”h]”hŒarmed before entering the state”…”�”}”(hj h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Mhj ubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhj ubjê)�”}”(hŒ)cancelled while entering any other state ”h]”hÌ)�”}”(hŒ(cancelled while entering any other state”h]”hŒ(cancelled while entering any other state”…”�”}”(hj5 h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Mhj1 ubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhj 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 event”h]”hŒ?untouched if the state does not change as a result of the event”…”�”}”(hjM h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´MhjI ubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhj ubjê)�”}”(hŒ:checked if the timer expired but the callback did not run ”h]”hÌ)�”}”(hŒ9checked if the timer expired but the callback did not run”h]”hŒ9checked if the timer expired but the callback did not run”…”�”}”(hje h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Mhja ubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhj ubjê)�”}”(hŒí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Ì)�”}”(hŒDavailable implementation are `HA_TIMER_HRTIMER` and `HA_TIMER_WHEEL`”h]”(hŒavailable implementation are ”…”�”}”(hj} h²hh³Nh´Nubjl)�”}”(hŒ`HA_TIMER_HRTIMER`”h]”hŒHA_TIMER_HRTIMER”…”�”}”(hj… h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhj} ubhŒ and ”…”�”}”(hj} h²hh³Nh´Nubjl)�”}”(hŒ`HA_TIMER_WHEEL`”h]”hŒHA_TIMER_WHEEL”…”�”}”(hj— h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhj} ubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M hjy ubjå)�”}”(hhh]”(jê)�”}”(hŒ7hrtimers are more precise but may have higher overhead ”h]”hÌ)�”}”(hŒ6hrtimers are more precise but may have higher overhead”h]”hŒ6hrtimers are more precise but may have higher overhead”…”�”}”(hj² h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M"hj® ubah}”(h]”h ]”h"]”h$]”h&]”uh1jéhj« ubjê)�”}”(hŒiselect 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]”(hŒselect by defining ”…”�”}”(hjÊ h²hh³Nh´Nubjl)�”}”(hŒ`HA_TIMER_TYPE`”h]”hŒ HA_TIMER_TYPE”…”�”}”(hjÒ h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjÊ ubhŒ before including the header:”…”�”}”(hjÊ h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M$hjÆ ubjœ)�”}”(hŒ&#define HA_TIMER_TYPE HA_TIMER_HRTIMER”h]”hŒ&#define HA_TIMER_TYPE HA_TIMER_HRTIMER”…”�”}”hjê sbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´M&hjÆ ubeh}”(h]”h ]”h"]”h$]”h&]”uh1jéhj« ubeh}”(h]”h ]”h"]”h$]”h&]”j7jÈuh1jäh³hÊh´M"hjy ubeh}”(h]”h ]”h"]”h$]”h&]”uh1jéhj ubeh}”(h]”h ]”h"]”h$]”h&]”j7jÈuh1jäh³hÊh´Mhj ubeh}”(h]”h ]”h"]”h$]”h&]”uh1jéhjµ h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”j7j8uh1jäh³hÊh´Mhjîh²hubhÌ)�”}”(hŒ6Constraint values can be specified in different forms:”h]”hŒ6Constraint values can be specified in different forms:”…”�”}”(hj h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M(hjîh²hubjå)�”}”(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 h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M*hj- ubjœ)�”}”(hŒ,preemptive == 0 clk < 100ns threshold <= 10j”h]”hŒ,preemptive == 0 clk < 100ns threshold <= 10j”…”�”}”hj? sbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´M,hj- ubeh}”(h]”h ]”h"]”h$]”h&]”uh1jéhj* h²hh³hÊh´Nubjê)�”}”(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 h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M0hjS ubjœ)�”}”(hŒ clk < MAX_NS”h]”hŒ clk < MAX_NS”…”�”}”hje sbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´M2hjS ubeh}”(h]”h ]”h"]”h$]”h&]”uh1jéhj* h²hh³hÊh´Nubjê)�”}”(hŒAparameter (lowercase string). E.g.:: clk <= threshold_jiffies ”h]”(hÌ)�”}”(hŒ$parameter (lowercase string). E.g.::”h]”hŒ#parameter (lowercase string). E.g.:”…”�”}”(hj} h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M4hjy ubjœ)�”}”(hŒclk <= threshold_jiffies”h]”hŒclk <= threshold_jiffies”…”�”}”hj‹ sbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´M6hjy ubeh}”(h]”h ]”h"]”h$]”h&]”uh1jéhj* h²hh³hÊh´Nubjê)�”}”(hŒDmacro (uppercase string with parentheses). E.g.:: clk < MAX_NS() ”h]”(hÌ)�”}”(hŒ1macro (uppercase string with parentheses). E.g.::”h]”hŒ0macro (uppercase string with parentheses). E.g.:”…”�”}”(hj£ h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M8hjŸ ubjœ)�”}”(hŒclk < MAX_NS()”h]”hŒclk < MAX_NS()”…”�”}”hj± sbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´M:hjŸ ubeh}”(h]”h ]”h"]”h$]”h&]”uh1jéhj* h²hh³hÊh´Nubjê)�”}”(hŒSfunction (lowercase string with parentheses). E.g.:: clk <= threshold_jiffies() ”h]”(hÌ)�”}”(hŒ4function (lowercase string with parentheses). E.g.::”h]”hŒ3function (lowercase string with parentheses). E.g.:”…”�”}”(hjÉ h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M<hjÅ ubjœ)�”}”(hŒclk <= threshold_jiffies()”h]”hŒclk <= threshold_jiffies()”…”�”}”hj× sbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´M>hjÅ ubeh}”(h]”h ]”h"]”h$]”h&]”uh1jéhj* h²hh³hÊh´Nubeh}”(h]”h ]”h"]”h$]”h&]”j7j8uh1jäh³hÊh´M*hjîh²hubhÌ)�”}”(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]”(hŒIn all cases, ”…”�”}”(hjñ h²hh³Nh´Nubjl)�”}”(hŒ`rvgen`”h]”hŒrvgen”…”�”}”(hjù h²hh³Nh´Nubah}”(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ñ h²hh³Nh´Nubjh)�”}”(hŒ``_NS``”h]”hŒ_NS”…”�”}”(hj h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghjñ ubhŒ or ”…”�”}”(hjñ h²hh³Nh´Nubjh)�”}”(hŒ ``_jiffies``”h]”hŒ_jiffies”…”�”}”(hj h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghjñ ubhŒ` are intended as clocks with ns and jiffy granularity, respectively. Literals with measure unit ”…”�”}”(hjñ h²hh³Nh´Nubjl)�”}”(hŒ`j`”h]”hŒj”…”�”}”(hj/ h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjñ ubhŒ. are jiffies and if a time unit is specified (”…”�”}”(hjñ h²hh³Nh´Nubjl)�”}”(hŒ`ns`”h]”hŒns”…”�”}”(hjA h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjñ ubhŒ to ”…”�”}”(hjñ h²hh³Nh´Nubjl)�”}”(hŒ`s`”h]”hŒs”…”�”}”(hjS h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjñ ubhŒ), ”…”�”}”(hjñ h²hh³Nh´Nubjl)�”}”(hŒ`rvgen`”h]”hŒrvgen”…”�”}”(hje h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjñ ubhŒ will convert the value to ”…”�”}”(hjñ h²hh³Nh´Nubjl)�”}”(hŒ`ns`”h]”hŒns”…”�”}”(hjw h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjñ ubhŒ.”…”�”}”(hjñ h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M@hjîh²hubhÌ)�”}”(hXÐConstants 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� h²hh³Nh´Nubjh)�”}”(hŒ``ha_monitor``”h]”hŒ ha_monitor”…”�”}”(hj— h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghj� ubhŒz, 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� h²hh³Nh´Nubjh)�”}”(hŒ``ha_get_target(ha_mon)``”h]”hŒha_get_target(ha_mon)”…”�”}”(hj© h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghj� ubhŒ.”…”�”}”(hj� h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´MFhjîh²hubhÌ)�”}”(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]”(hŒIf ”…”�”}”(hjÁ h²hh³Nh´Nubjl)�”}”(hŒ`rvgen`”h]”hŒrvgen”…”�”}”(hjÉ h²hh³Nh´Nubah}”(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Á h²hh³Nh´Nubjl)�”}”(hŒ`rvgen`”h]”hŒrvgen”…”�”}”(hjÛ h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jkhjÁ ubhŒ;. For instance, the getter for preemptive can be filled as:”…”�”}”(hjÁ h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´MNhjîh²hubjœ)�”}”(hŒ¢static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs env) { if (env == preemptible) return preempt_count() == 0; return ENV_INVALID_VALUE; }”h]”hŒ¢static 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&]”j«j¬uh1j›h³hÊh´MUhjîh²hubhÌ)�”}”(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]”(hŒThe function is supplied the ”…”�”}”(hj h²hh³Nh´Nubjh)�”}”(hŒ ``ha_mon``”h]”hŒha_mon”…”�”}”(hj h²hh³Nh´Nubah}”(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 h²hh³Nh´Nubjh)�”}”(hŒ``MAX_HA_ENV_LEN``”h]”hŒMAX_HA_ENV_LEN”…”�”}”(hj h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghj ubhŒ>, however such limitation doesn’t stand for other variables.”…”�”}”(hj h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M\hjîh²hubhÌ)�”}”(hX½Finally, 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]”(hŒcFinally, constraints on states are only valid for clocks and only if the constraint is of the form ”…”�”}”(hj3 h²hh³Nh´Nubjl)�”}”(hŒ `clk < N`”h]”hŒclk < N”…”�”}”(hj; h²hh³Nh´Nubah}”(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 h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Mbhjîh²hubhÌ)�”}”(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]”(hŒBBy default the generator implements timers with hrtimers (setting ”…”�”}”(hjS h²hh³Nh´Nubjh)�”}”(hŒ``HA_TIMER_TYPE``”h]”hŒ HA_TIMER_TYPE”…”�”}”(hj[ h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghjS ubhŒ to ”…”�”}”(hjS h²hh³Nh´Nubjh)�”}”(hŒ``HA_TIMER_HRTIMER``”h]”hŒHA_TIMER_HRTIMER”…”�”}”(hjm h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1jghjS ubhŒJ), this gives better responsiveness but higher overhead. The timer wheel (”…”�”}”(hjS h²hh³Nh´Nubjh)�”}”(hŒ``HA_TIMER_WHEEL``”h]”hŒHA_TIMER_WHEEL”…”�”}”(hj h²hh³Nh´Nubah}”(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 h²hh³Nh´Nubeh}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Mjhjîh²hubeh}”(h]”Œrv-ha-monitor-h”ah ]”h"]”Œrv/ha_monitor.h”ah$]”h&]”uh1hµhjBh²hh³hÊh´Mubeh}”(h]”Œmonitor-header-files”ah ]”h"]”Œmonitor header files”ah$]”h&]”uh1hµhh·h²hh³hÊh´KQubh¶)�”}”(hhh]”(h»)�”}”(hŒ Final remarks”h]”hŒ Final remarks”…”�”}”(hjª h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hºhj§ h²hh³hÊh´MqubhÌ)�”}”(hŒÅWith 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]”hŒÇWith 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¸ h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Mshj§ h²hubhÌ)�”}”(hŒq[1] For details about deterministic automata format and the translation from one representation to another, see::”h]”hŒp[1] For details about deterministic automata format and the translation from one representation to another, see:”…”�”}”(hjÆ h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´Mwhj§ h²hubjœ)�”}”(hŒ1Documentation/trace/rv/deterministic_automata.rst”h]”hŒ1Documentation/trace/rv/deterministic_automata.rst”…”�”}”hjÔ sbah}”(h]”h ]”h"]”h$]”h&]”j«j¬uh1j›h³hÊh´Mzhj§ h²hubhÌ)�”}”(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â h²hh³Nh´Nubah}”(h]”h ]”h"]”h$]”h&]”uh1hËh³hÊh´M|hj§ h²hubeh}”(h]”Œ final-remarks”ah ]”h"]”Œ final remarks”ah$]”h&]”uh1hµhh·h²hh³hÊh´Mqubeh}”(h]”Œ&runtime-verification-monitor-synthesis”ah ]”h"]”Œ&runtime verification monitor synthesis”ah$]”h&]”uh1hµhhh²hh³hÊh´Kubeh}”(h]”h ]”h"]”h$]”h&]”Œsource”hÊuh1hŒcurrent_source”NŒ current_line”NŒsettings”Œdocutils.frontend”ŒValues”“”)�”}”(hºNŒ generator”NŒ datestamp”NŒ source_link”NŒ source_url”NŒ toc_backlinks”Œentry”Œfootnote_backlinks”KŒ sectnum_xform”KŒstrip_comments”NŒstrip_elements_with_classes”NŒ strip_classes”NŒ report_level”KŒ halt_level”KŒexit_status_level”KŒdebug”NŒwarning_stream”NŒ traceback”ˆŒinput_encoding”Œ utf-8-sig”Œinput_encoding_error_handler”Œstrict”Œoutput_encoding”Œutf-8”Œoutput_encoding_error_handler”j#Œerror_encoding”Œutf-8”Œerror_encoding_error_handler”Œbackslashreplace”Œ language_code”Œen”Œrecord_dependencies”NŒconfig”NŒ id_prefix”hŒauto_id_prefix”Œid”Œ dump_settings”NŒdump_internals”NŒdump_transforms”NŒdump_pseudo_xml”NŒexpose_internals”NŒstrict_visitor”NŒ_disable_config”NŒ_source”hÊŒ _destination”NŒ _config_files”]”Œ7/var/lib/git/docbuild/linux/Documentation/docutils.conf”aŒfile_insertion_enabled”ˆŒ raw_enabled”KŒline_length_limit”M'Œpep_references”NŒ pep_base_url”Œhttps://peps.python.org/”Œpep_file_url_template”Œpep-%04d”Œrfc_references”NŒ rfc_base_url”Œ&https://datatracker.ietf.org/doc/html/”Œ tab_width”KŒtrim_footnote_reference_space”‰Œsyntax_highlight”Œlong”Œ smart_quotes”ˆŒsmartquotes_locales”]”Œcharacter_level_inline_markup”‰Œdoctitle_xform”‰Œ docinfo_xform”KŒsectsubtitle_xform”‰Œ image_loading”Œlink”Œembed_stylesheet”‰Œcloak_email_addresses”ˆŒsection_self_link”‰Œenv”NubŒreporter”NŒindirect_targets”]”Œsubstitution_defs”}”Œsubstitution_names”}”Œrefnames”}”Œrefids”}”Œnameids”}”(jý jú jDjAj?j<j¤ j¡ jþjûjëjèjœ j™ jõ jò uŒ nametypes”}”(jý ‰jD‰j?‰j¤ ‰jþ‰jë‰jœ ‰jõ ‰uh}”(jú h·jAj­j<jGj¡ jBjûj>jèjj™ jîjò j§ uŒ footnote_refs”}”Œ citation_refs”}”Œ autofootnotes”]”Œautofootnote_refs”]”Œsymbol_footnotes”]”Œsymbol_footnote_refs”]”Œ footnotes”]”Œ citations”]”Œautofootnote_start”KŒsymbol_footnote_start”KŒ id_counter”Œ collections”ŒCounter”“”}”…”R”Œparse_messages”]”Œtransform_messages”]”Œ transformer”NŒ include_log”]”Œ decoration”Nh²hub.