Title: An Operational Framework for Specifying Memory Models using Instantaneous Instruction Execution,
Abstract: There has been great progress recently in formally specifying the memory
model of microprocessors like ARM and POWER. These specifications are, however,
too complicated for reasoning about program behaviors, verifying compilers
etc., because they involve microarchitectural details like the reorder buffer
(ROB), partial and speculative execution, instruction replay on speculation
failure, etc. In this paper we present a new Instantaneous Instruction
Execution (I2E) framework which allows us to specify weak memory models in the
same style as SC and TSO. Each instruction in I2E is executed instantaneously
and in-order such that the state of the processor is always correct. The effect
of instruction reordering is captured by the way data is moved between the
processors and the memory non-deterministically, using three conceptual
devices: invalidation buffers, timestamps and dynamic store buffers. We prove
that I2E models capture the behaviors of modern microarchitectures and
cache-coherent memory systems accurately, thus eliminating the need to think
about microarchitectural details.