Concurrency Testing, Verification, and Debugging

Benchmarks and types of concurrency bugs

· W. Xiong, S. Park, J. Zhang, Y. Zhou, and Z. Ma, “Ad hoc synchronization considered harmful.”

· C. Artho, K. Havelund, and A. Biere, “High‐level data races,” Software Testing, Verification and Reliability, vol. 13, Dec. 2003, pp. 207-227.

· S. Lu, S. Park, E. Seo, and Y. Zhou, “Learning from mistakes — A Comprehensive Study on Real World Concurrency Bug Characteristics,” Proceedings of the International Conference on Architecture Support for Programming Languages and Operating Systems, 2008.

· N. Jalbert, C. Pereira, G. Pokam, and K. Sen, “RADBench: a concurrency bug benchmark suite,” Proceedings of the 3rd USENIX conference on Hot topics in parallelism, Berkeley, CA, USA: USENIX Association, 2011.

· R.H.B. Netzer and B.P. Miller, “What are race conditions?: Some issues and formalizations,” ACM Lett. Program. Lang. Syst., vol. 1, Mar. 1992, pp. 74–88.

Coverage Criteria

· S. Lu, W. Jiang, and Y. Zhou, “A Study of Interleaving Coverage Criteria,” Proceedings of the 15th ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2007.

· C.-S.D. Yang, A.L. Souter, and L.L. Pollock, “All-du-path coverage for parallel programs,” Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis, New York, NY, USA: ACM, 1998, pp. 153–162.

· Bron, E. Farchi, Y. Magid, Y. Nir, and S. Ur, “Applications of synchronization coverage,” Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, New York, NY, USA: ACM, 2005, pp. 206–212.

· M. Factor, E. Farchi, Y. Lichtenstein, and Y. Malka, “Testing concurrent programs: a formal evaluation of coverage criteria,” Proceedings of the Seventh Israeli Conference on Computer Systems and Software Engineering, IEEE, 1996, pp. 119-126.

· R.H. Carver and Kuo-Chung Tai, “Use of sequencing constraints for specification-based testing of concurrent programs,” IEEE Transactions on Software Engineering, vol. 24, Jun. 1998, pp. 471-490.

Non-determinism

· J. Burnim and K. Sen, “Asserting and checking determinism for multithreaded programs,” Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, New York, NY, USA: ACM, 2009, pp. 3–12.

· J. Burnim and K. Sen, “DETERMIN: inferring likely deterministic specifications of multithreaded programs,” Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 1, New York, NY, USA: ACM, 2010, pp. 415–424.

· J. Burnim, T. Elmas, G. Necula, and K. Sen, “NDSeq: runtime checking for nondeterministic sequential specifications of parallel correctness,” Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation, New York, NY, USA: ACM, 2011, pp. 401–414.

· J. Burnim, G. Necula, and K. Sen, “Separating functional and parallel correctness using nondeterministic sequential specifications,” Proceedings of the 2nd USENIX conference on Hot topics in parallelism, Berkeley, CA, USA: USENIX Association, 2010.

· C. Sadowski, S.N. Freund, and C. Flanagan, “SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs,” Programming Languages and Systems, G. Castagna, ed., Berlin, Heidelberg: Springer Berlin Heidelberg, 2009, pp. 394-409.

Random testing

· Y. Lin, X. Tang, Y. Chen, and J. Zhao, “A Divergence-Oriented Approach to Adaptive Random Testing of Java Programs,” Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, Washington, DC, USA: IEEE Computer Society, 2009, pp. 221–232.

· P. Joshi, C.-S. Park, K. Sen, and M. Naik, “A randomized dynamic program analysis technique for detecting real deadlocks,” Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation, New York, NY, USA: ACM, 2009, pp. 110–120.

· K. Sen, “Race directed random testing of concurrent programs,” Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, New York, NY, USA: ACM, 2008, pp. 11–21.

· C.-S. Park and K. Sen, “Randomized active atomicity violation detection in concurrent programs,” Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, New York, NY, USA: ACM, 2008, pp. 135–145.

· S. Scott D., “Testing Concurrent Java Programs using Randomized Scheduling,” Electronic Notes in Theoretical Computer Science, vol. 70, Dec. 2002, pp. 142-157.

· K. Sen, “Effective random testing of concurrent programs,” Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, New York, NY, USA: ACM, 2007, pp. 323–332.

