skip to main content
10.1145/1453101.1453121acmconferencesArticle/Chapter ViewAbstractPublication PagesfseConference Proceedingsconference-collections
research-article

Randomized active atomicity violation detection in concurrent programs

Published:09 November 2008Publication History

ABSTRACT

Atomicity is an important specification that enables programmers to understand atomic blocks of code in a multi-threaded program as if they are sequential. This significantly simplifies the programmer's job to reason about correctness. Several modern multithreaded programming languages provide no built-in support to ensure atomicity; instead they rely on the fact that programmers would use locks properly in order to guarantee that atomic code blocks are indeed atomic. However, improper use of locks can sometimes fail to ensure atomicity. Therefore, we need tools that can check atomicity properties of lock-based code automatically.

We propose a randomized dynamic analysis technique to detect a special, but important, class of atomicity violations that are often found in real-world programs. Specifically, our technique modifies the existing Java thread scheduler behavior to create atomicity violations with high probability. Our approach has several advantages over existing dynamic analysis tools. First, we can create a real atomicity violation and see if an exception can be thrown. Second, we can replay an atomicity violating execution by simply using the same seed for random number generation---we do not need to record the execution. Third, we give no false warnings unlike existing dynamic atomicity checking techniques. We have implemented the technique in a prototype tool for Java and have experimented on a number of large multi-threaded Java programs and libraries. We report a number of previously known and unknown bugs and atomicity violations in these Java programs.

