A Correctness Proof of a Speculative, Superscalar, Out-of-Order, Renaming Microarchitecture

Microarchitects are increasingly using techniques such as speculation, register renaming, and superscalar out-of-order execution to make use of instruction-level parallelism. However, the growing complexity of modern microprocessors exacerbates the difficulty of relating them to the simple machines that they emulate. Flaws found later in lower-level validation are often microarchitectural in nature. In this paper we provide high-level mathematical specifications for a basic machine and for a...