Verification of randomized consensus algorithms under round-rigid adversaries

Abstract

Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round \(r-1\). For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or’s and Bracha’s seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.

This is a preview of subscription content, access via your institution.

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7

Notes

  1. 1.

    This restriction is needed in Sect. 7.1 and in particular to establish Lemma 11.

References

  1. 1.

    Aguilera, M., Toueg, S.: The correctness proof of Ben-Or’s randomized consensus algorithm. Distrib. Comput. 25(5), 1–11 (2012). Online first

    Article  Google Scholar 

  2. 2.

    Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. IPL 15, 307–309 (1986)

    MathSciNet  Article  Google Scholar 

  3. 3.

    Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    Google Scholar 

  4. 4.

    Ben-Or, M.: Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract). In: PODC, pp. 27–30 (1983)

  5. 5.

    Berkovits, I., Lazic, M., Losa, G., Padon, O., Shoham, S.: Verification of threshold-based distributed algorithms by decomposition to decidable logics. In: CAV Part II, pp. 245–266 (2019)

  6. 6.

    Bertrand, N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: FSTTCS, volume 24 of LIPIcs, pp. 501–513 (2013)

  7. 7.

    Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. In: CONCUR, volume 140 of LIPIcs, pp. 33:1–33:15. Schloss Dagstuhl (2019)

  8. 8.

    Bertrand, N., Lazić, M., Widder, J.: A reduction theorem for randomized distributed algorithms under weak adversaries. In: VMCAI (2021) (to appear)

  9. 9.

    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)

    Google Scholar 

  10. 10.

    Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. In: CAV, pp. 372–391 (2018)

  11. 11.

    Bracha, G.: Asynchronous Byzantine agreement protocols. Inf. Comput. 75(2), 130–143 (1987)

    MathSciNet  Article  Google Scholar 

  12. 12.

    Chaouch-Saad, M., Charron-Bost, B., Merz, S.: A reduction theorem for the verification of round-based distributed algorithms. In: RP, volume 5797 of LNCS, pp. 93–106 (2009)

  13. 13.

    Charron-Bost, B., Merz, S.: Formal verification of a consensus algorithm in the heard-of model. IJSI 3(2–3), 273–303 (2009)

    Google Scholar 

  14. 14.

    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Heidelberg (2018)

    Google Scholar 

  15. 15.

    Damian, A., Drăgoi, C., Militaru, A., Widder, J.: Communication-closed asynchronous protocols. In: CAV (2), volume 11562 of Lecture Notes in Computer Science, pp. 344–363. Springer (2019)

  16. 16.

    Drăgoi, C., Henzinger, T.A., Veith, H., Widder, J., Zufferey, D.: A logic-based framework for verifying consensus algorithms. In: VMCAI, volume 8318 of LNCS, pp. 161–181 (2014)

  17. 17.

    Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155–173 (1982)

    Article  Google Scholar 

  18. 18.

    Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL, pp. 85–94 (1995)

  19. 19.

    Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374–382 (1985)

    MathSciNet  Article  Google Scholar 

  20. 20.

    Grimmet, G.R., Strizaker, D.: Probability and Random Processes, 2nd edn. Oxford Science Publications, Oxford (1992)

    Google Scholar 

  21. 21.

    Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S., Zill, B.: Ironfleet: proving safety and liveness of practical distributed systems. Commun. ACM 60(7), 83–92 (2017)

    Article  Google Scholar 

  22. 22.

    John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Towards modeling and model checking fault-tolerant distributed algorithms. In: SPIN, volume 7976 of LNCS, pp. 209–226 (2013)

  23. 23.

    Konnov, I., Lazic, M., Veith, H., Widder, J.: Para\(^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. Formal Methods Syst. Des. 51(2), 270–307 (2017)

    Article  Google Scholar 

  24. 24.

    Konnov, I., Lazić, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: POPL, pp. 719–734 (2017)

  25. 25.

    Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. Inf. Comput. 252, 95–109 (2017)

    MathSciNet  Article  Google Scholar 

  26. 26.

    Konnov, I., Widder, J.: ByMC: byzantine model checker. In: ISoLA (3), volume 11246 of LNCS, pp. 327–342. Springer (2018)

  27. 27.

    Kragl, B., Qadeer, S., Henzinger, T.A.: Synchronizing the asynchronous. In: CONCUR, pp. 21:1–21:17 (2018)

  28. 28.

    Kukovec, J., Konnov, I., Widder, J.: Reachability in parameterized systems: all flavors of threshold automata. In: CONCUR, pp. 19:1–19:17 (2018)

  29. 29.

    Kwiatkowska, M.Z., Norman, G.: Verifying randomized byzantine agreement. In: FORTE, pp. 194–209 (2002)

  30. 30.

    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: CAV, pp. 585–591 (2011)

  31. 31.

    Kwiatkowska, M.Z., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using Cadence SMV and PRISM. In: CAV, pp. 194–206 (2001)

  32. 32.

    Lamport, L.: Specifying systems: the TLA\(+\) language and tools for hardware and software engineers. Addison-Wesley, Boston (2002)

    Google Scholar 

  33. 33.

    Lehmann, Daniel J., Rabin, Michael O.: On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem. In: POPL, pp. 133–138 (1981)

  34. 34.

    Lengál, O., Lin, A.W., Majumdar, R., Rümmer, P.: Fair termination for parameterized probabilistic concurrent systems. In: TACAS, volume 10205 of LNCS, pp. 499–517 (2017). https://doi.org/10.1007/978-3-662-54577-5_29

  35. 35.

    Lin, A.W., Rümmer, P.: Liveness of randomised parameterised systems under arbitrary schedulers. In CAV, volume 9780 of LNCS, pp. 112–133. Springer (2016). https://doi.org/10.1007/978-3-319-41540-6_7

  36. 36.

    Maric, O., Sprenger, C., Basin, D.A.: Cutoff bounds for consensus algorithms. In: CAV, volume 10427 of LNCS, pp. 217–237 (2017)

  37. 37.

    McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. In: Monographs in Computer Science. Springer (2005). https://doi.org/10.1007/b138392

  38. 38.

    Mostéfaoui, A., Moumen, H., Raynal, M.: Randomized k-set agreement in crash-prone and Byzantine asynchronous systems. Theor. Comput. Sci. 709, 80–97 (2018)

    MathSciNet  Article  Google Scholar 

  39. 39.

    Nestmann, U., Fuzzati, R., Merro, M.: Modeling consensus in a process calculus. In: CONCUR, volume 2761 of LNCS, pp. 393–407 (2003)

  40. 40.

    Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: decidable reasoning about distributed protocols. PACMPL 1(OOPSLA), 108:1–108:31 (2017)

  41. 41.

    Pnueli, A., Zuck, L.D.: Verification of multiprocess probabilistic protocols. Distrib. Comput. 1(1), 53–72 (1986). https://doi.org/10.1007/BF01843570

    Article  MATH  Google Scholar 

  42. 42.

    Song, Y.J., van Renesse, R.: Bosco: one-step Byzantine asynchronous consensus. In: DISC, volume 5218 of LNCS, pp. 438–450 (2008)

  43. 43.

    Steiner, W., Rushby, J.M., Sorea, M., Pfeifer, H.: Model checking a fault-tolerant startup algorithm: from design exploration to exhaustive fault simulation. In: DSN, pp. 189–198 (2004)

  44. 44.

    Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Verifying safety of synchronous fault-tolerant algorithms bounded model checking. In: TACAS, Part II, volume 11428 of LNCS, pp. 357–374 (2019)

  45. 45.

    Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213–214 (1988)

    MathSciNet  Article  Google Scholar 

  46. 46.

    Swaminathan, M., Katoen, J.-P., Olderog, E.-R.: Layered reasoning for randomized distributed algorithms. Formal Asp. Comput. 24(4–6), 477–496 (2012). https://doi.org/10.1007/s00165-012-0231-x

    MathSciNet  Article  MATH  Google Scholar 

  47. 47.

    TLA\(+\) proof system. https://tla.msr-inria.inria.fr/tlaps/content/Home.html

  48. 48.

    Tsuchiya, T., Schiper, A.: Using bounded model checking to verify consensus algorithms. In: Distributed Computing, 22nd International Symposium, DISC 2008, Arcachon, France, September 22–24, 2008, Proceedings, pp. 466–480 (2008)

  49. 49.

    Tsuchiya, T., Schiper, A.: Verification of consensus algorithms using satisfiability solving. Distrub. Comput. 23(5–6), 341–358 (2011)

    Article  Google Scholar 

  50. 50.

    Gleissenthall, K.V., Kici, R.G., Bakst, A.L., Stefan, D.E., Jhala, R.A.: Pretend synchrony. PACMPL 3(POPL), 59:1–59:30 (2019)

  51. 51.

    Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.E.: Planning for change in a formal verification of the RAFT consensus protocol. In: CPP, pp. 154–165 (2016)

  52. 52.

    Zuck, L.D., McMillan, K.L., Torf, J.: \(P^5\): planner-less proofs of probabilistic parameterized protocols. In: VMCAI, pp. 336–357 (2018)

Download references

Author information

Affiliations

Authors

Corresponding author

Correspondence to Marijana Lazić.

Additional information

Supported by Interchain Foundation, Switzerland; by the Austrian Science Fund (FWF) via the National Research Network RiSE (S11403, S11405), project PRAVDA (P27722), and Doctoral College LogiCS (W1255-N23); by the Vienna Science and Technology Fund (WWTF) via project APALACHE (ICT15-103); and by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme Under Grant Agreement No. 787367 (PaVeS). Experiments presented in this paper were carried out using the Grid’5000 testbed, supported by a scientific interest group hosted by Inria and including CNRS, RENATER, and others, see www.grid5000.fr .

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This is an extended version of Bertrand et al. [7], which appeared in the proceedings of CONCUR 2019. In the conference version, we did not provide proofs. As a result, also the definitions where just sketched and we omitted preliminary lemmas. In this paper, we completely develop our theory. Moreover, we give more detailed discussions and explanation with new figures and diagrams, we add and extend examples.

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Bertrand, N., Konnov, I., Lazić, M. et al. Verification of randomized consensus algorithms under round-rigid adversaries. Int J Softw Tools Technol Transfer (2021). https://doi.org/10.1007/s10009-020-00603-x

Download citation

Keywords

  • Verification
  • Distributed algorithms
  • Fault tolerance
  • Probabilistic
  • Parameterized