Skip to content

Write the ownership verdict into the IR - #4

Closed
ZweZeya wants to merge 1 commit into
fix/analysis-soundnessfrom
feat/queue-kind-in-ir
Closed

ZweZeya wants to merge 1 commit into
fix/analysis-soundnessfrom
feat/queue-kind-in-ir

Conversation

@ZweZeya

@ZweZeya ZweZeya commented Oct 18, 2026 •

Copy link
Copy Markdown
Collaborator

Stacked on #3 (fix/analysis-soundness).

What this changes

The verdict was printed and nothing else, so no later pass could read it. Each queue's root (cir.global or cir.alloca) now carries wtc.queue_kind, and so does every push and pop. One op can reach several queues, so an op carries the join of their verdicts, the weakest (several producers / several consumers / unknown, or-ed). The stdout report is unchanged. The attribute and the stamping come from 253a2bc, extended to roots and to the join.

How it was checked

25 of 25 pass, no warnings: queue-kind-attribute.mlir (ported from 253a2bc) and queue-kind-join.mlir (one push reaching an SPSC and an MPSC queue is MPSC; each global keeps its own).

Checklist

  • CI is green
  • New behaviour has a test; a fixed bug has a test that failed before
  • No file moves or renames mixed in with substantive changes
  • The pinned LLVM revision is untouched, or this PR does nothing else

🤖 Generated with Claude Code

The verdict was printed and nothing else, so no later pass could read
it and the pipeline stopped exactly where specialisation would begin.

Each queue's root, its cir.global or cir.alloca, now carries its verdict
as wtc.queue_kind, and so does every push and pop. Since one op can reach
several queues -- a helper called with each of two -- an op carries the
join of its queues' verdicts, the weakest: a verdict is three facts
(several producers, several consumers, unknown) and the join ors them.
An op with an access that reached no queue the analysis could name is
UNKNOWN.

The stdout report is unchanged, so every existing test still holds.

The attribute and the stamping are carried over from 253a2bc
(feat/select-queue-impl), extended to roots and to the join.

Verified: 24 of 24 pass, no warnings.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@ZweZeya
ZweZeya force-pushed the feat/queue-kind-in-ir branch from b98246d to 9d20b82 Compare October 18, 2026 05:20
@ZweZeya
ZweZeya force-pushed the fix/analysis-soundness branch from 30eca14 to 25d430f Compare October 18, 2026 05:20
@apaznikov

Copy link
Copy Markdown
Collaborator

Closing as superseded by #10. The verdict is written into the IR there as #wtc.topology on each queue's root and on every push and pop, with an operation that may reach several queues joined to unknown. The idea of naming the queue on each operation is taken from this PR: mlir: Name the queue each operation acts on adds a queue_id on the root and on every operation that can only act on that root, which the borrow analysis and the declared-topology check then rely on.

@apaznikov apaznikov closed this Oct 19, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants