Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation
Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation
复制标题
DOI：
10.1145/3563290
复制
发表时间：
2022-10
影响因子：
--
通讯作者：
Meng-qi Liu;Zhong Shao;Hao Chen;Man-Ki Yoon;Jung-Eun Kim
中科院分区：
文献类型：
--
作者：
Meng-qi Liu;Zhong Shao;Hao Chen;Man-Ki Yoon;Jung-Eun Kim
实时系统支持需要彼此之间强隔离的安全关键型应用。这种隔离需要在两个正交级别上实施。在微架构级别，这主要涉及避免通过微架构状态（例如缓存行）的干扰。在算法层面上，这通常是通过采用实时分区来为每个应用程序预留资源来实现的。这种系统的实现通常是复杂的，需要正式的验证，以保证适当的隔离。在本文中，我们专注于算法隔离，这主要是有关的干扰引起的干扰。我们解决最早的截止日期优先（EDF）分区，以实现组合性和利用率，同时对任务的周期施加约束，并对这些周期性分区执行预算，以确保彼此之间的隔离。这种实时操作系统内核的正式验证是具有挑战性的，由于固有的复杂性的动态优先级分配的分区级别。我们解决这个问题，通过采用一个动态构造的抽象提升到一个抽象域的具体调度的推理。使用这个框架，我们验证了一个实时操作系统内核与执行EDF分区，并证明它确实确保分区之间的隔离。所有的证据都是机械化的。
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.