Safe optimisations for shared-memory concurrent programs

Current proposals for concurrent shared-memory languages, including C++ and C, provide sequential consistency only for programs without data races (the DRF guarantee). While the implications of such a contract for hardware optimisations are relatively well-understood, the correctness of compiler optimisations under the DRF guarantee is less clear, and experience with Java shows that this area is error-prone. In this paper we give a rigorous study of optimisations that involve both reordering and elimination of memory reads and writes, covering many practically important optimisations. We first define powerful classes of transformations semantically, in a languageindependent trace semantics. We prove that any composition of these transformations is sound with respect to the DRF guarantee, and moreover that they provide basic security guarantees (no thinair reads) even for programs with data races. To give a concrete example, we apply our semantic results to a simple imperative langua...

• Type: Journal
• Year: 2011
• Where: PLDI
• Authors: Jaroslav Sevcík
• Keywords: PLDI 2011, Programming Languages, Reliability Theory, Sequential Consistency, Trace Semantics