been implicit. Now we describe an algorithm where we always keep the last segment to write x and the last segment to read x for each active thread. Like Algorithm 4, this algorithm is able to detect at least one race if there are races. The storage requirements are di erent however; we comment on that issue in Remark 18 below. First, we need some definitions and results.

We say that there is a current flow conflict in x between two segments Si and Sj, where 1 ≤ i < j ≤ n, if at some given point, Si is the last segment to write x on its thread, Sj is the last segment to read x on its thread, and Si k Sj. Current conflicts of the other three types are defined in a similar way. A current race in x is a current conflict of type flow, anti, or output. Our algorithm in this subsection is based on the following theorem.

Theorem 17. If there is an access conflict in x of a given type, then there must be a current conflict in x of the same type.

Proof. The particular type of conflict chosen is irrelevant here. For definiteness, assume that there is a flow conflict in x between two segments Si and Sj such that 1 ≤ i < j ≤ n. Focus on the moment when Sj becomes the last segment to read x on its thread. By hypothesis, Si has already written x. If it is currently the last segment to write x on its thread, then we have a current flow conflict, and there is nothing left to prove.

Assume then that Si is not currently the last segment to write x on its thread. Let Sq denote the last segment to write x on the thread of Si, when Sj is the last segment to read x on the thread of Sj. Note that we have i < q < j. By hypothesis, Si and Sj are parallel. Lemma 6 then implies that either the segments Si and Sq are parallel, or the segments Sq and Sj are parallel. The first possibility is ruled out since Si and Sq belong to the same thread. Hence, Sq and Sj are parallel. These two segments cause a current conflict in x.

Corollary 2. If there is a race in x, then there must be a current race in x.

Proof. A race is an access conflict of type flow, anti, or output. If there is an access conflict of one of these three types, then there must also be a current conflict of the same type which is a current race.

Algorithm 5 (Current Conflict Detection Algorithm)

This algorithm detects all current conflicts in a location x in shared memory that is accessed by the given program. It can always detect if there is a data race in x, although it may not find all races. The requirement is that at any given point and for each active thread T , the information about the last segment on T to read x and the last segment on T to write x are always available.

Whenever a segment Sj is found to access x, compare it first with the last-write segment of each thread to see if the segments cause a current output or flow conflict. Then, compare Sj with the last-read segment of each thread to see if the segments cause a current anti or input conflict.

If, at the end of program execution, we report at least one current conflict of type flow, anti, or output, then there is a data race in x. Otherwise, there is no data race in x.

Remark 18 Algorithms 4 and 5 have similar capabilities: Each will predict at least one race if there are races, and each will say there are no races when there are none. For a given memory location x, Algorithm 5 needs to keep 2t segments at each step where t is the number of active threads: 2 segments for each thread. Algorithm 4, on the other hand, needs to keep only (p + 1) segments: 1 write-segment and p read-segments that are mutually parallel. Thus, Algorithm 5 needs to keep (2t − p − 1) more segments than Algorithm 4. Since these p read-segments are mutually parallel, they must come from di erent threads, so that t ≥ p. Hence, we have (2t − p − 1) ≥ t − 1. This di erence is huge when there are a large number of threads.

4. PREVIOUS WORK

The fundamental concept used in this paper is that of the precedence relationship ‘ ’ between segments. This is the happens-before relation ‘→’ introduced by Lamport in [4]. He also gives the definition of parallel (concurrent) segments. Logical clocks defined by Lamport in the same paper do not, however, quite capture the parallel relationship ‘k’ between segments. For that we had to use vector clocks.

Vector clocks have been used empirically by several researchers to solve specific problems since the early 1980’s. Fidge [2] and Mattern [5] are generally credited for introducing them as a formal concept and stating their basic properties in 1988, independently of each other.

Our race detection method (based on vector clocks) is similar to the one described in [3], [7], [8], and [9]. A hybrid detection method is described in [7] that combines two techniques one of which is based on the happens-before relation. Unlike the approach taken in [9], we do not use two passes, and we keep the values of vector clocks relatively low by counting only the posting segments that precede a given segment.

The algorithmic approach in [3] and [8] is described in detail in Section 3.4, rephrased in our framework to allow direct comparison with the other algorithms in this paper. Our Algorithm 4 and Algorithm 5 of [3, 8] both solve the entire problem of detecting at least one data race when races are present. Neither one will report a race when there are none. However, the storage requirements of the two are di erent. Let t denote the total number of threads and N the total number of memory locations accessed. Then, Algorithm 4 needs to keep (1 + p)N segments, where p ≤ t, and Algorithm 5 needs to keep 2tN segments.

Algorithm 3 (used by the Intel Thread Checker) may sometimes fail to detect a race in rare situations, but it needs to keep only 2N segments. An experimental discussion of how rare these situations are in real programs is beyond the scope of the present paper.

5. CONCLUSIONS

We have provided a solid mathematical foundation for the theory of data race detection. All four race detection algorithms can be used in a practical situation with di erent goals in mind. The Intel Thread Checker uses Algorithm 3. Practical applications of this algorithm have been possible due to the way it handles the tradeo between the ability to always detect data races and the need to conserve memory usage. By keeping the history of only two previous accesses to a memory location, the Thread Checker manages

to detect the existence of a data race in a vast majority of situations. Algorithm 4 or Algorithm 5 can be used to gain further improvement. Either one is capable of detecting at least one data race if races are present. Also, they will not report a race if there are none. While the two algorithms have similar capabilities, our Algorithm 4 needs less storage than the previously published Algorithm 5.

6.REFERENCES

[1]U. Banerjee, B. Bliss, Z. Ma, and P. Petersen. Unraveling Data Race Detection in the Intel R 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]A. Itzkovitz, A. Schuster, and O. Zeev-Ben-Mordehai. Towards Integration of Data Race Detection in DSM Systems. Journal of Parallel and Distributed Computing, Vol. 59, No. 2, November 1999, pp. 180–203.

[4]L. Lamport. Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM, Vol. 21, No. 7, July 1978, pp. 558–565.

[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]R. H. B. Netzer and B. P. Miller. What are Race Conditions? Some Issues and Formalizations. ACM Letters on Programming Languages and Systems, Vol. 1, No. 1, March 1992, pp. 74–88.

[7]R. O’Callahan and J.-D. Choi. Hybrid Dynamic Data Race Detection. Proceedings of the 2003 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, ACM Press, San Diego, California, June 2003, pp. 167–178.

[8]E. Pozniansky and A. Schuster. E cient On-the-fly Data Race Detection in Multithreaded C++ Programs. Proceedings of the 2003 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, ACM Press, San Diego, California, June 2003, pp. 179–190.

[9]M. Ronsse and K. de Bosschere. RecPlay: a Fully Integrated Practical Record/Replay System. ACM Transactions on Computer Systems, Vol. 17, No. 2, May 1999, pp. 1–17.

[10]O. Shacham, M. Sagiv, and A. Schuster. Scaling Model Checking of Data Races Using Dynamic Information.

Proceedings of the 2005 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming,

ACM Press, Chicago, Illinois, June 2005, pp. 107–118.