Data-Race-Freedom of Concurrent Programs

Reasoning about access isolation in a program that uses locks, transactions or both to coordinate accesses to shared memory is complex and error-prone. The programmer must understand when accesses issued to the same memory by distinct threads, under possibly different coordination semantics, are isolated, otherwise, data races are introduced. We present a program analysis that guarantees a program is data-race-free irrespective of whether locks, transactions or both are used to coordinate accesses to memory. Our framework entails two main steps: (i) a program is statically executed to determine its memory space and the types of accesses it issues to that memory, then (ii) our isolation algorithm checks that the accesses issued by the program do not result in a data race. To the best of our knowledge our work is the first to guarantee the data-race-freedom of concurrent programs that use locks, transactions or both to coordinate accesses to mutable memory.