Effective Papers

This post is a sequel to my last two posts on Streamlet. The first one explained the protocol . The second one presented a first draft modeling of the protocol. In this post, I present two improvements to the first draft modeling.  In the first, I will make the epochs monotonic at the process level. In the second one, I give each node its own inbox, instead of using a shared whiteboard message set. Again, I will introduce the model dev-log style, using the notes I took while developing it. Adding locally monotonic epochs Why don't I just sequentially increase e in the process main loop. Instead of using while true, with e \in E, the process will go through the epochs in increasing order. This still doesn't constrain the processes to go in lock-step through the epochs. Each process can go through epochs in its own pace independent of the others. The only requirement is if a process participated at an epoch (either as a proposer or voter), it will not participate at a lower epoch...

I had provided an overview of the Streamlet blockchain protocol in my last post , please read that before reading this post on modeling Streamlet in TLA+. Also if you want to get an idea about TLA+, this may be a good post to read. Here I model the crash fault-tolerant version of Streamlet provided in Appendix A of the paper. Modeling Byzantine nodes is very hard: How do you simulate arbitrary behavior of the nodes? How do you then hope to model check it? So I stick with the crash fault-tolerant version which is very similar to the Byzantine fault-tolerant version of the protocol. This version only considers crash faults and in turn it can tolerate up to a minority of node failures. The reason I started modeling was because I was suspicious how there was no need for using the epoch number knowledge in the protocol or the proof of safety in an asynchronous environment. The protocol employs only the longest chain rule. Longest chain does not necessarily mean the chain with the highest e...

In this 2020 technical report , the authors claim to present a very simple BFT consensus protocol. I am taking it that "textbook" in the title is used as praise for simplicity of the algorithm.  Nakamoto consensus is definitely simpler than Streamlet, but in contrast to Nakamoto consensus Streamlet provides deterministic finalization and does not suffer from the costly proof-of-work (POW) and the low-throughput POW induces. And, among the protocols that provide deterministic finalization, including PBFT, Tendermint, HotStuff, yes, Streamlet is the simplest protocol. So, yes, Streamlet deserves your attention. Streamlet protocol Streamlet is an amalgamation of existing techniques. It borrows stuff from Casper, HotStuff, and Elaine Shi's earlier work. But that's OK. The goal is to show the simplest protocol, not necessarily the most novel or the most efficient protocol. Here is the protocol, verbatim from the introduction of the paper. In Streamlet, each epoch has a de...

I came across this list of Crypto podcasts recently . The list is so long, it is practically useless. I googled to see what would be 5-10 high quality podcasts on blockchains. I worked with those shorter lists. I found that many of the recommended podcasts are coming from the finance angle, and some of them are mostly for speculating on coins for investing. I hated most of those. Another type of podcasts were from people who got involved in the area with Bitcoin (through the Bitcoin magazine and conferences). I didn't like those podcasts either as these guys tend to be fanatical, and also not very technical. But since they are in the field and trenches, I did not write them off completely and listened to some select episodes. Overall I am disappointed with the quality of the podcasts in this domain. Please recommend me good podcasts you are aware of. There should be 3-4 gems among this huge list of podcasts. (Epicenter and Unchained was sort of OK.) "Block Zero" podcast b...

A week or so ago, I told you I wanted to brainstorm about the future of work . Well, here it is for what it is worth. Work wants to be free/liberated  As liberties progress and more welfare is created, our expectations move higher up in Moslow's hierarchy . We are not satisfied with achieving bare survival by means of our work, and we want to thrive, flourish, and express ourselves via our work. We long to have more autonomy and freedom of choice and expression in our work. We like to pursue our own enterprises as part of our work. We already see things moving away from the traditional industrial model with company loyalty, closer to this type of model. In software field, which is well off compared to others, people switch jobs frequently, and try to build their own brands/niches, and demand fulfillment from their work. As these trends shape the future of work, we will see a growing gig economy that is served/supported by algorithmic platforms. Some primitive examples of this is us...

This semester I am teaching a small research course on Distributed Consensus, Decentralized Ledgers, and Blockchains. Blockchains! You? One should be able to call bullshit when one sees bullshit. In this blog, I did that several times for certain claims about blockchains technology.  But, just because of some stupid/hyped-up claims and some first-generation inefficient implementations, it is unacceptable to make fun of and ridicule the entire blockchains field. (Yes, it is definitely a field, when a Turing Award winner and a strong candidate for Turing Award publishes papers on the topic. ) A researcher should not use a broad brush to paint. Truth is multidimensional. Even when parts of a field is impractical right now, that doesn't justify putting the entire field down. P2P was impractical. It lost to the centralized model. But the best ideas from those work found their way to traditional datacenter computing. The distributed hash table idea got adopted for distributed key-val...

