TLA+ modeling of MongoDB logless reconfiguration

-

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. 

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 into how they are composed.

At the end I will also show you that by using tla-web application (developed by Will Schultz), it is possible to interactively-explore the executions of the combined spec without the need to install any TLA+ tooling at all by just using the web browser. This is a great way to share specifications and counterexample traces with your colleagues who don't dabble in TLA+ and I am excited for this.


CSM: MongoLoglessDynamicRaft 

This file is at https://github.com/will62794/logless-reconfig/blob/master/MongoLoglessDynamicRaft.tla if you like to follow along.

  • Server is the set of all nodes.
  • state denotes whether a node is Primary or Secondary.
  • currentTerm is the Raft term of a node
  • config is the current config the node knows of
  • configVersion is the version associated with the config
  • configTerm is the term associated with that config    

Refer back to our post on MongoDB logless reconfiguration to see how the configVersion and configTerm plays out. For ensuring safety, the protocol uses the (configTerm,configVersion) as a pair, and requires that the CSM commits the config on the most recent configTerm, and the OSM follows the committed configs in sequential order.  

These are the four possible actions in the CSM protocol.

 

The first action does not seem to constrain the newConfig and seem to allow it to be any possible set in all possible subsets of the Server set, claiming an unrestricted/arbitrary next reconfiguration. But, if you look at the preconditions of Reconfig action on line 99, the QuorumsOverlap check requires that all quorums of newConfig share at least one overlapping node with all quorums of the current config. Pew, sanity restored. If we comment out the QuorumsOverlap condition we would encounter a safety violation. You can try this, after I teach you about the tla-web app at the end of this post.

SendConfig is used for sharing config between any two servers. NewerConfig, determined by higher configTerm or if configTerms are equal by higher configVersion, dominates and gets adopted by the other server.

UpdateTerms is used for updating the currentTerm variable. And BecomeLeader is for one server to become a Primary by getting a quorum of votes from others and increasing its currentTerm. These two actions are shared with the OSM protocol, and we will later see how the composition model will insist that these actions get jointly executed by both CSM and OSM for a superposed composition of the two protocols.


OSM: MongoStaticRaft

This file is at https://github.com/will62794/logless-reconfig/blob/master/MongoStaticRaft.tla if you like to follow along. This is the pull-based replication protocol based on Raft that we covered in this post earlier.

Many of these variables/constants are shared with the CSM above, so let's talk about the diff.

  • log is the oplog for the OSM protocol.
  • committed is the set of committed (majority replicated) entries in the log.

Here are the actions of this OSM protocol

 

BecomeLeader is for becoming a Raft Primary, and UpdateTerms is for propagating the Raft currentTerm variable between two nodes. (These two actions are in fact the same as the same named two actions in the CSM: MongoLoglessDynamicRaft spec.) ClientRequest is for the Primary to accept a request for replication. GetEntries perform pull-based replication of entries in oplog. RollbackEntries performs oplog rollback when warranted upon a primary change, and CommitEntry commits majority replicated entries. Standard Raft stuff.


MongoRaftReconfig

This file is at https://github.com/will62794/logless-reconfig/blob/master/MongoRaftReconfig.tla

