Abstract
Testing concurrent programs is a challenging problem: (1) the tester has to come up with a set of input values that may trigger a bug, and (2) even with a bug-triggering input value, there may be a large number of interleavings that need to be explored. This paper proposes an approach for testing concurrent programs that explores both input and interleaving spaces in a systematic way. It is based on a program transformation technique that takes a concurrent program P as an input and generates a sequential program that simulates a subset of behaviours of P. It is then possible to use an available sequential testing tool to test the resulting sequential program. We introduce a new interleaving selection technique, called bounded-interference, which is based on the idea of limiting the degree of interference from other threads. The transformation is sound in the sense that any bug discovered by a sequential testing tool in the sequential program is a bug in the original concurrent program. We have implemented our approach into a prototype tool that tests concurrent C# programs. Our experiments show that our approach is effective in finding both previously known and new bugs.
Supported in part by the Austrian National Research Network S11403-N23 (RiSE) of the Austrian Science Fund (FWF), and by the Vienna Science and Technology Fund (WWTF) grant PROSEED.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: Exe: Automatically generating inputs of death. ACM Trans. Inf. Syst. Secur. 12, 10:1–10:38 (2008)
Flanagan, C., Freund, S.N.: Fasttrack: efficient and precise dynamic race detection. Commun. ACM 53, 93–101 (2010)
Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: PDLI, pp. 213–223. ACM (2005)
Lahiri, S.K., Qadeer, S., Rakamarić, Z.: Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 509–524. Springer, Heidelberg (2009)
Lal, A., Reps, T.: Reducing concurrent analysis under a context bound to sequential analysis. Form. Methods Syst. Des. 35, 73–97 (2009)
Miller, J.C., Maloney, C.J.: Systematic mistake analysis of digital computer programs. Commun. ACM 6, 58–63 (1963)
Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: OSDI, pp. 267–280 (2008)
Park, C.-S., Sen, K.: Randomized active atomicity violation detection in concurrent programs. In: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, SIGSOFT 2008/FSE-16, pp. 135–145. ACM, New York (2008)
Park, S., Lu, S., Zhou, Y.: Ctrigger: exposing atomicity violation bugs from their hiding places. In: ASPLOS, pp. 25–36 (2009)
Pozniansky, E., Schuster, A.: Multirace: efficient on-the-fly data race detection in multithreaded c++ programs: Research articles. Concurr. Comput.: Pract. Exper. 19, 327–340 (2007)
Qadeer, S., Wu, D.: Kiss: keep it simple and sequential. SIGPLAN Not. 39, 14–24 (2004)
Sen, K.: Race directed random testing of concurrent programs. In: PLDI, pp. 11–21 (2008)
Sen, K., Agha, G.: CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 419–423. Springer, Heidelberg (2006)
Sorrentino, F., Farzan, A., Madhusudan, P.: Penelope: weaving threads to expose atomicity violations. In: FSE 2010, pp. 37–46. ACM (2010)
Tillmann, N., de Halleux, J.: Pex–White Box Test Generation for.NET. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134–153. Springer, Heidelberg (2008)
La Torre, S., Madhusudan, P., Parlato, G.: Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 477–492. Springer, Heidelberg (2009)
Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-Based Symbolic Analysis for Atomicity Violations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 328–342. Springer, Heidelberg (2010)
Yi, J., Sadowski, C., Flanagan, C.: Sidetrack: generalizing dynamic atomicity analysis. In: PADTAD 2009, pp. 8:1–8:10. ACM, New York (2009)
Zhang, W., Lim, J., Olichandran, R., Scherpelz, J., Jin, G., Lu, S., Reps, T.: Conseq: detecting concurrency bugs through sequential errors. In: ASPLOS, pp. 251–264 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Razavi, N., Farzan, A., Holzer, A. (2012). Bounded-Interference Sequentialization for Testing Concurrent Programs. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. ISoLA 2012. Lecture Notes in Computer Science, vol 7609. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34026-0_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-34026-0_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34025-3
Online ISBN: 978-3-642-34026-0
eBook Packages: Computer ScienceComputer Science (R0)