SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Fri 9 Dec 2022 16:00 - 16:30 at AMRF Auditorium - Systems and Verification Chair(s): Suresh Jagannathan

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.

Fri 9 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:00
Systems and VerificationOOPSLA at AMRF Auditorium
Chair(s): Suresh Jagannathan Purdue University
15:30
30m
Talk
BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs
OOPSLA
Fengmin Zhu MPI-SWS, Michael Sammler MPI-SWS, Rodolphe Lepigre MPI-SWS, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS
DOI
16:00
30m
Talk
Compositional Virtual Timelines: Verifying Dynamic-Priority Partitions with Algorithmic Temporal Isolation
OOPSLA
Mengqi Liu Yale University, Zhong Shao Yale University, Hao Chen Yale University, Man-Ki Yoon Yale University, Jung-Eun Kim Yale University
DOI
16:30
30m
Research paper
Linear types for large-scale systems verificationDistinguished Paper
OOPSLA
Jialin Li , Andrea Lattuada ETH Zurich, Yi Zhou Carnegie Mellon University, Jonathan Cameron Carnegie Mellon University, Jon Howell VMWare Research, Bryan Parno Carnegie Mellon University, USA, Chris Hawblitzel Microsoft Research
DOI