The Community for Technology Leaders
RSS Icon
Issue No.04 - July/August (2010 vol.36)
pp: 509-527
Eric Bodden , Technical University Darmstadt, Darmstadt
Klaus Havelund , California Institute of Technology, Pasadena
In the past, researchers have developed specialized programs to aid programmers in detecting concurrent programming errors such as deadlocks, livelocks, starvation, and data races. In this work, we propose a language extension to the aspect-oriented programming language AspectJ, in the form of three new pointcuts, lock(), unlock(), and maybeShared(). These pointcuts allow programmers to monitor program events where locks are granted or handed back, and where values are accessed that may be shared among multiple Java threads. We decide thread locality using a static thread-local-objects analysis developed by others. Using the three new primitive pointcuts, researchers can directly implement efficient monitoring algorithms to detect concurrent-programming errors online. As an example, we describe a new algorithm which we call Racer, an adaption of the well-known Eraser algorithm to the memory model of Java. We implemented the new pointcuts as an extension to the AspectBench Compiler, implemented the Racer algorithm using this language extension, and then applied the algorithm to the NASA K9 Rover Executive and two smaller programs. Our experiments demonstrate that our implementation is effective in finding subtle data races. In the Rover Executive, Racer finds 12 data races, with no false warnings. Only one of these races was previously known.
Race detection, runtime verification, aspect-oriented programming, semantic pointcuts, static analysis.
Eric Bodden, Klaus Havelund, "Aspect-Oriented Race Detection in Java", IEEE Transactions on Software Engineering, vol.36, no. 4, pp. 509-527, July/August 2010, doi:10.1109/TSE.2010.25
[1] J. Harrow, "Runtime Checking of Multithreaded Applications with Visual Threads," SPIN Model Checking and Software Verification, K. Havelund, J. Penix, and W. Visser, eds., pp. 331-342, Springer, 2000.
[2] R. O'Callahan and J.-D. Choi, "Hybrid Dynamic Data Race Detection," Proc. ACM SIGPLAN Symp. Principles and Practice of Parallel Programming, pp. 167-178, 2003.
[3] C. von Praun and T.R. Gross, "Object Race Detection," Proc. Ann. ACM SIGPLAN Conf. Object-Oriented Programming, Systems, Languages, and Applications, pp. 70-82, 2001.
[4] K. Havelund, "Using Runtime Analysis to Guide Model Checking of Java Programs," SPIN Model Checking and Software Verification, pp. 245-264, Springer, 2000.
[5] K. Havelund and G. Roşu, "An Overview of the Runtime Verification Tool Java PathExplorer," Formal Methods in System Design, vol. 24, no. 2, pp. 189-215, 2004.
[6] C. Artho, K. Havelund, and A. Biere, "High-Level Data Races," Software Testing, Verification and Reliability, vol. 13, no. 4, pp. 207-227, 2003.
[7] C. Artho, K. Havelund, and A. Biere, "Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors," Automated Technology for Verification and Analysis, F. Wang, ed., pp. 150-164, Springer, 2004.
[8] C. Flanagan and S.N. Freund, "Atomizer: A Dynamic Atomicity Checker for Multithreaded Programs," Proc. 31st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp. 256-267, 2004.
[9] L. Wang and S.D. Stoller, "Run-Time Analysis for Atomicity," Electronic Notes in Theoretical Computer Science, vol. 89, no. 2, 2003.
[10] F. Chen, T.F. Serbanuta, and G. Roşu, "jPredictor: A Predictive Runtime Analysis Tool for Java," Proc. 30th Int'l Conf. Software Eng., pp. 221-230, 2008.
[11] M. Dahm, "BCEL," http://jakarta.apache.orgbcel, 2010.
[12] E. Bodden, "J-LO—A Tool for Runtime-Checking Temporal Assertions," master's thesis, RWTH Aachen Univ., http://www.bodden.depublications/, Nov. 2005.
[13] M. d'Amorim and K. Havelund, "Event-Based Runtime Verification of Java Programs," Proc. Third Int'l Workshop Dynamic Analysis, pp. 1-7, 2005.
[14] V. Stolz and E. Bodden, "Temporal Assertions Using AspectJ," Electronic Notes in Theoretical Computer Science, vol. 144, no. 4, pp. 109-124, 2006.
[15] F. Chen and G. Roşu, "MOP: An Efficient and Generic Runtime Verification Framework," Proc. Ann. ACM SIGPLAN Conf. Object-Oriented Programming, Systems, Languages, and Applications, R.P. Gabriel, D.F. Bacon, C.V. Lopes, J. Guy, and L. Steele, eds., pp. 569-588, 2007.
[16] C. Allan, P. Avgustinov, A.S. Christensen, L.J. Hendren, S. Kuzins, O. Lhoták, O. de Moor, D. Sereni, G. Sittampalam, and J. Tibble, "Adding Trace Matching with Free Variables to AspectJ," Proc. Ann. ACM SIGPLAN Conf. Object-Oriented Programming, Systems, Languages, and Applications, R. Johnson and R.P. Gabriel, eds., pp. 345-364, 2005.
[17] R.L. Halpert, C.J.F. Pickett, and C. Verbrugge, "Component-Based Lock Allocation," Proc. 16th Int'l Conf. Parallel Architectures and Compilation Techniques, pp. 353-364, 2007.
[18] P. Avgustinov, A.S. Christensen, L. Hendren, S. Kuzins, J. Lhoták, O. Lhoták, O. de Moor, D. Sereni, G. Sittampalam, and J. Tibble, "abc: An Extensible AspectJ Compiler," Proc. Int'l Conf. Aspect-Oriented Software Development, pp. 87-98, 2005.
[19] S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson, "Eraser: A Dynamic Data Race Detector for Multithreaded Programs," ACM Trans. Computer Systems, vol. 15, no. 4, pp. 391-411, 1997.
[20] E. Bodden and K. Havelund, "Racer: Effective Race Detection Using AspectJ," Proc. Int'l Symp. Software Testing and Analysis, pp. 155-165, July 2008.
[21] S. Bensalem and K. Havelund, "Dynamic Deadlock Analysis of Multi-Threaded Programs," Proc. Haifa Verification Conf., S. Ur, E. Bin, and Y. Wolfsthal, eds., pp. 208-223, 2005.
[22] "The AspectJ Home Page," http://eclipse.orgaspectj/, 2010.
[23] "The AspectJ Programming Guide," http://www.eclipse.orgaspectj, 2010.
[24] J. Gosling, B. Joy, G. Steele, and G. Bracha, The Java(TM) Language Specification, third ed. Addison-Wesley Professional, 2005.
[25] O. Lhoták and L. Hendren, "Scaling Java Points-to Analysis Using Spark," Proc. 12th Int'l Conf. Compiler Construction, G. Hedin, ed., pp. 153-169, Apr. 2003.
[26] J. Manson, W. Pugh, and S.V. Adve, "The Java Memory Model," Proc. 32nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp. 378-391, 2005.
[27] E. Bodden, F. Forster, and F. Steimann, "Avoiding Infinite Recursion with Stratified Aspects," Proc. Int'l Conf. Grid Service Eng. and Management, R. Hirschfeld, A. Polze, and R. Kowalczyk, eds., pp. 49-64, 2006.
[28] B. Goetz, Java Concurrency in Practice. Addison Wesley, 2006.
[29] T. Aotani and H. Masuhara, "SCoPE: An AspectJ Compiler for Supporting User-Defined Analysis-Based Pointcuts," Proc. Int'l Conf. Aspect-Oriented Software Development, pp. 161-172, 2007.
[30] G.P. Brat, D. Drusinsky, D. Giannakopoulou, A. Goldberg, K. Havelund, M.R. Lowry, C.S. Pasareanu, A. Venet, W. Visser, and R. Washington, "Experimental Evaluation of Verification and Validation Tools on Martian Rover Software," Formal Methods in System Design, vol. 25, nos. 2/3, pp. 167-198, 2004.
[31] W. Visser, K. Havelund, G.P. Brat, S. Park, and F. Lerda, "Model Checking Programs," Proc. 15th IEEE Int'l Conf. Automated Software Eng., pp. 203-232, 2003.
[32] D. Lea, Concurrent Programming in Java: Design Principles and Patterns. Addison-Wesley Longman Publishing Co., Inc., 1996.
[33] J. Gray, "Why Do Computers Stop and What Can Be Done about It?" Proc. Fifth Symp. Reliability in Distributed Software and Database Systems, pp. 3-12, 1986.
[34] A. Eustace and A. Srivastava, "ATOM: A Flexible Interface for Building High Performance Program Analysis Tools," Proc. USENIX Winter '95 Technical Conf., p. 25, 1995.
[35] L. Lamport, "Time, Clocks, and the Ordering of Events in a Distributed System," Comm. ACM, vol. 21, no. 7, pp. 558-565, 1978.
[36] T. Elmas, S. Qadeer, and S. Tasiran, "Goldilocks: A Race and Transaction-Aware Java Runtime," Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 245-255, 2007.
[37] S. Cohen, "Jtrek," Compaq, no longer maintained.
[38] "Soot Website," http://www.sable.mcgill.casoot/, 2010.
[39] R. Agarwal, L. Wang, and S.D. Stoller, "Detecting Potential Deadlocks with Static Analysis and Run-Time Monitoring," Proc. Haifa Verification Conf., S. Ur, E. Bin, and Y. Wolfsthal, eds., pp. 191-207, 2005.
[40] S. Bensalem, J.-C. Fernandez, K. Havelund, and L. Mounier, "Confirmation of Deadlock Potentials Detected by Runtime Analysis," Proc. 2006 Workshop Parallel and Distributed Systems: Testing and Debugging, pp. 41-50, 2006.
[41] Y. Eytani, K. Havelund, S.D. Stoller, and S. Ur, "Towards a Framework and a Benchmark for Testing Tools for Multi-Threaded Programs: Research Articles," Concurrency and Computation: Practice and Experience, vol. 19, no. 3, pp. 267-279, 2007.
[42] H. Barringer, A. Goldberg, K. Havelund, and K. Sen, "Rule-Based Runtime Verification," Proc. Int'l Conf. Verification, Model Checking, and Abstract Interpretation, B. Steffen and G. Levi, eds., pp. 44-57, 2004.
[43] E. Bodden, L.J. Hendren, and O. Lhoták, "A Staged Static Program Analysis to Improve the Performance of Runtime Monitoring," Proc. European Conf. Object-Oriented Programming, E. Ernst, ed., pp. 525-549, 2007.
[44] E. Bodden, P. Lam, and L. Hendren, "Static Analysis Techniques for Evaluating Runtime Monitoring Properties Ahead-of-Time," Technical Report abc-2007-6, http:/, 2007.
[45] E. Bruneton, R. Lenglet, and T. Coupaye, "ASM: A Code Manipulation Tool to Implement Adaptable Systems," Adaptable and Extensible Component Systems, http:/, Nov. 2002.
[46] "Valgrind," http:/, 2010.
[47] G.C. Necula, S. McPeak, S.P. Rahul, and W. Weimer, "CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs," Proc. Int'l Conf. Compiler Construction, R.N. Horspool, ed., pp. 213-228, 2002.
[48] A. Goldberg and K. Havelund, "Instrumentation of Java Bytecode for Runtime Analysis," Proc. Fifth ECOOP Workshop Formal Techniques for Java-Like Programs, July 2003.
[49] A. Kinneer, M.B. Dwyer, and G. Rothermel, "Sofya: Supporting Rapid Development of Dynamic Program Analyses for Java," Companion to the Proc. 29th Int'l Conf. Software Eng., pp. 51-52, 2007.
[50] M. Eichberg, M. Mezini, and K. Ostermann, "Pointcuts as Functional Queries," Proc. Second ASIAN Symp. Programming Languages and Systems, W.-N. Chin, ed., pp. 366-381, 2004.
[51] T. Aotani and H. Masuhara, "Compiling Conditional Pointcuts for User-Level Semantic Pointcuts," Proc. Software-Eng. Properties of Languages and Aspect Technologies Workshop, Mar. 2005.
[52] Hardware and Software Verification and Testing, S. Ur, E. Bin, and Y. Wolfsthal, eds. Springer, 2006.
18 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool