Memory virtualization by means of demand paging is a crucial component of every modern operating system. The formal verification is challenging since reasoning about the page fault handler has to cover two concurrent computational sources: the processor and the hard disk. We accurately model the interleaved executions of devices and the page fault handler, which is written in a high-level programming language with inline assembler portions. We describe how to combine results from sequential Hoare logic style reasoning about the page fault handler on the low-level concurrent machine model. To the best of our knowledge this is the first example of pervasive formal verification of software communicating with devices.

Online Copy

Available as PDF-File

BibTeX Entry

@inproceedings{Alkassar-TACAS08, AUTHOR = {Alkassar, Eyad and Schirmer, Norbert and Starostin, Artem}, TITLE = {Formal Pervasive Verification of a Paging Mechanism}, VOLUME = {4963}, YEAR = {2008}, PAGES = {109-123}, SERIES = {LNCS}, BOOKTITLE = {14th intl Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS08)}, PUBLISHER = {Springer}, EDITOR = {C. R. Ramakrishnan and Jakob Rehof}, EE = {http://dx.doi.org/10.1007/978-3-540-78800-3_9}, }