The MongoRaftReconfig file composes the MongoLoglessDynamicRaft (CSM) and MongoStaticRaft (OSM), and regulates the superpositioned execution of the two specs.

  • CSM and OSM share actions for BecomeLeader and UpdateTerms.
  • OSM reads from CSM config and uses this as the process set to execute the replication/commit and leader election protocol
  • CSM reads from OSM the OplogCommitment condition. (Note that the composition model guards the CSM's Reconfig action by OplogCommitment, and commenting this out will also lead to a safety violation as we will explore below.)

Due to the shared actions for CSM and OSM for BecomeLeader and UpdateTerms, the composition spec restricts both CSM's and OSM's possible computations/executions to become refinements of their respective original specs.

Note that the initial states of CSM and OSM also need to agree for their shared variables, which are currentTerm, state, and config. The variables of the composition spec is the union of the variables of CSM and OSM.


The composition spec defines OSMNext and CSMNext as follows. Note the OplogCommitment guarding the CSM reconfig action. The composition spec also restricts the shared actions BecomeLeader and UpdateTerms to execute jointly, meaning that both actions take effect in the corresponding specs at the same step. This keeps the CSM and OSM states in synchrony and prevent the two state machines diverging from each other's views.


The Next step here defines a step of the composition spec as either OSMNext, CSMNext, or JointNext. 


State exploration

It is time for us to reach out to the tla-web app and play around with an interactive version of this spec. The spec here is equivalent to the compositional spec we reviewed above, except that it is not specified in the compositional manner, but rather combined into one file together.

If you are ready, just follow my directions. This will be fun. 

Open this link in another tab. This will readily load the joint TLA+ spec. And you can see the spec by clicking the spec button at top right. You can even modify the spec, by commenting out a line.

And that is what we are going to do. The best way to learn something is to break it and see why it breaks, and then fix it back. Go to line 259, and comment the precondition check for OplogCommitment, by putting \* at the beginning of the line. Click the details button up top to come back to the initial page.

Now, the prompt there is asking us to choose a possible initial state. Choose the one where config={s1,s2} that means we have two replicas in the initial configuration. This is the second choice from top. Inspect the assignments in the variables in this initial state and click on it.  Note that the right side of the page changed to show the history of the trace. We only got one step into this execution, so that is what we see on the right. The left pane also changed to list the new actions/transitions that are enabled in this next state resulting from our initial state choice.

Choose the transition where node 1 becomes the leader. This is the BecomeLeader action with s1 becoming the leader using the quorum s1,s2. Note that there are two sub-buttons enabled, the other option is to choose s2 to become the leader. So, follow me, choose the first button to make s1 the leader.

Note that our trace grew by another state transition on the right, and we have a new set of options opened up for us. Choose SendConfig s1, s2. Now our trace is of length 3.

Oh, I almost forgot, on the right pane in the text entry at the top enter LeaderCompleteness and press the AddTraceExpression button next to it. This will let us monitor the invariant LeaderCompleteness, which is line 320 in the Spec tab if you like to check. This evaluates to TRUE now, but since we had introduced a bug in the spec by commenting out the OplogCommitment precondition, we should expect to see this violated soon. 

Let's go faster now.

Choose Reconfig s1, {s1} so that node 1 reconfigures the system to drop down to only one replica, that is itself.

Choose ClientRequest s1 option. And all the while monitor how the state variables evolve on the right as we take the system through this path of execution. Notice the log variable on s1 become <<1>>.

CommitEntry s1 {s1}. Note that s1 did not need another node to commit, since the reconfiguration took the system to just one node, it can commit locally.

Now, choose Reconfig s1, {s1,s2}.

SendConfig s1, s2

Reconfig s1, {s1,s2,s3}

SendConfig s1, s3

SendConfig s1, s2

BecomeLeader s2 {s2,s3}. Wow, notice that LeaderCompleteness became FALSE. This is because s2 does not have what s1 committed (locally), so we lost a commit. Let's continue to see what more trouble this can result in. On the right pane Add Trace Expression StateMachineSafety which is on line 325 in the spec. Note that this still shows as TRUE.

SendConfig s2, s3

ClientRequest s2, so s2 accepts to the same slot (1st slot in the log) another value <<2>>.

GetEntries s3, s2

CommitEntry s2 {s2, s3}. Wow! Notice the StateMachineSafety is violated now. This invariant said:

By modifying the spec and introducing a bug, we violated this invariant. We have a 16 step counter example for this violation. By copying the URL, or using the Copy Trace Link, we can share this counterexample with our colleagues.

But there is a catch for our case. We had done our modification on our local buffer, and not at the spec url, so this link will load the correct version and will only be able to follow the trace to step 8 where the faulty version diverges from the unmodified correct version. If you like to get the full 16 step counterexample you can put the modified version on a publicly accessible link and load that version, and share the steps from that faulty version.  


Comments

Post a Comment

Popular posts from this blog

Learning about distributed systems: where to start?

-
This is definitely not a "learn distributed systems in 21 days" post. I recommend a principled, from the foundations-up, studying of distributed systems, which will take a good three months in the first pass, and many more months to build competence after that. If you are practical and coding oriented you may not like my advice much. You may object saying, "Shouldn't I learn distributed systems with coding and hands on? Why can I not get started by deploying a Hadoop cluster, or studying the Raft code." I think that is the wrong way to go about learning distributed systems, because seeing similar code and programming language constructs will make you think this is familiar territory, and will give you a false sense of security. But, nothing can be further from the truth. Distributed systems need radically different software than centralized systems do.  --A. Tannenbaum This quotation is literally the first sentence in my distributed systems syllabus. Inst
Read more >>

Hints for Distributed Systems Design

-
This is with apologies to Butler Lampson, who published the " Hints for computer system design " paper 40 years ago in SOSP'83. I don't claim to match that work of course. I just thought I could draft this post to organize my thinking about designing distributed systems and get feedback from others. I start with the same  disclaimer Lampson gave. These hints are not novel, not foolproof recipes, not laws of design, not precisely formulated, and not always appropriate. They are just hints.  They are context dependent, and some of them may be controversial. That being said, I have seen these hints successfully applied in distributed systems design throughout my 25 years in the field, starting from the theory of distributed systems (98-01), immersing into the practice of wireless sensor networks (01-11), and working on cloud computing systems both in the academia and industry ever since. These heuristic principles have been applied knowingly or unknowingly and has proven
Read more >>

Foundational distributed systems papers

-
I talked about the importance of reading foundational papers last week. To followup, here is my compilation of foundational papers in the distributed systems area. (I focused on the core distributed systems area, and did not cover networking, security, distributed ledgers, verification work etc. I even left out distributed transactions, I hope to cover them at a later date.)  I classified the papers by subject, and listed them in chronological order. I also listed expository papers and blog posts at the end of each section. Time and State in Distributed Systems Time, Clocks, and the Ordering of Events in a Distributed System. Leslie Lamport, Commn. of the ACM,  1978. Distributed Snapshots: Determining Global States of a Distributed System. K. Mani Chandy Leslie Lamport, ACM Transactions on Computer Systems, 1985. Virtual Time and Global States of Distributed Systems.  Mattern, F. 1988. Practical uses of synchronized clocks in distributed systems. B. Liskov, 1991. Expository papers
Read more >>

Metastable failures in the wild

-
Image
This paper appeared in OSDI'22. There is a great summary of the paper by Aleksey (one of the authors and my former PhD student, go Aleksey!). There is also a great conference presentation video from Lexiang. Below I will provide a brief overview of the paper followed by my discussion points. This topic is very interesting and important, so I hope you have fun learning about this. Metastability concept and categories Metastable failure is defined as permanent overload with low throughput even after the fault-trigger is removed. It is an emergent behavior of a system, and it naturally arises from the optimizations for the common case that lead to sustained work amplification. In this paper, the authors are able to capture/abstract the system behavior of interest in terms of two parameters, the load and capacity. If the load is above capacity, you have work piling up, right? Or if the capacity drops under the sustained load level, the same effect, right? Both of these create  a tem
Read more >>

The demise of coding is greatly exaggerated

-
Image
NVDIA CEO Jensen Huang recently made very contraversial remarks : "Over the course of the last 10 years, 15 years, almost everybody who sits on a stage like this would tell you that it is vital that your children learn computer science, and everybody should learn how to program. And in fact, it’s almost exactly the opposite. It is our job to create computing technology such that nobody has to program and that the programming language is human. Everybody in the world is now a programmer.  This is the miracle of artificial intelligence." I am not going to wise crack and say that this is power poisioning and this is what happens when your company valuation more than triples in a year and surpasses Amazon and Google. (Although I don't discount this effect completely.) Jensen is very smart and also has some great wisdom , so I think we should give this the benefit of doubt and try to respond in a thoughtful manner.  A response is warranted because this statement got a lot of p
Read more >>

Scalable OLTP in the Cloud: What’s the BIG DEAL?

-
Image
This paper is from Pat Helland, the apostate philosopher of database systems, overall a superb person, and a good friend of mine. The paper appeared this week at CIDR'24. (Check out the program for other interesting papers). The motivating question behind this work is: " What are the asymptotic limits to scale for cloud OLTP (OnLine Transaction Processing) systems? " Pat says that the CIDR 2023 paper "Is Scalable OLTP in the Cloud a Solved Problem?" prompted this question.  The answer to the question? Pat says that the answer lies in the joint responsibility of database and the application. If you know of Pat's work, which I have summarized several in this blog , you would know that Pat has been advocating along these lines before. But this paper provides a very crisp, specific, concrete answer. Read on for my summary of the paper. Disclaimer: This is a wisdom and technical information/detail packed 13-page paper, so I will try my best to summarize the sa
Read more >>

The end of a myth: Distributed transactions can scale

-
Image
This paper appeared in VLDB'17. The paper presents NAM-DB, a scalable distributed database system that uses RDMA (mostly 1-way RDMA) and a novel timestamp oracle to support snapshot isolation (SI) transactions. NAM stands for network-attached-memory architecture, which leverages RDMA to enable compute nodes talk directly to a pool of memory nodes. Remote direct memory access (RDMA) allows bypassing the CPU when transferring data from one machine to another. This helps relieve a major factor in scalability of distributed transactions: the CPU overhead of the TCP/IP stack. With so many messages to process, CPU may spend most of the time serializing/deserializing network messages, leaving little room for the actual work. We had seen this phenomena first hand when we were researching the performance bottlenecks of Paxos protocols. This paper reminds me of the "Is Scalable OLTP in the Cloud a Solved Problem? (CIDR 2023)" which we reviewed recently. The two papers share one
Read more >>

SIGMOD panel: Future of Database System Architectures

-
Image
I mentioned this panel in my SIGMOD/PODS day 2 writeup.  The panel consisted of (from right to left) Gustavo Alonso (ETH), Swami Sivasubramanian (AWS), Anastasia Ailamaki (EPFL), Raghu Ramakrishnan (Microsoft), and Sam Madden (MIT). Sailesh Krishnamurthy from Google was unable to attend, so Anastasia who is on sabbatical at Google, also covered for him. The panel started with 5 minutes speeches from participants. The panel was lively and playful. The panelists tried to make their speeches controversial, and have zingers for each other.   Sam talked about the demise of DBMS monolith. He said, the Oracle of 90s is dead because it was incompatible with modern data ecosystem, and the modern DBMSs are shifting towards disaggregated designs. When Sam was a PhD student under Eric Brewer, Eric said we should build disaggregated databases, and people said that won't happen. But we are there now: Disaggregation has arrived! While Sam mentioned about the benefits of disaggregation, he also ca
Read more >>

Why I blog

-
Image
My blog has been going for 14 years now, and has just passed 4 million pageviews. Yay! I remember the 1 million pageviews moment in 2017 ! The main reason I was able to persist for so long is because I blog for selfish reasons. Let me try to unpack why I blog, and why I keep blogging. I write for myself The audience I have in mind is myself. I blog to clarify my understanding and thinking about a topic.  Reading a research/technical paper is already time consuming. I can't do it in less than 4 hours. Period. I love learning. And I am fortunate that I get to read research papers as part of my work. I double-dip on this effort to blog about them, to improve my understanding of these papers. Writing a blog post is the final step in my pipeline for reading a paper. I think my blog reviews of papers hits a good niche. Research papers are written for the wrong audience (or rather maybe the right audience but for the wrong reason): they are written to please 3 specific expert reviewers
Read more >>

There is plenty of room at the bottom

-
Image
This is a pun on the saying "there is always room at the top". This is also the title of a famous Feynman lecture from 1959 , where he made a case for nanotechnology.  In this post, I will try to argue that there is plenty of room at the bottom for distributed algorithms. Most work on distributed algorithms are done at a high-level abstraction plane. These high level solutions do not transfer well to the implementation level, and this opens a lot of space to explore at the implementation level. But this is not just an opportunistic argument. It is imperative to target the implementation level with our distributed algorithms work, otherwise they remain as theoretical, unused, inapplicable.  Let me try to demonstrate using consensus protocols as examples. Someone else can make the same case using another subdomain. Be mindful of what is swept under the rug What is succinct at the high level could be very hard to implement and get right at the low level. Paxos seems simple , bu
Read more >>