Skip to content

Enforcing linear ownership of QLX values in C++ verifiers - #5889

Open
sacpis wants to merge 20 commits into
NVIDIA:mainfrom
sacpis:p0_linearity_verifier
Open

sacpis wants to merge 20 commits into
NVIDIA:mainfrom
sacpis:p0_linearity_verifier

Conversation

@sacpis

@sacpis sacpis commented Nov 11, 2026 •

Copy link
Copy Markdown
Collaborator

Linear QLX values such as !qlx.logical_qubit, !fabric.patch and !phys.state must be consumed exactly once. Until now only the Python checker (linearity.py) enforced this, so qlx-opt accepted IR that consumed a qubit twice or leaked one (raised in review of #5860).

Here we have moved the check into C++ and run it from the op verifiers, so every entry point enforces it.

  • cudaq::LinearTypeInterface (isLinear, mayDrop) and four op traits are defined in LinearOwnershipInterfaces.td and compiled into libcudaqMLIR.so. The traits describe how ops treat linear values
    • ownership scopes
    • borrowing operands
    • exclusive regions (cflow.if, event.try_take)
    • repeated regions (cflow.repeat, cflow.while)

The generated headers are installed with the SDK, so preview/logical builds against an installed CUDA-Q. A new add_cudaq_type_interface CMake helper generates them. Quake's wire and cable types don't implement the interface yet. That comes in a follow-up PR.

  • MLIRQLXLinearOwnership is driven only by the interface and the traits, so it names no dialect. It reports a value that is:
    • consumed twice
    • consumed inside a loop it was captured into
    • used after it was consumed
    • never consumed, including consumed in only some branches of an if

Where it runs

  • qlx.program and qlx.objective_body run the analysis in verifyRegions, so invalid P0 IR fails at parse or verify time.
  • The qlx-verify-linearity pass runs the same analysis over every tier (lvm.kernel, fabric.gadget, fabric.protocol, fabric.circuit and phys.graph). It reports all violations instead of only the first.

A new C API and nanobind binding expose the analysis. linearity.py now calls it instead of its own name based checker, with the same public API.

Fixes #5883.

Signed-off-by: Sachin Pisal <spisal@nvidia.com>
Signed-off-by: Sachin Pisal <spisal@nvidia.com>
Signed-off-by: Sachin Pisal <spisal@nvidia.com>
Signed-off-by: Sachin Pisal <spisal@nvidia.com>
@github-actions github-actions Bot added build The issue related to the CUDA Quantum build cuda-q logical Related to CUDA-Q Logical. labels Nov 11, 2026
@sacpis
sacpis requested a review from anpaz November 11, 2026 04:37
@github-actions

github-actions Bot commented Nov 11, 2026 •

Copy link
Copy Markdown

CI Summary (push) — ✅ passed

Run #43473103876 · ✅ 8 · ⏩ 11 · ❌ 0 · ⛔ 0

Top-level jobs (19)
Job Result
binaries ⏩ skipped
build_and_test ✅ success
changes ✅ success
config_devdeps ✅ success
config_source_build ⏩ skipped
config_wheeldeps ✅ success
devdeps ✅ success
docker_image ⏩ skipped
documentation ✅ success
edem_wheels ⏩ skipped
gen_code_coverage ⏩ skipped
metadata ✅ success
python_devel_wheel ⏩ skipped
python_metapackages ⏩ skipped
python_wheels ⏩ skipped
python_wheels_cu12_validation ⏩ skipped
python_wheels_cu13 ⏩ skipped
source_build ⏩ skipped
wheeldeps ✅ success
⏩ Skipped jobs (11) — intentionally skipped on PR builds; run on merge_group / workflow_dispatch
Job
binaries
config_source_build
docker_image
edem_wheels
gen_code_coverage
python_devel_wheel
python_metapackages
python_wheels_cu12_validation
python_wheels_cu13
python_wheels
source_build
All sub-jobs (48) — every matrix leg, with links
Job Status Link
Build and test (amd64, gcc12, openmpi) / Dev environment (Debug) ✅ success view
Build and test (amd64, gcc12, openmpi) / Dev environment (Python) ✅ success view
Build and test (amd64, llvm, openmpi) / Dev environment (Debug) ✅ success view
Build and test (amd64, llvm, openmpi) / Dev environment (Python) ✅ success view
Build and test (arm64, llvm, openmpi) / Dev environment (Debug) ✅ success view
Build and test (arm64, llvm, openmpi) / Dev environment (Python) ✅ success view
CI Summary ❔ in_progress view
Check for stable CUDA-Q changes ✅ success view
Configure build (devdeps) ✅ success view
Configure build (source_build) ⏩ skipped view
Configure build (wheeldeps) ✅ success view
Create CUDA 12 Python wheels ⏩ skipped view
Create CUDA 13 Python wheels ⏩ skipped view
Create CUDA Quantum installer ⏩ skipped view
Create Docker images ⏩ skipped view
Create Python metapackages ⏩ skipped view
Create cudaq-edem wheels (${{ matrix.platform }}) ⏩ skipped view
Create shared Python development wheel ⏩ skipped view
Documentation / Build and check docs ✅ success view
Gen code coverage ⏩ skipped view
Load dependencies (amd64, gcc12) / Caching ✅ success view
Load dependencies (amd64, gcc12) / Finalize ✅ success view
Load dependencies (amd64, gcc12) / Metadata ✅ success view
Load dependencies (amd64, llvm) / Caching ✅ success view
Load dependencies (amd64, llvm) / Finalize ✅ success view
Load dependencies (amd64, llvm) / Metadata ✅ success view
Load dependencies (arm64, gcc12) / Caching ✅ success view
Load dependencies (arm64, gcc12) / Finalize ✅ success view
Load dependencies (arm64, gcc12) / Metadata ✅ success view
Load dependencies (arm64, llvm) / Caching ✅ success view
Load dependencies (arm64, llvm) / Finalize ✅ success view
Load dependencies (arm64, llvm) / Metadata ✅ success view
Load source build cache ⏩ skipped view
Load wheel dependencies (amd64, 12.6) / Caching ✅ success view
Load wheel dependencies (amd64, 12.6) / Finalize ✅ success view
Load wheel dependencies (amd64, 12.6) / Metadata ✅ success view
Load wheel dependencies (amd64, 13.0) / Caching ✅ success view
Load wheel dependencies (amd64, 13.0) / Finalize ✅ success view
Load wheel dependencies (amd64, 13.0) / Metadata ✅ success view
Load wheel dependencies (arm64, 12.6) / Caching ✅ success view
Load wheel dependencies (arm64, 12.6) / Finalize ✅ success view
Load wheel dependencies (arm64, 12.6) / Metadata ✅ success view
Load wheel dependencies (arm64, 13.0) / Caching ✅ success view
Load wheel dependencies (arm64, 13.0) / Finalize ✅ success view
Load wheel dependencies (arm64, 13.0) / Metadata ✅ success view
Prepare cache clean-up ✅ success view
Retrieve PR info ✅ success view
Validate CUDA 12 Python wheels ⏩ skipped view
✅ Required checks (7/7) — declared in .github/required-checks.yml for push
Required check Status Link
Build and test (amd64, llvm, openmpi) / Dev environment (Debug) ✅ success view
Build and test (amd64, llvm, openmpi) / Dev environment (Python) ✅ success view
Build and test (arm64, llvm, openmpi) / Dev environment (Debug) ✅ success view
Build and test (arm64, llvm, openmpi) / Dev environment (Python) ✅ success view
Build and test (amd64, gcc12, openmpi) / Dev environment (Debug) ✅ success view
Build and test (amd64, gcc12, openmpi) / Dev environment (Python) ✅ success view
Documentation / Build and check docs ✅ success view

@sacpis sacpis changed the title Enforcing linear single ownership of P0 values in C++ Enforcing linear ownership of QLX values in C++ verifiers Nov 11, 2026

@lmondada lmondada left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Awesome, I think it's a great step in the right direction to try to formalize the linearity constraints better! Can you evaluate whether there's any way this could supersede SSITrait (or if we could define SSITrait in terms of LinearTypeInterface?).

We don't need to resolve everything now, but it would be good to have a clear idea of where we want to go.

Signed-off-by: Sachin Pisal <spisal@nvidia.com>
Signed-off-by: Sachin Pisal <spisal@nvidia.com>
Signed-off-by: Sachin Pisal <spisal@nvidia.com>
@github-actions github-actions Bot added the testing Relates to testing label Nov 12, 2026
Signed-off-by: Sachin Pisal <spisal@nvidia.com>
@sacpis

sacpis commented Nov 12, 2026

Copy link
Copy Markdown
Collaborator Author

Awesome, I think it's a great step in the right direction to try to formalize the linearity constraints better! Can you evaluate whether there's any way this could supersede SSITrait (or if we could define SSITrait in terms of LinearTypeInterface?).

We don't need to resolve everything now, but it would be good to have a clear idea of where we want to go.

Thanks. Yes, I think the interface can supersede SSITypeTrait and here is where I would like to go.

  1. With this PR

    • The analysis and the verify-linear-ownership pass are in core, and cudaq-opt can run the pass.
    • SSITypeTrait now sits next to LinearTypeInterface.
    • A LinearTypeTraits<...>.traits helper gives a type both, and all QLX linear types use it. So in practice the trait is already defined in terms of the interface.
  2. With the next PR (regarding interface as a source of truth) will

    • Add LinearTypeInterface to BuiltinTypeInterfaces.td in our MLIR patch.
    • Change the patch's three hasTrait<TypeTrait::SSIType>() checks to implements the interface and isLinear().
    • Drop SSIType.
  3. About quake coverage

    • Tag !quake.wire and !quake.cable with the interface.
    • Let the analysis treat a function op as a scope, since func.func cannot carry our LinearOwnershipScope trait.
    • After that, the same verifier checks Quake value semantics IR as well.

Please let me know if you would like to see any updates to this plan here.

@sacpis
sacpis requested a review from lmondada November 12, 2026 22:08
@lmondada

Copy link
Copy Markdown
Collaborator

Thanks @sacpis that plan sounds great.

@lmondada lmondada left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you so much!

@sacpis

sacpis commented Nov 13, 2026

Copy link
Copy Markdown
Collaborator Author

Thanks @sacpis that plan sounds great.

Thank you Luca for your feedback.

Hold hold hold. Awaiting others feedback as well.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

build The issue related to the CUDA Quantum build core compiler cuda-q logical Related to CUDA-Q Logical. testing Relates to testing

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Check P0 linearity in C++, not only in Python

2 participants