Abstract

The Lyrebird framework for hardware simulators with formal semantics was developed during the L4.verified project, as an attempt to bridge the gap between the C language model and the underlying hardware, particularly for machine-management operations, such as cache flushing and page table switching. Lyrebird was initially presented at SSV 2010 .

As the scope of the overall project was curtailed, focussing sucessfully on the refinement between the abstract specification and the C language implementation, the Lyrebird work remained incomplete. What already exists is a DSL , together with compilers into both Isabelle/HOL and C, for specifying an interconnected processor architecture, including an ARM CPU core, a memory management unit, and a cache controller. This talk will explore whether this work might be combined with the more recent, and more complete, formalisations of the user-level semantics of the ARM instruction set: Particularly, whether they might be integrated to produce a sufficiently detailed machine model to support the verification of systems software.