Relaxed memory-consistency models are a fact of life that affect the meaning of multithreaded high-level programming languages in ways language designers, language implementors, and programmers cannot ignore. Both computer architectures and compilers can reorder memory operations in unintuitive ways and it is not feasible to prohibit all such reorderings. We are interested in making this nebulous world more sane without requiring overly strict requirements nor inventing more arcane memory models.
One approach, which has been taken by popular languages such as C and C++, is to assume that programs are data-race-free. Given this assumption, to what extent can we reason sequentially and locally about memory accesses in a program? Can we eliminate redundant loads within a synchronization-free region? Across a lock operation? Across a critical section?
It is well-known that the answer to the first question is "yes," but in our paper Extended Sequential Reasoning for Data-Race-Free Programs, we answer the second two questions, as well as other interesting code analysis questions, in the affirmative. This paper appeared at the workshop on memory systems correctness and performance (MSPC 2011); PDF.
This project is joint work with Hans-J. Boehm, Dhruva Chakrabarti, and Pramod Joisha of HP Labs.
We are also interested in how to design Modular Metatheory for Memory Consistency Models. We have developed a framework for modeling relaxed memory models using operational semantics. Our framework is modular: the semantics of the memory model is completely separate from the semantics of the rest of the programming language. This modularity means that our results generalize to many different languages and to many different memory models. The framework is also very flexible: it is possible to create memory models that support instruction reordering, non-atomic writes and speculative reads. All of the semantics and proofs have been mechanically verified using Coq and Proof General. The mechanization process has been incredibly useful for eliminating any errors or ambiguities (not that we had any of those, of course! ;) ).
This project is available as a technical report here. (TR#: UW-CSE-11-02-01)
Our Coq code is available here. That tarball includes a copy of the Metatheory library for Coq 8.2 (available here) - we had to make a one-line change in order to get it working with Coq's FMap library.
Current contacts: Laura Effinger-Dean, Dan Grossman