Skip to main content
Top
Published in: International Journal on Software Tools for Technology Transfer 4/2019

30-01-2018 | Regular Paper

Fast detection of concurrency errors by state space traversal with randomization and early backtracking

Authors: Pavel Parízek, Ondřej Lhoták

Published in: International Journal on Software Tools for Technology Transfer | Issue 4/2019

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

State space traversal is a very popular approach to detect concurrency errors and test concurrent programs. However, it is not practically feasible for complex programs with many thread interleavings and a large state space. Many techniques explore only a part of the state space in order to find errors quickly—building upon the observation that errors can often be found in a particular small part of the state space. Great improvements in performance have been achieved also through randomization. In the context of this research direction, we present the DFS-RB algorithm that augments the standard algorithm for depth-first traversal with early backtracking. Specifically, it is possible to backtrack early from a state before all outgoing transitions have been explored. The DFS-RB algorithm is non-deterministic—it uses random numbers, together with values of several parameters, to determine when and how early backtracking takes place in the search. To evaluate DFS-RB, we performed a large experimental study with our prototype implementation in Java Pathfinder on several Java programs. The results show that DFS-RB achieves better performance in terms of speed and error detection than many state-of-the-art techniques for many benchmarks in our set. Nevertheless, it is difficult to find a single configuration of DFS-RB that works well for many different benchmarks. We designed a ranking algorithm whose purpose is to identify configurations that yield overall consistently good performance with a small variation.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Appendix
Available only for authorised users
Footnotes
1
We used the release of JPF corresponding to the commit number 715 in the repository for JPF v6.
 
2
We used the version defined by the commit number 29 in the repository that contains JPF v8.
 
