Daniel Lustig, Michael Pellauer, Margaret Martonosi. Pipe Check: Specifying and Verifying Microarchitectural Enforcement of Memory Consistency Models. In 47th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2014, Cambridge, United Kingdom, December 13-17, 2014. pages 635-646, IEEE, 2014. [doi]
Abstract is missing.