CHESS

· M. Musuvathi, S. Qadeer, and T. Ball, CHESS: A Systematic Testing Tool for Concurrent Software., Microsoft Research, 2007.

· M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P.A. Nainar, and I. Neamtiu, “Finding and reproducing Heisenbugs in concurrent programs,” Proceedings of the 8th USENIX conference on Operating systems design and implementation, Berkeley, CA, USA: USENIX Association, 2008, pp. 267–280.

· K.E. Coons, S. Burckhardt, and M. Musuvathi, “GAMBIT: effective unit testing for concurrency libraries,” Proceedings of the 15th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, New York, NY, USA: ACM, 2010, pp. 15–24.

· M. Musuvathi and S. Qadeer, “Iterative context bounding for systematic testing of multithreaded programs,” Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, New York, NY, USA: ACM, 2007, pp. 446–455.

· T. Ball, S. Burckhardt, K. Coons, M. Musuvathi, and S. Qadeer, “Preemption Sealing for Efficient Concurrency Testing,” Tools and Algorithms for the Construction and Analysis of Systems, J. Esparza and R. Majumdar, eds., Springer Berlin / Heidelberg, 2010, pp. 420-434.

· M. Musuvathi and S. Qadeer, “Fair stateless model checking,” Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, New York, NY, USA: ACM, 2008, pp. 362–371.

Static analysis

· S.P. Masticola and B.G. Ryder, “A model of Ada programs for static deadlock detection in polynomial times,” Proceedings of the 1991 ACM/ONR workshop on Parallel and distributed debugging, New York, NY, USA: ACM, 1991, pp. 97–107.

· M. Naik, C.-S. Park, K. Sen, and D. Gay, “Effective static deadlock detection,” Proceedings of the 31st International Conference on Software Engineering, Washington, DC, USA: IEEE Computer Society, 2009, pp. 386–396.

· M. Naik, A. Aiken, and J. Whaley, “Effective static race detection for Java,” Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, New York, NY, USA: ACM, 2006, pp. 308–319.

· D. Engler and K. Ashcraft, “RacerX: effective, static detection of race conditions and deadlocks,” Proceedings of the nineteenth ACM symposium on Operating systems principles, New York, NY, USA: ACM, 2003, pp. 237–252.

· Z. Rakamarić, “STORM: static unit checking of concurrent programs,” Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2, New York, NY, USA: ACM, 2010, pp. 519–520.

Model checking and verification

· P. Garg and P. Madhusudan, “Compositionality Entails Sequentializability,” Tools and Algorithms for the Construction and Analysis of Systems, P.A. Abdulla and K.R.M. Leino, eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 26-40.

· S. Khurshid, C.S. PĂsĂreanu, and W. Visser, “Generalized Symbolic Execution for Model Checking and Testing,” Tools and Algorithms for the Construction and Analysis of Systems, H. Garavel and J. Hatcliff, eds., Berlin, Heidelberg: Springer Berlin Heidelberg, , pp. 553-568.

· P. Godefroid, “Model checking for programming languages using VeriSoft,” Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, New York, NY, USA: ACM, 1997, pp. 174–186.

· W. Visser, K. Havelund, G. Brat, S.J. Park, and F. Lerda, “Model checking programs,” Automated Software Engineering, vol. 10, 2003, pp. 203–232.

· Gupta, C. Popeea, and A. Rybalchenko, “Predicate abstraction and refinement for verifying multi-threaded programs,” Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, New York, NY, USA: ACM, 2011, pp. 331–344.

· D.L. Bruening, “Systematic testing of multithreaded Java programs,” Massachusetts Institute of Technology, 1999.

· W. Visser, C.S. Pǎsǎreanu, and S. Khurshid, “Test input generation with java PathFinder,” Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, New York, NY, USA: ACM, 2004, pp. 97–107.

· G.J. Holzmann, “The model checker SPIN,” IEEE Transactions on Software Engineering, vol. 23, May. 1997, pp. 279-295.

· Gupta, C. Popeea, and A. Rybalchenko, “Threader: A Constraint-Based Verifier for Multi-threaded Programs,” Computer Aided Verification, G. Gopalakrishnan and S. Qadeer, eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 412-417.

· K. Havelund, “Using Runtime Analysis to Guide Model Checking of Java Programs,” SPIN Model Checking and Software Verification, K. Havelund, J. Penix, and W. Visser, eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2000, pp. 245-264.

