Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads
Authors
Xinyu Feng
Zhong Shao
Yu Guo
Yuan Dong
Abstract
Hardware interrupts are widely used in the world's critical software
systems to support preemptive threads, device drivers, operating
system kernels, and hypervisors. Handling interrupts properly is an
essential component of low-level system programming. Unfortunately,
interrupts are also extremely hard to reason about: they dramatically
alter the program control flow and complicate the invariants in
low-level concurrent code (e.g., implementation of synchronization
primitives). Existing formal verification techniques---including
Hoare logic, typed assembly language, concurrent separation logic, and
the assume-guarantee method---have consistently ignored the issues of
interrupts; this severely limits the applicability and power of
today's program verification systems.
In this paper we present a novel Hoare-logic-like framework for
certifying low-level system programs involving both hardware
interrupts and preemptive threads. We show that enabling and disabling
interrupts can be formalized precisely using simple ownership-transfer
semantics, and the same technique also extends to the concurrent
setting. By carefully reasoning about the interaction among interrupt
handlers, context switching, and synchronization libraries, we are
able to---for the first time---successfully certify a preemptive
thread implementation and a large number of common synchronization
primitives. Our work provides a foundation for reasoning about
interrupt-based kernel programs and makes an important advance toward
building fully certified operating system kernels and hypervisors.
Published
Copyright © 2011 Xinyu Feng
|