Advertisement

Reducing Context-Bounded Concurrent Reachability to Sequential Reachability

  • Salvatore La Torre
  • P. Madhusudan
  • Gennaro Parlato
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)

Abstract

We give a translation from concurrent programs to sequential programs that reduces the context-bounded reachability problem in the concurrent program to a reachability problem in the sequential one. The translation has two salient features: (a) the sequential program tracks, at any time, the local state of only one thread (though it does track multiple copies of shared variables), and (b) all reachable states of the sequential program correspond to reachable states of the concurrent program.

We also implement our transformation in the setting of concurrent recursive programs with finite data domains, and show that the resulting sequential program can be model-checked efficiently using existing recursive sequential program reachability tools.

Keywords

Shared Variable Component Program Reachable State Sequential Program Concurrent Program 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Bouajjani, A., Fratani, S., Qadeer, S.: Context-bounded analysis of multithreaded programs with dynamic linked structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 207–220. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    La Torre, S., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 299–314. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  4. 4.
    La Torre, S., Madhusudan, P., Parlato, G.: Analyzing recursive programs using a fixed-point calculus. In: PLDI (2009)Google Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Musuvathi, M., Qadeer, S.: Chess: Systematic stress testing of concurrent software. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 15–16. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  9. 9.
    Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI, pp. 446–455. ACM, New York (2007)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    Qadeer, S., Wu, D.: Kiss: keep it simple and sequential. In: PLDI, pp. 14–24. ACM, New York (2004)Google Scholar
  12. 12.
    Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416–430 (2000)CrossRefGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Salvatore La Torre
    • 1
  • P. Madhusudan
    • 2
  • Gennaro Parlato
    • 1
    • 2
  1. 1.Università degli Studi di SalernoItaly
  2. 2.University of Illinois at Urbana-ChampaignUSA

Personalised recommendations