Skip to main content
SpringerLink
Log in

Context-Bounded Translations for Concurrent Software: An Empirical Evaluation

  • Conference paper
Model Checking Software (SPIN 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6349))

Included in the following conference series:

Abstract

Context-Bounded Analysis has emerged as a practical automatic formal analysis technique for fine-grained, shared-memory concurrent software. Two recent papers (in CAV 2008 and 2009) have proposed ingenious translation approaches that promise much better scalability, backed by compelling, but differing, theoretical and conceptual advantages. Empirical evidence comparing the translations, however, has been lacking. Furthermore, these papers focused exclusively on Boolean model checking, ignoring the also widely used paradigm of verification-condition checking. In this paper, we undertake a methodical, empirical evaluation of the three main source-to-source translations for context-bounded analysis of concurrent software, in a verification-condition-checking paradigm. We evaluate their scalability under a wide range of experimental conditions. Our results show: (1) The newest, CAV 2009 translation is the clear loser, with the CAV 2008 translation the best in most instances, but the oldest, brute-force translation doing surprisingly well. Clearly, previous results for Boolean model checking do not apply to verification-condition checking. (2) Disturbingly, confounding factors in the experimental design can change the relative performance of the translations, highlighting the importance of extensive and thorough experiments. For example, using a different (slower) SMT solver changes the relative ranking of the translations, potentially misleading researchers and practitioners to use an inferior translation. (3) SMT runtimes grow exponentially with verification-condition length, but different translations and parameters give different exponential curves. This suggests that the practical scalability of a translation scheme might be estimated by combining the size of the queries with an empirical or theoretical measure of the complexity of solving that class of query.

This work was supported by a Microsoft Research Graduate Fellowship and the Natural Science and Engineering Research Council of Canada.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Babić, D., Hu, A.J.: Calysto: Scalable and precise extended static checking. In: Intl. Conf. on Software Engineering (ICSE), pp. 211–220 (2008)

    Google Scholar 

  2. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Conf. on Programming Language Design and Implementation (PLDI), pp. 203–213 (2001)

    Google Scholar 

  3. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamarić, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 19–33. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design (FMSD) 19(1), 7–34 (2001)

    Article  MATH  Google Scholar 

  7. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Workshop, pp. 52–71 (1981)

    Google Scholar 

  8. Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  9. Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI–C programs using SAT. Formal Methods in System Design (FMSD) 25, 105–127 (2004)

    Article  MATH  Google Scholar 

  10. Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: Intl. Conf. on Software Engineering (ICSE), pp. 439–448 (2000)

    Google Scholar 

  11. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (2005)

    Google Scholar 

  13. Demartini, C., Iosif, R., Sisto, R.: A deadlock detection tool for concurrent Java programs. Software — Practice and Experience 29(7), 577–603 (1999)

    Article  Google Scholar 

  14. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18, 453–457 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  15. Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  16. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Conf. on Programming Language Design and Implementation (PLDI), pp. 234–245 (2002)

    Google Scholar 

  17. Ganai, M.K., Gupta, A.: Efficient modeling of concurrent systems in BMC. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 114–133. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)

    Google Scholar 

  19. Holzmann, G.J., Smith, M.H.: Software model checking. In: Formal Methods for Protocol Engineering and Distributed Systems (FORTE), pp. 481–497 (1999)

    Google Scholar 

  20. Kahlon, V., Sankaranarayanan, S., Gupta, A.: Semantic reduction of thread interleavings in concurrent programs. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 124–138 (2009)

    Google Scholar 

  21. 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)

    Chapter  Google Scholar 

  22. Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 37–51. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  23. Lal, A., Touili, T., Kidd, N., Reps, T.W.: Interprocedural analysis of concurrent programs under a context bound. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 282–298. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  24. Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Conf. on Programming Language Design and Implementation (PLDI), pp. 446–455 (2007)

    Google Scholar 

  25. Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  26. Qadeer, S., Wu, D.: KISS: Keep it simple and sequential. In: Conf. on Programming Language Design and Implementation (PLDI), pp. 14–24 (2004)

    Google Scholar 

  27. Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 82–97. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  28. Rakamarić, Z., Hu, A.J.: A scalable memory model for low-level code. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 290–304. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  29. Schulte, W., Xia, S., Smans, J., Piessens, F.: A glimpse of a verifying C compiler (extended abstract). In: C/C++ Verification Workshop, CCV (2007)

    Google Scholar 

  30. Suwimonteerabuth, D., Esparza, J., Schwoon, S.: Symbolic context-bounded analysis of multithreaded Java programs. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 270–287. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  31. Torre, S.L., 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)

    Chapter  Google Scholar 

  32. Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering 10(2), 203–232 (2003)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Critical Systems Labs, Vancouver, BC, Canada

    Naghmeh Ghafari

  2. Department of Computer Science, University of British Columbia, Canada

    Alan J. Hu & Zvonimir Rakamarić

Authors
  1. Naghmeh Ghafari
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alan J. Hu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zvonimir Rakamarić
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Formal Methods and Tools, Department of Computer Science, University of Twente, P.O. Box 217, 7500AE, Enschede, The Netherlands

    Jaco van de Pol  & Michael Weber  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ghafari, N., Hu, A.J., Rakamarić, Z. (2010). Context-Bounded Translations for Concurrent Software: An Empirical Evaluation. In: van de Pol, J., Weber, M. (eds) Model Checking Software. SPIN 2010. Lecture Notes in Computer Science, vol 6349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16164-3_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16164-3_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16163-6

  • Online ISBN: 978-3-642-16164-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation