Map Business Invariants to the Weakest Consistency Model That Still Preserves Correctness

Learning outcomes

Consistency is not a virtue that must be maximized uniformly. AtlasMart’s job is to protect business invariants while avoiding coordination that buys no useful correctness. “Inventory must not go negative” is different from “search should reflect catalog changes within 30 seconds,” and both are different from “the user should see their own profile edit immediately.” This final lesson turns those statements into explicit data contracts.

1. Start with the invariant, not the database

An invariant is a condition that must hold for states or histories the business considers correct. Examples include “confirmed reservations cannot exceed allocatable inventory” and “one idempotency key cannot cause two captured charges.” Other requirements are freshness or experience targets rather than hard invariants: “search results should update within 30 seconds,” or “recommendations may be minutes old.” Separating these categories prevents both over-coordination and accidental data corruption.

2. “Weakest that preserves correctness” means weakest for the operation

The aim is not to weaken everything. It is to avoid paying for stronger global coordination where the invariant does not require it. A search index can be asynchronous because the catalog database remains the source of truth and the business accepts lag. A customer profile can use eventual replication plus read-your-writes for the editing session. Scarce inventory may require a linearizable conditional write, single-owner routing, or a carefully designed rights/escrow scheme.

This operation-by-operation framing also improves failure behavior. Search can continue serving stale data with an explicit freshness age; inventory may reject on an isolated non-owner; profile editing may accept locally if merge semantics are safe; payment may require a durable idempotency decision before returning success.

3. Counterexample method: try to break the invariant

Before accepting a consistency design, construct the smallest concurrent history that could violate the invariant. For stock=1, two disconnected replicas each seeing 1 and each decrementing to 0 is enough. Each local database state satisfies stock >= 0, yet the combined business history contains two fulfilled reservations. This demonstrates why checking only local state is insufficient for a global invariant.

initial global right: 1 unit
East reads 1 -> accepts R-A -> local 0
West reads 1 -> accepts R-B -> local 0

local checks: both pass stock >= 0
business history: two acknowledged reservations for one unit -> invariant violated

4. Coordination, ownership, escrow, or compensation

When the counterexample fails, choose a mechanism deliberately. Coordination can serialize or condition conflicting changes. Single ownership routes a key or invariant to one authority. Escrow/rights allocation partitions a global quantity into independently spendable local rights so each region can act without contacting others until rights are exhausted. Compensation accepts that an invalid business outcome may occur temporarily and defines a later corrective action, such as back-ordering one reservation. Compensation is not the same as preserving the original invariant; it changes the allowed history.

5. Derived views can be weaker because they are reconstructable

AtlasMart’s search index and recommendation store do not own catalog truth. They are derived views. That allows asynchronous propagation, replay, reconciliation, and bounded freshness objectives. The key operational requirement shifts from “never stale” to “detect lag, preserve source-of-truth ownership, replay safely, and recover when the derived view is lost or corrupt.” Chapter 20 will develop change data capture and synchronization mechanisms in detail.

6. Use invariant confluence as a deeper reasoning tool

Research on invariant confluence formalizes when independently valid operations can be merged while preserving an invariant. The practical lesson is accessible without the full formalism: if two sides can each make a locally valid change and the merged result can violate the invariant, coordination or a redesign of the state/rights model is required. If all independent valid changes merge to another valid state, coordination can sometimes be avoided safely.

7. AtlasMart lab — write the decision notebook as executable data

from dataclasses import dataclass

@dataclass(frozen=True)
class Requirement:
    name: str
    invariant: str
    tolerated_anomaly: str
    chosen_model: str

requirements = [
    Requirement("inventory reservation", "available units never negative", "none", "single-owner/conditional strongly consistent write"),
    Requirement("customer profile", "latest accepted edits eventually converge", "brief remote staleness", "eventual + session read-your-writes"),
    Requirement("catalog search", "results derive from catalog source of truth", "index may lag <= 30 s", "bounded freshness target on derived view"),
    Requirement("recommendations", "no financial invariant", "minutes of staleness", "eventual"),
]

for r in requirements:
    print(f"{r.name:22} | invariant={r.invariant}")
    print(f"  tolerate: {r.tolerated_anomaly}")
    print(f"  choose:   {r.chosen_model}")

print("\nCounterexample: two independent replicas each see stock=1 and each decrement locally.")
print("Both local states are valid (stock=0), but the merged business history sold two units.")
print("The invariant is global, so this operation needs coordination, ownership, escrow, or compensation semantics.")

Expected output

inventory reservation  | invariant=available units never negative
  tolerate: none
  choose:   single-owner/conditional strongly consistent write
customer profile       | invariant=latest accepted edits eventually converge
  tolerate: brief remote staleness
  choose:   eventual + session read-your-writes
catalog search         | invariant=results derive from catalog source of truth
  tolerate: index may lag <= 30 s
  choose:   bounded freshness target on derived view
recommendations        | invariant=no financial invariant
  tolerate: minutes of staleness
  choose:   eventual

Counterexample: two independent replicas each see stock=1 and each decrement locally.
Both local states are valid (stock=0), but the merged business history sold two units.
The invariant is global, so this operation needs coordination, ownership, escrow, or compensation semantics.

The script does not “calculate” the correct database. It makes architecture assumptions reviewable. The important artifact is the mapping from invariant and tolerated anomaly to a consistency/ownership strategy that can later be tested against actual product semantics.

8. Extend the Chapter 01 decision notebook

Repeat this format for every critical data path. A generic “consistency: strong” field is too vague to operate during an incident.

9. Deliberately wrong approach — choose eventual consistency everywhere for speed

The mistake is attractive because weaker coordination can reduce latency and increase availability in some topologies. But performance is not a correctness proof. If the allowed histories violate inventory or payment invariants, the design is invalid unless the business explicitly accepts and compensates those outcomes. The opposite mistake—making all reads globally linearizable—can add cost and latency to derived or user-local paths without protecting any additional invariant.

10. Chapter summary and next bridge

Chapter 03 replaces CAP folklore with a repeatable method. Under a partition, linearizable consistency and availability for all requests can conflict. Outside a partition, latency and consistency still trade through coordination and distance. Consistency models define allowed client histories. Business invariants decide which histories are unacceptable. The architecture should therefore choose semantics per operation, not per fashion.

Chapter 04 adds time and ordering. Physical clocks can skew; Lamport clocks capture happens-before; version vectors can expose concurrency; hybrid logical clocks combine logical order with physical-time structure. Those tools help a distributed system reason about versions without pretending every machine shares a perfect clock.

Authoritative references

• Bailis et al. — Coordination Avoidance in Database Systems — invariant-confluence framework for when coordination is necessary for correctness
• Herlihy & Wing — Linearizability — strong client-visible ordering model
• Terry et al. — Session Guarantees — weaker per-session guarantees useful for user-facing data
• Daniel Abadi — PACELC — latency/consistency framing beyond partition failures