Safe optimisations for shared-memory concurrent programs

11 years 6 months ago
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...
Jaroslav Sevcík
Added 17 Sep 2011
Updated 17 Sep 2011
Type Journal
Year 2011
Where PLDI
Authors Jaroslav Sevcík
Comments (0)