MS1V8 mlir-stage-19-v1 passing 5000/5000
Estimated confidence: 91.1%. Conservative lower bound: 3.6% (95% level).
uniform over observed structural partitions. observed partitions; unseen partitions have no supplied target weight. Partitions use recursive production counts and derivation depth. Behavioral classes combine each input’s compiler coverage and assertion decision paths. Catalog partitions with no observations retain maximal missing mass.
Baseline tests: Every tracked test file with a RUN line invoking loom-raise-opt (77 files); other executables and native unit tests excluded
| Source file | Baseline coverage | Baseline + input | Contributing input |
|---|---|---|---|
…/lib/Dataflow/IR/DataflowFunctionLikeOps.cppMS1V | 693/1097lines63.2% 264/592branches44.6% | 734/1097lines66.9%+41 287/592branches48.5%+23 | |
41 newly covered lines · 23 newly covered branches102 | |||
…/lib/Frontend/Lowering/LowerForallToThreadPass.cppMS1V | 30/34lines88.2% 2/4branches50.0% | 31/34lines91.2%+1 4/4branches100.0%+2 | |
1 newly covered line · 2 newly covered branches37 | |||
…/lib/Dataflow/IR/DataflowDialect.cppMS1V | 22/32lines68.8% 4/10branches40.0% | 22/32lines68.8%+0 4/10branches40.0%+0 | Open PBT |
…/lib/Dataflow/IR/OperationSchema.cppMS1V | 274/716lines38.3% 127/350branches36.3% | 274/716lines38.3%+0 127/350branches36.3%+0 | Open PBT |
…/lib/Dataflow/Transforms/DataflowRewritePass.cppMS1V | 338/559lines60.5% 172/340branches50.6% | 338/559lines60.5%+0 172/340branches50.6%+0 | Open PBT |
…/lib/Frontend/Lowering/ExpandGraphMemrefCopyPass.cppMS1V | 79/90lines87.8% 20/22branches90.9% | 79/90lines87.8%+0 20/22branches90.9%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerForToGraphPass.cppMS1V | 1033/1240lines83.3% 374/540branches69.3% | 1033/1240lines83.3%+0 374/540branches69.3%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerGraphConstantsPass.cppMS1V | 80/83lines96.4% 18/24branches75.0% | 80/83lines96.4%+0 18/24branches75.0%+0 | Open PBT |
…/lib/Frontend/Lowering/LowerGraphMemoryPass.cppMS1V | 525/841lines62.4% 208/400branches52.0% | 525/841lines62.4%+0 208/400branches52.0%+0 | Open PBT |
…/lib/Frontend/Lowering/Pipeline.cppMS1V | 18/21lines85.7% branchesnot measured | 18/21lines85.7%+0 branchesnot measured | Open PBT |
…/lib/Frontend/Raising/DeduplicateSCFWhileStatePass.cppMS1V | 13/135lines9.6% 0/60branches0.0% | 13/135lines9.6%+0 0/60branches0.0%+0 | Open PBT |
…/lib/Frontend/Raising/LLVMArithToArithPass.cppMS1V | 300/319lines94.0% 94/116branches81.0% | 300/319lines94.0%+0 94/116branches81.0%+0 | Open PBT |
…/lib/Frontend/Raising/LLVMCfToCfPass.cppMS1V | 77/80lines96.2% 8/8branches100.0% | 77/80lines96.2%+0 8/8branches100.0%+0 | Open PBT |
…/lib/Frontend/Raising/LiftCFToSCFPass.cppMS1V | 616/694lines88.8% 293/386branches75.9% | 616/694lines88.8%+0 293/386branches75.9%+0 | Open PBT |
…/lib/Frontend/Raising/MaterializeFMulAddPass.cppMS1V | 70/106lines66.0% 11/26branches42.3% | 70/106lines66.0%+0 11/26branches42.3%+0 | Open PBT |
…/lib/Frontend/Raising/NormalizeLiftedSCFExitPass.cppMS1V | 232/250lines92.8% 120/182branches65.9% | 232/250lines92.8%+0 120/182branches65.9%+0 | Open PBT |
…/lib/Frontend/Raising/Pipeline.cppMS1V | 10/19lines52.6% branchesnot measured | 10/19lines52.6%+0 branchesnot measured | Open PBT |
…/lib/Frontend/Raising/SCFForToForallPass.cppMS1V | 494/738lines66.9% 241/458branches52.6% | 494/738lines66.9%+0 241/458branches52.6%+0 | Open PBT |
…/lib/Frontend/Raising/SCFWhileToForPass.cppMS1V | 164/176lines93.2% 70/94branches74.5% | 164/176lines93.2%+0 70/94branches74.5%+0 | Open PBT |
…/loom/tools/loom-raise-opt/loom-raise-opt.cppMS1V | 12/12lines100.0% branchesnot measured | 12/12lines100.0%+0 branchesnot measured | Open PBT |
N block arguments mirror function_type.inputs
exactly (each user body operand). Putting the signature args
first preserves the upstream FunctionOpInterface invariant
that the entry block's first N arguments correspond to
function_type.inputs[0..N]. This matches the gpu.func
precedent of "function args first, implicit extras after".dataflow.thread private @thread_0 domain(#dataflow.thread_domain<dense>)(%buf: memref<8xi32>) ctrl (%thread_ctrl: none) iv (%coord_0: index, %coord_1: index) { scf.forall (%lane) in (8) { } dataflow.thread.yield %thread_ctrl : none } func.func @host_0() { %buf = memref.alloc() : memref<8xi32> %g0 = arith.constant 4 : index %g1 = arith.constant 4 : index %token = dataflow.thread.launch @thread_0(%buf) grid(%g0, %g1) : (memref<8xi32>) -> !dataflow.thread_token return }
dataflow.thread private @thread_0 domain(#dataflow.thread_domain<dense>)(%buf: memref<8xi32>, %arg0: f32) ctrl (%thread_ctrl: none) iv (%coord_0: index) { %value = arith.constant 7 : i32 dataflow.thread.yield %thread_ctrl : none } func.func @host_0() { %buf = memref.alloc() : memref<8xi32> %h0 = arith.constant 1.000000e+00 : f32 %g0 = arith.constant 4 : index %token = dataflow.thread.launch @thread_0(%buf, %h0) grid(%g0) : (memref<8xi32>, f32) -> !dataflow.thread_token return } dataflow.thread private @thread_1 domain(#dataflow.thread_domain<dense>)(%buf: memref<8xi32>, %arg0: i32) ctrl (%thread_ctrl: none) { %value = arith.constant 7 : i32 scf.forall (%lane) in (2) { memref.store %value, %buf[%lane] : memref<8xi32> } dataflow.thread.yield } func.func @host_1() { %buf = memref.alloc() : memref<8xi32> %h0 = arith.constant 3 : i32 %token = dataflow.thread.launch @thread_1(%buf, %h0) : (memref<8xi32>, i32) -> !dataflow.thread_token return }
Part 3 rejects this form before graph mutation. It never drops the combining
region or publishes a dataflow.graph that omits the aggregation.
When the selected nest is inside an already materialized rank-zero Spatial ownership carrier, the same atomic decision promotes the new forall to the carrier's dense logical thread domain.
Code inside the thread definition remains InstructionCore code unless the
selected Structured Program Candidate explicitly wraps it in
loom.spatial_region. That compiler-internal region remains the temporary
SpatialCore ownership carrier until Part 3 atomically replaces it with a
finalized dataflow.graph definition and launch.
If Part 2 selects an effect-form forall as an AccCore thread domain, the input accepted by Part 3 is already the definition-and-launch carrier shape below.
An unprojectable bound rejects only that candidate. The transformation never weakens the fixed-domain requirement for a retained graph-owned parallel form.
retained a graph-owned forall only as a mapping-free, effect-form,
compile-time fixed-domain construct whose P[] width, ownership, and
cross-lane legality are materialized in semantic IR and can be re-proved;
A dynamic domain, mapping attribute, shared output, result, combining action, or failed legality re-proof causes atomic failure before canonical graph publication. Cached provenance never changes this result.
For this boundary, an accepted effect-form forall has no shared_outs, no op
results, and an empty scf.forall.in_parallel terminator.
materialized every supported aggregation or reduction into accepted semantics, or failed finalizability truthfully.
candidate.pg// Part 3 definition-and-launch carrier inputs for loom-lower-forall-to-thread. // Each sample is a module of `dataflow.thread` definitions (dense domain, // private visibility, entry block `(args_*, thread_ctrl, coord_*)`) whose // bodies carry a mapping-free, effect-form, compile-time fixed-domain // `scf.forall` with no shared_outs, no results and an empty in_parallel // terminator, paired with the module-scope launch of each definition. start: {new NTHREADS = random.randint(1, 3); new T = 0} module_body; module_body: (T < NTHREADS) thread_unit {T += 1} module_body | (T == NTHREADS) ''; thread_unit: {new EXTRA = random.randint(0, 2); new RANK = random.randint(0, 2); new TYPES = []; new A = 0; new B = 0; new C = 0; new D = 0; new G = 0; new H = 0; new K = 0} 'dataflow.thread private @thread_' t_idx ' domain(#dataflow.thread_domain<dense>)(%buf: memref<8xi32>' extra_decls ') ctrl (%thread_ctrl: none)' iv_clause ' {\n' thread_body '}\n' host_func; t_idx: [str(T)]; // Payload arguments after the leading memref: the `args_*` prefix. extra_decls: (A < EXTRA) {TYPES.append(random.choice(['i32', 'f32', 'index']))} ', %arg' a_idx ': ' a_ty {A += 1} extra_decls | (A == EXTRA) ''; a_idx: [str(A)]; a_ty: [TYPES[A]]; // Dense coordinate suffix: one `index` slot per launch-domain dimension. iv_clause: (RANK == 0) '' | (RANK > 0) ' iv (' iv_decls ')'; iv_decls: (K < RANK) iv_sep '%coord_' k_idx ': index' {K += 1} iv_decls | (K == RANK) ''; iv_sep: (K == 0) '' | (K > 0) ', '; k_idx: [str(K)]; thread_body: ' %value = arith.constant 7 : i32\n' forall_op yield_op; // Effect-form forall: no shared_outs, no results, no mapping attribute, // compile-time fixed zero-based domain, empty in_parallel terminator. forall_op: ' scf.forall (%lane) in (' extent ') {\n' ' memref.store %value, %buf[%lane] : memref<8xi32>\n' ' }\n' | ''; extent: '2' | '4' | '8'; yield_op: ' dataflow.thread.yield\n' | ' dataflow.thread.yield %thread_ctrl : none\n'; host_func: 'func.func @host_' t_idx '() {\n' ' %buf = memref.alloc() : memref<8xi32>\n' extra_defs grid_defs ' %token = dataflow.thread.launch @thread_' t_idx '(%buf' extra_uses ')' grid_clause ' : (memref<8xi32>' extra_types ') -> !dataflow.thread_token\n' ' return\n' '}\n'; extra_defs: (B < EXTRA) ' %h' b_idx ' = ' const_rhs '\n' {B += 1} extra_defs | (B == EXTRA) ''; b_idx: [str(B)]; const_rhs: (TYPES[B] == 'i32') 'arith.constant 3 : i32' | (TYPES[B] == 'f32') 'arith.constant 1.000000e+00 : f32' | (TYPES[B] == 'index') 'arith.constant 2 : index'; extra_uses: (C < EXTRA) ', %h' c_idx {C += 1} extra_uses | (C == EXTRA) ''; c_idx: [str(C)]; extra_types: (D < EXTRA) ', ' d_ty {D += 1} extra_types | (D == EXTRA) ''; d_ty: [TYPES[D]]; grid_defs: (G < RANK) ' %g' g_idx ' = arith.constant 4 : index\n' {G += 1} grid_defs | (G == RANK) ''; g_idx: [str(G)]; grid_clause: (RANK == 0) '' | (RANK > 0) ' grid(' grid_uses ')'; grid_uses: (H < RANK) grid_sep '%g' h_idx {H += 1} grid_uses | (H == RANK) ''; grid_sep: (H == 0) '' | (H > 0) ', '; h_idx: [str(H)];
The first
Nblock arguments mirrorfunction_type.inputsexactly (each user body operand). Putting the signature args first preserves the upstreamFunctionOpInterfaceinvariant that the entry block's firstNarguments correspond tofunction_type.inputs[0..N].
candidate.spctpostcondition thread_entry_prefix_mirrors_function_inputs { language v0; vocabulary mlir = mlir.generic@1; metadata { project = "PolyArch/loom"; revision = "48615bc5925ef4b9db8b4550b5d4322933cf4b7b"; source = "docs/spec-compiler-part-3-dfg.md:L1008-L1013"; } constraints { let bodied_threads = seq { op | op in output.operations where op.name == "dataflow.thread" and cardinality(op.regions) >= 1 and cardinality(op.regions[0].blocks) >= 1 }; forall t in bodied_threads { assert entry_prefix_mirrors_function_type_inputs: forall pair in zip_exact( seq { a.type | a in t.regions[0].blocks[0].arguments.take( cardinality(t.attributes["function_type"].type.inputs)) }, t.attributes["function_type"].type.inputs) where pair.left == pair.right; } } }
dataflow.thread private @thread_0 domain(#dataflow.thread_domain<dense>)(%buf: memref<8xi32>) ctrl (%thread_ctrl: none) iv (%coord_0: index, %coord_1: index) { scf.forall (%lane) in (8) { } dataflow.thread.yield %thread_ctrl : none } func.func @host_0() { %buf = memref.alloc() : memref<8xi32> %g0 = arith.constant 4 : index %g1 = arith.constant 4 : index %token = dataflow.thread.launch @thread_0(%buf) grid(%g0, %g1) : (memref<8xi32>) -> !dataflow.thread_token return }
20260911-085053started2026-09-11T08:50:53Zsubjectloom-raise-optsubject revision48615bc5925erun results
output condition verdicts
raw trace evidence
dataflow.thread private @thread_0 domain(#dataflow.thread_domain<dense>)(%buf: memref<8xi32>, %arg0: f32) ctrl (%thread_ctrl: none) iv (%coord_0: index) { %value = arith.constant 7 : i32 dataflow.thread.yield %thread_ctrl : none } func.func @host_0() { %buf = memref.alloc() : memref<8xi32> %h0 = arith.constant 1.000000e+00 : f32 %g0 = arith.constant 4 : index %token = dataflow.thread.launch @thread_0(%buf, %h0) grid(%g0) : (memref<8xi32>, f32) -> !dataflow.thread_token return } dataflow.thread private @thread_1 domain(#dataflow.thread_domain<dense>)(%buf: memref<8xi32>, %arg0: i32) ctrl (%thread_ctrl: none) { %value = arith.constant 7 : i32 scf.forall (%lane) in (2) { memref.store %value, %buf[%lane] : memref<8xi32> } dataflow.thread.yield } func.func @host_1() { %buf = memref.alloc() : memref<8xi32> %h0 = arith.constant 3 : i32 %token = dataflow.thread.launch @thread_1(%buf, %h0) : (memref<8xi32>, i32) -> !dataflow.thread_token return }
"builtin.module"() ({ "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<8xi32>, f32) -> (), sym_name = "thread_0", sym_visibility = "private"}> ({ ^bb0(%arg4: memref<8xi32>, %arg5: f32, %arg6: none, %arg7: index): %8 = "arith.constant"() <{value = 7 : i32}> : () -> i32 "dataflow.thread.yield"(%arg6) : (none) -> () }) : () -> () "func.func"() <{function_type = () -> (), sym_name = "host_0"}> ({ %4 = "memref.alloc"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> memref<8xi32> %5 = "arith.constant"() <{value = 1.000000e+00 : f32}> : () -> f32 %6 = "arith.constant"() <{value = 4 : index}> : () -> index %7 = "dataflow.thread.launch"(%4, %5, %6) <{callee = @thread_0, operandSegmentSizes = array<i32: 2, 1, 0>}> : (memref<8xi32>, f32, index) -> !dataflow.thread_token "func.return"() : () -> () }) : () -> () "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = (memref<8xi32>, i32) -> (), sym_name = "thread_1", sym_visibility = "private"}> ({ ^bb0(%arg0: memref<8xi32>, %arg1: i32, %arg2: none): %3 = "arith.constant"() <{value = 7 : i32}> : () -> i32 "scf.forall"() <{operandSegmentSizes = array<i32: 0, 0, 0, 0>, staticLowerBound = array<i64: 0>, staticStep = array<i64: 1>, staticUpperBound = array<i64: 2>}> ({ ^bb0(%arg3: index): "memref.store"(%3, %arg0, %arg3) : (i32, memref<8xi32>, index) -> () "scf.forall.in_parallel"() ({ ^bb0: }) : () -> () }) : () -> () "dataflow.thread.yield"() : () -> () }) : () -> () "func.func"() <{function_type = () -> (), sym_name = "host_1"}> ({ %0 = "memref.alloc"() <{operandSegmentSizes = array<i32: 0, 0>}> : () -> memref<8xi32> %1 = "arith.constant"() <{value = 3 : i32}> : () -> i32 %2 = "dataflow.thread.launch"(%0, %1) <{callee = @thread_1, operandSegmentSizes = array<i32: 2, 0, 0>}> : (memref<8xi32>, i32) -> !dataflow.thread_token "func.return"() : () -> () }) : () -> () }) : () -> ()
partial source coverage: Approved for execution and public reporting; translation accuracy and completeness remain separately unvalidated.
authoring-context.json{"entries":[{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"988-1037","path":"docs/spec-compiler-part-3-dfg.md","roles":["context","input_construction","input_well_formedness"],"text":"* `dataflow.thread` is a Symbol-bearing, module-scope, function-\n like callable. It does not itself execute; one or more\n `dataflow.thread.launch` ops materialize launches of it.\n* `function_type` is a `FunctionType` whose inputs are the kernel's\n user-data operand types `(T0, ..., TN)` and whose results are\n empty. The thread definition has no SSA data results; the\n per-launch completion token is launch-side, not part of the\n callable signature. Asynchronous execution is expressed by launch\n dependencies and the mandatory launch completion token, not by the\n function type.\n* `sym_name` is required and module-unique. `sym_visibility` is\n required and must equal `\"private\"` under the baseline visibility\n policy. The verifier rejects `\"public\"` and `\"nested\"` unless\n cross-module linkage is enabled by a separate spec.\n* `domain` is the closed `DenseRectangular` or\n `DynamicWork { work_item_arg_ordinal }` value owned by Part 4. A dynamic\n definition has coordinate rank zero and its ordinal must select exactly one\n `function_type` input. A dense definition has no work-item ordinal.\n* A dense entry block has the layout `(args_*, thread_ctrl, coord_*)`; a\n dynamic entry block has `(args_*, thread_ctrl)`:\n - The first `N` block arguments mirror `function_type.inputs`\n exactly (each user body operand). Putting the signature args\n first preserves the upstream `FunctionOpInterface` invariant\n that the entry block's first `N` arguments correspond to\n `function_type.inputs[0..N]`. This matches the `gpu.func`\n precedent of \"function args first, implicit extras after\".\n - `thread_ctrl : none` is the per-launch AccCore start signal.\n It is produced by the launch op once async dependencies are\n satisfied and the AccCore instance begins execution. Root\n `dataflow.graph.launch` ops with no InstructionCore predecessor use\n this value as their `ctrl_in` operand.\n - For a dense definition, `coord_0, ..., coord_{K-1} : index` are the\n per-instance logical\n coordinates, one per launch-domain dimension, in source-dimension order.\n Their count is the definition's coordinate rank. Rank is derived from\n this canonical suffix after the `function_type` inputs and unique\n `thread_ctrl`; there is no duplicate rank, grid, or mapping attribute.\n - For a dynamic definition, the designated ordinary argument carries the\n current work-item payload. The runtime `WorkItemId` is execution identity,\n not an additional SSA argument or payload wrapper.\n* `arg_attrs` is indexed only by the `args_*` payload prefix. Forall\n promotion copies each captured source function argument dictionary,\n including arbitrary attributes such as `llvm.noalias`, into capture order.\n Locally defined captures have an empty dictionary. `thread_ctrl` and\n `coord_*` are not payload arguments and never inherit source argument\n metadata.\n* The body is `IsolatedFromAbove`. No SSA value defined outside\n the def's body may be used inside it; the launch's body operands\n are the only inputs.\n#### 5.4.2 `dataflow.thread.launch`","why":"Governing context for dataflow.thread: private visibility, result-free function_type, closed dense/dynamic domain, and the (args_*, thread_ctrl, coord_*) entry-block layout that the generated definition-and-launch carrier inputs must instantiate."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"2008-2023","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction","input_well_formedness"],"text":"* retained a graph-owned forall only as a mapping-free, effect-form,\n compile-time fixed-domain construct whose `P[]` width, ownership, and\n cross-lane legality are materialized in semantic IR and can be re-proved;\n and\n* materialized every supported aggregation or reduction into accepted\n semantics, or failed finalizability truthfully.\n\nPart 3 does not convert aggregation form, decide thread ownership, rewrite\nforall to parallel as an optimization policy, infer `P[]`, serialize lanes, or\nselect a reduction strategy. A dynamic domain, mapping attribute, shared\noutput, result, combining action, or failed legality re-proof causes atomic\nfailure before canonical graph publication. Cached provenance never changes\nthis result.\n\nFor this boundary, an accepted effect-form forall has no `shared_outs`, no op\nresults, and an empty `scf.forall.in_parallel` terminator. In the example,","why":"Fixes the accepted forall form carried into Part 3: mapping-free, effect-form, compile-time fixed domain, no shared_outs, no results, empty scf.forall.in_parallel terminator, and no dynamic domain."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"2052-2061","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction","applicability"],"text":"Part 3 rejects this form before graph mutation. It never drops the combining\nregion or publishes a `dataflow.graph` that omits the aggregation. Any legal\nmaterialization belongs to the Part 2 owner; this document intentionally does\nnot define a bufferization or combining algorithm.\n\nIf Part 2 selects an effect-form forall as an AccCore thread domain, the input\naccepted by Part 3 is already the definition-and-launch carrier shape below.\nThe rank-one source sketch is retained only to relate the source induction\nvariable to the canonical logical-coordinate ABI; it is not a Part 3\ntransformation:","why":"States that a forall selected as an AccCore thread domain reaches Part 3 already in the definition-and-launch carrier shape, which is the input shape the grammar samples."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"2096-2100","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction"],"text":"Code inside the thread definition remains InstructionCore code unless the\nselected Structured Program Candidate explicitly wraps it in\n`loom.spatial_region`. That compiler-internal region remains the temporary\nSpatialCore ownership carrier until Part 3 atomically replaces it with a\nfinalized `dataflow.graph` definition and launch. Memory operations outside","why":"Code inside a thread definition stays InstructionCore code unless explicitly wrapped in loom.spatial_region, justifying thread bodies that hold plain scf/memref code without a spatial region."},{"file_sha256":"bfc1e646e91fe0ba6d7d16e43994100b05c3b8ff79c2e07288e8955c43d9d79d","kind":"documentation_input","lines":"934-942","path":"docs/spec-compiler-part-2-scf.md","roles":["input_construction","input_well_formedness"],"text":"temporary joint proof do not survive in the child. When the selected nest is\ninside an already materialized rank-zero Spatial ownership carrier, the same\natomic decision promotes the new forall to the carrier's dense logical thread\ndomain. Ownership remains the sole owner of extent arithmetic and\nsource-induction reconstruction: every exact thread launch must project all\nbounds from its body operands, the thread and Spatial ABIs acquire the rank-N\ncoordinate suffix, and no graph-owned forall remains. An unprojectable bound\nrejects only that candidate. The transformation never weakens the fixed-domain\nrequirement for a retained graph-owned parallel form.","why":"Promotion into a dense logical thread domain and the fixed-domain requirement for a retained graph-owned parallel form; drives the zero-based constant forall extents and dense domain attribute in generated inputs."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"614-739","path":"include/Dataflow/IR/DataflowOps.td","roles":["input_construction","input_well_formedness"],"text":"def Dataflow_ThreadOp : Dataflow_Op<\"thread\", [\n AutomaticAllocationScope,\n IsolatedFromAbove,\n HasParent<\"::mlir::ModuleOp\">,\n SingleBlockImplicitTerminator<\"ThreadYieldOp\">,\n FunctionOpInterface,\n RecursiveMemoryEffects\n]> {\n let summary = \"Symbol-bearing function-like AccCore kernel definition\";\n let description = [{\n Module-scope, function-like callable that holds an AccCore kernel\n body. It does not itself execute; one or more\n `dataflow.thread.launch` ops materialize launches of it.\n\n The body's entry block has the layout\n `(args_*, thread_ctrl: none, iv_*: index)` (per spec section\n 5.4.1). The first N block args mirror `function_type.inputs`; the\n trailing `thread_ctrl` and grid index args are NOT in\n `function_type` (they are launch-instance extras). Specifically:\n\n * Args[0 .. N-1] match `function_type.inputs` position-wise.\n * Args[N] is `none` -- the per-launch `thread_ctrl`\n slot, used as the AccCore start signal and\n consumed by root `dataflow.graph.launch` ops\n in the body as a dependency event.\n * Args[N+1 .. end] are all `index` -- one per grid dim.\n\n The custom assembly format prints the required `domain(...)` immediately\n after the symbol and the trailing extras after the function-style\n signature using a separate `ctrl ( ... )` clause\n (the `thread_ctrl` slot) and an `iv ( ... )` clause (the\n grid-index slots). Either / both clauses are optional; threads\n written without them are accepted at parse time only when the op\n is external (i.e., body is empty), since a body-having thread\n must carry the trailing `thread_ctrl` slot per the verifier.\n\n The op is `IsolatedFromAbove`; values flow in only through the\n matching `dataflow.thread.launch` body operands.\n\n Every definition carries one closed `domain`: DenseRectangular or\n DynamicWork. Dense rank is derived solely from the trailing index block\n arguments. DynamicWork carries one ordinary function-input ordinal and has\n no coordinate suffix.\n }];\n\n let arguments = (ins\n SymbolNameAttr:$sym_name,\n TypeAttrOf<FunctionType>:$function_type,\n Dataflow_ThreadDomainAttr:$domain,\n OptionalAttr<StrAttr>:$sym_visibility,\n OptionalAttr<DictArrayAttr>:$arg_attrs,\n OptionalAttr<DictArrayAttr>:$res_attrs);\n\n let regions = (region SizedRegion<1>:$body);\n\n let hasCustomAssemblyFormat = 1;\n let hasVerifier = 1;\n\n let builders = [\n OpBuilder<(ins\n \"::llvm::StringRef\":$name,\n \"::mlir::FunctionType\":$type,\n \"::dataflow::ThreadDomainAttr\":$domain,\n CArg<\"::llvm::ArrayRef<::mlir::NamedAttribute>\", \"{}\">:$attrs)>\n ];\n\n let extraClassDeclaration = [{\n /// FunctionOpInterface methods.\n ::llvm::ArrayRef<::mlir::Type> getArgumentTypes() {\n return getFunctionType().getInputs();\n }\n ::llvm::ArrayRef<::mlir::Type> getResultTypes() {\n return getFunctionType().getResults();\n }\n ::mlir::Region *getCallableRegion() {\n return isExternal() ? nullptr : &getBody();\n }\n bool isExternal() { return getBody().empty(); }\n\n /// Override the default FunctionOpInterface body verifier: a\n /// dataflow.thread body's entry block leads with the\n /// function-signature args, then a `none`-typed `thread_ctrl`\n /// slot, then zero or more `index`-typed `iv_*` slots (per spec\n /// section 5.4.1: `(args_*, thread_ctrl, iv_*)`).\n ::llvm::LogicalResult verifyBody() {\n if (isExternal())\n return ::mlir::success();\n ::mlir::Block &entry = getBody().front();\n ::llvm::ArrayRef<::mlir::Type> inputs = getFunctionType().getInputs();\n const size_t N = inputs.size();\n // Body-carrying threads MUST have the trailing thread_ctrl slot.\n if (entry.getNumArguments() < N + 1)\n return emitOpError(\"entry block must have at least \")\n << (N + 1)\n << \" arguments (function inputs + 1 thread_ctrl slot)\";\n // First N entry block arguments must match function_type.inputs.\n for (size_t i = 0; i < N; ++i) {\n if (entry.getArgument(i).getType() != inputs[i])\n return emitOpError(\"type of entry block argument #\")\n << i << '(' << entry.getArgument(i).getType()\n << \") must match the corresponding function signature input (\"\n << inputs[i] << ')';\n }\n // Slot N must be the `none`-typed thread_ctrl per spec\n // section 5.4.1.\n if (!::llvm::isa<::mlir::NoneType>(entry.getArgument(N).getType()))\n return emitOpError(\"entry block argument #\")\n << N << \" (thread_ctrl) must have type `none`, got \"\n << entry.getArgument(N).getType();\n if (getDomain().getKind() ==\n ::dataflow::ThreadDomainKind::DynamicWork &&\n entry.getNumArguments() != N + 1)\n return emitOpError(\"dynamic-work thread body must not have coordinate \"\n \"arguments\");\n // All remaining dense-domain slots are grid induction variables of\n // `index`.\n for (size_t i = N + 1, e = entry.getNumArguments(); i < e; ++i) {\n if (!::llvm::isa<::mlir::IndexType>(entry.getArgument(i).getType()))\n return emitOpError(\"entry block argument #\")\n << i << \" (grid iv) must have type `index`, got \"\n << entry.getArgument(i).getType();\n }\n return ::mlir::success();\n }\n }];\n}","why":"Dataflow_ThreadOp definition: operands/attributes (sym_name, function_type, domain, sym_visibility), the custom `domain(...) (...) ctrl (...) iv (...)` assembly clauses, and verifyBody's entry-block prefix/ctrl/index slot requirements that generated inputs must satisfy."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"741-820","path":"include/Dataflow/IR/DataflowOps.td","roles":["input_construction","input_well_formedness"],"text":"def Dataflow_ThreadYieldOp : Dataflow_Op<\"thread.yield\", [\n Terminator,\n ParentOneOf<[\"::dataflow::ThreadOp\"]>,\n Pure\n]> {\n let summary = \"Terminator for a dataflow.thread body\";\n let description = [{\n Accepts an unordered all-of completion frontier of `none` values.\n Tensor-result aggregation from `scf.forall` is materialised into\n explicit destination-buffer writes before thread promotion, so the\n thread definition has no parallel combining region or thread data\n results.\n }];\n\n let arguments = (ins Variadic<NoneType>:$completionFrontier);\n\n let assemblyFormat = \"($completionFrontier^ `:` type($completionFrontier))? attr-dict\";\n\n let skipDefaultBuilders = 1;\n let builders = [\n OpBuilder<(ins CArg<\"::mlir::ValueRange\", \"{}\">:$completionFrontier), [{\n $_state.addOperands(completionFrontier);\n }]>\n ];\n}\n\ndef Dataflow_ThreadLaunchOp : Dataflow_Op<\"thread.launch\", [\n AttrSizedOperandSegments,\n DeclareOpInterfaceMethods<SymbolUserOpInterface>\n]> {\n let summary = \"Async launch of a dataflow.thread callable\";\n let description = [{\n References a `dataflow.thread` definition by symbol and supplies\n body operands and optional grid upper bounds. Always produces one\n `!dataflow.thread_token` completion handle for all dynamic launch\n instances.\n\n Grid lower bounds and steps are not modeled; body operands, upper bounds,\n and async dependencies are explicit.\n }];\n\n let arguments = (ins\n FlatSymbolRefAttr:$callee,\n Variadic<AnyType>:$bodyOperands,\n Variadic<Index>:$gridUpperBounds,\n Variadic<Dataflow_ThreadTokenType>:$asyncDependencies);\n\n let results = (outs Dataflow_ThreadTokenType:$asyncToken);\n\n let assemblyFormat = [{\n $callee\n `(` $bodyOperands `)`\n ( `grid` `(` $gridUpperBounds^ `)` )?\n ( `wait` `(` $asyncDependencies^ `)` )?\n attr-dict `:`\n functional-type($bodyOperands, results)\n }];\n\n let skipDefaultBuilders = 1;\n let builders = [\n OpBuilder<(ins\n \"::mlir::FlatSymbolRefAttr\":$callee,\n \"::mlir::ValueRange\":$bodyOperands,\n \"::mlir::ValueRange\":$gridUpperBounds,\n \"::mlir::ValueRange\":$asyncDependencies), [{\n $_state.addOperands(bodyOperands);\n $_state.addOperands(gridUpperBounds);\n $_state.addOperands(asyncDependencies);\n auto &properties = $_state.getOrAddProperties<Properties>();\n properties.operandSegmentSizes = {\n static_cast<int32_t>(bodyOperands.size()),\n static_cast<int32_t>(gridUpperBounds.size()),\n static_cast<int32_t>(asyncDependencies.size())};\n properties.callee = callee;\n $_state.addTypes(::dataflow::ThreadTokenType::get($_builder.getContext()));\n }]>\n ];\n\n let hasVerifier = 1;\n}","why":"Dataflow_ThreadYieldOp terminator and Dataflow_ThreadLaunchOp assembly format (callee, body operands, optional grid and wait clauses, thread_token result) used to spell the launch side of each sampled carrier."},{"file_sha256":"0616db64bbc547b2c92dd9801dbf1dac5136f19fc11ebdd1019ffd9660af9534","kind":"verifier","lines":"413,563-584,602-639","path":"lib/Dataflow/IR/DataflowFunctionLikeOps.cpp","roles":["input_well_formedness"],"text":"ParseResult ThreadOp::parse(OpAsmParser &parser, OperationState &result) {\nLogicalResult ThreadOp::verify() {\n if (!getSymVisibility() || *getSymVisibility() != \"private\")\n return emitOpError(\"requires explicit 'private' visibility\");\n if (getFunctionType().getNumResults() != 0)\n return emitOpError(\"must not declare function results\");\n\n if (getDomain().getKind() == ThreadDomainKind::DynamicWork) {\n uint64_t ordinal = *getDomain().getWorkItemArgOrdinal();\n ArrayRef<Type> inputs = getFunctionType().getInputs();\n if (ordinal >= inputs.size())\n return emitOpError(\"dynamic-work item argument ordinal \")\n << ordinal << \" is out of bounds for \" << inputs.size()\n << \" thread inputs\";\n for (auto [index, type] : llvm::enumerate(inputs))\n if (DataflowDialect::containsChannelOrThreadToken(type))\n return emitOpError(\"dynamic-work thread input #\")\n << index << \" must not contain a channel or thread token\";\n }\n if (!ownsThreadLaunchExtentAnalysis(*this))\n return success();\n return verifyThreadLaunchExtents(cast<ModuleOp>((*this)->getParentOp()));\n}\nLogicalResult ThreadLaunchOp::verifySymbolUses(SymbolTableCollection &symbols) {\n auto callee =\n symbols.lookupNearestSymbolFrom<ThreadOp>(*this, getCalleeAttr());\n if (!callee)\n return emitOpError(\"'\")\n << getCallee()\n << \"' does not reference a valid 'dataflow.thread' op\";\n\n // Body operand types must equal callee.function_type.inputs\n // position-by-position.\n ArrayRef<Type> calleeInputs = callee.getFunctionType().getInputs();\n if (getBodyOperands().size() != calleeInputs.size())\n return emitOpError(\"body operand count (\")\n << getBodyOperands().size()\n << \") does not match callee input count (\" << calleeInputs.size()\n << \")\";\n for (size_t i = 0, e = calleeInputs.size(); i < e; ++i) {\n Type expected = calleeInputs[i];\n Type actual = getBodyOperands()[i].getType();\n if (actual != expected)\n return emitOpError(\"body operand #\")\n << i << \" type \" << actual << \" does not match callee input type \"\n << expected;\n }\n\n size_t calleeRank = 0;\n if (!callee.isExternal()) {\n size_t entryArgumentCount = callee.getBody().front().getNumArguments();\n size_t requiredArgumentCount = calleeInputs.size() + 1;\n if (entryArgumentCount >= requiredArgumentCount)\n calleeRank = entryArgumentCount - requiredArgumentCount;\n }\n if (getGridUpperBounds().size() != calleeRank)\n return emitOpError(\"grid upper bound count (\")\n << getGridUpperBounds().size() << \") must match callee rank (\"\n << calleeRank << \")\";\n return success();\n}","why":"ThreadOp::parse derives function_type from the printed signature; ThreadOp::verify requires explicit private visibility and no function results; ThreadLaunchOp::verifySymbolUses requires body-operand types to equal callee inputs and grid count to equal callee coordinate rank. These bound which generated modules the subject accepts."},{"file_sha256":"0616db64bbc547b2c92dd9801dbf1dac5136f19fc11ebdd1019ffd9660af9534","kind":"verifier","lines":"313-347","path":"lib/Dataflow/IR/DataflowFunctionLikeOps.cpp","roles":["input_well_formedness"],"text":"static LogicalResult verifyThreadLaunchExtents(ModuleOp module) {\n ExtentConstantEvaluator evaluator;\n WalkResult result =\n module.walk<WalkOrder::PreOrder>([&](Operation *op) -> WalkResult {\n if (op != module.getOperation() && op->hasTrait<OpTrait::SymbolTable>())\n return WalkResult::skip();\n\n auto launch = dyn_cast<ThreadLaunchOp>(op);\n if (!launch)\n return WalkResult::advance();\n // A launch whose segmentation cannot be read safely is diagnosed by\n // its own verification; this analysis just leaves it alone.\n if (!hasReadableOperandSegments(launch))\n return WalkResult::advance();\n for (auto [index, extent] :\n llvm::enumerate(launch.getGridUpperBounds())) {\n auto constant =\n dyn_cast_or_null<IntegerAttr>(evaluator.evaluate(extent));\n if (constant && constant.getValue().isNegative()) {\n launch.emitOpError(\"grid upper bound #\")\n << index << \" must be nonnegative\";\n return WalkResult::interrupt();\n }\n }\n return WalkResult::advance();\n });\n return success(!result.wasInterrupted());\n}\n\nstatic bool ownsThreadLaunchExtentAnalysis(ThreadOp thread) {\n for (Operation *previous = thread->getPrevNode(); previous;\n previous = previous->getPrevNode())\n if (isa<ThreadOp>(previous))\n return false;\n return true;","why":"Module-scope thread launch extent analysis rejecting negative constant grid upper bounds; generated grid bounds are nonnegative index constants."},{"file_sha256":"c6f79ffa52853dc0bfac5214fbc7f94b0dacc45f8e5cdf216b2f0812c02bdff2","kind":"implementation","lines":"1-70","path":"lib/Frontend/Lowering/LowerForallToThreadPass.cpp","roles":["applicability","context"],"text":"// Reject implicit thread ownership for host scf.forall operations.\n//\n// dataflow.thread.launch models only zero-based grid extents. Thread\n// promotion therefore requires a recognized Loom mapping and a prior\n// structured-domain transformation that preserves lower bounds and steps.\n// Neither authority is currently materialized by this pass.\n\n#include \"Frontend/Lowering/Passes.h\"\n\n#include \"mlir/Dialect/Func/IR/FuncOps.h\"\n#include \"mlir/Dialect/SCF/IR/SCF.h\"\n#include \"mlir/IR/BuiltinOps.h\"\n#include \"mlir/Pass/Pass.h\"\n#include \"mlir/Pass/PassRegistry.h\"\n\nnamespace {\n\nstruct LowerForallToThreadPass\n : public ::mlir::PassWrapper<LowerForallToThreadPass,\n ::mlir::OperationPass<::mlir::ModuleOp>> {\n MLIR_DEFINE_EXPLICIT_INTERNAL_INLINE_TYPE_ID(LowerForallToThreadPass)\n\n ::llvm::StringRef getArgument() const final {\n return \"loom-lower-forall-to-thread\";\n }\n\n ::llvm::StringRef getDescription() const final {\n return \"Reject scf.forall thread promotion without a recognized Loom \"\n \"mapping and faithfully represented domain.\";\n }\n\n void getDependentDialects(::mlir::DialectRegistry ®istry) const final {\n registry.insert<::mlir::func::FuncDialect, ::mlir::scf::SCFDialect>();\n }\n\n void runOnOperation() final {\n bool rejected = false;\n getOperation().walk([&](::mlir::scf::ForallOp forall) {\n if (!forall->getParentOfType<::mlir::func::FuncOp>())\n return;\n forall.emitError(\n \"loom-lower-forall-to-thread: raw scf.forall has no recognized \"\n \"Loom thread mapping; preserve it until structured ownership and \"\n \"its complete domain are selected\");\n rejected = true;\n });\n if (rejected)\n signalPassFailure();\n }\n};\n\n} // namespace\n\nnamespace loom {\nnamespace lowering {\n\nstd::unique_ptr<::mlir::Pass> createLowerForallToThreadPass() {\n return std::make_unique<LowerForallToThreadPass>();\n}\n\nvoid registerLowerForallToThreadPass() {\n static bool once = []() {\n ::mlir::PassRegistration<LowerForallToThreadPass>();\n return true;\n }();\n (void)once;\n}\n\n} // namespace lowering\n} // namespace loom","why":"The selected stage only diagnoses scf.forall ops that have a func.func ancestor and never materializes a dataflow.thread; this fixes which sampled inputs the stage accepts (forall inside the thread carrier) and is the evidence for the reported stage-attribution mismatch."},{"file_sha256":"7f380008fb405f6cf8d60d16d1b5980dc1d2e694f9842bcfeb6538fbcfa01099","kind":"implementation","lines":"1-30","path":"lib/Frontend/Lowering/Pipeline.cpp","roles":["applicability","context"],"text":"// Pipeline glue and pass-registry hooks for the SCF-to-DFG lowering\n// passes. The standard pipeline runs:\n//\n// loom-lower-for-to-graph (module-level)\n//\n// `loom-lower-for-to-graph` owns the atomic publication transaction. It\n// consumes explicit loom.spatial_region candidates, runs graph finalization\n// on a scratch module, validates the native result, and publishes only the\n// completed module. Graph memref-copy expansion is part of that finalization,\n// so a copy the current profile cannot expand fails the transaction instead of\n// reaching the published program.\n//\n// Thread ownership must already be present in the Structured Program\n// Candidate. The independently registered forall pass only diagnoses raw\n// implicit promotion requests.\n\n#include \"Frontend/Lowering/Passes.h\"\n\n#include \"mlir/Pass/PassManager.h\"\n#include \"mlir/Pass/PassRegistry.h\"\n#include \"mlir/Transforms/Passes.h\"\n\nnamespace loom {\nnamespace lowering {\n\nvoid registerExpandGraphMemrefCopyPass();\nvoid registerLowerForallToThreadPass();\nvoid registerLowerForToGraphPass();\nvoid registerLowerGraphConstantsPass();\nvoid registerLowerGraphMemoryPass();","why":"Documents that thread ownership must already be present in the Structured Program Candidate and that the forall pass only diagnoses raw implicit promotion requests; supports keeping the stage flag and sampling pre-formed carriers."},{"file_sha256":"634d4f13677fbd71bdd190bbb48feb1619c6d88f387330c467c4e1fe84203407","kind":"test","lines":"1-26","path":"test/raise/scf-to-dfg-forall-to-thread.mlir","roles":["applicability"],"text":"// RUN: not loom-raise-opt --loom-lower-forall-to-thread \\\n// RUN: --mlir-disable-threading --mlir-print-ir-after-failure \\\n// RUN: --mlir-print-ir-module-scope %s 2>&1 | FileCheck %s\n\n// Thread promotion must not infer ownership for an unmapped forall. The\n// thread launch ABI cannot represent this offset, strided domain, so failure\n// must preserve the complete source domain rather than treating the upper\n// bound as a zero-based grid extent.\n\n// CHECK: error: loom-lower-forall-to-thread: raw scf.forall has no recognized Loom thread mapping\n// CHECK-LABEL: func.func @offset_strided(\n// CHECK: scf.forall\n// CHECK-SAME: (%{{.*}}) = (%{{.*}}) to (%{{.*}}) step (%{{.*}})\n// CHECK-NOT: dataflow.thread.launch\n// CHECK-NOT: dataflow.thread private\n\nfunc.func @offset_strided(%buffer: memref<?xi32>) {\n %lower = arith.constant 5 : index\n %upper = arith.constant 9 : index\n %step = arith.constant 2 : index\n %value = arith.constant 7 : i32\n scf.forall (%index) = (%lower) to (%upper) step (%step) {\n memref.store %value, %buffer[%index] : memref<?xi32>\n }\n return\n}","why":"Non-normative evidence that a raw func-level scf.forall makes the selected stage fail with no output, so generated inputs place the effect-form forall inside the thread definition instead."},{"file_sha256":"7b2bea863a561d79b9cc6deb6f69e2c6e535d46e50f23d7fddb0e13d1a952c7d","kind":"example","lines":"1-57","path":"test/dataflow/unit/thread/valid.mlir","roles":["input_construction"],"text":"// RUN: loom %s | loom | FileCheck %s\n\n// Empty thread body carrying just the thread_ctrl slot per spec\n// section 5.4.1's `(args_*, thread_ctrl, iv_*)` layout.\n// CHECK-LABEL: dataflow.thread private @t_empty domain(#dataflow.thread_domain<dense>)() ctrl (%{{.*}}: none)\ndataflow.thread private @t_empty domain(#dataflow.thread_domain<dense>)() ctrl (%c: none) {\n dataflow.thread.yield\n}\n\n// Thread definition with two body operands, the thread_ctrl slot,\n// and one trailing grid iv slot.\n// CHECK-LABEL: dataflow.thread private @t_two_args domain(#dataflow.thread_domain<dense>)(%{{.*}}: i32, %{{.*}}: f32) ctrl (%{{.*}}: none) iv (%{{.*}}: index)\ndataflow.thread private @t_two_args domain(#dataflow.thread_domain<dense>)(%a: i32, %b: f32) ctrl (%c: none) iv (%i: index) {\n dataflow.thread.yield\n}\n\n// Every launch produces one completion token, including a launch carrying\n// mapped operands and a grid upper bound.\n// CHECK-LABEL: func.func @launch_demo\nfunc.func @launch_demo(%a: i32, %b: f32, %n: index) {\n // CHECK: %{{.*}} = dataflow.thread.launch @t_two_args(%{{.*}}, %{{.*}}) grid(%{{.*}}) : (i32, f32) -> !dataflow.thread_token\n %completion = dataflow.thread.launch @t_two_args(%a, %b) grid(%n) : (i32, f32) -> !dataflow.thread_token\n return\n}\n\n// Launch dependencies and waits both express unordered all-of completion.\n// CHECK-LABEL: func.func @wait_for_launches\nfunc.func @wait_for_launches() {\n // CHECK: %{{.*}} = dataflow.thread.launch @t_empty() : () -> !dataflow.thread_token\n %first = dataflow.thread.launch @t_empty() : () -> !dataflow.thread_token\n // CHECK: %{{.*}} = dataflow.thread.launch @t_empty() wait(%{{.*}}) : () -> !dataflow.thread_token\n %second = dataflow.thread.launch @t_empty() wait(%first) : () -> !dataflow.thread_token\n // CHECK: dataflow.thread.wait %{{.*}}, %{{.*}} : !dataflow.thread_token, !dataflow.thread_token\n dataflow.thread.wait %first, %second : !dataflow.thread_token, !dataflow.thread_token\n return\n}\n\n// Completion frontiers carry zero or more unordered none-typed values.\n// CHECK-LABEL: dataflow.thread private @t_frontier domain(#dataflow.thread_domain<dense>)() ctrl (%{{.*}}: none)\ndataflow.thread private @t_frontier domain(#dataflow.thread_domain<dense>)() ctrl (%ctrl: none) {\n // CHECK: dataflow.thread.yield %{{.*}} : none\n dataflow.thread.yield %ctrl : none\n}\n\n// A dynamic-work definition designates one ordinary input as its root payload\n// and has no coordinate suffix or launch extents.\n// CHECK-LABEL: dataflow.thread private @t_dynamic domain(#dataflow.thread_domain<dynamic_work, work_item_arg = 0>)\ndataflow.thread private @t_dynamic domain(#dataflow.thread_domain<dynamic_work, work_item_arg = 0>)(%work: i32) ctrl (%ctrl: none) {\n dataflow.thread.yield\n}\n\n// CHECK-LABEL: func.func @launch_dynamic\nfunc.func @launch_dynamic(%root: i32) {\n // CHECK: dataflow.thread.launch @t_dynamic(%{{.*}}) : (i32) -> !dataflow.thread_token\n %completion = dataflow.thread.launch @t_dynamic(%root) : (i32) -> !dataflow.thread_token\n return\n}","why":"Accepted spellings of dataflow.thread definitions (dense and dynamic domains, ctrl/iv clauses, thread.yield) and of dataflow.thread.launch with grid and wait clauses; used only for concrete syntax."},{"file_sha256":"3e2863717e0d5713893e5cabfb8e646c854432da0abd1478ee022ec7a610e62f","kind":"example","lines":"80-93","path":"test/raise/scf-to-dfg-atomic-publication.mlir","roles":["input_construction"],"text":"dataflow.thread private @parallel_channel_sender domain(#dataflow.thread_domain<dense>)(\n %channel: !dataflow.channel<i32>, %message: i32) ctrl (%start: none) {\n \"loom.spatial_region\"(%message, %channel)\n <{operandSegmentSizes = array<i32: 1, 0, 0, 1>,\n resultSegmentSizes = array<i32: 0, 0>}> ({\n ^bb0(%payload: i32, %output: !dataflow.channel<i32>):\n scf.forall (%lane) in (2) {\n dataflow.channel.send %output, %payload : !dataflow.channel<i32>\n }\n \"loom.spatial_yield\"()\n <{operandSegmentSizes = array<i32: 0, 0>}> : () -> ()\n }) {graph_name = \"parallel_channel_graph\", source_maps = []} :\n (i32, !dataflow.channel<i32>) -> ()\n dataflow.thread.yield","why":"Accepted spelling of an effect-form `scf.forall (%lane) in (2)` nested inside a dataflow.thread carrier, matching the sampled input shape."}],"primary_bundle_sha256":"bf761224d3ed8af6b66873c51c5c09d0291c0db4ea2bfc275ad80b806290ed1e","project":"PolyArch/loom","revision":"48615bc5925ef4b9db8b4550b5d4322933cf4b7b","schema":"spectriad.authoring-context/v1","selection_sha256":"b79feafca278e758c042da43242e7412169f3c7faee3662d7b43252e46b7c844"}
sessions/reverse-generator/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 47031,
"duration_ms": 47090,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1479,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 4655,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.135635,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 3563,
"provider": "firstParty",
"thinkingTokens": 805,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "## Preconditions\n\n1. Every emitted program is a single MLIR module whose top level consists only of `dataflow.thread` definitions and `func.func` host functions, with no other module-scope operations, attributes, or nesting.\n2. Every `dataflow.thread` definition is declared `private` and is named `@thread_N` where `N` is the zero-based index of the definition in module order.\n3. Every `dataflow.thread` definition carries the domain attribute `domain(#dataflow.thread_domain<dense>)` and no other domain kind.\n4. The entry block of every `dataflow.thread` begins with the argument `%buf: memref<8xi32>`, which is always present and is the first declared argument.\n5. Any additional entry-block payload arguments follow `%buf` in a comma-separated list, are named `%arg0`, `%arg1`, \u2026 in consecutive zero-based order, and each is annotated with exactly one of the element types `i32`, `f32`, or `index`.\n6. Every `dataflow.thread` definition declares a control argument in a separate clause written `ctrl (%thread_ctrl: none)`, of type `none`, placed after the payload argument list.\n7. A definition with a nonzero launch-domain rank declares a coordinate clause ` iv (...)` after the `ctrl` clause containing exactly one `index`-typed argument per domain dimension, named `%coord_0`, `%coord_1`, \u2026 in consecutive zero-based order and separated by `, `.\n8. A definition whose launch-domain rank is zero emits no `iv` clause at all, and its paired launch emits no `grid` clause; the presence of the coordinate clause and the presence of the grid clause are strictly linked.\n9. The body of every `dataflow.thread` begins with the SSA definition `%value = arith.constant 7 : i32`, so any operation consuming `%value` is dominated by its definition.\n10. If an `scf.forall` appears in a thread body, it is written in effect form: it has no `shared_outs` clause, produces no results, carries no mapping attribute, and has an implicit empty `in_parallel` terminator (no explicit terminator region is written).\n11. Any emitted `scf.forall` has exactly one induction variable `%lane` and a single-dimension upper bound given as a compile-time integer literal, with an implicit zero lower bound and unit step.\n12. The sole operation inside any `scf.forall` body is `memref.store %value, %buf[%lane] : memref<8xi32>`, storing the thread-body constant into the entry-block memref at the induction variable, and the store index range is bounded by the memref's static extent of 8.\n13. Every `dataflow.thread` body is terminated by a `dataflow.thread.yield`, either with no operands or with the single operand `%thread_ctrl : none` taken from the declared control argument.\n14. Each `dataflow.thread` definition is immediately followed at module scope by exactly one host function `func.func @host_N()` whose numeric suffix matches that definition, taking no arguments and returning no results.\n15. Each host function allocates its buffer with `%buf = memref.alloc() : memref<8xi32>`, whose type matches the first entry-block argument type of the callee.\n16. Each host function defines one SSA constant `%h0`, `%h1`, \u2026 per extra payload argument of its callee, in consecutive zero-based order, and the constant's type and literal form match the declared type of the payload argument at the same position (`arith.constant 3 : i32`, `arith.constant 1.000000e+00 : f32`, or `arith.constant 2 : index`).\n17. Each host function defines one `index` constant `%g0`, `%g1`, \u2026 per launch-domain dimension, in consecutive zero-based order, before the launch.\n18. Every host function contains exactly one `dataflow.thread.launch @thread_N(...)` whose callee symbol matches the preceding definition and whose operand list is `%buf` followed by `%h0 \u2026 %hK` in the same order and arity as the callee's declared arguments.\n19. The launch's explicit operand type list is `(memref<8xi32>` followed by the payload types in declaration order `) -> !dataflow.thread_token`, so the signature written at the launch agrees element-for-element with the callee's entry block, and the launch yields exactly one token result bound to `%token`.\n20. When the callee declares coordinates, the launch carries a `grid(...)` clause listing exactly the `%g0 \u2026 %gR-1` constants, one per coordinate argument, in order and separated by `, `, so grid arity equals coordinate arity.\n21. All constant definitions in a host function precede the launch that uses them, and the launch precedes the terminating `return`.\n22. Every host function ends with `return` and a closing brace, and contains no operation consuming `%token`.\n23. No emitted program uses the thread's coordinate arguments or payload arguments inside the thread body; the only value flowing into the body's operations is `%value` and `%buf`.\n\n## Sampling conventions\n\n1. The module contains between 1 and 3 `dataflow.thread` definitions inclusive, each paired with its host function, and definitions/host pairs are emitted interleaved (definition then its host function) rather than grouped.\n2. The number of extra payload arguments per thread is chosen independently per thread from 0 to 2 inclusive, so total entry-block arity ranges from 1 to 3.\n3. The launch-domain rank per thread is chosen independently from 0 to 2 inclusive, so a definition has zero, one, or two coordinate arguments; ranks of 3 or more are never emitted.\n4. Each extra payload type is drawn independently from exactly the three-element set `i32`, `f32`, `index`; no vector, memref, tensor, or other types appear in payload positions.\n5. The buffer type is fixed to `memref<8xi32>` in every definition and every host allocation; no other shape or element type is ever emitted.\n6. The thread-body constant is fixed to `arith.constant 7 : i32`, and the host-side constant literals are fixed per type (3 for `i32`, 1.000000e+00 for `f32`, 2 for `index`).\n7. The grid constants are always `arith.constant 4 : index`, identical for every dimension, so no non-uniform or non-constant grid sizes are exercised.\n8. The `scf.forall` upper bound is drawn from exactly `2`, `4`, or `8`; other extents, including extents exceeding the memref's static size, are never emitted.\n9. The `scf.forall` is optional: a thread body either contains exactly one such loop or contains none, and never contains two or more, nor any nested or sibling loops.\n10. The yield form is chosen between the operandless `dataflow.thread.yield` and the control-passing `dataflow.thread.yield %thread_ctrl : none`; no other operand sets are emitted.\n11. Names follow fixed schemes with zero-based consecutive numbering and no gaps: `@thread_N`/`@host_N` for symbols, `%argI` for payload arguments, `%coord_K` for coordinates, `%hB` for host payload constants, `%gG` for grid constants, plus the fixed names `%buf`, `%thread_ctrl`, `%value`, `%lane`, and `%token`.\n12. Indentation is fixed: module-scope operations at column zero, thread-body and host-body operations indented two spaces, and the `scf.forall` body indented four spaces.\n13. Separators are fixed: `, ` between coordinate declarations, grid operands, payload declarations, launch operands, and launch operand types, with no trailing separator before a closing parenthesis.\n14. The `dataflow.thread.launch` result is always bound to `%token` even though it is never consumed, rather than using a result-discarding form.\n15. Host functions are always named after and matched one-to-one with their callee, never sharing a host function across threads and never launching a thread more than once.\n16. The store inside the loop always writes the same `%value` to the same `%buf`, so no aliasing, multiple-buffer, or load-based access patterns are exercised.\n17. The skeleton is kept flat and finite: no control flow other than the optional single `scf.forall`, no calls other than the launch, no region-bearing ops besides `dataflow.thread`, `func.func`, and `scf.forall`.",
"result_index": 0,
"session_id": "ef25b0ed-8e37-45b4-9564-09367f5d1322",
"stop_reason": "end_turn",
"subagent_stats": {
"by_type": {},
"completed": 0,
"failed": 0,
"killed": {
"parent": 0,
"system": 0,
"user": 0
},
"max_depth": 0,
"refused": {
"budget": 0,
"concurrency_limit": 0,
"depth_limit": 0
},
"requested": {
"background": 0,
"foreground": 0,
"unset": 0
},
"spawned": 0,
"spawned_by_subagents": 0,
"started_in_background": 0
},
"subtype": "success",
"terminal_reason": "completed",
"time_to_request_ms": 59,
"total_cost_usd": 0.135635,
"ttft_ms": 13252,
"ttft_stream_ms": 1305,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 4655,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 4655,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 3563,
"output_tokens_details": {
"thinking_tokens": 805
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "dac6434f-c5b4-47ba-a67b-8ec1b88d647e"
}
]
sessions/reverse-postcondition/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 15122,
"duration_ms": 15149,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1687,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 5410,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.07826,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 966,
"provider": "firstParty",
"thinkingTokens": 385,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "This postcondition quantifies universally over the entire output program: it walks every operation at any nesting depth and keeps those whose name is exactly `dataflow.thread` and that have at least one region whose first block list is non-empty, so threads with no region or with an empty first region are simply not selected. For each selected thread it reads the thread's own `function_type` attribute, projects its declared input type list, and takes that many leading entry-block arguments from `regions[0].blocks[0]`, collecting their types; the two sequences are then paired positionally with `zip_exact` and every pair must compare equal as types. Because the left sequence is truncated by `take(n)`, a thread whose entry block carries *more* arguments than the signature declares is accepted as long as the leading prefix matches, while a thread with *fewer* arguments than declared inputs yields a short left sequence and `zip_exact` makes the assertion fail with both lengths as the witness. Values come only from the output program \u2014 the argument types come from the entry block of the thread's first region and the expected types come from the thread operation's own `function_type` attribute \u2014 and the `input` program is never consulted, so nothing here relates output to input. Equality is type equality, position by position, with no allowance for reordering, conversion, or partial matching. A selected thread that lacks a `function_type` attribute, or whose `function_type` is not a type-valued attribute of function kind, produces an evaluation error rather than a pass or a clean failure. The condition is vacuously satisfied when the output contains no thread operations meeting the selection filter, and likewise for any selected thread whose declared input list is empty, since the zipped sequence is then empty and the inner universal quantification holds trivially. Non-vacuous force arises only when at least one bodied `dataflow.thread` declares one or more input types.",
"result_index": 0,
"session_id": "bf224824-bf97-4bac-8d54-48b990a32d18",
"stop_reason": "end_turn",
"subagent_stats": {
"by_type": {},
"completed": 0,
"failed": 0,
"killed": {
"parent": 0,
"system": 0,
"user": 0
},
"max_depth": 0,
"refused": {
"budget": 0,
"concurrency_limit": 0,
"depth_limit": 0
},
"requested": {
"background": 0,
"foreground": 0,
"unset": 0
},
"spawned": 0,
"spawned_by_subagents": 0,
"started_in_background": 0
},
"subtype": "success",
"terminal_reason": "completed",
"time_to_request_ms": 27,
"total_cost_usd": 0.07826,
"ttft_ms": 7041,
"ttft_stream_ms": 1269,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 5410,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 5410,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 966,
"output_tokens_details": {
"thinking_tokens": 385
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "344ed1d7-5f2b-4091-9c87-e8523cc1e296"
}
]
This paired revision was activated by an explicit partial-scope team review bound to both executable artifact hashes.
Approved for execution and public reporting; translation accuracy and completeness remain separately unvalidated.