Memory-Model-Sensitive Data Race Analysis

Abstract. We present a “memory-model-sensitive” approach to validating correctness properties for multithreaded programs. Our key insight is that by specifying both the inter-thread memory consistency model and the intra-thread program semantics as constraints, a program verification task can be reduced to an equivalent constraint solving problem, thus allowing an exhaustive examination of all thread interleavings precisely allowed by a given memory model. To demonstrate, this paper formalizes race conditions according to the new Java memory model, for a simplified but non-trivial source language. We then describe the implementation of a memory-model-sensitive race detector using constraint logic programming (CLP). In comparison with conventional program analysis, our approach does not offer the same kind of performance and scalability due to the complexity involved in exact formal reasoning. However, we show that a formal semantics can serve more than documentation purposes —...

• Type: Conference
• Year: 2004
• Where: ICFEM
• Authors: Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom
• Keywords: ICFEM 2004, Intra-thread Program Semantics, Memory Consistency Model, Memory Model