Document Open Access Logo

Distributed Controller Synthesis for Deadlock Avoidance

Authors Hugo Gimbert, Corto Mascle, Anca Muscholl, Igor Walukiewicz

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2022.125.pdf
  • Filesize: 0.7 MB
  • 20 pages

Document Identifiers

Author Details

Hugo Gimbert
  • Université de Bordeaux, CNRS, France
Corto Mascle
  • Université de Bordeaux, France
Anca Muscholl
  • Université de Bordeaux, France
Igor Walukiewicz
  • Université de Bordeaux, CNRS, France

Funding

Work partially funded by ANR project FREDDA (ANR-17-CE40-0013).

Cite AsGet BibTex

Hugo Gimbert, Corto Mascle, Anca Muscholl, and Igor Walukiewicz. Distributed Controller Synthesis for Deadlock Avoidance. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 125:1-125:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ICALP.2022.125

Abstract

We consider the distributed control synthesis problem for systems with locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction this problem is undecidable even for three processes each using a fixed number of locks. We propose two restrictions that make distributed control decidable. The first one is to allow each process to use at most two locks. The problem then becomes complete for the second level of the polynomial time hierarchy, and even in Ptime under some additional assumptions. The dining philosophers problem satisfies these assumptions. The second restriction is a nested usage of locks. In this case the synthesis problem is Nexptime-complete. The drinking philosophers problem falls in this case.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
Keywords
  • Distributed Synthesis
  • Concurrency
  • Lock Synchronisation
  • Deadlock Avoidance

Metrics

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

Related Versions

References

  1. A. Arnold and I. Walukiewicz. Nondeterministic controllers of nondeterministic processes. In J. Flum, E. Grädel, and T. Wilke, editors, Logic and Automata, volume 2 of Texts in Logic and Games, pages 29-52. Amsterdam University Press, 2007. Google Scholar
  2. B. Bérard, B. Bollig, P. Bouyer, M. Függer, and N. Sznajder. Synthesis in presence of dynamic links. In J-F. Raskin and D. Bresolin, editors, Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, volume 326 of EPTCS, pages 33-49, 2020. To appear in Information and Computation. URL: https://doi.org/10.4204/EPTCS.326.3.
  3. R. Beutner, B. Finkbeiner, and J. Hecking-Harbusch. Translating asynchronous games for distributed synthesis. In W. J. Fokkink and R. van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, volume 140 of LIPIcs, pages 26:1-26:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.26.
  4. K. M. Chandy and J. Misra. The drinking philosophers problem. ACM Trans. Program. Lang. Syst., 6(4):632-646, October 1984. URL: https://doi.org/10.1145/1780.1804.
  5. A. Church. Applications of recursive arithmetic to the problem of cricuit synthesis. In Summaries of the Summer Institute of Symbolic Logic, volume I, pages 3-50. Cornell Univ., Ithaca, N.Y., 1957. Google Scholar
  6. E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52-71. Springer Verlag, 1981. Google Scholar
  7. M. D. Ernst, A. Lovato, D. Macedonio, F. Spoto, and J. Thaine. Locking discipline inference and checking. In L. K. Dillon, W. Visser, and L. A. Williams, editors, Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, pages 1133-1144. ACM, 2016. URL: https://doi.org/10.1145/2884781.2884882.
  8. B. Finkbeiner. Bounded synthesis for Petri games. In R. Meyer, A. Platzer, and H. Wehrheim, editors, Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday. Proceedings, volume 9360 of Lecture Notes in Computer Science, pages 223-237. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23506-6_15.
  9. B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, and E.-R. Olderog. Global winning conditions in synthesis of distributed systems with causal memory. In F. Manea and A. Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, Virtual Conference, volume 216 of LIPIcs, pages 20:1-20:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.20.
  10. B. Finkbeiner and E.-R. Olderog. Petri games: Synthesis of distributed systems with causal memory. Inf. Comput., 253:181-203, 2017. Google Scholar
  11. B. Finkbeiner and S. Schewe. Uniform distributed synthesis. In 20th IEEE Symposium on Logic in Computer Science (LICS) 2005, Proceedings, pages 321-330. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/LICS.2005.53.
  12. P. Gastin, B. Lerman, and M. Zeitoun. Distributed games with causal memory are decidable for series-parallel systems. In K. Lodaya and M. Mahajan, editors, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Proceedings, volume 3328 of Lecture Notes in Computer Science, pages 275-286. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30538-5_23.
  13. P. Gastin, N. Sznajder, and M. Zeitoun. Distributed synthesis for well-connected architectures. Formal Methods in System Design, 34(3):215-237, June 2009. Google Scholar
  14. B. Genest, H. Gimbert, A. Muscholl, and I. Walukiewicz. Asynchronous games over tree architectures. In F. V. Fomin, R. Freivalds, M. Z. Kwiatkowska, and D. Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 275-286. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_26.
  15. M. Gieseking, J. Hecking-Harbusch, and A. Yanich. A web interface for Petri nets with transits and Petri games. In J. F. Groote and K. G. 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, Proceedings, Part II, volume 12652 of Lecture Notes in Computer Science, pages 381-388. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_22.
  16. H. Gimbert. On the control of asynchronous automata. In S. V. Lokam and R. Ramanujam, editors, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, volume 93 of LIPIcs, pages 30:1-30:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2017.30.
  17. H. Gimbert. Distributed asynchronous games with causal memory are undecidable. CoRR, abs/2110.14768, 2021. Submitted. URL: http://arxiv.org/abs/2110.14768.
  18. J. Hecking-Harbusch and N. O. Metzger. Efficient trace encodings of bounded synthesis for asynchronous distributed systems. In Y. F. Chen, C. H. Cheng, and J. Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science, pages 369-386. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_22.
  19. V. Kahlon and A. Gupta. An automata-theoretic approach for model checking threads for LTL properties. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), Proceedings, pages 101-110. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.11.
  20. O. Kupferman and M. Y. Vardi. Synthesizing distributed systems. In 16th Annual IEEE Symposium on Logic in Computer Science, Proceedings, pages 389-398. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/LICS.2001.932514.
  21. D. Lehmann and M. O. Rabin. On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem. In J. White, R. J. Lipton, and P. C. Goldberg, editors, Conference Record of the Eighth Annual ACM Symposium on Principles of Programming Languages, pages 133-138. ACM Press, 1981. URL: https://doi.org/10.1145/567532.567547.
  22. N. A. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996. Google Scholar
  23. P. Madhusudan and P. S. Thiagarajan. Distributed controller synthesis for local specifications. In F. Orejas, P. G. Spirakis, and J. van Leeuwen, editors, Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Proceedings, volume 2076 of Lecture Notes in Computer Science, pages 396-407. Springer, 2001. URL: https://doi.org/10.1007/3-540-48224-5_33.
  24. P. Madhusudan, P. S. Thiagarajan, and S. Yang. The MSO theory of connectedly communicating processes. In R. Ramanujam and S. Sen, editors, FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, volume 3821 of Lecture Notes in Computer Science, pages 201-212. Springer, 2005. URL: https://doi.org/10.1007/11590156_16.
  25. A. Muscholl and I. Walukiewicz. Distributed synthesis for acyclic architectures. In V. Raman and S. P. Suresh, editors, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, volume 29 of LIPIcs, pages 639-651. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2014.639.
  26. G. L. Peterson and J. H. Reif. Multiple-person alternation. In 20th Annual Symposium on Foundations of Computer Science, pages 348-363. IEEE Computer Society, 1979. URL: https://doi.org/10.1109/SFCS.1979.25.
  27. A. Pnueli and R. Rosner. Distributed reactive systems are hard to synthesize. In 31st Annual Symposium on Foundations of Computer Science, pages 746-757. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/FSCS.1990.89597.
  28. P. J.G. Ramadge and W. M. Wonham. The control of discrete event systems. Proceedings of the IEEE, 77(2):81-98, 1989. Google Scholar
  29. K. Rudie and W. M. Wonham. Think globally, act locally: Decentralized supervisory control. IEEE Trans. on Automat. Control, 37(11):1692-1708, 1992. Google Scholar
  30. J. G. Thistle. Undecidability in decentralized supervision. Systems & Control Letters, 54(5):503-509, 2005. URL: https://doi.org/10.1016/j.sysconle.2004.10.002.
  31. S. Tripakis. Undecidable problems in decentralized observation and control for regular languages. Information Processing Letters, 90(1):21-28, 2004. Google Scholar
  32. I. Walukiewicz. Synthesis with finite automata. In J.-É. Pin, editor, Handbook of Automata Theory, pages 1217-1260. European Mathematical Society Publishing House, Zürich, Switzerland, 2021. URL: https://doi.org/10.4171/Automata-2/11.
  33. Y. Wang, S. Lafortune, T. Kelly, M. Kudlur, and S. A. Mahlke. The theory of deadlock avoidance via discrete control. In Z. Shao and B. C. Pierce, editors, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pages 252-263. ACM, 2009. URL: https://doi.org/10.1145/1480881.1480913.
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