Verification of randomized consensus algorithms under round-rigid adversaries
Tóm tắt
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.
Tài liệu tham khảo
Aguilera, M., Toueg, S.: The correctness proof of Ben-Or’s randomized consensus algorithm. Distrib. Comput. 25(5), 1–11 (2012). Online first
Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. IPL 15, 307–309 (1986)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Ben-Or, M.: Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract). In: PODC, pp. 27–30 (1983)
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)
Bertrand, N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: FSTTCS, volume 24 of LIPIcs, pp. 501–513 (2013)
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)
Bertrand, N., Lazić, M., Widder, J.: A reduction theorem for randomized distributed algorithms under weak adversaries. In: VMCAI (2021) (to appear)
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)
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)
Bracha, G.: Asynchronous Byzantine agreement protocols. Inf. Comput. 75(2), 130–143 (1987)
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)
Charron-Bost, B., Merz, S.: Formal verification of a consensus algorithm in the heard-of model. IJSI 3(2–3), 273–303 (2009)
Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Heidelberg (2018)
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)
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)
Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155–173 (1982)
Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL, pp. 85–94 (1995)
Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374–382 (1985)
Grimmet, G.R., Strizaker, D.: Probability and Random Processes, 2nd edn. Oxford Science Publications, Oxford (1992)
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)
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)
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)
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)
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)
Konnov, I., Widder, J.: ByMC: byzantine model checker. In: ISoLA (3), volume 11246 of LNCS, pp. 327–342. Springer (2018)
Kragl, B., Qadeer, S., Henzinger, T.A.: Synchronizing the asynchronous. In: CONCUR, pp. 21:1–21:17 (2018)
Kukovec, J., Konnov, I., Widder, J.: Reachability in parameterized systems: all flavors of threshold automata. In: CONCUR, pp. 19:1–19:17 (2018)
Kwiatkowska, M.Z., Norman, G.: Verifying randomized byzantine agreement. In: FORTE, pp. 194–209 (2002)
Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: CAV, pp. 585–591 (2011)
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)
Lamport, L.: Specifying systems: the TLA\(+\) language and tools for hardware and software engineers. Addison-Wesley, Boston (2002)
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)
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
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
Maric, O., Sprenger, C., Basin, D.A.: Cutoff bounds for consensus algorithms. In: CAV, volume 10427 of LNCS, pp. 217–237 (2017)
McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. In: Monographs in Computer Science. Springer (2005). https://doi.org/10.1007/b138392
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)
Nestmann, U., Fuzzati, R., Merro, M.: Modeling consensus in a process calculus. In: CONCUR, volume 2761 of LNCS, pp. 393–407 (2003)
Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: decidable reasoning about distributed protocols. PACMPL 1(OOPSLA), 108:1–108:31 (2017)
Pnueli, A., Zuck, L.D.: Verification of multiprocess probabilistic protocols. Distrib. Comput. 1(1), 53–72 (1986). https://doi.org/10.1007/BF01843570
Song, Y.J., van Renesse, R.: Bosco: one-step Byzantine asynchronous consensus. In: DISC, volume 5218 of LNCS, pp. 438–450 (2008)
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)
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)
Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213–214 (1988)
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
TLA\(+\) proof system. https://tla.msr-inria.inria.fr/tlaps/content/Home.html
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)
Tsuchiya, T., Schiper, A.: Verification of consensus algorithms using satisfiability solving. Distrub. Comput. 23(5–6), 341–358 (2011)
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)
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)
Zuck, L.D., McMillan, K.L., Torf, J.: \(P^5\): planner-less proofs of probabilistic parameterized protocols. In: VMCAI, pp. 336–357 (2018)