确定性自动机监控器合成¶
应用运行时验证 (RV) 技术的起点是 规范 或 建模 被检查系统的期望（或不期望）的行为。
然后需要将正式的表示形式 合成 为一个 监控器，该监控器可以用于分析系统的跟踪。 监控器 通过 仪器 连接到系统，该 仪器 将来自 系统 的事件转换为 规范 的事件。
在 Linux 术语中，运行时验证监控器封装在 RV 监控器 抽象中。 RV 监控器包括一组监控器实例（每个 CPU 监控器、每个任务监控器等）、将监控器粘合到系统参考模型的辅助函数，以及作为事件解析和异常的反应的跟踪输出，如下所示
Linux +----- RV Monitor ----------------------------------+ Formal
Realm | | Realm
+-------------------+ +----------------+ +-----------------+
| Linux kernel | | Monitor | | Reference |
| Tracing | -> | Instance(s) | <- | Model |
| (instrumentation) | | (verification) | | (specification) |
+-------------------+ +----------------+ +-----------------+
| | |
| V |
| +----------+ |
| | Reaction | |
| +--+--+--+-+ |
| | | | |
| | | +-> trace output ? |
+------------------------|--|----------------------+
| +----> panic ?
+-------> <user-specified>
DA 监控器合成¶
基于自动机模型的合成到 Linux RV 监控器 抽象由 dot2k 工具和 rv/da_monitor.h 头文件自动化，该文件包含一组自动生成监控器代码的宏。
dot2k¶
dot2k 实用程序通过将 DOT 格式的自动机模型转换为 C 表示 [1] 并创建 C 中的内核监控器骨架来利用 dot2c。
例如，可以使用以下命令将 [1] 中存在的 wip.dot 模型转换为每个 CPU 监控器
$ dot2k -d wip.dot -t per_cpu
这将创建一个名为 wip/ 的目录，其中包含以下文件
wip.h：C 中的 wip 模型
wip.c：RV 监控器
wip.c 文件包含监控器声明和系统仪器的起点。
监控器宏¶
rv/da_monitor.h 使用 C 宏为 监控器实例 启用自动代码生成。
使用宏进行监控器合成的好处是三方面的，因为它
减少了代码重复；
方便了错误修复/改进；
避免了开发人员更改监控器代码核心以（假设）非标准方式操作模型的情况。
此初始实现提供了三种不同的监控器实例类型
#define DECLARE_DA_MON_GLOBAL(name, type)#define DECLARE_DA_MON_PER_CPU(name, type)#define DECLARE_DA_MON_PER_TASK(name, type)
第一个声明全局确定性自动机监控器的函数，第二个声明每个 CPU 实例的监控器函数，第三个声明每个任务实例的函数。
在所有情况下，“name” 参数都是一个标识监控器的字符串，“type” 参数是 dot2k 在 C 中表示模型时使用的数据类型。
例如，具有两个状态和三个事件的 wip 模型可以存储在“unsigned char”类型中。考虑到抢占控制是每个 CPU 的行为，则“wip.c”文件中的监控器声明为
DECLARE_DA_MON_PER_CPU(wip, unsigned char);
通过发送要通过以下函数处理的事件来执行监控器
da_handle_event_$(MONITOR_NAME)($(event from event enum));
da_handle_start_event_$(MONITOR_NAME)($(event from event enum));
da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum));
函数 da_handle_event_$(MONITOR_NAME)() 是常规情况，如果监控器正在处理事件，则将处理该事件。
启用监控器后，它将放置在自动机的初始状态。但是，监控器不知道系统是否处于 初始状态。
da_handle_start_event_$(MONITOR_NAME)() 函数用于通知监控器系统正在返回到初始状态，因此监控器可以开始监控下一个事件。
da_handle_start_run_event_$(MONITOR_NAME)() 函数用于通知监控器已知系统处于初始状态，因此监控器可以开始监控并监控当前事件。
以 wip 模型为例，“preempt_disable”和“sched_waking”事件应分别通过 [2] 发送到监控器
da_handle_event_wip(preempt_disable_wip);
da_handle_event_wip(sched_waking_wip);
而“preempt_enabled”事件将使用
da_handle_start_event_wip(preempt_enable_wip);
通知监控器系统将返回到初始状态，因此系统和监控器应同步。
最后说明¶
通过使用 rv/da_monitor.h 和 dot2k 实现监控器合成，开发人员的工作应仅限于系统仪器，从而提高对整体方法的信心。
[1] 有关确定性自动机格式以及从一种表示形式到另一种表示形式的转换的详细信息，请参见
Documentation/trace/rv/deterministic_automata.rst
[2] dot2k 将监控器的名称后缀附加到事件枚举中，以避免在导出 BPF 程序使用的全局 vmlinux.h 时发生冲突的变量。