Popek and Goldberg Virtualization Requirements - Virtualization Theorems

Virtualization Theorems

To derive their virtualization theorems, which give sufficient (but not necessary) conditions for virtualization, Popek and Goldberg introduce a classification of instructions of an ISA into 3 different groups:

Privileged instructions

Those that trap if the processor is in user mode and do not trap if it is in system mode.

Control sensitive instructions

Those that attempt to change the configuration of resources in the system.

Behavior sensitive instructions

Those whose behavior or result depends on the configuration of resources (the content of the relocation register or the processor's mode).

The main result of Popek and Goldberg's analysis can then be expressed as follows.

Theorem 1. For any conventional third-generation computer, an effective VMM may be constructed if the set of sensitive instructions for that computer is a subset of the set of privileged instructions.

Intuitively, the theorem states that to build a VMM it is sufficient that all instructions that could affect the correct functioning of the VMM (sensitive instructions) always trap and pass control to the VMM. This guarantees the resource control property. Non-privileged instructions must instead be executed natively (i.e., efficiently). The holding of the equivalence property also follows.

This theorem also provides a simple technique for implementing a VMM, called trap-and-emulate virtualization, more recently called classic virtualization: because all sensitive instructions behave nicely, all the VMM has to do is trap and emulate every one of them.

A related problem is that of deriving sufficient conditions for recursive virtualization, that is, the conditions under which a VMM that can run on a copy of itself can be built. Popek and Goldberg present the following (sufficient) conditions.

Theorem 2. A conventional third-generation computer is recursively virtualizable if

1. it is virtualizable and
2. a VMM without any timing dependencies can be constructed for it.

Some architectures, like the non-hardware-assisted x86, do not meet these conditions, so they cannot be virtualized in the classic way. But architectures can still be fully virtualized (in the x86 case meaning at the CPU and MMU level) by using different techniques like binary translation, which replaces the sensitive instructions that do not generate traps, which are sometimes called critical instructions. This additional processing however makes the VMM less efficient in theory, but hardware traps have non-negligible performance cost as well, and a well-tuned caching binary translation system may achieve comparable performance, and it does in the case of x86 binary translation relative to first generation x86 hardware assist, which merely made sensitive instructions trappable. Effectively this gives a theorem with different sufficiency conditions.