The Impossibility Tax — How Formal Proofs Clear the Design Space Before You Start

14 March 2026 • Yuriy Polyulya •

#distributed-systems #engineering-principles #trade-offs #formal-methods

---

The Design Space Problem

Every distributed system confronts the same structural question: what can this architecture actually achieve? The folklore answer — “pick 2 of 3” — is both wrong and unhelpful. Wrong because the actual result is not a menu: a network partition forces a specific binary choice between accepting stale reads or rejecting writes, not a free selection among three equal properties [2] . Unhelpful because it offers no vocabulary for the space between the extremes.

Architecture by Vibes — Case Study: Formal Boundary Analysis of a Multi-Region Rate Limiter. A platform team needs to enforce a global API quota: 1,000 requests per minute, applied uniformly across US-East and EU-West. The product requirement is three sentences: never permit more than 1,000 req/min globally, respond to every increment request within 50ms, and keep enforcing during network incidents.

A database was selected from a vendor comparison landing page — “globally distributed,” “multi-region active-active,” “serverless scale,” “zero operational overhead.” The team deployed it with default consistency settings and described the result as battle-tested. No one asked which corner of the design space the default settings occupied, because the marketing copy implied it occupied all of them simultaneously.

The defaults were eventual consistency with asynchronous cross-region replication — an AP position on the CAP spectrum, though nobody in the selection meeting had used those words.

The contradiction should have surfaced in staging. A one-hour partition injection test — splitting the staging cluster into two isolated halves using any network partition tool, driving load against both — would have revealed the AP position before a single line of production traffic ran. Both partitions would have accepted writes and diverged; the global rate would have exceeded quota; the test would have failed exactly as the production incident later did.

Instead, the contradiction surfaced in production. Three weeks post-launch: a 90-second trans-Atlantic BGP re-route. US-East and EU-West partitioned. Both regions kept accepting requests against their local counter state. Both independently approached 1,000 req/min. Total global rate at peak: 1,847 req/min.

The database behaved correctly — eventually consistent, exactly as configured. But “eventually consistent” means: accept writes during a partition, converge after. The product requirement meant: never exceed 1,000 req/min globally, partition or not. Different corners. Same database. No resolution.

The database did what it promised. “Architecture by vibes” means selecting a Pareto position — counter-accuracy coordinates, availability coordinates, latency coordinates — without ever reading those coordinates out loud. The vendor landing page implied all corners were occupied simultaneously. The BGP re-route revealed which one actually was. Production is not the measurement environment for CAP position. It is the anomaly detector that fires when staging missed something or requirements changed after deployment.

This post replaces the landing page with geometry. The rate limiter is the running specimen: each impossibility theorem removes a face from its design cube, and the achievable region that remains is the map the team should have read before the selection meeting.

The actual design space is a continuous region in multiple dimensions (consistency, availability, latency, throughput, fault tolerance). Its boundary is carved by impossibility theorems that remove specific corners, faces, or threshold cuts from the design cube. Each theorem excludes a specific region — not “you cannot have these properties simultaneously” in some vague sense, but “this specific combination of property values is provably unreachable.” Any algorithm claiming to reach it leads to a contradiction. Each theorem cuts out a different shape from the design space. CAP and SNOW each remove a single corner — the one point where all named properties are simultaneously maximal, which no real system can reach. FLP removes an entire face — the region where deterministic consensus completes with full liveness in a purely asynchronous network, a guarantee no protocol can provide. The availability coordination boundary (Proposition 5) draws a horizontal cut through the consistency axis — everything above causal consistency requires coordination, regardless of how the system is implemented. Physics makes other regions prohibitively expensive but not excluded by proof. The distinction matters: you can negotiate with physics; you cannot negotiate with a proof.

Each theorem creates an exclusion zone — a region permanently removed from the design space by the structure of logic, not by implementation limits. An exclusion zone is not a challenge to overcome. It is a coordinate that does not exist.

Engineers have cleared every other category of technical limit with enough cleverness, hardware, and time. Not these. Any algorithm claiming to cross an exclusion zone generates a formal contradiction — the proof does not care about implementation quality, infrastructure budget, or engineering seniority. Work aimed at an exclusion zone disappears into the proof; the destination point was never there to reach. The engineer’s job is navigation within the space that remains: knowing which walls are exclusion zones, which are protocol choices wearing constraint costumes, and how to move the operating point deliberately when the system evolves.

This post builds the geometric vocabulary. Two objects carry the entire argument: the achievable region (what you can reach) and the Pareto frontier (the boundary where genuine trade-offs live). Every impossibility theorem in this post carves an excluded corner from the achievable region. What remains — and where on its boundary you choose to stand — is the only engineering question that matters.

---

Framework Overview

Four proofs explain why the rate limiter above failed before the first line of code was written. CAP , FLP , SNOW, and HAT are not separate academic results — they are four exclusion results acting on the same achievable region, the shared geometric object representing every operating point your architecture can actually reach. A network partition forces a choice between counter accuracy and availability — CAP removes the partition-available corner. Any distributed algorithm that tries to reach consensus without a timing assumption may wait forever — FLP removes deterministic liveness. A serializable read that completes in one hop without blocking concurrent writes is impossible by construction — SNOW removes that operating point. Enforcing consistency above causal consistency always requires coordination — HAT limits coordination-free consistency below strict serializability. Together they eliminate the perfect corner. What survives is the Pareto frontier: the map every real engineering decision lives on.

This post builds the formal geometry of the distributed design space. Six definitions establish the core objects: the achievable region (Definition 1) is the set of operating points your architecture can actually reach; its Pareto frontier (Definition 2) is the boundary where every gain costs something else. Harvest and yield (Definitions 3–4) replace availability’s binary switch with two continuous, measurable quantities. The PACELC classification (Definition 5) names the trade-off stance in both the partition and normal-operation regime. The consistency level (Definition 6) orders the coordination spectrum from strict serializability down to eventual consistency.

Three further definitions (7–9) extend the binary network model to the continuous reachability function that gray failures require, introduce differential observability as the navigational instrument, and classify nodes on the resulting gradient.

Six impossibility propositions carve corners from that space by proof. Proposition 1 formalizes the CAP theorem as an excluded region in property space — no algorithm simultaneously guarantees consistency, availability, and partition tolerance. Proposition 2 bounds the harvest-yield operating envelope under node failures: $h \cdot y \leq (n-k)/n$ under equipartition, with separate corrections for data skew and traffic skew. Proposition 3 presents the FLP bivalence lemma at practitioner level and shows how Paxos and Raft bypass its liveness restriction by assuming bounded message delays (partial synchrony).

Proposition 4 states the SNOW impossibility for transaction protocols. Proposition 5 draws the HAT coordination boundary: no partition-available protocol can guarantee consistency above causal consistency. Propositions 1–5 assume binary reachability — a node is either up or partitioned. Proposition 6 extends the framework to the continuous failure model: under partial reachability $r \in (0,1)$ , the Pareto frontier contracts continuously with the reachability function, displacing operating points from the frontier into the interior without any binary threshold crossing — the formal basis for gray failure analysis. Together, these six results carve and continuously deform the boundary of the achievable region that every distributed system inhabits — the geometric object that replaces “pick 2 of 3” as the engineering mental model.

Concept	What It Tells You	Design Consequence	How to Locate Your System
CAP / Gilbert-Lynch	The perfect corner where consistency, availability, and partition tolerance are all maximal is excluded by proof	Every system chooses its partition behavior; not choosing is still a choice	Inject a network partition in staging; observe the outcome: stale read = AP, rejected write = CP. That is your actual CAP position — not your intended one
Gray Failure / Differential Observability	The CAP model assumes binary reachability; gray failures occupy $r \in (0,1)$ — the Pareto frontier contracts continuously as reachability degrades, with no binary threshold to fire	Classify nodes as healthy, gray-failing, or partitioned; gray-failing nodes require routing away, not leader election	Sample the differential observability vector $\mathbf{O}(i,t)$ on each heartbeat: health channel passes while heartbeat variance and replication lag diverge — that inconsistency is the gray failure fingerprint
Harvest/Yield	Availability and consistency are continuous quantities, not binary switches	Design the degradation curve deliberately, not by accident	Measure yield from client error rate and client-side timeouts — not server logs. Server 200s miss client aborts. Measure harvest by sampling response completeness against a known-complete reference. Lab: establish the known-complete reference by running the system against a clean replica set in staging; that baseline is what production anomaly detection compares against
PACELC	The latency/consistency trade-off is permanent, not only triggered during faults	Normal-operation consistency level is the most important design decision you make	Lab, not production: run two separate load tests in staging at identical offered load — one with synchronous replication, one with asynchronous. The P99 write latency delta is your EC cost; the stale-read frequency under sustained load is your EL cost. Production traffic variance is too noisy to isolate a 2–10ms delta between replication modes; a controlled load test is not
FLP	Consensus in asynchronous systems is impossible; every real consensus protocol adds timing assumptions	Your election timeout is a safety assumption, not a tuning knob	Document your election timeout as a formal architectural parameter with a justification: “we assume message delivery within T ms after GST.” If you cannot justify T, you do not know your liveness assumption
Pareto frontier	The boundary of what is achievable under your constraints	Move toward the frontier first; only then accept trade-offs along it	Lab, not production: in staging with failure injection active (partition injection, network delay injection), reduce coordination overhead by one step — weaken consistency level or lower replication factor. Run a CO-free load test. If throughput improves without consistency violations, you are interior. If violations appear immediately, you are on the frontier. Testing interior position in production risks discovering you were already on the frontier during an incident

Three symbols, used consistently across all six posts in this series. $\Omega$ names the achievable region ( Definition 1 ): the set of operating points your architecture can actually reach. $\mathcal{F}$ names the Pareto frontier of $\Omega$ : the boundary where every gain costs something. $\mathbf{T}$ names the cumulative tax vector: all coordination costs an operating point pays.

Successive posts add new components to $\mathbf{T}$ — a physics component, a logical component, a stochastic component, and a governance component — each formally defined in its respective post. Your system’s complete position is a point in $\Omega$ relative to $\mathcal{F}$ , paying the accumulated tax $\mathbf{T}$ .

Two refinements apply at the edges of the component taxonomy. The logical component extends to $(\beta, L \times p, O_{\text{protocol}}, \Delta T_{\text{merge}}, \Delta X_{\text{GC}})$ for conflict-free merge deployments where $\beta \approx 0$ and read-path merge cost is the dominant term. When a differential-privacy mechanism is deployed, the privacy budget $\epsilon$ applies as a hard floor constraint — an Assumed Constraint, not a component of $\mathbf{T}_{\text{stoch}}$ . $\mathcal{F}$ contracts inward as taxes accumulate; architecture changes expand it outward.

The design consequence column is the entire post compressed: every impossibility result removes a corner from the design space, and what remains is the achievable region. The boundary of that region — the Pareto frontier — is where every real system stands. Getting to the frontier is engineering improvement; moving along it is compromise. Not choosing where to stand is still a choice.

---

The Achievable Region

The first object is the design space itself — the formal language for every position a system can occupy within it.

The achievable region is every combination of consistency, availability, latency, and throughput that your system can actually reach given its architecture and deployment environment. Points outside this region are physically impossible — no tuning will reach them. Points inside it are reachable by adjusting configuration. The region’s shape is determined by your architecture and constrained by impossibility theorems — changing the architecture changes the region.

Definition 1 -- Achievable Region: the set of operating points reachable from a given architecture under its physical and logical constraints

Axiom: Definition 1: Achievable Region

Formal Constraint: Given a system configuration $\Sigma$ and network model $\mathcal{N}$ , the achievable region is the set of all objective vectors reachable by feasible operating configurations — protocol parameters, replication factors, and timeout values compatible with $\Sigma$ and $\mathcal{N}$ .

$$\Omega(\Sigma, \mathcal{N}) = \left\{ \mathbf{f}(x) = (f_1(x), \ldots, f_m(x)) \;\middle|\; x \in \mathcal{X}(\Sigma, \mathcal{N}) \right\}$$

Engineering Translation: The achievable region is your architecture’s performance envelope. Changing the protocol or topology changes the region’s shape; no tuning of configuration parameters reaches points outside it.

The rate limiter specimen. Concretely instantiated for the global counter: increment latency $l$ (ms per counter update, minimized) — what the 50ms SLA consumes. Counter accuracy $c_{\text{acc}} \in [0, 1]$ (fraction of enforcement decisions based on the true global count, maximized) — whether “allow” or “deny” reflects the actual world-state or a stale estimate. Availability $a$ (fraction of increments answered within the 50ms SLA during a US-EU partition, maximized). Counter drift $d$ (maximum over-admission above the 1,000 req/min limit per convergence window, minimized). The ideal point $(l=0,\; c_{\text{acc}}=1,\; a=1,\; d=0)$ is the perfect global counter: instantaneous, perfectly accurate, always available, zero over-admission. It is not in the achievable region. CAP removes the $(c_{\text{acc}}=1,\; a=1)$ face during partition; FLP removes deterministic convergence from the async model; SNOW removes the one- RTT serializable read-before-increment. What remains is the set of rate limiters that actually exist.