References

  1. S. V. Adve, M. D. Hill, B. P. Miller, and R. H. B. Netzer. Detecting data races on weak memory systems. In 18th annual International Symposium on Computer architecture (ISCA), pages 234--243. ACM, 1991. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. R. Agarwal, A. Sasturkar, L. Wang, and S. D. Stoller. Optimized run-time race detection and atomicity checking using partial discovered types. In 20th IEEE/ACM International Conference on Automated software engineering (ASE), pages 233--242. ACM, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. A. Aiken and D. Gay. Barrier inference. In 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 342--354. ACM, 1998. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. D. F. Bacon, R. E. Strom, and A. Tarafdar. Guava: a dialect of java without data races. In ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA'00), pages 382--400, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. C. Boyapati and M. C. Rinard. A parameterized type system for race-free java programs. In ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA'01), pages 56--69, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. D. Bruening. Systematic testing of multithreaded Java programs. Master's thesis, MIT, 1999.Google ScholarGoogle Scholar
  7. S. Burckhardt, R. Alur, and M. M. K. Martin. Checkfence: checking consistency of concurrent data types on relaxed memory models. In CM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI), pages 12--21, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. R. H. Carver and Y. Lei. A general model for reachability testing of concurrent programs. In 6th International Conference on Formal Engineering Methods (ICFEM'04), volume 3308 of LNCS, pages 76--98, 2004.Google ScholarGoogle ScholarCross RefCross Ref
  9. 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. In Proc. of the ACM SIGPLAN Conference on Programming language design and implementation, pages 258--269, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. J.-D. Choi, B. P. Miller, and R. H. B. Netzer. Techniques for debugging parallel programs with flowback analysis. ACM Trans. Program. Lang. Syst., 13(4):491--530, 1991. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. A. Dinning and E. Schonberg. Detecting access anomalies in programs with critical sections. In Proc. of the ACM/ONR Workshop on Parallel and Distributed Debugging, 1991. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. M. B. Dwyer, S. Elbaum, S. Person, and R. Purandare. Parallel randomized state-space search. In 29th International Conference on Software Engineering (ICSE), pages 3--12. IEEE, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. 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. Form. Methods Syst. Des., 25(2--3):199--240, 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. J. E. M. Clarke, O. Grumberg, and D. A. Peled. Model checking. MIT Press, 1999. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. O. Edelstein, E. Farchi, Y. Nir, G. Ratsaby, and S. Ur. Multithreaded Java program test generation. IBM Systems Journal, 41(1):111--125, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. D. R. Engler and K. Ashcraft. Racerx: effective, static detection of race conditions and deadlocks. In 19th ACM Symposium on Operating Systems Principles (SOSP), pages 237--252, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. A. Farzan and P. Madhusudan. Causal atomicity. In Computer Aided Verification (CAV'06), volume 4144 of Lecture Notes in Computer Science, pages 315--328. Springer, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. C. Flanagan. Verifying commit-atomicity using model-checking. In 11th International SPIN Workshop, pages 252--266, 2004.Google ScholarGoogle ScholarCross RefCross Ref
  19. C. Flanagan and S. N. Freund. Type-based race detection for java. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'00), pages 219--232, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. C. Flanagan and S. N. Freund. Detecting race conditions in large programs. In Proc. of the Program Analysis for Software Tools and Engineering Conference, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. C. Flanagan and S. N. Freund. Atomizer: a dynamic atomicity checker for multithreaded programs. In 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 256--267, 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. C. Flanagan, S. N. Freund, and J. Yi. Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In PLDI '08: Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, pages 293--303. ACM, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Proc. of the ACM SIGPLAN Conference on Programming language design and implementation (PLDI'03), pages 338--349, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. S. N. Freund and S. Qadeer. Checking concise specifications for multithreaded software. Journal of Object Technology, 3(6):81--101, 2004.Google ScholarGoogle ScholarCross RefCross Ref
  25. D. Gay, P. Levis, R. von Behren, M. Welsh, E. Brewer, and D. Culler. The nesC language: A holistic approach to networked embedded systems. In ACM SIGPLAN Conference on Programming language design and implementation, pages 1--11, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  26. P. Godefroid. Model checking for programming languages using verisoft. In 24th Symposium on Principles of Programming Languages, pages 174--186, 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. R. Grosu and S. A. Smolka. Monte carlo model checking. In 11th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), volume 3440 of LNCS, pages 271--286, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. J. Hatcliff, Robby, and M. B. Dwyer. Verifying atomicity specifications for concurrent object-oriented software using model-checking. In Proc. of the International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04), pages 175--190, 2004.Google ScholarGoogle ScholarCross RefCross Ref
  29. K. Havelund and T. Pressburger. Model Checking Java Programs using Java PathFinder. Int. Journal on Software Tools for Technology Transfer, 2(4):366--381, 2000.Google ScholarGoogle ScholarCross RefCross Ref
  30. T. A. Henzinger, R. Jhala, and R. Majumdar. Race checking by context inference. SIGPLAN Not., 39(6):1--13, 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. G. Holzmann. The Spin model checker. IEEE Transactions on Software Engineering, 23(5):279--295, 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  32. R. J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717--721, 1975. Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In ACM Symposium on Programming Language Design and Implementation (PLDI'07), 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  34. M. Naik, A. Aiken, and J. Whaley. Effective static race detection for java. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 308--319, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  35. S. Narayanasamy, Z. Wang, J. Tigani, A. Edwards, and B. Calder. Automatically classifying benign and harmful data racesallusing replay analysis. In ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI), pages 22--31, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  36. P. Pratikakis, J. S. Foster, and M. Hicks. LOCKSMITH: context-sensitive correlation analysis for race detection. In ACM SIGPLAN conference on Programming language design and implementation (PLDI), pages 320--331. ACM, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  37. S. Qadeer and D. Wu. Kiss: keep it simple and sequential. In ACM SIGPLAN 2004 conference on Programming language design and implementation (PLDI), pages 14--24. ACM, 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  38. S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. E. Anderson. Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst., 15(4):391--411, 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  39. K. Sen. Effective random testing of concurrent programs. In 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE'07), 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  40. K. Sen. Race directed random testing of concurrent programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08), 2008. To appear. Google ScholarGoogle ScholarDigital LibraryDigital Library
  41. K. Sen and G. Agha. A race-detection and flipping algorithm for automated testing of multi-threaded programs. In Haifa verification conference 2006 (HVC'06), Lecture Notes in Computer Science. Springer, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  42. S. F. Siegel, A. Mironova, G. S. Avrunin, and L. A. Clarke. Using model checking with symbolic execution to verify parallel numerical programs. In International symposium on Software testing and analysis (ISSTA), pages 157--168. ACM Press, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  43. N. Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, pages 97--106, 1993.Google ScholarGoogle Scholar
  44. S. D. Stoller. Testing concurrent Java programs using randomized scheduling. In Workshop on Runtime Verification (RV'02), volume 70 of ENTCS, 2002.Google ScholarGoogle ScholarCross RefCross Ref
  45. R. Vallee-Rai, L. Hendren, V. Sundaresan, P. Lam, E. Gagnon, and P. Co. Soot - a Java optimization framework. In CASCON 1999, pages 125--135, 1999.Google ScholarGoogle ScholarDigital LibraryDigital Library
  46. W. Visser, K. Havelund, G. Brat, and S. Park. Model checking programs. In 15th International Conference on Automated Software Engineering (ASE). IEEE, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  47. C. von Praun and T. R. Gross. Object race detection. In 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications (OOPSLA), pages 70--82. ACM, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  48. L. Wang and S. D. Stoller. Run-time analysis for atomicity. In 3rd Workshop on Run-time Verification (RV'03), volume 89 of ENTCS, 2003.Google ScholarGoogle ScholarCross RefCross Ref
  49. L. Wang and S. D. Stoller. Accurate and efficient runtime detection of atomicity errors in concurrent programs. In Proc. ACM SIGPLAN 2006 Symposium on Principles and Practice of Parallel Programming (PPoPP), pages 137--146. ACM Press, Mar. 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Randomized active atomicity violation detection in concurrent programs

              Recommendations

              Comments

              Login options

              Check if you have access through your login credentials or your institution to get full access on this article.

              Sign in
              • Published in

                cover image ACM Conferences
                SIGSOFT '08/FSE-16: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering
                November 2008
                369 pages
                ISBN:9781595939951
                DOI:10.1145/1453101

                Copyright © 2008 ACM

                Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

                Publisher

                Association for Computing Machinery

                New York, NY, United States

                Publication History

                • Published: 9 November 2008

                Permissions

                Request permissions about this article.

                Request Permissions

                Check for updates

                Qualifiers

                • research-article

                Acceptance Rates

                Overall Acceptance Rate17of128submissions,13%

                Upcoming Conference

                FSE '24

              PDF Format

              View or Download as a PDF file.

              PDF

              eReader

              View online with eReader.

              eReader