确定性自动机监视器合成¶
运行时验证 (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 时出现变量冲突。