Abstracting from the rate limiter specimen to any distributed system: $c_{\text{acc}}$ and $d$ both express positions on the consistency axis — $c_{\text{acc}}$ measures accuracy of the current operating point and $d$ measures its drift cost — so both map onto the single consistency level coordinate $c$ ; throughput $t$ generalizes what the rate-limiter expressed as counter accuracy. The four principal axes of the achievable region correspond to quantities a load test can measure. Write latency $l$ (ms, minimized), consistency level $c$ (integer index 0–6 from eventual to strict serializable per Definition 5 , maximized), availability $a$ (fraction of correct responses during a network partition, maximized), and throughput $t$ (ops/sec at the operating node count, maximized). A design point is a vector $(l, c, a, t)$ . The ideal point $(l = 0,\; c = 6,\; a = 1,\; t = \infty)$ is excluded from the achievable region. As the four exclusion results above establish, each removes a different face of this corner from the design cube. Together they remove the ideal point entirely. Every operating point a real system can reach lies strictly inside the space bounded away from it.

The Pareto frontier is the boundary of the achievable region where improving one objective requires degrading another. A system operating in the interior has room for free improvement — reduce latency, increase throughput, or strengthen consistency without paying anything. A system on the frontier faces genuine trade-offs: every gain requires a corresponding loss. Movement toward the frontier is pure improvement; movement along it is compromise.

Watch out for: the achievable region is parameterized by the network model, and the network model is a runtime variable, not a fixed property. A region computed under partial synchrony contains consensus; the same region computed under the asynchronous model does not. Practical consensus protocols (Raft, Paxos, Zab) rely on timeouts for liveness — not safety. Safety invariants (quorum overlap, term numbers, log consistency) hold unconditionally across both models. If your system’s safety depends on a timeout, that is a design error: a long enough partition approaches asynchronous behavior, and safety would fail exactly when you need it most. The correct dependency: timeouts enforce liveness; quorums enforce safety. A network shift toward asynchrony removes liveness guarantees from your achievable region without touching safety guarantees.

In the idealized model — fixed topology, deterministic latency, constant $\kappa$ — $\mathcal{F}$ is a surface of zero thickness: each architecture maps to exactly one frontier curve. In a production environment, two effects degrade this picture. The first is positional: the system’s operating point oscillates as TCP retransmits extend write latency, GC pauses inflate round-trip times, and packet loss contracts effective quorum availability — the system drifts off its nominal coordinate transiently, then recovers when conditions stabilize. The second is structural: the frontier’s own location shifts as $\kappa$ varies with load distribution, co-tenant pressure, and deployment environment — a $\kappa$ measured in a clean load test may not match $\kappa$ under production jitter, and the frontier moves with it. Robust design accounts for both: a deliberate margin inward absorbs positional oscillation; capacity ceilings calibrated against the high end of the observed $\kappa$ range defend against structural drift.

Definition 2 -- Pareto Frontier: the boundary where every improvement on one axis requires a measurable cost on another

Axiom: Definition 2: Pareto Frontier

Formal Constraint: The Pareto frontier is the set of all operating points in the achievable region where no feasible configuration dominates — i.e., is at least as good on every objective and strictly better on at least one.

$$\mathcal{F} = \left\{ \mathbf{f}(x^*) \in \Omega \;\middle|\; \nexists\, x \in \mathcal{X} : \mathbf{f}(x) \preceq \mathbf{f}(x^*),\; \mathbf{f}(x) \neq \mathbf{f}(x^*) \right\}$$

Assumption: This definition treats $\mathcal{F}$ as a fixed surface under constant $\kappa$ and deterministic latency — the idealized commissioning model. In a live deployment, $\kappa$ varies with load distribution, co-tenant pressure, and deployment-environment jitter, so $\mathcal{F}$ is a ribbon rather than a line. The commissioning fit establishes the baseline position; later posts quantify how that position shifts under production conditions.

Engineering Translation: A system in the interior of $\Omega$ has free improvements available — you can gain latency, throughput, or consistency without trading anything. A system on $\mathcal{F}$ does not: every gain requires a corresponding loss, and that trade-off must be made deliberately.

---

CAP — The Excluded Corner

The most cited and most misunderstood result in distributed systems is the CAP theorem. Brewer’s 2000 conjecture was formalized by Gilbert and Lynch in 2002 [1] and self-corrected by Brewer himself in 2012 [2] . The folk version — “pick 2 of 3” — is wrong in every important way. The actual result is narrower, more precise, and more useful.

Proposition 1 ( CAP Boundary Condition — Gilbert-Lynch 2002). In the asynchronous network model, no algorithm implementing a read-write register can simultaneously guarantee all three of the following:

(C) Linearizability — every read returns the value of the most recent completed write

(A) Availability — every request to a non-failing node receives a response

(P) Partition tolerance — the system continues to operate correctly despite arbitrary message loss between nodes

Formally: under the Gilbert-Lynch asynchronous model, where C and A are binary properties (linearizability either holds or it does not; a response either arrives in finite time or it does not), CAP excludes the entire boundary face where both safety (linearizability, C=1) and liveness (finite-time availability, A=1) are deterministic during an active partition (P=1). The exclusion is not a halfspace constraint — it does not impose a linear inequality like $C + A \leq 1$ (which would incorrectly exclude achievable points such as $(C=0.6, A=0.6, P=1)$ ). Every point $(c, a, 1)$ with $c < 1$ or $a < 1$ remains in $\Omega$ . The continuous trade-off — the ability to operate at $C=0.99, A=0.999$ — emerges only when substituting semantic degradation (Harvest: returning partial results) or probabilistic timeouts (Yield: accepting non-response with bounded probability) for the strict binary Gilbert-Lynch properties. Under those substitutions the excluded region contracts toward the deterministic corner; under the original binary model, the entire face where both C and A are simultaneously at their deterministic maximum during P=1 is excluded.

Proof sketch -- CAP (Gilbert-Lynch 2002): why simultaneous consistency, availability, and partition tolerance is provably unreachable

Axiom: Proposition 1: CAP Boundary Condition (Gilbert-Lynch 2002)

Formal Constraint: In the asynchronous model, no read-write register replicated across two partitioned nodes can be simultaneously consistent and available. A client writes $v$ to $G_1$ ; all messages between $G_1$ and $G_2$ are lost; $G_2$ must respond (availability) but cannot return $v$ (partition prevents delivery) — violating linearizability. The contradiction removes the $(C=1, A=1, P=1)$ vertex from the achievable region. [1]

Engineering Translation: During a partition your system must choose: serve stale data or refuse to serve. There is no third option — and the choice must be an explicit design decision made before any partition occurs, not an emergency response during one.

Physical translation. Every database holds a position on the consistency-availability curve, determined either by deliberate design or by the defaults that governed initial deployment. During a partition, the system executes whichever choice was made — or was left unmade. The theorem does not say “pick 2 of 3” — perfect consistency and perfect availability cannot coexist during a partition, but every other combination is potentially reachable.

Four corrections to the folk version matter for engineering:

1. Partition tolerance is not optional. Partitions happen in every real network — between datacenters, between racks, between a node and its disk. The actual choice is consistency vs. availability during a partition, not whether to tolerate partitions at all.

2. Continuity requires Harvest and Yield — the Gilbert-Lynch properties are binary. The theorem operates on strictly binary C and A: a node either returns the most recent write or it does not; a response either arrives in finite time or it does not. The continuous trade-off space ($C=0.99, A=0.999$ ) becomes accessible only when C and A are re-interpreted as Harvest (fraction of complete results returned) and Yield (fraction of requests receiving any response). Under those substitutions real systems do live between the extremes; under the strict binary model, the entire deterministic boundary face at P=1 is excluded, not only a single corner.

3. The choice is per-operation, per-data-item. A single database can serve user profiles with eventual consistency and financial transactions with linearizability. The system-level CAP classification is a simplification.

4. The model is asynchronous-only. Under partial synchrony [9] , where message delivery is bounded after some unknown time, different results hold. Paxos and Raft operate in this model — not the asynchronous model where CAP lives.

    
    %%{init: {'theme': 'neutral'}}%%
