Document Open Access Logo

Checking Refinement of Asynchronous Programs Against Context-Free Specifications

Authors Pascal Baumann , Moses Ganardi , Rupak Majumdar , Ramanathan S. Thinniyam , Georg Zetzsche

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2023.110.pdf
  • Filesize: 0.92 MB
  • 20 pages

Document Identifiers

Author Details

Pascal Baumann
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Moses Ganardi
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Rupak Majumdar
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Ramanathan S. Thinniyam
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Georg Zetzsche
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

Funding

Funded by the European Union (ERC, FINABIS, 101077902). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council Executive Agency. Neither the European Union nor the granting authority can be held responsible for them. Partially funded by the DFG project 389792660 TRR 248-CPEC.

Cite AsGet BibTex

Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. Checking Refinement of Asynchronous Programs Against Context-Free Specifications. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 110:1-110:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ICALP.2023.110

Abstract

In the language-theoretic approach to refinement verification, we check that the language of traces of an implementation all belong to the language of a specification. We consider the refinement verification problem for asynchronous programs against specifications given by a Dyck language. We show that this problem is EXPSPACE-complete - the same complexity as that of language emptiness and for refinement verification against a regular specification. Our algorithm uses several technical ingredients. First, we show that checking if the coverability language of a succinctly described vector addition system with states (VASS) is contained in a Dyck language is EXPSPACE-complete. Second, in the more technical part of the proof, we define an ordering on words and show a downward closure construction that allows replacing the (context-free) language of each task in an asynchronous program by a regular language. Unlike downward closure operations usually considered in infinite-state verification, our ordering is not a well-quasi-ordering, and we have to construct the regular language ab initio. Once the tasks can be replaced, we show a reduction to an appropriate VASS and use our first ingredient. In addition to the inherent theoretical interest, refinement verification with Dyck specifications captures common practical resource usage patterns based on reference counting, for which few algorithmic techniques were known.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Software and its engineering → Software verification
Keywords
  • Asynchronous programs
  • VASS
  • Dyck languages
  • Language inclusion
  • Refinement verification

Metrics

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

Related Versions

References

  1. Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. Context-bounded verification of context-free specifications. Proc. ACM Program. Lang., 7(POPL):2141-2170, 2023. URL: https://doi.org/10.1145/3571266.
  2. Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. Context-bounded verification of thread pools. Proc. ACM Program. Lang., 6(POPL):1-28, 2022. URL: https://doi.org/10.1145/3498678.
  3. I. Borosh and L. B. Treybig. Bounds on positive integral solutions of linear diophantine equations. Proceedings of the American Mathematical Society, 55(2):299-304, 1976. Google Scholar
  4. Laura Bozzelli and Pierre Ganty. Complexity analysis of the backward coverability algorithm for VASS. In Giorgio Delzanno and Igor Potapov, editors, Reachability Problems - 5th International Workshop, RP 2011, Genoa, Italy, September 28-30, 2011. Proceedings, volume 6945 of Lecture Notes in Computer Science, pages 96-109. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24288-5_10.
  5. Bruno Courcelle. On constructing obstruction sets of words. Bulletin of the EATCS, 44:178-186, 1991. Google Scholar
  6. Wojciech Czerwinski and Piotr Hofman. Language inclusion for boundedly-ambiguous vector addition systems is decidable. In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, volume 243 of LIPIcs, pages 16:1-16:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.16.
  7. Wojciech Czerwiński and Łukasz Orlikowski. Reachability in vector addition systems is Ackermann-complete. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229-1240. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  8. Ankush Desai, Pranav Garg, and P. Madhusudan. Natural proofs for asynchronous programs using almost-synchronous reductions. In Andrew P. Black and Todd D. Millstein, editors, Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014, pages 709-725. ACM, 2014. URL: https://doi.org/10.1145/2660193.2660211.
  9. Ankush Desai and Shaz Qadeer. P: modular and safe asynchronous programming. In Shuvendu K. Lahiri and Giles Reger, editors, Runtime Verification - 17th International Conference, RV 2017, Seattle, WA, USA, September 13-16, 2017, Proceedings, volume 10548 of Lecture Notes in Computer Science, pages 3-7. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-67531-2_1.
  10. Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 34(1):6, 2012. URL: https://doi.org/10.1145/2160910.2160915.
  11. Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, and Viktor Vafeiadis. Rely/guarantee reasoning for asynchronous programs. 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 483-496. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2015.483.
  12. Jean Goubault-Larrecq, Simon Halfon, P. Karandikar, K. Narayan Kumar, and Philippe Schnoebelen. The ideal approach to computing closed subsets in well-quasi-orderings. In Peter M. Schuster, Monika Seisenberger, and Andreas Weiermann, editors, Well-Quasi Orders in Computation, Logic, Language and Reasoning, volume 53 of Trends In Logic, pages 55-105. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-30229-0_3.
  13. Ranjit Jhala and Rupak Majumdar. Interprocedural analysis of asynchronous programs. In POPL '07: Proc. 34th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, pages 339-350. ACM Press, 2007. Google Scholar
  14. Dexter Kozen. Automata and computability. Undergraduate texts in computer science. Springer, 1997. Google Scholar
  15. Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, and Shaz Qadeer. Inductive sequentialization of asynchronous programs. In Alastair F. Donaldson and Emina Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 227-242. ACM, 2020. URL: https://doi.org/10.1145/3385412.3385980.
  16. Bernhard Kragl, Shaz Qadeer, and Thomas A. Henzinger. Synchronizing the asynchronous. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 21:1-21:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.21.
  17. Jérôme Leroux. The Reachability Problem for Petri Nets is Not Primitive Recursive. In 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS), pages 1241-1252, February 2022. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  18. Richard Lipton. The reachability problem is exponential-space hard. Yale University, Department of Computer Science, Report, 62, 1976. Google Scholar
  19. Raphaela Löbel. Linear Tree Transducers: From Equivalence to Balancedness. PhD thesis, Technical University of Munich, Germany, 2020. URL: https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20201127-1552125-1-5.
  20. Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. General decidability results for asynchronous shared-memory programs: Higher-order and beyond. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I, volume 12651 of Lecture Notes in Computer Science, pages 449-467. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72016-2_24.
  21. Shaz Qadeer and Dinghao Wu. KISS: keep it simple and sequential. In William W. 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.
  22. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223-231, 1978. Google Scholar
  23. Robert W Ritchie and Frederick N Springsteel. Language recognition by marking automata. Information and Control, 20(4):313-330, 1972. Google Scholar
  24. Walter J Savitch. Relationships between nondeterministic and deterministic tape complexities. Journal of computer and system sciences, 4(2):177-192, 1970. Google Scholar
  25. Koushik Sen and Mahesh Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. In CAV '06: Proc. 18th Int. Conf. on Computer Aided Verification, volume 4144 of LNCS, pages 300-314. Springer, 2006. Google Scholar
  26. Akihiko Tozawa and Yasuhiko Minamide. Complexity results on balanced context-free languages. In Helmut Seidl, editor, Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007, Proceedings, volume 4423 of Lecture Notes in Computer Science, pages 346-360. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71389-0_25.
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