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.
- 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.Google Scholar
- 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. In R. Johnson and R. P. Gabriel, editors, OOPSLA, pages 345--364. ACM, 2005. Google ScholarDigital Library
- 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.Google Scholar
- C. Artho, K. Havelund, and A. Biere. High-level data races. Software Testing, Verification and Reliability, 13(4):207--227, 2003.Google ScholarCross Ref
- 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.Google Scholar
- 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. In AOSD conference, pages 87--98. ACM Press, 2005. Google ScholarDigital Library
- 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.Google Scholar
- S. Bensalem, J.-C. Fernandez, K. Havelund, and L. Mounier. Confirmation of deadlock potentials detected by runtime analysis. In PADTAD '06: Proceeding of the 2006 workshop on Parallel and distributed systems: testing and debugging, pages 41--50, New York, NY, USA, 2006. ACM. Google ScholarDigital Library
- S. Bensalem and K. Havelund. Dynamic deadlock analysis of multi-threaded programs. In Ur et al. {39}, pages 208--223. Google ScholarDigital Library
- 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.Google Scholar
- E. Bodden and K. Havelund. Racer: Effective race detection using AspectJ (extended version). Technical Report abc-2008-1, http://www.aspectbench.org/, 05 2008.Google Scholar
- 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. Google ScholarDigital Library
- 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.Google Scholar
- 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, 25(2-3):167--198, 2004. Google ScholarDigital Library
- 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.Google Scholar
- F. Chen, T. F. Serbanuta, and G. Rosu. jPredictor: A predictive runtime analysis tool for Java. In International Conference on Software Engineering (ICSE'08). ACM press, 2008. To appear. Google ScholarDigital Library
- S. Cohen. Jtrek. Compaq. No longer maintained.Google Scholar
- M. Dahm. BCEL. http://jakarta.apache.org/bcel.Google Scholar
- M. d'Amorim and K. Havelund. Event-based runtime verification of Java programs. In WODA '05: Proceedings of the third international workshop on Dynamic analysis, pages 1--7, New York, NY, USA, 2005. ACM Press. Google ScholarDigital Library
- 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.Google Scholar
- A. Eustace and A. Srivastava. ATOM: a flexible interface for building high performance program analysis tools. In Technical Conference Proceedings on USENIX 1995, pages 25--25, Berkeley, CA, USA, 1995. USENIX Association. Google ScholarDigital Library
- 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, 19(3):267--279, 2007. Google ScholarDigital Library
- C. Flanagan and S. Freund. Atomizer: A dynamic atomicity checker for multithreaded programs. SIGPLAN Notices, 39(1):256--267, 2004. Google ScholarDigital Library
- B. Goetz. Java concurrency in practice. Addison Wesley, 2006.Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- R. L. Halpert, C. J. F. Pickett, and C. Verbrugge. Component-based lock allocation. In PACT'07: Proceedings of the 16th International Conference on Parallel Architectures and Compilation Techniques, pages 353--364, Sept. 2007. Google ScholarDigital Library
- J. Harrow. Runtime checking of multithreaded applications with visual threads. In K. Havelund, J. Penix, and W. Visser, editors, SPIN Model Checking and Software Verification, volume 1885 of Lecture Notes in Computer Science, pages 331--342. Springer, 2000. http://h30097.www3.hp.com/dtk/visualthreads_ov.html Google ScholarDigital Library
- K. Havelund. Using runtime analysis to guide model checking of Java programs. In SPIN Model Checking and Software Verification, volume 1885 of Lecture Notes in Computer Science, pages 245--264. Springer, 2000. Google ScholarDigital Library
- K. Havelund. Using runtime analysis to guide model checking of Java programs. In SPIN Model Checking and Software Verification, volume 1885 of Lecture Notes in Computer Science, pages 245--264. Springer, 2000. Google ScholarDigital Library
- A. Kinneer, M. B. Dwyer, and G. Rothermel. Sofya: Supporting rapid development of dynamic program analyses for java. In ICSE COMPANION '07: Companion to the proceedings of the 29th International Conference on Software Engineering, pages 51--52, Washington, DC, USA, 2007. IEEE Computer Society. Google ScholarDigital Library
- D. Lea. Concurrent Programming in Java: Design Principles and Patterns. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1996. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In R. N. Horspool, editor, CC, volume 2304 of Lecture Notes in Computer Science, pages 213--228. Springer, 2002. Google ScholarDigital Library
- R. O'Callahan and J.-D. Choi. Hybrid dynamic data race detection. In ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'03), pages 167--178, 2003. Google ScholarDigital Library
- S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: a dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems, 15(4):391--411, 1997. Google ScholarDigital Library
- S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: a dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems, 15(4):391--411, 1997. Google ScholarDigital Library
- V. Stolz and E. Bodden. Temporal assertions using AspectJ. Electr. Notes in Theor. Computer Science, 144(4):109--124, 2006. Google ScholarDigital Library
- S. Ur, E. Bin, and Y. Wolfsthal, editors. Hardware and Software Verification and Testing, First International Haifa Verification Conference, Haifa, Israel, November 13-16, 2005, volume 3875 of Lecture Notes in Computer Science. Springer, 2006. Google ScholarDigital Library
- Valgrind. http://valgrind.org.Google Scholar
- W. Visser, K. Havelund, G. P. Brat, S. Park, and F. Lerda. Model checking programs. In 15th IEEE International Conference on Automated Software Engineering, volume 10, pages 203--232, 2003. Google ScholarDigital Library
- C. von Praun and T. R. Gross. Object race detection. In OOPSLA, pages 70--82, 2001. Google ScholarDigital Library
- L. Wang and S. D. Stoller. Run-time analysis for atomicity. Electronic Notes in Theoretical Computer Science, 89(2), 2003.Google Scholar
Index Terms
- Racer: effective race detection using aspectj
Recommendations
Aspect-Oriented Race Detection in Java
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 ...
TRADE: Precise Dynamic Race Detection for Scalable Transactional Memory Systems
As other multithreaded programs, transactional memory (TM) programs are prone to race conditions. Previous work focuses on extending existing definitions of data race for lock-based applications to TM applications, which requires all transactions to be ...
Fast&Furious: A Tool for Detecting Covert Racing
PARMA-DITAM '15: Proceedings of the 6th Workshop on Parallel Programming and Run-Time Management Techniques for Many-core ArchitecturesExisting multi-threaded applications perform synchronization either in an explicit way, e.g., making use of the functionality provided by synchronization libraries or in an implicit or "covert" way, e.g., using shared variables. Unfortunately, the ...
Comments