Metadata

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. Dafny Dafny 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 https://rise4fun.com/Dafny/tutorial 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) sol

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

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 sam

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. https://en.wikipedia.org/wiki/Minimalism#Literary_minimalism 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 co