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

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 >>

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 >>

Making database systems usable

-
Image
C. J. Date's Sigmod 1983 keynote, "Database Usability", was prescient. Usability is the most important thing to the customers. They care less about impressive benchmarks or clever algorithms, and more about whether they can operate and use a database efficiently to query, update, analyze, and persist their data with minimal headache. (BTW, does anyone have a link to the contents of this Sigmod'83 talk? There is no transcript around, except for this short abstract .) The paper we cover today is from Sigmod 2007. It takes on the database usability problem raised in that 1983 keynote head-on, and calls out that the king is still naked.  Let's give some context for the year 2007. Yes, XML format was still popular then. The use-case in the paper is XQuery. The paper does not contain any  reference to json. MongoDB would be released in 2009 with the document model; and that seems to be great timing for some of the usability pains mentioned in the paper! Web 2.0 was in
Read more >>

Looming Liability Machines (LLMs)

-
As part of our zoom reading group ( wow, 4.5 years old now ), we discussed a paper that uses LLMs for automatic root cause analysis (RCA) for cloud incidents. This was a pretty straightforward application of LLMs. The proposed system employs an LLM to match incoming incidents to incident handlers based on their alert types, predicts the incident's root cause category, and provides an explanatory narrative. The only customization is through prompt-engineering. Since this is a custom domain, I think a more principled and custom-designed  machine learning system would be more appropriate rather than adopting LLMs. Anyways, the use of LLMs for RCAs spooked me vicerally. I couldn't find the exact words during the paper discussion, but I can articulate this better now. Let me explain. RCA is serious business Root cause analysis (RCA) is the process of identifying the underlying causes of a problem/incident, rather than just addressing its symptoms. One RCA heuristic is asking 5 Why&#
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 >>

Advice to the young

-
Image
I notice I haven't written any advice posts recently. Here is a collection of my advice posts pre 2020. I've been feeling all this elderly wisdom pent up in me, ready to pour at any moment. So here it goes. Get ready to quench your thirst from my fount of wisdom. No man, think for yourself, only get what works for you. It is called foundations, not theory Foundations of computer science (or rather any field of study) are the most important topics you can learn. These lay down the frame of thinking/perspective for that area of study. Yet, I am saddened to hear these called as "theory", and labeled as "unpractical". This couldn't be farther from the truth. Take a look at how I recommend studying distributed systems . Don't you dare call this "theory" and "unpractical". This lays the bedrock that you build your practice on. Don't skimp on the foundations. Don't build your home on quicksand. Keep your hands dirty, your mind cl
Read more >>

Linearizability: A Correctness Condition for Concurrent Objects

-
Image
This paper is from Herlihy and Wing appeared in ACM Transactions on Programming Languages and Systems 1990. This is the canonical reference for the linearizability definition. I had not read this paper in detail before, so I thought it would be good to go to the source to see if there are additional delightful surprises in the original text. Hence, this post. I will dive into a technical analysis of the paper first, and then discuss some of my takes toward the end. I had written an accessible explanation of linearizability earlier; you may want to read that first. I will assume an understanding of linearizability to keep this review at reasonable length. Introduction I love how the old papers just barge in with the model, without bothered by pleasantries such as motivation of the problem. These are the first two sentences of the introduction. "A concurrent system consists of a collection of sequential processes that communicate through shared typed objects . This model encompass
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 >>

Understanding the Performance Implications of Storage-Disaggregated Databases

-
Image
Storage-compute disaggregation in databases has emerged as a pivotal architecture in cloud environments, as evidenced by Amazon ( Aurora ), Microsoft ( Socrates ), Google (AlloyDB), Alibaba ( PolarDB ), and Huawei (Taurus). This approach decouples compute from storage, allowing for independent and elastic scaling of compute and storage resources. It provides fault-tolerance at the storage level. You can then share the storage for other services, such as adding read-only replicas for the databases. You can even use the storage level for easier sharding of your database. Finally, you can also use this for exporting a changelog asynchronously to feed into peripheral cloud services, such as analytics. Disaggregated architecture was the topic of Sigmod 23 panel . I think this quote summarizes the industry's thinking on the topic. "Disaggregated architecture is here, and is not going anywhere. In a disaggregated architecture, storage is fungible, and computing scales independently.
Read more >>

Designing Data Intensive Applications (DDIA) Book

-
Image
We started reading this book as part of Alex Petrov's book club . We just got started, so you can join us, by joining the discord channel above. We meet Wednesday's 11am Eastern Time.  Previously we had read transaction processing book by Grey and Reuters. This page links to my summaries of that book. Chp 1. Reliable, Scalable, and Maintainable Applications I love the diagrams opening each chapter. Beautiful! The first chapter consists of warm up stuff. It talks about the definitions of reliabilty, scalability, and maintainability. It is still engaging, because  it is written with an educator and technical blogger voice, rather than a dry academic voice. This book came out on 2017. Martin is working on the new version. So if you have comments for things to focus on for the new version, it would be helpful to collect them in a document and email it to Martin. For example, I am curious about how the below paragraph from the Preface will get revised with 8 more years of hindsight:
Read more >>