Making Sense of Complex Real-World Memory Consistency Models

In the shared memory parallel programming model, data values in memory are made visible to the threads of a program following the rules of a memory consistency model. In the past, memory model definitions have relied on natural language descriptions, programmer intuition, and/or sets of examples to specify how memory should behave. In recent years, however, a fundamental shift has been taking place. Many popular programming languages (C/C++, Java, OpenCL) and processor architectures (x86-TSO, Power, ARM, GPUs) have deprecated their informal memory model descriptions in favor of mathematically-rigorous formal specifications. Is this really necessary? Why deal with the extra complexity and obfuscation presented by formalization? Aren't simpler descriptions sufficient?

In the first part of my talk, I will demonstrate how under-specifying a memory model can leave it prone to wildly unexpected behaviors. I will then show how the types of formalization used in modern real-world memory models can actually make it easier (yes, easier!) to restore sanity to these models. For the second part of my talk, I will present my thesis work on uhbCheck, a methodology and set of tools for specifying and verifying memory model implementations at the microarchitecture level. I will show how uhbCheck has allowed architects to verify the correctness of and eliminate bugs in hardware optimizations such as out-of-order execution, speculative load reordering, and lazy cache coherence. To conclude, I will describe how modern research tools are making it increasingly possible to prove programs correct from the language level all the way down to the microarchitecture level, and I will explain how this is both interesting from a research perspective and extremely useful from a practical debugging point of view.

Speaker: Daniel Lustig, NVIDIA