Dataflow analysis for concurrent programs using datarace detection

ABSTRACT

Dataflow analyses for concurrent programs differ from their single-threaded counterparts in that they must account for shared memory locations being overwritten by concurrent threads. Existing dataflow analysis techniques for concurrent programs typically fall at either end of a spectrum: at one end, the analysis conservatively kills facts about all data that might possibly be shared by multiple threads; at the other end, a precise thread-interleaving analysis determines which data may be shared, and thus which dataflow facts must be invalidated. The former approach can suffer from imprecision, whereas the latter does not scale.

We present RADAR, a framework that automatically converts a dataflow analysis for sequential programs into one that is correct for concurrent programs. RADAR uses a race detection engine to kill the dataflow facts, generated and propagated by the sequential analysis, that become invalid due to concurrent writes. Our approach of factoring all reasoning about concurrency into a race detection engine yields two benefits. First, to obtain analyses for code using new concurrency constructs, one need only design a suitable race detection engine for the constructs. Second, it gives analysis designers an easy way to tune the scalability and precision of the overall analysis by only modifying the race detection engine. We describe the RADAR framework and its implementation using a pre-existing race detection engine. We show how RADAR was used to generate a concurrent version of a null-pointer dereference analysis, and we analyze the result of running the generated concurrent analysis on several benchmarks.

REFERENCES

• 1: 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
• 2: J. M. Cobleigh, L. A. Clarke, and L. J. Osterweil. FLAVERS: A finite state verification technique for software systems. IBM Systems Journal, 41(1):140--165, 2002.
• 3: Nathan Cooprider , John Regehr, Pluggable abstract domains for analyzing embedded software, Proceedings of the 2006 ACM SIGPLAN/SIGBED conference on Language, compilers, and tool support for embedded systems, June 14-16, 2006, Ottawa, Ontario, Canada
• 4: Isil Dillig , Thomas Dillig , Alex Aiken, Static error detection using semantic inconsistency inference, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 5: 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
• 6: 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
• 7: C. Flanagan and S. Qadeer. Thread-modular model checking. In SPIN, LNCS 2648, pages 213--224. Springer, 2003.
• 8: David Gay , Philip Levis , Robert von Behren , Matt Welsh , Eric Brewer , David Culler, The nesC language: A holistic approach to networked embedded systems, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 9: Dirk Grunwald , Harini Srinivasan, Data flow equations for explicitly parallel programs, Proceedings of the fourth ACM SIGPLAN symposium on Principles and practice of parallel programming, p.159-168, May 19-22, 1993, San Diego, California, United States
• 10: Brian Hackett , Manuvir Das , Daniel Wang , Zhe Yang, Modular checking for buffer overflows in the large, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134319]
• 11: 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
• 12: C. B. Jones, Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.4, p.596-619, Oct. 1983 [doi>10.1145/69575.69577]
• 13: Jens Knoop , Bernhard Steffen , Jürgen Vollmer, Parallelism for free: efficient and optimal bitvector analyses for parallel programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.3, p.268-299, May 1996 [doi>10.1145/229542.229545]
• 14: L. Lamport, Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, v.3 n.2, p.125-143, March 1977 [doi>10.1109/TSE.1977.229904]
• 15: Jaejin Lee , David A. Padua , Samuel P. Midkiff, Basic compiler algorithms for parallel programs, Proceedings of the seventh ACM SIGPLAN symposium on Principles and practice of parallel programming, p.1-12, May 04-06, 1999, Atlanta, Georgia, United States
• 16: Richard J. Lipton, Reduction: a new method of proving properties of systems of processes, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.78-86, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512985]
• 17: 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
• 18: Gleb Naumovich , George S. Avrunin , Lori A. Clarke, An efficient algorithm for computing MHP information for concurrent Java programs, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.338-354, Nov. 1999
• 19: S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):319--340, 1976.
• 20: 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
• 21: G. Ramalingam, Context-sensitive synchronization-sensitive analysis is undecidable, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.416-430, March 2000 [doi>10.1145/349214.349241]
• 22: Radu Rugina , Martin Rinard, Pointer analysis for multithreaded programs, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.77-90, May 01-04, 1999, Atlanta, Georgia, United States
• 23: Alexandru Salcianu , Martin Rinard, Pointer and escape analysis for multithreaded programs, Proceedings of the eighth ACM SIGPLAN symposium on Principles and practices of parallel programming, p.12-23, June 2001, Snowbird, Utah, United States
• 24: Vivek Sarkar, Analysis and Optimization of Explicitly Parallel Programs Using the Parallel Program Graph Representation, Proceedings of the 10th International Workshop on Languages and Compilers for Parallel Computing, p.94-113, August 07-09, 1997
• 25: David A. Schmidt, Data flow analysis is model checking of abstract interpretations, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.38-48, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268950]
• 26: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 27: Arnaud Venet , Guillaume Brat, Precise and efficient static array bound checking for large embedded C programs, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 28: 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
• 29: Jan Wen Voung , Ranjit Jhala , Sorin Lerner, RELAY: static race detection on millions of lines of code, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia [doi>10.1145/1287624.1287654]

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Languages, Reliability, Verification

Keywords:
interprocedural analysis, locksets, multithreaded programs, summaries