M2K: Making the Model-Kernel Interface Explicit for Reliable CUDA Kernel Verification

Mengting He; Shihao Xia; Haomin Jia; Wenfei Wu; Linhai Song

cs.PLMar 6, 2026

M2K: Making the Model-Kernel Interface Explicit for Reliable CUDA Kernel Verification

Authors: Mengting He, Shihao Xia, Haomin Jia, Wenfei Wu, Linhai Song

Organizations: Penn State, USA · SKLP, ICT, CAS, China · Peking University, China

Abstract

Large language model (LLM) inference systems rely on CUDA kernels for core GPU computations, yet the interface between models and kernels is implicit and poorly specified. Models and kernels evolve independently and often make incompatible assumptions about tensor shapes and input sizes, leading to subtle memory bugs in CUDA kernels. These bugs can crash inference services, corrupt model weights, or be exploited by remote adversaries. Existing techniques either incur prohibitive runtime overhead, require specialized hardware, or fail to handle dynamic tensor shapes and variable kernel launch configurations, leaving the CUDA memory bugs largely unaddressed. This paper presents M2K, a fully automated framework that makes the model-kernel interface explicit and leverages it to detect memory bugs in CUDA kernels used in LLM inference systems. M2K consists of two components. HFProbe traces model execution without GPU hardware, classifies kernel arguments into model-fixed and user-variable, and emits symbolic constraints that capture the interface. cuKLEE then performs symbolic execution on CUDA kernels to pinpoint memory bugs under the interface constraints, modeling tensors as disjoint memory regions and treating thread identifiers symbolically to scale to thousands of threads. In the evaluation, M2K discovers 181 previously unknown bugs in real LLM inference systems, while producing only nine false positives, demonstrating its effectiveness.

Figures & tables

Panel of Figure 2 — Figure 2. A CUDA kernel example, its wrapper function, its registration to vLLM, and a Hugging Face model using the kernel.

Dimension	Breakdown	Count
How discovered	User-reported (production failure)	13
	Unit test	6
	Code review	1
Memory location	GPU global memory (tensors)	17
Memory location	GPU shared memory	3
Bug type	Integer overflow $\rightarrow$ buffer overflow	10

Table 1. Summary of 20 kernel memory bugs in vLLM.

Tensor Fields	Description	Variables
t.storage_.data_ptr_	base address	$B_{t}$
t.numel_	# of elements	$N_{t}$
t.sizes_and_strides_.size_	# of dimensions	$D_{t}$
t.sizes_and_strides_	dimensions	$d_{t}^{0}$ , $d_{t}^{1}$ , … $d_{t}^{D-1}$
t.data_type_.itemsize_	element size	$S_{t}$

Table 2. Constraint variables defined for tensor t .

Category	Tensor Methods	Constraints
I	t.numel()	$N_{t}$
I	t.data_ptr()	$B_{t}$
II	t2=t1.sum(0)	$N_{t2}=N_{t1}/d^{0}_{t1}$ , $D_{t2}=D_{t1}-1$ , $S_{t2}=S_{t1}$ , $d^{0}_{t2}=d^{1}_{t1}$ , …, $d^{D-1}_{t2}=d^{D}_{t1}$
III	check_dim_size (t, n, i, exp)	$D_{t}=n$ , $d^{i}_{t}=exp$
IV	t.toString()	-

Table 3. Tensor-method handling examples. (’-’: ignored.)

Variables	Description	Type
$blockIdx.x/y/z$	block identifier	ID
$threadIdx.x/y/z$	thread identifier	ID
$gridDim.x/y/z$	grid size	launch
$blockDim.x/y/z$	block size	launch

Table 4. Constraint variables defined for CUDA threads.

	Models	Kernels	IO	OOB	DR	NULL	Total
vLLM	$62$	$50$	$7_{2}$	$19_{5}$	$0_{2}$	-	$26_{9}$
HF	$54$	$117$	$131_{0}$	-	-	-	$131_{0}$
Papers	$4$	$6$	$24_{0}$	-	-	-	$24_{0}$
Total	$120$	$173$	$162_{2}$	$19_{5}$	$0_{2}$	-	$181_{9}$