Partial-order reduction

· C. Flanagan and P. Godefroid, “Dynamic partial-order reduction for model checking software,” Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, NY, USA: ACM, 2005, pp. 110–121.

Reachability testing

· Y. Lei, R.H. Carver, R. Kacker, and D. Kung, “A combinatorial testing strategy for concurrent programs,” Software Testing, Verification & Reliability, vol. 17, Dec. 2007, pp. 207–225.

· R.H. Carver and Y. Lei, “A General Model for Reachability Testing of Concurrent Programs,” Formal Methods and Software Engineering, J. Davies, W. Schulte, and M. Barnett, eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, pp. 76-98.

· Y. Lei and R. Carver, “A New Algorithm for Reachability Testing of Concurrent Programs,” Proceedings of the 16th IEEE International Symposium on Software Reliability Engineering, Washington, DC, USA: IEEE Computer Society, 2005, pp. 346–355.

· R.H. Carver and J. Lei, “A Stateful Approach to Testing Monitors in Multithreaded Programs,” Proceedings of the 2010 IEEE 12th International Symposium on High-Assurance Systems Engineering, Washington, DC, USA: IEEE Computer Society, 2010, pp. 54–63.

· Yu Lei and Kuo-Chung Tai, “Efficient reachability testing of asynchronous message-passing programs,” Eighth IEEE International Conference on Engineering of Complex Computer Systems, 2002. Proceedings, IEEE, 2002, pp. 35- 44.

· W.E. Wong and Y. Lei, “Reachability Graph-Based Test Sequence Generation for Concurrent Programs,” International Journal on Software Engineering and Knowledge Engineering, vol. 18, 2008, pp. 803-822.

· Y. Lei and R.H. Carver, “Reachability Testing of Concurrent Programs,” IEEE Transactions on Software Engineering, vol. 32, Jun. 2006, pp. 382–403.

· G.-H. Hwang, K.-C. Tai, and T.-L. Hwang, “Reachability testing: an approach to testing concurrent software.”

· W.E. Wong, Yu Lei, and Xiao Ma, “Effective generation of test sequences for structural testing of concurrent programs,” 10th IEEE International Conference on Engineering of Complex Computer Systems, 2005. ICECCS 2005. Proceedings, IEEE, 2005, pp. 539- 548.

Structural testing

· F.S. Sarmanho, P.S.L. Souza, S.R.S. Souza, and A.S. Simão, “Structural Testing for Semaphore-Based Multithread Programs,” Computational Science – ICCS 2008, M. Bubak, G.D. Albada, J. Dongarra, and P.M.A. Sloot, eds., Berlin, Heidelberg: Springer Berlin Heidelberg, , pp. 337-346.

· R.N. Taylor, D.L. Levine, and C.D. Kelly, “Structural testing of concurrent programs,” IEEE Transactions on Software Engineering, vol. 18, Mar. 1992, pp. 206-215.

Race detection and flipping

· K. Sen and G. Agha, “A race-detection and flipping algorithm for automated testing of multi-threaded programs,” Proceedings of the 2nd international Haifa verification conference on Hardware and software, verification and testing, Berlin, Heidelberg: Springer-Verlag, 2007, pp. 166–182.

· K. Sen and G. Agha, “CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools,” Computer Aided Verification, T. Ball and R.B. Jones, eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, pp. 419-423.

Detecting atomicity violations

· C. Flanagan and S.N. Freund, “Atomizer: a dynamic atomicity checker for multithreaded programs,” Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, NY, USA: ACM, 2004, pp. 256–267.

· S. Lu, J. Tucek, F. Qin, and Y. Zhou, “AVIO: detecting atomicity violations via access interleaving invariants,” Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, New York, NY, USA: ACM, 2006, pp. 37–48.

· S. Park, S. Lu, and Y. Zhou, “CTrigger: exposing atomicity violation bugs from their hiding places,” Proceeding of the 14th international conference on Architectural support for programming languages and operating systems, New York, NY, USA: ACM, 2009, pp. 25–36.

· S. Lu, S. Park, and Y. Zhou, “Finding Atomicity-Violation Bugs through Unserializable Interleaving Testing,” IEEE Transactions on Software Engineering, vol. PP, 0, pp. 1-1.

