A registry of every lock, what it guards, and its ordering.

Synchronization model (meta-sync)

Intent — A typed registry that models the system's synchronization behaviour — every OS-level lock (flock/lockf), which shared resource it guards, and the required acquisition ordering — so concurrency contracts are declared and checkable, not tribal.

Summary	A registry of every lock, what it guards, and its ordering.
Target	Bridge · System models
Form	`typed-ir`
Move	`package` — a constraint shipped with its sensors
Model	`is-a-model` — a structured model you check a system property against
Enforcement	Hard (deterministic) — a structured model held true by the lock-coverage lint (every `fcntl.flock` site must be declared or annotated)
Derivation	`model-from-code` — induced from the code, reconciled at build

Its place in the environment — a variant / known-use of Executable Source of Truth, under KNOW · Maintain authoritative system knowledge. Preserved here for its technical texture; the construction kit shows how it folds.

Motivation — the failure it kills

A fleet of agents on one host contends over shared resources through OS locks — the test-serializer's dotnet test flock, the build-serializer semaphore, the whole-repo lint mutex, the commit-slave serializer. Left undocumented, two failures lurk: an undeclared lock nobody knows guards what, and an inverted acquisition order between two locks that deadlocks. Both are invisible in the code and catastrophic at runtime, and they recur as new locks are added.

Why it's not just "just use flock where you need it"

Ad-hoc flock calls scattered across tools give no answer to "which locks exist, what do they guard, in what order must they be taken?" — so a deadlock-inducing ordering can't be detected, only suffered. The synchronization model declares each lock (SyncLock: path, cap, model, bypass-env, audit-log), each acquisition site (LockAcquirer), and each ordering constraint (LockOrdering). A coverage lint can then flag an undeclared flock, and an ordering lint can flag an inverted acquisition against the declared graph. A declared model lets a lint answer "which locks exist and in what order" before the code runs, so an inverted acquisition fails at author time. Scattered locks answer that question only by deadlocking in production, where the lesson arrives too late to act on.

Mechanism

The Synchronization registry composes three records — SyncLock (one OS primitive), LockAcquirer (one declared acquisition site, or lock="none" with a rationale), LockOrdering (before/after with rationale). A coverage lint scans the fcntl.flock/lockf call sites and requires each to be declared or carry a # noqa: not-a-sync-lock annotation; an ordering lint walks the declared ORDERINGS + call-graph to catch inverted acquisition.

Prerequisites

A typed lock/acquirer/ordering schema covering the three record kinds.
A coverage lint over the real flock call sites (so undeclared locks are caught).
An ordering constraint graph the lint can check acquisition against.

Consequences & costs

Every new lock is a registry entry. An undeclared flock fails the coverage lint (deliberately).
The ordering graph must be maintained. A missing edge lets a real inversion through.
Exempt sites need a rationale. The closed-set EXEMPT_RATIONALES is a small carve-out surface.

Known uses

The Synchronization registry — the SyncLock / LockAcquirer / LockOrdering records for the dev-time locks.
The sync-coverage lint (undeclared-flock gate) + the ordering-constraint lint (deadlock-risk gate).

Related mechanisms

Bridge — the agent fleet's mediators acquire these locks (agent side) ◀──▶ the model governs the concurrency contracts the codebase must honour (product side).
Counterpart — drift-parity-gates: the coverage/ordering lints that hold the model true.
See also — concurrency-contracts: the single-writer / mediator side of the same concurrency story.

Governed by

The mechanisms that hold this model true — inverted from their Governs edges at build time, never hand-written. A direct governor names this model; a trunk mechanism governs every model.

Coverage → model-node mapping (which invariants are actually tested) — Project test coverage onto model nodes (states, seams, invariants) so untested ones are visible. governs every model
Drift & parity gates — Bidirectional model↔reality checks so models cannot drift. governs every model
Enforce at the right semantic level — Match a mechanism's enforcement scope to the semantic scope of the property it checks. governs every model
Executable source-of-truth models — Structured models read every run and generated from; can't drift. governs every model
Formal invariant verification (temporal form → model checking) — Each invariant's temporal-logic form derives its checker — proven, not sampled. governs every model
Invariant-DAG execution policy (a typed Scheduler separates correctness from resource + cost) — A DAG holds correctness + cost-gate edges only; a typed Scheduler rations load + budget per host. governs every model
Meta-model consumption discipline (read, don't hardcode) — Read the model at runtime; never hardcode a snapshot. governs every model
Model query surface (`repo-query`) — repo-query — the agent-facing read API over the models. governs every model
Model-derived test-obligation census (derive what should be tested, lint the gap) — Derive the should-be-tested set from the models and lint the gap to the tests that exist. governs every model
Model-driven codegen — Generate real artifacts from the models, provenance-headed. governs every model
Model-graded finding severity (distance-graded gate) — A gate grades each finding block/warn/silence by its model-distance from the changed files. governs every model
Orphan-coverage metric (walk code → governance; score the un-covered remainder) — Walk code → governing model/control; score the orphans; each orphan cluster is candidate work. governs every model
The agent-first MBSE harness — Structured frozen-record models + five hand-rolled disciplines; adopt the schema, skip the runtime. governs every model