nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems

verfasst von : Roderick Bloem, Nicolas Braud-Santoni, Swen Jacobs

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Fault-tolerant distributed algorithms play an increasingly important role in many applications, and their correct and efficient implementation is notoriously difficult. We present an automatic approach to synthesise provably correct fault-tolerant distributed algorithms from formal specifications in linear-time temporal logic. The supported system model covers synchronous reactive systems with finite local state, while the failure model includes strong self-stabilisation as well as Byzantine failures. The synthesis approach for a fixed-size network of processes is complete for realisable specifications, and can optimise the solution for small implementations and short stabilisation time. To solve the bounded synthesis problem with Byzantine failures more efficiently, we design an incremental, CEGIS-like loop. Finally, we define two classes of problems for which our synthesis algorithm obtains solutions that are not only correct in fixed-size networks, but in networks of arbitrary size.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Fast, Flexible, and Minimal CTL Synthesis via SMT

Nächstes Kapitel A Decision Procedure for Sets, Binary Relations and Partial Functions

Related to this are also approaches for the synthesis of robust systems [6], essentially modelling failures in the environment of a single process.

Essentially, this is because our model is not probabilistic, and because the protocol must work for any choice of Byzantine nodes and any behaviour they can exhibit, which includes all possible behaviours of an adaptive adversary.

Also, note that fail-stop failures can be seen as a special case of Byzantine failures, and can be modelled in a similar way: instead of giving arbitrary outputs, the chosen nodes at some point move into a special stop state, from which they cannot recover.

In fact, in our prototype implementation we use a heuristic that avoids throwing away the formula by re-assigning the value of \(\hat{x}\) in the formula whenever the outer SMT call returns a new value. Then, we do not throw away the formula at all, but risk that it grows unnecessarily large. In our experiments, this has shown favourable effects.

This is an extension of the argument for proving the exact number of Byzantine failures that can be survived while solving consensus problems [38].

It is not sufficient to prove that k-set agreement is not expressible in FO. However, k-set agreement – for any given \(k\ge 2\) – can easily be proven non-local by contradiction.

