This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Runtime Analysis of Atomicity for Multithreaded Programs
February 2006 (vol. 32 no. 2)
pp. 93-110
Atomicity is a correctness condition for concurrent systems. Informally, atomicity is the property that every concurrent execution of a set of transactions is equivalent to some serial execution of the same transactions. In multithreaded programs, executions of procedures (or methods) can be regarded as transactions. Correctness in the presence of concurrency typically requires atomicity of these transactions. Tools that automatically detect atomicity violations can uncover subtle errors that are hard to find with traditional debugging and testing techniques. This paper describes two algorithms for runtime detection of atomicity violations and compares their cost and effectiveness. The reduction-based algorithm checks atomicity based on commutativity properties of events in a trace; the block-based algorithm efficiently represents the relevant information about a trace as a set of blocks (i.e., pairs of events plus associated synchronizations) and checks atomicity by comparing each block with other blocks. To improve the efficiency and accuracy of both algorithms, we incorporate a multilockset algorithm for checking data races, dynamic escape analysis, and happen-before analysis. Experiments show that both algorithms are effective in finding atomicity violations. The block-based algorithm is more accurate but more expensive than the reduction-based algorithm.

[1] R. Agarwal, L. Wang, and S.D. Stoller, “Detecting Potential Deadlocks with Static Analysis and Runtime Monitoring,” Proc. Parallel and Distributed Systems: Testing and Debugging (PADTAD) Track of the 2005 IBM Verification Conf., Nov. 2005.
[2] C. Artho, K. Havelund, and A. Biere, “High-Level Data Races,” Proc. First Int'l Workshop Verification and Validation of Enterprise Information Systems (VVEIS), Apr. 2003.
[3] P.A. Bernstein, V. Hadzilacos, and N. Goodman, Concurrency Control and Recovery in Database Systems. Addison Wesley, 1987.
[4] C. Boyapati, R. Lee, and M. Rinard, “Ownership Types for Safe Programming: Preventing Data Races and Deadlocks,” Proc. 17th ACM Conf. Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pp. 211-230, Nov. 2002.
[5] C. Boyapati and M.C. Rinard, “A Parameterized Type System for Race-Free Java Programs,” Proc. 16th ACM Conf. Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), Nov. 2001.
[6] J.-D. Choi, K. Lee, A. Loginov, R. O'Callahan, V. Sarkar, and M. Sridharan, “Efficient and Precise Datarace Detection for Multithreaded Object-Oriented Programs,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), pp. 258-269, 2002.
[7] M.B. Dwyer, J. Hatcliff Robby, and V.P. Ranganath, “Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs,” Formal Methods in System Design, vol. 25, nos. 2-3, pp. 199-240, 2004.
[8] C. Flanagan, “Verifying Commit-Atomicity Using Model-Checking,” Proc. 11th Int'l SPIN Workshop Model Checking of Software, 2004.
[9] C. Flanagan and S. Freund, “Type-Based Race Detection for Java,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), pp. 219-232, 2000.
[10] C. Flanagan and S.N. Freund, “Atomizer: A Dynamic Atomicity Checker for Multithreaded Programs,” Proc. ACM Symp. Principles of Programming Languages (POPL), pp. 256-267, 2004.
[11] C. Flanagan and S.N. Freund, “Type Inference against Races,” Static Analysis Symp. (SAS), Aug. 2004.
[12] C. Flanagan, S.N. Freund, and M. Lifshin, “Type Inference for Atomicity,” Proc. ACM SIGPLAN Int'l Workshop Types in Languages Design and Implementation (TLDI), Jan. 2005.
[13] C. Flanagan, S.N. Freund, and S. Qadeer, “Exploiting Purity for Atomicity,” Proc. ACM Int'l Symp. Software Testing and Analysis (ISSTA), pp. 221-231, 2004.
[14] C. Flanagan and S. Qadeer, “A Type and Effect System for Atomicity,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2003.
[15] C. Flanagan and S. Qadeer, “Types for Atomicity,” Proc. ACM SIGPLAN Int'l Workshop Types in Languages Design and Implementation (TLDI), pp. 1-12, 2003.
[16] J. Hatcliff Robby and M.B. Dwyer, “Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking,” Proc. Fifth Int'l Conf. Verification, Model Checking and Abstract Interpretation (VMCAI), Jan. 2004.
[17] K. Havelund, “Using Runtime Analysis to Guide Model Checking of Java Programs,” Proc. Seventh Int'l SPIN Workshop Model Checking of Software, Aug. 2000.
[18] M.P. Herlihy and J.M. Wing, “Linearizability: A Correctness Condition for Concurrent Objects,” ACM Trans. Programming Languages and Systems, vol. 12, no. 3, pp. 463-492, July 1990.
[19] Java Grande forum, Java Grande Multithreaded Benchmark Suite, version 1.0, http:/www.javagrande.org/, 2001.
[20] Jigsaw, version 2.2.4, http:/www.w3c.org, 2004.
[21] Decision Management Systems GmbH, Kopi compiler, http://www.dms.atkopi/, 2002.
[22] R.J. Lipton, “Reduction: A Method of Proving Properties of Parallel Programs,” Comm. ACM, vol. 18, no. 12, pp. 717-721, 1975.
[23] F. Mattern, “Virtual Time and Global States of Distributed Systems,” Proc. Int'l Workshop Parallel and Distributed Algorithms, pp. 120-131, 1989.
[24] R. O'Callahan and J.-D. Choi, “Hybrid Dynamic Data Race Detection,” Proc. ACM SIGPLAN 2003 Symp. Principles and Practice of Parallel Programming (PPoPP), pp. 167-178, 2003.
[25] C.H. Papadimitriou, “The Serializability of Concurrent Database Updates,” J. ACM, vol. 26, no. 4, pp. 631-653, Oct. 1979.
[26] W. Pugh, “Fixing the Java Memory Model,” Proc. ACM Conf. Java Grande, pp. 89-98, 1999.
[27] E. Ruf, “Effective Synchronization Removal for Java,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), pp. 208-218, June 2000.
[28] S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T.E. Anderson, “Eraser: A Dynamic Data Race Detector for Multithreaded Programs,” ACM Trans. Computer Systems, vol. 15, no. 4, pp. 391-411, Nov. 1997.
[29] C. von Praun and T.R. Gross, “Object Race Detection,” Proc. 16th ACM Conf. Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), Oct. 2001.
[30] C. von Praun and T.R. Gross, “Static Detection of Atomicity Violations in Object-Oriented Programs,” J. Object Technology, vol. 3, no. 6, June 2004.
[31] L. Wang and S.D. Stoller, “Run-Time Analysis for Atomicity,” Proc. Third Workshop Runtime Verification (RV '03), 2003.
[32] L. Wang and S.D. Stoller, “Static Analysis for Programs with Non-Blocking Synchronization,” Proc. ACM SIGPLAN 2005 Symp. Principles and Practice of Parallel Programming (PPoPP), June 2005.

Index Terms:
Concurrent programming, testing and debugging, Java, data race, atomicity.
Citation:
Liqiang Wang, Scott D. Stoller, "Runtime Analysis of Atomicity for Multithreaded Programs," IEEE Transactions on Software Engineering, vol. 32, no. 2, pp. 93-110, Feb. 2006, doi:10.1109/TSE.2006.18
Usage of this product signifies your acceptance of the Terms of Use.