This paper is authored by Miguel Castro and Barbara Liskov, and it appeared in OSDI 1999. The conference version has around 2500 citations, and the journal version has close to 1500 citations. This paper is the grandfather for most Byzantine Fault Tolerant (BFT) protocols, including work that appeared through 2000s-2010s at OSDI/SOSP, and more recent blockchain BFT work such as LibraBFT.  The serpentine history of Byzantine fault-tolerance The paper starts with this declaration: "We believe that Byzantine fault-tolerant algorithms will be increasingly important in the future because malicious attacks and software errors are increasingly common and can cause faulty nodes to exhibit arbitrary behavior." How prescient of them. When Byzantine fault tolerance (BFT) was first introduced by Lamport in 1982 , it was mostly of theoretical interest, and it remained so for a long time. Although the prediction in this 1999 paper eventually came true, I don't think it happened due to...

This paper presents LibraBFT , the state machine replication system designed for Facebook's Libra Blockchain. LibraBFT is based on HotStuff, which I had summarized recently . LibraBFT adds modules, such as a pacemaker, to adopt and operationalize the HotStuff protocol within a real-world blockchain system. The plan with the Libra project is that, initially, the participating validators will be permitted into the consensus network by "Founding Members". Later on, membership eligibility will gradually become open/permissionless while preserving decentralization with careful governance. (To facilitate dynamic membership, Libra BFT can reconfigure itself by embedding configuration-change commands in the sequence.) In my summary below I mostly use prose lifted from the LibraBFT whitepaper . It is a 41 page paper, so I focus only on the important parts to provide the summary. After the summary, I add a brief discussion about how LibraBFT compares with other blockchain consensus...

This paper appeared in PODC 2019, and is by Maofan Yin, Dahlia Malkhi, Michael K. Reiter, Guy Golan Gueta, and Ittai Abraham.  The paper presents HotStuff, a leader-based Byzantine fault-tolerant consensus protocol. HotStuff forms the basis of LibraBFT which is used in Facebook's Libra project. HotStuff uses the partially synchronous model for liveness, but it is safe even under an asynchronous model. (This is also how Paxos operates, as a crash tolerant consensus protocol.) Once network communication becomes synchronous, HotStuff enables a correct leader to drive the protocol to consensus at the pace of actual (vs. maximum) round duration --a property called responsiveness . Another innovation in HotStuff is that it provides communication complexity that is linear  (rather than quadratic) in the number of replicas. In other words, all-to-all broadcasts are replaced with only participant-to-leader and leader-to-participant communication, with rotating leaders. HotStuff is the ...

This paper appeared in VLDB'19 and is authored by Maurice Herlihy, Barbara Liskov, and Liuba Shrira. How can autonomous, mutually-distrusting parties cooperate safely and effectively? This question is very important for enabling commerce. The trading world answered this question so far by relying on a trusted third party, and in the worst case, on the government/rule-of-law to litigate parties deviating from their contracts. With prevalence of e-commerce and decentralization, this question is recently  considered in *trustless* settings by modern distributed data management systems. Solving the trustless multi-party cooperation when all the parties use the same blockchain is achievable via smartcontracts, but solving the problem where the parties use different blockchains bring many additional challenges. Some of these challenges are familiar to us from the classical distributed systems research on distributed transactions, such as how to combine multiple steps into a single atomic...

In PODC 1983, Michael Ben-Or published a randomized distributed asynchronous consensus algorithm in a paper titled "Another advantage of free choice (Extended Abstract): Completely asynchronous agreement protocols" . After 15 years, a paper in 1998 provided a correctness proof of Ben-Or's algorithm . Above is the pseudocode for Ben-Or from that paper. From the pseudocode it looks like Ben-Or is a very simple algorithm, but in reality its behavior is not easy to understand and appreciate. But fret not, TLA+ modeling and model checking helps a lot for understanding the behavior of the Ben-Or algorithm. It is fulfilling when you finally understand how the algorithm works, and how safety is always preserved and progress is achieved eventually probabilistically. I had assigned modeling of Ben-Or as the TLA+ project for my distributed systems class . Here I share my PlusCal modeling of Ben-Or, and discuss how this model helps us to understand the algorithm better. Here is the l...