Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Automated Technology for Verification and Analysis

ATVA 2012: Automated Technology for Verification and Analysis pp 152–166Cite as

Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7561))

Abstract

We address the model checking problem of omega-regular linear-time properties for shared memory concurrent programs modeled as multi-pushdown systems. We consider here boolean programs with a finite number of threads and recursive procedures. It is well-known that the model checking problem is undecidable for this class of programs. In this paper, we investigate the decidability and the complexity of this problem under the assumption of scope-boundedness defined recently by La Torre and Napoli in [24]. A computation is scope-bounded if each pair of call and return events of a procedure executed by some thread must be separated by a bounded number of context-switches of that thread. The concept of scope-bounding generalizes the one of context-bounding [31] since it allows an unbounded number of context switches. Moreover, while context-bounding is adequate for reasoning about safety properties, scope-bounding is more suitable for reasoning about liveness properties that must be checked over infinite computations. It has been shown in [24] that the reachability problem for multi-pushdown systems under scope-bounding is PSPACE-complete. We prove in this paper that model-checking linear-time properties under scope-bounding is also decidable and is EXPTIME-complete.

Partially supported by the Swedish Research Council within UPMARC, CNRS LIA InForMel, and the project ANR-09-SEGI-016 Veridyc.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Etessami, K., Madhusudan, P.: A Temporal Logic of Nested Calls and Returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467–481. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Atig, M.F., Bollig, B., Habermehl, P.: Emptiness of Multi-pushdown Automata Is 2ETIME-Complete. In: Ito, M., Toyama, M. (eds.) DLT 2008. LNCS, vol. 5257, pp. 121–133. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Atig, M.F., Bouajjani, A., Qadeer, S.: Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 107–123. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  4. Atig, M.F.: From Multi to Single Stack Automata. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 117–131. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  5. Atig, M.F.: Global model checking of ordered multi-pushdown systems. In: FSTTCS. LIPIcs, vol. 8, pp. 216–227. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2010)

    Google Scholar 

  6. Atig, M.F., Bouajjani, A., Emmi, M., Lal, A.: Detecting Fair Non-termination in Multithreaded Programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 210–226. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  7. Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P.: Model checking branching-time properties of multi-pushdown systems is hard. CoRR abs/1205.6928 (2012)

    Google Scholar 

  8. Atig, M.F., Bouajjani, A., Touili, T.: Analyzing asynchronous programs with preemption. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008). LIPIcs, vol. 2, pp. 37–48. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2008)

    Google Scholar 

  9. Atig, M.F., Bouajjani, A., Touili, T.: On the Reachability Analysis of Acyclic Networks of Pushdown Systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 356–371. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  10. Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model-Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  11. Bouajjani, A., Maler, O.: Reachability analysis of pushdown automata. In: Proc. Intern. Workshop on Verification of Infinite-State Systems, Infinity 1996 (1996)

    Google Scholar 

  12. Bouajjani, A., Müller-Olm, M., Touili, T.: Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 473–487. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Bouajjani, A., Emmi, M., Parlato, G.: On Sequentializing Concurrent Programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 129–145. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. Bouajjani, A., Esparza, J., Schwoon, S., Strejček, J.: Reachability Analysis of Multithreaded Software with Asynchronous Communication. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 348–359. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  16. Breveglieri, L., Cherubini, A., Citrini, C., Crespi Reghizzi, S.: Multi-push-down languages and grammars. Intl. Journal of Foundations of Computer Science 7(3), 253–292 (1996)

    Article  MATH  Google Scholar 

  17. Emmi, M., Qadeer, S., Rakamarić, Z.: Delay-bounded scheduling. In: POPL 2011: Proc. 38th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 411–422. ACM (2011)

    Google Scholar 

  18. Ganty, P., Majumdar, R., Monmege, B.: Bounded Underapproximations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 600–614. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  19. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley (1979)

    Google Scholar 

  20. La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: Proceedings of LICS, pp. 161–170. IEEE (2007)

    Google Scholar 

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

    Chapter  Google Scholar 

  22. La Torre, S., Madhusudan, P., Parlato, G.: Model-Checking Parameterized Concurrent Programs Using Linear Interfaces. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 629–644. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  23. La Torre, S., Madhusudan, P., Parlato, G.: Analyzing recursive programs using a fixed-point calculus. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2009), pp. 211–222. ACM (2009)

    Google Scholar 

  24. La Torre, S., Napoli, M.: Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 203–218. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  25. La Torre, S., Napoli, M.: A temporal logic for multi-threaded programs. In: IFIP TCS. IFIP. Springer (to appear, 2012)

    Google Scholar 

  26. La Torre, S., Parlato, G.: Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width. Technical report, University of Southampton (March 2012)

    Google Scholar 

  27. Lal, A., Reps, T.: 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 

  28. Lange, M., Leiß, H.: To CNF or not to CNF ? An efficient yet presentable version of the CYK algorithm. Informatica Didactica 8 (2008-2010)

    Google Scholar 

  29. Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI, pp. 446–455. ACM (2007)

    Google Scholar 

  30. Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE (1977)

    Google Scholar 

  31. 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 

  32. Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416–430 (2000)

    Article  Google Scholar 

  33. Sen, K., Viswanathan, M.: Model Checking Multithreaded Programs with Asynchronous Atomic Methods. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 300–314. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  34. Vardi, M.Y.: A temporal fixpoint calculus. In: POPL, pp. 250–259 (1988)

    Google Scholar 

  35. Vardi, M.Y.: Alternating Automata and Program Verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 471–485. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  36. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, pp. 332–344. IEEE Computer Society (1986)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Uppsala University, Sweden

    Mohamed Faouzi Atig

  2. LIAFA, Université Paris Diderot, France

    Ahmed Bouajjani

  3. Chennai Mathematical Institute, India

    K. Narayan Kumar & Prakash Saivasan

Authors
  1. Mohamed Faouzi Atig
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ahmed Bouajjani
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. K. Narayan Kumar
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Prakash Saivasan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Indian Institute of Technology, Computer Science and Engineering, Dept. of Computer Science and Engineering, IIT Bombay, Powai, 400076, Mumbai, Maharashtra, India

    Supratik Chakraborty

  2. Chennai Mathematical Institute, H1, SIPCOT IT Park, Kelambakkam, 603103, Siruseri, Tamil Nadu, India

    Madhavan Mukund

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P. (2012). Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding. In: Chakraborty, S., Mukund, M. (eds) Automated Technology for Verification and Analysis. ATVA 2012. Lecture Notes in Computer Science, vol 7561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33386-6_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33385-9

  • Online ISBN: 978-3-642-33386-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation