20992883ff
---ci--- project: atelier phase: 1 milestone: v0.4 status: complete phase_role: execution phase_tag: v0.3.1 requirements: covered: [ATELIER-92, ATELIER-93, ATELIER-94, ATELIER-95, ATELIER-96] partial: [] ---/ci---
315 lines
18 KiB
Markdown
315 lines
18 KiB
Markdown
# Sync — Derived Rules
|
|
|
|
> Derives from `domains/edge/first-principles.md`. Applies P4 (Sync
|
|
> Conflicts are Bounded, Not Infinite) primarily, with P5
|
|
> (idempotent merge operations), P2 (offline as the precondition),
|
|
> and P10 (sync is observable). Cross-links `domains/data/migrations`
|
|
> for schema migration under sync and `domains/concurrency/patterns`
|
|
> for the immutability-aid-merge principle.
|
|
|
|
## What the Sync Problem Is (P4 Sync Conflicts are Bounded, Not Infinite)
|
|
|
|
- Sync is the discipline of reconciling divergent state across
|
|
partitioned nodes. While partitioned, each node accepts writes
|
|
independently; on reconnect, the divergent state must converge.
|
|
The correctness contract is that the merge terminates and
|
|
converges — oscillation and infinite sync loops are correctness
|
|
failures, not eventual consistency (P4).
|
|
- Sync is the edge domain's deepest problem: it is the
|
|
reconciliation layer above `P2 Offline is a First-Class State`.
|
|
Without offline operation there is nothing to sync; with it, the
|
|
reconnect reconciliation is the correctness mechanism. See
|
|
`domains/edge/offline-first.md` for the offline write-queue that
|
|
produces the divergent state to be reconciled.
|
|
- The boundary is per D-061: edge owns the partitioned-reconcile
|
|
angle; concurrency owns the in-process analog
|
|
(`concurrency/P1 Immutability by Default` — immutability aids
|
|
merge); data owns the generic migration discipline
|
|
(`data/migrations`). Sync is an edge concern because its defining
|
|
trait is partitioned divergence, a concern that only arises at the
|
|
network edge.
|
|
|
|
## Conflict Resolution Strategies (P4, C1 Correctness, C5 Reversibility)
|
|
|
|
- A conflict is when two nodes have divergent state for the same
|
|
logical entity and no total order determines which is correct.
|
|
Resolution strategies fall into two families:
|
|
- **Conflict-free**: the data type guarantees convergence by
|
|
construction (CRDTs). The merge is deterministic; no conflict
|
|
surfaces to the user or the application.
|
|
- **Conflict-tolerant**: the data type can conflict; the
|
|
resolution policy (last-write-win, three-way merge,
|
|
application-specific) arbitrates. Conflicts may surface to the
|
|
user or be silently resolved per a documented policy.
|
|
- The choice is a P4 decision: conflict-free types guarantee the
|
|
bound (convergence) but constrain the data model; conflict-tolerant
|
|
types are flexible but require the resolution policy to be correct
|
|
and bounded (no oscillation). See the decision matrix below.
|
|
|
|
## CRDTs — Conflict-Free Replicated Data Types (P4, C5, C6)
|
|
|
|
- A CRDT is a data type whose merge operation is associative,
|
|
commutative, and idempotent. Given any set of divergent replicas,
|
|
merging them in any order converges to the same state — the merge
|
|
is deterministic and terminating (P4 bound). CRDTs derive from C5
|
|
Reversibility (divergent state reverses to convergence) and C6
|
|
Composability (CRDTs compose: a CRDT map of CRDT registers is
|
|
itself a CRDT).
|
|
- **State-based (CvRDT — convergent):** each replica carries its
|
|
full state; merge is a least-upper-bound on a semi-lattice. The
|
|
payload is larger (full state per merge); the merge is simple
|
|
(one function). Fits small state and unreliable networks.
|
|
- **Operation-based (CmRDT — commutative):** each replica carries
|
|
operations; merge is applying the operations in causal order. The
|
|
payload is smaller (ops, not state); the delivery must be
|
|
reliable and causally ordered. Fits large state and reliable
|
|
transport.
|
|
- The tradeoff: state-based is simpler but heavier; operation-based
|
|
is lighter but requires causal delivery. Both guarantee
|
|
convergence (P4); the choice is a C8 Economy decision (bandwidth
|
|
vs delivery complexity).
|
|
|
|
```typescript
|
|
// CRDT register: LWW-element-set (state-based, CvRDT). The merge
|
|
// is deterministic — the register with the later timestamp wins.
|
|
// Convergence is guaranteed (P4); the merge is idempotent (P5).
|
|
|
|
interface LWWRegister<T> {
|
|
value: T;
|
|
timestamp: number; // monotonic clock; ties broken by node id
|
|
nodeId: string;
|
|
}
|
|
|
|
function mergeLWWRegister<T>(
|
|
local: LWWRegister<T>,
|
|
remote: LWWRegister<T>,
|
|
): LWWRegister<T> {
|
|
// The merge is associative, commutative, idempotent (P4, P5).
|
|
// (local.timestamp, local.nodeId) > (remote.timestamp, remote.nodeId)
|
|
// is a total order — no oscillation, no infinite loop.
|
|
if (local.timestamp > remote.timestamp) return local;
|
|
if (local.timestamp < remote.timestamp) return remote;
|
|
// Tie: break by node id for a deterministic total order.
|
|
return local.nodeId > remote.nodeId ? local : remote;
|
|
}
|
|
|
|
// The register is a CRDT: merge(merge(a, b), c) === merge(a, merge(b, c))
|
|
// for any replicas a, b, c. Convergence is guaranteed (P4).
|
|
```
|
|
|
|
```typescript
|
|
// CRDT set: add-wins last-write-wins element set (state-based).
|
|
// Each element carries a timestamp; remove only wins if the
|
|
// remove-timestamp is later than the add-timestamp. This avoids
|
|
// the remove-wins-vs-add race (P4) without surfacing a conflict.
|
|
|
|
interface AWLWWSet<T> {
|
|
adds: Map<T, number>; // element -> add-timestamp
|
|
removes: Map<T, number>; // element -> remove-timestamp
|
|
}
|
|
|
|
function mergeAWLWWSet<T>(a: AWLWWSet<T>, b: AWLWWSet<T>): AWLWWSet<T> {
|
|
const adds = new Map<T, number>(a.adds);
|
|
const removes = new Map<T, number>(a.removes);
|
|
for (const [el, ts] of b.adds) {
|
|
adds.set(el, Math.max(adds.get(el) ?? 0, ts)); // add-wins union
|
|
}
|
|
for (const [el, ts] of b.removes) {
|
|
removes.set(el, Math.max(removes.get(el) ?? 0, ts));
|
|
}
|
|
return { adds, removes };
|
|
}
|
|
|
|
function contains<T>(set: AWLWWSet<T>, el: T): boolean {
|
|
const addTs = set.adds.get(el) ?? 0;
|
|
const rmTs = set.removes.get(el) ?? 0;
|
|
return addTs > rmTs; // add wins on equal timestamp (P4 bounded)
|
|
}
|
|
```
|
|
|
|
## Last-Write-Win (LWW) with Vector Clocks (P4, C1, C5)
|
|
|
|
- LWW is the simplest conflict-tolerant strategy: the write with the
|
|
latest timestamp wins. It is cheap, but it silently discards
|
|
concurrent writes — the "lost update" is the correctness cost. LWW
|
|
is correct only when the timestamp is a total order (a monotonic
|
|
clock, not wall time), and when lost concurrent writes are
|
|
acceptable (e.g., caching, presence, ephemeral state).
|
|
- **Vector clocks** are the timestamp that knows about concurrency.
|
|
A vector clock records the logical time of each node; two writes
|
|
are concurrent iff neither vector dominates the other. LWW with
|
|
vector clocks: a write that is causally later wins; a write that
|
|
is concurrent conflicts and is resolved by a tiebreak (node id,
|
|
wall time, or application policy).
|
|
- The tiebreak is the P4 bound: the conflict must be resolved
|
|
deterministically (no oscillation) and the resolution must be
|
|
documented. A tiebreak by wall time alone (no vector clock) is a
|
|
P4 violation waiting to happen — wall time skews across nodes,
|
|
and a clock skew can flip the tiebreak, oscillating the merge.
|
|
|
|
```typescript
|
|
// LWW with vector clocks (conflict-tolerant, P4 bounded). The
|
|
// vector clock records causal order; concurrent writes conflict;
|
|
// the conflict is tiebroken deterministically (no oscillation).
|
|
|
|
type VectorClock = Record<string, number>; // nodeId -> counter
|
|
|
|
function compareClock(a: VectorClock, b: VectorClock): "before" | "after" | "equal" | "concurrent" {
|
|
let aBefore = false, bBefore = false;
|
|
const keys = new Set([...Object.keys(a), ...Object.keys(b)]);
|
|
for (const k of keys) {
|
|
const av = a[k] ?? 0;
|
|
const bv = b[k] ?? 0;
|
|
if (av < bv) aBefore = true;
|
|
if (av > bv) bBefore = true;
|
|
}
|
|
if (aBefore && bBefore) return "concurrent";
|
|
if (aBefore) return "before";
|
|
if (bBefore) return "after";
|
|
return "equal";
|
|
}
|
|
|
|
interface LWWVectorState<T> {
|
|
value: T;
|
|
clock: VectorClock;
|
|
writerId: string; // tiebreak: deterministic, no oscillation (P4)
|
|
}
|
|
|
|
function mergeLWWVector<T>(
|
|
local: LWWVectorState<T>,
|
|
remote: LWWVectorState<T>,
|
|
): LWWVectorState<T> {
|
|
const order = compareClock(local.clock, remote.clock);
|
|
if (order === "before") return remote; // remote causally later
|
|
if (order === "after" || order === "equal") return local;
|
|
// Concurrent: tiebreak by writer id (deterministic, P4 bounded).
|
|
return local.writerId > remote.writerId ? local : remote;
|
|
}
|
|
```
|
|
|
|
- The merge is idempotent (P5): merging the same two replicas twice
|
|
yields the same result. The tiebreak by `writerId` is a total
|
|
order, so the merge cannot oscillate (P4 bound).
|
|
- A vector-clock merge that surfaces the concurrent conflict to the
|
|
application (instead of tiebreaking) is also valid — the
|
|
application resolves per its own policy. The P4 bound is that the
|
|
resolution terminates; the policy determines whether the user sees
|
|
the conflict or the system silences it.
|
|
|
|
## Merge Semantics (P4, P5, cross-link concurrency/patterns)
|
|
|
|
- The merge function is the heart of sync. Its properties (P4):
|
|
- **Associative**: `merge(merge(a, b), c) === merge(a, merge(b, c))`.
|
|
- **Commutative**: `merge(a, b) === merge(b, a)`.
|
|
- **Idempotent**: `merge(a, a) === a` (P5 — retried merges are safe).
|
|
- Immutability aids merge: an immutable state representation (the
|
|
CRDT payload, the LWW register with a clock) makes the merge a
|
|
pure function of two inputs, with no in-place mutation race. See
|
|
`domains/concurrency/patterns` (`concurrency/P1 Immutability by
|
|
Default`) for the in-process immutability principle; sync is the
|
|
cross-partition instance of it.
|
|
- A merge that mutates in place is a P5 violation waiting to
|
|
happen: a retried merge mutates the same state twice, and the
|
|
result is not idempotent. Always merge into a new state; never
|
|
mutate the inputs.
|
|
|
|
## Conflict-Free vs Conflict-Tolerant Data Types (P4, C3 Simplicity)
|
|
|
|
- **Conflict-free (CRDTs):** the data type guarantees convergence.
|
|
The application never sees a conflict; the merge is deterministic.
|
|
The cost: the data model is constrained (counters, sets, registers,
|
|
maps of these). A conflict-free type for arbitrary JSON is hard;
|
|
a conflict-free type for a counter is a PN-counter.
|
|
- **Conflict-tolerant (LWW, three-way merge, application policy):**
|
|
the data type can conflict; the resolution policy arbitrates. The
|
|
cost: the policy must be correct and bounded (no oscillation), and
|
|
the conflict may surface to the user. The benefit: any data model
|
|
can be made conflict-tolerant (just pick a tiebreak).
|
|
- The choice is the decision matrix below. It is a P4 decision
|
|
(which bound), a C1 decision (which correctness cost is
|
|
acceptable), and a C3 decision (which simplicity is affordable).
|
|
See also `domains/data/migrations` for the schema-evolution angle
|
|
— a schema change under sync must be compatible with both
|
|
replicas, or the merge fails on the new shape.
|
|
|
|
## Schema Migration Under Sync (P4, cross-link data/migrations)
|
|
|
|
- A schema migration under sync is harder than a single-node
|
|
migration: both replicas must understand the new shape, or the
|
|
merge fails. The migration must be forward-and-backward compatible
|
|
across all replicas that may still hold the old shape — see
|
|
`domains/data/migrations` for the generic compatibility discipline.
|
|
- A breaking schema change under sync requires a staged migration:
|
|
deploy the new-shape-aware merge first (it accepts both shapes),
|
|
then deploy the new shape, then deploy the old-shape-removing
|
|
merge. A big-bang schema change under sync is a P4 violation: the
|
|
replicas that have not yet upgraded will fail the merge, and the
|
|
sync will not converge.
|
|
- The merge function's version awareness is the P4 bound: the merge
|
|
must handle every shape version that may exist in the fleet, or
|
|
reject (and surface) the merge rather than silently corrupting.
|
|
|
|
## CRDT vs Last-Write-Win — Decision Matrix (D-069)
|
|
|
|
| Strategy | When | Correctness Guarantee | Operational Cost | Failure Mode |
|
|
|----------|------|------------------------|-------------------|--------------|
|
|
| CRDT (state-based, CvRDT) | The data model fits a CRDT (counter, set, register, map of these); convergence must be guaranteed without surfacing conflicts; the network is unreliable (full-state merge tolerates dropped ops) | Strong eventual convergence — `merge(a, b) === merge(b, a)` for any replicas (P4 bound by construction) | Medium — full state per merge (bandwidth); semi-lattice merge function per type; CRDT library or hand-rolled | A bug in the merge function = silent divergence (C1); large state = bandwidth cost on constrained links (P3) |
|
|
| CRDT (operation-based, CmRDT) | The data model fits a CRDT; bandwidth is constrained (ops are smaller than state); the transport is reliable and causally ordered | Strong eventual convergence — same guarantee, smaller payload | High — requires causal delivery (vector clock or broker with ordering); op transform must be idempotent (P5) | Causal-delivery violation = lost ops = divergence; op-transform bug = silent divergence |
|
|
| Last-Write-Win (LWW) with vector clocks | The data model is arbitrary (any JSON, any record); concurrent writes are acceptable to discard or tiebreak; a total order tiebreak (node id) is acceptable | Bounded convergence — causally-later writes win; concurrent writes are tiebroken deterministically (P4 bound via tiebreak) | Low — simple merge (compare clocks, pick winner); no CRDT library; small payload | Concurrent writes are silently discarded (lost update); tiebreak by wall time = clock-skew oscillation (P4 violation); no vector clock = no concurrent-write detection = silent loss |
|
|
| LWW with wall-clock timestamp only | The data model is ephemeral (cache, presence); lost updates are acceptable; the clock is roughly synchronized (NTP) | Weak — convergence eventually, but concurrent writes may oscillate with clock skew; no concurrent-write detection | Lowest — one timestamp per write; no clock vector | Clock skew = oscillation (P4 violation); concurrent writes silently lost; not a correctness-safe strategy for durable state |
|
|
| Three-way merge (application-specific) | The data model is structured (documents, forms); conflicts should surface to the user or a domain-specific resolver; the merge is field-level | Bounded if the merge function is correct (associative, commutative, idempotent — P4, P5); conflicts surface per field | High — application-specific merge function per type; UI for conflict resolution; user-facing conflict surface | Merge-function bug = silent divergence or oscillation; unbounded conflict UI = user fatigue |
|
|
|
|
- The default for structured state that must converge silently is a
|
|
**CRDT** (state-based for unreliable networks, operation-based for
|
|
bandwidth-constrained reliable transport). The default for
|
|
arbitrary JSON where lost concurrent updates are acceptable is
|
|
**LWW with vector clocks** (never wall-clock-only for durable
|
|
state). The default for user-facing documents where conflicts
|
|
should surface is **three-way merge** with a documented resolution
|
|
policy.
|
|
- The failure-mode column is the P4 check: every row except
|
|
wall-clock-only LWW carries a bounded failure mode (the bug is in
|
|
the implementation, not the strategy). Wall-clock-only LWW carries
|
|
an unbounded failure mode (clock skew = oscillation) and is a P4
|
|
violation for durable state. Use it only for ephemeral state
|
|
where lost updates are acceptable.
|
|
- The choice is a P4 decision (which bound) and a C1 decision
|
|
(which correctness cost). A CRDT guarantees convergence but
|
|
constrains the data model; LWW is flexible but discards concurrent
|
|
writes. Neither is universally correct; the matrix is the
|
|
decision tool.
|
|
|
|
## Observability of Sync (P10 Edge Observability Survives Partition)
|
|
|
|
- Sync is itself an observable operation: the merge count, the
|
|
conflict count, the convergence lag (time from reconnect to
|
|
convergence), and the divergent-replica count are first-class
|
|
signals. A sync that runs forever without converging is the
|
|
`edge-sync-loop` chaos anti-pattern (P4 breach); without
|
|
observability it is invisible until the user notices the stale
|
|
state.
|
|
- A conflict that is silently resolved should be logged (the
|
|
resolution policy applied, the discarded write's idempotency key,
|
|
the winning write's clock). A conflict that surfaces to the user
|
|
should be metricated (the conflict rate, the resolution time).
|
|
See `domains/observability/metrics` for the generic discipline.
|
|
- A divergent replica that has not converged after the expected
|
|
window is an incident; without a metric it is invisible (P10
|
|
breach). Wire sync convergence to an alert — the
|
|
`divergent-replica-count` is the sync analog of the messaging
|
|
`consumer-lag` metric.
|
|
|
|
## What Violates Sync Discipline
|
|
|
|
| Violation | Principle |
|
|
|-----------|-----------|
|
|
| Sync loop that oscillates forever (CRDT without merge-semantics, LWW without monotonic clock) | P4 Sync Conflicts are Bounded, Not Infinite |
|
|
| LWW with wall-clock timestamp only on durable state (clock skew = oscillation) | P4, C1 (no concurrent-write detection) |
|
|
| Merge function that mutates inputs in place (retried merge is not idempotent) | P5 Edge Operations are Idempotent, `domains/concurrency/patterns` |
|
|
| Big-bang schema change under sync (replicas fail the merge) | P4, `domains/data/migrations` |
|
|
| Conflict silently resolved with no log (the policy is invisible) | P10 Edge Observability Survives Partition |
|
|
| Divergent replica with no convergence-lag metric (invisible stale state) | P10, `domains/observability/metrics` |
|
|
| Three-way merge with an unbounded conflict UI (user fatigue, no termination) | P4 (the merge must terminate) |
|
|
| Operation-based CRDT without causal delivery (lost ops = divergence) | P4, C1 (the delivery contract is the bound) |
|
|
| Merge that surfaces every concurrent conflict to the user (no default policy) | P4, C3 (the default policy is the simplicity bound) |
|
|
| Sync with no convergence test (the merge is untested under partition) | P4, `domains/testing/pyramid` | |