University of Cambridge > > Microsoft Research Cambridge, public talks > Checking microarchitectural implementations of weak memory

Checking microarchitectural implementations of weak memory

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

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.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity