Appendix B - 20. Synchronization model (meta-sync)

The Structure of Synchronization model (meta-sync) — its shape at a glance:

Three record kinds compose the registry — the lock, its acquisition site, and an ordering constraint. A coverage lint flags an undeclared lock; an ordering lint walks the constraint graph and flags an inverted acquisition.

erDiagram
  LOCK ||--o{ ACQUIRER : "acquired at"
  LOCK ||--o{ ORDERING : "constrains"
  LOCK {
    string path PK
    int cap
  }
  ACQUIRER {
    string site PK
    string path FK
  }
  ORDERING {
    string before FK
    string after FK
  }

Accessible description: a lock record relates to many acquisition sites and many ordering constraints. A coverage lint checks every real lock call site is a declared acquirer; an ordering lint checks acquisitions respect the before/after constraints.

Projected from the catalogue entry system-models / Synchronization model (meta-sync).

On this page: Intent · Motivation · Applicability · Structure · Sample Code · Consequences · Example use within DocAble · Related Patterns

Intent

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.

Motivation

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.

Applicability

• 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.

Structure

The Structure diagram appears at the top of this page.

Sample Code

The registry declares each lock and the order pairs. An ordering lint walks a lock-acquisition sequence against the declared graph and fails on an inversion — so a deadlock-inducing order is caught at author time, not suffered in production.

import sys

# Declared ordering: a lock in `before` must be acquired before its `after` lock.
ORDERINGS = [("db-lock", "cache-lock")]      # db before cache, always

def ordering_lint(acquire_sequence: list[str]) -> list[str]:
    """A held-lock acquiring one that must precede it is an inversion (deadlock risk)."""
    findings, held = [], []
    for lock in acquire_sequence:
        for before, after in ORDERINGS:
            if lock == before and after in held:
                findings.append(f"acquired '{before}' while holding '{after}' — order inverted")
        held.append(lock)
    return findings

if __name__ == "__main__":
    # `walk_acquisitions` reads a code path's lock-acquisition order from the declared sites.
    findings = ordering_lint(walk_acquisitions())
    for f in findings:
        print(f"LOCK-ORDER: {f}")
    sys.exit(1 if findings else 0)

Consequences

• 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.

Example use within DocAble

• 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 Patterns

• 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.