The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Compositional Virtual Timeline: Verifying Dynamic-Priority Partitions with Algorithmic Temporal Isolation

Last modified: Fri Sep 16 19:55:01 2022 GMT.

Authors

Mengqi Liu
Zhong Shao
Hao Chen
Man-Ki Yoon
Jung-Eun Kim

Abstract

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.

Published

In Proc. 2022 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'22), Auckland, New Zealand, October 2022. Published as Proceedings of the ACM on Programming Languages (PACMPL), Volume 6, Number OOPSLA2, Article 127 (October 2022), 29 pages.
  • Conference Paper [PDF]

  • Copyright © 1996-2022 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon