Advertisement

Towards Synthesis of Distributed Algorithms with SMT Solvers

  • Carole Delporte-Gallet
  • Hugues Fauconnier
  • Yan Jurski
  • François Laroussinie
  • Arnaud SangnierEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11704)

Abstract

We consider the problem of synthesizing distributed algorithms working on a specific execution context. We show it is possible to use the linear time temporal logic in order to both specify the correctness of algorithms and their execution contexts. We then provide a method allowing to reduce the synthesis problem of finite state algorithms to some model-checking problems. We finally apply our technique to automatically generate algorithms for consensus and epsilon-agreement in the case of two processes using the SMT solver Z3.

References

  1. 1.
    Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7–34 (2001)CrossRefGoogle Scholar
  2. 2.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982).  https://doi.org/10.1007/BFb0025774CrossRefGoogle Scholar
  3. 3.
    Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA + Proofs. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 147–154. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-32759-9_14CrossRefGoogle Scholar
  4. 4.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  5. 5.
    Emerson, E.A.: Temporal and modal logic. In: Leeuwen, J.V. (ed.) Handbook of Theoretical Computer Science, vol. B, Chapter 16, pp. 995–1072. Elsevier (1990)Google Scholar
  6. 6.
    Fischer, M.J., Lynch, N.A., Paterson, M.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374–382 (1985)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]. LNCS, vol. 2500. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-36387-4CrossRefGoogle Scholar
  8. 8.
    Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst. 13(1), 124–149 (1991)CrossRefGoogle Scholar
  9. 9.
    Herlihy, M., Luchangco, V., Moir, M.: Obstruction-free synchronization: double-ended queues as an example. In: ICDCS 2003, pp. 522–529 (2003)Google Scholar
  10. 10.
    Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, Burlington (2008)Google Scholar
  11. 11.
    Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)Google Scholar
  12. 12.
    Lazic, M., Konnov, I., Widder, J., Bloem, R.: Synthesis of distributed algorithms with parameterized threshold guards. In: OPODIS 2017, vol. 95. LIPIcs, pp. 32:1–32:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)Google Scholar
  13. 13.
    Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS 1977), pp. 46–57. IEEE Computer Society Press, October–November 1977Google Scholar
  14. 14.
    Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982).  https://doi.org/10.1007/3-540-11494-7_22CrossRefGoogle Scholar
  15. 15.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS 1986, pp. 332–344. IEEE Computer Society (1986)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Carole Delporte-Gallet
    • 1
  • Hugues Fauconnier
    • 1
  • Yan Jurski
    • 1
  • François Laroussinie
    • 1
  • Arnaud Sangnier
    • 1
    Email author
  1. 1.IRIF, Univ Paris Diderot, CNRSParisFrance

Personalised recommendations