MS1V3 mlir-stage-12-v1 passing 5000/5000
Estimated confidence: 63.2%. Conservative lower bound: 1.7% (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/DataflowDialect.cppMS1V | 22/32lines68.8% 4/10branches40.0% | 25/32lines78.1%+3 7/10branches70.0%+3 | |
3 newly covered lines · 3 newly covered branches24 | |||
…/lib/Dataflow/IR/DataflowFunctionLikeOps.cppMS1V | 693/1097lines63.2% 264/592branches44.6% | 747/1097lines68.1%+54 298/592branches50.3%+34 | |
54 newly covered lines · 34 newly covered branches102 | |||
…/lib/Frontend/Lowering/LowerForallToThreadPass.cppMS1V | 30/34lines88.2% 2/4branches50.0% | 30/34lines88.2%+0 3/4branches75.0%+1 | |
1 newly covered branch45 | |||
…/lib/Dataflow/IR/DataflowChannelOps.cppMS1V | 59/88lines67.0% 13/38branches34.2% | 59/88lines67.0%+0 13/38branches34.2%+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 |
Review PR: Regression test from seed 0
function_type is a FunctionType whose inputs are the kernel's
user-data operand types (T0, ..., TN) and whose results are
empty. The thread definition has no SSA data results; the
per-launch completion token is launch-side, not part of the
callable signature. Asynchronous execution is expressed by launch
dependencies and the mandatory launch completion token, not by the
function type.dataflow.thread private @t_0 domain(#dataflow.thread_domain<dynamic_work, work_item_arg = 0>)(%arg_0: index, %arg_1: memref<?xf32>, %arg_2: i32) ctrl (%thread_ctrl: none) { dataflow.thread.yield } dataflow.thread private @t_1 domain(#dataflow.thread_domain<dense>)() ctrl (%thread_ctrl: none) iv (%coord_0: index, %coord_1: index) { dataflow.thread.yield %thread_ctrl : none } func.func @host(%m_ref: memref<?xf32>) { %c_i32 = arith.constant 1 : i32 %c_idx = arith.constant 4 : index %token_0 = dataflow.thread.launch @t_0(%c_idx, %m_ref, %c_i32) : (index, memref<?xf32>, i32) -> !dataflow.thread_token dataflow.thread.wait %token_0 : !dataflow.thread_token %token_1 = dataflow.thread.launch @t_1() grid(%c_idx, %c_idx) : () -> !dataflow.thread_token return }
dataflow.thread private @t_0 domain(#dataflow.thread_domain<dynamic_work, work_item_arg = 0>)(%arg_0: index, %arg_1: memref<?xf32>, %arg_2: i32) ctrl (%thread_ctrl: none) { dataflow.thread.yield } dataflow.thread private @t_1 domain(#dataflow.thread_domain<dense>)() ctrl (%thread_ctrl: none) iv (%coord_0: index, %coord_1: index) { dataflow.thread.yield %thread_ctrl : none } func.func @host(%m_ref: memref<?xf32>) { %c_i32 = arith.constant 1 : i32 %c_f32 = arith.constant 1.000000e+00 : f32 %c_i64 = arith.constant 1 : i64 %c_idx = arith.constant 4 : index %token_0 = dataflow.thread.launch @t_0(%c_idx, %m_ref, %c_i32) : (index, memref<?xf32>, i32) -> !dataflow.thread_token dataflow.thread.wait %token_0 : !dataflow.thread_token %token_1 = dataflow.thread.launch @t_1() grid(%c_idx, %c_idx) : () -> !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// Input domain: the definition-and-launch carrier shape that Part 3 accepts // for an effect-form forall selected as an AccCore thread domain // (docs/spec-compiler-part-3-dfg.md lines 2057-2061). Each module carries one // or more module-scope `dataflow.thread` definitions (private visibility, a // closed dense or dynamic-work domain, the `(args_*, thread_ctrl, coord_*)` // entry block) and one host `func.func` holding the matching // `dataflow.thread.launch` ops. No `scf.forall` is emitted: a graph-owned // forall retained by Part 2 is mapping-free, effect-form and fixed-domain, and // this boundary carries no shared_outs, results or combining action. start: {new TYPE_NAMES = ['i32', 'f32', 'i64', 'index', 'memref<?xf32>', 'i32', 'f32', 'i64', 'index', 'memref<?xf32>']; new VALUE_NAMES = ['%c_i32', '%c_f32', '%c_i64', '%c_idx', '%m_ref', '%c_i32', '%c_f32', '%c_i64', '%c_idx', '%m_ref']; new NUM = random.randint(1, 3); new ARITIES = []; new OFFSETS = []; new RANKS = []; new IDX = 0} thread_defs {IDX = 0} 'func.func @host(%m_ref: memref<?xf32>) {\n' ' %c_i32 = arith.constant 1 : i32\n' ' %c_f32 = arith.constant 1.000000e+00 : f32\n' ' %c_i64 = arith.constant 1 : i64\n' ' %c_idx = arith.constant 4 : index\n' launches ' return\n' '}\n'; thread_defs: (IDX < NUM) thread_def {IDX += 1} thread_defs | (IDX == NUM) ''; // Arity, argument types and coordinate rank are sampled per definition and // recorded so the launch side can reproduce the same signature. thread_def: {new ARITY = random.randint(0, 3); new OFFSET = random.randint(0, 4); new RANK = random.randint(0, 2); new DYN_SEL = random.choice([0, 1]); new ORDINAL = 0} thread_shape; thread_shape: (ARITY > 0 and DYN_SEL == 1) {RANK = 0; ORDINAL = random.randint(0, ARITY - 1)} dynamic_def | (ARITY == 0 or DYN_SEL == 0) dense_def; // A dynamic definition has coordinate rank zero and its ordinal selects // exactly one function_type input. dynamic_def: {ARITIES.append(ARITY); OFFSETS.append(OFFSET); RANKS.append(0)} 'dataflow.thread private @' def_symbol ' domain(#dataflow.thread_domain<dynamic_work, work_item_arg = ' ordinal_text '>)' def_args ' ctrl (%thread_ctrl: none) {\n' terminator '}\n\n'; // A dense definition has no work-item ordinal and carries one `index` // coordinate argument per launch-domain dimension. dense_def: {ARITIES.append(ARITY); OFFSETS.append(OFFSET); RANKS.append(RANK)} 'dataflow.thread private @' def_symbol ' domain(#dataflow.thread_domain<dense>)' def_args ' ctrl (%thread_ctrl: none)' coord_clause ' {\n' terminator '}\n\n'; def_symbol: 't_' index_text; index_text: [str(IDX)]; ordinal_text: [str(ORDINAL)]; terminator: ' dataflow.thread.yield\n' | ' dataflow.thread.yield %thread_ctrl : none\n'; def_args: {new J = 0} '(' def_arg_list ')'; def_arg_list: (J < ARITY) arg_sep def_arg {J += 1} def_arg_list | (J == ARITY) ''; arg_sep: (J == 0) '' | (J > 0) ', '; def_arg: '%arg_' arg_index ': ' arg_type; arg_index: [str(J)]; arg_type: [TYPE_NAMES[OFFSET + J]]; coord_clause: (RANK == 0) '' | (RANK > 0) {new K = 0} ' iv (' coord_list ')'; coord_list: (K < RANK) coord_sep coord_arg {K += 1} coord_list | (K == RANK) ''; coord_sep: (K == 0) '' | (K > 0) ', '; coord_arg: '%coord_' coord_index ': index'; coord_index: [str(K)]; // One launch per definition; body operands reproduce function_type.inputs and // the grid upper bounds match the definition's coordinate rank. launches: (IDX < NUM) launch {IDX += 1} launches | (IDX == NUM) ''; launch: {new ARITY = ARITIES[IDX]; new OFFSET = OFFSETS[IDX]; new RANK = RANKS[IDX]} ' %token_' index_text ' = dataflow.thread.launch @t_' index_text launch_operands grid_clause ' : ' launch_signature ' -> !dataflow.thread_token\n' wait_clause; wait_clause: '' | ' dataflow.thread.wait %token_' index_text ' : !dataflow.thread_token\n'; launch_operands: {new J = 0} '(' launch_operand_list ')'; launch_operand_list: (J < ARITY) arg_sep launch_operand {J += 1} launch_operand_list | (J == ARITY) ''; launch_operand: operand_name; operand_name: [VALUE_NAMES[OFFSET + J]]; grid_clause: (RANK == 0) '' | (RANK > 0) {new K = 0} ' grid(' grid_list ')'; grid_list: (K < RANK) coord_sep grid_bound {K += 1} grid_list | (K == RANK) ''; grid_bound: '%c_idx'; launch_signature: {new J = 0} '(' launch_type_list ')'; launch_type_list: (J < ARITY) arg_sep launch_type {J += 1} launch_type_list | (J == ARITY) ''; launch_type: arg_type;
function_typeis aFunctionTypewhose inputs are the kernel's user-data operand types(T0, ..., TN)and whose results are empty. The thread definition has no SSA data results; the per-launch completion token is launch-side, not part of the callable signature.
candidate.spctpostcondition thread_function_type_signature { language v0; vocabulary mlir = mlir.generic@1; metadata { project = "PolyArch/loom"; revision = "48615bc5925ef4b9db8b4550b5d4322933cf4b7b"; source = "docs/spec-compiler-part-3-dfg.md:L991-L997"; } constraints { let threads = seq { op | op in output.operations where op.name == "dataflow.thread" }; forall t in threads { assert function_type_has_no_results: cardinality(t.attributes["function_type"].type.results) == 0; assert no_ssa_data_results: cardinality(t.results) == 0; assert completion_token_not_in_signature: forall ty in t.attributes["function_type"].type.inputs where ty.canonical_text != "!dataflow.thread_token"; } let launches = seq { op | op in output.operations where op.name == "dataflow.thread.launch" }; forall l in launches { forall t in mlir::resolve_symbol_reference(output, l, "callee") where t.name == "dataflow.thread" { assert function_type_inputs_are_user_data_operand_types: forall p in zip_exact(t.attributes["function_type"].type.inputs, seq { v.type | v in mlir::operand_segment(l, 0) }) where p.left == p.right; } } } }
dataflow.thread private @t_0 domain(#dataflow.thread_domain<dynamic_work, work_item_arg = 0>)(%arg_0: index, %arg_1: memref<?xf32>, %arg_2: i32) ctrl (%thread_ctrl: none) { dataflow.thread.yield } dataflow.thread private @t_1 domain(#dataflow.thread_domain<dense>)() ctrl (%thread_ctrl: none) iv (%coord_0: index, %coord_1: index) { dataflow.thread.yield %thread_ctrl : none } func.func @host(%m_ref: memref<?xf32>) { %c_i32 = arith.constant 1 : i32 %c_idx = arith.constant 4 : index %token_0 = dataflow.thread.launch @t_0(%c_idx, %m_ref, %c_i32) : (index, memref<?xf32>, i32) -> !dataflow.thread_token dataflow.thread.wait %token_0 : !dataflow.thread_token %token_1 = dataflow.thread.launch @t_1() grid(%c_idx, %c_idx) : () -> !dataflow.thread_token return }
20260911-083547started2026-09-11T08:35:48Zsubjectloom-raise-optsubject revision48615bc5925erun results
output condition verdicts
raw trace evidence
dataflow.thread private @t_0 domain(#dataflow.thread_domain<dynamic_work, work_item_arg = 0>)(%arg_0: index, %arg_1: memref<?xf32>, %arg_2: i32) ctrl (%thread_ctrl: none) { dataflow.thread.yield } dataflow.thread private @t_1 domain(#dataflow.thread_domain<dense>)() ctrl (%thread_ctrl: none) iv (%coord_0: index, %coord_1: index) { dataflow.thread.yield %thread_ctrl : none } func.func @host(%m_ref: memref<?xf32>) { %c_i32 = arith.constant 1 : i32 %c_f32 = arith.constant 1.000000e+00 : f32 %c_i64 = arith.constant 1 : i64 %c_idx = arith.constant 4 : index %token_0 = dataflow.thread.launch @t_0(%c_idx, %m_ref, %c_i32) : (index, memref<?xf32>, i32) -> !dataflow.thread_token dataflow.thread.wait %token_0 : !dataflow.thread_token %token_1 = dataflow.thread.launch @t_1() grid(%c_idx, %c_idx) : () -> !dataflow.thread_token return }
"builtin.module"() ({ "dataflow.thread"() <{domain = #dataflow.thread_domain<dynamic_work, work_item_arg = 0>, function_type = (index, memref<?xf32>, i32) -> (), sym_name = "t_0", sym_visibility = "private"}> ({ ^bb0(%arg4: index, %arg5: memref<?xf32>, %arg6: i32, %arg7: none): "dataflow.thread.yield"() : () -> () }) : () -> () "dataflow.thread"() <{domain = #dataflow.thread_domain<dense>, function_type = () -> (), sym_name = "t_1", sym_visibility = "private"}> ({ ^bb0(%arg1: none, %arg2: index, %arg3: index): "dataflow.thread.yield"(%arg1) : (none) -> () }) : () -> () "func.func"() <{function_type = (memref<?xf32>) -> (), sym_name = "host"}> ({ ^bb0(%arg0: memref<?xf32>): %0 = "arith.constant"() <{value = 1 : i32}> : () -> i32 %1 = "arith.constant"() <{value = 1.000000e+00 : f32}> : () -> f32 %2 = "arith.constant"() <{value = 1 : i64}> : () -> i64 %3 = "arith.constant"() <{value = 4 : index}> : () -> index %4 = "dataflow.thread.launch"(%3, %arg0, %0) <{callee = @t_0, operandSegmentSizes = array<i32: 3, 0, 0>}> : (index, memref<?xf32>, i32) -> !dataflow.thread_token "dataflow.thread.wait"(%4) : (!dataflow.thread_token) -> () %5 = "dataflow.thread.launch"(%3, %3) <{callee = @t_1, operandSegmentSizes = array<i32: 0, 2, 0>}> : (index, index) -> !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"],"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: module-scope private callable, required domain attribute, the (args_*, thread_ctrl, coord_*) entry-block layout and IsolatedFromAbove body. Fixes the terminology and the shape every generated definition must have."},{"file_sha256":"d76b4cb1e888697d5f011a939e68cbc6230647c4d457c12d22689740aa43a44d","kind":"documentation_input","lines":"2052-2061","path":"docs/spec-compiler-part-3-dfg.md","roles":["input_construction","input_well_formedness"],"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 when Part 2 selects an effect-form forall as an AccCore thread domain, the input accepted at this boundary is already the definition-and-launch carrier shape; this is why the grammar emits dataflow.thread definitions plus dataflow.thread.launch rather than a raw scf.forall."},{"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":"Constrains the accepted boundary form: mapping-free, effect-form, compile-time fixed domain, no shared_outs, no op results, no combining action; a dynamic domain or mapping attribute fails before publication. The grammar therefore emits no shared_outs/result/mapping constructs."},{"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 the thread definition remains InstructionCore code unless explicitly wrapped in loom.spatial_region; justifies generating plain bodies with only the thread.yield terminator."},{"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":"Part 2 promotion into a dense logical thread domain and the fixed-domain requirement for a retained graph-owned parallel form; supports sampling dense coordinate ranks and rejecting unprojectable/offset-strided domains from the input domain."},{"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":"ODS for dataflow.thread: sym_name/function_type/domain/sym_visibility/arg_attrs operands, SizedRegion body with implicit ThreadYieldOp terminator, the documented custom assembly format with domain(...), ctrl(...) and iv(...) clauses, and verifyBody's entry-block layout rules. Fixes the exact input spelling emitted by the grammar."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"741-765","path":"include/Dataflow/IR/DataflowOps.td","roles":["input_construction"],"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}","why":"ODS for dataflow.thread.yield: the optional variadic none-typed completion frontier and its assembly format, used for both terminator spellings the grammar samples."},{"file_sha256":"f4e60b2e62b496c3714437bd100ab5236540abebd3685dfbd25eeddb37cb7160","kind":"language_definition","lines":"767-820","path":"include/Dataflow/IR/DataflowOps.td","roles":["input_construction","input_well_formedness"],"text":"def 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":"ODS for dataflow.thread.launch: callee symbol, bodyOperands/gridUpperBounds/asyncDependencies operand segments (AttrSizedOperandSegments, the segmentation the postcondition reads with mlir::operand_segment) and the assembly format with grid(...)/wait(...) clauses."},{"file_sha256":"0616db64bbc547b2c92dd9801dbf1dac5136f19fc11ebdd1019ffd9660af9534","kind":"verifier","lines":"413-509","path":"lib/Dataflow/IR/DataflowFunctionLikeOps.cpp","roles":["input_construction","input_well_formedness"],"text":"ParseResult ThreadOp::parse(OpAsmParser &parser, OperationState &result) {\n ::mlir::Builder &builder = parser.getBuilder();\n ::mlir::StringAttr visibilityAttr;\n StringRef visibility;\n if (succeeded(parser.parseOptionalKeyword(&visibility, {\"private\"}))) {\n visibilityAttr = builder.getStringAttr(visibility);\n }\n\n StringAttr nameAttr;\n if (parser.parseSymbolName(nameAttr, SymbolTable::getSymbolAttrName(),\n result.attributes))\n return failure();\n\n if (parser.parseKeyword(\"domain\") || parser.parseLParen())\n return failure();\n ThreadDomainAttr domain;\n if (parser.parseAttribute(domain) || parser.parseRParen())\n return failure();\n result.addAttribute(getDomainAttrName(result.name), domain);\n\n // Function arguments + (empty) results.\n SmallVector<OpAsmParser::Argument> arguments;\n SmallVector<Type> resultTypes;\n SmallVector<DictionaryAttr> resultAttrs;\n bool isVariadic = false;\n if (function_interface_impl::parseFunctionSignatureWithArguments(\n parser, /*allowVariadic=*/false, arguments, isVariadic, resultTypes,\n resultAttrs))\n return failure();\n if (!resultTypes.empty())\n return parser.emitError(parser.getNameLoc(),\n \"dataflow.thread does not have function results\");\n\n SmallVector<Type, 4> argTypes;\n for (auto &arg : arguments)\n argTypes.push_back(arg.type);\n auto funcType = builder.getFunctionType(argTypes, /*results=*/{});\n result.addAttribute(getFunctionTypeAttrName(result.name),\n TypeAttr::get(funcType));\n call_interface_impl::addArgAndResultAttrs(\n builder, result, arguments, resultAttrs, getArgAttrsAttrName(result.name),\n getResAttrsAttrName(result.name));\n\n // Helper: parse a parenthesized comma-separated list of typed\n // arguments into the given vector. Allows an empty list `()`.\n auto parseTypedArgList =\n [&](SmallVectorImpl<OpAsmParser::Argument> &out) -> ParseResult {\n if (parser.parseLParen())\n return failure();\n if (succeeded(parser.parseOptionalRParen()))\n return success();\n auto parseOne = [&]() -> ParseResult {\n OpAsmParser::Argument arg;\n if (parser.parseArgument(arg, /*allowType=*/true))\n return failure();\n out.push_back(arg);\n return success();\n };\n if (parseOne())\n return failure();\n while (succeeded(parser.parseOptionalComma()))\n if (parseOne())\n return failure();\n return parser.parseRParen();\n };\n\n // Optional `ctrl ( <name> : <type> )` for the thread_ctrl slot.\n SmallVector<OpAsmParser::Argument> ctrlArgs;\n if (succeeded(parser.parseOptionalKeyword(\"ctrl\"))) {\n if (parseTypedArgList(ctrlArgs))\n return failure();\n }\n\n // Optional `iv ( <name> : <type> [, ...] )` for grid IV slots.\n SmallVector<OpAsmParser::Argument> ivArgs;\n if (succeeded(parser.parseOptionalKeyword(\"iv\"))) {\n if (parseTypedArgList(ivArgs))\n return failure();\n }\n\n if (visibilityAttr) {\n result.addAttribute(getSymVisibilityAttrName(result.name), visibilityAttr);\n }\n if (parser.parseOptionalAttrDictWithKeyword(result.attributes))\n return failure();\n\n Region *body = result.addRegion();\n SmallVector<OpAsmParser::Argument> allArgs(arguments);\n for (auto &a : ctrlArgs)\n allArgs.push_back(a);\n for (auto &a : ivArgs)\n allArgs.push_back(a);\n if (parser.parseRegion(*body, allArgs, /*enableNameShadowing=*/false))\n return failure();\n ThreadOp::ensureTerminator(*body, builder, result.location);\n return success();\n}","why":"ThreadOp::parse: how the private keyword, domain clause, function signature, ctrl and iv clauses are consumed and how function_type is built from the signature arguments only; determines the textual form the generated input must use to parse."},{"file_sha256":"0616db64bbc547b2c92dd9801dbf1dac5136f19fc11ebdd1019ffd9660af9534","kind":"verifier","lines":"563-584","path":"lib/Dataflow/IR/DataflowFunctionLikeOps.cpp","roles":["input_well_formedness"],"text":"LogicalResult 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}","why":"ThreadOp::verify: requires explicit private visibility, rejects declared function results, bounds the dynamic-work ordinal against function_type inputs and forbids channel/thread-token inputs there. Keeps the sampled definitions verifier-accepted."},{"file_sha256":"0616db64bbc547b2c92dd9801dbf1dac5136f19fc11ebdd1019ffd9660af9534","kind":"verifier","lines":"313-348","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;\n}","why":"Thread launch extent analysis rejecting negative constant grid upper bounds; the grammar only emits a nonnegative constant index extent per coordinate dimension."},{"file_sha256":"0616db64bbc547b2c92dd9801dbf1dac5136f19fc11ebdd1019ffd9660af9534","kind":"verifier","lines":"602-639","path":"lib/Dataflow/IR/DataflowFunctionLikeOps.cpp","roles":["input_well_formedness"],"text":"LogicalResult 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":"ThreadLaunchOp::verifySymbolUses: body operand types must equal callee function_type inputs position-by-position and the grid upper bound count must equal the callee's derived coordinate rank; the grammar reproduces the sampled signature and rank on the launch side."},{"file_sha256":"7b2bea863a561d79b9cc6deb6f69e2c6e535d46e50f23d7fddb0e13d1a952c7d","kind":"test","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 dense and dynamic-work thread definitions, ctrl/iv clauses, and launches with grid(...)/wait(...) plus the thread_token result type; used as concrete syntax evidence for the generated modules."},{"file_sha256":"c6f79ffa52853dc0bfac5214fbc7f94b0dacc45f8e5cdf216b2f0812c02bdff2","kind":"implementation","lines":"36-49","path":"lib/Frontend/Lowering/LowerForallToThreadPass.cpp","roles":["applicability"],"text":"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 }","why":"The named stage's whole behaviour: it emits an error for every func-nested scf.forall and otherwise leaves the module unchanged. Evidence that the stage never materializes a dataflow.thread, so the carrier must be supplied on the input side and inputs must contain no func-nested scf.forall for an output to exist."},{"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":"The stage's own lit test confirming that a raw scf.forall input fails the pass and that no dataflow.thread or dataflow.thread.launch is produced by it."},{"file_sha256":"8a0c5049c3721e2ae00c8509a0e6366803279237fc0361d741d2d2af0c47c815","kind":"implementation","lines":"23-34","path":"tools/loom-raise-opt/loom-raise-opt.cpp","roles":["applicability"],"text":"int main(int argc, char **argv) {\n ::mlir::DialectRegistry registry;\n ::mlir::registerAllDialects(registry);\n ::mlir::registerAllExtensions(registry);\n ::mlir::registerAllPasses();\n registry.insert<::dataflow::DataflowDialect, ::loom::LoomDialect>();\n loom::raising::registerRaisingPasses();\n loom::lowering::registerLoweringPasses();\n dataflow::registerDataflowTransformsPasses();\n return ::mlir::asMainReturnCode(::mlir::MlirOptMain(\n argc, argv, \"Loom raising-pass MLIR optimizer driver\\n\", registry));\n}","why":"Driver registration showing the Dataflow and Loom dialects are available and which Loom passes exist; basis for keeping the pass pipeline unchanged in subject-command.json."}],"primary_bundle_sha256":"5201ac9412e4d3f764ed9c41f8e23e4eb011a85de3f78b06ce525d942d928600","project":"PolyArch/loom","revision":"48615bc5925ef4b9db8b4550b5d4322933cf4b7b","schema":"spectriad.authoring-context/v1","selection_sha256":"b63d11544e46a57fba3997340bc5aad16a854d29370ea98d296cf2f336a10f18"}
sessions/reverse-generator/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 46800,
"duration_ms": 46850,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1324,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 5282,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.14380500000000002,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 3639,
"provider": "firstParty",
"thinkingTokens": 1056,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "## Preconditions\n\n1. Every emitted program is a single MLIR module body consisting of one or more module-scope `dataflow.thread` definitions followed by exactly one `func.func` named `@host`, in that order.\n2. Every `dataflow.thread` definition is declared with `private` visibility and a symbol name, and every symbol name is distinct within the module.\n3. Every `dataflow.thread` definition carries exactly one `domain(#dataflow.thread_domain<...>)` clause, which is either a closed dense domain (`dense`) or a dynamic-work domain (`dynamic_work, work_item_arg = N`); no other domain kind appears.\n4. A `dynamic_work` domain always names a `work_item_arg` ordinal `N`, and that ordinal is a valid zero-based index into the definition's own declared argument list, so a dynamic-work definition always has at least one declared argument.\n5. A `dynamic_work` definition never carries a coordinate (`iv`) clause \u2014 its coordinate rank is zero.\n6. A `dense` definition never carries a `work_item_arg` ordinal, and it carries an `iv (...)` clause exactly when its coordinate rank is nonzero; every coordinate argument in that clause has type `index`.\n7. Every `dataflow.thread` definition's entry signature has the fixed three-part shape: a parenthesized data-argument list, then a control clause `ctrl (%thread_ctrl: none)`, then (dense only, rank > 0) the coordinate clause \u2014 in that fixed order.\n8. Every `dataflow.thread` definition has a non-empty region terminated by a `dataflow.thread.yield`, which either takes no operands or takes exactly the control value `%thread_ctrl` of type `none`; the region contains no other operations.\n9. Each `dataflow.thread` definition is accompanied by exactly one `dataflow.thread.launch` in the host function, and the launches appear in the same order as the definitions they target.\n10. Every `dataflow.thread.launch` references its definition by the definition's symbol via `@`-symbol reference, and that symbol is always defined in the same module.\n11. The operand list of every launch has exactly the same arity as the referenced definition's data-argument list, and the i-th operand's type equals the i-th declared argument type of the definition.\n12. The explicit type signature written on every launch, `(types...) -> !dataflow.thread_token`, lists exactly the referenced definition's data-argument types in order and always produces the single result type `!dataflow.thread_token`.\n13. Every launch carries a `grid(...)` clause exactly when the referenced definition is a dense definition of nonzero coordinate rank, and the number of grid upper bounds equals that coordinate rank; launches targeting rank-zero or dynamic-work definitions carry no grid clause.\n14. Every grid upper bound operand has type `index`.\n15. Every launch binds its token result to an SSA name, and each such token name is unique within the host function.\n16. Every `dataflow.thread.wait` operand is the token produced by a preceding launch in the same block, and is written with the result type `!dataflow.thread_token`.\n17. Every SSA value used as a launch operand or grid bound is defined earlier in the host function \u2014 either as the function's own block argument or by an `arith.constant` in the entry block \u2014 so all uses are dominated by their definitions.\n18. The host function is terminated by `return` and returns no results.\n19. No `scf.forall` appears anywhere in an emitted program; the carrier shape is purely definition-plus-launch, with no mapping attribute, no `shared_outs`, no forall results and no combining region.\n20. No launch produces or consumes results other than its thread token, and no value flows back out of a thread definition to the host.\n\n## Sampling conventions\n\n1. The grammar emits between 1 and 3 thread definitions per module, never zero and never more than three.\n2. Definition symbols follow the fixed scheme `t_<i>` where `<i>` is the definition's zero-based position, and launch tokens follow the parallel scheme `%token_<i>` for the same index.\n3. Each definition's data arity is sampled from 0 to 3 inclusive; arities above three are never emitted.\n4. Argument types are drawn from a fixed cyclic palette of five types \u2014 `i32`, `f32`, `i64`, `index`, `memref<?xf32>` \u2014 by taking a contiguous run starting at a per-definition offset of 0 to 4, so the argument type list of any definition is always a contiguous rotation-free slice of that palette rather than an arbitrary combination; with arity at most 3 and offset at most 4, only palette positions 0 through 6 are ever reached.\n5. Data arguments are named `%arg_0`, `%arg_1`, ... in ascending order with no gaps.\n6. Coordinate rank for dense definitions is sampled from 0 to 2 inclusive, so no dense domain of rank 3 or higher is ever emitted; coordinate arguments are named `%coord_0`, `%coord_1`, ... in order.\n7. Dynamic-work versus dense is chosen by an even binary selection, but the dynamic branch is only taken when arity is greater than zero; zero-arity definitions are therefore always dense, and choosing the dynamic branch also forces the definition's recorded coordinate rank to zero.\n8. The `work_item_arg` ordinal of a dynamic-work definition is drawn uniformly over the whole valid range `0 .. arity-1`, so it may select any declared argument, not only the first or last.\n9. The control argument is always spelled exactly `%thread_ctrl: none`; no other control name or type is emitted.\n10. Both yield forms \u2014 the bare `dataflow.thread.yield` and the operand form `dataflow.thread.yield %thread_ctrl : none` \u2014 are emitted, chosen independently per definition.\n11. Each definition block is followed by a blank line; definitions and the host function are separated by that fixed whitespace skeleton.\n12. The host function has the fixed signature `func.func @host(%m_ref: memref<?xf32>)`, so the only memref value in scope is the function's block argument rather than a locally allocated buffer.\n13. The host entry block always begins with the same four-constant preamble, regardless of what the launches actually need: `%c_i32 = arith.constant 1 : i32`, `%c_f32 = arith.constant 1.000000e+00 : f32`, `%c_i64 = arith.constant 1 : i64`, and `%c_idx = arith.constant 4 : index`.\n14. Launch operands are selected by a name palette that mirrors the type palette one-for-one (`%c_i32`, `%c_f32`, `%c_i64`, `%c_idx`, `%m_ref`) using the same offset and position, so operand identity is fully determined by the argument's type slot and the same constant is reused for every occurrence of a given type.\n15. Every grid upper bound is the single constant `%c_idx` (value 4), so all launch domains are square and no varying or non-constant extents are exercised.\n16. A `dataflow.thread.wait` is optionally emitted immediately after each launch, chosen independently per launch, so a program may mix awaited and un-awaited launches; waits are never grouped, reordered, or placed anywhere other than directly after their own launch.\n17. Launch bodies are emitted in a fixed textual order \u2014 operands, then optional grid clause, then the `: (types) -> !dataflow.thread_token` signature \u2014 and always with the explicit type signature spelled out rather than elided.\n18. All launches are placed in a single straight-line block between the constant preamble and `return`, with no control flow, nesting, or interleaved computation.\n19. Indentation is fixed at two spaces for all operations inside the host function and inside thread regions.",
"result_index": 0,
"session_id": "3aff1233-c70d-4b5f-9033-9e0240fbe7cc",
"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": 50,
"total_cost_usd": 0.14380500000000002,
"ttft_ms": 14825,
"ttft_stream_ms": 1070,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 5282,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 5282,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 3639,
"output_tokens_details": {
"thinking_tokens": 1056
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "a170ca7c-ec71-49f5-be32-7f103c9458d5"
}
]
sessions/reverse-postcondition/session-evidence/result-events.json[
{
"api_error_status": null,
"duration_api_ms": 15703,
"duration_ms": 15730,
"fast_mode_disabled_reason": "sdk_opt_in_required",
"fast_mode_state": "off",
"first_content_frame_ms": 1529,
"is_error": false,
"modelUsage": {
"claude-opus-5": {
"cacheCreationInputTokens": 5536,
"cacheReadInputTokens": 0,
"canonicalModel": "claude-opus-5",
"contextWindow": 1000000,
"costBasis": "list",
"costUSD": 0.083045,
"inputTokens": 2,
"maxOutputTokens": 64000,
"outputTokens": 1107,
"provider": "firstParty",
"thinkingTokens": 359,
"webSearchRequests": 0
}
},
"num_turns": 1,
"permission_denials": [],
"queued_turn_count": 0,
"result": "This postcondition examines only the `output` program \u2014 the `input` root is never referenced \u2014 and it scans `output.operations`, so every operation at every nesting depth is in scope. It builds two selections by exact name: `threads` (ops named `dataflow.thread`) and `launches` (ops named `dataflow.thread.launch`); ops of any other name, including other `dataflow.*` ops, are ignored entirely. Universally over each thread, it rejects unless the `function_type` attribute's function type has exactly zero declared results, the operation itself has exactly zero SSA results, and every declared input type in that same `function_type` has a `canonical_text` different from the literal string `!dataflow.thread_token` \u2014 so a thread whose signature declares any result, or which produces any SSA value, or which takes a parameter whose canonical text is exactly that token string, is rejected. Universally over each launch, it resolves the launch's `callee` symbol attribute against the output program and, for each resolved target whose name is `dataflow.thread`, requires that the callee's declared `function_type` inputs correspond position by position with the types of the values in operand segment 0 of the launch (the segment decoded from the launch's `operandSegmentSizes`); each zipped pair must be equal as types, and a length mismatch between the two sequences makes that assert fail with both lengths reported. Allowed value sources are thus exclusively the output's operation names, SSA result lists, `function_type` attribute projections, type canonical text and type equality, symbol resolution, and segment-0 operand types; nothing is compared against the input and no counts relate the two programs. The check is vacuously satisfied when the output contains no `dataflow.thread` ops and no `dataflow.thread.launch` ops, and each launch's inner claim is likewise vacuous when its `callee` resolves to no operations or to no operation named `dataflow.thread`; a thread with an empty input-type list also passes the token assertion vacuously. No assertion demands that any thread or launch exist, so an output with none of these ops is accepted. Conversely, the postcondition does not pass but errs where a selected thread or a resolved callee lacks a `function_type` attribute, where that attribute is not a function type, or where a launch carries no `operandSegmentSizes` property to decode segment 0.",
"result_index": 0,
"session_id": "e6c12c44-c2b2-4342-8e30-d8b9fa5b996a",
"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.083045,
"ttft_ms": 5837,
"ttft_stream_ms": 1078,
"type": "result",
"usage": {
"cache_creation": {
"ephemeral_1h_input_tokens": 5536,
"ephemeral_5m_input_tokens": 0
},
"cache_creation_input_tokens": 5536,
"cache_read_input_tokens": 0,
"inference_geo": "not_available",
"input_tokens": 2,
"iterations": [],
"output_tokens": 1107,
"output_tokens_details": {
"thinking_tokens": 359
},
"server_tool_use": {
"web_fetch_requests": 0,
"web_search_requests": 0
},
"service_tier": "standard",
"speed": "standard"
},
"uuid": "62e3250c-ff41-42c7-a398-9133079cd289"
}
]
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.