Armada: Low-Effort Verification of High-Performance Concurrent Programs

This paper appeared in PLDI 2020 and is authored by Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao.The paper presents the Armada framework for code-level verification of concurrent (multithreaded rather than distributed) programs. Armada is roughly a stepwise-refinement extended version of Dafny. So that is where I will start explaining.
DafnyDafny is an open source iterative compiled language for writing verified code. The code is verified with respect to the specifications the developer writes by adding high-level annotations alongside the code, such as ensures P and invariant P. At you will find an interactive tutorial, that will get you up and running proving programs with Dafny. It is really fun, you should try this out now!  Dafny leverages Z3 for discharging proof obligations. Ok, so what is Z3?Z3 is a popular open source Satisfiability modulo theories (SMT) solver. SMT…

Designing Distributed Systems Using Approximate Synchrony in Data Center Networks

This paper is from Dan R. K. Ports Jialin Li Vincent Liu Naveen Kr. Sharma Arvind Krishnamurthy (University of Washington) and appeared in NSDI 2015.The previous week, in our Zoom Reading Group, we had read the "Scalable State Machine Replication" paper in our group. SSMR built on top of a "slow" atomic multicast (implemented with Multi-Ring Paxos) and imposed a total order for all messages before SMR. This paper introduces SpecPaxos (Speculative Paxos), which also tries to impose an ordering of requests messages before SMR processing. SpecPaxos builds on a carefully constructed network to have most messages ordered correctly to start with and provides a way to deal with messages reorderings as needed. The relaxing of the ordering requirement allows Speculative Paxos to achieve good (average) latency and high throughput, and escape the heavy cost of atomic multicast implementation. (To be fair, SpecPaxos doesn't consider the problem of partitioning SMR and stil…

Scalable state machine replication

This paper is by Carlos Eduardo Bezerra, Fernando Pedone, and Robbert van Renesse, and it appeared in DSN 2014. This paper presents a non-Paxos non-consensus state machine replication (SMR) solution. When I see a non-Paxos solution to SMR, I always ask, "Ok, but where is Paxos hiding here?" It turns out, in this SMR solution, Paxos is hiding in the atomic multicast. The SMR protocol described in the paper assumes atomic multicast feed it. And atomic multicast is a problem equivalent to distributed consensus, and in the evaluation we see that they implement the atomic multicast service using MultiRing Paxos."Atomic multicast ensures that (i) if a server delivers m, then all correct   servers deliver m (agreement); (ii) if a correct process multicasts m to groups, then all correct servers in every group deliver m (validity); and (iii) relation < is acyclic (order). The order property implies that if s and r deliver messages m and m′, then they deliver them in the same …

Book review. Consider this: moments in my writing life after which everything was different (Chuck Palahniuk, 2020)

I had recently listened to Chuck Palahniuk in Tim Ferris's podcast. I got hooked immediately by Palahniuk's views on minimalism in writing. The man is right. The novelist has no business telling how the characters feel and how you should feel. Literary minimalism is characterized by an economy with words and a focus on surface description. Minimalist writers eschew adverbs and prefer allowing context to dictate meaning. Readers are expected to take an active role in creating the story, to "choose sides" based on oblique hints and innuendo, rather than react to directions from the writer.
It was clear that Palahniuk had thought a lot about how to choose words and how to give a rhythm to the story. So to learn more of his craft, I picked up his new book on writing: Consider This: Moments In My Writing Life After Which Everything Was Different. I loved it. I recommend it if you care about improving how you commu…

Zoom, zoom, zoom

The new school year is on its way. My daughter is a kindergartener, my other daughter is a fourth grader, and my son is an eight grader. They will all be attending school as remote. It is going to be a challenging school year for all of us.
The school offered a hybrid version of 2 days of in-person teaching followed by a day of remote teaching, and assignments. But we chose the all remote version. Our reasoning was that these schools will all be converting to remote in a month or two anyways, so why keep up the facade. A better strategy for the schools would be to keep it simple, and put all their preparation efforts for a fully online platform. I think most of the reason for putting up the facade is because of the pressure from the parents who are unable to accept this new reality. 
For my little daughter we sure had imagined this year differently. We were thinking that she would be holding hands with her older sister, sharing seats on the school bus ride to school and back, and have g…

My Distributed Systems Seminar's reading list for Fall 2020

In the Plex: How Google Thinks, Works, and Shapes Our Lives (Steven Levy, 2011)

I read this book recently. Going into this, I knew I wouldn't learn many new/surprising things. After all, I have been following Google from outside since 1999. After I saw Google in action, I had switched to it immediately. I was quick to get on board with Gmail as well, and followed many Google services over the years. I have seen things.As I anticipated, I didn't find many surprises in the book. But I liked the book nevertheless. It is always nice to read stuff from Steven Levy. Steven Levy is one of my favorite authors. I have a dog-eared copy of the Hackers book he wrote. It was excellent writing. So much research went into each character in the book, and he made each character come alive. He also weaved the narration together artistically around a handful of themes and related new information/events back to these themes. He had put a lot of his interpretation and insight in to the facts/narrative, and I really enjoyed that. This book is not as colorful. It has a raw blan…

Popular posts from this blog

I have seen things

SOSP19 File Systems Unfit as Distributed Storage Backends: Lessons from 10 Years of Ceph Evolution

PigPaxos: Devouring the communication bottlenecks in distributed consensus

Learning about distributed systems: where to start?

My Distributed Systems Seminar's reading list for Fall 2020

Fine-Grained Replicated State Machines for a Cluster Storage System

My Distributed Systems Seminar's reading list for Spring 2020

Cross-chain Deals and Adversarial Commerce

Book review. Tiny Habits (2020)

Zoom Distributed Systems Reading Group