flowchart LR
    PERFECT["Deterministic boundary face: C=1, A=1, P=1
excluded under binary Gilbert-Lynch model"]:::warn
    FRONTIER["Pareto Frontier"]:::root
    CP["CP region
Spanner, CockroachDB
Strong consistency"]:::leaf
    AP["AP region
Cassandra, DynamoDB
High availability"]:::leaf
    INTERIOR["Interior
free improvement available"]:::ok

    PERFECT -.->|"excluded"| FRONTIER
    FRONTIER --- CP
    FRONTIER --- AP
    INTERIOR -->|"improve toward frontier"| FRONTIER

    classDef root fill:none,stroke:#333,stroke-width:3px;
    classDef leaf fill:none,stroke:#333,stroke-width:1px;
    classDef ok fill:none,stroke:#22c55e,stroke-width:2px;
    classDef warn fill:none,stroke:#b71c1c,stroke-width:2px,stroke-dasharray: 4 4;

The perfect corner is excluded by proof. The frontier curves between CP systems (Spanner, CockroachDB — strong consistency, reduced availability under partition) and AP systems (Cassandra, DynamoDB — high availability, eventual consistency under partition). Interior systems have room to move without trade-offs; frontier systems do not.

Mental Model: The Fenced Face. Picture the design space as a unit cube with three axes: consistency, availability, and partition tolerance. Almost the entire cube is reachable — partial consistency, reduced availability, and limited fault tolerance are all achievable combinations. Under the strict binary Gilbert-Lynch model, the entire face of the cube where C and A are simultaneously at their deterministic maximum during a partition (the P=1 face at C=1 and A=1) is fenced off by the proof. Under Harvest and Yield, that exclusion contracts toward the corner: systems that return partial results (Harvest $<1$ ) or accept non-response with bounded probability (Yield $<1$ ) can approach the fence asymptotically. The Pareto frontier hugs that face: CP systems stand near the C=1 edge, trading availability during partitions; AP systems stand near the A=1 edge, trading consistency. The engineering question is not “can we reach the corner?” but “which edge of the frontier fits our fault tolerance requirements, and are we using Harvest or Yield to reach our operating point on it?”

A fifth correction for production: the partition model is binary, but failures are not. CAP’s proof conditions assume a partition is binary — messages either arrive or are lost. Production failures are rarely binary. A replica responding at $10\times$ its normal latency is reachable; it does not fire a partition detector. A network path with 5% packet loss reduces throughput without triggering TCP-level failure. These gray failures — components that degrade their performance contract without crossing any hard binary threshold — sit in the $r \in (0,1)$ band of a continuous reachability function. The binary CAP model provides no language for them — the CAP analysis above assumes binary partition. The harvest/yield framing and the continuous reachability model generalize to the $r \in (0,1)$ band; both are developed in this post.

---

Harvest and Yield — The Operational Framing

CAP classifies systems. It does not help you design degradation. Fox and Brewer’s 1999 harvest/yield model [3] provides the operational framing that CAP should have been — continuous quantities that measure exactly how a system degrades under faults.

Definition 3 -- Harvest: the completeness fraction of a single response, from empty to fully consistent

Axiom: Definition 3: Harvest

Formal Constraint: The harvest of a response is the fraction of complete data it contains:

$$h = \frac{\text{data in response}}{\text{complete data}} \in [0, 1]$$

$h = 1$ : full response, no degradation. $h = 0$ : empty payload (timeout or null). The value is continuous and independently observable per request.

Engineering Translation: A search returning 80 of 100 relevant documents has $h = 0.80$ — the system degraded, not failed. Harvest is observable from the client by comparing against a known-complete reference under identical queries; server logs cannot report it reliably.

Harvest measures completeness; yield measures success rate. Both are independently observable from the client side.

Definition 4 -- Yield: the fraction of requests successfully served under partial failure

Axiom: Definition 4: Yield

Formal Constraint: The yield of a system is the fraction of requests it successfully completes:

$$y = \frac{\text{requests completed}}{\text{requests attempted}} \in [0, 1]$$

$y = 1$ : all requests answered within SLA. $y = 0$ : fully unavailable. Harvest and yield are independent — a system under partition may maintain $y = 1$ by returning partial results ($h < 1$ ), or maintain $h = 1$ by rejecting unserviceable requests ($y < 1$ ).

Engineering Translation: The operating point on the $h \times y$ envelope is a design decision. If it was not made explicitly, the system chose implicitly when the first partition fired. Serve partial data to all users, or complete data to fewer users — configure the policy before the incident, not during it.

Measure yield from the client side — server logs systematically overestimate it under load, because a response received after the client has timed out and retried still registers as success.

Proposition 2 -- Harvest-Yield Envelope: the maximum joint completeness-availability product under k simultaneous node failures

Axiom: Proposition 2: Harvest-Yield Operating Envelope

Formal Constraint: Define an equipartitioned system as one where each of the $n$ shards holds exactly $1/n$ of the total data and receives exactly $1/n$ of the request traffic under nominal load. In such a system under $k$ simultaneous node failures, the achievable $(h, y)$ region satisfies:

$$h \cdot y \leq \frac{n - k}{n}$$

The boundary is achievable by two extreme strategies: pure harvest reduction ($h = (n-k)/n,\; y = 1$ ) or pure yield reduction ($h = 1,\; y = (n-k)/n$ ).

Engineering Translation: $k$ failures give a budget of $(n-k)/n$ to allocate between data completeness and request success rate. A 100-shard cluster losing 5 shards has 0.95 to spend: 95% data to all users, or 100% data to 95% of users. The split must be pre-configured — degradation policy set during an incident defaults to whichever behavior the system happens to exhibit first.

Proof sketch -- Harvest-Yield envelope (Fox & Brewer 1999): why the joint product of completeness and availability is bounded by the surviving node fraction

Axiom: Harvest-Yield Envelope — Fox & Brewer 1999

Formal Constraint: With $k$ shards down, at most $(n-k)/n$ of total data-request capacity survives. If every request is served ($y = 1$ ), each response can contain at most $(n-k)/n$ of the data. If every response must be complete ($h = 1$ ), only requests touching no failed shard can be served, giving $y = (n-k)/n$ under uniform access. The product $h \cdot y$ is bounded by surviving capacity. [3]

Engineering Translation: The uniform bound $1 - k/n$ assumes equal shard weights. Your actual harvest floor is $1 - \max_i P_i$ — set by your hottest shard. A shard owning 30% of the keyspace drops harvest to 0.70 when it fails, regardless of cluster size. Measure actual shard weights under production key distribution before publishing any harvest budget.

Under $k$ node failures, a system with $n$ shards has a budget of $(n-k)/n$ that it can spend on data completeness or on request completion — but not both simultaneously at full value. A 100-shard system losing 5 shards has a budget of 0.95: it can serve 95% of data to 100% of users, or 100% of data to 95% of users, or any combination where the product does not exceed 0.95. The degradation curve is a design choice, not a system property.

The bound $h \cdot y \leq (n-k)/n$ is valid only when every shard holds exactly $1/n$ of the data and receives exactly $1/n$ of the traffic — the equipartitioned assumption. In production, neither holds. Define the skew-adjusted harvest for a single node failure as $h_{\text{skew}} = 1 - P_i$ , where $P_i \in [0,1]$ is the fraction of state held by node $i$ . If your hottest shard owns 30% of the keyspace — common under any Zipf-distributed access pattern — losing it drops harvest to 0.70 regardless of whether $n = 10$ or $n = 1000$ . The formula says you lose $1/n = 0.1\%$ of harvest on a 1000-node cluster; your users experience 30% data loss.

On-call warning. The uniform bound $1 - k/n$ is a ceiling, not a floor. Your actual harvest floor is $1 - \max_i P_i$ — set by your hottest shard, not your cluster size. Measure $P_i$ per shard under your real key distribution before publishing any harvest budget.

The equipartitioned assumption fails on two independent axes. Data skew — covered above — shifts the harvest bound: hot shards own a disproportionate share of state, so losing one costs more data than $1/n$ predicts. Traffic skew shifts the yield bound through a separate mechanism. If shard $i$ receives fraction $q_i$ of all requests, failure of that shard cannot be routed around: the requests that would have hit shard $i$ have nowhere to go. Yield drops to $1 - q_i$ regardless of cluster size $n$ . A shard receiving 40% of all traffic produces $y = 0.60$ when it fails — not the formula’s $(n-k)/n$ prediction, which assumes each shard receives $1/n$ of traffic. On a 100-node cluster, the formula predicts $y = 0.99$ ; the actual yield is $0.60$ .

Watch out for: the envelope is a steady-state bound, not a dynamic model. The three degradation paths are not equivalent from a stability standpoint. Yield reduction — failing requests — triggers client retries. Under retry rate $\rho$ per failed request, effective offered load increases to approximately $\lambda / (1 - \rho(1-y))$ , where $\lambda$ is the original arrival rate. If this additional load drives the failure rate higher, yield collapses non-linearly — not sliding along the $h \cdot y$ curve but falling off it. This is a metastable failure [10] : the node failures that triggered the degradation may resolve, but the retry storm sustains the failure state independently. The system cannot self-recover by navigating back along the frontier; it is stuck below it.

Harvest reduction is structurally more stable from a protocol perspective: requests succeed at reduced completeness, no automatic retry load accumulates, and the queue drains at the normal rate. This stability is relative, not absolute. Serving partial data triggers a different amplification vector: clients that receive incomplete responses — a dashboard missing metrics, a feed with gaps — typically respond with manual refresh. Unlike protocol-level retries, these are human-initiated and not subject to backoff. At sustained high harvest reduction ($h < 0.8$ ), application-level refresh behavior can generate load amplification comparable to a protocol-level retry storm. The defense is edge-layer caching with a strict TTL — a CDN or API gateway that serves the cached partial result for 30–60 seconds prevents manual refresh from reaching the database at all. If your degradation policy defaults to yield reduction, you need an explicit circuit breaker — forcing $y$ to zero to drain in-flight retries — before recovery becomes possible. The choice between the paths is not symmetric: one is a managed trade-off, the other is a cliff edge.

    
    %%{init: {'theme': 'neutral'}}%%
flowchart LR
    START["k=5 failures, n=100 shards
budget = 0.95"]:::root
    HARVEST["Reduce harvest
h=0.95, y=1.0
partial data to all users"]:::ok
    MIX["Mixed reduction
h=0.975, y=0.975
h*y approx 0.95"]:::branch
    YIELD["Reduce yield
h=1.0, y=0.95
complete data, fewer users"]:::warn

    START --> HARVEST
    START --> MIX
    START --> YIELD

    classDef root fill:none,stroke:#333,stroke-width:3px;
    classDef branch fill:none,stroke:#ca8a04,stroke-width:2px;
    classDef ok fill:none,stroke:#22c55e,stroke-width:2px;
    classDef warn fill:none,stroke:#b71c1c,stroke-width:2px,stroke-dasharray: 4 4;

Starting from $k = 5$ failures in a 100-shard system, the 0.95 budget splits along three paths. Harvest reduction keeps the queue draining at moderate reduction levels; yield reduction risks an immediate retry storm. The paths are not symmetric — the rightmost path is a cliff edge disguised as a design option, and the leftmost path carries its own secondary risk at deep reduction.

Mental Model: Harvest and Yield as Two Valves. Picture the degraded system as a water main with two valves: one controls data completeness (harvest) and one controls request acceptance rate (yield). Under $k$ node failures, you must close the valves enough that their product equals the surviving capacity $(n-k)/n$ . You can close one fully and leave the other open, or partially close both — the budget constraint is the same either way. The asymmetry is downstream. Closing the harvest valve reduces data completeness but lets requests keep flowing to all users; the queue drains. Closing the yield valve fails requests, which causes users to hammer the valve trying to reopen it (retries), multiplying offered load and potentially collapsing the system below the frontier entirely. The right policy assigns which valve closes first before the fault occurs: harvest-first degrades gracefully at moderate reduction ($h > 0.8$ ); yield-first risks a metastable collapse that requires a circuit breaker to drain before recovery is possible. At deep harvest reduction the harvest valve can still induce application-level refresh amplification, but it remains bounded by session timeouts where yield-driven retry storms are unbounded by default.

Harvest and yield together complete the picture CAP leaves unfinished: they parameterize the Availability axis of the CAP triangle, turning the binary “available or not” label into a continuous operating envelope $(h, y) \in [0,1]^2$ . The PACELC partition stance encodes which endpoint of the harvest-yield budget you aim for during a partition: choosing Availability (PA) means holding $y = 1$ while accepting $h < 1$ — return partial data rather than block; choosing Consistency (PC) means holding $h = 1$ while accepting $y < 1$ — reject unserviceable requests rather than serve stale data. The binary PA-or-PC label is the design commitment that determines which axis of the continuous $(h, y)$ budget absorbs the degradation. What harvest and yield do not address is the Latency/Consistency axis — the trade-off that governs every request during normal, partition-free operation. That is what the EL side of PACELC formalizes next.

---

PACELC — The Hidden Continuous Tax

CAP describes what happens during a partition. Partitions are rare — most production systems experience them for minutes per year. The trade-off that dominates every other second of operation is latency vs. consistency, and CAP says nothing about it. PACELC fills that gap by parameterizing the interior of the CAP triangle — the region where partitions are absent and the only question is how much latency you pay for each consistency level you require.

Partition duration matters for CAP position choice. Gill et al.’s empirical study of datacenter network failures [11] found that the majority of link failures are short-lived: median duration under 1 minute, with a long tail of multi-hour events driven by device failures rather than link transients. This distribution significantly affects the practical weight of the CP vs. AP choice. A CP system that becomes unavailable during partition will be unavailable for the median partition duration — under a minute. An AP system that admits stale reads during partition will have stale state for the same median duration, then converge. For most workloads, these two behaviors are effectively equivalent at the median. The CAP choice becomes consequential at the tail: the rare multi-hour partition is where CP unavailability becomes a sustained outage and AP consistency divergence accumulates enough state to make convergence expensive. Designing your CAP position for the median partition duration optimizes for the unimportant case; designing for the tail is what Drift Triggers encode.

Definition 5 -- PACELC Classification: trade-off stance under partition (Availability vs. Consistency) and under normal operation (Latency vs. Consistency), extending CAP to cover the daily latency cost on every request

Axiom: Definition 5: PACELC Classification

Formal Constraint: The PACELC classification of a distributed system describes its trade-off stance in two regimes [4] :

If Partition (P): choose Availability (A) or Consistency (C). Else (E) during normal operation: choose Latency (L) or Consistency (C).

A system that chooses availability during partition and latency during normal operation is classified PA/EL. One that chooses consistency in both regimes is PC/EC. The latency/consistency trade-off in normal operation is not an emergency measure — it is a line item on every request: a linearizable write to a three-node Raft cluster requires at least one round-trip to a quorum before acknowledging regardless of network health. Representative system classifications:

System	Partition Behavior	Normal Behavior	Classification
Cassandra	Availability	Latency	PA/EL
DynamoDB	Availability	Latency	PA/EL
Riak	Availability	Latency	PA/EL
MongoDB < 5.0 (default: single-node acknowledgment)	Availability	Consistency	PA/EC
MongoDB 5.0 and later (default: majority-quorum acknowledgment)	Consistency	Consistency (writes) / Latency (reads)	PC/EC (writes) / PC/EL (reads)(*)
VoltDB	Consistency	Consistency	PC/EC
PostgreSQL (sync replication)	Consistency	Consistency	PC/EC
CockroachDB	Consistency	Consistency	PC/EC
Spanner	Consistency	Consistency	PC/EC

(*) MongoDB 5.0 and later cannot be placed in a single PACELC cell. The partition behavior is PC: a primary that cannot reach a quorum majority steps down rather than acknowledge writes. The normal-operation behavior splits by operation type: writes require quorum acknowledgment (EC), but reads default to local consistency — returning the local replica’s value without waiting for majority acknowledgment (EL). Treating the write path as representative gives PC/EC; treating the read path as representative gives PC/EL. Neither is wrong — they describe different default operations on the same system.

Engineering Translation: CAP governs the partition regime only; PACELC governs both. The normal-operation column — the E/L vs. E/C choice — determines the performance characteristics users experience 99.9% of the time and is the more consequential design decision, yet CAP never mentions it. Record both PACELC cells on the birth certificate alongside $\kappa$ and $\beta$ . For systems with per-operation consistency knobs (Cassandra ONE/QUORUM, DynamoDB eventually vs. strongly consistent reads, MongoDB readConcern), the classification is per-default-configuration — the birth certificate entry should name the specific default, not just the system.

This is a limitation of PACELC, not a quirk of MongoDB. PACELC assigns one cell per system, which works cleanly for systems with uniform consistency behavior across operation types. It struggles with any system that exposes per-operation consistency knobs — Cassandra (ONE vs. QUORUM reads), DynamoDB (eventually consistent vs. strongly consistent reads), and MongoDB all land in different PACELC cells depending on which default you treat as the system’s representative stance. For these systems, the more useful question is not “which cell?” but “what is the default operating point and what does moving the knob cost in latency?” — which is the Pareto frontier framing this series uses.

Physical translation. CAP tells you what happens during a partition; PACELC tells you what you pay all day, every day. The latency tax on linearizability is not an emergency measure — it is a line item on every write. A PA/EL system (Cassandra, Riak) accepts weak consistency for low latency in both regimes; a PC/EC system (CockroachDB, Spanner) accepts higher latency for strong consistency in both. The normal-operation column — the E/L or E/C choice — determines the performance characteristics users experience 99.9% of the time; it is the most consequential design decision, yet CAP never mentions it.

Watch out for: the PACELC classification is per-system and per-default-configuration. It is designed for systems with a uniform consistency stance across operation types. For systems with per-operation consistency knobs — MongoDB, Cassandra, DynamoDB — the classification is underdetermined: you get a different cell depending on which default you treat as representative. This is not a deficiency in those systems; it is a structural limitation of a framework that assigns one cell to a system that deliberately exposes a knob. The table entry above makes the split explicit rather than forcing a single cell.

---

FLP — Why Consensus Is Impossible

The CAP and PACELC results bound the consistency-availability-latency space. A deeper result bounds what distributed systems can compute: the FLP impossibility theorem [5] , awarded the Dijkstra Prize in 2001, proves that no deterministic protocol solves consensus in an asynchronous system — even if only one process can fail.

The rate limiter makes the core problem tangible. The US-East shard runs a Raft leader for the distributed quota counter. When the leader has been silent for an interval approaching $T_{\text{election}}$ , each follower must decide independently: did the leader crash, or is the heartbeat still in transit? Both are locally indistinguishable. Both outcomes — start an election now, or wait longer — remain valid from the follower’s perspective. That moment of indistinguishability is what FLP formalizes as bivalence: the protocol is in a state where both decision values (0 = wait, 1 = elect) are still reachable through some valid execution. A deterministic protocol must eventually break the tie — but an adversary controlling network timing can always delay the next message by exactly the right amount to keep the configuration bivalent one step longer. No timer setting eliminates this: the adversary simply delays the message past whatever threshold the protocol uses. Raft’s election timeout is not a solution to bivalence — it is the engineer’s decision to stop waiting at a specific point and commit to “crashed” even though “delayed” remains logically possible. That commitment costs a potential spurious election; the cost of not committing is indefinite blocking of quota enforcement.

Proposition 3 ( FLP Bivalence Lemma — Fischer, Lynch, Paterson 1985). In an asynchronous distributed system (messages are eventually delivered but with unbounded delay), no deterministic protocol solves binary consensus if even one process may crash-fail. Formally: every such protocol has an admissible execution that never terminates.

The argument proceeds through the concept of bivalence:

• A configuration is bivalent if both outcomes (0 and 1) are still reachable from it through some admissible execution
• A configuration is univalent if only one outcome is reachable — the decision is forced

Proof sketch -- FLP bivalence (Fischer-Lynch-Paterson 1985): deterministic consensus impossible in async systems

Axiom: Proposition 3: FLP Bivalence Lemma (Fischer-Lynch-Paterson 1985)

Formal Constraint: Three steps establish impossibility. (1) Any initial configuration is bivalent — one silent process makes “decided 0” and “decided 1” both reachable from the start, because a silent-before-sending crash is indistinguishable from a late-sending one. (2) Every bivalent configuration has an adversary-chosen event delivery order that keeps the outcome bivalent — applying any message delivery $e$ can always be arranged to reach another bivalent configuration rather than forcing a decision. (3) An adversarial scheduler chains these together: infinite admissible execution, never univalent, never decides. [5]

Engineering Translation: Deterministic consensus is impossible in the asynchronous model because a slow process and a crashed one are indistinguishable without timing bounds. The practical exit is partial synchrony: commit to a timeout $T_{\text{election}}$ as your bound assertion. Safety holds unconditionally via quorum overlap; liveness holds when $\delta < T_{\text{election}}/2$ . When the assertion is violated — GC pause, brownout — the system halts safely rather than guesses.

From impossibility to engineering: the partial synchrony assumption. FLP ’s proof operates in the asynchronous model: messages are eventually delivered but with unbounded delay. The adversary controls timing — no deterministic algorithm can distinguish “this process crashed” from “this message is still in transit.” The practical exit is to change the model. The FLP adversary maintains bivalence by controlling message timing indefinitely — delay any message long enough and the protocol cannot distinguish a slow process from a crashed one. Remove unbounded delays and the adversary loses the tool: it can no longer keep the outcome undecided once timing is constrained.

Dwork, Lynch, and Stockmeyer (1988) [9] introduced partial synchrony: there exists a Global Stabilization Time (GST) after which all message delays are bounded by some unknown constant $\delta$ . Before GST the network behaves asynchronously; after GST timing bounds hold. The key word is exists — GST is not known in advance and $\delta$ is not known in advance. The model only asserts that both will eventually materialize.

This single assumption unlocks consensus, but with a precise cost. FLP shows liveness cannot hold in the asynchronous model. Partial synchrony splits the problem into two independent halves:

Property	Asynchronous model	Partial synchrony (after GST)
Safety — no two nodes commit conflicting values	Holds unconditionally	Holds unconditionally
Liveness — progress is eventually made	Impossible ( FLP )	Holds when $\delta < T_{\text{election}}/2$

Safety in Raft rests entirely on quorum arithmetic: vote uniqueness, quorum intersection, log completeness on election. None of these reference time — they hold regardless of message delay. Liveness requires that after GST a follower detects leader absence within $T_{\text{election}}$ and wins an election, which requires message delivery bounded by $\delta < T_{\text{election}}/2$ .

Raft and Paxos do not solve FLP — they take a side. The safety column of the table above holds unconditionally in both models: no timing assumption, no GST required. A Raft cluster with a partitioned network, a crashed leader, or a brownout will not produce conflicting committed values. It may stop producing values. That halt is correct behavior — the protocol honoring its commitment to safety by refusing to decide under indistinguishable conditions. The ‘No’ of FLP is not a wall but a fork: safety without liveness is achievable; liveness without safety is not. Every consensus deployment is this choice made concrete — and partial synchrony is the model that makes the choice tractable.

Partial synchrony does not eliminate uncertainty; it defers it. Before GST, the asynchronous adversary controls everything and FLP applies. After GST, the engineer controls the timeout, and engineering begins. Setting $T_{\text{election}}$ is the moment engineering enters: a bet that $\delta < T_{\text{election}}/2$ will hold often enough for the system to make progress. The bet is usually correct. When it is not, the system halts rather than corrupts.

The timeout as a formal commitment. Setting $T_{\text{election}} = 500$ ms is the engineer’s operationalization of the partial synchrony assumption: “We assert that after GST, message delivery delays are bounded by $\delta$ , and $T_{\text{election}} > 2\delta$ .” If this assertion holds, Raft guarantees liveness: a stable leader will be elected, entries will be committed. If this assertion is violated — a cloud brownout elevates RTT P99.9 above $\delta$ , a JVM GC pause holds a heartbeat for $T_{\text{election}}$ — liveness fails and progress halts. Safety never fails: quorum intersection holds regardless of timing. This is not a workaround. It is a deliberate engineering compromise with formal semantics: during network instability the system prioritizes safety over liveness, stopping progress rather than risking conflicting commits. The timeout is the instrument of that choice.

The timeout as a Pareto frontier. Every setting of $T_{\text{election}}$ is a position on a two-dimensional trade-off: detection speed on one axis, false-positive election rate on the other. No setting dominates — shorter timeouts detect real failures faster but trigger spurious elections whenever a transient delay exceeds $T_{\text{election}}/2$ ; longer timeouts absorb transient delays but extend the unavailability window when a leader actually fails. The heartbeat interval is $T_{\text{election}}/10$ by Raft convention, so the timeout determines the gossip rate too — tuning $T_{\text{election}}$ moves the operating point on the frontier; it does not move the frontier itself.

$T_{\text{election}}$	$\delta$ assertion	Protected against	Vulnerable to	Unavailability on real failure
50ms	$\delta < 25$ ms	Hard crashes only	Any GC pause, P99.9 spike	50ms + election round-trip
150ms	$\delta < 75$ ms	GC pauses under 75ms	Cloud brownouts	150ms + election round-trip
500ms	$\delta < 250$ ms	Most cloud brownouts	Extended partitions	500ms + election round-trip
2,000ms	$\delta < 1{,}000$ ms	Nearly all transient delays	Slow leader failure detection	2s + election round-trip

Each row in the table is an operating point on this frontier — a position an engineering team chooses, not discovers. A cluster running in a well-connected datacenter with modern hardware can afford 150ms and gains fast failure recovery. A cluster spanning regions with JVM-based nodes and potential GC pauses needs 500ms or higher. Neither is wrong. Both are deliberate navigation of the same trade-off surface that FLP forced into existence.

The partial synchrony model assumes $\delta$ is an unknown but fixed constant — the network transitions once from pre-GST asynchrony to post-GST bounded delays. In a degrading production network, the transition is not a step function but an oscillation: the network repeatedly satisfies and violates the $\delta < T_{\text{election}}/2$ bound at a rate proportional to instability. The distribution of message delays is fat-tailed, and each delivery whose latency crosses $T_{\text{election}}/2$ fires a spurious election. Election churn — re-election without leader failure, log reconciliation overhead, transient unavailability — is the continuous operational metric of how far the deployed network has drifted from its partial synchrony assumption.

Physical translation. Every production consensus protocol — Paxos, Raft, Zab, Viewstamped Replication — operates under partial synchrony, not the asynchronous model where FLP lives. A Raft cluster during a brownout that exceeds its $\delta$ assertion stops committing entries; it does not corrupt state. That is the intended behavior: safety preserved, liveness sacrificed, deliberately. Lease-based coordination is a distinct category where clock-drift violation is a safety failure, not a liveness failure.

Mental Model: The Undecidable Timeout. The FLP result rests on a single observation: in an asynchronous network, a slow process and a crashed process look identical to every other process. A message that has not arrived could still be in transit or could never arrive — there is no way to tell from the outside. This indistinguishability is the proof’s engine: an adversary controlling message timing can always arrange delivery to keep the outcome undecided indefinitely. The engineering response is not to solve indistinguishability — it is to commit to a belief at a chosen time. The election timeout $T_{\text{election}}$ is that commitment: “I will treat any process that has not sent a heartbeat in $T_{\text{election}}$ as crashed, whether or not it actually is.” Setting $T_{\text{election}} = 500$ ms is the assertion $\delta < 250$ ms — “after GST, messages arrive within 250ms.” If the assertion holds, the system decides. If it fails — brownout, GC pause, NTP slew — the system halts safely rather than guessing. The timeout does not detect crashes; it converts unbounded indistinguishability into a bounded, deliberate commitment. That commitment is the price of escaping FLP .

Watch out for: FLP applies only to deterministic protocols. Randomized consensus protocols (Ben-Or 1983) can achieve consensus with probability 1 in the asynchronous model. The randomization breaks the adversary’s ability to maintain bivalence indefinitely. This does not contradict FLP — it changes the model from deterministic to probabilistic termination.

Leases: A Distinct Safety Condition

The claim that safety is time-independent holds for consensus protocols. It does not hold for lease-based coordination. A lease grants a node exclusive rights for a bounded duration $T$ . Safety — no two nodes simultaneously hold a valid lease, and no two nodes simultaneously hold the leader role — depends on two physical assumptions: clocks advance monotonically, and clock drift between any two nodes is bounded by $\delta < T/2$ . If either condition fails — a VM pause, a process suspended across a checkpoint, NTP slewing a clock backward — a lease holder may continue serving requests after its lease has logically expired while a new grant has already been issued. Two nodes simultaneously believe they hold a valid lease. That is a safety violation, and it is a function of physical time, not quorum overlap. Spanner’s TrueTime addresses this directly: GPS and atomic clocks bound clock uncertainty to an interval $\epsilon$ ; commit-wait (holding a transaction open for $\epsilon$ before committing) converts the hardware time bound into an external consistency guarantee. Systems without TrueTime — etcd, CockroachDB range leases, Chubby — use conservative lease margins and grace periods to absorb drift, but cannot eliminate the physical-time dependency. The boundary: consensus safety rests on quorum intersection and is time-independent; lease safety rests on bounded clock drift and is not. If your system uses leases for leader exclusion, range ownership, or lock TTLs, the bounded-drift assumption is a safety precondition. Treat it as one.

---

Transaction Impossibility Boundaries

The preceding results bound individual operations: reads, writes, consensus decisions. Transactions compound the problem. Two results bound the transaction design space and complete the picture of what is excluded from the achievable region.

Definition 6 -- Consistency Level: position in the formal partial order from strict serializability to eventual consistency, where each step down trades a coordination round for reduced latency or metadata overhead

Axiom: Definition 6: Consistency Level

Formal Constraint: The consistency level of a distributed storage system is a position in the partial order defined by Viotti and Vukolic (2016) [8] , ranging from strict serializability (strongest — most coordination) to eventual consistency (weakest — least coordination). Each step down the order reduces the coordination required between nodes and increases the metadata overhead or semantic complexity needed to maintain correctness guarantees.

Level	Guarantee	Coordination cost	Representative systems
Strict serializability	Linearizable ops + real-time transaction order	Highest — quorum on every op	Spanner, CockroachDB
Serializability	Transactions appear serial (no real-time bound)	High — distributed locking or OCC	PostgreSQL (SSI), VoltDB
Snapshot isolation	Reads see consistent snapshot; write-write conflicts abort	Medium — version tracking	PostgreSQL (default), MySQL InnoDB
Causal consistency	Causally related ops seen in order by all	Low — vector clocks or DAG tracking	MongoDB causal sessions, COPS
Read-your-writes	A writer sees its own writes immediately	Very low — client session affinity	Most databases with sticky routing
Eventual consistency	Replicas converge; no ordering guarantee	None — async replication	Cassandra (ONE), DynamoDB (default)

The Highly Available Transaction ( HAT ) boundary sits between snapshot isolation and causal consistency — above it, coordination is unavoidable during a partition.

Engineering Translation: Each level in this table is a row in the consistency price list: a guarantee with a denominated coordination cost. The consistency tax function from Definition 14 prices each step in multiples of the cross-shard RTT floor $L$ . Strict serializability costs $3L$ per cross-shard write; eventual consistency costs $0L$ in coordination but $O(\text{replicas})$ in per-message metadata. The HAT boundary is not a performance concern — it is a hard structural line: any application requirement that demands snapshot isolation or stronger cannot be met without at least one coordination round per transaction, regardless of implementation cleverness.

The four-corner trap in practice. A user-profile service shards its database across two regional nodes — US-East holds credentials and subscription tiers; EU-West holds preferences and activity history. A profile read must query both shards and assemble a coherent snapshot. During a cache-miss storm — a nightly batch job invalidates 15% of profile cache entries — both shards suddenly absorb direct read load. The reads still land fast: 12ms and 14ms respectively, well inside the 50ms SLA. But between the two shard contacts, a concurrent write updates the user’s subscription tier on US-East. The assembled response sees the new tier from US-East and the old preferences from EU-West — preferences that reference a feature revoked with the tier downgrade. No error fires. The SLA is 26ms — a green dashboard. The client receives a structurally valid but semantically inconsistent response, and the failure surfaces two API calls later when the revoked feature check fails.

Making the read strictly serializable prevents this — but requires a coordination round before reading, adding one RTT per shard. At 12ms inter-region P99, that coordination blows the budget. The team wanted strict serializability, no blocking, one hop per shard, and concurrent writes — all four simultaneously. That combination does not exist.

The rate limiter makes the conflict concrete. Before admitting a request, the system must read the current quota counter across both regional shards — US-East and EU-West — while increment transactions from live traffic are simultaneously updating both counters. The design goal is four properties at once: a count that reflects reality across both shards (S — strict serializability), without holding up the ongoing increments while reading (N — non-blocking), in a single contact per shard to stay within the 50ms admission budget (O — one round-trip), and with live writes running throughout (W — write-compatible). All four feel necessary. Proposition 4 proves they cannot all hold simultaneously. The failure mode is exact: if the read contacts US-East and then EU-West sequentially without a coordination round, an increment can land on EU-West between the two contacts. The read sees US-East’s new counter and EU-West’s stale counter — the total is wrong, and no retry logic catches it, because the protocol never detected the inconsistency. Every read-only transaction protocol drops one of the four properties. The question is not whether to sacrifice one, but which one is least damaging for this specific workload — and whether the team knows which sacrifice they made. The bank balance version of the same problem (read-while-deposit-is-inflight) has the same four-corner structure, applied to a single-shard case: one of strict serializability, non-blocking, single-round-trip must give.

Proposition 4 (SNOW Impossibility — Lu et al. 2016). No read-only transaction algorithm can simultaneously achieve all four of the following properties [6] :

(S) Strict serializability — transactions appear to execute in some serial order consistent with real time

(N) Non-blocking — no transaction waits for another to complete

(O) One round-trip — each shard is contacted at most once

(W) Write-compatibility — the algorithm works correctly in the presence of concurrent write transactions

Any three of the four are achievable. All four are not.

Proof sketch -- SNOW impossibility (Lu et al. 2016): why strict serializable, one-RTT, non-blocking, and wait-free read-only transactions cannot all hold simultaneously

Axiom: Proposition 4: SNOW Impossibility (Lu et al. 2016)

Formal Constraint: A read-only transaction spanning two shards that must satisfy S (strict serializability), N (non-blocking), and O (one round-trip per shard) must read a consistent snapshot without coordination. A concurrent write modifies both shards between the transaction’s two shard contacts. Without a second round-trip (violating O) or blocking (violating N), the read cannot detect the inconsistency — violating S. Therefore $\{S, N, O, W\}$ cannot all hold simultaneously. [6]

Engineering Translation: Every read-only transaction protocol sacrifices one of the four. Name which one your protocol drops — accidental sacrifice is the most common source of invisible data races in distributed query systems. If you want single-hop reads alongside concurrent writes, choose between blocking and weakened serializability explicitly; the choice is yours only if you make it consciously.

Physical translation. If you want read-only transactions that are strictly serializable, non-blocking, and work alongside concurrent writes, you will need more than one round-trip per shard. If you want one round-trip, you must either block, weaken serializability, or restrict concurrent writes. Every transaction protocol makes this choice. Proposition 4 tells you which combinations are available and which are not — the transaction design space has a four-cornered exclusion, and your protocol stands in the region where one corner has been removed.

Two contrasting operations make the availability coordination boundary concrete before the proof. Adding an item to a shopping cart needs no cross-region coordination — if US-East and EU-West temporarily show different cart contents during a partition, they converge and neither customer loses an item. Reserving seat 14A on a flight cannot tolerate a stale read — two passengers boarding on the same seat is a correctness failure, not a temporary inconsistency that converges away. This boundary draws the formal line between these categories. Operations that naturally commute — add-to-cart, increment-counter, append-to-log — sit below it and need no coordination to be correct. Operations whose correctness depends on a globally consistent view — debit-exact-balance, reserve-specific-seat, compare-and-swap — sit above it and require at minimum snapshot isolation. That line is provable: no protocol can provide snapshot isolation while remaining available during a partition.

Proposition 5 ( HAT Coordination Boundary — Bailis et al. 2014). Every consistency level above causal consistency requires at least one cross-shard coordination round per transaction. No partition-available protocol can guarantee snapshot isolation or above; causal consistency is the strongest level achievable without coordination [7] .

Proof sketch -- HAT boundary (Bailis et al. 2014): why snapshot isolation requires at least one cross-replica coordination round and cannot be provided without it

Axiom: Proposition 5: HAT Coordination Boundary (Bailis et al. 2014)

Formal Constraint: Suppose snapshot isolation is achievable without cross-shard coordination. Write $W$ updates shards A and B atomically to $a'$ and $b'$ . Read $R$ reads $a'$ from A but the old $b$ from B — propagation to B is incomplete. Without a coordination round, $R$ cannot detect the cross-snapshot read, violating snapshot isolation. Repeatable Read, Serializability, and Strict Serializability impose stronger requirements and are excluded by the same argument. No partition-available protocol reaches snapshot isolation or above. [7]

Engineering Translation: Causal consistency is the strongest level available to partition-tolerant, always-available systems. Operations that commute (add-to-cart, append-to-log) stay below the boundary; operations requiring a globally consistent view (debit-exact-balance, reserve-specific-seat) cross it and must pay at least one coordination round. If your design claims snapshot isolation and partition availability simultaneously, one of those claims is false.

Bailis et al. (2014) map which consistency levels require coordination and which do not:

Achievable without coordination: Read Committed, Monotonic Atomic View, Read-Your-Writes, Causal Consistency

Requires coordination: Snapshot Isolation, Repeatable Read, One-Copy Serializability, Strict Serializability

This result draws a hard line through the consistency spectrum: everything at or above Snapshot Isolation requires coordination, meaning latency, reduced partition availability, and protocol complexity. Everything at or below Causal Consistency is available without coordination. If your application semantics are satisfied by causal consistency, you can have both high consistency and high availability. If they require serializability, you cannot.

Physical translation. Your application does not choose whether to coordinate — it chooses which operations must pay the coordination cost. Every operation whose correctness requires a globally consistent view (reserve a specific seat, debit an exact balance, compare-and-swap on shared state) must pay at least one cross-shard coordination round per transaction. That round-trip is not a protocol limitation — it is the price of the guarantee, and no implementation escapes it. Every operation that commutes naturally (add-to-cart, increment-counter, append-to-log) can be served without coordination and is available during a partition. Causal consistency is the ceiling of what you can hold without paying. If your application currently has no explicit consistency level, it has made this choice implicitly — almost certainly by accident.

Fault model boundary — crash-stop vs. Byzantine. The three theorems above assume a crash-stop fault model: nodes fail by stopping; they do not send malicious or conflicting messages. Byzantine faults — where nodes behave arbitrarily, including sending inconsistent messages to different peers — create additional and larger exclusion zones. Byzantine fault-tolerant consensus requires $3f+1$ nodes to tolerate $f$ failures (vs. $2f+1$ for crash-stop), contracting the achievable region: every point reachable under BFT assumptions is reachable under crash-stop, but not the reverse. The entire series assumes crash-stop. Systems where participants include externally-supplied components — third-party APIs, AI inference nodes, multi-tenant infrastructure — occupy an intermediate fault zone: components may return plausible but incorrect results rather than simply timing out. That intermediate zone has no single canonical theorem, but the engineering consequence mirrors BFT: tolerating it requires either redundancy above the crash-stop threshold, or external validation at the system boundary, priced as an additional coordination round outside the current tax map.

---

Gray Failures and the Continuous Achievable Region

The five propositions above assume binary reachability: a node either responds or it does not; a partition is present or it is not. This binary model makes the proofs clean. It is not the failure mode that kills systems processing tens of billions of transactions per day.

A gray failure is a component that degrades its performance contract without crossing any hard binary threshold — a network path dropping 5% of packets, a node returning correct data 94% of the time, a JVM replica pausing for 1.8 seconds every 12 seconds. The binary network model has no vocabulary for these states. The CAP proof requires messages to be delivered or not. The FLP adversary chooses to delay messages arbitrarily — but at any given instant the process is considered either reachable or crashed. Gray failures inhabit the space between those two values.

Definition 7 -- Gray Failure Reachability: the continuous link-reliability signal that replaces binary up/down with a probability of message delivery

Axiom: Definition 7: Gray Failure Reachability

Formal Constraint: Extend the binary network model by replacing $r(i,j) \in \{0,1\}$ with a continuous reachability function:

$$r: V \times V \times \mathcal{T} \to [0,1]$$

where $r(i,j,t)$ is the probability a message from node $i$ reaches node $j$ during interval $t$ , independently across attempts. $r = 1$ : fully reliable. $r = 0$ : classical partition. $r \in (0,1)$ : partially degraded. The achievable region under gray failure is $\Omega(\Sigma, \mathcal{N}(r))$ , reducing to the classical region at $r = 1$ . [12]

Engineering Translation: A JVM replica in a GC storm has $r \approx 0.85$ — reachable, health-endpoint green, yet degrading quorum success probability to $r^k$ per write. The binary failure detector cannot see this gradient. Measure $r$ per node-pair per heartbeat cycle; flag gradient onset before the binary detector fires.

Proposition 6 (Frontier Contraction under Partial Reachability). For a system at operating point $p \in \mathcal{F}(\Sigma, \mathcal{N})$ on the Pareto frontier under binary reachability, and for any $r \in (0,1)$ applied uniformly to quorum communication links, there exists a threshold $r^* \in (0,1)$ such that for $r < r^*$ , $p \notin \mathcal{F}(\Sigma, \mathcal{N}(r))$ : the operating point has been displaced into the interior of the achievable region by consistency violations the binary model cannot represent.

Proof sketch -- Frontier contraction (Proposition 6): how probabilistic link failure continuously shrinks the achievable region even when all nodes appear up

Axiom: Proposition 6: Frontier Contraction under Partial Reachability

Formal Constraint: Under strict serializability, a $k$ -of-$N$ quorum write requires all $k$ acknowledgments within timeout $T$ . Under partial reachability $r < 1$ , each acknowledgment arrives independently with probability $r$ , so quorum success probability is $r^k$ . At $k = 3$ , $r = 0.95$ : $r^k \approx 0.857$ — 14.3% of writes either time out or proceed on minority acknowledgment, violating the consistency guarantee. As $r$ falls continuously from 1, consistency violations increase continuously and the Pareto frontier contracts inward, even though architecture $\Sigma$ is unchanged.

Engineering Translation: At $r = 0.95$ on a Raft cluster with $k = 3$ , 14% of writes silently violate strict serializability while health endpoints return 200. The binary model cannot name this state. Track $r$ per node-pair per heartbeat cycle; the frontier is contracting continuously with it, and a Pareto Ledger entry calibrated at $r = 1$ is already stale.

Proposition 6 is the formal bridge between the binary impossibility results and production reality. CAP, FLP, and SNOW define the absolute maximum boundaries of $\Omega$ at $r = 1$ — the theoretically clean case where every message is delivered exactly once. Real systems operate with $r$ fluctuating between 0.99 and 0.9999; at $r = 0.95$ a system is not defying CAP, it is experiencing micro-CAP exclusions on 5% of its traffic, which its retry logic and consensus mechanisms average into a continuous latency penalty or error rate. The binary exclusion zones bleed outward into the achievable region as $r$ falls below 1, proportional to $1 - r^k$ .

Physical translation. The impossibility results in Propositions 1–5 remove fixed corners from the achievable region — regions excluded permanently by the structure of logic. Proposition 6 describes a different kind of exclusion: a frontier that contracts continuously as the reachability function degrades. The system does not fall off a cliff; it slides down a gradient. The binary failure detector fires at $r = 0$ ; Proposition 6 shows the damage accumulates well before that threshold.

The contraction follows the binomial tail distribution — for a $k$ -of-$N$ quorum with each link independently degraded to reachability $r$ , the probability of achieving quorum is $\sum_{j=k}^{N} \binom{N}{j} r^j (1-r)^{N-j}$ . Quorum success probability falls non-linearly: at $r = 0.95$ with a 3-of-5 quorum, quorum success probability is approximately 0.988; at $r = 0.85$ it falls to approximately 0.973. The system remains nominally within the strict-serializable region while silently delivering 6.1% minority-acknowledged writes — consistency violations the binary model cannot name. When the gray failure resolves and $r$ recovers to 1, the frontier re-expands. But the Pareto Ledger entry calibrated at $r = 1$ does not expire cleanly: it records the frontier position that was accurate when measured, not the position the system inhabits while gray failure is in progress. Staleness of the ledger is not a documentation failure — it is the direct consequence of operating on a dynamically contracting frontier with a statically recorded position.

The JVM garbage collection storm: a canonical gray failure. A Raft replica running on a JVM process enters a garbage collection storm: stop-the-world pauses of 1.8 seconds every 12 seconds. Between pauses the node processes requests normally — the health endpoint returns 200, the leader receives its heartbeat, writes are acknowledged. During each pause the node goes silent for 1.8 seconds. Its effective reachability from the leader’s perspective is $r \approx 0.85$ : messages sent during the 15% of time that coincides with a pause window are not delivered.

A binary failure detector configured with a 2-second timeout classifies the node as alive on almost every cycle. When a pause extends to 2.1 seconds, the detector fires a leadership probe. If a second replica is simultaneously in a GC pause, the leader loses quorum contact and initiates re-election. The cluster enters a churn cycle: re-election, log reconciliation, normal operation, pause, re-election. Write throughput collapses — not because any node has failed, but because the binary failure detector is generating false signal from a continuous degradation gradient.

The CAP and FLP models cannot represent this state. From their perspective the cluster oscillates between two discrete achievable-region points — fully operational and partitioned. From the gray failure model, the cluster has been at $r \approx 0.85$ on two links for hours. The binary model lacks the resolution to see the gradient; the binary detector produces the wrong response to it.

Differential Observability

Binary observability asks one question per node: up or down? The answer matches the binary network model. Gray failures require a vector instrument that tracks the rate of change of divergence across observation channels — not the absence of any single channel, but the inconsistency between them.

Definition 8 -- Differential Observability: the five-channel signal vector that detects gray failures invisible to binary health checks

Axiom: Definition 8: Differential Observability

Formal Constraint: For a node $i$ at time $t$ , the differential observability signal is a 5-component vector:

$$\mathbf{O}(i,t) = \bigl(h_i(t),\;\delta_{\mathrm{RTT}}(i,t),\;\delta_{\mathrm{lag}}(i,t),\;\delta_{\sigma\text{-hb}}(i,t),\;\delta_{\mathrm{gc}}(i,t)\bigr)$$

where $h_i(t) \in \{0,1\}$ is the health endpoint, $\delta_{\mathrm{RTT}}$ is the median RTT deviation from the P50 baseline over the prior hour, $\delta_{\mathrm{lag}}$ is the replication lag delta versus the peer median, $\delta_{\sigma\text{-hb}}$ is the heartbeat inter-arrival standard deviation over 100 samples, and $\delta_{\mathrm{gc}}$ is the GC pause rate per minute. A node is observably anomalous when any component exceeds its established threshold — not when the node becomes unreachable.

Engineering Translation: A JVM node in a GC storm has $h_i = 1$ (health endpoint returns 200) while $\delta_{\sigma\text{-hb}}$ shows a bimodal inter-arrival distribution and $\delta_{\mathrm{lag}}$ opens on a 12-second cycle. No single channel detects it; the vector’s inconsistency across channels is the fingerprint of gray failure. Arm threshold alerts on each component independently; require vector consistency before escalating to leader re-election.

A clean partition sets $\mathbf{O}$ to a boundary value instantly: all timing channels drop simultaneously. A gray failure grows the divergence gradually and selectively: $h_i$ remains 1 while $\delta_{\sigma\text{-hb}}$ climbs, $\delta_{\mathrm{lag}}$ opens on a fixed cycle, and $\delta_{\mathrm{RTT}}$ P99 diverges from P50. The JVM storm is unambiguous under this instrument: the health endpoint returns 200 throughout, but $\delta_{\sigma\text{-hb}}$ shows a bimodal inter-arrival distribution with a second mode at the nominal interval plus 1.8 seconds, and $\delta_{\mathrm{lag}}$ opens on a 12-second cycle. The inconsistency between the health channel and the timing channels is the fingerprint of a gray failure. One channel alone cannot see it.

Definition 9 -- Gray Failure Classification: three-state node health taxonomy (Healthy, Gray-failing, Partitioned) derived from the five-channel observability signal, enabling protocol responses calibrated to failure severity

Axiom: Definition 9: Gray Failure Classification

Formal Constraint: A node $i$ at time $t$ is classified by its observability signal $\mathbf{O}(i,t)$ as:

• Healthy: $\|\mathbf{O}(i,t) - \mathbf{O}_{\text{baseline}}\|_\infty < \theta$ — all five channels within threshold.
• Gray-failing: $h_i(t) = 1$ AND at least one timing component of $\mathbf{O}(i,t)$ exceeds $\theta$ — binary health check passes but timing signal diverges.
• Partitioned: $h_i(t) = 0$ AND all timing channels are silent — node is unreachable.

Engineering Translation: Gray-failing and partitioned nodes require categorically different protocol responses. A gray-failing node should be routed away from, have its quorum weight reduced, and trigger active diagnosis — but must not trigger leader election, which is the correct response to a partition and the wrong response to a JVM GC pause storm. A single binary health check cannot distinguish these two states. The five-channel vector from Definition 8 is the minimum instrument that separates them — without it, the protocol collapses three distinct operational states into two, and the response to one will be wrong for the other two.

Gray failures are not anomalous partitions. At systems processing tens of billions of transactions, gray failures — nodes slightly slow, links dropping fractions of packets, hardware degrading before it fails hard — are the normal operating condition. The impossibility exclusion zones hold unconditionally: CAP, FLP, and SNOW constraints are fixed by proof — those corners do not reappear under degradation. What shifts is the frontier’s own position within the achievable space. Proposition 6 contracts $\mathcal{F}$ as $r$ falls; independently, $\kappa$ measured at baseline may not equal $\kappa$ under gray failure conditions — elevated retransmits and GC pauses alter the coherency coefficient, moving $\mathcal{F}$ before the binary detector fires. The Pareto Ledger gains one new row: measured $r(i,j,t)$ per active node pair, updated on each heartbeat cycle, flagging gradient onset before the binary failure detector fires. Precision of position is the difference between a governance record and a production surprise.

---

Excluded Corners in Production

The impossibility results above define regions no implementation can reach. The rate limiter case study runs four of them to ground: not as an academic exercise, but as a formal boundary analysis of a system that was designed toward excluded corners and discovered it in production.

CAP — the consistent-available counter. The product requirement was explicit: accurate global counts AND available during network incidents. Gilbert-Lynch removes exactly this corner. A 90-second trans-Atlantic BGP re-route disconnects US-East from EU-West. A request arrives at US-East. The counter faces a binary choice. Contact EU-West before committing: block until the partition heals or the timeout fires — availability fails, the 50ms SLA is violated immediately. Commit locally without contacting EU-West: respond in 2ms, but EU-West’s local counter has not seen this increment — both regions simultaneously tally against their own local state, and the global count exceeds 1,000 req/min by whatever volume arrived in both regions during the partition window.

The default configuration was the second path. During the 90-second partition, US-East and EU-West each independently admitted traffic while their local tallies approached the limit. The over-admission was discovered in the next day’s billing reconciliation, not as a partition alert. The system was implicitly AP — availability chosen over accuracy — but the team had no circuit breaker on drift, no measurement of how far the counter could diverge, and no documented partition stance. CAP did not cause the billing anomaly. The team’s failure to commit to a partition behavior — and to bound the $d$ axis of the achievable region — caused it. Diagnostic: inject a 60-second US-EU partition in staging. Measure how far $d$ grows before convergence. That number is your AP price, and it should be in the ADR before the system ships.

FLP — the consensus counter. The first remediation: add distributed consensus. Every counter increment passes through a Raft quorum spanning both US-East and EU-West. Every decision is linearizable by construction; $c_{\text{acc}} = 1$ by definition. FLP has an opinion. In the asynchronous network model, no deterministic consensus protocol terminates on every execution. The adversary controlling message delivery delays the cross-Atlantic message: “message in transit or leader crashed?” is undecidable without a timing assumption. The team added one — election timeout of 3 seconds, chosen to absorb typical US-EU RTT variance. Any increment that cannot reach a cross-Atlantic quorum within 3 seconds blocks.

A cloud brownout elevated P99.9 trans-Atlantic RTT from 80ms to 3,200ms for 45 seconds. Every increment stalled. Zero over-admission. Zero admission. The fix for $d = 0$ produced $a = 0$ . The election timeout is the instrument of the liveness bet: “we assert P99.9 RTT stays below 1,500ms after GST.” When the assertion is violated, the protocol halts rather than over-admits — safety preserved, liveness sacrificed, by design. Whether that halt is useful depends on whether 45 seconds of zero admission is preferable to an unknown quantity of over-admission. FLP forced the choice into existence. The team’s failure to document the liveness assumption — and to define an explicit policy for which side of the $(a, c_{\text{acc}})$ trade-off to take under partition — meant the choice was made by the brownout.

SNOW — the serializable enforcement check. The second remediation: a read-before-increment transaction. Before admitting a request, read the current global count from both US-East and EU-West shards, verify the sum is below 1,000, then commit the increment. SNOW applies specifically to the read phase of this operation — and that phase is exactly a read-only transaction: a cross-shard count query that must be strictly serializable (S), non-blocking (N), complete in one round-trip per shard to fit the 50ms SLA (O), and compatible with concurrent write transactions (W). SNOW removes this corner for read-only transactions. The four-property vertex $\{S, N, O, W\}$ does not exist for the read phase; the subsequent write commits add coordination costs that SNOW does not govern, making the full read-write transaction strictly harder than the theorem’s boundary alone.

Under 800 req/sec, the read phase returned a sum that never reflected actual global state: US-East was read before a burst of 80 EU-West increments, EU-West was read after — the sum was 80 counts under-reported. The counter admitted traffic beyond the limit. This was not a bug in the write path. It was the SNOW theorem extracting its toll from the read-only sub-transaction: the team had inadvertently built a read-only quota check targeting the excluded corner. The fix required dropping O from the read phase: a second round-trip to confirm the count before committing the increment. Increment latency rose from 45ms to 115ms. The 50ms SLA was revised to 150ms. This is what moving along the frontier looks like: a constraint was relaxed, a corresponding guarantee was purchased, and the operating point moved to a coordinate that exists in the achievable region.

HAT — the coordination-free reconciliation. The third remediation introduced a background reconciliation job: every 5 seconds, US-East and EU-West exchange their local counter totals and negotiate a global view. The design goal was an “always available” job — it must never block, it must run during a partition, and it should require no distributed coordination overhead. That requirement set maps exactly onto HAT’s boundary condition. Bailis et al. prove that no protocol providing stronger consistency than causal can remain available during a partition. The reconciliation job discovered this empirically: attempting to produce a globally consistent snapshot (Snapshot Isolation) of both regions’ counters during a partition required a coordination round, which blocked. Dropping the requirement to Causal Consistency — “each region sees the other’s writes in order, but not necessarily immediately” — allowed the job to proceed without coordination. The trade-off: the reconciled count lags by up to the sync interval’s worth of increments before converging. That lag was documented and accepted; it replaced an implicit, undocumented over-admission window with an explicit, bounded one. The HAT boundary did not cause the problem. Targeting Snapshot Isolation without coordination — an excluded corner — caused it.

---

The Pareto Frontier as Unifying Object

The geometric picture before the formalism. Picture the design space as a four-dimensional space with axes: write latency $l$ (lower is better), consistency level $c$ (higher is better), availability under partition $a$ (higher is better), and throughput $t$ (higher is better). The ideal corner — $(l=0, c=6, a=1, t=\infty)$ — is the point where everything is perfect simultaneously. Every impossibility theorem is a proof that removes a face of this 4D design cube. What remains — the set of $(l, c, a, t)$ vectors your system can actually reach — is the achievable region. Its boundary is the Pareto frontier: a curved surface where every point is a genuine trade-off.

An engineer on the frontier, moving along it, trades one coordinate for another: strengthen consistency (raise $c$ ) and latency rises ($l$ increases), or increase throughput (raise $t$ ) and consistency weakens. There is no free lunch at the frontier — the curve’s shape encodes the exact exchange rates. An engineer in the interior, moving toward the frontier, is fixing interior waste: their system is below the surface because it is paying coordination costs that are not buying corresponding guarantees. Moving toward the frontier improves all objectives simultaneously — no trade-off required — because the system was not on the curve to begin with.

Theorem	Face removed from the design cube	What it looks like on-call
CAP (Gilbert-Lynch 2002)	$c=1$ AND $a=1$ face during partition — perfect consistency and full availability cannot coexist	Reads block or return stale data during an inter-DC BGP withdrawal; the response depends on partition stance you may not have documented
FLP (Fischer, Lynch, Paterson 1985)	Deterministic consensus AND full liveness face in the asynchronous model	A JVM GC pause that exceeds the election timeout triggers a spurious re-election; the system halts safely, but the timeout was a formal liveness claim you may not have measured against
SNOW (Lu et al. 2016)	$c=6$ AND one- RTT AND non-blocking face for read-only transactions	A read-only cross-shard quota check returns an internally inconsistent count because it cannot simultaneously be strictly serializable, non-blocking, and single-round-trip alongside concurrent increment transactions
HAT (Bailis et al. 2014)	Coordination-free face above causal consistency	Every consistency level above causal requires a network round-trip; there is no protocol trick that delivers Snapshot Isolation without quorum

Each impossibility result in this post carves an excluded region from the design space through a different geometric mechanism — vertex exclusion, face exclusion, and threshold cut, as detailed in the theorem sections above. Beyond the four impossibility results, harvest/yield bounds degradation under faults as a continuous envelope rather than a binary switch, and PACELC reveals that the latency/consistency trade-off is permanent, not only triggered during partitions.

The correct reading of every result above is this: an excluded corner is a geometric feature of the design space, not an engineering failure. CAP did not fail the team whose system blocked during a partition — it described the space their architecture inhabits. FLP did not fail the cluster that paused during a brownout — it described the liveness model they were operating in. SNOW did not fail the engineers who shipped a phantom read — it named the four-property corner they had inadvertently targeted. Impossibility is a physical property of the space. The team that interprets hitting a theorem as an indictment of past decisions has misread it. The theorem is a map. The architect’s job is to read it before designing, not after the postmortem.

The four results act on the same achievable region $\Omega(\Sigma, \mathcal{N})$ , not on separate frameworks. Their geometric structures differ: CAP and SNOW each remove a vertex from the design cube, FLP removes an entire face under the asynchronous model, and HAT draws a threshold through the consistency axis. Treating them as a uniform family of linear halfspace constraints would be formally incorrect; the actual structures are a vertex exclusion, a boundary exclusion, a combinatorial impossibility, and a discrete threshold. Their combined effect removes the ideal corner $(l=0, c=6, a=1, t=\infty)$ entirely. The Pareto frontier $\mathcal{F}$ of what survives is the only map worth reading.

Three kinds of movement are possible in this space:

Movement toward the frontier. Condition: $\mathbf{f}(x) \in \Omega(\Sigma, \mathcal{N}) \setminus \mathcal{F}$ — the system is in the interior, not on the frontier. Signature: there exists $x' \in \mathcal{X}$ such that $\mathbf{f}(x')$ Pareto-dominates $\mathbf{f}(x)$ — at least one objective improves with no other objective degrading. A system operating in the interior carries interior waste: coordination overhead that is not buying correctness, latency that is not buying consistency, replication that is not buying durability. Interior waste accumulates through unexamined defaults — consistency levels set by convention, replication factors chosen to match a past incident, election timeouts copied from a blog post. It is not a design failure; it is a measurement gap. In production it looks like this: a service using 5-way Raft replication for user-preference reads where read-your-writes semantics would suffice; a cluster running 60 nodes when the USL $N_{\max}$ is 18, actively degrading throughput with every pod the autoscaler adds; a distributed two-phase commit locking inventory for a transaction where only a single user’s session ever touches that row. None of these are visible from the architecture diagram. All of them are detectable with a single interior diagnostic experiment — reduce coordination overhead one step, measure for 15 minutes at production load, and observe whether throughput improves without violations. If it does, free improvement exists. Eliminating interior waste moves the operating point toward $\mathcal{F}$ without accepting any trade-off. It is always improvement, and it is the first obligation before any trade-off is considered — because accepting a genuine trade-off from an interior position means paying the cost of compromise without first claiming the free improvement that was already available.

Movement along the frontier. Condition: $\mathbf{f}(x) \in \mathcal{F}$ — the system is on the frontier. Signature: for every $x' \in \mathcal{X}$ that improves $f_i$ for some $i$ , there exists $j \neq i$ with $f_j(x') < f_j(x)$ — every gain requires a corresponding loss. Strengthening consistency from causal to linearizable increases coordination latency. Reducing replication factor decreases durability. These are genuine trade-offs at the boundary of what $\Sigma$ permits. This is the domain of architecture decisions.

Expansion of the frontier. Condition: a change from $\Sigma$ to $\Sigma'$ such that $\Omega(\Sigma', \mathcal{N}) \supsetneq \Omega(\Sigma, \mathcal{N})$ — the achievable region itself grows. Signature: operating points unreachable under $\Sigma$ become reachable under $\Sigma'$ , pushing $\mathcal{F}$ outward. This is qualitatively different from the first two movements: it is not parameter tuning within a fixed achievable region but an architectural change that redraws the region’s boundary. Adopting a new protocol, restructuring the network model assumption, or changing the replication topology are actions in this class. This is the most valuable engineering intervention — not choosing better among existing trade-offs, but making new operating points exist.

Frontier expansion: structural patterns. The definition above names expansion but does not give it a vocabulary. Four structural patterns account for most frontier expansions in practice.

Protocol substitution replaces a protocol with one that relaxes a specific coupling constraint while maintaining the same guarantee. Raft to EPaxos removes the single-leader throughput bottleneck at consistency level 6 without weakening consistency — same guarantee, larger throughput frontier. ReadIndex to lease reads removes the per-read quorum RTT at consistency level 6 given bounded clock skew — same guarantee, lower read-latency floor. The coupling constraint that was removed in each case is different (leader serialization; quorum-per-read), but the structure is identical: identify the constraint that sets the boundary, replace it with a mechanism that does not impose that constraint.

Workload decomposition splits a mixed workload so each operation class travels its own coordination path. A service enforcing linearizable consistency on every operation because payments require it pays that cost on catalog reads that only need causal consistency. Separating the two means each operation pays only the coordination cost its correctness requirement demands — the frontier for the composite workload expands because the binding constraint no longer applies uniformly. Flexible Paxos quorum asymmetry is the same pattern applied within a single protocol: shifting coordination weight from reads to writes expands the read-latency frontier without changing consistency. The signature: two or more operations previously constrained by the same coordination mechanism now inhabit different positions on the frontier simultaneously.

Axis elimination removes a coordination requirement entirely for a class of operations. Conflict-free merge structures eliminate write-time consensus for data types with a merge-compatible lattice — the write-coordination axis disappears from that data type’s cost structure, expanding the write-throughput frontier at that consistency level to effectively unbounded. Caching eliminates read coordination for stale-tolerant reads. The signature: a coordination type stops appearing in the cost structure for an operation class. Note that axis elimination never removes a cost — it relocates it. Conflict-free merge write-coordination cost moves to read-path merge and tombstone GC . The frontier expands on one axis and contracts or shifts on another.

Infrastructure investment shifts a physical constraint that appeared fixed. Reducing TrueTime’s $\epsilon$ from 7ms to 1ms expands the (latency, external-consistency) feasibility surface: operating points jointly infeasible under 7ms uncertainty become reachable at 1ms. RDMA lowers the RTT floor for all consensus-based protocols simultaneously. Clock infrastructure and network hardware are inputs to $\Omega$ ’s boundary, not fixed parameters of the problem.

When expansion is required vs. preferred. The decision between frontier expansion and along-frontier movement reduces to a two-stage test. First: does the desired operating point lie inside $\Omega(\Sigma, \mathcal{N})$ ? If no — if no configuration of the current architecture reaches it — expansion is necessary, not just preferred. No amount of tuning navigates to an excluded region; only changing $\Sigma$ can reach that point. Second, if the desired point is inside $\Omega$ but requires an along-frontier trade-off: compare the one-time migration cost of expansion, amortized over the system’s expected lifetime, against the ongoing per-operation cost of accepting the trade-off. A service paying 5ms of unnecessary latency per write indefinitely may find a protocol migration cheaper than that tax in perpetuity. The comparison must include the operability delta $\Delta O_{\text{protocol}}$ the new architecture imposes — a lower-$\beta$ protocol that doubles incident diagnosis complexity may not expand the effective frontier when the team’s $C_{\text{team}}$ ceiling is already near its limit. The formal criterion: prefer expansion when the desired operating point is unreachable, or when $\text{migration\_cost} + \Delta O_{\text{protocol}} \times \text{lifetime} < \text{trade-off\_cost\_per\_op} \times \text{op\_rate} \times \text{lifetime}$ .

Protocol coordinates on the map. The (l, c, a, t) framework becomes actionable when real protocols are placed in it as explicit points. Each entry is a specific protocol with a specific default configuration — a point in the achievable region, not a range.

Protocol / Mode	c	a under partition	l (write)	Position
Raft, single-DC RF=3	6 — strict serial	0.999 — CP: rejects writes without quorum	1–5 ms — 1 quorum RTT	Near frontier for c=6
CockroachDB default	6 — strict serial	0.999 — CP	5–15 ms — cross-range 2PC	On frontier; cross-shard beta visible
Spanner	6 — strict serial	0.9999 — multi-region CP	10–50 ms — TrueTime commit-wait	On frontier; highest l in class
Cassandra CL=ONE	1 — eventual	~1.0 — AP: always responds	< 1 ms — local write	Near frontier for c=1
Cassandra CL=QUORUM	4 — sequential	0.999 — degrades under partition	2–10 ms — quorum RTT	Often interior vs. Raft at same c
DynamoDB strongly consistent	4–5	0.999	5–10 ms	Near frontier for c=4–5
Riak r=quorum	2 — causal/RYW	~1.0	2–5 ms	Near frontier for c=2

A specific configuration is a point in the (l, c, a, t) space. The frontier for a protocol family is the set of best achievable (l, c, a, t) vectors across all valid configurations of that protocol. Raft’s frontier traces the CAP exclusion boundary at c=6: it extends from high-l/low-t (many nodes, high coordination) toward low-l/high-t (fewer nodes, less coordination), but it cannot cross into (c=6, a=1) — that face is excluded by proof. Cassandra CL=ONE navigates a different frontier entirely, at c=1, where the boundary extends much further in the a and t directions because coordination is absent. Choosing a protocol is choosing which frontier curve to inhabit. Configuration tunes your position on that curve. Cassandra CL=QUORUM sits in the interior relative to both neighbors: at the same consistency level as Raft, it has higher latency; at the same latency as CL=ONE, it has weaker throughput. CL=QUORUM is a configuration that satisfies neither objective as well as its neighbors on the frontier — an interior point with room to move in both directions.

Locating your system. The three movement types are only useful if you can determine which one applies to your system right now. The diagnostic is a single experiment: reduce coordination overhead by one incremental step — drop consistency from linearizable to causal for one operation type, reduce replication factor by one replica, or disable one synchronous cross-region write. Then measure: did throughput improve? Did latency drop? Did consistency violations appear? If throughput improved with no violations, you are interior — the frontier is further out than your current position and free improvement is available. If violations appeared immediately, you are on the frontier — any further relaxation costs correctness. If nothing changed, your bottleneck is not coordination; look elsewhere. This experiment is cheap to run in staging and provides more information about your system’s actual position than any amount of theoretical classification.

The $\beta$ coefficient is not an abstract parameter — it is measurable from a load test. Run your service at $N = 10, 20, 50$ nodes, measure throughput at each point, and plot the curve. If throughput grows sub-linearly and eventually turns over, you have a positive $\beta$ . The rate of turn-over tells you how fast your frontier is contracting with scale. The Physics Tax gives the full fitting procedure; the point here is that $\beta$ is an empirical number your team can own, not a theoretical construct.

A fourth dynamic the geometric picture omits: falling off the frontier. The Pareto frontier is computed for steady-state operation. It does not encode recovery cost — the work required to return to a given operating point after a perturbation drives the system away from it. Two points on the same frontier can be at the same (harvest, yield, latency) coordinates but have radically different stability properties. A yield-reduced point $(h=1.0, \; y=0.95)$ and a harvest-reduced point $(h=0.95, \; y=1.0)$ satisfy the same Pareto bound, but the yield-reduced point sits adjacent to the metastable region: if yield drops further, retry load can exceed available capacity and the system enters a state where the gradient back toward the frontier is reversed. Recovery from this state requires discontinuous intervention — circuit breaking, load shedding, rolling restarts — not smooth movement along the frontier.

The “Excluded” region in the CAP diagram therefore has two distinct components that the geometric picture conflates. The impossibility-excluded zone is the perfect corner that Gilbert-Lynch removes by proof — no architecture reaches it by design. The recovery-excluded zone is the region a system enters via metastable collapse — no architecture was designed to operate there, but systems drift in via positive feedback loops that the static frontier model cannot anticipate. The former is a design constraint; the latter is an operational failure mode. The Pareto frontier tells you where you stand; it does not tell you how far you are from the cliff.

The two zones interact with gray failure in structurally different ways. The impossibility-excluded zone is static — CAP, FLP, and SNOW remove fixed regions from $\Omega$ regardless of $r$ . The recovery-excluded zone is dynamic: degraded partitioned environments are almost never in steady state, and the metastable attractor’s depth depends on how far $r$ has fallen. Stateful protocol reactions compound this — TCP exponential backoff widens retry windows asymmetrically, Raft candidate storms accumulate log divergence that survives the gray failure’s resolution, and circuit breakers calibrated for binary failure thresholds miss the gradual degradation entirely. A system navigating gray failure at $r = 0.90$ is not 10% closer to the impossibility boundary — it is closer to the recovery-excluded zone along a second, independent axis: at $r = 0.90$ , quorum success probability falls to approximately 0.973 for a 3-of-5 group, a rate low enough to admit minority-acknowledged writes while keeping the binary circuit breaker silent, and high enough to feed retry accumulation that the detector cannot see.

Read the animation. The green dashed curve is the Pareto frontier at low coordination cost ($\beta = 0.001$ ) — a wide achievable region where high throughput and strong consistency coexist; as $\beta$ increases, the frontier contracts inward. This contraction is the coordination tax: $\beta = 0.001$ peaks around 32 nodes; $\beta = 0.01$ peaks around 10 — both within the range measured in production consensus-heavy systems. The “excluded” label marks the perfect corner that CAP removes by proof — unreachable regardless of $\beta$ . The Physics Tax shows how to read your system’s $\beta$ from a standard load test.

This geometric picture unifies every result in this post. Every impossibility result and every trade-off taxonomy acts on the same underlying object — the achievable region. Each one removes or prices a specific slice of that region: the partition trade-off, the consensus termination limit, the read-only transaction constraint, the coordination boundary, the harvest/yield degradation curve, the latency-consistency trade-off under normal operation. None of these are separate frameworks; they are cuts into the same design space from different angles. The Pareto frontier of what remains is the map.

Each result acts on a different part of the $(l, c, a, t)$ design space through a different exclusion mechanism, as established in the preceding sections. The diagram below maps each exclusion to the face of the ideal corner it removes. Their intersection removes the ideal corner $(l = 0, c = 6, a = 1, t = \infty)$ from the achievable region — not as a design choice but as a formal consequence.

    
    %%{init: {'theme': 'neutral'}}%%
flowchart TD
    ORIGIN["Ideal corner: l=0, c=max, a=1, t=inf
excluded by all impossibility results"]:::warn
    CAP_C["CAP: removes c=max and a=1 face"]:::leaf
    SNOW_C["SNOW: removes c=max, a=1, and l=single-RTT"]:::leaf
    FLP_C["FLP: removes deterministic-consensus and a=1"]:::leaf
    HAT_C["HAT: c above causal forces l above zero"]:::leaf
    FRONTIER["Pareto frontier
every gain costs something else"]:::root
    INTERIOR["Interior: l and t suboptimal
free gains available"]:::ok
    FRONTIER_NEW["Expanded frontier after protocol change
EPaxos: beta drops, t ceiling rises 2x"]:::ok

    ORIGIN -->|"excluded by CAP"| CAP_C
    ORIGIN -->|"excluded by SNOW"| SNOW_C
    ORIGIN -->|"excluded by FLP"| FLP_C
    ORIGIN -->|"excluded by HAT"| HAT_C
    INTERIOR -->|"reduce beta, remove unnecessary coordination"| FRONTIER
    FRONTIER -->|"change architecture or protocol"| FRONTIER_NEW

    classDef root fill:none,stroke:#333,stroke-width:3px;
    classDef leaf fill:none,stroke:#333,stroke-width:1px;
    classDef ok fill:none,stroke:#22c55e,stroke-width:2px;
    classDef warn fill:none,stroke:#b71c1c,stroke-width:2px,stroke-dasharray: 4 4;

The diagram separates three qualitatively different engineering situations. An interior point has reducible overhead — the system pays coordination costs that are not buying correctness guarantees. A frontier point faces genuine trade-offs — any gain in one objective costs another. The expanded frontier after a protocol change represents new reachable territory — operating points that were previously impossible become possible when the architecture changes. These three situations require different engineering responses: performance tuning, architecture decisions, and protocol research, respectively.

---

Architecture by vibes — designing toward a corner because it feels right — is not a failure of effort. It is a failure of vocabulary. The architect who has never read Gilbert-Lynch can still ship a system that degrades correctly under partition, by accident or by experience. But they cannot explain why it degrades that way, cannot predict when the operating point will shift, and cannot defend the choice when the system fails and the post-mortem demands a justification. Formal results do not replace engineering judgment. They give it a precise language.

Compromise is not failure. Compromise is the only possible outcome when structural load limits bound the design space. Every system that runs in production stands somewhere on the Pareto frontier of its achievable region. The question is whether it got there deliberately — with a documented position, a measured cost, and an explicit trigger for revision — or accidentally, by inheriting defaults that someone else chose without knowing why. Not choosing is still a choice.

The ledger obligation. Every architectural decision has an impossibility result attached to it — whether the engineer names it or not. A team choosing eventual consistency is occupying the AP side of the CAP partition boundary; the proof determines what happens to reads during a partition, not the team’s preference. A team setting a Raft election timeout is making a formal liveness assertion: “we assert that message delivery is bounded by $T_{\text{election}}/2$ after GST.” A team implementing serializable read-only transactions alongside concurrent writes has staked a position in SNOW’s four-property space and implicitly dropped one of the four — whether or not they know which one.

Recording these choices without naming the theorem produces a historical snapshot. Recording them with the theorem produces a contract: one that specifies which boundary the decision occupies, what it costs, and what would require revision. “We chose eventual consistency for performance” is a snapshot. “We occupy the AP region of CAP — during a partition, writes to any replica succeed, reads may return values up to [sync interval] stale, and the sync interval is reviewed when cross-region RTT baseline changes by more than 20%” is a contract. Every architecture decision that follows this contract begins by naming the impossibility result it is paying for — because a decision that does not name the exclusion zone it borders cannot know when it has crossed it.

The minimum viable ADR header for any distributed systems decision:

Field	Content
Theorem paid	Which impossibility result bounds this decision ( CAP , FLP , SNOW, HAT , or combination)
Exclusion zone	Which face of the design cube is fenced off; what operating point is being avoided
Operating point	Specific $(l, c, a, t, O_{\text{protocol}})$ coordinates: consistency level, availability under partition, latency budget, throughput target, and protocol operability score (failure-mode states times concurrent transitions — a dimensionless count, defined in The Logical Tax)
Revision trigger	The specific metric threshold — not a general hope — that moves this decision to “Under Review”

A team that cannot fill in “Theorem paid” and “Exclusion zone” has not yet understood what they decided. The impossibility result is not a justification for the choice; it is the physical boundary the choice navigates. Naming it converts an architectural opinion into a navigational commitment.

Pareto Ledger — Impossibility Boundaries

Tax Type	Metric / Notation	Price Paid — Rate Limiter Case Study	Drift Trigger
Impossibility — CAP	Strong consistency, availability, and partition tolerance cannot all hold simultaneously	Chose AP: regional Raft admits bounded over-admission during partition; writes never block	Partition tolerance requirement eliminated (single-DC migration) — re-run CAP position
Impossibility — FLP	$T_{\text{election}}$ (practical liveness bound in async model)	$T_{\text{election}} = 3 \times L_{\text{intra}}$ ; liveness assumed under 50ms network jitter	Median RTT increases > 50% — review $T_{\text{election}}$
Impossibility — SNOW	For read-only transactions: strict serializability, non-blocking, one-round-trip, and write-compatibility cannot all hold simultaneously	Quota read phase (read-only cross-shard count query): dropped O — two rounds; R-O transaction is now strictly serializable at the cost of 70ms added latency	Staleness tolerance on the read phase tightens to zero — single-round ReadIndex insufficient; review write ceiling
Impossibility — HAT	Highly Available Transactions cannot provide serializable cross-shard atomicity	Cross-region quota reconciliation uses eventual convergence; cross-shard strict atomicity absent	Hard financial settlement constraint added — re-evaluate: HAT is insufficient for zero-overage enforcement

---

References

1. S. Gilbert, N. Lynch. “Brewer’s Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web Services.” ACM SIGACT News, 33(2), 2002.

2. E. Brewer. “ CAP Twelve Years Later: How the ‘Rules’ Have Changed.” IEEE Computer, 45(2), 2012.

3. A. Fox, E. Brewer. “Harvest, Yield, and Scalable Tolerant Systems.” HotOS VII, 1999.

4. D. Abadi. “Consistency Tradeoffs in Modern Distributed Database System Design.” IEEE Computer, 45(2), 2012.

5. M. Fischer, N. Lynch, M. Paterson. “Impossibility of Distributed Consensus with One Faulty Process.” Journal of the ACM, 32(2):374-382, 1985.

6. H. Lu, K. Hodsdon, K. Ngo, S. Mu, W. Lloyd. “The SNOW Theorem and Latency-Optimal Read-Only Transactions.” OSDI, 2016.

7. P. Bailis, A. Davidson, A. Fekete, A. Ghodsi, J. Hellerstein, I. Stoica. “Highly Available Transactions: Virtues and Limitations.” VLDB, 7(3), 2014.

8. P. Viotti, M. Vukolic. “Consistency in Non-Transactional Distributed Storage Systems.” ACM Computing Surveys, 49(1), 2016.

9. C. Dwork, N. Lynch, L. Stockmeyer. “Consensus in the Presence of Partial Synchrony.” Journal of the ACM, 35(2):288-323, 1988.

10. N. Bronson, A. Amsden, G. Cabrera, P. Chakka, P. Dimov, H. Ding, J. Ferris, A. Giardullo, J. Hoon, E. Hung, W. Kaldewey, N. Khoury, A. Parmar, M. Perelman, T. Petrovic, T. Reed, D. Savage, B. Smith, A. Staszewski, N. Taylor, P. Tran, and K. VanNess. “Metastable Failures in Distributed Systems.” HotOS XVIII, 2021.

11. P. Gill, N. Jain, N. Nagappan. “Understanding Network Failures in Data Centers: Measurement, Analysis, and Implications.” SIGCOMM, 2011.

12. P. Huang, C. Guo, L. Zhou, J. R. Lorch, Y. Dang, M. Chintalapati, R. Yao. “Gray Failure: The Achilles’ Heel of Cloud-Scale Systems.” HotOS XVI, 2017.

---

Back to top