一句话：提出组合式虚拟时间线抽象，用 Coq 机器化验证带预算的 EDF 分区内核并证明分区间时间隔离。
实时系统承载安全攸关应用，需要在微体系结构与算法两个层面实现强隔离，其中算法级隔离主要源于调度引起的相互干扰。这类系统实现复杂，需形式化验证才能保证隔离正确。本文针对最早截止期优先（EDF）分区，在任务周期上施加约束、在周期性分区上施加预算，以同时获得组合性与资源利用率，并强制分区之间的隔离。由于分区级动态优先级分配本身极其复杂，直接验证具体调度器十分困难。作者提出组合式虚拟时间线框架，通过动态构造的抽象把具体调度器的推理提升到抽象域，从而在抽象层面完成论证。基于该框架，作者验证了一个实施预算的 EDF 分区实时操作系统内核，证明其确实保证了分区之间的隔离，全部证明均在 Coq 中机器化完成。
Real-time systems power safety-critical applications that require strong isolation among each other. Such isolation needs to be enforced at two orthogonal levels. On the micro-architectural level, this mainly involves avoiding interference through micro-architectural states, such as cache lines. On the algorithmic level, this is usually achieved by adopting real-time partitions to reserve resources for each application. Implementations of such systems are often complex and require formal verification to guarantee proper isolation. In this paper, we focus on algorithmic isolation, which is mainly related to scheduling-induced interferences. We address earliest-deadline-first (EDF) partitions to achieve compositionality and utilization, while imposing constraints on tasks' periods and enforcing budgets on these periodic partitions to ensure isolation between each other. The formal verification of such a real-time OS kernel is challenging due to the inherent complexity of the dynamic priority assignment on the partition level. We tackle this problem by adopting a dynamically constructed abstraction to lift the reasoning of a concrete scheduler into an abstract domain. Using this framework, we verify a real-time operating system kernel with budget-enforcing EDF partitions and prove that it indeed ensures isolation between partitions. All the proofs are mechanized in Coq.
@article{paperbot1457,
title = {Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation},
author = {Mengqi Liu and Zhong Shao and Hao Chen and Man-Ki Yoon and Jung-Eun Kim},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563290}
}