Physical addressing on real hardware in Isabelle/HOL

Authors: Reto Achermann, Lukas Humbel, David Cock and Timothy Roscoe

Paper Information

Title:Physical addressing on real hardware in Isabelle/HOL
Authors:Reto Achermann, Lukas Humbel, David Cock and Timothy Roscoe
Proceedings:ITP Papers
Editors: Jeremy Avigad and Assia Mahboubi
Keywords:Isabelle/HOL, MIPS TLB, Hardware model, HW-SW interface, Memory

ABSTRACT. Modern computing platforms are inherently complex and diverse: a heterogeneous collection of cores, interconnects, programmable memory transla- tion units, and devices means that there is no single physical address space, and each core or DMA device may see other devices at different physical addresses. This is a problem because correct operation of system software relies on correct configuration of these interconnects, and current operating systems (and asso- ciated formal specifications) make assumptions about global physical addresses which do not hold. We present a formal model in Isabelle/HOL to express this complex addressing hardware that captures the intricacies of different real plat- forms or Systems-on-Chip (SoCs), and demonstrate its expressivity by showing, as an example, the impossibility of correctly configuring a MIPS R4600 TLB as specified in its documentation. Such a model not only facilitates proofs about hardware, but is used to generate correct code at compile time and device config- uration at runtime in the Barrelfish research OS.

Talk:Jul 11 09:30 (Session 60D)