Physical Addressing on Real Hardware in Isabelle/HOL

Authors

Reto Achermann, Lukas Humbel, David Cock and Timothy Roscoe

Venue

Proceedings of the 9th International Conference on Interactive Theorem Proving (ITP'18)

Links

[ .doi ] [ .pdf ] [ .bib ]

Abstract

Modern computing platforms are inherently complex and diverse: a heterogeneous collection of cores, interconnects, programmable memory translation 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 associated 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 platforms 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 configuration at runtime in the Barrelfish research OS.

Bibtex

@inproceedings{Achermann:2018:PAR,
 author = {Reto Achermann and Lukas Humbel and David Cock and Timothy Roscoe},
 booktitle = {Proceedings of the 9th International Conference on Interactive Theorem Proving},
 doi = {10.1007/978-3-319-94821-8_1},
 id = {Achermann:2018:PAR},
 isbn = {978-3-319-94821-8},
 keywords = {},
 location = {Oxford, UK},
 pages = {1--19},
 publisher = {Springer International Publishing},
 series = {ITP'18},
 title = {Physical Addressing on Real Hardware in Isabelle/HOL},
 url = {https://doi.org/10.1007/978-3-319-94821-8_1},
 year = {2018}
}

Contact

The University of British Columbia
Department of Computer Science
2366 Main Mall
ICICS Building, Office 341
Vancouver, BC V6T 1Z4
Canada

achreto [at] cs.ubc.ca
+1 604 827 2446