vLLM

The executable model and oracle correspondence use vLLM 0c87a197. They cover a synchronous scheduling fragment, not every vLLM feature. The source survey below separately examines full-attention scheduling and KV cache in v0.31.0rc2. The oracle does not establish equivalence with that entire version.

Tagged behavior

Scheduler.schedule shares a token budget between resident and waiting requests, using computed progress to determine selected work. Allocation failure triggers victim selection: FCFS and priority paths choose differently. Scheduler

KVCacheManager.get_computed_blocks finds reusable prefixes, while allocate_slots acquires space for scheduled work and lookahead. Identical prefixes can share blocks across requests, requiring more than a session's cached length. KV manager

The scheduler guards whether victim blocks can actually be freed and manages deferred free. AsyncScheduler tracks output placeholders and in-flight results. Releasing or publishing KV before completion can create invalid reuse. Victim/free guard, async scheduler

Executable serQ model

examples/multi-turn/vllm.sq

// vLLM v1 on one device (ref/vllm at 0c87a197, `vllm/v1/core/sched/
// scheduler.py`, `kv_cache_manager.py`, `block_pool.py`), as a serQ
// program. Continuous batching with chunked prefill: every iteration hands
// a token budget to the running requests in admission order (one token per
// decoding request, up to the per-run cap (`each at most`) per prefilling one), then admits waiting
// requests FCFS while the request cap and the KV blocks allow, the first
// that does not fit blocking the rest. KV memory is a block pool with a
// block-level LRU prefix cache: a finished (or preempted) request's full
// blocks stay cached and are evicted tail first when the free queue is
// drained; the next turn of a session reuses its cached prefix (full blocks,
// never the whole prompt). A request grows one block at a time as it
// decodes; when no block is free the most recently admitted request is
// preempted (its blocks freed to the cache, it re-enters the waiting queue
// at the head and recomputes what was lost). See docs/language.md §7 for
// the line-by-line correspondence and how this engine differs from it.
use "../../lib/vllm.sq";

use "std/args";

let B = 8192;          // max_num_batched_tokens
let bs = 16;           // block_size
let a = 2e-5;          // compute per scheduled token (s)
let omega = 2e-4;      // weights read per iteration (s)
let beta = 2e-9;       // KV read per iteration per resident context token (s)
let c0 = 0;            // fixed cost per iteration (s)
let p = 0.9;           // continue after a turn

fn main() {
  let max_seqs = args.number("max_seqs", 16);     // max_num_seqs
  let blocks = args.number("blocks", 10000);    // num_gpu_blocks (less the null block)
  let chunk_cap = args.number("chunk_cap", inf);   // long_prefill_token_threshold (inf: none)
  let Lambda = args.number("Lambda", 0.3);      // sessions per second
  let Z = args.number("Z", 3.0);           // tool time (s)

  device gpu {
    compute (t) = t * a;
    hbm (k) = omega + beta * k;
    kv cap blocks * bs;
  }
  pool kv on gpu { block bs; evict lru; preempt lifo; }
  engine vllm on gpu {
    reqs cap max_seqs;
    tokens cap B;
    // What vLLM does with one request. `known` is every token it has: the
    // prompt, or after a preemption the position it had reached plus the
    // token sampled there, and never fewer than it had before (`kept`: vLLM
    // keeps the generated tokens and drops only their KV,
    // scheduler.py:1560-1561). `reused` is how many of them the prefix cache
    // holds in full blocks; `observe hit` says whether any.
    request (prompt, output) {
      set kept = prompt;
      at admission {
        known = max(kept, computed + 1);
        reused = min(cachedin(kv), reusable(known, blocksize(kv)));
      }
      set kept = known;
      set c = min(cached, reusable(known, blocksize(kv)));
      observe hit = c > 0;                    // any reused block, again after a preemption
      observe prefill_tokens = known - c;
      prefill (known - c) growing kv;
      decode (output - 1 - (known - prompt)) growing kv;
      cache (prompt + output);                // a finished request's blocks stay cached
    }
    schedule {
      // long_prefill_token_threshold binds only while another request is
      // running or waiting; a request alone takes the whole budget (scheduler.py:606-616)
      let threshold = running.count + waiting.count > 1 ? chunk_cap : inf;
      advance running each at most (threshold);
      // A slot of `reqs` and the blocks of `kv`. The scheduler looks up the
      // prefix hit when it admits (scheduler.py:932-939) and allocates the
      // tokens it reuses plus the chunk the budget allows
      // (scheduler.py:1078-1128, 1214-1226), but admits only if every token
      // fits, the reused ones counted
      // (scheduler_reserve_full_isl, on by default: config/scheduler.py:191,
      // kv_cache_manager.py:515-531): the `reserve`.
      // docs/language.md §7 "Admission" has the argument.
      admit waiting while (running.preempted == 0) each at most (threshold)
        taking reqs (1), kv (min(known, reused + budget_left(vllm))) reserve (known);
    }
    execute (c0 + max(hbm(batch.kv_decode + batch.kv_prefill), compute(batch.tokens)));
  }
  pool reqs on vllm { queue fifo; }   // the engine admits the waiting, FCFS

  // The client: sessions arrive, each turn brings a prompt of n new tokens
  // on a context of K and wants o tokens back, and after a turn the session
  // calls a tool and comes back with probability p. Nothing here is vLLM.
  workload {
    arrive poisson(Lambda);
    hidden o;              // the scheduler knows max_tokens, not the length (sched/utils.py:98-119)
    init { set K = 0; }
    turn {
      set n = ceil(K == 0 ? ~uniform(1000, 3000) : ~exp(500));
      set o = floor(~exp(200)) + 1;
      set more = ~bernoulli(p);
    }
    session {
      turn;
      while (more) {
        set K = K + n + o;
        tool (~exp(Z));
        turn;
      }
    }
  }

  // A turn is one request to the engine.
  server {
    set prompt = K + n;
    vllm (prompt, o);
  }
}

