A theory of data race detection

ABSTRACT

This paper presents a rigorous mathematical theory for the detection of data races in threaded programs. After creating a structure with precise definitions and theorems, it goes on to develop four algorithms with the goal of detecting at least one race in the situation where the history kept on previous memory accesses is limited. The algorithms demonstrate the tradeoff between the amount of access history kept and the kinds of data races that can be detected. One of these algorithms is a reformulation of a previously known algorithm; the other three are new. One of the new ones is actually used in the tool called Intel® Thread Checker.

REFERENCES

• 1: U. Banerjee, B. Bliss, Z. Ma, and P. Petersen. Unraveling Data Race Detection in the Intel® Thread Checker. Presented at The First Workshop on Software Tools for Multi-core Systems (STMCS), in conjunction with IEEE/ACM International Symposium on Code Generation and Optimization (CGO), March 26, 2006, Manhattan, New York, NY.
• 2: C. J. Fidge. Timestamps in Message-Passing Systems that Preserve the Partial Ordering. Proceedings of the 11th Australian Computer Science Conference (ACSC'88), K. Raymond (Editor), February 1988, pp. 56--66.
• 3: Ayal Itzkovitz , Assaf Schuster , Oren Zeev-Ben-Mordehai, Toward integration of data race detection in DSM systems, Journal of Parallel and Distributed Computing, v.59 n.2, p.180-203, Nov. 1999 [doi>10.1006/jpdc.1999.1574]
• 4: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 5: F. Mattern. Virtual Time and Global States of Distributed Systems. Proceedings of the International Workshop on Parallel and Distributed Algorithms, Elsevier Science Publishers, M. Corsnard et al. (Editors), Chateau de Bonas, France, October 1988, pp. 215--226.
• 6: Robert H. B. Netzer , Barton P. Miller, What are race conditions?: Some issues and formalizations, ACM Letters on Programming Languages and Systems (LOPLAS), v.1 n.1, p.74-88, March 1992 [doi>10.1145/130616.130623]
• 7: Robert O'Callahan , Jong-Deok Choi, Hybrid dynamic data race detection, Proceedings of the ninth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 11-13, 2003, San Diego, California, USA
• 8: Eli Pozniansky , Assaf Schuster, Efficient on-the-fly data race detection in multithreaded C++ programs, Proceedings of the ninth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 11-13, 2003, San Diego, California, USA
• 9: Michiel Ronsse , Koen De Bosschere, RecPlay: a fully integrated practical record/replay system, ACM Transactions on Computer Systems (TOCS), v.17 n.2, p.133-152, May 1999 [doi>10.1145/312203.312214]
• 10: Ohad Shacham , Mooly Sagiv , Assaf Schuster, Scaling model checking of dataraces using dynamic information, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065958]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming

General Terms:
Algorithms, Reliability, Theory

Keywords:
access conflict, data race, dependence, happens-before, synchronization, thread, vector clock