Conditional must not aliasing for static race detection

ABSTRACT

Race detection algorithms for multi-threaded programs using the common lock-based synchronization idiom must correlate locks with the memory locations they guard. The heart of a proof of race freedom is showing that if two locks are distinct, then the memory locations they guard are also distinct. This is an example of a general property we call conditional must not aliasing: Under the assumption that two objects are not aliased, prove that two other objects are not aliased. This paper introduces and gives an algorithm for conditional must not alias analysis and discusses experimental results for sound race detection of Java programs.

REFERENCES

• 1: Sarita V. Adve , Mark D. Hill , Barton P. Miller , Robert H. B. Netzer, Detecting data races on weak memory systems, Proceedings of the 18th annual international symposium on Computer architecture, p.234-243, May 27-30, 1991, Toronto, Ontario, Canada
• 2: Rahul Agarwal , Amit Sasturkar , Liqiang Wang , Scott D. Stoller, Optimized run-time race detection and atomicity checking using partial discovered types, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1101944]
• 3: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 4: Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
• 5: Jong-Deok Choi , Keunwoo Lee , Alexey Loginov , Robert O'Callahan , Vivek Sarkar , Manu Sridharan, Efficient and precise datarace detection for multithreaded object-oriented programs, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 6: J. Choi, A. Loginov, and V. Sarkar. Static datarace analysis for multithreaded object-oriented programs. Technical Report RC22146, IBM Research, 2001.
• 7: Jong-Deok Choi , Barton P. Miller , Robert H. B. Netzer, Techniques for debugging parallel programs with flowback analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.491-530, Oct. 1991 [doi>10.1145/115372.115324]
• 8: M. Christiaens and K. Brosschere. TRaDe: A topological approach to on-the-fly race detection in Java programs. In Proceedings of JVM'01, pages 105--116, 2001.
• 9: Patrick Causot , Radhia Cousot, Static determination of dynamic properties of generalized type unions, Proceedings of an ACM conference on Language design for reliable software, p.77-94, March 28-30, 1977, Raleigh, North Carolina
• 10: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 11: A. Dinning , E. Schonberg, An empirical comparison of monitoring algorithms for access anomaly detection, Proceedings of the second ACM SIGPLAN symposium on Principles & practice of parallel programming, p.1-10, March 14-16, 1990, Seattle, Washington, United States
• 12: Anne Dinning , Edith Schonberg, Detecting access anomalies in programs with critical sections, Proceedings of the 1991 ACM/ONR workshop on Parallel and distributed debugging, p.85-96, May 20-21, 1991, Santa Cruz, California, United States
• 13: Dawson Engler , Ken Ashcraft, RacerX: effective, static detection of race conditions and deadlocks, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 14: C. Flanagan. Verifying commit-atomicity using model-checking. In Proceedings of SPIN'04, pages 252--266, 2004.
• 15: Cormac Flanagan , Martín Abadi, Types for Safe Locking, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.91-108, March 22-28, 1999
• 16: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 17: Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.256-267, January 14-16, 2004, Venice, Italy
• 18: Cormac Flanagan , Stephen N. Freund , Marina Lifshin, Type inference for atomicity, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.47-58, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040299]
• 19: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 20: Cormac Flanagan , Shaz Qadeer, Types for atomicity, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 21: Sanjay Ghemawat , Keith H. Randall , Daniel J. Scales, Field analysis: getting useful and low-cost interprocedural information, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.334-344, June 18-21, 2000, Vancouver, British Columbia, Canada
• 22: Dan Grossman, Type-safe multithreading in cyclone, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 23: Jerry J. Harrow, Runtime Checking of Multithreaded Applications with Visual Threads, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.331-342, August 30-September 01, 2000
• 24: David L. Heine , Monica S. Lam, A practical flow-sensitive and context-sensitive C and C++ memory leak detector, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 25: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Race checking by context inference, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 26: 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]
• 27: T. Lev-Ami, N. Immerman, T. Reps, S. Sagiv, S. Srivastava, and G. Yorsh. Simulating reachability using first-order logic with applications to verification of linked data structures. In Proceedings of CADE'05, pages 99--115, 2005.
• 28: O. Lhoták and L. Hendren. Context-sensitive points-to analysis: is it worth it? In Proceedings of CC'06, 2006.
• 29: Richard J. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM, v.18 n.12, p.717-721, Dec. 1975 [doi>10.1145/361227.361234]
• 30: S. McPeak and G. Necula. Data structure specifications via local equality axioms. In Proceedings of CAV'05, pages 476--490, 2005.
• 31: John Mellor-Crummey, On-the-fly detection of data races for programs with nested fork-join parallelism, Proceedings of the 1991 ACM/IEEE conference on Supercomputing, p.24-33, November 18-22, 1991, Albuquerque, New Mexico, United States [doi>10.1145/125826.125861]
• 32: Ana Milanova , Atanas Rountev , Barbara G. Ryder, Parameterized object sensitivity for points-to and side-effect analyses for Java, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 33: Mayur Naik , Alex Aiken , John Whaley, Effective static race detection for Java, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 34: 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
• 35: 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
• 36: Polyvios Pratikakis , Jeffrey S. Foster , Michael Hicks, LOCKSMITH: context-sensitive correlation analysis for race detection, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 37: Shaz Qadeer , Dinghao Wu, KISS: keep it simple and sequential, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 38: 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]
• 39: Amit Sasturkar , Rahul Agarwal , Liqiang Wang , Scott D. Stoller, Automated type-based analysis of data races and atomicity, 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.1065956]
• 40: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multi-threaded programs, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.27-37, October 05-08, 1997, Saint Malo, France
• 41: D. Schonberg, On-the-fly detection of access anomalies, Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, p.285-297, June 19-23, 1989, Portland, Oregon, United States
• 42: N. Sterling. WARLOCK - a static data race analysis tool. In Proceedings of the Usenix Winter 1993 Technical Conference, pages 97--106, 1993.
• 43: Christoph von Praun , Thomas R. Gross, Object race detection, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.70-82, October 14-18, 2001, Tampa Bay, FL, USA
• 44: Christoph von Praun , Thomas R. Gross, Static conflict analysis for multi-threaded object-oriented programs, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 45: Liqiang Wang , Scott D. Stoller, Static analysis of atomicity for programs with non-blocking synchronization, 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.1065953]
• 46: Liqiang Wang , Scott D. Stoller, Runtime Analysis of Atomicity for Multithreaded Programs, IEEE Transactions on Software Engineering, v.32 n.2, p.93-110, February 2006 [doi>10.1109/TSE.2006.1599419]
• 47: Yuan Yu , Tom Rodeheffer , Wei Chen, RaceTrack: efficient detection of data race conditions via adaptive tracking, Proceedings of the twentieth ACM symposium on Operating systems principles, October 23-26, 2005, Brighton, United Kingdom

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability

General Terms:
Experimentation, Reliability, Verification

Keywords:
Java, concurrency, multi-threading, static race detection, synchronization