Metadata

In this post, we model and explore the two-phase commit protocol using TLA+. The two-phase commit protocol is practical and is used in many distributed systems today. Yet it is still brief enough that we can model it quickly, and learn a lot from modeling it. In fact, we see that through this example we get to illustrate a fundamental impossibility result in distributed systems directly. The two-phase commit problem A transaction is performed over resource managers (RMs).  All RMs must agree on whether the transaction is committed  or aborted . The transaction manager (TM)  finalizes the transaction with a commit or abort decision. For the transaction to be committed, each participating RM must be prepared to commit it. Otherwise, the transaction must be aborted. Some notes about modeling We perform this modeling in the shared memory model, rather than in message passing, to keep things simple. This also ensures that the model checking is fast. But we add nonatomicity to

My new years resolution for 2018 was to "ask more/better/crazier questions." To realize this resolution, I knew I needed to implement it as a system. So I committed to "ask at least a couple of MAD questions in each blog post." After close to 12 months and 70 posts, these are what I learned from this exercise. 1. Questioning is very useful Adding the MAD questions section significantly extended/complemented my posts, and with little effort. Just by adding this section, I went for another 15-20 minutes, forcing myself out of my default mode. Sometimes I grudgingly did it, just because I had committed to it, but almost always I was surprised by how useful it was. Many times the MAD questions section got longer than the main post body. And on average it was about 25% of the main body. Questioning also improved the main content, and I had incorporated the findings/leads from some of the MAD questions in the main body of the post. I keep many half-baked posts in

As is the custom in a year-end post, here are some highlights among my 2018 posts. Blockchains Spring 18 Distributed Systems Seminar   Remember peer-to-peer systems?   Replying to why decentralization matters   Snowflake to Avalanche: A Novel Metastable Consensus Protocol Family for Cryptocurrencies   IPFS: Content addressed, versioned, P2P file system   The last mile problem in trust   TLA+  Why you should use modeling [with TLA+]   Debugging designs with TLA+  Modeling the DAO attack in PlusCal  Azure Cosmos DB Azure Cosmos DB   Schema-Agnostic Indexing with Azure Cosmos DB   Logical index organization in Cosmos DB   Academia Academic/research impact  Research and climbing  How to fix scholarly peer review Paxos  Anatomical similarities and differences between Paxos and blockchain consensus protocols  Paxos derived  SDPaxos: Building efficient semi-decentralized geo-replicated state machines  Distributed systems The Lambda and the Kappa

All academics invariably suffer from an occasional bad and unfair review. We pour our sweat (and sometimes tears) over a paper for many months to watch it summarily and unfairly shot-down by a reviewer. Opening a decision email to read such a review feels so sickening that it hurts in the stomach. Even after 20 years, I am unable to desensitize myself to the pain of being shot-down by an unfair review. I suspect quite many people quit academia being frustrated over bad reviews. Peer review is a complex and sensitive topic, and this post will inevitably fall short of capturing some important aspects of it. But I believe this topic is so important that it deserves more attention and conversation. Here I first write a bit about how to handle bad reviews. Then I outline some problems with our current peer review process and suggest some fixes to start a conversation on this. The first rule of review club The first rule of review club is to always give the benefit of doubt to the revi