2 Related Work

2.1 System-Level Emulators

There are many x86 emulators. Emulators such as Bochs [7] and QEMU [6] do not aim to accurately implement undefined behavior, as most software runs correct. Some emulators, such as MartyPC [17] implement fully accurate semantics and cycle-accurate timing. However, this work relies on the reverse-engineered 8086/8088 microcode and has currently not advanced beyond the original 808x CPUs. All these emulators hard-code their semantics, meaning the semantics cannot be easily changed, or extracted and translated to different formats.

2.2 x86 Semantics

Models of x86 semantics, such as the x86isa ACL2 model by Goel et al. [11], as well as its translation into SAIL [12] and Gem5 [8] allow for full-system execution. ACL2 and Gem5 can execute these semantics directly, while SAIL can generate emulators as C or OCaml code.

A lack of hardware implementations, as well as performance issues, make it impractical to run real operating systems on these emulators. The emulators do not support most of the hardware required to boot regular operating systems, and are only able to boot Linux kernels. The x86isa project requires compiling Linux from scratch because it does not implement standard x86 timer- and display functionality. Gem5 generally does not execute normal bootloaders, and instead loads a (Linux) kernel image directly. We were unable to verify if the SAIL x86 semantics are able to generate a functional emulator, as only instructions for MIPS emulation are provided.

In full-system emulation mode, the ACL2 model can execute around 320 thousand instructions per second [11]. The SAIL model has similar execution performance when booting an FreeBSD kernel. At this performance level, it would take two to three hours to boot a typical Windows XP installation, or half a day for Windows 7. This makes it unfeasible to use these emulators for typical x86 operating systems.

Pydrofoil [18] generates a JITing emulator from the RISC-V SAIL specification and achieves a $250\times$ speedup over the default emulator generated by SAIL. However, despite this speedup, which allows it to reach a peak of 22 million instructions executed per second in some benchmarks, its performance still falls short of QEMU and Bochs: it is still $26.7\times$ slower than QEMU. In comparison, according to our measurements, Sem86 is just 2.1 times slower than QEMU.

Captive [19] can automatically generate emulators from a specification. In ARM benchmarks, it achieves a $1.68\times$ speedup over QEMU. The emulator runs partially inside a virtual machine, as a bare metal program. A bare metal program can use hardware features typically only accessible by operating systems, which makes it possible to generate more efficient code, but requires a host with virtualization support (KVM). It currently only supports emulation of x86-64 in userspace mode, and does not support 32-bit x86 at all.

Many other semantics exist, but only focused on userspace [13, 14, 16, 20–22]. For example, Morrisett et al. [20] implemented a Coq model for a subset of x86, for use in Google’s Native Client (NaCl). The CompCert compiler [21] proves equivalence between C source code and compiled artifacts, using a Coq model for x86 which also only implements a subset of x86. While all of these semantics are executable, and some have been used to implement userspace emulators [16], none are capable of full-system emulation.