Abstract
In this work we present an abstraction-guided symbolic execution technique that quickly detects errors in concurrent programs. The input to the technique is a set of target locations that represent a possible error in the program. We generate an abstract system from a backward slice for each target location. The backward slice contains program locations relevant in testing the reachability of the target locations. The backward slice only considers sequential execution and does not capture any inter-thread dependencies. A combination of heuristics are to guide a symbolic execution along locations in the abstract system in an effort to generate a corresponding feasible execution trace to the target locations. When the symbolic execution is unable to make progress, we refine the abstraction by adding locations to handle inter-thread dependencies. We demonstrate empirically that abstraction-guided symbolic execution generates feasible execution paths in the actual system to find concurrency errors in a few seconds where exhaustive symbolic execution fails to find the same errors in an hour.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Anand, S., Godefroid, P., Tillmann, N.: Demand-driven compositional symbolic execution. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 367–381. Springer, Heidelberg (2008)
Artho, C., Biere, A.: Applying static analysis to large-scale, multi-threaded java programs. In: Proc. ASWEC, Washington, DC, USA, p. 68. IEEE Computer Society, Los Alamitos (2001)
Ball, T., Rajamani, S.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001)
Edelkamp, S.: Planning with pattern databases. In: Proc. European Conference on Planning, pp. 13–24 (2001)
Engler, D., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. In: Proc. SOSP 2003, Bolton Landing, NY, USA, pp. 237–252. ACM Press, New York (2003)
Eytani, Y., Havelund, K., Stoller, S.D., Ur, S.: Towards a framework and a benchmark for testing tools for multi-threaded programs: Research articles. Concurr. Comput. Pract. Exper. 19(3), 267–279 (2007)
Godefroid, P.: Model checking for programming languages using Verisoft. In: Proc. of POPL, pp. 174–186. ACM, New York (1997)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)
Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. SIGPLAN Not. 39(4), 229–243 (2004)
Khurshid, S., Pasareanu, C., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003)
King, J.C.: Symbolic execution and program testing. Communications of the ACM 19(7), 385–394 (1976)
Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. SIGPLAN Not. 42(6), 446–455 (2007)
Musuvathi, M., Qadeer, S.: Fair stateless model checking. In: Proc. of PLDI, pp. 362–371. ACM, New York (2008)
Nanshi, K., Somenzi, F.: Guiding simulation with increasingly refined abstract traces. In: Proc. DAC, pp. 737–742. ACM, New York (2006)
De Paula, F.M., Hu, A.J.: An effective guidance strategy for abstraction-guided simulation. In: Proc. DAC 2007, pp. 63–68. ACM, New York (2007)
Pǎsǎreanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: Proc. ISSTA, pp. 15–26. ACM, New York (2008)
Rungta, N., Mercer, E.G.: Hardness for explicit state software model checking benchmarks. In: Proc. SEFM, London, U.K, September 2007, pp. 247–256 (2007)
Rungta, N., Mercer, E.G.: A meta heuristic for effectively detecting concurrency errors. In: Haifa Verification Conference, Haifa, Israel (2008)
Rungta, N., Mercer, E.G.: Guided model checking for programs with polymorphism. In: Proc. PEPM, pp. 21–30. ACM, New York (2009)
Sen, K.: Race directed random testing of concurrent programs. SIGPLAN Not. 43(6), 11–21 (2008)
Sen, K., Agha, G.: A race-detection and flipping algorithm for automated testing of multi-threaded programs. In: Bin, E., Ziv, A., Ur, S. (eds.) HVC 2006. LNCS, vol. 4383, pp. 166–182. Springer, Heidelberg (2007)
Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proc. ESEC/FSE-13, pp. 263–272. ACM, New York (2005)
Tomb, A., Brat, G., Visser, W.: Variably interprocedural program analysis for runtime error detection. In: Proc. ISSTA, pp. 97–107. ACM Press, New York (2007)
Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering 10(2), 203–232 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rungta, N., Mercer, E.G., Visser, W. (2009). Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution. In: Păsăreanu, C.S. (eds) Model Checking Software. SPIN 2009. Lecture Notes in Computer Science, vol 5578. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02652-2_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-02652-2_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02651-5
Online ISBN: 978-3-642-02652-2
eBook Packages: Computer ScienceComputer Science (R0)