Publication
Balancing the Load: Leveraging a Semantics Stack for Systems Verification
Eyad Alkassar; Mark Hillebrand; Dirk Leinenbach; Norbert Schirmer; Artem Starostin; Alexandra Tsyban
In: Journal of Automated Reasoning (JAR), Vol. 42, No. 2-4, Pages 389-454, Springer, 2/2009.
Abstract
We have developed a stack of semantics for a high-level C-like language and
low-level assembly code, which has been carefully crafted to support the
pervasive verification of system software. It can handle mixed-language
implementations and concurrently operating devices, and permits the transferral
of properties to the target architecture while obeying its resource
restrictions. We demonstrate the applicability of our framework by proving the
correct virtualization of user memory in our microkernel, which implements
demand paging. This verification target is of particular interest because it
has a relatively simple top-level specification and it exercises all parts of
our semantics stack. At the bottom level a disk driver written in assembly
implements page transfers via a swap disk. A page-fault handler written in C
uses the driver to implement the paging algorithm. It guarantees that a step
of the currently executing user can be simulated at the architecture level.
Besides the mere theoretical and technical difficulties the project also bore
the social challenge to manage the large verification effort, spread over many
sites and people, concurrently contributing to and maintaining a common theory
corpus. We share our experiences and elaborate on lessons learned.