Literature
1.
go back to reference Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Proceedings of POPL. ACM (2014) Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Proceedings of POPL. ACM (2014)
2.
go back to reference Barnat, J., Brim, L., Rockai, P.: On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties. Sci. Comput. Program. 77(12), 1272–1288 (2012)CrossRefMATH Barnat, J., Brim, L., Rockai, P.: On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties. Sci. Comput. Program. 77(12), 1272–1288 (2012)CrossRefMATH
3.
go back to reference Behrmann, G., Hune, T., Vaandrager, F.: Distributing timed model checking—how the search order matters. In: Proceedings of CAV, LNCS, vol. 1855 (2000) Behrmann, G., Hune, T., Vaandrager, F.: Distributing timed model checking—how the search order matters. In: Proceedings of CAV, LNCS, vol. 1855 (2000)
4.
go back to reference Biere, A.: PicoSAT essentials. J. Satisf. Boolean Model. Comput. (JSAT) 4, 75–97 (2008)MATH Biere, A.: PicoSAT essentials. J. Satisf. Boolean Model. Comput. (JSAT) 4, 75–97 (2008)MATH
5.
go back to reference Bisiani, R.: Beam Search. Encyclopedia of Artificial Intelligence. Wiley, New York (1992) Bisiani, R.: Beam Search. Encyclopedia of Artificial Intelligence. Wiley, New York (1992)
6.
go back to reference Burckhardt, S., Kothari, P., Musuvathi, M., Nagarakatte, S.: A Randomized scheduler with probabilistic guarantees of finding bugs. In: Proceedings of ASPLOS. ACM (2010) Burckhardt, S., Kothari, P., Musuvathi, M., Nagarakatte, S.: A Randomized scheduler with probabilistic guarantees of finding bugs. In: Proceedings of ASPLOS. ACM (2010)
7.
go back to reference Ciardo, G., Gluckman, J., Nicol, D.: Distributed state space generation of discrete-state stochastic models. INFORMS J. Comput. 10(1), 82–93 (1998)CrossRef Ciardo, G., Gluckman, J., Nicol, D.: Distributed state space generation of discrete-state stochastic models. INFORMS J. Comput. 10(1), 82–93 (1998)CrossRef
8.
go back to reference Coons, K.E., Burckhardt, S., Musuvathi, M.: GAMBIT: effective unit testing for concurrency libraries. In: Proceedings of PPoPP. ACM (2010) Coons, K.E., Burckhardt, S., Musuvathi, M.: GAMBIT: effective unit testing for concurrency libraries. In: Proceedings of PPoPP. ACM (2010)
9.
go back to reference Dwyer, M.B., Elbaum, S.G., Person, S., Purandare, R.: Parallel randomized state-space search. In: Proceedings of ICSE, IEEE CS (2007) Dwyer, M.B., Elbaum, S.G., Person, S., Purandare, R.: Parallel randomized state-space search. In: Proceedings of ICSE, IEEE CS (2007)
10.
go back to reference Dwyer, M., Hatcliff, J., Robby, Ranganath, V.: Exploiting object escape and locking information in artial-order reductions for concurrent object-oriented programs. Formal Methods Syst. Des. 25(2–3), 199–240 (2004)CrossRefMATH Dwyer, M., Hatcliff, J., Robby, Ranganath, V.: Exploiting object escape and locking information in artial-order reductions for concurrent object-oriented programs. Formal Methods Syst. Des. 25(2–3), 199–240 (2004)CrossRefMATH
11.
go back to reference Dwyer, M.B., Person, S., Elbaum, S.G.: Controlling factors in evaluating path-sensitive error detection techniques. In: Proceedings of SIGSOFT FSE. ACM (2006) Dwyer, M.B., Person, S., Elbaum, S.G.: Controlling factors in evaluating path-sensitive error detection techniques. In: Proceedings of SIGSOFT FSE. ACM (2006)
12.
go back to reference Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Int. J. Softw. Tools Technol. Transf. 5(2–3), 247–267 (2004)CrossRefMATH Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Int. J. Softw. Tools Technol. Transf. 5(2–3), 247–267 (2004)CrossRefMATH
13.
go back to reference Edelkamp, S., Schuppan, V., Bosnacki, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on directed model checking. In: Proceedings of 5th International Workshop on Model Checking and Artificial Intelligence, LNCS, vol. 5348 (2008) Edelkamp, S., Schuppan, V., Bosnacki, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on directed model checking. In: Proceedings of 5th International Workshop on Model Checking and Artificial Intelligence, LNCS, vol. 5348 (2008)
14.
go back to reference Een, N., Sorensson, N.: An extensible SAT-solver. In: Proceedings of SAT, LNCS, vol. 2919 (2003) Een, N., Sorensson, N.: An extensible SAT-solver. In: Proceedings of SAT, LNCS, vol. 2919 (2003)
15.
go back to reference Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. In: Proceedings of POPL. ACM (2011) Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. In: Proceedings of POPL. ACM (2011)
16.
go back to reference Engels, T.A.N., Groote, J.F., van Weerdenburg, M.J., Willemse, T.A.C.: Search algorithms for automated validation. J. Logic Algebr. Program. 78(4), 274–287 (2009)MathSciNetCrossRefMATH Engels, T.A.N., Groote, J.F., van Weerdenburg, M.J., Willemse, T.A.C.: Search algorithms for automated validation. J. Logic Algebr. Program. 78(4), 274–287 (2009)MathSciNetCrossRefMATH
17.
go back to reference Farzan, A., Holzer, A., Razavi, N., Veith, H.: Con2colic testing. In: Proceedings of ESEC/FSE. ACM (2013) Farzan, A., Holzer, A., Razavi, N., Veith, H.: Con2colic testing. In: Proceedings of ESEC/FSE. ACM (2013)
18.
go back to reference Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of POPL. ACM (2005) Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of POPL. ACM (2005)
19.
go back to reference Godefroid, P.: Partial-order methods for the verification of concurrent systems. In: LNCS, vol. 1032 (1996) Godefroid, P.: Partial-order methods for the verification of concurrent systems. In: LNCS, vol. 1032 (1996)
20.
go back to reference Gomes, C., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of AAAI (1998) Gomes, C., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of AAAI (1998)
21.
go back to reference Groce, A., Visser, W.: Heuristics for model checking Java programs. Int. J. Softw. Tools Technol. Transf. 6(4), 260–276 (2004)CrossRefMATH Groce, A., Visser, W.: Heuristics for model checking Java programs. Int. J. Softw. Tools Technol. Transf. 6(4), 260–276 (2004)CrossRefMATH
22.
go back to reference Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Proceedings of SPIN, LNCS, vol. 4595 (2007) Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Proceedings of SPIN, LNCS, vol. 4595 (2007)
23.
go back to reference Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Softw. Eng. 33(10), 659–674 (2007)CrossRef Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Softw. Eng. 33(10), 659–674 (2007)CrossRef
24.
go back to reference Holzmann, G.J., Joshi, R., Groce, A.: Tackling large verification problems with the swarm tool. In: Proceedings of SPIN, LNCS, vol. 5156 (2008) Holzmann, G.J., Joshi, R., Groce, A.: Tackling large verification problems with the swarm tool. In: Proceedings of SPIN, LNCS, vol. 5156 (2008)
25.
go back to reference Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification. In: Proceedings of ASE, IEEE CS (2008) Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification. In: Proceedings of ASE, IEEE CS (2008)
26.
go back to reference Jagannath, V., Kirn, M., Lin, Y., Marinov, D.: Evaluating machine-independent metrics for state-space exploration. In: Proceedings of ICST, IEEE CS (2012) Jagannath, V., Kirn, M., Lin, Y., Marinov, D.: Evaluating machine-independent metrics for state-space exploration. In: Proceedings of ICST, IEEE CS (2012)
27.
go back to reference Jones, M., Mercer, E.: Explicit state model checking with hopper. In: Proceedings of SPIN, LNCS, vol. 2989 (2004) Jones, M., Mercer, E.: Explicit state model checking with hopper. In: Proceedings of SPIN, LNCS, vol. 2989 (2004)
28.
go back to reference Jones, M., Sorber, J.: Parallel search for LTL violations. Int. J. Softw. Tools Technol. Transf. 7(1), 31–42 (2005)CrossRef Jones, M., Sorber, J.: Parallel search for LTL violations. Int. J. Softw. Tools Technol. Transf. 7(1), 31–42 (2005)CrossRef
29.
go back to reference Kalibera, T., Hagelberg, J., Pizlo, F., Plsek, A., Titzer, B., Vitek, J.: CDx: a family of real-time Java benchmarks. In: Proceedings of JTRES. ACM (2009) Kalibera, T., Hagelberg, J., Pizlo, F., Plsek, A., Titzer, B., Vitek, J.: CDx: a family of real-time Java benchmarks. In: Proceedings of JTRES. ACM (2009)
30.
go back to reference Laarman, A., Langerak, R., van de Pol, J., Weber, M., Wijs, A.: Multi-core nested depth-first search. In: Proceedings of ATVA, LNCS, vol. 6996 (2011) Laarman, A., Langerak, R., van de Pol, J., Weber, M., Wijs, A.: Multi-core nested depth-first search. In: Proceedings of ATVA, LNCS, vol. 6996 (2011)
31.
go back to reference Laarman, A., van de Pol, J., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Proceedings of FMCAD. IEEE (2010) Laarman, A., van de Pol, J., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Proceedings of FMCAD. IEEE (2010)
32.
go back to reference Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Proceedings of SPIN, LNCS, vol. 1680 (1999) Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Proceedings of SPIN, LNCS, vol. 1680 (1999)
33.
34.
go back to reference van Moorsel, A.P.A., Wolter, K.: Analysis of restart mechanisms in software systems. IEEE Trans. Softw. Eng. 32(8), 547–558 (2006)CrossRef van Moorsel, A.P.A., Wolter, K.: Analysis of restart mechanisms in software systems. IEEE Trans. Softw. Eng. 32(8), 547–558 (2006)CrossRef
35.
go back to reference Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of PLDI. ACM (2007) Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of PLDI. ACM (2007)
36.
go back to reference Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Proceedings of OSDI, USENIX (2008) Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Proceedings of OSDI, USENIX (2008)
37.
go back to reference Parízek, P., Kalibera, T.: Efficient detection of errors in Java components using random environment and restarts. In: Proceedings of TACAS, LNCS, vol. 6015 (2010) Parízek, P., Kalibera, T.: Efficient detection of errors in Java components using random environment and restarts. In: Proceedings of TACAS, LNCS, vol. 6015 (2010)
38.
go back to reference Parízek, P., Lhoták, O.: Randomized backtracking in state space traversal. In: Proceedings of SPIN, LNCS, vol. 6823 (2011) Parízek, P., Lhoták, O.: Randomized backtracking in state space traversal. In: Proceedings of SPIN, LNCS, vol. 6823 (2011)
39.
go back to reference Parízek, P., Lhoták, O.: Identifying future field accesses in exhaustive state space traversal. In: Proceedings of ASE, IEEE CS (2011) Parízek, P., Lhoták, O.: Identifying future field accesses in exhaustive state space traversal. In: Proceedings of ASE, IEEE CS (2011)
40.
go back to reference Parízek, P.: Hybrid analysis for partial order reduction of programs with arrays. In: Proceedings of VMCAI, LNCS, vol. 9583 (2016) Parízek, P.: Hybrid analysis for partial order reduction of programs with arrays. In: Proceedings of VMCAI, LNCS, vol. 9583 (2016)
41.
go back to reference Parízek, P.: Fast error detection with hybrid analyses of future accesses. In: Proceedings of SAC, MUSEPAT Track. ACM (2016) Parízek, P.: Fast error detection with hybrid analyses of future accesses. In: Proceedings of SAC, MUSEPAT Track. ACM (2016)
42.
go back to reference Qadeer, S.: Daisy File System. Joint CAV/ISSTA special event on specification, verification and testing of concurrent software (2004) Qadeer, S.: Daisy File System. Joint CAV/ISSTA special event on specification, verification and testing of concurrent software (2004)
43.
go back to reference Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Proceedings of TACAS, LNCS, vol. 3440 (2005) Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Proceedings of TACAS, LNCS, vol. 3440 (2005)
44.
go back to reference Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Proceedings of CAV, LNCS, vol. 3576 (2005) Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Proceedings of CAV, LNCS, vol. 3576 (2005)
45.
go back to reference Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Parallel explicit model checking for generalized Büchi automata. In: Proceedings of TACAS, LNCS, vol. 9035 (2015) Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Parallel explicit model checking for generalized Büchi automata. In: Proceedings of TACAS, LNCS, vol. 9035 (2015)
46.
go back to reference Rungta, N., Mercer, E.: Generating counter-examples through randomized guided search. In: Proceedings of SPIN, LNCS, vol. 4595 (2007) Rungta, N., Mercer, E.: Generating counter-examples through randomized guided search. In: Proceedings of SPIN, LNCS, vol. 4595 (2007)
47.
go back to reference Rungta, N., Mercer, E.: Clash of the titans: tools and techniques for hunting bugs in concurrent programs. In: Proceedings of PADTAD. ACM (2009) Rungta, N., Mercer, E.: Clash of the titans: tools and techniques for hunting bugs in concurrent programs. In: Proceedings of PADTAD. ACM (2009)
48.
go back to reference Sen, K.: Effective random testing of concurrent programs. In: Proceedings of ASE. ACM (2007) Sen, K.: Effective random testing of concurrent programs. In: Proceedings of ASE. ACM (2007)
49.
go back to reference Seppi, K., Jones, M., Lamborn, P.: Guided model checking with a bayesian meta-heuristic. Fundamenta Informaticae 70(1–2), 111–126 (2006)MathSciNetMATH Seppi, K., Jones, M., Lamborn, P.: Guided model checking with a bayesian meta-heuristic. Fundamenta Informaticae 70(1–2), 111–126 (2006)MathSciNetMATH
51.
go back to reference Spearman, C.: The proof and measurement of association between two things. Am. J. Psychol. 15(1), 72–101 (1904)CrossRef Spearman, C.: The proof and measurement of association between two things. Am. J. Psychol. 15(1), 72–101 (1904)CrossRef
52.
go back to reference Stern, U., Dill, D.L.: Parallelizing the murphi verifier. In: Proceedings of CAV, LNCS, vol. 1254 (1997) Stern, U., Dill, D.L.: Parallelizing the murphi verifier. In: Proceedings of CAV, LNCS, vol. 1254 (1997)
53.
go back to reference Thomson, P., Donaldson, A.F., Betts, A.: Concurrency testing using schedule bounding: an empirical study. In: Proceedings of PPoPP. ACM (2014) Thomson, P., Donaldson, A.F., Betts, A.: Concurrency testing using schedule bounding: an empirical study. In: Proceedings of PPoPP. ACM (2014)
54.
go back to reference Udupa, A., Desai, A., Rajamani, S.: Depth bounded explicit-state model checking. In: Proceedings of SPIN, LNCS, vol. 6823 (2011) Udupa, A., Desai, A., Rajamani, S.: Depth bounded explicit-state model checking. In: Proceedings of SPIN, LNCS, vol. 6823 (2011)
55.
go back to reference Vargha, A., Delaney, H.D.: A critique and improvement of the CL common language effect size statistics of McGraw and Wong. J. Educ. Behav. Stat. 25(2), 101–132 (2000) Vargha, A., Delaney, H.D.: A critique and improvement of the CL common language effect size statistics of McGraw and Wong. J. Educ. Behav. Stat. 25(2), 101–132 (2000)
56.
go back to reference Walsh, T.: Search in a small world. In: Proceedings of IJCAI, Morgan Kaufmann (1999) Walsh, T.: Search in a small world. In: Proceedings of IJCAI, Morgan Kaufmann (1999)
57.
go back to reference Wehrle, M., Kupferschmid, S., Podelski, A.: Transition-based directed model checking. In: Proceedings of TACAS, LNCS, vol. 5505 (2009) Wehrle, M., Kupferschmid, S., Podelski, A.: Transition-based directed model checking. In: Proceedings of TACAS, LNCS, vol. 5505 (2009)
58.
go back to reference Wehrle, M., Kupferschmid, S.: Context-enhanced directed model checking. In: Proceedings of SPIN, LNCS, vol. 6349 (2010) Wehrle, M., Kupferschmid, S.: Context-enhanced directed model checking. In: Proceedings of SPIN, LNCS, vol. 6349 (2010)
59.
go back to reference Wijs, A., Bosnacki, D.: Many-core on-the-fly model checking of safety properties using GPUs. Int. J. Softw. Tools Technol. Transf. 18(2), 169–185 (2016)CrossRef Wijs, A., Bosnacki, D.: Many-core on-the-fly model checking of safety properties using GPUs. Int. J. Softw. Tools Technol. Transf. 18(2), 169–185 (2016)CrossRef
60.
go back to reference Wijs, A., Lisser, B.: Distributed extended beam search for quantitative model checking. In: Proceedings of MoChArt, LNCS, vol. 4428 (2006) Wijs, A., Lisser, B.: Distributed extended beam search for quantitative model checking. In: Proceedings of MoChArt, LNCS, vol. 4428 (2006)
61.
go back to reference Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: a runtime model checker for multithreaded C programs. Technical Report UUCS-08-004, University of Utah (2008) Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: a runtime model checker for multithreaded C programs. Technical Report UUCS-08-004, University of Utah (2008)
Metadata
Title
Fast detection of concurrency errors by state space traversal with randomization and early backtracking
Authors
Pavel Parízek
Ondřej Lhoták
Publication date
30-01-2018
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 4/2019
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-018-0484-7

Other articles of this Issue 4/2019

International Journal on Software Tools for Technology Transfer 4/2019 Go to the issue

Premium Partner