Table 5. Benchmark information and detection results. ( IO: integer overflow, OOB: out-of-bounds, DR: data race, and NULL: null-pointer dereference.

x_{y}

: x true positives, y false positives. ’-’ indicates zero true and false positives.)

Figure 5. How the number of bugs changes with GPU memory. (The vertical line represents NVIDIA B300.)

	Honeycomb	GKLEE	ESBMC-GPU	cuKLEE
vLLM	/	/	/	15
Simplified	0	5	3	19

Table 6. Comparison with baseline techniques. (20 bugs are for each row. ‘/’: not applicable.)

Figure 7. Contributions of M2K’s components. (26 bugs detected in vLLM. W.O.: without, C: cuKLEE, H: HFProbe, M: configuration mutation, and V: Validation.)

GPU Kernel Correctness Verification

See all 14 papers

AutoMegaKernel: A Statically-Checked Agent Harness for Self-Retargeting Megakernel Synthesis
Jun 8, 2026Jaber Jaber, Osama JaberGPU Kernel Optimization High-Performance Computing
RightNow AI
CUDABeaver: Benchmarking LLM-Based Automated CUDA Debugging
May 8, 2026Shiyang Li, Haoyang Chen, Mattia Fazzini +1LLM Evaluation Automated Program Repair
University of Minnesota
From Tokens to Regions: CUDA-Sensitive Instruction Tuning for GPU Kernel Generation
Jun 15, 2026Wentao Chen, Jiace Zhu, Xing Zhe Chai +4GPU Kernel Optimization LLM Fine-Tuning
1Shanghai Jiao Tong University · 2Biren Technology

Jun 8, 2026J/K move · Enter open · S save

AutoMegaKernel: A Statically-Checked Agent Harness for Self-Retargeting Megakernel Synthesis

Jaber Jaber, Osama Jaber

RightNow AI

GPU Kernel Optimization High-Performance Computing LLM Inference Acceleration GPU Kernel Generation Neural Network Hardware Acceleration

Open paper AskPDF arXiv

AutoMegaKernel (AMK) compiles a HuggingFace Llama-family model into a single persistent cooperative CUDA kernel that runs the whole forward pass in one launch, with no per-model hand-written CUDA. The contribution is the system, not raw speed. A frozen schedule-IR validator statically certifies deadlock-freedom and race-freedom via static graph checks (not a mechanized proof), so an unsafe agent-proposed schedule is rejected before launch: across 7,160 adversarial schedules (6,091 unsafe) it had zero false-accepts and accepted all 360 real lowerings. The same source retargets sm_80/sm_90/sm_120 from one codebase, auto-generates correct megakernels for 10 of 10 supported models, and on a real SmolLM2-135M checkpoint reproduces HuggingFace greedy decode token-for-token (perplexity match 2.5e-7). An unattended, agent-drivable autoresearch loop self-improves the megakernel over its own baseline (1.25-1.72x). A search-found int8 (W8A16) megakernel beats CUDA-graphed cuBLAS bf16 at batch-1 decode across NVIDIA's datacenter inference fleet: L4 up to 1.33x, the current-gen L40S 1.25-1.27x, A10G up to 1.08x at scale, and the consumer RTX 5090 1.19-1.23x. The ordering is not a clean function of bandwidth (the 864 GB/s L40S beats the 600 GB/s A10G); the divide is inference-class vs training-class. AMK trails cuBLAS on the high-bandwidth training-class A100/H100, where the harness localizes the cross-SM-sync bottleneck; we report the gap plainly. This is a precision-asymmetric (W8A16 vs bf16) comparison at decode position 0; the largest real checkpoint is TinyLlama-1.1B. Code and the harness: https://github.com/RightNow-AI/AutoMegaKernel

Abstract

GPU Kernel Correctness Verification

Explore similar work

AutoMegaKernel: A Statically-Checked Agent Harness for Self-Retargeting Megakernel Synthesis

CUDABeaver: Benchmarking LLM-Based Automated CUDA Debugging

From Tokens to Regions: CUDA-Sensitive Instruction Tuning for GPU Kernel Generation