MongoDB Engineering Blog
Posts on Engineering efforts, achievements, and culture at MongoDB.
The Ground Beneath the Database
October 8, 2026
Engineering Blog
Same Query, Same Score: Consistent Ranking with StableTfl in Atlas Search
Suppose you run paginated search in your application, or a RAG pipeline where the top ten retrieved documents feed a model. One of your users searches for a recipe collection for "chocolate cake." Page one ends with "Flourless Chocolate Cake." They click next, and the first result on page two is "Flourless Chocolate Cake" again. Between the two requests, nothing about the query changed; only the requested page did. An Atlas Search customer running paginated search brought us this exact problem. The usual workarounds, such as pinning each user to one replica or holding an index snapshot open for every pagination session, require the system to store additional state per query, and they are either too cumbersome or don’t fully close the gap. We fixed it instead by building a new scoring function, StableTfl, that needs no extra state at all. It resolved their issue, and we have since contributed it to Apache Lucene, the open source search engine that powers Atlas Search, so any search system built on top of Lucene can use it.
Accelerating Vector Search with Bulk Scoring
Suppose you are building a recommendation engine for your app. When you display a product page, you want to show other products that are “like” this product in a semantic sense – for example, you might show speakers and cables as a related product for a record player. Folks are often reaching for dense vector search to serve these kinds of applications, as embedding models are good at capturing semantic similarity. When you get it working, you might notice it’s not as fast as you hope. Dense vectors tend to be large (4-12KB), and scoring matches involves computing a geometric distance metric between a query vector and vectors in the database.
MongoDB Predictive Auto-Scaling: An Experiment
You can often predict a load spike before it arrives. Maybe it happens at the same time every day, or there’s always a spike at midnight on a Friday when you run a certain batch job. Or maybe it’s not cyclical, but load is rising steadily, and it’s a reasonable guess that it will keep rising for a while. MongoDB Atlas’s reactive auto-scaler handles these spikes, but scaling to the right size takes several minutes. What if MongoDB Atlas could use these temporal patterns—cycles and trends—to scale up a replica set before it’s overloaded?
Towards Model-based Verification of a Key-Value Storage Engine
In our previous post, we talked about our process of specifying MongoDB’s distributed transactions protocol and how it enabled novel analysis of its performance characteristics. In this follow-up, we talk about how the modularity of our specification also enabled us to check that the underlying storage engine implementation actually conforms to the abstract behavior defined in our formal specification. That is, we are able to formalize the interface boundary between the sharded transaction protocol and WiredTiger, the underlying key-value storage engine, and develop an automated way to generate tests for checking conformance between the semantics of the underlying storage engine layer and this abstract model. As mentioned in the previous post, a deeper exploration of the concepts covered in this post is covered in our recently published VLDB ’25 paper, Design and Modular Verification of Distributed Transactions in MongoDB. Modular, Model-Based Verification As discussed in Part 1, we had developed a TLA+ specification of MongoDB’s distributed transactions protocol in a compositional manner, describing the high level protocol behavior while also formalizing the boundary between the distributed aspect of the transactions protocol and the underlying single-node WiredTiger storage engine component. As mentioned, the distributed transactions protocol can be viewed as running atop the lower level storage layer. When considering the correctness guarantees of the distributed transactions protocol, a subtle aspect is its interaction with the concurrency control mechanisms at each layer of the system. In particular, its interaction with the WiredTiger storage engine API, which has various timestamp-based operations implemented to adequately support the correct operation of the distributed transactions protocol. Our formal model of the distributed transactions protocol was useful for checking its guarantees, but we also wanted to formalize the contract between this distributed protocol and the underlying storage engine, to check that this interface boundary, as defined in our abstract specification, was matched by the implementation. Leveraging the clean interface boundary in our specification, we developed a tool for automatically checking conformance between the WiredTiger implementation and this abstract storage specification (Storage) we defined. Our storage layer specification itself serves as a useful and precise definition of a subset of the WiredTiger storage engine semantics, but we can also use it for automatically generating test cases to check conformance of WiredTiger semantics to our spec. Figure 1. Compositional specification of distributed transactions in TLA+ and storage engine component. Path-based test case generation To do this, we make use of a modified version of the TLC model checker to first generate the storage component specification’s complete graph of reachable states for finite parameters. We then compute a set of path coverings in this graph, where each path is then converted to an individual test case as a sequence of underlying storage engine API calls. This model-based verification technique allows us to automatically generate tens of thousands of individual test cases for WiredTiger which each check that the implementation matches the behavior defined in our abstract specification, which is also the contract relied on by the high level, distributed transactions protocol. Figure 2. Model-based test case generation workflow. For a small, complete finite model (2 keys and 2 transactions), we are able to check conformance with WiredTiger with a generated suite of 87,143 tests, which are generated and executed against the storage engine in around ~40 minutes. Figure 3. Test case generation statistics for the storage layer model. Our current storage layer specification can be found in Github, and a link to an interactive, explorable version of it can also be found in Github. In the future, we hope to explore modeling of a more extensive subset of the WiredTiger API and explore alternate state space exploration strategies for generating tests, e.g., randomized path sampling, or other strategies that only require approximate coverage of the state space model. This approach bears similarity to other testing efforts we had explored in the past. Conclusion Modeling our distribution transactions protocol enabled verification of protocol correctness, and our use of modularity and compositional verification was instrumental in letting us reason about these high-level correctness properties while also being able to automatically check that our abstract storage interface correctly matches the semantics of the implementation. Similar approaches have been explored recently for model-based verification of distributed systems, as well as other approaches for testing systems using path-based test case generation techniques. In the future, we also remain optimistic about the role that LLMs can play in this type of verification workflow. For example, once such a testing harness for checking conformance is developed, having LLMs autonomously develop a model of the underlying system behavior allows for precise characterization of behavior, along with automated test suite generation capabilities. You can find more details about this work in our recently published VLDB ‘25 paper, and in the associated Github repo that contains our specifications and code, as well as links to in-browser, explorable versions of our specifications.
Formal Methods Beyond Correctness: Isolation & Permissiveness of Distributed Transactions in MongoDB
MongoDB has supported distributed, multi-document transactions since 2019, enabling ACID, cross-shard transactions at snapshot isolation. In this post, we will dive into how the distributed transactions protocol works in MongoDB and discuss recent work we have done on formal modeling and verification to examine our transactions protocol in more depth.
Token-count-based Batching: Faster, Cheaper Embedding Inference for Queries
Embedding model inference often struggles with efficiency when serving large volumes of short requests—a common pattern in search, retrieval, and recommendation systems. At Voyage AI by MongoDB, we call these short requests queries, and other requests are called documents. Queries typically must be served with very low latency (typically 100–300 ms). Queries are typically short, and their token-length distribution is highly skewed. As a result, query inference tends to be memory-bound rather than compute-bound. Query traffic is pretty spiky, so autoscaling is too slow. In sum, serving many short requests sequentially is highly inefficient. In this blog post, we explore how batching can be used to serve queries more efficiently. We first discuss padding removal in modern inference engines, a key technique that enables effective batching. We then present practical strategies for forming batches and selecting an appropriate batch size. Finally, we walk through the implementation details and share the resulting performance improvements: a 50% reduction in GPU inference latency—despite using 3X fewer GPUs. Padding removal makes effective batching possible Given the patterns of query traffic, one straightforward idea is: can we batch them to improve inference efficiency? Padding removal, supported in inference engines like vLLM and SGLang, makes efficient batching possible. Most inference engines accept requests in the form (B, S), where B is the sequence number in the batch, and S is the maximum sequence length. Sequences should be padded to the max sequence length so that tensors line up. But that convenience comes at a cost: padding tokens do no useful work but still consume compute and memory bandwidth, so latency scales with B × S instead of the actual token count. With serving large volumes of short requests, this wastes a large share of compute and can inflate tail latency.Padding removal and variable-length processing fix this by concatenating all active sequences into one long "super sequence" of length T = Σtoken_count_i, where token_count_i is the token count in sequence i. Inference engines like vLLM and SGLang can process this combined sequence. Attention masks and position indices ensure that each sequence only attends to its own tokens. As a result, inference time now tracks T rather than B × S, aligning GPU work with what matters. Proposal: token-count-based batching In Voyage AI, we proposed and built token-count-based batching, batching queries (short requests) by total token count in the batch (Σtoken_count_i), rather than by total request count or arbitrary time windows. Time-window batching is inefficient when serving many short requests. Time-window batching swings between under- and over-filled batches depending on traffic. A short window keeps latency low but produces small, under-filled batches; a long window improves utilization but adds queueing delay. Traffic is bursty, so a single window size oscillates between under- and over-filling. Time-window batching introduces variability in resource utilization, causing the system to shift between memory-bound and compute-bound operations. Request-count batching has similar problems. Diagram illustrating the difference between request-number-based batching and token-count-based batching. Figure 1. Request-number-based batching VS token-count-based batching. Token-count batching aligns the batch size (total token count in the batch) with the actual compute required. When many queries arrive close together, we group them by token counts so the GPU processes a larger combined workload in a single forward pass. Based on our experiment, token-count-based batching amortizes fixed costs, reduces per-request latency and cost, and increases throughput and model flops utilization (MFU). What is the optimal batch size? Our inference-latency-vs-token-count profiling of query inference shows a clear pattern: latency is approximately flat up to a threshold (saturation point) and then becomes approximately linear. For small requests, fixed per-request overheads (like GPU scheduling, memory movement, pooling and normalization, etc.) dominate, and latency stays nearly constant; beyond that point, latency scales with token count. The threshold (saturation point) depends on factors like the model architecture, inference engines, and GPU. For our voyage-3 model running on A100, the threshold is about 600 tokens. Line graph showing that GPU inference latency for the Voyage-3 model on A100 is approximately flat for batches up to about 600 tokens (the saturation point), and then increases linearly with the total token count. Figure 2. Inference latency vs token count for Voyage-3 on A100. Based on the data of inference latency vs token count, we can analyze FLOPs Utilization (MFU) vs. token count and throughput vs. token count, which are shown in the following graph. We observe that Model FLOPs Utilization (MFU) and throughput scale approximately linearly with token count until reaching a saturation point. Most of our queries inferences are in the memory-bound zone, far away from the saturation point. Approximated diagram showing Model FLOPs Utilization (MFU) and throughput scaling linearly with token count up to a saturation point, and inference latency remaining flat until the saturation point, after which it also scales linearly. This illustrates how batching can shift inference from memory-bound to compute-bound. Figure 3. Approximated diagram of MFU/throughput/inference latency vs token count. Batching short requests can move the inference from memory-bound to compute-bound. If we choose the saturation point in Figure 3 as the batch size (total token count in the batch), the latency and throughput/MFU can be balanced and optimized. Queue design: enabling token-count-based batching Token-count–based batching needs a data system that does more than simple FIFO delivery. The system has to attach an estimated token_count to each request, peek across pending requests, and then atomically claim a subset whose total tokens fit the optimal batch size (Σtoken_count_i ≤ optimal_batch_size). Without these primitives, we either underfill the GPU—wasting fixed overheads—or overfill it and spike tail latency. General-purpose brokers like RabbitMQ and Kafka are excellent at durability, fan-out, and delivery, but their batching knobs are message count/bytes, not tokens. RabbitMQ’s prefetch is request-count-based, and messages are pushed to consumers, so there’s no efficient way to peek and batch requests by Σtoken_count_i. Kafka batches by bytes/messages within a partition; token count varies with text and tokenizer, so there is no efficient way to batch requests by Σtoken_count_i. So there are two practical paths to make token-count-based batching work. One is to place a lightweight aggregator in front of Kafka/RabbitMQ that consumes batches by token counts and then dispatches batches to model servers. The other is to use a store that naturally supports fast peek + conditional batching—for example, Redis with Lua script. In our implementation, we use Redis because it lets us atomically “pop up to the optimal batch size” and set per-item TTLs within a single lua script call. Whatever we choose, the essential requirement is the same: the queue must let our system see multiple pending items, batch by Σtoken_count_i, and claim them atomically to keep utilization stable and latency predictable. Our system enqueues each embedding query request into a Redis list as: Code Snippet 1 <token_count>:: :: Model servers call lua script atomically to fetch a batch of requests until the optimal batch size is reached. The probability of Redis losing data is very low. In the rare case that it does happen, users may receive 503 Service Unavailable errors and can simply retry. When QPS is low, batches are only partially filled and GPU utilization remains low, but latency still improves. Diagram illustrating the token-count-based batching implementation, where incoming embedding query requests are enqueued into a Redis list and model servers atomically fetch a batch of requests up to the optimal total token count using a Lua script. Figure 4. Batching implementation. Results We ran a production experiment on the Voyage-3-Large model serving, comparing our new pipeline (query batching + vLLM) against our old pipeline (no batching + Hugging Face Inference). We saw a 50% reduction in GPU inference latency—despite using 3X fewer GPUs. We gradually onboarded 7+ models to the above query batching solution, and saw the following results (note that these results are based on our specific implementations of the “new” and “old” pipelines, and are not necessarily generalizable): vLLM reduces GPU inference time by up to ~20 ms for most of our models. GPU utilization and MFU increase, reflecting reduced padding, better amortization of per-batch overhead, and inference moving closer to the compute-bound regime. Throughput improves by up to 8× via token-count–based batching. Some model servers see P90 end-to-end latency drop by 60+ ms as queuing time is reduced under resource contention. P90 end-to-end latency is more stable during traffic spikes, even with fewer GPUs. In summary, combining padding removals with token-count-based batching improves throughput and reduces latency, while improving resource utilization and lowering operational costs during short query embedding inference.
To Lock or Not: MongoDB’s Lock-Free B-Tree Unlocks Throughput
Realizing that I’ve been building storage engines for nearly two decades has led me to reflect on what’s changed. During that time, I’ve learned what it takes to build trust in my products. Happily, it’s a mutually beneficial equation: the safer I keep users' information, the less likely an emergency is to occur—and the more likely they are to trust and use my work.
Carrying Complexity, Delivering Agility
Resilience, intelligence, and simplicity: The pillars of MongoDB’s engineering vision for innovating at scale We’re relatively new to MongoDB— Ashish joined two years ago via the Granite acquisition after a decade-plus building Google’s databases and distributed systems, and Akshat joined in June 2024 after 15 years building databases at AWS. We have a shared obsession with distributed systems. We’d seen how much developers loved MongoDB, which is part of the reason we joined the company—MongoDB is one of the most loved databases in the world. So one of the first things we sought to understand was why. It turned out to be simpler than we thought: MongoDB’s vision is to get developers to production fast. This means making it easy to start, and easier to keep going—one command spin-up, sane defaults for day one, and zero downtime upgrades and zero downtime expansion to multiple clouds as you scale. That’s what developer agility looks like in practice: the ability to choose the best tools, move quickly, and to trust the system to carry the weight of failure, complexity, and change. At MongoDB, three principles drive that vision: resilience, intelligence, and simplicity. Resilience is the ability to keep going when something breaks, intelligence is the ability to adapt to changing conditions, and simplicity is reducing cognitive and operational load so users and operators can move quickly and safely. These are not just technical goals—we treat them as non-negotiable design constraints. So if a change widens blast radius, breaks adaptive performance, or adds operator toil, it doesn’t ship. In this post, we share the key engineering themes shaping our work and the mechanisms that keep us honest. Security as a first principle Security isn't a wall you build around your data. It's an assumption you design against from the very beginning. The assumption is simple: in a distributed system, you can’t trust the network, you can’t trust the hardware, and you certainly can't trust your neighbors. This starts with architectural isolation. In most cloud database service offerings, you're sharing walls with strangers. Shared walls hurt performance, they leak failures, and sometimes they leak secrets. We minimize shared walls, and where utilities must be shared, we build firebreaks. Stronger isolation reduces the blast radius of mistakes and attacks. With a MongoDB Atlas dedicated cluster, you get the whole building. Your cluster runs on its own provisioned servers, in its own private network (VPC). Your unencrypted data is never available in a shared VM or process. There are no "noisy neighbors" because you have no neighbors. The attack surface shrinks dramatically, and resource contention disappears. The blast radius of a problem elsewhere stops at your door. In other words, we follow an anti-Vegas principle—what happens outside your cluster will stay outside. But true security is layered. Once we’ve isolated the environment, we defend it from the inside out. We start by asking the hard questions: Who are you? That's strong authentication, from SCRAM to AWS IAM. What can you do? That's fine-grained RBAC, enforcing the principle of least privilege. What if someone gets in? That's encryption everywhere—in transit, at rest, and even in use with Client-Side Field Level Encryption . How do we lock down the roads? That’s network controls like IP access lists and private endpoints. And how do we prove it? That's granular auditing for a clear, immutable trail. Every one of these layers reflects defense in depth. Figure 1. Queryable Encryption. The history of database security is full of trade-offs between safety and functionality. For decades, the trade-off has been brutal: to run a query, you had to decrypt your data on the server, exposing it to risk. Queryable Encryption —an industry-first searchable encryption scheme developed by MongoDB Research—breaks this paradigm. It allows your application to run expressive queries, including equality and range checks on data that remains fully encrypted on the server. The decryption keys never leave your client. The server maintains encrypted indexes for the fields you wish to query on, and queries can be done entirely on the encrypted data, maintaining the strongest privacy and security of your sensitive data. By carrying these defenses in the platform itself, security stops being another burden developers have to design around. They get the privacy guarantees , the audit trails, and the compliance , without sacrificing functionality or velocity. Achieving resilience: Architecture, operations, and proof Systems don’t live in a vacuum. They live in messy realities: network partitions, power outages, kernel panics, cloud control plane hiccups, operator mistakes. The measure of resilience is not “will it fail?” but “what happens next?” Resilience is the ability to keep going when the thing you depend on stops working, not because you planned for it to fail, but because you planned for it to recover. Here’s how we achieve resilience. Architecture: MongoDB Atlas is built on the assumption that something may fail at any time. Every cluster starts life as a replica set, spread across independent availability zones. That’s the default, not an upgrade. The moment a primary becomes unreachable, an election happens. Within seconds, another node takes over, clients reconnect, and in-flight writes retry automatically. Single-zone diversity buys you protection against a data center outage. Adding more regions buys you protection against a full region failure. Adding more cloud providers buys you insulation against provider-wide events. Each step up that ladder buys you more protection against bigger failures. The trade-off is that each step adds more moving parts to manage, and the failure modes evolve: intra-region links are fast; cross-region introduce wide, lossy links; cross-cloud adds different fabrics, load balancers, and failure semantics. Figure 2. Resilience options: Single zone, multi-AZ, multi-region, multi-cloud. Our job is to make any type of failures (node failures, link failures, gray failures) invisible to you. Writes are only committed when a majority of voting members have the entry in the same term. That rule sounds small, but it’s the safety net that prevents a primary stranded on the wrong side of a partition from accepting writes it can’t keep. Heartbeats and UpdatePosition messages carry progress and truth; if a node learns of a higher term, it steps down immediately. When elections happen, the new primary doesn’t open for writers until it has caught up to the latest known state, preserving as many uncommitted writers as possible. Secondaries apply operations as they arrive, even over lossy links. Operating discipline: Resilience isn’t just in the code and architecture, it’s in how you operate it every day. Even the best design will fail without the discipline to detect problems early and recover quickly. You need to embed it in how you operate. Operational excellence is about preventing avoidable failures, detecting the ones you can’t prevent, and recovering quickly when they happen. And we’ve turned that into a discipline. Every week, the people closest to the work—engineers, on-calls, product managers, and leaders—step out of the day’s firefight to review the system with rigor. We celebrate the small wins that quietly make the system safer. We dig into failures to understand not just what happened, but how to make sure it doesn’t happen again anywhere. The goal isn’t perfection. Instead, it’s building a system where every lesson learned and every fix made raises the floor for everyone. A single automation can remove a whole category of incidents. A well-written postmortem can stop the same mistake from happening across dozens of systems. The return isn’t linear—it compounds. Figure 3. The ops excellence flywheel. When resilience works, failure stops being something every developer has to carry in their head. The system absorbs it, recovers, and lets them keep moving. Proof before shipping: Testing tells you that your code works in the cases you’ve thought to test. Formal verification tells you whether it works in all the cases that matter, even the ones you didn’t think to test. MongoDB is among the few cloud databases that apply and publish formal methods on the core database paths. This rigor translates into agility; teams using the database ship products without worrying about node failures, failovers, or clock skew, causing edge cases. Those edge cases in the database have already been explored, proven, and designed against. Figure 4. Formal methods. When we design a new replication or failover protocol, we don’t just code it, run a few chaos tests, and ship it. We build a mathematical model of the core logic stripped of distracting details like disk format or thread pools and ask a model checker to try every possible interleaving of events. The tool doesn’t skip the “unlikely” cases. It tries them all. Take logless reconfiguration . The idea is simple: MongoDB decouples configuration changes from the data replication log, so membership changes no longer queue behind user writes. But while the idea is simple, the implementation is not. Without care, concurrent configs can fork the cluster, primaries can be elected on stale terms, or new majorities can lose the old majority’s writes. We modeled the protocol in TLA+, explored millions of interleavings, and distilled the solution down to four invariants: terms block stale primaries, monotonic versions prevent forks, majority votes stop minority splits, and the oplog-commit rule ensures durability carries forward. For transactions , we developed a modular formal specification of the multi-shard protocol in TLA+ to verify protocol correctness and snapshot isolation, defined and tested the WiredTiger storage interface with automated model-based techniques, and analyzed permissiveness to assess how well concurrency is maximized within the isolation level. These models are not giant, perfect representations of the whole system. They’re small, precise abstractions that focus on the essence of correctness. The payoff is simple: the model checker explores more corner cases in minutes than a human tester could in years. Alongside formal proofs, we use additional tools to test the implementation under deterministic simulation: fuzzing, fault injection, and message reordering against real binaries. Determinism gives us one-click bug replication, CI/CD regression gates, and reliable incident replays—o rare timing bugs become easy fixes. Mastering the multi-cloud reality with simple abstractions Developer agility isn’t about having a hundred choices on a menu; it's about removing the friction that makes real choice impossible. One such choice that almost never materializes in practice is multi-cloud. We achieve multi-cloud by building a unified data fabric that lets you put your data anywhere you need it, controlled from a single place. A DIY multi-cloud database where you run self-managed MongoDB across AWS, Microsoft Azure, and Google Cloud seems simple on paper. In practice, it involves weeks of networking (VPC/VNet peering, routing, and firewall rules) and brittle scripts. The theoretical agility that you got by going multi-cloud collapses under the weight of operational reality. Figure 5. Multi-cloud replica sets with MongoDB. Now contrast this with MongoDB Atlas, where you don’t have to manually orchestrate provisioning across three different cloud APIs. A single replica set can span AWS, Google Cloud, and Azure. Provisioning, networking, and failover are handled for you. Your app connects with a standard mongodb+srv string, and our intelligent drivers ensure that if your AWS primary fails, traffic automatically fails over to a new primary in GCP or Azure without any changes to your code. This transforms an operational nightmare into a simple deployment choice, giving you freedom from vendor lock-in and a robust defense against provider-wide outages. Agility also means precise data placement for data sovereignty and global latency. Global Clusters and Zone sharding let you describe simple rules so data stays where policy requires and users are served locally, e.g., A rule to map "DE", "FR", and "ES" to the EU_Zone can guarantee that all European customer data and order history physically reside within European borders, satisfying strict GDPR requirements out of the box. Because Zone Sharding is built into the core sharding system, you can add or adjust placement without app rewrites. That’s real agility: the platform removes the hard parts, so the choices are real. From data to intelligence: Building the next generation of AI-powered applications Building intelligent AI-powered features has been a complex and fragmented process. The traditional approach forced developers to maintain separate vector databases for semantic search, creating brittle ETL pipelines to shuttle data back and forth from their primary operational database. This introduced architectural complexity, latency, and a higher total cost of ownership. That’s not agility. That’s friction. Our approach is to eliminate this friction entirely. We believe the best place to build AI-powered applications is directly on your operational data. This is the vision behind MongoDB Atlas Vector Search. Instead of creating a separate product, we integrated vector search capabilities directly into the MongoDB query engine. This is a profound simplification for developers. You can now perform semantic search—finding results based on meaning and context, not just keywords—using the same MongoDB Query API (MQL) and drivers you already know. There are no new systems to learn and no data to synchronize. You can seamlessly combine vector search with traditional filters, aggregations, and updates in a single, expressive query. This dramatically accelerates the development of modern features like RAG ( retrieval-augmented generation ) for chatbots, sophisticated recommendation engines, and intelligent search experiences. Intelligence isn’t something you bolt on. It’s something you build on. This is an area where we continue to make multiple enhancements. For example, with the acquisition of Voyage AI earlier this year, we are making progress towards integrating Voyage's embedding and reranking models into Atlas to deliver a truly native experience . We are also actively applying AI toward our Application Modernization efforts. Consider a relational database application that involves pages of SQL statements representing a view or a query. How do you translate it so it can work effectively with MongoDB’s MQL? LLMs have advanced enough to provide a base version that may be mostly the correct shape, but to get it accurate and performant requires building additional tooling. We are actively working with several customers, not only on the SQL → MQL translation, but also on modernizing their application code using similar techniques. What’s next? We’ll keep pushing on the same three levers: resilience, intelligence, and simplicity. Keep watching this space. We’ll publish deep dives similar to our TLA+ write-up on logless reconfiguration , covering formal methods and other behind-the-scenes work on hard engineering problems, such as MongoDB 8.0 performance improvement challenges . Our vision is to carry the complexity so developers don’t have to—and to give them the agility & freedom to build the next generation of intelligent applications wherever they want. For more on how MongoDB went from a “niche” NoSQL database to a powerhouse with the high availability, tunable consistency, ACID transactions, and robust security that enterprises demand, check out the MongoDB blog .
Lower-Cost Vector Retrieval with Voyage AI’s Model Options
Vector search is often the first step in retrieval augmented generation (RAG) systems. In a previous post, we discussed the future of AI-powered search at MongoDB . At MongoDB, we’re making it easier to select an embedding model so your search solution can scale. At scale, the choice of vector representations and dimensionality can have a significant impact on the cost and performance of a vector search system. In this blog post, we discuss options to reduce the storage and compute costs of your vector search solution. The cost of dimensionality Many MongoDB customers use vector indexes on the order of hundreds of gigabytes. An index’s size is determined by the number of documents and the dimensionality (or count of floating-point numbers) of the vector representation that encodes a document’s semantics. For example, it would require ~500 GB to store 41M documents if the embedding model uses 3072 dimensions to represent a document. At query time, each vector similarity computation will require 3072 floating-point operations. However, if these documents could be represented by a 512-dimensional vector, a similar index would only require 84GB of storage—a six-fold reduction in storage costs, as well as less computation at query time. In sum, the dimensionality of a document’s vector representation will directly affect the storage and retrieval costs of the system. Smaller vectors are cheaper to store, index, and query since they are represented with fewer floating-point numbers, but this may come with a tradeoff in accuracy. Put simply, an embedding model converts an input into a vector of fixed dimensions. The model was trained to ensure that vectors from similar documents are close to one another in the embedding space. The amount of storage and compute required for a vector search query is directly proportional to the dimensionality of the vector. If we can reduce the vector representation without compromising retrieval accuracy, our system can more quickly answer queries while using less storage space. Matroyshka representation learning So, how do we shrink vectors without losing meaning? One answer is Matroyshka Representation Learning (MRL) representations. Instead of reducing the vector size through quantization , MRL structures the embedding vector like a stacking doll, in which smaller representations are packed inside the full vector and appear very similar to the larger representation. This means we can select the level of fidelity we would like to use within our system because the similarity between lower-dimensional vectors approximates the similarity of their full-fidelity representations. With MRL representations, we can find the right balance of storage, compute, and accuracy. Figure 1. Visualization of Matroyshka Representation Learning. To use MRL, we must first select an embedding model that was trained for it. When training with MRL, an additional term is added to the loss function that ensures the similarity between lower-dimensional representations approximates the similarities of the full-fidelity counterparts. Voyage AI’s latest text embedding models— voyage-3-large , voyage-3.5 , and voyage-3.5-lite —are trained with MRL terms and allow the user to specify an output dimension of 256, 512, 1024, and 2048. We can use the output_dimension parameter to specify which representation we want to consider. Let’s see how the similarities among shorter vectors can approximate the similarities among full-fidelity vectors with voyage-3.5 : def cosine_similarity(v1,v2): magnitude_v1 = 0.0 magnitude_v2 = 0.0 dot_product = 0.0 for i,v in enumerate(v1): dot_product += v1[i]*v2[i] magnitude_v1 += v1[i]**2 magnitude_v2 += v2[i]**2 return dot_product/(math.sqrt(magnitude_v1)*math.sqrt(magnitude_v2)) # Calculating cosine similarities for MRL representations cosine_similarity(query[:256],relevant_doc[:256]) cosine_similarity(query[:256],non_relevant_doc[:256]) cosine_similarity(query[:512],relevant_doc[:512]) cosine_similarity(query[:512],non_relevant_doc[:512]) cosine_similarity(query[:1024],relevant_doc[:1024]) cosine_similarity(query[:1024],non_relevant_doc[:1024]) cosine_similarity(query,relevant_doc) cosine_similarity(query,non_relevant_doc]) We’ll use three MRL vectors, a query, a relevant document vector, and a non-relevant document vector. We expect the cosine similarity between the query and the relevant document vector to be larger than the similarity between the query and a non-relevant document vector. Cosine similarity measures the alignment between two vectors, where a high score indicates that the vectors point in the same direction in the embedding space. A score of 1.0 means the query and document vectors are identical, and a score of 0.0 means the vectors are orthogonal. Let’s see if that’s the case: Table 1. Similarity scores under several MRL sub-dimensions. The full-fidelity similarity scores can be approximated well with the 256, 512, and 1024 dimension vectors, so using all 2048 dimensions may not be necessary. For example, the full fidelity scores, 0.702 and 0.340, are close to the cosine similarities of the 512-dimensional representations, 0.704 and 0.346. This suggests that indexes built using the shorter vectors will have similar performance to indexes that use the 2048-dimensional vectors. MongoDB vector search collections. We will generate four vector search indexes, each with a different MRL configuration, and measure the retrieval performance on the dataset’s queries for each index (for existing vectors, we can build MRL indexes with Views ). We will examine the normalized discounted cumulative gain (NDCG) and the mean reciprocal rank (MRR). The results are below: table, th, td { border: 1px solid black; border-collapse: collapse; } th, td { padding: 5px; } Dimensions NDCG@10 MRR@10 Relative Performance Storage for 100M Vectors 256 0.703 0.653 0.963 102GB 512 0.721 0.672 0.987 205GB 1024 0.729 0.681 0.998 410GB 2048 0.730 0.682 1.000 820GB We can then analyze the plot of relative accuracy versus storage costs: Figure 2. Retrieval accuracy versus storage costs. The results indicate that for this corpus, we can represent documents with vectors of 512 dimensions, as the system provides retrieval accuracies comparable to those of higher-dimensional vectors, while achieving a significant reduction in storage and compute costs. This choice dramatically cuts the amount of storage and compute required for vector retrieval, so our system will provide the best retrieval quality for each dollar spent on storage, achieving ~99% relative performance at a quarter of the storage and compute cost. Faster and cheaper search This blog post demonstrates that we can easily assess shorter vector representations to reduce the cost of our vector search systems using MRL parameters exposed in VoyageAI’s models. Using retrieval quality analysis tools, we discover that a vector 25% the length of the full fidelity representation is suitable for our use case, so our system will be less expensive and faster. MRL options enable our customers to select the optimal representation for their data. Evaluating new vector search options can lead to improved overall system performance. We’re continuing to make it easy to tune vector search solutions and will be releasing additional features to tune and measure search system performance. For more information about Voyage AI's models, check out the Voyage AI documentation page . Join our MongoDB Community to learn about upcoming events, hear stories from MongoDB users, and connect with community members from around the world.
Rapid Prototyping a Safe, Logless Reconfiguration Protocol for MongoDB with TLA+
MongoDB provides high availability and fault tolerance using replica sets, which are a group of database servers that operate a Raft-like consensus protocol. Each database write operation is replicated in a sequential log (the oplog ) and applied to all replicas. The consensus protocol guarantees that once an oplog entry is committed on a majority of replica set nodes, the write will be durable even if some nodes fail. Over time, however, we may need to change the set of servers operating within a replica set, to remove or replace failed nodes, a problem known as dynamic reconfiguration . Reconfiguration is a critical operation within replica sets for dynamically expanding a cluster or replacing unhealthy nodes, so its correctness is crucial for enabling customer confidence in these operations and overall reliability within a replica set or sharded cluster. In 2019, we needed to implement a new, safe reconfiguration protocol with rigorous correctness guarantees. At the time, the MongoDB replication system had an existing, legacy reconfiguration mechanism, but it had several known correctness bugs which necessitated a new protocol design. Although the existing protocol had correctness issues, it also had some attractive design characteristics. In particular, it decoupled reconfigurations from the main database operation log and employed a logless design, storing configurations as single objects and replicating them between nodes in a gossip-based manner. Therefore, as part of our design process, we had a goal of developing a new, safe reconfiguration protocol while minimizing changes to this existing, legacy gossip-based reconfiguration protocol. We knew that dynamic reconfiguration protocols were notoriously difficult to design correctly, so we needed a design approach that would allow us to proceed efficiently and with high confidence. With the help of formal specification and model checking tools—specifically TLA+ and its model checker, TLC—we were able to embark on a process of rapidly developing the design of a new, safe, logless reconfiguration protocol in just a couple of weeks, and implementing it in production in a few months. In this post, we discuss our process of formally modeling the legacy reconfiguration protocol in TLA+, characterizing its bugs with a model checker, and iteratively developing modifications to lead to a safe, logless reconfiguration protocol design. There were a few key, high-level takeaways from our process. Most notably, rigorous, formal modeling didn’t slow us down, but instead accelerated design and delivery timelines while maintaining a high correctness bar. It also led to a simpler protocol design, allowing maintenance of a unified reconfiguration engine, rather than dealing with two parallel protocols, which could be prone to unexpected interactions and maintenance burden. The new protocol also provided novel performance benefits over standard reconfiguration approaches, due to the decoupling of reconfigurations from the main database log. Background and motivation The original MongoDB replication system used a legacy, gossip-based reconfiguration protocol that was fully decoupled from the main oplog. Each configuration was ordered by a numeric, monotonic config version, and nodes in a replica set learned the latest config from each other via periodic heartbeat messages. Upon learning of a higher config, it was immediately installed and took effect on that node. We refer to this original protocol design as logless, since it stored configurations as a single object and propagated them in a gossip-based manner, with no use of a sequential log for recording and replicating reconfiguration operations. This protocol also had a “force reconfig” feature, allowing users to install a new configuration even if a majority of nodes were offline. While the legacy protocol performed well in most scenarios, it was known to be unsafe in certain cases. Moreover, we expected reconfiguration to become a more common operation in MongoDB, necessitating the development of a new, safe reconfiguration protocol. Initially, we considered Raft's existing reconfiguration protocols , including its single-node reconfiguration protocol, which restricts reconfigurations to adding or removing a single server. The standard Raft approach, however, was ultimately deemed incompatible with "force reconfig," and would require maintenance of both a new, log-based implementation and the legacy, gossip-based one. It would also be complicated to ensure the two protocols didn’t interfere with each other. Instead, we hoped to develop a new protocol that minimized changes to the existing legacy protocol to simplify design and implementation. Ideally, we would be able to adopt ideas from Raft’s single-node reconfiguration protocol to our gossip-based, legacy reconfig protocol—which would allow for better compatibility with "force" reconfig, would be easier to upgrade and downgrade, and would eliminate the need for a new oplog entry format for reconfigurations. This idea of developing a safe, logless reconfiguration protocol seemed promising, as it would eliminate the need to mix two protocols and to share the basic mechanism for both normal and force reconfigurations. We needed, however, to be very confident in the correctness of such an approach, which was difficult to do manually and with a short design time frame. When we first pitched this idea early in the design process, it was unclear if such a solution was possible and whether it could be successful and implemented safely in production. There was some existing work on decoupling reconfigurations and on logless consensus , but none that directly applied to a Raft-based consensus system such as ours. Also, the discovery of a critical safety bug in one of Raft's reconfiguration protocols after its initial publication highlighted how challenging the task of designing or modifying reconfiguration protocols for consensus systems can be. This bug was only discovered over a year after Raft’s initial publication and required subtle protocol modifications to address. Around that time, in 2019, MongoDB’s replication team had had some past success with TLA+ and model checking on similar protocol design problems. Encouraged by these experiences, we set off to employ TLA+ and its model checker, TLC, to rapidly iterate on a candidate design and to develop a safe, logless reconfiguration protocol design that was simpler, easier to implement, and which provided novel performance benefits. Modeling the legacy protocol We were focused on developing a reconfiguration protocol that minimized design changes to the existing system, so we started by developing a TLA+ specification of the legacy reconfiguration protocol. This allowed us to characterize the flaws in this legacy protocol precisely and guide us towards modifications needed to make the protocol safe. To model the legacy, gossip-based protocol, we extended an existing TLA+ specification we had developed for an abstract version of the MongoDB replication protocol that did not include reconfiguration behavior. We extended this specification with two key reconfiguration-related actions: a Reconfig action, which represents the installation of a new config on a primary node, and a SendConfig action, which gossips a new config with a higher config version from one node to another. This model also defines the high-level safety properties of the protocol. The fundamental external guarantee is that when a majority write is committed on a replica set, the write will be durable as long as a majority of nodes are alive. This guarantee is largely captured in the LeaderCompleteness property, stating that any new leader in a higher term must contain log entries committed in earlier terms. Along with this, we also include a lower-level correctness property of Raft-based systems, ElectionSafety , which states that there can never be two primaries in the same term. Iteratively strengthening our reconfiguration rules Our legacy protocol model and its underlying correctness properties served as the starting point for a series of experiments, guided by the model checker, that iteratively led us towards a safe protocol design. We explored a series of design candidates by incrementally analyzing and refining our design in response to counterexamples discovered by the model checker. Single node changes One of the fundamental, challenging aspects of dynamic reconfiguration is related to the fact that the notion of “quorum” (i.e., majority) changes when the set of servers operating the protocol changes. For example, consider a reconfiguration that expands the protocol’s set of servers from C1={n 1 , n 2 , n 3 } to C2={n 1 , n 2 , n 3 , n 4 , n 5 }. Contacting a quorum in C1 may (correctly) contact servers Q1={n 1 , n 2 }, but a valid quorum in C2 may be Q2={n 3 , n 4 , n 5 }, which is problematic since Q1 and Q2 do not intersect, a key property of all quorums in standard Raft (and most other practical consensus protocols). Raft’s single-node approach attempts to partially address this by restricting configuration changes to those that add or remove a single node, which enforces overlapping quorums between such configurations. So we started by considering a basic initial question: does enforcing single-node changes partially address the safety issues of the legacy protocol? We had expected this would not be a fully sufficient condition for safety, but it was a stepping stone towards safer protocol revisions, and we wanted to confirm each of our hypotheses along the way. We introduced the single node change rule in the Reconfig action, which ensures that any majority of nodes in the old config and any majority of nodes in the new config share at least one common node. In our specification, we employed a slightly generalized definition of this property, which allows reconfigurations between any nodes where majority quorums overlap, even if not strictly a single-node change (e.g. all majority quorums of C1={n 1 , n 2 } and C2={n 1 , n 2 , n 3 , n 4 } intersect, but you cannot move from one to the other via a single addition/removal). One of the benefits of specifying the protocol in a high-level, mathematical specification language like TLA+ is that it enables concise definition of these kinds of properties, as seen below. After adding this condition to our Reconfig action, TLC was able to produce a violation trace for this updated protocol in a few seconds, and this bug was clear to understand, as shown below (only modified variables are shown in each state): Essentially, single-node changes only guarantee safe quorum intersection between adjacent configurations, but a series of locally adjacent reconfigurations may lead to a globally unsafe situation—i.e., two configurations that are both active but violate the quorum overlap property. This is demonstrated in the above trace concretely, and leads to a violation of the ElectionSafety property, with two nodes acting as primary in the same term in State 6. Node n 1 was safely elected in configuration {n 1 }, but then two subsequent reconfigurations occur to move the system to {n 1 , n 2 , n 3 }, and n 2 is elected in this configuration with a quorum of {n 2 , n 3 }, with no intersection of the original quorum of config {n 1 }. Our initial expectation was that just adding the single-node change constraint would not be correct by itself, but it was reassuring to have the model checker confirm this with a counterexample in just a few seconds. This began to give us more confidence to iterate on a new protocol design, which we proceeded to develop over the next week or so, next moving on to understand a deeper investigation of protocol safety requirements. Config commitment rule Adopting the single-node change condition is straightforward, as it only requires verifying new configurations in a pairwise, local manner. As we saw above, though, it is still problematic to move through arbitrary sequences of overlapping configurations, so we need to take extra care to avoid these problematic cases. Our first hunch was to add an explicit notion of “config commitment” within the protocol, similar to the commitment rules of Raft. That is, restrict a reconfiguration from taking place until some appropriate commitment conditions have been satisfied. Intuitively, this would place restrictions on how quickly, for example, a primary could execute reconfigurations—i.e., it would prevent a primary from moving to a new configuration before an older, non-overlapping configuration was, in a sense, “deactivated.” One natural idea was to borrow some similar concepts from Raft on log commitment, adapted for our logless, gossip-based setting. After a few iterations, we developed the following additional preconditions for the Reconfig action: ConfigQuorumCheck : A quorum of nodes have the same config version as the primary executing the reconfig. TermQuorumCheck : A majority of nodes in the primary’s config have reached the term of the primary or newer. We modeled the protocol with these new TermQuorumCheck and ConfigQuorumCheck , and they were initially sufficient to rule out the counterexamples we encountered previously. They were not yet fully general to ensure safety, though, as we will see below, where we worked out a final solution for config commitment. Oplog commitment rule In addition to the "config commitment" idea, it is worth noting the relationship between the config and oplog caused by the divergence from Raft. Raft sequences a reconfiguration among other oplog entries, thereby establishing a strong implicit ordering among them. However, since the gossip-based reconfig protocol does not include the configuration as part of the oplog, there may be some implicit dependencies between oplog entries and configurations that are not accounted for. We had started to think about this interaction between oplog entry commitment and reconfiguration, and conjectured a few problematic scenarios that we were able to confirm with the model checker. An example of this problem is illustrated by the following, simplified error trace: The core issue here is that config C3={n 1 , n 2 , n 3 } (with version=3) is installed even though the entry <<1,1>> (index, term) that was committed in a previous configuration, C1={n 1 }, has not been committed in the current configuration, C2={n 1 ,n 2 }. Since quorums may not overlap for non-adjacent configurations (e.g., C1 and C3), by ensuring that the commitment of writes in a previous configuration is also guaranteed in the current configuration, we can "propagate" the durability guarantee of earlier configurations to the future. As a result, we need to explicitly check this property when accepting reconfiguration commands. The rules for accepting a new configuration now include this additional, newly developed precondition: This rule is about ensuring that durable, replicated log entries from older configs are transferred to newer configs, which must be upheld to ensure safe protocol operation over time. This feature is implicit in Raft reconfiguration due to the tight coupling of reconfigurations and the main operation oplog, but must be handled explicitly here due to the decoupled design. The config as logless state machine We were now confident that we had established strong rules to guarantee local quorum overlap, the proper sequential ordering of configs, and the appropriate transfer of oplog entries between configs. After re-checking our model with these new preconditions, though, the model checker discovered a new counterexample after running for several hours on a larger workstation. The following is a simplified version of this error trace: In this case, node n 1 executes a reconfig to Ca={n 1 ,n 2 ,n 3 }, but hasn't propagated it to any other nodes at state 3. Then, n 2 becomes the primary and reconfigures to config Cb={n 1 ,n 2 ,n 4 } in state 6. n 1 can then be elected in term 3 with quorum {n 1 ,n 3 }, and n 2 can be elected in term 3 with quorum {n 2 ,n 4 }, violating the ElectionSafety property. The problem in the above trace is that when n 2 moved to a new config, it should have ensured that, in the future, no leaders would ever be elected in “earlier” configs. It failed to do so and, in the last step, a quorum was then able to be formed in a config with version 2, leading to two active, non-overlapping quorums. A key here is that divergence between configs in different terms leads to the issue. That is, config commitment as we did above was sufficient for a sequence of reconfigs by a single leader, but not with concurrent leaders in competing terms. Figure 1. Concurrent configurations with non-intersecting majority quorums. After going through these counterexamples, we understood the problem more clearly and had a path to refine our correctness argument. We realized that agreeing on the configuration among nodes can be viewed as a separate kind of consensus problem, separate from the oplog consensus but with similar rules. In our system, the config itself can be viewed as a compacted (i.e., rolled up) replicated state machine (RSM) that does not require a log (i.e., it is “logless”), since explicit maintenance of config history isn’t needed and only the latest config takes effect. Propagating the config via heartbeats can be viewed as “appending” to the config log (e.g. as in Raft), and rolling back a config is never explicitly required—i.e., we always simply install a more up-to-date config. This config RSM already shares many similarities with the oplog RSM, such as term propagation. The similarity suggests that just using the config version to identify a config is not sufficient. Viewing the config as its own RSM, we need to assign the primary’s term to configs. The config term is then a separate property of the config, similar to how the oplog entry’s term is part of every oplog entry. Thus, a config should be defined and ordered by the tuple (configVersion, configTerm), analogous to how an oplog entry is identified and ordered by its (timestamp, term), with term being compared first, followed by timestamp/version. The elections of these two consensus protocols can then be merged together by adding a new rule that a voter checks if the candidate’s config is stale in addition to other checks. Moreover, we can borrow the definition of “commitment” from the oplog RSM to the config RSM. That is, when a config is propagated to a majority of nodes in the primary’s term, the config is committed. It also became clear that the RSM only moves ahead through committed configs sequentially - the config RSM can choose the next config and commit it only if its current one is committed. Putting it all together Our final protocol specification included all of the above preconditions and features, producing a version of the protocol which we refer to as safe, logless dynamic reconfiguration. We conducted final model checking runs for several cases over 20 hours, exploring over 800 million protocol states, with configurations of four and five servers, along with pen and paper explanations for the correctness of the final result. Note that, at a high level, we can understand dynamic reconfiguration protocols like this as needing to deal with two core conceptual aspects: (1) config deactivation and (2) state transfer. Our various config commitment rules combine to address the first, which is related to ensuring that different configs that diverge over time cannot both be concurrently active. Aspect (2) relates to the fact that various types of replicated, durable state within a configuration must be appropriately transferred over to newer configurations. This is what the oplog commitment rules address, as well as the rules for ensuring that the term state propagates appropriately between configurations. Once we had the abstract protocol ironed out and gained confidence in its correctness, we were ready to move forward swiftly to implementation, and completed it in the MongoDB replication system over the course of a few months. The protocol has been running reliably in MongoDB and in production for several years since its introduction, and the implementation and protocol were significantly simpler than our original design alternatives. Takeaways Overall, we were able to get a draft protocol in one week, and within two weeks we finalized the protocol and successfully passed correctness checks using the model checker. It was motivating to see our vague ideas turn into something tangible, and the successful outcome from this design phase gave us the confidence to move forward to the implementation phase. Model checking is an excellent tool for rapidly and precisely answering "what if" design questions. Our efforts also emphasized an important feature of lightweight, design-level formal methods techniques, which is about more than simply ensuring correctness of your system design. Rather, it enables the exploration of protocol optimizations at a level of aggressiveness and velocity that would typically be infeasible with manual design methods. From this perspective, we can view these formal methods tools as not only a means for improving correctness of our systems and protocols, but as a means for efficient exploration of the optimization design space while maintaining a high correctness bar. This also speaks to the potential value of investing some amount of time upfront in models for key protocols that are highly critical and may need to evolve over time. Due to our novel protocol design, the scope of the implementation changes also became much smaller. We delivered the project in three months with three to four developers, and "force reconfig" was implemented using the same mechanism with relaxed rules. Version upgrade/downgrade only involves a small on-disk format change of the config, avoiding switching between two different reconfig approaches. In addition, our approach also provided potential performance improvements. Specifically, the decoupled reconfiguration design can bypass the oplog to recover the system when the oplog becomes the bottleneck. Similar ideas have since been explored in other, recent reconfiguration protocols like Matchmaker Paxos . Since its introduction in MongoDB 4.4 in 2019, the new, logless reconfiguration protocol has proven to be reliable and has served as a solid building block for other features, such as automatically assigning new nodes votes only after their initial sync. There have been no significant protocol bugs discovered since its deployment, a testament to the value of these rigorous protocol design techniques. While we focused on the intuition of the new protocol and the experience of leveraging model checking in this article, our paper , published in OPODIS 2021, includes a much more detailed description of the reconfiguration protocol, and a formal safety proof was also published. The final versions of the specifications we developed and published can be found in this Github repository , as well as some of the original specs we used in the MongoDB repository .