Racer: effective race detection using aspectj

ABSTRACT

Programming errors occur frequently in large software systems, and even more so if these systems are concurrent. In the past researchers have developed specialized programs to aid programmers 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 amongst 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 expose a new algorithm which we call Racer, an adoption 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. Our experiments proved our implementation very effective. In the Rover Executive Racer finds 70 data races. Only one of these races was previously known. We further applied the algorithm to two other multi-threaded programs written by Computer Science researchers, in which we found races as well.

REFERENCES

• 1: R. Agarwal, L. Wang, and S. D. Stoller. Detecting potential deadlocks with static analysis and run-time monitoring. In Ur et al. {39}, pages 191--207.
• 2: Chris Allan , Pavel Avgustinov , Aske Simon Christensen , Laurie Hendren , Sascha Kuzins , Ondřej Lhoták , Oege de Moor , Damien Sereni , Ganesh Sittampalam , Julian Tibble, Adding trace matching with free variables to AspectJ, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 3: T. Aotani and H. Masuhara. Compiling conditional pointcuts for user-level semantic pointcuts. In Software-Engineering Properties of Languages and Aspect Technologies (SPLAT), March 2005.
• 4: C. Artho, K. Havelund, and A. Biere. High-level data races. Software Testing, Verification and Reliability, 13(4):207--227, 2003.
• 5: C. Artho, K. Havelund, and A. Biere. Using block-local atomicity to detect stale-value concurrency errors. In F. Wang, editor, ATVA, volume 3299 of LNCS, pages 150--164. Springer, 2004.
• 6: Pavel Avgustinov , Aske Simon Christensen , Laurie Hendren , Sascha Kuzins , Jennifer Lhoták , Ondřej Lhoták , Oege de Moor , Damien Sereni , Ganesh Sittampalam , Julian Tibble, abc: an extensible AspectJ compiler, Proceedings of the 4th international conference on Aspect-oriented software development, p.87-98, March 14-18, 2005, Chicago, Illinois [doi>10.1145/1052898.1052906]
• 7: H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Rule-based runtime verification. In B. Steffen and G. Levi,editors, VMCAI, volume 2937 of Lecture Notes in Computer Science, pages 44--57. Springer, 2004.
• 8: Saddek Bensalem , Jean-Claude Fernandez , Klaus Havelund , Laurent Mounier, Confirmation of deadlock potentials detected by runtime analysis, Proceedings of the 2006 workshop on Parallel and distributed systems: testing and debugging, July 17-17, 2006, Portland, Maine, USA [doi>10.1145/1147403.1147412]
• 9: S. Bensalem and K. Havelund. Dynamic deadlock analysis of multi-threaded programs. In Ur et al. {39}, pages 208--223.
• 10: E. Bodden, F. Forster, and F. Steimann. Avoiding infinite recursion with stratified aspects. In R. Hirschfeld, A. Polze, and R. Kowalczyk, editors, GI-Edition Lecture Notes in Informatics "NODe 2006 GSEM 2006", volume P-88, pages 49--64. Gesellschaft für Informatik, Bonner Köllen Verlag, 2006.
• 11: E. Bodden and K. Havelund. Racer: Effective race detection using AspectJ (extended version). Technical Report abc-2008-1, http://www.aspectbench.org/, 05 2008.
• 12: E. Bodden, L. J. Hendren, and O. Lhoták. A staged static program analysis to improve the performance of runtime monitoring. In E. Ernst, editor, ECOOP, volume 4609 of Lecture Notes in Computer Science, pages 525--549. Springer, 2007.
• 13: E. Bodden, P. Lam, and L. Hendren. Static analysis techniques for evaluating runtime monitoring properties ahead-of-time. Technical Report abc-2007-6, http://www.aspectbench.org/, 11 2007.
• 14: Guillaume Brat , Doron Drusinsky , Dimitra Giannakopoulou , Allen Goldberg , Klaus Havelund , Mike Lowry , Corina Pasareanu , Arnaud Venet , Willem Visser , Rich Washington, Experimental Evaluation of Verification and Validation Tools on Martian Rover Software, Formal Methods in System Design, v.25 n.2-3, p.167-198, September-November 2004 [doi>10.1023/B:FORM.0000040027.28662.a4]
• 15: E. Bruneton, R. Lenglet, and T. Coupaye. ASM: A code manipulation tool to implement adaptable systems. In Adaptable and Extensible Component Systems, Grenoble, France, November 2002. http://asm.objectweb.org.
• 16: Feng Chen , Traian Florin Serbanuta , Grigore Rosu, jPredictor: a predictive runtime analysis tool for java, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany [doi>10.1145/1368088.1368119]
• 17: S. Cohen. Jtrek. Compaq. No longer maintained.
• 18: M. Dahm. BCEL. http://jakarta.apache.org/bcel.
• 19: Marcelo d'Amorim , Klaus Havelund, Event-based runtime verification of java programs, Proceedings of the third international workshop on Dynamic analysis, p.1-7, May 17-17, 2005, St. Louis, Missouri
• 20: M. Eichberg, M. Mezini, and K. Ostermann. Pointcuts as functional queries. In W.-N. Chin, editor, APLAS, volume 3302 of Lecture Notes in Computer Science, pages 366--381. Springer, 2004.
• 21: Alan Eustace , Amitabh Srivastava, ATOM: a flexible interface for building high performance program analysis tools, Proceedings of the USENIX 1995 Technical Conference Proceedings on USENIX 1995 Technical Conference Proceedings, p.25-25, January 16-20, 1995, New Orleans, Louisiana
• 22: Yaniv Eytani , Klaus Havelund , Scott D. Stoller , Shmuel Ur, Towards a framework and a benchmark for testing tools for multi-threaded programs: Research Articles, Concurrency and Computation: Practice & Experience, v.19 n.3, p.267-279, March 2007 [doi>10.1002/cpe.v19:3]
• 23: Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, ACM SIGPLAN Notices, v.39 n.1, p.256-267, January 2004
• 24: B. Goetz. Java concurrency in practice. Addison Wesley, 2006.
• 25: A. Goldberg and K. Havelund. Instrumentation of Java bytecode for runtime analysis. In Fifth ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP'03), July 2003. Darmstadt, Germany.
• 26: A. Goldberg and K. Havelund. Instrumentation of Java bytecode for runtime analysis. In Fifth ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP'03), July 2003. Darmstadt, Germany.
• 27: Richard L. Halpert , Christopher J. F. Pickett , Clark Verbrugge, Component-Based Lock Allocation, Proceedings of the 16th International Conference on Parallel Architecture and Compilation Techniques, p.353-364, September 15-19, 2007 [doi>10.1109/PACT.2007.23]
• 28: 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
• 29: Klaus Havelund, Using Runtime Analysis to Guide Model Checking of Java Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.245-264, August 30-September 01, 2000
• 30: Klaus Havelund, Using Runtime Analysis to Guide Model Checking of Java Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.245-264, August 30-September 01, 2000
• 31: Alex Kinneer , Matthew B. Dwyer , Gregg Rothermel, Sofya: Supporting Rapid Development of Dynamic Program Analyses for Java, Companion to the proceedings of the 29th International Conference on Software Engineering, p.51-52, May 20-26, 2007 [doi>10.1109/ICSECOMPANION.2007.68]
• 32: Doug Lea, Concurrent Programming in Java: Design Principles and Patterns, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 33: O. Lhot´ak and L. Hendren. Scaling Java points-to analysis using Spark. In G. Hedin, editor, Compiler Construction, 12th International Conference, volume 2622 of LNCS, pages 153--169, Warsaw, Poland, April 2003. Springer.
• 34: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 35: 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
• 36: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 37: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 38: V. Stolz and E. Bodden. Temporal assertions using AspectJ. Electr. Notes in Theor. Computer Science, 144(4):109--124, 2006.
• 39: Shmuel Ur , Eyal Bin , Yaron Wolfsthal, Hardware and Software, Verification and Testing: First International Haifa Verification Conference, Haifa, Israel, November 13-16, 2005, Revised Selected Papers (Lecture Notes in Computer Science), Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 40: Valgrind. http://valgrind.org.
• 41: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]
• 42: 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
• 43: L. Wang and S. D. Stoller. Run-time analysis for atomicity. Electronic Notes in Theoretical Computer Science, 89(2), 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Monitors

General Terms:
Algorithms, Languages, Reliability, Verification

Keywords:
aspect-oriented programming, race detection, runtime verification, semantic pointcuts, static analysis