Francesco Sorrentino
ABSTRACT
Testing concurrent programs is challenged by the interleaving explosion problem--- the problem of exploring the large number of interleavings a program exhibits, even under a single test input. Rather than try all interleavings, we propose to test wisely: to exercise only those schedules that lead to interleavings that are typical error patterns. In particular, in this paper we select schedules that exercise patterns of interaction that correspond to atomicity violations. Given an execution of a program under a test harness, our technique is to algorithmically mine from the execution a small set of alternate schedules that cause atomicity violations. The program is then re-executed under these predicted atomicity-violating schedules, and verified by the test harness. The salient feature of our tool is the efficient algorithmic prediction and synthesis of alternate schedules that cover all possible atomicity violations at program locations. We implement the tool PENELOPE that realizes this testing framework and show that the monitoring, prediction, and rescheduling (with precise repro) are efficient and effective in finding bugs related to atomicity violations.
- http://http://www.javagrande.org/.Google Scholar
- http://jakarta.apache.org/bcel/.Google Scholar
- F. Chen, T.F. Serbanuta, and G. Rosu. jpredictor: a predictive runtime analysis tool for java. In ICSE, pages 221--230, 2008. Google ScholarDigital Library
- A. Farzan and P. Madhusudan. Monitoring atomicity in concurrent programs. In CAV, pages 52--65, 2008. Google ScholarDigital Library
- A. Farzan, P. Madhusudan, and F. Sorrentino. Meta-analysis for atomicity violations under nested locking. In CAV, pages 248--262, 2009. Google ScholarDigital Library
- C. Flanagan and S. N Freund. Atomizer: a dynamic atomicity checker for multithreaded programs. In POPL, pages 256--267, 2004. Google ScholarDigital Library
- C. Flanagan, S. N. Freund, and J. Yi. Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In PLDI, pages 293--303, 2008. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. A type and effect system for atomicity. In PLDI, pages 338--349, 2003. Google ScholarDigital Library
- J. Hatcliff, Robby, and M. Dwyer. Verifying atomicity specifications for concurrent object-oriented software using model checking. In VMCAI, pages 175--190, 2004.Google ScholarCross Ref
- V. Kahlon, F. Ivancic, and A. Gupta. Reasoning about threads communicating via locks. In CAV, pages 505--518, 2005. Google ScholarDigital Library
- R. J. Lipton. Reduction: a method of proving properties of parallel programs. Commun. ACM, 18(12):717--721, 1975. Google ScholarDigital Library
- S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In ASPLOS, pages 329--339, 2008. Google ScholarDigital Library
- M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI, pages 446--455. ACM, 2007. Google ScholarDigital Library
- C. Papadimitriou. The theory of database concurrency control. Computer Science Press., 1986. Google ScholarDigital Library
- C-S Park and K. Sen. Randomized active atomicity violation detection in concurrent programs. In SIGSOFT '08/FSE-16, pages 135--145, New York, NY, USA, 2008. ACM. Google ScholarDigital Library
- S. Park, S. Lu, and Y. Zhou. Ctrigger: exposing atomicity violation bugs from their hiding places. In ASPLOS, pages 25--36, 2009. Google ScholarDigital Library
- S., J. Tucek, F. Qin, and Y. Zhou. Avio: detecting atomicity violations via access interleaving invariants. In ASPLOS, pages 37--48, 2006.Google Scholar
- C. von Praun and T. R. Gross. Object race detection. SIGPLAN Not., 36(11):70--82, 2001. Google ScholarDigital Library
- C. Wang, R. Limaye, M. Ganai, and A. Gupta. Trace-based symbolic analysis for atomicity violations. In TACAS, 2010. Google ScholarDigital Library
- L. Wang and S. D. Stoller. Accurate and efficient runtime detection of atomicity errors in concurrent programs. In PPoPP, pages 137--146, 2006. Google ScholarDigital Library
- L. Wang and S. D. Stoller. Runtime analysis of atomicity for multi-threaded programs. IEEE Transactions on Software Engineering, 32:93--110, 2006. Google ScholarDigital Library
- M. Xu, R. Bodík, and M. D. Hill. A serializability violation detector for shared--memory server programs. SIGPLAN Not., 40(6):1--14, 2005. Google ScholarDigital Library
- J. Yi, C. Sadowski, and C. Flanagan. Sidetrack: generalizing dynamic atomicity analysis. In PADTAD, pages 1--10, 2009. Google ScholarDigital Library
Recommendations
Randomized active atomicity violation detection in concurrent programs
SIGSOFT '08/FSE-16: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineeringAtomicity 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 ...
Sound and efficient concurrency bug prediction
ESEC/FSE 2021: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software EngineeringConcurrency bugs are extremely difficult to detect. Recently, several dynamic techniques achieve sound analysis. M2 is even complete for two threads. It is designed to decide whether two events can occur consecutively. However, real-world concurrency ...
RacerX: effective, static detection of race conditions and deadlocks
SOSP '03This paper describes RacerX, a static tool that uses flow-sensitive, interprocedural analysis to detect both race conditions and deadlocks. It is explicitly designed to find errors in large, complex multithreaded systems. It aggressively infers checking ...
Comments