The program's definition reusable is a library the other vLLM programs share:

lib/vllm.sq

// vLLM v1 (ref/vllm at 0c87a197, `vllm/v1/core/sched/scheduler.py`,
// `kv_cache_manager.py`, `block_pool.py`): the rule a program states as an
// expression, `use "…/lib/vllm.sq";`. docs/language.md §7 has the
// line-by-line correspondence, for `examples/replay/vllm_replay.sq`.

// What a cache hit may cover of a request of x tokens: its full blocks of
// `bs` tokens, and never the last token, which is computed for its logits
// (kv_cache_manager.py:289-300).
def reusable(x, bs) { floor((x - 1) / bs) * bs }

Requirement	Current expression	Limit of the model
Token budget and chunked prefill	engine … { tokens cap …; schedule { … each at most (…); } }	Resident selection then waiting admission is a specific policy
Request slots and KV space	hold, admission bindings, reserve, growing	Tagged fit/lookahead conditions are not fully validated
FCFS/priority	Queue order and preempt lifo; PRIORITY is preempt by (-priority, -t0) requeue tail beside queue by (priority, t0)	No oracle scenario checks the PRIORITY victim
Shared prefix	cachedin, reuse, cache	Cache identity is session-based, not content-key shared objects
Local decode preemption	computed-aware known in the server block	Latest-tag recovery paths need differential validation
Async and speculative execution	Cost expressions, explicit leases/transfers	In-flight scheduler state and proposed/accepted progress remain absent

Validation

The vLLM correspondence records the existing scheduler scenarios and trace. Those checks apply to their stated reference and paths, not to every feature of v0.31.0rc2.

See vendor plugins for the reference versions, executable model and remaining limitations.

Measured replay

examples/replay/vllm_replay.sq models the A100/Qwen3-8B testbed using examples/replay/data/short_base.csv (333 sessions). It uses block size 16, token budget 512, 64 request slots and 128 160 tokens of KV capacity. Session i starts at i * spacing; later turns follow their recorded think times. This is a separate calibration from the tagged-source survey above.

Cost and calibration

tools/a100/step_fit.json records a fit to 3 022 measured steps:

cost = c + d * decoders + e * kv_decode + a * prefilled + b * attention

Coefficient	Value
c	13.9 ms
d	41 µs
e	0.138 µs
a	51.5 µs
b	4.02 ns

The fit's mean absolute percentage errors are 2.7% for decode, 5.6% for prefill and 5.7% for mixed steps. For served-path replay, two light-load runs calibrated c_it = 4 ms per step and c0 = 40 ms per request. These are effective parameters: those runs do not uniquely identify the split between per-step and per-request overhead.

Reported comparison

Session spacing	Policy	Predicted mean TTFT	Measured mean TTFT
3.0 s	Unpinned waiting prefixes	0.605 s	0.441 s
2.5 s	Unpinned waiting prefixes	39.1 s	34.6 s
2.5 s	Pinned waiting prefixes	0.888 s	0.878 s

The pinning prediction preceded its measurement. Each point is one run; the two 2.5 s measurements were made on different days, and only the pinned run carried a step tracer. The run records are not published; the scripts are in serving-queue-theory/scripts/exp/. This table records that comparison, not a reproducible benchmark shipped with this repository.