Tayfun Elmas
Abstract
We present CONCURRIT, a domain-specific language (DSL) for reproducing concurrency bugs. Given some partial information about the nature of a bug in an application, a programmer can write a CONCURRIT script to formally and concisely specify a set of thread schedules to explore in order to find a schedule exhibiting the bug. Further, the programmer can specify how these thread schedules should be searched to find a schedule that reproduces the bug. We implemented CONCURRIT as an embedded DSL in C++, which uses manual or automatic source instrumentation to partially control the scheduling of the software under test. Using CONCURRIT, we were able to write concise tests to reproduce concurrency bugs in a variety of benchmarks, including the Mozilla's SpiderMonkey JavaScript engine, Memcached, Apache's HTTP server, and MySQL.
- G. Altekar and I. Stoica. ODR: Output-deterministic replay for multicore debugging. In SOSP, 2009. Google Scholar
Digital Library
- T. Ball, S. Burckhardt, K. Coons, M. Musuvathi, , and S. Qadeer. Preemption sealing for efficient concurrency testing. Technical Report MSR-TR-2009-143, 2009.Google Scholar
- C. Bienia, S. Kumar, J. P. Singh, and K. Li. The PARSEC Benchmark Suite: Characterization and Architectural Implications. In PACT, 2008. Google ScholarDigital Library
- S. Burckhardt, P. Kothari, M. Musuvathi, and S. Nagarakatte. A randomized scheduler with probabilistic guarantees of finding bugs. In ASPLOS, 2010. Google ScholarDigital Library
- P. Godefroid. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Springer-Verlag Inc., 1996. URL citeseer.ist.psu.edu/godefroid95partialorder.html. Google ScholarDigital Library
- P. Godefroid. Software model checking: The verisoft approach. In Form. Methods Syst. Des., 2005. Google ScholarDigital Library
- G. Gueta, C. Flanagan, E. Yahav, and M. Sagiv. Cartesian partial-order reduction. In SPIN, 2007. Google ScholarDigital Library
- R. Iosif. Symmetry reduction criteria for software model checking. In SPIN, 2002. Google ScholarDigital Library
- Jagannath, Gligoric, Jin, Luo, Rosu, and Marinov}jagannath11imunitV. Jagannath, M. Gligoric, D. Jin, Q. Luo, G. Rosu, and D. Marinov. Improved multithreaded unit testing. In ESEC/FSE, 2011. Google ScholarDigital Library
- Jagannath, Luo, and Marinov}jagannath11changeawareV. Jagannath, Q. Luo, and D. Marinov. Change-aware preemption prioritization. In ISSTA, 2011. Google ScholarDigital Library
- N. Jalbert and K. Sen. A trace simplification technique for effective debugging of concurrent programs. In FSE, 2010. Google ScholarDigital Library
- N. Jalbert, C. Pereira, G. Pokam, and K. Sen. RADBench: A concurrency bug benchmark suite. In HOTPAR, 2011. Google ScholarDigital Library
- R. Jhala and R. Majumdar. Software model checking. In ACM Comput. Surv., 2009. Google ScholarDigital Library
- M. Kim, Y. Kim, and H. Kim. A comparative study of software model checkers as unit testing tools: An industrial case study. In IEEE Trans. Softw. Eng., 2011. Google ScholarDigital Library
- S. La Torre, M. Parthasarathy, and G. Parlato. Analyzing recursive programs using a fixed-point calculus. In PLDI, 2009. Google ScholarDigital Library
- B. Long, D. Hoffman, and P. Strooper. Tool support for testing concurrent Java components. In IEEE Trans. Softw. Eng., 2003. Google ScholarDigital Library
- S. Lu, J. Tucek, F. Qin, and Y. Zhou. AVIO: Detecting atomicity violations via access interleaving invariants. In ASPLOS, 2006. Google ScholarDigital Library
- C.-K. Luk, R. Cohn, R. Muth, H. Patil, A. Klauser, G. Lowney, S. Wallace, V. J. Reddi, and K. Hazelwood. Pin: Building customized program analysis tools with dynamic instrumentation. In PLDI, 2005. Google ScholarDigital Library
- M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI, 2007. Google ScholarDigital Library
- M. Musuvathi and S. Qadeer. Fair stateless model checking. In PLDI, 2008. Google ScholarDigital Library
- V. Mutilin. Concurrent testing of Java components using Java PathFinder. In ISoLA, 2006. Google ScholarDigital Library
- S. Park, Y. Zhou, W. Xiong, Z. Yin, R. Kaushik, K. H. Lee, and S. Lu. PRES: Probabilistic replay with execution sketching on multiprocessors. In SOSP, 2009. Google ScholarDigital Library
- W. Pugh and N. Ayewah. Unit testing concurrent software. In ASE, 2007. Google ScholarDigital Library
- K. Sen. Race directed random testing of concurrent programs. In PLDI, 2008. Google ScholarDigital Library
- O. Shacham, N. Bronson, A. Aiken, M. Sagiv, M. Vechev, and E. Yahav. Testing atomicity of composed concurrent operations. In OOPSLA, 2011. Google ScholarDigital Library
- Y. Yang, X. Chen, and G. Gopalakrishnan. Inspect: A runtime model checker for multithreaded C programs. Technical Report UUCS-08-004, 2008.Google Scholar
Index Terms
- CONCURRIT: a domain specific language for reproducing concurrency bugs
Recommendations
CONCURRIT: a domain specific language for reproducing concurrency bugs
PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe present CONCURRIT, a domain-specific language (DSL) for reproducing concurrency bugs. Given some partial information about the nature of a bug in an application, a programmer can write a CONCURRIT script to formally and concisely specify a set of ...
CTrigger: exposing atomicity violation bugs from their hiding places
ASPLOS 2009Multicore hardware is making concurrent programs pervasive. Unfortunately, concurrent programs are prone to bugs. Among different types of concurrency bugs, atomicity violation bugs are common and important. Existing techniques to detect atomicity ...
CTrigger: exposing atomicity violation bugs from their hiding places
ASPLOS 2009Multicore hardware is making concurrent programs pervasive. Unfortunately, concurrent programs are prone to bugs. Among different types of concurrency bugs, atomicity violation bugs are common and important. Existing techniques to detect atomicity ...
Comments