Static data race detection for concurrent programs with asynchronous calls

ABSTRACT

A large number of industrial concurrent programs are being designed based on a model which combines threads with event-based communication. These programs consist of several threads which perform computation by dispatching tasks to other threads via asynchronous function calls. These asynchronous function calls are implemented using function objects, which are essentially wrappers containing a pointer to the function that should be executed on a particular thread with the corresponding arguments. In many cases, the arguments, in turn, contain function objects which serve as callbacks. Verifying such programs which involves reasoning about complex concurrency constructs comprising function pointers and callback functions is extremely tricky especially in the presence of recursion. In this paper, we present a fast and accurate static data race detection technique for multi-threaded C programs with asynchronous function calls and demonstrate its application to real-life software.

REFERENCES

• 1: R. Barik. Effficient computation of may-happen-in-parallel information for concurrent java programs. In LCPC, pages 152--169, 2005.
• 2: M. Burrows and K. Leino. Finding stale-value errors in concurrent programs. In Compaq Systems Research Center SRC-TR-2002-004, 2002.
• 3: P. Chandrasekaran, C. L. Conway, J. M. Joy, and S. K. Rajamani. Programming asynchronous layers with clarity. In FSE, 2007.
• 4: D. Detlefs, K. Leino, G. Nelson, and J. Saxe. Extended static checking. In TR SRC-159 Compaq SRC, 1998.
• 5: A. Dinning and E. Schonberg. An empirical comparision of monitoring algorithms for access anomaly detection. In PPoPP, 1990.
• 6: M. Emami, R. Ghiya, and L. J. Hendren. Context-sensitive interprocedural points-to analysis in the presence of function pointers. pages 242--256, 1994.
• 7: D. Engler and K. Ashcraft. RacerX: Effective, Static Detection of Race Conditions and Deadlocks. In SOSP, 2003.
• 8: P. Ganty, R. Majumdar, and A. Rybalchenko. Verifying liveness for asynchronous programs. In POPL, pages 102--113, 2009.
• 9: C. J, K. Lee, A. Loginov, R.O'Callahan, V. Sarkar, and M. Sridharan. Effficient and precise datarace detection for multithreaded object-oriented programs. In PLDI, 2002.
• 10: R. Jhala and R. Majumdar. Interprocedural analysis of asynchronous programs. In POPL, 2007.
• 11: V. Kahlon. Bootstrapping: A technique for scalable flow and context-sensitive pointer alias analysis. In PLDI, 2008.
• 12: V. Kahlon, S. Sankaranarayanan, and A. Gupta. Semantic reduction of thread interleavings for concurrent programs. In TACAS, 2009.
• 13: V. Kahlon, Y. Yang, S. Sankaranarayanan, and A. Gupta. Fast and accurate static data-race detection for concurrent programs. In CAV, 2007.
• 14: R. Leino, G. Neslon, and J. Saxe. Esc/java users' manual. In Technical Note 2000-002, Compaq Systems Research Center, 2001.
• 15: P. Li and S. Zdancewic. Combining events and threads for scalable network services implementation and evaluation of monadic, application-level concurrency primitives. In PLDI, 2007.
• 16: J. Mellor-Crummey. One-the-fly detection of data races for programs with nested fork-join parallelism. In Proceedings of the 1991 Supercomputer Debugging Workshop, 1991.
• 17: M. Naik and A. Aiken. Conditional must not aliasing for static race detection. In POPL, 2007.
• 18: M. Naik, A. Aiken, and J. Whaley. Effective static race detection for java. In PLDI, 2006.
• 19: C. Pheatt. Intel Rthreading building blocks. J. Comput. Small Coll., 23(4):298--298, 2008.
• 20: P. Pratikakis, J. S. Foster, and M. Hicks. LOCKSMITH: Context-Sensitive Correlation Analysis for Race Detection. In PLDI, 2006.
• 21: M. C. Rinard. Analysis of multithreaded programs. In SAS, 2001.
• 22: S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A dynamic data race detector for multithreaded programming. In ACM TCS, volume 15(4), 1997.
• 23: J. G. Siek, L.-Q. Lee, and A. Lumsdaine. The Boost Graph Library User Guide and Reference Manual (With CD-ROM). Addison-Wesley Professional, December 2001.
• 24: B. Steensgaard. Points-to analysis in almost linear time. In POPL, 1996.
• 25: N. Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, 1993.
• 26: C. von Praun and T. R. Gross. Static conflict analysis for multi-threaded object-oriented programs. SIGPLAN Not., 38(5):115--128, 2003.
• 27: M. Welsh, D. Culler, and E. Brewer. Seda: an architecture for well-conditioned, scalable internet services. SIGOPS Oper. Syst. Rev., 35(5):230--243, 2001.

INDEX TERMS

Primary Classification:
  D. Software
  D.0 GENERAL

General Terms:
Algorithms, Verification

Keywords:
asynchronous programs, bootstrapping, pointer analysis, static data race detection