確定性自動機監視器合成¶
執行時驗證 (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 時出現變數衝突。