Document Open Access Logo

Reachability in Concurrent Uninterpreted Programs

Authors Salvatore La Torre, Madhusudan Parthasarathy

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2019.46.pdf
  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Author Details

Salvatore La Torre
  • Università degli Studi di Salerno, Italia
Madhusudan Parthasarathy
  • University of Illinois, Urbana-Champaign, USA

Acknowledgements

This material is based upon work supported by the National Science Foundation under Grant CCF-1527395, GNCS 2019 grant and MIUR-FARB 2018-19 grant.

Cite AsGet BibTex

Salvatore La Torre and Madhusudan Parthasarathy. Reachability in Concurrent Uninterpreted Programs. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 46:1-46:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSTTCS.2019.46

Abstract

We study the safety verification (reachability problem) for concurrent programs with uninterpreted functions/relations. By extending the notion of coherence, recently identified for sequential programs, to concurrent programs, we show that reachability in coherent concurrent programs under various scheduling restrictions is decidable by a reduction to multistack pushdown automata, and establish precise complexity bounds for them. We also prove that the coherence restriction for these various scheduling restrictions is itself a decidable property.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Formal languages and automata theory
  • Software and its engineering → Formal software verification
Keywords
  • Verification
  • uninterpreted programs
  • concurrent programs
  • shared memory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Aziz Abdulla, C. Aiswarya, and Mohamed Faouzi Atig. Data Multi-Pushdown Automata. In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 38:1-38:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.38.
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine, and Jari Stenman. Budget-bounded model-checking pushdown systems. Formal Methods in System Design, 45(2):273-301, 2014. URL: https://doi.org/10.1007/s10703-014-0207-y.
  3. Rajeev Alur and P. Madhusudan. Adding nesting structure to words. J. ACM, 56(3):16:1-16:43, 2009. URL: https://doi.org/10.1145/1516512.1516518.
  4. Mohamed Faouzi Atig, Benedikt Bollig, and Peter Habermehl. Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete. Int. J. Found. Comput. Sci., 28(8):945-976, 2017. URL: https://doi.org/10.1142/S0129054117500332.
  5. Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads. Logical Methods in Computer Science, 7(4), 2011. URL: https://doi.org/10.2168/LMCS-7(4:4)2011.
  6. Mikolaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27:1-27:26, 2011. URL: https://doi.org/10.1145/1970398.1970403.
  7. Mikolaj Bojańczyk, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data trees and XML reasoning. J. ACM, 56(3):13:1-13:48, 2009. URL: https://doi.org/10.1145/1516512.1516515.
  8. Benedikt Bollig, Aiswarya Cyriac, Paul Gastin, and K. Narayan Kumar. Model Checking Languages of Data Words. In Lars Birkedal, editor, Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7213 of Lecture Notes in Computer Science, pages 391-405. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28729-9_26.
  9. Ahmed Bouajjani, Michael Emmi, and Gennaro Parlato. On Sequentializing Concurrent Programs. In Eran Yahav, editor, Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings, volume 6887 of Lecture Notes in Computer Science, pages 129-145. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23702-7_13.
  10. Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag, Berlin, Heidelberg, 2007. Google Scholar
  11. Luca Breveglieri, Alessandra Cherubini, Claudio Citrini, and Stefano Crespi-Reghizzi. Multi-Push-Down Languages and Grammars. Int. J. Found. Comput. Sci., 7(3):253-292, 1996. URL: https://doi.org/10.1142/S0129054196000191.
  12. Denis Bueno and Karem A. Sakallah. euforia: Complete Software Model Checking with Uninterpreted Functions. In Constantin Enea and Ruzica Piskac, editors, Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings, volume 11388 of Lecture Notes in Computer Science, pages 363-385. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-11245-5_17.
  13. Aiswarya Cyriac, Paul Gastin, and K. Narayan Kumar. MSO decidability of multi-pushdown systems via split-width. In Maciej Koutny and Irek Ulidowski, editors, CONCUR 2012 - Concurrency Theory - 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings, volume 7454 of Lecture Notes in Computer Science, pages 547-561. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32940-1_38.
  14. Claire David, Leonid Libkin, and Tony Tan. On the Satisfiability of Two-Variable Logic over Data Words. In Christian G. Fermüller and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, volume 6397 of Lecture Notes in Computer Science, pages 248-262. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-16242-8_18.
  15. Martin Davis. Kurt Gödel. Über Die Vollständigkeit des Logikkalküls . Collected Works, Volume I, Publications 1929-1936, by Kurt Gödel, Edited by Solomon Feferman, John W. Dawson Jr., Stephen C. Kleene, Gregory H. Moore, Robert M. Solovay, and Jean van Heijenoort, Clarendon Press, Oxford University Press, New York and Oxford, 1986, Even Pp. 60- 100. - Kurt Gödel. On the Completeness of the Calculus of Logic . English Translation by Stefan Bauer-Mengelberg and Jean van Heijenoort of the Preceding. Journal of Symbolic Logic, 55(1):341-342, 1990. URL: https://doi.org/10.2307/2274974.
  16. Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, and Rupak Majumdar. Model checking parameterized asynchronous shared-memory systems. Formal Methods in System Design, 50(2-3):140-167, 2017. URL: https://doi.org/10.1007/s10703-016-0258-3.
  17. Michael Emmi, Shaz Qadeer, and Zvonimir Rakamaric. Delay-bounded scheduling. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 411-422. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926432.
  18. Sumit Gulwani and Ashish Tiwari. Assertion Checking Unified. In Byron Cook and Andreas Podelski, editors, Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings, volume 4349 of Lecture Notes in Computer Science, pages 363-377. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-69738-1_26.
  19. Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 585-602. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_39.
  20. Salvatore La Torre, P. Madhusudan, and Gennaro Parlato. A Robust Class of Context-Sensitive Languages. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 161-170. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.9.
  21. Salvatore La Torre, P. Madhusudan, and Gennaro Parlato. Model-Checking Parameterized Concurrent Programs Using Linear Interfaces. In Tayssir Touili, Byron Cook, and Paul B. Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, pages 629-644. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14295-6_54.
  22. Salvatore La Torre, Anca Muscholl, and Igor Walukiewicz. Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable. In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 72-84. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2015.72.
  23. Salvatore La Torre, Margherita Napoli, and Gennaro Parlato. A Unifying Approach for Multistack Pushdown Automata. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, volume 8634 of Lecture Notes in Computer Science, pages 377-389. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44522-8_32.
  24. Salvatore La Torre, Margherita Napoli, and Gennaro Parlato. Scope-Bounded Pushdown Languages. Int. J. Found. Comput. Sci., 27(2):215-234, 2016. URL: https://doi.org/10.1142/S0129054116400074.
  25. Akash Lal and Thomas W. Reps. Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design, 35(1):73-97, 2009. URL: https://doi.org/10.1007/s10703-009-0078-9.
  26. P. Madhusudan and Gennaro Parlato. The tree width of auxiliary storage. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 283-294. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926419.
  27. Umang Mathur, P. Madhusudan, and Mahesh Viswanathan. Decidable verification of uninterpreted programs. PACMPL, 3(POPL):46:1-46:29, 2019. URL: https://dl.acm.org/citation.cfm?id=3290359, URL: https://doi.org/10.1145/3290359.
  28. Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, and Mahesh Viswanathan. Deciding Memory Safety for Forest Datastructures. CoRR, abs/1907.00298, 2019. URL: http://arxiv.org/abs/1907.00298.
  29. Andrzej S. Murawski, Steven J. Ramsay, and Nikos Tzevelekos. Reachability in pushdown register automata. J. Comput. Syst. Sci., 87:58-83, 2017. URL: https://doi.org/10.1016/j.jcss.2017.02.008.
  30. Shaz Qadeer and Jakob Rehof. Context-Bounded Model Checking of Concurrent Software. In Nicolas Halbwachs and Lenore D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3440 of Lecture Notes in Computer Science, pages 93-107. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-31980-1_7.
  31. Shaz Qadeer and Dinghao Wu. KISS: keep it simple and sequential. In William Pugh and Craig Chambers, editors, Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, Washington, DC, USA, June 9-11, 2004, pages 14-24. ACM, 2004. URL: https://doi.org/10.1145/996841.996845.
  32. Nikos Tzevelekos. Fresh-register automata. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 295-306. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926420.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact