@inproceedings{7f6ef2e0d5f04316bf81807c36a05146,
title = "Brief Announcement: What's Live? Understanding Distributed Consensus",
abstract = "Distributed consensus algorithms such as Paxos have been studied extensively. Many different liveness properties and assumptions have been stated for them, but there are no systematic comparisons for better understanding of these properties. This paper systematically studies and compares different liveness properties stated for over 30 prominent consensus algorithms and variants. We introduced a precise high-level language and formally specified these properties in the language. We then create a hierarchy of liveness properties combining two hierarchies of the assumptions used and a hierarchy of the assertions made, and compare the strengths and weaknesses of algorithms that ensure these properties. Our formal specifications and systematic comparisons led to the discovery of a range of problems in various stated liveness properties. We also developed TLA+ specifications of these liveness properties, and we used model checking of execution steps to illustrate liveness patterns for Paxos.",
keywords = "distributed consensus, liveness",
author = "Saksham Chand and Liu, \{Yanhong A.\}",
note = "Publisher Copyright: {\textcopyright} 2021 Owner/Author.; 40th ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, PODC 2021 ; Conference date: 26-07-2021 Through 30-07-2021",
year = "2021",
month = jul,
day = "23",
doi = "10.1145/3465084.3467947",
language = "English",
series = "Proceedings of the Annual ACM Symposium on Principles of Distributed Computing",
publisher = "Association for Computing Machinery",
pages = "565--568",
booktitle = "PODC 2021 - Proceedings of the 2021 ACM Symposium on Principles of Distributed Computing",
}