Concurrent processes, their lanes, and the edges where they race over shared state.

Process view (concurrent processes, lanes, and racing edges)

Intent — Project a system's concurrency as an explicit process view: the concurrent processes that run at once, the lanes they run in, and the racing edges where two of them touch shared state at the same time. It answers a different question than the machines-and-invariants model beneath it — not "what are the legal transitions?" but "what is live simultaneously, and where can they collide?" — so a race is a named edge you can point at, review, and guard, not a surprise found in production (our instance: a concurrent-process-and-lane projection over the composed lifecycle machines, naming each racing edge as a first-class element).

SummaryConcurrent processes, their lanes, and the edges where they race over shared state.
TargetBridge · System models
Formtyped-ir
Movepackage — a constraint shipped with its sensors
Modelis-a-model — a structured model you check a system property against
EnforcementHard (deterministic) — a typed projection held true against the concurrency structure it views; a declared racing edge with no guarding lock, or a lock guarding no declared edge, is a build finding
Derivationmodel-from-code — projected from the concurrency structure and reconciled against the real concurrent processes

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

Concurrency bugs are the ones a static read of the code never shows. Every process looks correct on its own; the defect lives in the simultaneity — two workers popping the same queue entry, a preemption requeue racing a terminal write, a cache refreshed by one process while another reads it half-written. Teams carry this knowledge as folklore: someone remembers that these two paths must not run at once, and when that person is an agent with no memory across sessions, the folklore is simply gone. Nothing in the codebase names the set of things that run concurrently, so nothing enumerates the pairs that can collide, so no one can check that each collision is guarded. The race is invisible until it fires, and it fires rarely enough to survive every test that isn't looking for it.

Why it's not just the state-machine model

The composed state-machine model and this view describe the same concurrency, but they answer different questions, and folding them into one blurs both. The machine model is about legality over time: for one lifecycle, which transitions are allowed and which predicates hold across the machines. The process view is about simultaneity in space: which processes are alive at the same moment, which lane each occupies, and which pairs share a resource. An invariant like "a chunk is never both leased and free" belongs to the machine model; "the preemption requeue and the stale-sweep both write the chunk row, so that edge is a race" belongs here. You can hold every transition legal and still have an unguarded race, because the race is a relationship between two processes, not a property of either one's state graph. Keeping the view separate is what lets a reviewer scan the racing edges without re-deriving them from the transition tables every time.

Mechanism

Prerequisites

Consequences & costs

Known uses

Related mechanisms

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.