Do your replicas agree after the repair code runs?

1The problem you already have

Many backend systems apply the same events in more than one place, in different orders:

• active-active databases and multi-region writes;
• offline-first apps that sync when they reconnect;
• queues that retry, redeliver and reorder messages;
• event-sourced projections built from several streams.

Most of these systems also have business rules. Often a rule is not kept by refusing a write. The write is accepted, and code that runs afterwards puts things right:

• cap inventory at what the shelf or warehouse holds;
• clamp a balance at a floor;
• run a saga's compensating step when a later step fails;
• drop duplicates;
• clean up records that point at something deleted;
• a reconciler loop that compares actual state with desired state and fixes the difference.

This guide calls that code the repair. The question is this: if every replica sees the same events, in different orders, and runs the same repair code, do they end up agreeing?

Not always. The repair can be correct on every replica, and the replicas can still disagree. The next section shows the smallest example.

2Try it: the shelf

A shelf holds at most 5 items and has 4 in stock. Two events arrive: "add 3" and "remove 1". The repair caps the stock at 5. Pick an order for each replica.

Repair on every write. The two orders end at 4 and 5. In the order "add 3" then "remove 1", the cap throws away 2 items, and the removal then takes a real item off a full shelf. In the other order the removal comes before the overflow, so the cap later throws away only 1 item. Same events, same code, different stock.

Store raw, cap when reading. The store keeps the raw count, and the cap is applied each time the value is read. Adding and subtracting give the same total in any order, so every replica stores 6 and reads 5, whatever the order. This changes the business meaning. The store now accepts the overflow: it records 6 items for a shelf of 5, and removing one item from a full shelf can still read 5 afterwards, because the removal came out of the overflow. That is right for a backlog of items waiting for shelf space, and wrong for a shelf that refuses extra items.

3Three questions to ask of your repair code

These are the plain versions of the conditions the theory proves. Write apply(e, s) for event e applied to state s, and repair(s) for the repair run until it is done.

What is proved. Take one service whose repair always finishes, where events can arrive in any order and an event can arrive before the repair has finished. Its replicas agree in every order exactly when (a) and (b) both hold at the states replicas can reach. "Exactly" means both directions: if (a) and (b) hold, every order agrees; if either fails, some run of events and repair steps ends in two different states. Neither question implies the other. Some systems pass (a) and fail (b), and some pass (b) and fail (a).

Proof: cc_exact · nd_derived_from · descent_not_history · history_not_descent

Tests you can add today

Here are the three questions as property-based tests, written for Python's Hypothesis. Supply your own START, EVENTS, apply, is_valid, repair_step (one step of the repair), repair (the repair run to the end) and measure. For the shelf they are:

START, CAP = 4, 5
EVENTS = ["add 3", "remove 1"]
def apply(e, s):     return s + 3 if e == "add 3" else max(s - 1, 0)
def is_valid(s):     return s <= CAP
def repair_step(s):  return min(s, CAP)          # one step: cap the stock
def repair(s):
    while not is_valid(s): s = repair_step(s)
    return s
def measure(s):      return max(s - CAP, 0)      # items over the cap

The tests:

from hypothesis import given, strategies as st

events = st.sampled_from(EVENTS)

@st.composite
def reachable(draw):
    """A state a replica can be in: events applied, repair partly run."""
    s = START
    for e in draw(st.lists(events, max_size=6)):
        s = apply(e, s)
        for _ in range(draw(st.integers(0, 3))):
            if not is_valid(s):
                s = repair_step(s)
    return s

@st.composite
def reachable_repaired(draw):
    """A state after every event has been repaired."""
    s = START
    for e in draw(st.lists(events, max_size=6)):
        s = repair(apply(e, s))
    return s

# (a) Repairing early or late: same result after the repair.
@given(reachable(), events)
def test_repair_early_or_late(s, e):
    assert repair(apply(e, repair(s))) == repair(apply(e, s))

# (b) Two repaired events give the same result in either order.
@given(reachable_repaired(), events, events)
def test_order(s, e1, e2):
    assert repair(apply(e2, repair(apply(e1, s)))) == \
           repair(apply(e1, repair(apply(e2, s))))

# (c) Every repair step makes the measure smaller.
@given(reachable())
def test_repair_finishes(s):
    if not is_valid(s):
        assert measure(repair_step(s)) < measure(s)

Run against the shelf, the first two tests fail with 4 against 5 and the third passes. For (a), Hypothesis reports a raw stock of 7 and "remove 1"; for (b), a stock of 4 with "add 3" and "remove 1". The states are built by replaying events from START on purpose: the conditions need to hold only at states a replica can reach, and testing arbitrary states can report failures that never happen. If your queue can deliver a message twice, a duplicate is one more order to check; the atlas gives the exact condition for each delivery guarantee.

A property-based test samples states and events. It can find a counterexample. It cannot show that none exists, because it does not try every state. That is what gsm and the proofs are for: gsm tries every state of a finite model at build time, and the proofs show that these are the right conditions to check.

4When the repair runs matters

