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:
- 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).
Beyond these concrete bug discoveries, our tools have also been used to reproduce other known bugs and deepen understanding of them.