Metadata

This paper, by Finn Hackett, Joshua Rowe, Markus Kuppe, appeared in International Conference on Software Engineering 2023. It presents a specification of Azure Cosmos DB consistency behavior as exposed to the clients.  During my sabbatical at CosmosDB in 2018, I was involved in a specification of CosmosDB as exposed to the clients .  The nice thing about these specs is that they didn't need to model internal implementation but just captured the consistency semantics for clients precisely, rather than ambiguously like English explanations do. They aimed to answer the question of what kind of behavior should a client be able to witness while interacting with the service? The feedback at that time was that customers found this very useful. This 2023 paper improves on our preliminary specs from 2018. It has this great opening paragraph, which echoes the experience of everyone that has painstakingly specified a distributed/concurrent system behavior. Consistency guarantees for dis...

I have been impressed by the usability of TLA-Web from Will Schultz . Recently I have been using it for my TLA+ modeling of MongoDB catalog protocols internally, and found it very useful to explore and understand behavior. This got me thinking that TLA-Web would be really useful when exploring and understanding an unfamiliar spec I picked up on the web. To test my hunch, I browsed through the TLA+ spec examples here ,  and I came across this spec about the Naiad Clock . Since I had read DBSP paper recently , this was all the more interesting to me. I had written about Naiad in 2014 , and about dataflow systems more broadly in 2017 . Getting to the ASCII version of the spec Unfortunately, I would not be able to play with the spec, because it only came in paper form: "The Naiad Clock Protocol: Specification, Model Checking, and Correctness Proof. "  The spec was available only as 13 pages of latex symbols in the Appendix A of this paper. I did briefly consider manually transfor...

I am teaching CSE 4/586 Distributed Systems class  again this Fall (Fall 2014). This is the course I have most fun teaching. (I would like to think my students also feel that way :-) I teach the course with emphasis on reasoning about the correctness of distributed algorithms. Here are the topics I cover in sequence: Introduction, Syntax and semantics for distributed programs, predicate calculus Safety and progress properties Proof of program properties Time: logical clocks, State: distributed snapshots Mutual exclusion, Dining philosophers Consensus, Paxos Fault-tolerance, replication, rollback recovery, self-stabilization Programming support for distributed systems Data center computing and cloud computing  CAP theorem and NOSQL systems Distributed/WAN storage systems I put emphasis on reasoning about distributed algorithms because concurrency is very tricky; it truly humbles human brain. More than 3 actions in a distributed program and your intuitions will f...

I recently gave a two day seminar on "debugging your designs with TLA+/PlusCal" at Dell. So I wanted to write some of the motivation for modeling and debugging your models while this is still fresh in my mind. You need modeling No, not that kind of modeling! Actually the naming clash is not accidental after all: fashion designers need models to test/showcase their designs. You need modeling because: Failing to plan is planning to fail  Everything is a distributed system The corner cases ... they are so many Do it for the development process Being smart does not scale Failing to plan is planning to fail This is from the paper, " Use of formal methods at Amazon Web Services , 2014". "Before launching any complex service, we need to reach extremely high confidence that the core of the system is correct. We have found that the standard verification techniques in industry (deep design reviews, code reviews, static code analysis, stress testing, ...

Here we do a walkthrough of the TLA+ specs for the MongoDB logless reconfiguration protocol we have reviewed recently. The specs are available at the  https://github.com/will62794/logless-reconfig  repo provided by Will Schultz, Siyuan Zhou, and Ian Dardik.  This is the protocol model for managing logless reconfiguration. Let's call this the "config state machine" (CSM). This is the protocol model for static MongoDB replication protocol based on Raft. Let's call this the "oplog state machine" (OSM).  Finally this model composes the above two protocols so they work in a superimposed manner. I really admire how these specs provided a modular composition of the reconfiguration protocol and Raft-based replication protocol. I figured I would explain how this works here, since walkthroughs of advanced/intermediate TLA+ specifications, especially for composed systems, are rare. I will cover the structure of the two protocols (CSM and OSM) briefly, before diving ...

