Title :
Verifying shadow page table algorithms
Author :
Alkassar, Eyad ; Cohen, Emmanuel ; Hillebrand, M. ; Kovalev, Mikhail ; Paul, Wolfgang J.
Author_Institution :
Saarland Univ., Saarbrücken, Germany
Abstract :
Efficient virtualization of translation lookaside buffers (TLBs), a core component of modern hypervisors, is complicated by the concurrent, speculative walking of page tables in hardware. We give a formal model of an x64-like TLB, criteria for its correct virtualization, and outline the verification of a virtualization algorithm using shadow page tables. The verification is being carried out in VCC, a verifier for concurrent C code.
Keywords :
buffer storage; formal verification; virtualisation; VCC; hypervisors; shadow page table algorithm verification; translation lookaside buffer virtualization; x64-like TLB; Arrays; Hardware; Legged locomotion; Registers; Switches; Virtual machine monitors;
Conference_Titel :
Formal Methods in Computer-Aided Design (FMCAD), 2010
Conference_Location :
Lugano
Print_ISBN :
978-1-4577-0734-6
Electronic_ISBN :
978-0-9835678-0-6
