diff --git a/cuda-oxide/crates/mir-importer/src/translator/terminator/drop_glue.rs b/cuda-oxide/crates/mir-importer/src/translator/terminator/drop_glue.rs index ec0359ebb2..3d95fc512e 100644 --- a/cuda-oxide/crates/mir-importer/src/translator/terminator/drop_glue.rs +++ b/cuda-oxide/crates/mir-importer/src/translator/terminator/drop_glue.rs @@ -8,8 +8,8 @@ //! This module provides two capabilities: //! //! 1. **No-op analysis** ([`drop_glue_is_noop`]): a conservative static proof -//! that dropping a value does nothing observable, allowing the `Drop` -//! terminator to be lowered as a plain branch (fast path). +//! that dropping a value does nothing observable and returns, allowing +//! the `Drop` terminator to be lowered as a plain branch (fast path). //! //! 2. **Drop glue emission** (`emit_drop_glue`): when the no-op proof fails, //! emits a device-side call to the monomorphized `drop_in_place::` @@ -42,6 +42,11 @@ //! Anything else (writes through pointers, asserts, inline asm, calls we //! cannot resolve or whose body we cannot see) fails the proof. //! +//! The proof also requires the glue to return. A reachable control-flow +//! cycle, or a call back into an instance that is already under proof, +//! fails it even when every statement is harmless: erasing a call that +//! may never return would let the code after the drop execute. +//! //! The walk follows constant `switchInt` discriminants, so branches that //! the compiler has already folded shut (for example checks behind the //! `UbChecks` flag, which is off for device builds) do not have to be @@ -320,16 +325,17 @@ fn compute_drop_place_address( } // ============================================================================ -// No-op analysis (unchanged from original) +// Conservative no-op and termination analysis // ============================================================================ -/// Proves that calling `instance` does nothing observable. +/// Proves that erasing a call to `instance` preserves observable behavior, +/// including whether control can return to its caller. /// /// `in_progress` holds the mangled names of instances currently being -/// proven further up the call stack. If we meet one of them again we -/// treat the cycle as harmless: a cycle cannot *introduce* an -/// observable effect, every effect would already have failed the proof -/// on some statement or terminator along the way. +/// proven further up the call stack. Meeting one again means termination +/// is not proven: even recursion with no externally visible writes can +/// diverge, and erasing such a call would make unreachable code execute. +/// Recursion therefore fails this conservative proof. fn instance_is_noop(instance: &Instance, in_progress: &mut Vec) -> bool { // Fast path: a type with no drop glue at all resolves to an "empty" // drop shim that exists only to fill vtable slots. rustc_public @@ -344,7 +350,7 @@ fn instance_is_noop(instance: &Instance, in_progress: &mut Vec) -> bool let name = instance.mangled_name(); if in_progress.contains(&name) { - return true; + return false; } // No body means we cannot see what the call does (an intrinsic, a @@ -359,102 +365,136 @@ fn instance_is_noop(instance: &Instance, in_progress: &mut Vec) -> bool result } -/// Walks every block of `body` reachable from the entry block and -/// checks that nothing observable happens on the way to `return`. +/// Walks every block of `body` reachable from the entry block and proves +/// that execution is effect-free and contains no reachable control-flow cycle. +/// +/// A cycle fails the proof even when every statement in it is locally harmless: +/// removing a call that can diverge would change whether its continuation runs. fn body_is_noop(body: &mir::Body, in_progress: &mut Vec) -> bool { - let mut visited = vec![false; body.blocks.len()]; - let mut worklist: Vec = vec![0]; + #[derive(Clone, Copy, PartialEq, Eq)] + enum BlockState { + Unseen, + InProgress, + Proven, + } - while let Some(idx) = worklist.pop() { - if std::mem::replace(&mut visited[idx], true) { - continue; - } - let block = &body.blocks[idx]; + #[derive(Clone, Copy)] + enum WorkItem { + Enter(mir::BasicBlockIdx), + Finish(mir::BasicBlockIdx), + } - for stmt in &block.statements { - if !statement_is_noop(&stmt.kind) { - return false; - } - } + let mut states = vec![BlockState::Unseen; body.blocks.len()]; + let mut worklist = vec![WorkItem::Enter(0)]; - match &block.terminator.kind { - // Reaching `return` with only no-op work behind us is the - // success case. `unreachable` cannot execute in a valid - // program, so it cannot contribute an effect either. - mir::TerminatorKind::Return | mir::TerminatorKind::Unreachable => {} - - mir::TerminatorKind::Goto { target } => worklist.push(*target), - - mir::TerminatorKind::SwitchInt { discr, targets } => { - match const_operand_bits(discr) { - // Known discriminant: only the matching branch can - // run, so only that branch needs to be a no-op. - // This is what skips the dead "really drop the - // elements" branch in `IntoIter`'s destructor. - Some(value) => { - let target = targets - .branches() - .find(|(branch_value, _)| *branch_value == value) - .map(|(_, target)| target) - .unwrap_or_else(|| targets.otherwise()); - worklist.push(target); - } - // Unknown discriminant: every branch must be a - // no-op. - None => worklist.extend(targets.all_targets()), - } + while let Some(item) = worklist.pop() { + match item { + WorkItem::Finish(idx) => { + debug_assert!(matches!(states[idx], BlockState::InProgress)); + states[idx] = BlockState::Proven; + continue; } - // A nested drop is fine when the dropped value's own glue - // passes this same proof. - mir::TerminatorKind::Drop { place, target, .. } => { - let Ok(place_ty) = place.ty(body.locals()) else { - return false; - }; - let nested = Instance::resolve_drop_in_place(place_ty); - if !instance_is_noop(&nested, in_progress) { - return false; + WorkItem::Enter(idx) => { + match states[idx] { + // A completed block reached through another predecessor is + // ordinary CFG reconvergence. + BlockState::Proven => continue, + + // A block already on the active DFS path is a reachable CFG + // cycle. Effect-freedom does not prove that it terminates. + BlockState::InProgress => return false, + + BlockState::Unseen => {} } - worklist.push(*target); - } - // A call is fine when we can resolve exactly which function - // runs and that function passes this same proof. The - // `drop_in_place` shim for a type with an `impl Drop` is a - // single such call to `::drop`. - mir::TerminatorKind::Call { - func, - destination, - target: Some(target), - .. - } => { - if place_writes_through_pointer(destination) { - return false; + states[idx] = BlockState::InProgress; + let block = &body.blocks[idx]; + + for stmt in &block.statements { + if !statement_is_noop(&stmt.kind) { + return false; + } } - let Ok(func_ty) = func.ty(body.locals()) else { - return false; - }; - let TyKind::RigidTy(RigidTy::FnDef(def, args)) = func_ty.kind() else { - // A function pointer or other indirect callee: we - // do not know what runs. - return false; - }; - let Ok(callee) = Instance::resolve(def, &args) else { - return false; - }; - if !instance_is_noop(&callee, in_progress) { - return false; + + // Only mark this block Proven after every runtime-reachable + // successor has itself been proven. + worklist.push(WorkItem::Finish(idx)); + + match &block.terminator.kind { + mir::TerminatorKind::Return | mir::TerminatorKind::Unreachable => {} + + mir::TerminatorKind::Goto { target } => { + worklist.push(WorkItem::Enter(*target)); + } + + mir::TerminatorKind::SwitchInt { discr, targets } => { + match const_operand_bits(discr) { + Some(value) => { + let target = targets + .branches() + .find(|(branch_value, _)| *branch_value == value) + .map(|(_, target)| target) + .unwrap_or_else(|| targets.otherwise()); + + worklist.push(WorkItem::Enter(target)); + } + + None => { + for target in targets.all_targets() { + worklist.push(WorkItem::Enter(target)); + } + } + } + } + + mir::TerminatorKind::Drop { place, target, .. } => { + let Ok(place_ty) = place.ty(body.locals()) else { + return false; + }; + + let nested = Instance::resolve_drop_in_place(place_ty); + if !instance_is_noop(&nested, in_progress) { + return false; + } + + worklist.push(WorkItem::Enter(*target)); + } + + mir::TerminatorKind::Call { + func, + destination, + target: Some(target), + .. + } => { + if place_writes_through_pointer(destination) { + return false; + } + + let Ok(func_ty) = func.ty(body.locals()) else { + return false; + }; + + let TyKind::RigidTy(RigidTy::FnDef(def, args)) = func_ty.kind() else { + return false; + }; + + let Ok(callee) = Instance::resolve(def, &args) else { + return false; + }; + + if !instance_is_noop(&callee, in_progress) { + return false; + } + + worklist.push(WorkItem::Enter(*target)); + } + + // Asserts, diverging calls, inline asm, resume/abort, and + // unknown terminators do not prove normal termination. + _ => return false, } - worklist.push(*target); } - - // Everything else (asserts, diverging calls, inline asm, - // resume/abort) either has an effect or might not return. - // Asserts fail the proof deliberately: following only the - // success edge would silently delete a would-be device trap. - // A failed proof now emits the real drop_in_place call, so - // there is no pressure to widen the proof here. - _ => return false, } } diff --git a/cuda-oxide/crates/rustc-codegen-cuda/STATUS.md b/cuda-oxide/crates/rustc-codegen-cuda/STATUS.md index d90ba3af6e..f42a90129f 100644 --- a/cuda-oxide/crates/rustc-codegen-cuda/STATUS.md +++ b/cuda-oxide/crates/rustc-codegen-cuda/STATUS.md @@ -39,9 +39,10 @@ other device function; see the `drop_glue` example. This covers direct `impl Drop` types reachable from kernels. The shim and every `Drop::drop` body it reaches go through the same device pipeline, so drop glue whose MIR uses constructs the pipeline cannot yet translate -(e.g. slice/`Vec` element drops, panic formatting) still fails +(e.g. `Vec` element drops, panic formatting) still fails compilation with a diagnostic. Destructors are never silently skipped: -a drop is either proven unobservable or its call is emitted. +a drop is either proven unobservable and terminating, or its call is +emitted. The remaining enum storage fixtures deliberately fail closed. Pointer and integer payloads cannot share one lowered slot without erasing LLVM pointer diff --git a/cuda-oxide/crates/rustc-codegen-cuda/examples/drop_glue/README.md b/cuda-oxide/crates/rustc-codegen-cuda/examples/drop_glue/README.md index bbbb15d6a9..4ca68b357a 100644 --- a/cuda-oxide/crates/rustc-codegen-cuda/examples/drop_glue/README.md +++ b/cuda-oxide/crates/rustc-codegen-cuda/examples/drop_glue/README.md @@ -42,6 +42,34 @@ distinguish a destructor that ran from one that was correctly suppressed. | 5 | `MaybeUninit::write` + `assume_init_drop` | `0xDEADBEEF` | | 6 | `MaybeUninit::assume_init_read` | `0xDEADBEEF` | +## Compile-only drop proof probes + +Three additional kernels guard the proof that lets the compiler erase a +destructor call: two against erasing a non-terminating destructor (#1360), +one against rejecting a destructor the proof should accept. + +- `diverging_cfg_drop_probe`: the destructor contains `loop {}`. +- `diverging_recursive_drop_probe`: the destructor calls an unconditionally + recursive helper. +- `reconverging_drop_probe`: the destructor is an effect-free `if`/`else` + whose branches join back together. The proof must still accept it, so + the drop lowers to a plain branch. + +Each probe writes a sentinel before the drop and a different value after +it. `verify-code-shape.sh` first asserts the importer's decision in the +pre-opt `drop_glue.ll`: the two diverging probes keep a call to their drop +glue in the kernel body, and the reconverging probe has none. It then +checks the optimized PTX. For the diverging probes the pre-drop store +remains and is immediately followed by an unconditional self-loop, while +the unreachable post-drop store is absent. For the reconverging probe both +stores remain. The PTX adjacency holds because `opt -O2` inlines the +retained glue; `#[inline(never)]` is not propagated as `noinline`. + +These kernels are compiled but **never launched by `main`**. Do not launch +the diverging probes manually: their destructors intentionally never +return. The existing runtime checks above continue to exercise terminating +destructors only. + ## Usage Optimized: @@ -56,6 +84,21 @@ Low MIR optimization: CUDA_OXIDE_NO_OPT=1 cargo oxide run drop_glue ``` +Optimized compile-only code checks, from the cuda-oxide repository root: + +```bash +cargo oxide build drop_glue +bash crates/rustc-codegen-cuda/examples/drop_glue/verify-code-shape.sh +``` + +The shape check targets optimized output; rebuild without +`CUDA_OXIDE_NO_OPT=1` before running it. The existing smoketest runner also +discovers and runs this script automatically: + +```bash +scripts/smoketest.sh -o '^drop_glue$' +``` + ## Expected output ```text diff --git a/cuda-oxide/crates/rustc-codegen-cuda/examples/drop_glue/src/main.rs b/cuda-oxide/crates/rustc-codegen-cuda/examples/drop_glue/src/main.rs index 3e3f455599..fa3b02fddb 100644 --- a/cuda-oxide/crates/rustc-codegen-cuda/examples/drop_glue/src/main.rs +++ b/cuda-oxide/crates/rustc-codegen-cuda/examples/drop_glue/src/main.rs @@ -41,6 +41,59 @@ impl Drop for DropMarker { } } +// Compile-only regression probes. These destructors intentionally never return; +// their kernels are generated but never launched by `main`. +#[allow(dead_code)] +struct LoopingDrop(u8); + +impl Drop for LoopingDrop { + #[inline(never)] + #[allow(clippy::empty_loop)] + fn drop(&mut self) { + loop {} + } +} + +#[allow(unconditional_recursion)] +#[inline(never)] +fn recursive_noop() { + recursive_noop(); +} + +#[allow(dead_code)] +struct RecursiveDrop(u8); + +impl Drop for RecursiveDrop { + #[inline(never)] + fn drop(&mut self) { + recursive_noop(); + } +} + +// Precision control for the proof. An effect-free destructor whose two +// branches join back together returns on every path, so the proof must keep +// accepting it and lower the drop to a plain branch. The callees have visible +// empty bodies; `#[inline(never)]` keeps the diamond in the destructor's MIR. +#[inline(never)] +fn left_noop() {} + +#[inline(never)] +fn right_noop() {} + +#[allow(dead_code)] +struct DiamondDrop(u8); + +impl Drop for DiamondDrop { + #[inline(never)] + fn drop(&mut self) { + if self.0 == 0 { + left_noop() + } else { + right_noop() + } + } +} + #[cuda_module] mod kernels { use super::*; @@ -57,6 +110,71 @@ mod kernels { } } + /// Compile-only regression: a reachable CFG cycle inside Drop::drop + /// must not be classified as an erasable no-op. + #[kernel] + pub fn diverging_cfg_drop_probe(mut out: DisjointSlice) { + if thread::index_1d().get() != 0 { + return; + } + + unsafe { + let slot = out.as_mut_ptr(); + slot.write(0x1111_1111); + + { + let _guard = LoopingDrop(0); + } + + // Semantically unreachable. + slot.write(0x2222_2222); + } + } + + /// Compile-only regression: recursive nontermination in a callee must + /// likewise prevent drop elision. + #[kernel] + pub fn diverging_recursive_drop_probe(mut out: DisjointSlice) { + if thread::index_1d().get() != 0 { + return; + } + + unsafe { + let slot = out.as_mut_ptr(); + slot.write(0x3333_3333); + + { + let _guard = RecursiveDrop(0); + } + + // Semantically unreachable. + slot.write(0x4444_4444); + } + } + + /// Compile-only precision control: an effect-free `if`/`else` inside + /// `Drop::drop` joins back together, so the proof must still erase the + /// drop. The post-drop store goes to a second slot so neither store is + /// dead and both stay visible in the optimized PTX. + #[kernel] + pub fn reconverging_drop_probe(mut out: DisjointSlice) { + if thread::index_1d().get() != 0 { + return; + } + + unsafe { + let slot = out.as_mut_ptr(); + slot.write(0x5555_5555); + + { + let _guard = DiamondDrop(thread::index_1d().get() as u8); + } + + // Reachable: the destructor returns. + slot.add(1).write(0x6666_6666); + } + } + #[kernel] pub fn drop_control_kernel(mut out: DisjointSlice) { if thread::index_1d().get() != 0 { diff --git a/cuda-oxide/crates/rustc-codegen-cuda/examples/drop_glue/verify-code-shape.sh b/cuda-oxide/crates/rustc-codegen-cuda/examples/drop_glue/verify-code-shape.sh new file mode 100644 index 0000000000..e9695f81bd --- /dev/null +++ b/cuda-oxide/crates/rustc-codegen-cuda/examples/drop_glue/verify-code-shape.sh @@ -0,0 +1,154 @@ +#!/usr/bin/env bash +# SPDX-FileCopyrightText: Copyright (c) 2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +# The device-side drop no-op proof may erase a destructor call only when the +# glue is effect-free and returns. Assert the importer's decision in the +# pre-opt drop_glue.ll: the two diverging probes keep a call to their drop +# glue in the kernel body, and the reconverging control has none. Then check +# what LLVM made of it in the optimized PTX, so a regression in either +# direction cannot pass compile-only CI. + +set -euo pipefail + +root="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +ll="${1:-${root}/drop_glue.ll}" +ptx="${2:-${root}/drop_glue.ptx}" + +for artifact in "${ll}" "${ptx}"; do + if [[ ! -s "${artifact}" ]]; then + echo "error: missing ${artifact}; run cargo oxide build drop_glue without CUDA_OXIDE_NO_OPT" >&2 + exit 1 + fi +done + +python3 - "${ll}" "${ptx}" <<'VERIFY_PY' +import re +import sys + +ll_path, ptx_path = sys.argv[1], sys.argv[2] +ll = open(ll_path, encoding="utf-8").read() +ptx = open(ptx_path, encoding="utf-8").read() +# Strip comments so a mention in a comment cannot satisfy or hide a check. +ll = re.sub(r";[^\n]*", "", ll) +ptx = re.sub(r"/\*.*?\*/|//[^\n]*", "", ptx, flags=re.S) + +# A call to the monomorphized `core::ptr::drop_glue::` shim, in the v0 +# mangling the device build uses. +GLUE_CALL = re.compile(r"call void @\S*4core3ptr9drop_glue\S*\(") + +def kernel_body(name): + header = re.search( + r"^define ptx_kernel void @" + re.escape(name) + r"\(.*$", + ll, + flags=re.M, + ) + if header is None: + raise SystemExit(f"error: missing LLVM kernel {name} in {ll_path}") + + end = re.compile(r"^\}$", flags=re.M).search(ll, header.end()) + if end is None: + raise SystemExit(f"error: unterminated LLVM kernel {name} in {ll_path}") + + return ll[header.end():end.start()] + +def require_glue_call(body, type_name, name): + pattern = rf"call void @\S*drop_glue\d+{type_name}\S*\(" + if re.search(pattern, body) is None: + raise SystemExit( + f"error: {name} lost the drop_glue::<{type_name}> call in {ll_path}" + ) + +def reject_glue_call(body, name): + call = GLUE_CALL.search(body) + if call is not None: + raise SystemExit( + f"error: {name} kept a drop glue call the no-op proof should have " + f"erased: {call.group(0)}" + ) + +def entry_body(name): + header = re.search( + r"\.entry\s+" + re.escape(name) + r"\s*\([^)]*\)\s*\{", + ptx, + ) + if header is None: + raise SystemExit(f"error: missing PTX entry {name}") + + depth = 1 + end = header.end() + + while depth and end < len(ptx): + if ptx[end] == "{": + depth += 1 + elif ptx[end] == "}": + depth -= 1 + end += 1 + + if depth: + raise SystemExit(f"error: unterminated PTX entry {name}") + + return ptx[header.end():end - 1] + +def require_store(body, value, name, label="pre-drop"): + pattern = rf"^\s*st\.global\.b32\s+\[[^\]]+\],\s*{value}\s*;" + store = re.search(pattern, body, flags=re.M) + if store is None: + raise SystemExit( + f"error: {name} lost required {label} store {value}" + ) + return store.end() + +# The PTX adjacency below holds because `opt -O2` inlines the retained glue +# and the destructor into the kernel: `#[inline(never)]` is not propagated as +# `noinline`, as the cluster example's shape check also notes. The +# drop_glue.ll assertion is the one that tracks the importer's own decision; +# this check confirms what LLVM made of the call it kept. +def require_nonreturning_loop(body, after_store, name): + # Both optimized probes lower to a store followed by an unconditional + # self-loop. Tie the loop to that store's continuation: an unrelated + # loop elsewhere in the entry would not prove the drop was preserved. + pattern = r"\s*([\w$.]+):\s*bra(?:\.uni)?\s+\1\s*;" + if not re.match(pattern, body[after_store:]): + raise SystemExit( + f"error: {name} pre-drop store is not followed by an unconditional self-loop" + ) + +def reject_store(body, value, name): + pattern = rf"\bst\.global\.b32\s+\[[^\]]+\],\s*{value}\s*;" + if re.search(pattern, body): + raise SystemExit( + f"error: {name} retained unreachable post-drop store {value}" + ) + +diverging = ( + ("diverging_cfg_drop_probe", "LoopingDrop", 0x11111111, 0x22222222), + ("diverging_recursive_drop_probe", "RecursiveDrop", 0x33333333, 0x44444444), +) + +for name, type_name, before, after in diverging: + require_glue_call(kernel_body(name), type_name, name) + body = entry_body(name) + after_store = require_store(body, before, name) + reject_store(body, after, name) + require_nonreturning_loop(body, after_store, name) + print( + f"{name}: drop_glue::<{type_name}> call kept in drop_glue.ll, " + "pre-drop store followed by non-returning self-loop in drop_glue.ptx PASS" + ) + +# Precision control: an effect-free destructor whose branches join back +# together must still be proven a no-op, so no glue call may appear in the +# kernel and both of its stores survive. +name, before, after = ("reconverging_drop_probe", 0x55555555, 0x66666666) +reject_glue_call(kernel_body(name), name) +body = entry_body(name) +require_store(body, before, name) +require_store(body, after, name, label="post-drop") +print( + f"{name}: no drop glue call in drop_glue.ll, " + "pre-drop and post-drop stores kept in drop_glue.ptx PASS" +) + +print("drop_glue code shape: PASS") +VERIFY_PY diff --git a/cuda-oxide/cuda-oxide-book/compiler/images/drop-proof-termination.svg b/cuda-oxide/cuda-oxide-book/compiler/images/drop-proof-termination.svg new file mode 100644 index 0000000000..c4e27ddac8 --- /dev/null +++ b/cuda-oxide/cuda-oxide-book/compiler/images/drop-proof-termination.svg @@ -0,0 +1,155 @@ + + + + + + + + + +A destructor that never returns is not a no-op +cuda-oxide erases a destructor call when a proof says it does nothing visible. The proof now also demands that the destructor returns. +RUST SOURCE (examples/drop_glue, a compile-only probe) +MAIN (the bug: the call was erased) +PR #1361 (the fix: the call is kept) + +examples/drop_glue/src/main.rs +struct LoopingDrop(u8); + +impl Drop for LoopingDrop { + #[inline(never)] + #[allow(clippy::empty_loop)] + fn drop(&mut self) { + loop {} + } +} + +#[kernel] +pub fn diverging_cfg_drop_probe(mut out: DisjointSlice<u32>) { + if thread::index_1d().get() != 0 { + return; + } + + unsafe { + let slot = out.as_mut_ptr(); + slot.write(0x1111_1111); +store A + + { + let _guard = LoopingDrop(0); +drop: never returns + } + + // Semantically unreachable. + slot.write(0x2222_2222); +store B: must never run + } +} + +What the old proof checked +It walks the destructor's blocks and looks for +visible effects: writes through pointers, asserts, +inline asm. loop {} has none, so the verdict was +harmless: erase the call, lower the drop to a branch. +It never asked whether the destructor returns. +A block seen twice was skipped (a loop looked like +a join), and a call back into a destructor already +under proof was accepted as harmless. + +verdict: no-op. The kernel IR has 0 destructor calls. + +drop_glue.ptx (main backend), thread 0 +$L__BB4_1: // %bb3 + st.global.b32 [%rd1], 572662306; +$L__BB4_2: // %bb5 + ret; +572662306 is 0x22222222: store B ran. +Store A is gone too: once the call between them was +erased, B overwrote A at once and LLVM deleted A. +No loop. The thread returns. + +What the new proof checks +The same walk, depth first, with three states +per block: Unseen, InProgress, Proven. +A successor that is still InProgress is a +cycle: the proof fails and the call is kept. +A Proven successor is a join: skip it, go on. +A call into a destructor that is already +under proof fails the same way. +loop {} fails: bb1 branches back to bb1. + +not proven: the kernel IR keeps the call. + +drop_glue.ptx (PR backend), thread 0 +$L__BB4_1: // %bb3 + st.global.b32 [%rd1], 286331153; +$L__BB4_2: // %bb1.i.i + bra.uni $L__BB4_2; +286331153 is 0x11111111: store A ran. +Then bra.uni to its own label: the thread +spins in the destructor's loop {}, inlined. +Store B is gone, as in the Rust source. + + + +The three states, on two destructors from the example +Depth-first walk from the entry block. A block turns Proven only after every successor is Proven. + +Unseen +not reached yet + +InProgress +on the current path; its exits are not yet proven + +Proven +every exit returns and does nothing visible +Fails: an InProgress block met again, or a call into +a destructor already under proof. Verdict: keep the call. +LoopingDrop::drop +bb0: goto bb1; bb1: goto bb1; + +bb0 + +bb1 + + +goto bb1 again: +still InProgress, a cycle +bb1 is met again before it is Proven. The proof fails, +the destructor call stays, the PTX spins after store A. +RecursiveDrop: the callee is already under proof, same +verdict (858993459 = 0x33333333, then a self-loop). +DiamondDrop::drop +an if/else that joins back; every exit returns + +test + +left_noop + +right_noop + +return + + + + +second visit: +Proven, a join +if self.0 == 0 { left_noop() } else { right_noop() } +return is reached twice; the second visit finds it Proven: a join. +Every path returns and writes nothing, so the drop is still erased. +PTX: two stores (0x55555555, 0x66666666) and ret, on both backends. + diff --git a/cuda-oxide/cuda-oxide-book/compiler/mir-importer.md b/cuda-oxide/cuda-oxide-book/compiler/mir-importer.md index 86fb1d2e7b..d6c3281ade 100644 --- a/cuda-oxide/cuda-oxide-book/compiler/mir-importer.md +++ b/cuda-oxide/cuda-oxide-book/compiler/mir-importer.md @@ -376,6 +376,20 @@ slip through (array bounds checks, unwrap on `None`), a GPU trap is the correct behavior anyway -- there is nothing useful a GPU thread can do to "recover" from a logic error mid-kernel. +Drop glue follows the same rule. The importer erases a destructor call only when +its proof shows that the destructor does nothing visible and returns. A destructor +that loops forever, or calls back into an instance already under proof, keeps its +call, so the code after it never runs, as in the Rust source. + +```{figure} images/drop-proof-termination.svg +:align: center +:width: 100% + +The drop no-op proof requires that the destructor returns. Before, the call to a `loop {}` +destructor was erased and the store after it ran. Now the call stays, so the PTX stores once and +spins, while an `if`/`else` destructor that joins back is still erased. +``` + --- ## Putting It All Together