Synthesizing memory models from framework sketches and Litmus tests
Abstract
A memory consistency model specifies which writes to shared memory a given read may see. Ambiguities or errors in these specifications can lead to bugs in both compilers and applications. Yet architectures usually define their memory models with prose and litmus tests—small concurrent programs that demonstrate allowed and forbidden outcomes. Recent work has formalized the memory models of common architectures through substantial manual effort, but as new architectures emerge, there is a growing need for tools to aid these efforts.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jun 14, 2017
- Source ID
- 10.1145/3140587.3062353
Entities
People
- Emina Torlak
- James Bornholt
Organizations
- Defense Advanced Research Projects Agency
- University of Washington