• DocumentCode
    545677
  • 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
  • fYear
    2010
  • fDate
    20-23 Oct. 2010
  • Firstpage
    267
  • Lastpage
    270
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • 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
  • Type

    conf

  • Filename
    5770958
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=545677