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.

SummaryA registry of every lock, what it guards, and its ordering.
TargetBridge · System models
Formtyped-ir
EnforcementHard (deterministic) — a typed model held true by the lock-coverage lint (every fcntl.flock site must be declared or annotated)

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

Consequences & costs

Known uses

Related mechanisms