Alur, R., Bodik, R., Juniwal, G., Martin, M.M., Raghothaman, M., Seshia, S., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design (FMCAD), 2013, pp. 1–8. IEEE (2013)
Aminof, B., Jacobs, S., Khalimov, A., Rubin, S.: Parameterized model checking of token-passing systems. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 262–281. Springer, Heidelberg (2014). http://doai.io/10.1007/978-3-642-54013-4_15 View Article
Außerlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. In: Jobstmann, B., et al. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 476–494. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49122-5_23 View Article
Babiak, T., Křetínský, M., Řehák, V., Strejček, J.: LTL to Büchi automata translation: fast and more deterministic. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 95–109. Springer, Heidelberg (2012). http://doai.io/10.1007/978-3-642-28756-5_8 View Article
Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)View Article
Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T., Hofferek, G., Jobstmann, B., Könighofer, B., Könighofer, R.: Synthesizing robust systems. Acta Informatica 51(3), 193–220 (2014). http://doai.io/10.1007/s00236-013-0191-5 MathSciNetView ArticleMATH
Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2015). http://doai.io/10.2200/S00658ED1V01Y201508DCT013
Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911–938 (2012). http://doai.io/10.1016/j.jcss.2011.08.007 MathSciNetView ArticleMATH
Bollig, B.: Logic for communicating automata with parameterized topology. In: CSL-LICS, pp. 18:1–18:10. ACM (2014)
Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011). http://doai.io/10.1007/978-3-642-18275-4_7 View Article
Canetti, R., Damgrd, I., Dziembowski, S., Ishai, Y., Malkin, T.: On adaptive vs. non-adaptive security of multiparty protocols. In: Pfitzmann, B. (ed.) EUROCRYPT 2001. LNCS, vol. 2045, pp. 262–279. Springer, Heidelberg (2001)View Article
Černý, P., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Tarrach, T.: Efficient synthesis for concurrency by semantics-preserving transformations. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 951–967. Springer, Heidelberg (2013). http://doai.io/10.1007/978-3-642-39799-8_68 View Article
Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643–644 (1974)View ArticleMATH
Dimitrova, R., Finkbeiner, B.: Synthesis of fault-tolerant distributed systems. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 321–336. Springer, Heidelberg (2009). http://doai.io/10.1007/978-3-642-04761-9_24 View Article
Dolev, D., Korhonen, J.H., Lenzen, C., Rybicki, J., Suomela, J.: Synchronous counting and computational algorithm design. In: Higashino, T., Katayama, Y., Masuzawa, T., Potop-Butucaru, M., Yamashita, M. (eds.) SSS 2013. LNCS, vol. 8255, pp. 237–250. Springer, Heidelberg (2013). http://doai.io/10.1007/978-3-319-03089-0_17 View Article
Dolev, S.: Self-Stabilization. MIT Press, Cambridge (2000)MATH
Dolev, S., Welch, J.L.: Self-stabilizing clock synchronization in the presence of Byzantine faults. J. ACM (JACM) 51(5), 780–799 (2004)MathSciNetView ArticleMATH
Dragoi, C., Henzinger, T.A., Zufferey, D.: PSync: a partially synchronous language for fault-tolerant distributed algorithms. In: POPL, pp. 400–415. ACM (2016). http://doai.io/10.1145/2837614.2837650
Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527–550 (2003). http://doai.io/10.1142/S0129054103001881 MathSciNetView ArticleMATH
Emerson, E., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol. 1831, pp. 236–254. Springer, Berlin Heidelberg (2000)View Article
Faghih, F., Bonakdarpour, B.: SMT-based synthesis of distributed self-stabilizing systems. TAAS 10(3), 21 (2015). http://doai.io/10.1145/2767133 View Article
Finkbeiner, B., Jacobs, S.: Lazy synthesis. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 219–234. Springer, Heidelberg (2012)View Article
Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: (LICS 2005), pp. 321–330. IEEE Computer Society (2005). http://doai.io/10.1109/LICS.2005.53
Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5–6), 519–539 (2013). http://doai.io/10.1007/s10009-012-0228-z View ArticleMATH
Fischer, M.J., Lynch, N.A., Paterson, M.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374–382 (1985). http://doai.io/10.1145/3149.214121 MathSciNetView ArticleMATH
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004). http://doai.io/10.1007/978-3-540-27813-9_14 View Article
German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992)MathSciNetView ArticleMATH
Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving practical distributed systems correct. In: SOSP, pp. 1–17. ACM (2015)
Jacobs, S.: Incremental instance generation in local reasoning. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 368–382. Springer, Heidelberg (2009)View Article
Jacobs, S., Bloem, R.: Parameterized synthesis. Log. Methods Comput. Sci. 10, 1–29 (2014). http://arxiv.org/abs/1401.3588
Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114–128. Springer, Heidelberg (2012)View Article
Khalimov, A., Jacobs, S., Bloem, R.: PARTY parameterized synthesis of token rings. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 928–933. Springer, Heidelberg (2013)View Article
Khalimov, A., Jacobs, S., Bloem, R.: Towards efficient parameterized synthesis. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 108–127. Springer, Heidelberg (2013)View Article
Köksal, A.S., Pu, Y., Srivastava, S., Bodík, R., Fisher, J., Piterman, N.: Synthesis of biological models from mutation experiments. In: POPL, pp. 469–482. ACM (2013)
Konnov, I., Veith, H., Widder, J.: SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 85–102. Springer, Heidelberg (2015). http://doai.io/10.1007/978-3-319-21690-4_6 View Article
Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Functional synthesis for linear arithmetic and sets. STTT 15(5–6), 455–474 (2013). http://doai.io/10.1007/s10009-011-0217-7 View Article
Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS 2005, pp. 531–542. IEEE Computer Society (2005). http://doai.io/10.1109/SFCS.2005.66
Lamport, L., Shostak, R., Pease, M.: The Byzantine generals problem. ACM Trans. Program. Lang. Syst. 4(3), 382–401 (1982). http://doai.io/10.1145/357172.357176 View ArticleMATH
Lamport, L.: Brief announcement: leaderless Byzantine paxos. In: Peleg, D. (ed.) Distributed Computing. LNCS, vol. 6950, pp. 141–142. Springer, Heidelberg (2011)View Article
McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 250–264. Springer, Heidelberg (2002). http://doai.io/10.1007/3-540-45657-0_19 View Article
de Moura, L., Bjørner, N.S.: Efficient e-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183–198. Springer, Heidelberg (2007)View Article
de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). http://doai.io/10.1007/978-3-540-78800-3_24 View Article
Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. J. ACM 27(2), 228–234 (1980)MathSciNetView ArticleMATH
Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: 2013 IEEE 54th Annual Symposium on Foundations of Computer Science 1990, vol. 2, pp. 746–757 (1990)
Qadir, J., Hasan, O.: Applying formal methods to networking: Theory, techniques and applications. CoRR abs/1311.4303 (2013). http://arxiv.org/abs/1311.4303
Saissi, H., Bokor, P., Muftuoglu, C.A., Suri, N., Serafini, M.: Efficient verification of distributed protocols using stateful model checking. In: SRDS, pp. 133–142. IEEE (2013). http://doai.io/10.1109/SRDS.2013.22
Saks, M.E., Zaharoglou, F.: Wait-free k-set agreement is impossible: the topology of public knowledge. SIAM J. Comput. 29(5), 1449–1483 (2000). http://doai.io/10.1137/S0097539796307698 MathSciNetView ArticleMATH
Schewe, S.: Distributed synthesis is simply undecidable. Inf. Process. Lett. 114(4), 203–207 (2014). http://doai.io/10.1016/j.ipl.2013.11.012 MathSciNetView ArticleMATH
Schwentick, T., Barthelmann, K.: Local norms forms for first-order logic with applications to games and automata. In: Meinel, C., Morvan, M. (eds.) STACS 1998. LNCS, vol. 1373, pp. 444–454. Springer, Heidelberg (1998)View Article
Sickert, S.: Converting linear temporal logic to deterministic (generalised) rabin automata. Archive of Formal Proofs 2015 (2015)
Solar Lezama, A.: Program synthesis by sketching. Ph.D. thesis, EECS Department, University of California, Berkeley (2008). http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-177.html
Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS 2006, pp. 404–415. ACM (2006). http://doai.io/10.1145/1168857.1168907
Tixeuil, S.: Self-stabilizing algorithms. In: Algorithms and Theory of Computation Handbook. Applied Algorithms and Data Structures, 2nd edn, pp. 26.1–26.45. Chapman & Hall/CRC, CRC Press, Taylor & Francis Group (2009)
Vechev, M., Yahav, E., Yorsh, G.: Inferring synchronization under limited observability. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 139–154. Springer, Heidelberg (2009). http://doai.io/10.1007/978-3-642-00768-2_13 View Article

Titel: Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems
verfasst von: Roderick Bloem
Nicolas Braud-Santoni
Swen Jacobs
Verlag: Springer International Publishing
Buch: Computer Aided Verification
Print ISBN: 978-3-319-41527-7

Electronic ISBN: 978-3-319-41528-4

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-41528-4_9

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner