TY - JOUR
T1 - Eventual consensus in Synod
T2 - verification using a failure-aware actor model
AU - Paul, Saswata
AU - Agha, Gul
AU - Patterson, Stacy
AU - Varela, Carlos
N1 - Funding Information:
This research was partially supported by the National Science Foundation (NSF), Grant No.—CNS-1816307 and the Air Force Office of Scientific Research (AFOSR), DDDAS Grant No.—FA9550-19-1-0054.
Publisher Copyright:
© 2022, The Author(s), under exclusive licence to Springer-Verlag London Ltd., part of Springer Nature.
PY - 2022
Y1 - 2022
N2 - Successfully attaining consensus in the absence of a centralized coordinator is a fundamental problem in distributed multi-agent systems. We analyze progress in the Synod consensus protocol—which does not assume a unique leader—under the assumptions of asynchronous communication and potential agent failures. We identify a set of sufficient conditions under which it is possible to guarantee that a set of agents will eventually attain consensus using Synod. First, a subset of the agents must not permanently fail or exhibit Byzantine failure until consensus is reached, and second, at least one proposal must be eventually uninterrupted by higher-numbered proposals. To formally reason about agent failures, we introduce a failure-aware actor model (FAM). Using FAM, we model the identified conditions and provide a formal proof of eventual progress in Synod. Our proof has been mechanically verified using the Athena proof assistant and, to the best of our knowledge, it is the first machine-checked proof of eventual progress in Synod.
AB - Successfully attaining consensus in the absence of a centralized coordinator is a fundamental problem in distributed multi-agent systems. We analyze progress in the Synod consensus protocol—which does not assume a unique leader—under the assumptions of asynchronous communication and potential agent failures. We identify a set of sufficient conditions under which it is possible to guarantee that a set of agents will eventually attain consensus using Synod. First, a subset of the agents must not permanently fail or exhibit Byzantine failure until consensus is reached, and second, at least one proposal must be eventually uninterrupted by higher-numbered proposals. To formally reason about agent failures, we introduce a failure-aware actor model (FAM). Using FAM, we model the identified conditions and provide a formal proof of eventual progress in Synod. Our proof has been mechanically verified using the Athena proof assistant and, to the best of our knowledge, it is the first machine-checked proof of eventual progress in Synod.
KW - Athena
KW - Fairness
KW - Formal theorem proving
KW - Liveness
KW - Paxos
KW - Urban air mobility
UR - http://www.scopus.com/inward/record.url?scp=85135154101&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85135154101&partnerID=8YFLogxK
U2 - 10.1007/s11334-022-00463-5
DO - 10.1007/s11334-022-00463-5
M3 - Article
AN - SCOPUS:85135154101
SN - 1614-5046
JO - Innovations in Systems and Software Engineering
JF - Innovations in Systems and Software Engineering
ER -