How we use formal modeling, lightweight simulations, and chaos testing to design reliable distributed systems
Courier’s design illustrates why distributed systems need more than unit, integration, and chaos testing. Datadog combined formal modeling, lightweight simulation, and conventional testing to uncover system-level risks before implementation. The approach was especially important after the March 8, 2023 outage, which showed how locally reasonable decisions can produce severe global failures. ## Why Distributed Systems Require Additional Analysis - Distributed systems provide greater scale and availability, but introduce concurrency, coordination, and failure modes that are difficult to reason about intuitively. - Traditional tests operate at relatively low levels of detail and may miss high-level design flaws. - Formal models and simulations allow teams to evaluate system behavior during the design phase, before implementation choices become expensive to change. - Model checking exhaustively explores all states permitted by a design and verifies defined correctness properties. ## Formal Modeling and Lightweight Simulation - Formal modeling uses a high-level specification language to describe: - System components and their interactions - Allowed system states - Properties the system must satisfy - Lightweight simulation builds a replica that runs under controlled conditions to study statistical characteristics such as: - Latency - Cost - Scalability - Behavior under realistic workloads - Modeling verifies correctness but cannot fully assess performance-related concerns. - Neither technique validates the final implementation directly. - Keeping models and simulations synchronized with the production design adds maintenance overhead. - Datadog considered the additional effort worthwhile because Courier was foundational, needed strong reliability guarantees, and incorporated lessons from the 2023 outage. ## Courier’s Requirements Courier was created to replace a decade-old Redis-backed queuing system that had begun to face throughput, scaling, and durability limitations. Its main requirements were: - **Multi-tenancy:** Isolate teams and products so one tenant cannot significantly disrupt others. - **At-least-once delivery:** Messages must not be lost; they must be delivered and acknowledged or sent to a dead-letter queue. - **Graceful degradation and high availability:** Throughput should decline roughly linearly as compute capacity is lost, rather than collapsing entirely. - **Horizontal scalability:** Throughput should increase linearly as compute capacity is added. The graceful-degradation requirement directly addressed the March 8 outage, when lost compute capacity caused a disproportionate throughput failure. ## FoundationDB Sharding for Tenant Isolation - Courier uses multiple FoundationDB clusters. - Each tenant is assigned to a subset of clusters. - No two tenants share the exact same cluster subset. - The initial design used: - Eight FoundationDB clusters - Four clusters per tenant - A theoretical maximum of `8 choose 4 = 70` tenant assignments - If one tenant saturated or disabled its four clusters, other tenants would still retain access to at least 25% of the total cluster capacity. - This arrangement provided sufficient isolation for the intended workloads. ## Broker Layer and High Availability - A broker layer exposes gRPC APIs for: - Sending messages - Receiving messages - Deleting messages - Clients connect only to the brokers, which apply the tenant-sharding logic. - Brokers health-check FoundationDB clusters and remove unhealthy clusters from consideration. - Both brokers and FoundationDB clusters are deployed across three availability zones to improve resilience. Courier demonstrates that formal verification and simulation are valuable complements to implementation testing. For mission-critical distributed services, teams should validate both correctness and operational behavior early, while also using unit, integration, and chaos testing to verify the final system.
Read original(opens in new tab)