Skip to main content

Implementing hardware-supported virtualization in OKL4 on ARM


Prashant Varanasi

NICTA, Sydney, Australia
UNSW, Australia


Virtualization is an already popular trend in the desktop and server markets, and is becoming increasingly important on mobile devices, where ARM is the leading architecture. This thesis presents the design and implementation of a hypervisor integrating ARM's recently announced virtualization extensions. This hypervisor is capable of running multiple concurrent unmodified guest operating systems such as Linux, and supporting efficient communication between guests. Benchmarking in ARM's Fast Models simulator show that virtualization overheads are small, although true overheads cannot be measured till hardware or a timing-accurate simulator is released.

BibTeX Entry

    author           = {Prashant Varanasi},
    month            = nov,
    year             = {2010},
    title            = {Implementing Hardware-supported Virtualization in {OKL4} on {ARM}},
    address          = {Sydney, Australia},
    school           = {School of Computer Science and Engineering}


Served by Apache on Linux on seL4.