Capstan.Gtid (Capstan v0.1.0)

Copy Markdown View Source

MySQL GTID-set algebra — the dedup correctness core.

A GTID set is the sole authority for replication position (ADR-0001): dedup is set membership, never an ordinal comparison. This module is the one place GTID-set membership and interval math live, so no consumer — the connection's gap gate, the assembler, or a sink — ever hand-rolls them.

String format (MySQL canonical, INCLUSIVE bounds)

A comma-separated list of per-UUID entries; each entry is <uuid>:<interval>[:<interval>...]; an interval is a single number N or an inclusive range N-M with M >= N. "" is the empty set. A UUID is the 36-char hyphenated hex form; GNOs are integers >= 1. Ranges are inclusive: uuid:1-11 is GTIDs 1..11 and uuid:7 is uuid:7-7. Multi-source sets are supported — several UUID entries in one string.

render/1 produces the canonical form: UUIDs lower-cased and ordered lexicographically, intervals within a UUID sorted ascending and coalesced (merged where overlapping or adjacent), single-element intervals rendered as N. Parsing normalises to this form, so parse |> render is idempotent and, for any already canonical string s, s |> parse |> render == s.

Malformed input

parse/1 raises ArgumentError on any string outside the grammar above — a bad UUID, a GNO < 1 or non-numeric, a descending range, an empty entry. A dedup core must never silently coerce a malformed position into a plausible-but- wrong set, so parsing fails closed rather than guessing.

Single GTID shape

member?/2 takes a set and a single GTID as {uuid :: String.t(), gno :: pos_integer()}. The UUID is matched case-insensitively.

Scope

The bounds here are INCLUSIVE and stay inclusive. The COM_BINLOG_DUMP_GTID wire encoding uses an EXCLUSIVE end (uuid:1-11 -> wire end 12); that conversion is Task 3's concern and is deliberately not baked into this module.

Summary

Types

A GTID transaction sequence number; always >= 1.

A single GTID: one transaction from one source.

t()

A GTID set. Internally a map from UUID to a sorted, coalesced list of inclusive {low, high} intervals; a UUID with no live intervals is absent (never []). The representation is canonical by construction — treat it as opaque and build/inspect it only through this module's functions.

A source-server UUID in canonical lower-case 36-char hyphenated form.

Functions

Are a and b disjoint? True iff a ∩ b is empty.

Set intersection a ∩ b, per-UUID. Composes with subtract/2 for the F1 gap predicate (gtid_executed − checkpoint) ∩ gtid_purged.

Is one GTID a member of the set? The dedup idiom txn.gtid ∈ checkpoint.gtid_set.

Parses a canonical GTID-set string into a set. Raises ArgumentError on malformed input. parse("") is the empty set.

Renders a set to its canonical GTID-set string. The empty set renders as "".

Returns the set as a canonical, ordered list of per-source intervals: sources sorted by UUID, and — within each source — intervals sorted ascending and coalesced.

Is a a subset of b? The empty set is a subset of everything.

Set difference a − b (GTIDs in a not in b), splitting intervals as needed. subtract("uuid:1-10","uuid:4-6") renders "uuid:1-3:7-10".

Set union with adjacent-range coalescing. union("uuid:1-3","uuid:4-6") renders "uuid:1-6". Merges per-UUID.

Types

gno()

@type gno() :: pos_integer()

A GTID transaction sequence number; always >= 1.

gtid()

@type gtid() :: {uuid(), gno()}

A single GTID: one transaction from one source.

t()

@opaque t()

A GTID set. Internally a map from UUID to a sorted, coalesced list of inclusive {low, high} intervals; a UUID with no live intervals is absent (never []). The representation is canonical by construction — treat it as opaque and build/inspect it only through this module's functions.

uuid()

@type uuid() :: String.t()

A source-server UUID in canonical lower-case 36-char hyphenated form.

Functions

disjoint?(a, b)

@spec disjoint?(t(), t()) :: boolean()

Are a and b disjoint? True iff a ∩ b is empty.

intersection(a, b)

@spec intersection(t(), t()) :: t()

Set intersection a ∩ b, per-UUID. Composes with subtract/2 for the F1 gap predicate (gtid_executed − checkpoint) ∩ gtid_purged.

member?(set, arg)

@spec member?(t(), gtid()) :: boolean()

Is one GTID a member of the set? The dedup idiom txn.gtid ∈ checkpoint.gtid_set.

parse(string)

@spec parse(String.t()) :: t()

Parses a canonical GTID-set string into a set. Raises ArgumentError on malformed input. parse("") is the empty set.

render(set)

@spec render(t()) :: String.t()

Renders a set to its canonical GTID-set string. The empty set renders as "".

sources(set)

@spec sources(t()) :: [{uuid(), [{gno(), gno()}]}]

Returns the set as a canonical, ordered list of per-source intervals: sources sorted by UUID, and — within each source — intervals sorted ascending and coalesced.

Bounds stay INCLUSIVE, matching the rest of this module. This is the read-side accessor the COM_BINLOG_DUMP_GTID resume encoder iterates; the exclusive-end wire conversion (high -> high + 1) is that encoder's concern and is deliberately not applied here. The empty set has no sources.

subset?(a, b)

@spec subset?(t(), t()) :: boolean()

Is a a subset of b? The empty set is a subset of everything.

subtract(a, b)

@spec subtract(t(), t()) :: t()

Set difference a − b (GTIDs in a not in b), splitting intervals as needed. subtract("uuid:1-10","uuid:4-6") renders "uuid:1-3:7-10".

union(a, b)

@spec union(t(), t()) :: t()

Set union with adjacent-range coalescing. union("uuid:1-3","uuid:4-6") renders "uuid:1-6". Merges per-UUID.