· J. Burnim, G. Necula, and K. Sen, “Specifying and checking semantic atomicity for multithreaded programs,” Proceedings of the sixteenth international conference on Architectural support for programming languages and operating systems, New York, NY, USA: ACM, 2011, pp. 79–90.

Verification for different memory models

· S.V. Adve, M.D. Hill, B.P. Miller, and R.H.B. Netzer, “Detecting data races on weak memory systems,” Proceedings of the 18th Annual International Symposium on Computer Architecture, New York, NY, USA: ACM, 1991, pp. 234–243.

· J. Burnim, K. Sen, and C. Stergiou, “Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models,” Tools and Algorithms for the Construction and Analysis of Systems, P.A. Abdulla and K.R.M. Leino, eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 11-25.

· J. Burnim, K. Sen, and C. Stergiou, “Testing concurrent programs on relaxed memory models,” Proceedings of the 2011 International Symposium on Software Testing and Analysis, New York, NY, USA: ACM, 2011, pp. 122–132.

· S. Burckhardt and M. Musuvathi, “Effective Program Verification for Relaxed Memory Models,” Computer Aided Verification, A. Gupta and S. Malik, eds., Berlin, Heidelberg: Springer Berlin Heidelberg, , pp. 107-120.

Reproduction of concurrency bugs

· Y. Lei, R.H. Carver, R. Kacker, and D. Kung, “A combinatorial testing strategy for concurrent programs,” Software Testing, Verification & Reliability, vol. 17, Dec. 2007, pp. 207–225.

· Y. Lei and R.H. Carver, “Reachability Testing of Concurrent Programs,” IEEE Transactions on Software Engineering, vol. 32, Jun. 2006, pp. 382–403.

· G.-H. Hwang, K.-C. Tai, and T.-L. Hwang, “Reachability testing: an approach to testing concurrent software.”

Offline analysis

· N. Jalbert and K. Sen, “A trace simplification technique for effective debugging of concurrent programs,” Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering, New York, NY, USA: ACM, 2010, pp. 57–66.

· J. Huang and C. Zhang, “An Efficient Static Trace Simplification Technique for Debugging Concurrent Programs,” Static Analysis, E. Yahav, ed., Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 163-179.

· S. Narayanasamy, Z. Wang, J. Tigani, A. Edwards, and B. Calder, “Automatically classifying benign and harmful data races using replay analysis,” Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, New York, NY, USA: ACM, 2007, pp. 22–31.

Concurrency bug avoidance

· J. Wu, H. Cui, and J. Yang, “Bypassing races in live applications with execution filters,” Proceedings of the 9th USENIX Conference on Operating Systems Design and Implementation, Berkeley, CA, USA: USENIX Association, 2010, pp. 1–13.

· H. Cui, J. Wu, C.-C. Tsai, and J. Yang, “Stable deterministic multithreading through schedule memoization,” Proceedings of the 9th USENIX conference on Operating systems design and implementation, Berkeley, CA, USA: USENIX Association, 2010, pp. 1–13.

Other publications on concurrency testing and verification

· Y. Lei, R. Carver, D. Kung, V. Gupta, and M. Hernandez, “A State Exploration-Based Approach to Testing Java Monitors,” Proceedings of the 17th International Symposium on Software Reliability Engineering, Washington, DC, USA: IEEE Computer Society, 2006, pp. 256–265.

· P. Joshi, M. Naik, K. Sen, and D. Gay, “An effective dynamic analysis for detecting generalized deadlocks,” Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering, New York, NY, USA: ACM, 2010, pp. 327–336.

· M. Vaziri, F. Tip, and J. Dolby, “Associating synchronization constraints with data in an object-oriented language,” Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, New York, NY, USA: ACM, 2006, pp. 334–345.

· P. Parizek, J. Adamek, and T. Kalibera, “Automated Construction of Reasonable Environment for Java Components,” Electronic Notes in Theoretical Computer Science, vol. 253, Oct. 2009, pp. 145-160.

· K. Sen and G. Agha, “Automated Systematic Testing of Open Distributed Programs,” Fundamental Approaches to Software Engineering, L. Baresi and R. Heckel, eds., Springer Berlin / Heidelberg, 2006, pp. 339-356.

· P. Joshi, M. Naik, C.-S. Park, and K. Sen, “CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs,” Proceedings of the 21st International Conference on Computer Aided Verification, Berlin, Heidelberg: Springer-Verlag, 2009, pp. 675–681.

