Checking microarchitectural implementations of weak memory

Опубликовано 22 июня 2016, 2:34

In parallel programs, threads communicate according to the memory consistency model: the set of memory ordering rules enforced by a given architecture. A great deal of research effort has gone into rigorous formalization of memory models. However, comparatively little attention has been paid to the microarchitectural implementation of these models. Standard testing-based techniques are insufficient: unobserved behaviors are not guarantees of non-observability, and failed tests offer little insight into the microarchitectural reason behind failure. I will present PipeCheck, a methodology and automated tool for verifying that a given microarchitecture correctly implements the memory consistency model specified by its architectural specification. PipeCheck adapts the formal notion of a "happens before" graph to the microarchitecture space. Architectural specifications such as preserved program order are then treated as propositions to be verified, rather than simply as assumptions. We also specify and analyze the behavior of common microarchitectural optimizations such as speculative load reordering. Using PipeCheck, we were able to validate the OpenSPARC T2 in just minutes, and we found and fixed a bug in a architectural simulator widely used in academia. PipeCheck has been nominated for the Best Paper award at MICRO 2014, to be held in Cambridge, UK this December. At the end, I will also briefly introduce ArMOR, a framework for defining dynamic binary translation layers that seamlessly translate between memory consistency models such as those used by x86, ARM, and Power.