Memory-Model-Sensitive Data Race Analysis

11 years 6 months ago
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 —...
Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Authors Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom
Comments (0)