How do we know that an algorithm satisfies the required properties? Because of concurrency, partial failures, and network delays, there are a huge number of potential states. We need to guarantee that the properties hold in every possible state and ensure that we haven’t forgotten about any edge cases.
One approach is to formally verify an algorithm by describing it mathematically and using proof techniques to show that it satisfies the required properties in all situations that the system model allows. Proving an algorithm correct does not mean its implementation on a real system will necessarily always behave correctly. But it’s a very good first step, because the theoretical analysis can uncover problems in an algorithm that might remain hidden for a long time in a real system and that come to bite you only when your assumptions (e.g., about timing) are defeated by unusual circumstances.
It is prudent to combine theoretical analysis with empirical testing to verify that implementations behave as expected. Techniques such as property-based testing, fuzzing, and deterministic simulation testing use randomization to test a system in a wide range of situations. Organizations such as Amazon Web Services, FoundationDB, and TigerBeetle have successfully used a combination of these techniques on many of their products.
Model checking and specification languages
Model checkers are tools that help verify that an algorithm or system behaves as expected. An algorithm specification is written in a purpose-built language such as TLA+, Gallina, or FizzBee. These languages make it easier to focus on an algorithm’s behavior without worrying about code implementation details. Model checkers then use these models to verify that invariants hold across all of an algorithm’s states by systematically trying all the things that could happen.
Model checking can’t actually prove that an algorithm’s invariants hold for every possible state, since most real-world algorithms have an infinite state space. A true verification of all states would require a formal proof, which can be done, but which is typically more difficult than running a model checker. Instead, model checkers encourage you to reduce the algorithm’s model to an approximation that can be fully verified, or to limit the execution to an upper bound (e.g., by setting a maximum number of messages that can be sent). Any bugs that occur only with longer executions would then not be found.
Still, model checkers strike a nice balance between ease of use and the ability to find nonobvious bugs. CockroachDB, TiDB, Kafka, and many other distributed systems use model specifications to find and fix bugs. For example, using TLA+, researchers were able to demonstrate the potential for data loss in viewstamped replication (VR) caused by ambiguity in the prose description of the algorithm.
By design, model checkers don’t run your actual code, but rather a simplified model that specifies only the core ideas of your protocol. This makes it more tractable to systematically explore the state space, but it risks that your specification and your implementation go out of sync with each other. It is possible to check whether the model and the real implementation have equivalent behavior, but this requires instrumentation in the real implementation.
Fault injection
Many bugs are triggered when machine and network failures occur. Fault injection is an effective (and sometimes scary) technique that verifies whether a system’s implementation works as expected when things go wrong. The idea is simple: inject faults into a running system’s environment and see how it behaves. Faults can be network failures, machine crashes, disk corruption, paused processes—anything you can imagine going wrong with a computer.
Fault injection tests are typically run in an environment that closely resembles the production environment where the system will run. Some even inject faults directly into their production environment. Netflix popularized this approach with its Chaos Monkey tool. Production fault injection is often referred to as chaos engineering, which we discussed in “Reliability and Fault Tolerance”.
To run fault injection tests, the system under test is first deployed along with fault injection coordinators and scripts. Coordinators are responsible for deciding what faults to execute and when to execute them. Local or remote scripts are responsible for injecting failures into individual nodes or processes. Injection scripts use many tools to trigger faults. A Linux process can be paused or killed using Linux’s kill command, a disk can be unmounted with umount, and network connections can be disrupted through firewall settings. You can inspect system behavior during and after faults are injected to make sure things work as expected.
The myriad of tools required to trigger failures make fault injection tests cumbersome to write. It’s common to adopt a fault injection framework like Jepsen to run fault injection tests to simplify the process. Such frameworks come with integrations for various operating systems and many prebuilt fault injectors. Jepsen has been remarkably effective at finding critical bugs in many widely used systems.
Deterministic simulation testing
Another formalization technique, which has become a popular complement to model checking and fault injection, is deterministic simulation testing (DST). It uses a similar state space exploration process to a model checker, but it tests your actual code, not a model.
In DST, a simulation automatically runs through a large number of randomized executions of the system. Network communication, I/O, and clock timing during the simulation are all replaced with mocks that allow the simulator to control the exact order in which things happen, including various timings and failure scenarios. This allows the simulator to explore many more situations than handwritten tests or fault injection could. If a test fails, it can be rerun since the simulator knows the exact order of operations that triggered the failure—in contrast to fault injection, which does not have such fine-grained control over the system.
DST requires the simulator to be able to control all sources of nondeterminism, such as network delays or thread scheduling in multithreaded code. One of three strategies is generally adopted to make code deterministic:
Application-level
Some systems are built from the ground up to make it easy to execute code deterministically. For example, FoundationDB, one of the pioneers in the DST space, is built using an asynchronous communication library called Flow. Flow provides a point for developers to inject a deterministic network simulation into the system. Similarly, TigerBeetle is an OLTP database with first-class DST support. The system’s state is modeled as a state machine, with all mutations occurring within a single event loop. When combined with mock deterministic primitives such as clocks, such an architecture is able to run deterministically.
Runtime-level
Languages with asynchronous runtimes and commonly used libraries provide an insertion point to introduce determinism. A single-threaded runtime is used to force all asynchronous code to run sequentially. FrostDB, for example, patches Go’s runtime to execute goroutines sequentially. Rust’s MadSim library works in a similar manner. It provides deterministic implementations of Tokio’s asynchronous runtime API, Amazon’s S3 library, Kafka’s Rust library, and many others; applications can swap in deterministic libraries and runtimes to get deterministic test executions without changing their code.
Machine-level
Rather than patching code at runtime, an entire machine can be made deterministic. This is a delicate process that requires a machine to respond to all normally nondeterministic calls with deterministic responses. Tools such as Antithesis do this by building a custom hypervisor that replaces normally nondeterministic operations with deterministic ones. Everything from clocks to network and storage needs to be accounted for. Once that’s done, though, developers can run their entire distributed system in a collection of containers within the hypervisor and get a completely deterministic distributed system.
DST provides several advantages beyond replayability. For example, Antithesis attempts to explore many paths in application code by branching a test execution into multiple subexecutions when it discovers less common behavior. And because deterministic tests often use mocked clocks and network calls, such tests can run faster than wall clock time. TigerBeetle’s time abstraction, for instance, allows simulations to simulate network latency and timeouts without actually taking the full length of time to trigger the timeout. Such techniques allow the simulator to explore more code paths faster.
The Power of Determinism
Nondeterminism is at the core of all the distributed systems challenges we discussed in this topic: concurrency, network delay, process pauses, clock jumps, and crashes all happen in unpredictable ways that vary from one run of a system to the next. Conversely, if you can make a system deterministic, that can hugely simplify things.
In fact, making things deterministic is a simple but powerful idea that arises again and again in distributed system design. Besides deterministic simulation testing, we have seen several ways of using determinism over the past chapters:
-
A key advantage of event sourcing (see “Event Sourcing and CQRS”) is that you can deterministically replay a log of events to reconstruct derived materialized views.
-
Workflow engines (see “Durable Execution and Workflows”) rely on workflow definitions being deterministic to provide durable execution semantics.
-
State machine replication, which we will discuss in “Using shared logs”, replicates data by independently executing the same sequence of deterministic transactions on each replica. We have already seen two variants of that idea: statement-based replication (see “Implementation of Replication Logs”) and serial transaction execution using stored procedures (see “Pros and cons of stored procedures”).
However, making code fully deterministic requires care. Even once you have removed all concurrency and replaced I/O, network communication, clocks, and random number generators with deterministic simulations, elements of nondeterminism may remain. For example, in some programming languages, the order in which you iterate over the elements of a hash table may be nondeterministic. Whether you run into a resource limit (memory allocation failure, stack overflow) is also nondeterministic.