Abstract
We revisit the interactive consistency problem introduced by Pease, Shostak and Lamport. We first show that their algorithm does not achieve interactive consistency if faults are transient, even if faults are non-malicious. We then present an algorithm that achieves interactive consistency in the presence of non-malicious, asymmetric and transient faults, but only under an additional guaranteed delayed ack assumption. We discovered our algorithm using an automated synthesis technique that is based on bounded model checking and QBF solving. Our synthesis technique is general and simple, and it is a promising approach for synthesizing distributed algorithms.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 101–115. Springer, Heidelberg (2011)
de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496–500. Springer, Heidelberg (2004)
Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. JACM 32(2), 374–382 (1985)
Gascon, A., Tiwari, A.: Webpage: Synthesis of fault-tolerant distributed algorithms (2013), http://www.csl.sri.com/users/tiwari/softwares/synth_distributed/
Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Proc. PLDI (2011)
Kulkarni, S.S., Arora, A., Chippada, A.: Polynomial time synthesis of byzantine agreement. In: 20th Symp. on Reliable Distributed Systems, SRDS (2001)
Lala, J.H.: A Byzantine resilient fault tolerant computer for nuclear power applications. In: Fault Tolerant Computing Symposium, pp. 338–343 (1986)
Lamport, L., Shostak, R.E., Pease, M.C.: The byzantine generals problem. ACM Trans. Program. Lang. Syst. 4(3), 382–401 (1982)
Lincoln, P., Rushby, J.: Formal verification of an interactive consistency algorithm for the Draper FTP architecture under a hybrid fault model. In: Proc. 9th Conf. on Computer Assurance, COMPASS (1994)
Lonsing, F., Biere, A.: DepQBF: A Dependency-Aware QBF Solver. JSAT 7(2-3), 71–76 (2010)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann (1996)
Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Trans. on Programming Languages and Systems 6, 68–93 (1984)
Miner, P., Geser, A., Pike, L., Maddalon, J.: A Unified Fault-Tolerance Protocol. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT 2004. LNCS, vol. 3253, pp. 167–182. Springer, Heidelberg (2004)
Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. JACM 27(2), 228–234 (1980)
The SAL intermediate language. Computer Science Laboratory, SRI International, Menlo Park, CA (2003), http://sal.csl.sri.com/
Solar-Lezama, A., Rabbah, R., Bodík, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI (2005)
Solar-Lezama, A., Tancau, L., Bodík, R., Saraswat, V., Seshia, S.: Combinatorial Sketching for Finite Programs. In: ASPLOS (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Gascón, A., Tiwari, A. (2014). A Synthesized Algorithm for Interactive Consistency. In: Badger, J.M., Rozier, K.Y. (eds) NASA Formal Methods. NFM 2014. Lecture Notes in Computer Science, vol 8430. Springer, Cham. https://doi.org/10.1007/978-3-319-06200-6_23
Download citation
DOI: https://doi.org/10.1007/978-3-319-06200-6_23
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06199-3
Online ISBN: 978-3-319-06200-6
eBook Packages: Computer ScienceComputer Science (R0)