TY - JOUR
T1 - Formal virtualization requirements for the ARM architecture
AU - Penneman, Niels
AU - Kudinskas, Danielius
AU - Rawsthorne, Alasdair
AU - De Sutter, Bjorn
AU - De Bosschere, Koen
PY - 2013
Y1 - 2013
N2 - We present an analysis of the virtualizability of the ARMv7-A architecture carried out in the context of the seminal paper published by Popek and Goldberg 38 years ago. Because their definitions are dated, we first extend their machine model to modern architectures with paged virtual memory, IO and interrupts. We then use our new model to show that ARMv7-A is not classically virtualizable. Insights such as binary translation enable efficient virtualization beyond the original criteria. Companies are also making their architectures virtualizable through extensions. We analyse both approaches for ARM and conclude that both have their use in future systems. © 2013 Elsevier B.V. All rights reserved.
AB - We present an analysis of the virtualizability of the ARMv7-A architecture carried out in the context of the seminal paper published by Popek and Goldberg 38 years ago. Because their definitions are dated, we first extend their machine model to modern architectures with paged virtual memory, IO and interrupts. We then use our new model to show that ARMv7-A is not classically virtualizable. Insights such as binary translation enable efficient virtualization beyond the original criteria. Companies are also making their architectures virtualizable through extensions. We analyse both approaches for ARM and conclude that both have their use in future systems. © 2013 Elsevier B.V. All rights reserved.
KW - Binary translation
KW - Hypervisor
KW - Instruction set architecture
KW - Virtual machine monitor
KW - Virtualization
UR - https://www.scopus.com/pages/publications/84875454407
U2 - 10.1016/j.sysarc.2013.02.003
DO - 10.1016/j.sysarc.2013.02.003
M3 - Article
SN - 1383-7621
VL - 59
SP - 144
EP - 154
JO - Journal of Systems Architecture
JF - Journal of Systems Architecture
IS - 3
ER -