vLLM Formally Verified Sliding-Window Prefix Cache Optimization

Project Summary

Formally verified and implemented an O(N/W + W) stride jump search for sliding-window prefix caching in vLLM V1. The algorithm replaces an O(N) backwards linear scan. It reduces CPU scheduler stalls by up to 61.3x across models released post-June 2026. Machine-checked proofs in Lean 4 prove soundness, boundary safety, and prefix fallback correctness with zero sorry axioms. Upstream contribution submitted to vllm-project/vllm as Pull Request #65086.

1. Problem Statement

In vLLM V1 (single_type_kv_cache_manager.py), sliding window attention models require locating the rightmost contiguous run of at least W (sliding_window_contiguous_blocks) cached KV blocks.

The legacy implementation performed an O(N) linear loop scanning backwards block by block from max_num_blocks - 1 down to 0:

# Legacy linear scan
for i in range(max_num_blocks - 1, -1, -1):
    if cached_block := block_pool.get_cached_block(block_hashes[i], ...):
        ...

Critical Bottlenecks:

1. CPU Scheduler Starvation: At 128K context (8,192 blocks), a single request performed 8,192 sequential Python hash lookups. Under concurrent batch serving, the single-threaded CPU engine stalled for hundreds of milliseconds, leaving GPUs idle.
2. Prior Failed Attempts: Prior attempt PR #63798 attempted stride probing. However, heuristic boundary expansion caused off-lattice cache misses and corrupted prefix fallback with NULL block leaks.
3. Open Maintainer Debt: Upstream maintainers explicitly marked line 1002 with # TODO: reduce i by sliding_window_contiguous_blocks when cache miss.

2. Algorithm Architecture

flowchart TD
    A["Candidate Window: [e - W, e)"] --> B{"Probe Anchor Block p = e - W"}
    B -- "Miss" --> C["Jump e <- e - W (Skip W blocks in 1 probe)"]
    C --> A
    B -- "Hit" --> D{"Probe Inner Blocks k in [e-1 .. p+1]"}
    D -- "Miss at k" --> E["Jump e <- k (Skip invalid window run)"]
    E --> A
    D -- "All Hit" --> F["Full Window Hit Found: Return [e - W, e)"]
    A -- "e < W (No window hit)" --> G{"Forward Prefix Fallback"}
    G --> H["Scan k in [0 .. W-1] until miss: Return Contiguous Run"]

Invariant Principles:

1. Anchor Probing: For a window of length W ending at e, index $p = e - W$ is mandatory. If index p is a cache miss, no window ending in $[e - W + 1, e]$ can be valid. The candidate end safely jumps e \leftarrow e - W.
2. Inner Probing: When anchor p hits, verify remaining blocks from right to left ($e - 1$ down to $p + 1$). If index k misses, jump candidate end e \leftarrow k.
3. Sound Prefix Fallback: When $e < W$, probe forward from index 0. If block 0 misses, exit in 1 lookup. Real prefix hits align cleanly without uninitialized block leakage.

3. Formal Verification in Lean 4

The algorithm was modeled and verified in Lean 4 (lean_prefix_cache/LeanPrefixCache.lean) with zero axioms (sorry).

Formal Specification: ValidWindow

def ValidWindow (cache : Array Bool) (w : Nat) (s e : Nat) : Prop :=
  e - s ≥ w ∧ e ≤ cache.size ∧ ∀ (i : Nat), s ≤ i → i < e → ∃ (h : i < cache.size), cache[i] = true

Proven Theorems:

1. Soundness (strideSearch_sound):

   theorem strideSearch_sound (cache : Array Bool) (w : Nat) (s e : Nat) :
       strideSearch cache w = some (s, e) → ValidWindow cache w s e

   Guarantees that every returned window $[s, e)$ has length ≥ W and contains only valid cached blocks.

2. Boundary Safety (strideSearch_boundary_safety):

   theorem strideSearch_boundary_safety (cache : Array Bool) (w : Nat) (s e : Nat) :
       strideSearch cache w = some (s, e) →
       e ≤ cache.size ∧ (∀ i : Nat, s ≤ i → i < e → i < cache.size)

   Guarantees no out-of-bounds indices are dereferenced or returned.

3. Prefix Fallback Soundness (prefixFallback_correct): Guarantees maximal prefix extraction without NULL block table corruption.

The project compiled to a C shared library (libprefix_cache_lean.so) and passed 1,000 property-based random tests via C FFI.

4. Empirical Performance Benchmarks

4.1 CPU Scheduler Microbenchmarks (PR Stride Jumping)

Evaluated on official Hugging Face checkpoints released post-June 2026 using vLLM BlockPool at 5% sparse cache hits:

4.2 Live End-to-End GPU Generation on AMD Instinct MI50

Validated live multi-token inference on physical AMD Instinct MI50 hardware (32 GB HBM2, gfx906, ROCm 7.14 / PyTorch 2.13):

Benchmark A: cyankiwi/Qwen3.8-27B-AWQ-INT4 (27B Post-June 2026 Model)

• Architecture: Qwen3_5ForConditionalGeneration (Hybrid attention + linear attention SSM, mamba cache mode: align, page size 1024 tokens).
• Quantization: 4-bit compressed-tensors (format: pack-quantized, 19.6 GB on disk).
• GPU Resource Utilization: Single AMD Instinct MI50 (31.96 GB VRAM free, gpu_memory_utilization=0.75).
• Cold Uncached Run: 9.8493 s total latency (809 prompt tokens, 64 generated tokens, 6.50 tokens/sec end-to-end).
• Warm Prefix-Cached Batch: 47.8147 s for 9 batched queries (7,298 prompt tokens processed, 266 generated tokens, 5.56 tokens/sec aggregate throughput).

Benchmark B: Qwen/Qwen3-8B-AWQ (Dense 8B Model)

• Architecture: Qwen3ForCausalLM (36 hidden layers, max sequence length 40,960).
• Quantization: 4-bit AutoAWQ GEMM (5.8 GB on disk).
• GPU Resource Utilization: AMD Instinct MI50 (gpu_memory_utilization=0.35).
• Cold Uncached Run: 4.1078 s total latency (547 prompt tokens, 64 generated tokens, 15.58 tokens/sec end-to-end).
• Warm Prefix-Cached Batch: 10.8766 s for 9 batched queries (4,943 prompt tokens processed, 576 generated tokens, 52.96 tokens/sec end-to-end).
• End-to-End Throughput Speedup: 3.40x faster with prefix caching hit on dense attention.

Benchmark C: Physical Cluster Job Algorithmic Scaling (PR #65086 vs Upstream Baseline)

Evaluated directly inside the k3s MI50 container pod (vllm-live-gpu-bench):

5. Upstream PR & Verification Status

• PR Link: vLLM PR #65086
• Branch: perf/stride-sliding-window-prefix-cache (0 commits behind upstream/main)
• Reviewers Assigned: Woosuk Kwon, Robert Shaw, Nick Hill, Roger Wang, and 6 core maintainers.
• Review Feedback Addressed: GitHub Copilot review comments resolved with new regression tests (test_sliding_window_stride_jump_inner_miss_and_off_lattice_window and test_sliding_window_dropped_eagle_block_fallback_alignment).
• All Local Tests: 52/52 pytest tests pass; 15/15 pre-commit hooks pass.