← All papers
First page of A Tight Linear Deterministic Competitive Ratio for Fully Online KV-Cache Scheduling

A Tight Linear Deterministic Competitive Ratio for Fully Online KV-Cache Scheduling

Ian D'Ambrosio

cs.DS Aug 14, 2026 · v1
Lean 4 with Mathlib machine-checks the model, causality argument, comparator schedules, and quantifier order for the KV-cache scheduling competitive-ratio bounds.
Jaillet et al. introduced a fully online model for batching nonpreemptive LLM requests under a growing KV-cache memory constraint. For total end-to-end latency they proved that every deterministic algorithm has competitive ratio Omega(sqrt(n)), while the elementary sequential upper bound is n. We close this gap. Let R_det(n,M) be the optimal deterministic ratio for exactly n requests at memory M, and let R_det(n)=sup_M R_det(n,M). For every n >= 2 we prove (n-1)/12 <= R_det(n) <= n, so R_det(n)=Theta(n). The lower bound releases one memory-filling long request, observes its deterministic start time, and then releases n-1 wide one-token requests halfway through the long run. No short request can overlap the long one, whereas a hindsight schedule runs the two groups in the opposite order when useful. The hard instance uses the explicit fixed memory M=2(n-1)n. The upper bound is achieved by a uniform causal serial policy. The exact model, causality argument, both comparator branches, and quantifier order are machine-checked in Lean 4. Exact finite controls and replay commands accompany the proof.

Jaillet et al. proved that every deterministic algorithm for fully online nonpreemptive KV-cache batching under a growing memory constraint has competitive ratio Omega(sqrt(n)) for total end-to-end latency, while the trivial serial upper bound is n, leaving a polynomial gap.

The optimal deterministic ratio R_det(n) is bounded from above by a uniform causal serial policy and from below by a hard instance using fixed memory M=2(n-1)n. The lower bound releases one memory-filling long request, observes its deterministic start, then releases n-1 wide one-token requests halfway through, so no short request can overlap the long one while a hindsight schedule reorders them. The exact model, causality argument, both comparator branches, and quantifier order are machine-checked in Lean 4 with Mathlib.

For every n >= 2, (n-1)/12 <= R_det(n) <= n, establishing R_det(n)=Theta(n) and closing the gap. The audited Lean declaration relies only on the standard axioms propext, Classical.choice, and Quot.sound, and 30 focused tests plus exact finite controls replay successfully.