Question (a) is about timing, so whether you need it depends on when your repair runs.

• In the same transaction as the event. Each event and its repair commit together, and no other event sees the state in between. Then only (b) matters, checked on the repaired steps: replicas agree exactly when repaired events give the same result in either order, at the states replicas reach.
• Separately from the event. A background reconciler, a cron job, an asynchronous compensation, a consumer of a change stream. Events keep arriving while the repair has not run, so an event can land on a state the repair has not repaired yet. Then (a) is needed as well: replicas agree exactly when they would agree with an in-transaction repair and (a) holds at the states replicas reach.

Proof: atomic_exact · atomic_derived_from

The difference is real. A system can be correct with an in-transaction repair and break with a background reconciler.

In practice: if your repair runs in the same transaction as the event, test (b). If anything runs it later, test (a) as well, or move the repair into the transaction.

5When a check fails: your options

These are standard design moves, not results of the theory, except where a proof link says otherwise.

• Make the events commute. Design operations so that order never matters: counters kept as separate increments and decrements, sets with an add-wins or remove-wins rule, registers with a deterministic tiebreak. This is the CRDT approach, and the repair then has nothing to do.
• Keep what later events need. If (a) fails, the repair is throwing away something a later event reads. Store the raw facts and derive the result when reading, as in the shelf demo. Or have each event record a fact, and let the repair recompute the outcome from the facts; the order-fulfillment example in the gsm README is built this way.
• Move the repair into the transaction. If (a) fails only because a reconciler runs late, see section 4.
• Coordinate only the events that conflict. Use a lock, a single leader or a consensus round for the pairs of events that fail (b), and let the rest run without coordination. When gsm rejects a model, it names the pair of events and the state where they diverge. Across a network of services, where a link is a connection between two services that copy each other's data (section 6), finding the fewest links to coordinate is NP-hard in the cases the atlas covers, so unless P = NP no efficient method finds the minimum in general.

Proof (fewest links): maxcut_plan_reduction · lmin_reduction

6More than one service

Services often copy data to each other: a catalog feeds search, orders feed billing, billing feeds a ledger. Each service enforces its own rules with its own repair. The questions change with the shape of the network.

No loops

When data flows one way, along a chain or a tree of services, the check splits into two local checks per link. An event gives the same result whether or not the link's repair has run (question (a), at the link). Two independent events on one service (events that nothing orders, so they can arrive in either order) give the same result in either order after that repair (question (b)). Settling needs no check of its own: when every service keeps getting its turn, a network without loops always settles at one state.

Proof: fed_exact · rb_robert_fair

Loops

When rules feed each other in a loop, repairs can push against each other forever. A schedule that gives every rule its turn can cycle without end, even when exactly one consistent state exists. The proved example is as small as a loop gets: one record and two rules that act on it. One rule swaps two bad values, A and B. The other repairs A to the good value. If the repair rule only ever gets its turn while the record holds B, the good value is never reached. As an analogy only, this is much like two controllers that each undo the other's change; the proof itself is about one record with two rules. Knowing the one consistent state is not enough; whether runs reach it is a separate question.

Proof: flip2_unique_solution_livelock

Questions with no efficient general check

Suppose the copies between services can lose information (a copy keeps a summary, not the whole record) and no single source feeds every service. Then deciding whether any state satisfies every link at once is NP-complete. Unless P = NP, no efficient check answers it in general. An engineer asks this question when linking services whose rules might contradict each other: is there any consistent state at all across these linked services?

Proof: net_section_iff_sat

7 open problems (9 open tiles on the atlas), most of them about loops, are still open; each is listed with its progress in the regime audit. The Convergence Atlas maps every case on one page. Press "Start here" for a six-stop tour.

7How it relates to what you know

CRDTs

A CRDT is the case where the repair does nothing: the events commute by design. Repair code lets you use operations that do not commute. Some operations converge only with a repair, and no system without one converges using them.

What a repair does not add is outcomes a CRDT cannot have. Every system that converges with repairs behaves like a CRDT on its repaired steps, where an event and its repair count as one operation. The gain is in which operations you may write, and in when the repair may run (section 4), not in which end states are possible.

Proof: crdt_boundary · causal_convergence_exact · merge_action_exact

Database constraints that reject writes

A CHECK constraint or a unique index refuses a write that would break a rule. The research question for that style is invariant confluence (Bailis and others, VLDB 2015): which transactions can run on replicas without coordination and never break a rule. This guide is about the other style, where the write is accepted and a repair restores the rule. With a repair, some transactions that are not invariant confluent converge anyway, at a cost: the repair may undo a committed write, which the rejecting style never does.

Proof: repair_enlarges

Reconcile loops

This is an analogy, not a claim about any product. A controller that compares actual state with desired state and acts until they match, the pattern behind Kubernetes controllers, is a repair that runs separately from the events. In the terms of this guide, section 4 applies to it: question (a) is needed. When several controllers act on each other's output, the loop questions of section 6 apply: do they settle, and on one state?

8Glossary

The research term on the left; what it means in a backend on the right.

9Where to go next