From 2013 to the present, our work on specifying, verifying and translating memory consistency models has led to a number of publications, tool releases, and industry adoption.
Perhaps most importantly for a verification project, our verification tools have found numerous major design errors at this point. These include:
- New speculative execution attack varaints affecting Intel processors (more info).
- Fundamental deficiencies in the draft specification of a widely-discussed instruction set architecture (more info).
- An error in the consistency implementation for a widely used simulator (more info).
- A corner case in a proposed lazy coherence method (more info)(updated spec).
- Errors in compiler mappings for translating high-level synchronization primitives onto particular instruction sets with weak memory model. And, an error in the formal proof previously thought to ensure the correctness of those mappings (more info).
- An error in the RTL implementation of memory in an open-source processor. (more info).
Beyond these concrete bug discoveries, our tools have also been used to reproduce other known bugs and deepen understanding of them.