· M. Ricken and R. Cartwright, “ConcJUnit: unit testing for concurrent programs,” Proceedings of the 7th International Conference on Principles and Practice of Programming in Java, New York, NY, USA: ACM, 2009, pp. 129–132.

· W. Zhang, C. Sun, and S. Lu, “ConMem: detecting severe concurrency bugs through an effect-oriented approach,” Proceedings of the fifteenth edition of ASPLOS on Architectural support for programming languages and operating systems, New York, NY, USA: ACM, 2010, pp. 179–192.

· W. Zhang, J. Lim, R. Olichandran, J. Scherpelz, G. Jin, S. Lu, and T. Reps, “ConSeq: detecting concurrency bugs through sequential errors,” Proceedings of the sixteenth international conference on Architectural support for programming languages and operating systems, New York, NY, USA: ACM, 2011, pp. 251–264.

· R. Agarwal, L. Wang, and S.D. Stoller, “Detecting Potential Deadlocks with Static Analysis and Run-Time Monitoring,” Hardware and Software, Verification and Testing, S. Ur, E. Bin, and Y. Wolfsthal, eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, pp. 191-207.

· C. von Praun, “Detecting Synchronization Defects in Multi-Threaded Object-Oriented Programs,” Swiss Federal Institute of Technology Zurich, 2004.

· Y. Shi, S. Park, Z. Yin, S. Lu, Y. Zhou, W. Chen, and W. Zheng, “Do I use the wrong definition?: DefUse: definition-use invariants for detecting concurrency and sequential bugs,” Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, New York, NY, USA: ACM, 2010, pp. 160–174.

· S. Bensalem and K. Havelund, “Dynamic Deadlock Analysis of Multi-threaded Programs,” Hardware and Software, Verification and Testing, S. Ur, E. Bin, and Y. Wolfsthal, eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, pp. 208-223.

· S. Qadeer and D. Wu, “KISS: keep it simple and sequential,” Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, New York, NY, USA: ACM, 2004, pp. 14–24.

· O. Edelstein, E. Farchi, Y. Nir, G. Ratsaby, and S. Ur, “Multithreaded Java program test generation,” IBM Systems Journal, vol. 41, 2002, pp. 111-125.

· S. Lu, S. Park, C. Hu, X. Ma, W. Jiang, Z. Li, R.A. Popa, and Y. Zhou, “MUVI: automatically inferring multi-variable access correlations and detecting related semantic and concurrency bugs,” Proceedings of twenty-first ACM SIGOPS symposium on Operating systems principles, New York, NY, USA: ACM, 2007, pp. 103–116.

· C. von Praun and T.R. Gross, “Object race detection,” Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, New York, NY, USA: ACM, 2001, pp. 70–82.

· R.-D. Yang and C.-G. Chung, “Path analysis testing of concurrent programs,” Information and Software Technology, vol. 34, Jan. 1992, pp. 43-56.

· J. Huang and C. Zhang, “Persuasive prediction of concurrency access anomalies,” Proceedings of the 2011 International Symposium on Software Testing and Analysis, New York, NY, USA: ACM, 2011, pp. 144–154.

· J.J. Harrow, “Runtime Checking of Multithreaded Applications with Visual Threads,” SPIN Model Checking and Software Verification, K. Havelund, J. Penix, and W. Visser, eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2000, pp. 331-342.

· R. Agarwal and S.D. Stoller, “Run-time detection of potential deadlocks for programs with locks, semaphores, and condition variables,” Proceedings of the 2006 workshop on Parallel and distributed systems: testing and debugging, New York, NY, USA: ACM, 2006, pp. 51–60.

· T. Katayama, E. Itoh, Z. Furukawa, and K. Ushijima, “Test-case generation for concurrent programs with the testing criteria using interaction sequences,” Software Engineering Conference, 1999. (APSEC ’99) Proceedings. Sixth Asia Pacific, IEEE, 1999, pp. 590-597.

· C. Sadowski and J. Yi, “User evaluation of correctness conditions: a case study of cooperability,” Evaluation and Usability of Programming Languages and Tools, New York, NY, USA: ACM, 2010, pp. 2:1–2:6.

Web sites

· http://code.google.com/p/jchord/

· http://theory.stanford.edu/~aiken/

· http://cseweb.ucsd.edu/~lerner/radar.html