I am done with my distributed systems class this semester . At the end of the semester, I polled my students for feedback about the class. I was especially interested in hearing about their feedback on using TLA+ in the course and course projects, and using research paper reviewing for homework assignments. Of course, I didn't mention these when I solicited their feedback. I asked them to write a brief review for what they have learned in my distributed systems class this semester. I received overwhelmingly positive feedback. Below I share some of the comments about TLA+ and the paper review assignments. (I removed the flattering feedback about my teaching, while I enjoyed reading them.  I put a lot of effort in my teaching and I am happy when the students recognize how much I care.  That keeps me motivated. ) Feedback about using TLA+ I assigned two TLA+ projects. The first project was modeling Voldemort key-value store with client-side routing , and the second project ...

In my distributed systems class for Fall 17, I assigned modeling of the synchronized round consensus algorithm as the first project. I have been assigning TLA+/PlusCal modeling projects in my class for the last 4 years and releasing the projects and their solutions. I believe this is useful for the distributed systems community, because at this point the barrier before wider adoption of TLA+ tools seems to be the lack of more TLA+ modeling examples of algorithms/systems. My goal is to provide a TLA+/PlusCal example for everything I teach in the class. This way the students will get a hands-on experience in algorithms design and dealing with the intrinsic complexities of distributed systems: concurrent execution, asymmetry of information, concurrency bugs, and a series of untimely failures. Here is some previous discussion/context about why I started assigning TLA+/PlusCal modeling projects in distributed systems classes. Timing of the project I think I timed this project well. I...

Maurice Herlihy's paper: "Blockchains from a distributed computing perspective" explains the DAO attack as follows: "Figure 1 shows a fragment of a DAO-like contract, illustrating a function that allows an investor to withdraw funds. First, the function extracts the client's address (Line 2), then checks whether the client has enough funds to cover the withdrawal (Line 3). If so, the funds are sent to the client through an external function call (Line 4), and if the transfer is successful, the client’s balance is decremented (Line 5).  This code is fatally  flawed. In June 2016, someone exploited this function to steal about $50 million funds from the DAO. As noted, the expression in Line 3 is a call to a function in the client's contract. Figure 2 shows the client's code. The client's contract immediately calls withdraw() again (Line 4). This re-entrant call again tests whether the client has enough funds to cover the withdrawal (Line 3), and b...

This work provides a TLA+ formalization of t he state-based isolation model introduced in the PODC 2017 paper. The TLA+ models provided here will be very useful for you if you are a distributed database developer. Using these, you can show your database protocols satisfy the desired isolation levels, and as you extend the design, you can keep checking that the guarantees still hold. I have been suffering from this problem recently. I wrote a TLA+ model for a distributed database design. I thought I would be able to write serializability predicates using TLA+ formulas relatively easily. When I tried doing so, I realized what a mess I am in. I made a couple attempts and found that operation-centric specification of database isolation is hard to define and check. I decided approach the problem sideways and wrote some BaitInvariants to show what behaviors are out-ruled, only to find that what I thought would always be rejected was actually valid serialization behavior in some scenarios. ...

For the second project in my distributed systems class Fall 17, I assigned modeling of the two-phase transaction commit protocol. I ask students to model what happens when the initiator/transaction manager (TM) fails, how would a backup (TM) take over, and what type of problems could arise. Here is the description of the project. I will post the solution later on. 2 phase commit In a distributed system, a transaction is performed by a collection of processes called resource managers (RMs), each executing on a different node. The transaction ends when the transaction manager (TM) issues a request either to commit or to abort the transaction. For the transaction to be committed, each participating RM must be willing to commit it. Otherwise, the transaction must be aborted. The fundamental requirement is that all RMs must eventually agree on whether the transaction is committed or aborted. Here is a model of 2-phase commit. ( This was built by modifying the /P2TCommit.tla/ at Lamp...