Module concurrency_mesh 

LOGOS concurrency pattern RECOGNIZERS — the source-reading half of the concurrency tier.

A Launch a task to producer with ch + Send v into ch (in the task) + Receive x from ch (in main) is CSP dataflow, and this module is what READS that out of a LOGOS program: the pipe, the fan-out, the loop-driven producer, the select, and the two racing selects, each reduced to a spec of exactly what the source said. A non-matching program is DECLINED (the caller falls back to the sound refusal), never miscompiled.

★ THE EMITTERS ARE GONE; THE RECOGNIZERS ARE THE POINT. This module used to end each recognizer with a hand-written pair of baby-RISC-V kernels around a circular buffer — the producer pushing, the consumer waiting and popping, with the recognized values baked into the C++ as a const uint32_t vals[N]. Those kernels are now PRINTED FROM THE SPATIAL IR like every other lowering (spatial::passes::from_tensor_op builds the template, the Tensix printer emits it), because a pattern that is spelled out by hand is a claim about a kernel while a pattern that is lowered is a claim about a program: the same numbers, but reachable by every pass, the census and the evaluator instead of sealed inside text.

★ EVERY RESOLUTION HERE IS COMPILE-TIME, WHICH IS WHY THE IR STAYS A MARKED GRAPH. A select does not race: the VM’s virtual-time scheduler fires whichever event has the smaller virtual time, and both times are literals of the source. So the compiler RESOLVES the arm and lowers the resolved program, rather than teaching the IR a free choice — which would cost the confluence that makes eval_choreography_confluent a proof rather than a spot-check, for every program sharing the IR.

Structs

ConcurrencySpec

A recognized producer/consumer pipe program: a task sends a fixed sequence of integers into a pipe, and main receives them and folds them (first increment: an integer sum) into a shown result.

DynamicSpec

A recognized dynamic-channel producer: Repeat for i from lo to hi: Send <expr> into ch. The pipe is fed by a LOOP, and each sent value is a (possibly computed) expression of the loop variable.

FanoutSpec

A recognized fan-out: N distinct tasks each send one value into a shared pipe, and main receives all N and folds them (commutative sum — so the mesh’s arrival order doesn’t matter and it stays ≡VM).

MeshLowering

What the concurrency tier produces for a recognized pattern: what the SOURCE said, and the spatial program it lowers to.

RacyMultiSpec

A recognized multi-task race: N tasks each sleep then send; main awaits receive-or-timeout. The deterministic scheduler fires the global-minimum-virtual-time event.

RacySelectSpec

A recognized racy select: a task sleeps then sends; main awaits the first of {receive, timeout}. The VM’s deterministic scheduler fires the smaller-virtual-time event, so the outcome is a COMPARISON of the send’s virtual time (the task’s cumulative sleep) against the timeout — reproducible on the mesh by a coordinator core, independent of real hardware timing.

SelectSpec

A recognized select (Await the first of { Receive … / After … }) on a READY channel: main pre-sends presend into the pipe, so the deterministic scheduler takes the RECEIVE arm; timeout_ticks is the (dead-on-this-path) timeout duration.

Functions

recognize_dynamic_producer

Recognize a loop-driven producer: main launches a task whose body is a single Repeat for i from lo to hi: Send <expr> into ch. Extracts the bounds + the C send expression.

recognize_fanout

Recognize the fan-out pattern: main launches N (≥2) distinct tasks, each of which sends exactly one integer literal into a shared pipe, and main receives N values. None if the program is not this shape.

recognize_multi_racy

Recognize a multi-task race: main launches ≥2 tasks (each sleeps then sends one literal, no pre-send in main) and awaits the first of a receive + a timeout. Extracts each task’s (value, send-vtime) + timeout.

recognize_producer_consumer

Recognize the producer/consumer pipe pattern and extract its ConcurrencySpec, or None if the program is not this shape (the caller then falls back to the sound single-core refusal).

recognize_racy_select

Recognize a racy select: main launches a task (which sleeps then sends one literal) and awaits the first of a receive + a timeout, with NO pre-send in main. Extracts the send’s virtual time + the timeout.

recognize_select

Recognize a select on a ready channel: Send v into ch then Await the first of { Receive x from ch: …; After n …: … }. Returns the spec, or None if not this shape.