serQ v0.1.4

IR v12 separates workload Size values from resource-bound Cost values. Workloads specify request sizes; servers convert sizes with cost(resource, amount). Primitive run/hold/grow/load operations require costs for their target resources. Explicit Size and Cost declarations and multi-resource Cost records lower to scalar IR costs; serving vocabulary performs the conversion.

IR readers must regenerate older programs: attr_types and sides are mandatory. While is part of IR v12; turn now draws the next request and waits for its server to complete, replacing request in client sessions without resetting RNG streams. The Lean generator and oracle vectors consume this version together.

This release also fixes aggregate expression validation stack overflow. See the language and IR specifications for migration details.

What's Changed

• feat(lang): serQ as a serving specification language, with a vLLM target by @vrvrv in #350
• docs(site): simplify reader documentation and theorem presentation by @vrvrv in #380
• docs(site): clarify capabilities and verification scope by @vrvrv in #381
• feat(frontend): add explicit main and declared program inputs by @vrvrv in #383
• docs(api): organize Python and language reference entries by @vrvrv in #384
• refactor(frontend)!: require workload sessions and request handlers by @vrvrv in #382
• docs(guide): document and apply program organization conventions by @vrvrv in #385
• refactor(frontend)!: use braces for expression definitions by @vrvrv in #387
• refactor(frontend)!: separate execution settings from models by @vrvrv in #386
• docs(examples): standardize resource and observation names by @vrvrv in #389
• feat(workload): express sessions as completed turns by @vrvrv in #388
• feat(types)!: separate workload sizes from resource costs by @vrvrv in #390
• chore(release): prepare v0.1.4 by @vrvrv in #391

Full Changelog: v0.1.3...v0.1.4

serQ v0.1.3

IR 11 is first tagged in this release. Regenerate IR from source when moving from v0.1.2 (IR 10); update downstream readers and re-record seeded simulation results.

A seed now names a workload: init and turn draws use streams keyed by (seed, session, turn), statement draws by (seed, session), independently of scheduling. Seeded numbers change. Deterministic oracle schedules and the prefix-cache trace remain unchanged.

The iteration is programmable: CStep.iteration contains Serve, Admit, Branch and Set operations; Program.registers and CExpr::Reg give stages state between iterations. The former CStep.only field is removed: serve only compiles to an iteration body. Serve keys read the current resident totals, including requests admitted in that iteration. Preempt::Lifo is replaced by By {keys, tail}; preempt lifo compiles to the equivalent key and head requeue. Victim keys can read position, admission and decoding. CPool.reserve_held keeps a reservation until its hold ends, CStep.granule constrains prefill allocation, and CStmt::Fork/Join express concurrent request legs.

A state-dependent hold or reservation waits instead of being rejected at queue entry; an over-cap head at run end is reported. A preempted hold caches its computed position rather than an uncomputed allocation. Validation rejects invisible context reads, unsafe hold indices and loops that cannot advance time; invalid amounts and indices, non-settling instants and zero-cost token iterations fail loudly.

Claims state mechanically checked properties of runs, with aggregates and demand, served and arrived contexts. The Lean model and generated claims now connect the paper programs to Dai, Bari and Kong results, including Poisson drift and recurrence results. The Lean fragment follows expression-dependent chunks and the LIFO encoding. Arbitrary iteration bodies, registers, reserve held, granules and fork/join remain outside it; the generators reject unsupported programs. The claims generator accepts the serve-only body it knows.

The examples exercise the new iteration, reservation, victim and granule mechanisms. pyserq adds deployment drawing. CLI, Python wheels and the Serq Lake package share this release; downstream consumers should pin v0.1.3 together.

What's Changed

• feat(lang): the stochastic-process definition and the four rules it asked for by @vrvrv in #256
• fix(lang): the re-ready bound is per session, a hold's header may not draw by @vrvrv in #259
• docs(claude): ask why a bug happened and whether a check should refuse it by @vrvrv in #266
• feat(lang): serve only (p), and FasterTransformer as a use case by @vrvrv in #263
• feat(draw): draw what one request runs, not the workload's choices by @vrvrv in #264
• fix(lang): grow and growing need an enclosing hold of their pool by @vrvrv in #281
• fix(ir): budget_left needs a step stage by @vrvrv in #283
• fix(lang): a renewal gap must be a positive time, and not a panic by @vrvrv in #285
• fix(ir): a constant hold larger than every cap it may name does not link by @vrvrv in #287
• fix(ir): a poisson rate must be positive and finite by @vrvrv in #288
• docs(pyserq): the install section is the two pip lines by @vrvrv in #292
• feat(pyserq): draw, the deployment view as serq draw prints it by @vrvrv in #291
• fix(examples): the vLLM programs admit through the engine, as vLLM does by @vrvrv in #294
• fix(ir): a step's budget does not read budget_left by @vrvrv in #299
• fix(examples): the vLLM programs draw whole token counts by @vrvrv in #298
• fix(interp): a negative or NaN amount and a bad index are errors, not 0 by @vrvrv in #290
• refactor(ir): one CExpr walk, which a static eviction key no longer skips by @vrvrv in #300
• fix(lang): the parser folds an aggregate, so its let sizes an array by @vrvrv in #301
• refactor(interp): return what is removed, flag a preemption, one tolerance by @vrvrv in #302
• fix(lang): an arrival count is a whole number in range, not a cast by @vrvrv in #303
• refactor(interp): a hold's pools are structs, and one search finds the innermost by @vrvrv in #306
• docs(nav): pyserq is a top-level page beside the CLI reference by @vrvrv in #308
• fix(ir): validate checks what the interpreter assumes the linker checked by @vrvrv in #307
• test(interp): check that pools conserve what sessions hold, in a debug run by @vrvrv in #311
• feat(lang): claims, and three papers' propositions proved in Lean by @vrvrv in #304
• fix(ir): a hold whose body sets its index does not grow, load or release by it by @vrvrv in #312
• refactor(frontend): one draw walk and one substitution, on Expr by @vrvrv in #316
• fix(ir): a hold takes each pool once by @vrvrv in #315
• feat(lang): a validate error points at its statement's line by @vrvrv in #318
• fix(ir): a hold a pool may preempt reads no index that moves by @vrvrv in #319
• docs(site): a home page that says what serQ is for, and tabs by @vrvrv in #314
• docs(language): only what is true today, and shorter by @vrvrv in #320
• feat(lang): an iteration claim reads arrived, and Dai Theorem 2(b) pathwise by @vrvrv in #324
• feat(lean): Foster's criterion on a finite-support kernel by @vrvrv in #325
• docs(brand): the serQ logo in the README and on the site by @vrvrv in #321
• docs(use-cases): Bari Theorem 2 waits on the kernel, not on Foster by @vrvrv in #327
• fix(interp): a served resident preempted in its iteration leaves it by @vrvrv in #322
• fix(lang): vLLM caps a prefill only while another request is eligible by @vrvrv in #323
• feat(lean): a program with random arrivals as a Markov kernel, and Dai Theorem 2(b) on it by @vrvrv in #332
• feat(lean): Bari Theorem 2 on the kernel by @vrvrv in #333
• docs(getting-started): say that serQ runs from Python too by @vrvrv in #335
• fix(lang): an override refused on IR names what it overrides, not a flag by @vrvrv in #336
• refactor(view): one place maps a format name to its writer by @vrvrv in #338
• fix(interp): a preempted hold caches what it computed, not what it was allocated by @vrvrv in #340
• fix(lang): override errors speak of the let or def, not the CLI flag by @vrvrv in #341
• feat(lean): positive recurrence of Dai's and Bari's chains by @vrvrv in #342
• refactor(lean): a step's chunk is a function of the program's expression by @vrvrv in #343
• docs(language): a served victim caches its position, by choice by @vrvrv in #344
• fix(lean): DaiSim and BariSim name the chunk field chunkAt by @vrvrv in #346
• refactor(lean): one translator of IR expressions, with a leaf per moment by @vrvrv in #348
• ci: run on a merge queue's groups by @vrvrv in #349
• refactor(lean): the step lemmas of the semantics in one module by @vrvrv in #351
• refactor(lean): one slot invariant for DaiStable and BariStable by @vrvrv in #352
• feat(lean): Foster's drift for Poisson arrivals in Dai et al. and Bari et al. by @vrvrv in #359
• feat(lean): Bari et al. over g nodes with the random planner by @vrvrv in #358
• refactor(lean): the paper proofs beside the paper programs by @vrvrv in #361
• feat(lean): Kong Theorems 3.4 and 3.5, with Harris's inequality by @vrvrv in #353
• docs(design): engine neutrality, SGLang, TensorRT-LLM and TGI as serQ programs by @vrvrv in #354
• feat(ir): preempt by (keys) requeue head|tail, the victim a program chooses by @vrvrv in #360
• feat(ir): a step stage's iteration as a program body by @vrvrv in #362
• feat(ir): a step stage's registers, state NAME = c set by its body by @vrvrv in #367
• fix(interp): a reserve that reads the state waits instead of being rejected by @vrvrv in #369
• refactor(ir): a stage's serve only (p) is an iteration body; CStep.only removed by @vrvrv in https://github.com/servingQ/serQ/pull...

serQ v0.1.2

IR version 10, as v0.1.1: no change to the IR or to what the interpreter does (one comment changed). This release brings the Lean model of the language into this repository and makes it the interpreter's.

The Lean model is the Serq package in lean/ (#245, docs/lean.md): syntax and pool semantics, the executable semantics Exec, the serving order, and the vLLM scenarios of tools/oracle/ as theorems generated by scripts/gen_lean_oracle.py; make lean checks it. Another Lake project requires it at a tag (serving-queue-theory does).

Exec is event-driven like the interpreter, events in (time, event number) order, with an iteration cost affine in tokens, prefilled, decoders, kv_decode and attention (#247, #248). Differential random testing against the interpreter (make drt, CI: 200 random cases and the 333-session trace with the whole A100 cost fit) found three differences in the Lean semantics, now fixed: a run of zero work yields, settle and a hold's end admit as the interpreter does (#249), and a preemption takes the engine resident admitted last and sets computed (#250); tests/lean-regress/ holds them as generated theorems. serq-lean-bench runs Exec on a workload (#246); the compiled code evicts an entry's blocks at once, proved equal to the definition (makeRoomFast_eq, @[csimp]).

Serq/Fill.lean proves that an iteration of the step engine is the greedy fill of its budget in serving order (#252, assign_iter_eq_fillIter, fillAmounts_fifo, fillAmounts_sum), the property a FIFO prefill queue needs from the engine.

What's Changed

• feat(lean): move the Lean model into serQ as the Serq package by @vrvrv in #245
• perf(lean): serq-lean-bench, and Exec fast enough to replay the trace by @vrvrv in #246
• feat(lean): event-driven Exec with an iteration cost by @vrvrv in #247
• feat(lean): kv_decode and attention in the iteration cost by @vrvrv in #248
• fix(lean): a run of zero work yields, as in the interpreter by @vrvrv in #249
• fix(lean): a preemption picks the interpreter's victim and leaves computed by @vrvrv in #250
• test(lean): differential random testing against the interpreter, in CI by @vrvrv in #251
• feat(lean): an iteration of the step engine fills its budget in serving order by @vrvrv in #252
• chore(release): v0.1.2, IR 10 by @vrvrv in #255

Full Changelog: v0.1.1...v0.1.2

serQ v0.1.1

IR version 10 (#234): the cache clause is what admits a hold to the prefix cache. A hold without it leaves the session's cached blocks where they are and reads cached as 0, where 9 consumed the entry at every admission, so a reservation written around the request's hold on the same pool cost the request its hit. cache (0) is the 9 meaning (consume, keep nothing); a cached read or a reuse in a hold without cache is a link error. Companion: serving-queue-theory's gen_serq_oracle.py pins 10 and SerqExec.lean's admit consumes only with cache.

The linker rejects a session attribute or a let named like a context variable (#235): set present = … made ps(min(present, 16)) read the attribute.

serq --version, and run --json records serq_version (#236; pyserq Report.serq_version). The text report notes a test observe (a comparison, &&, ||, !) that was 0 over 40 or more samples (#240). lib/vllm.sq says what hit counts (#239).

Since v0.1.0 also: queue, the gateway, prefill, link and decode as the roles of one queue (#87), a pod's NIC and D pull P latency x share s (#207), a link's serve latency (#196); gauge, the time average of a function of the state (#204); the laws a caller varies are named defs in the examples (#192), --def; the report tells an array's members apart by index (#213, #217), reports a step stage's batches (#210) and the gaps between a turn's tokens (#222), and compares colocated vs split engines (#210, #233); draw boxes an instance (#197), starts a deciding turn at a decision node (#199) and draws a pool held at one station in it (#224); vllm-rbln keeps vLLM's prefix cache and preemption (#226); the P/D batching baseline's variations (#227); a def's request captures only what its gateway assigns (#209); a queue family of one is a family (#215); the case studies are Use cases (#221).

What's Changed

• docs(readme): release badge from PyPI by @vrvrv in #190
• refactor(examples): the laws a caller varies are named defs by @vrvrv in #192
• feat(parser): queue — gateway, prefill, link and decode as the roles of one queue (RFC #72) by @vrvrv in #87
• feat(parser): a link's serve takes a latency, a wait before every transfer over it by @vrvrv in #196
• feat(draw): an instance is a box, and a transfer between two crosses between them by @vrvrv in #197
• feat(draw): a turn that decides first starts at a decision node, and comes back to it by @vrvrv in #199
• feat(parser): a pod owns its nic, and 'D pull P latency x share s;' is its read by @vrvrv in #207
• feat: gauge, the time average of a function of the deployment's state by @vrvrv in #204
• fix(parser): a def's request captures only what its gateway assigns by @vrvrv in #209
• feat(report): tell an array's members apart by index by @vrvrv in #213
• chore(claude): design-reviewer and sim-reviewer subagents for when Copilot is at its limit by @vrvrv in #212
• fix(report): a one-member array keeps its index by @vrvrv in #217
• feat(parser): a queue family of one is still a family, called by index by @vrvrv in #215
• feat(report): a step stage reports its batches, and colocated vs split engines are compared by @vrvrv in #210
• docs: fold the case studies into Use cases by @vrvrv in #221
• feat(draw): a pool held at one station is drawn in that station by @vrvrv in #224
• fix(examples): vllm-rbln keeps vLLM's prefix cache and preemption by @vrvrv in #226
• fix(interp): a hold without cache leaves the session's prefix where it is by @vrvrv in #234
• feat(report): a step stage reports the gaps between a decode's tokens by @vrvrv in #222
• fix(link): a context variable's name cannot be an attribute or a constant by @vrvrv in #235
• feat(cli): serq --version, and the report records serq_version by @vrvrv in #236
• docs(lib): say what vllm.sq's hit counts, and when by @vrvrv in #239
• feat(examples): the variations of the P/D batching baseline, one at a time by @vrvrv in #227
• feat(tools): colocated vs split on llm-d's deployment, open and closed by @vrvrv in #233
• feat(report): a test observe that never held is noted by @vrvrv in #240
• chore(release): v0.1.1, IR 10 by @vrvrv in #242

Full Changelog: v0.1.0...v0.1.1

serQ v0.1.0

The first release. serQ and pyserq are one version, X.Y.Z; licensed Apache-2.0.

pyserq is on PyPI: pip install pyserq (linux x86_64, macOS arm64; Python 3.9+, abi3). Every commit on main that passes CI is published as a dev release of the next patch (pip install --pre pyserq, e.g. 0.1.1.dev3) (#188). pyserq.Rng is the generator a run draws from (#185).

--def name=expr gives an expression definition its body from outside (#186). A NaN constant's error keeps the expression's place (#184).

IR version 9, as in v0.1.0-rc7.

What's Changed

• chore(release): v0.1.0, licensed, pyserq on PyPI by @vrvrv in #188

Full Changelog: v0.1.0-rc8...v0.1.0

serQ v0.1.0-rc8

--def NAME=expr (pyserq: compile(..., defs={"NAME": "expr"})) gives an expression def its body from outside, as --set gives a let its value: the program is the one written with that body, IR and all. A distribution, a key or a law per class the program leaves open under a name is a parameter of the run, where it had to be spliced into the program's text. The body may draw, read attributes and use the definitions before it; statement definitions and unknown names are errors; rejected on .json (#186).

pyserq Rng(seed): the generator a run draws from, rand 0.9's StdRng (next_u32, next_u64, random_f64, range_u64/range_u32/range_f64 with both ends included). A run seeded s draws its arrivals from Rng(s) (#185).

A NaN constant's error points at the expression when it has a place (#184).

IR version 9, as in rc7. No breaking change.

What's Changed

• fix(link): a NaN constant's error keeps the expression's place by @vrvrv in #184
• feat(pyserq): Rng, the generator a run draws from by @vrvrv in #185
• feat: --def gives an expression definition its body from outside by @vrvrv in #186
• chore(release): v0.1.0-rc8 by @vrvrv in #187

Full Changelog: v0.1.0-rc7...v0.1.0-rc8

serQ v0.1.0-rc7

IR version 9 (breaking): a pool's waiting queue is ordered when a request is selected, on the admission clock, not by a key cached at enqueue. CPool.queue is a list of keys compared in order, ties by enqueue order; waited is the time a request has waited. A time-dependent queue policy changes meaning; a static one-key policy keeps its order. Older IR is not read: regenerate JSON from source (#178).

pyserq (breaking): the report by field. Report has the summary's fields by name, observes, stages and pools, and observe/stage/stages_named/pool by name; an Observe has its statistics and its samples, times, sessions, turns. Report.observe(name) returns an Observe (or None), not a tuple. The attribute names are the JSON field names, which REPORT_VERSION (1) names (#181). read_trace(path) gives a trace's sessions by the parser a replay uses (#177).

Constants: an infinity passed to sets is inf (#179). A constant that evaluates to NaN (0/0, inf - inf) is a link error in every constant position (let, --set, cap, block, fifo, the arrival, the run block), where it used to reach the IR as "inf" (#182).

What's Changed

• feat(pyserq): read_trace, a trace's sessions by the parser a replay uses by @vrvrv in #177
• fix(link): set_num refuses only NaN; an infinity is inf by @vrvrv in #179
• feat(ir)!: select waiting requests on the admission clock by @vrvrv in #178
• docs(use-cases): describe tagged full-attention vendor schedulers by @vrvrv in #164
• feat(pyserq): the report by field: observes, stages and pools as objects by @vrvrv in #181
• fix(link): a constant that is NaN is refused by @vrvrv in #182
• chore(release): v0.1.0-rc7 by @vrvrv in #183

Full Changelog: v0.1.0-rc6...v0.1.0-rc7

serQ v0.1.0-rc6

The first release as serQ, and the first with pyserq, the Python binding: pyserq.compile(path_or_source, sets=…, seed=…) gives the IR, pyserq.run(program) runs it with the GIL released, and the report and each observation's samples come back as data. The release carries abi3 wheels for linux x86_64 and macOS arm64. REPORT_VERSION (1) names the shape of the report JSON.

Breaking: seQ is serQ. The crate and CLI are serq, the library serq::, program files .sq, the environment variables SERQ_*, the repository vrvrv/serQ. IR version 8: a run holds several stages at once. serve exclusive prefill constrains the whole batch, a waiting prefill included.

What's Changed

• feat(ir)!: a run holds several stages at once (IR v8) by @vrvrv in #157
• feat(examples): a NIXL read holds both NICs in llmd_nixl_pull by @vrvrv in #160
• perf(interp): recompute the flows a change can reach by @vrvrv in #162
• fix(draw): a flow's stations are neighbours, and no arrow runs through a station by @vrvrv in #165
• test(draw): the site's figures are their programs' figures by @vrvrv in #168
• refactor!: seQ is serQ by @vrvrv in #166
• docs: vLLM refuses a request that can never fit, it does not ignore it by @vrvrv in #170
• fix(draw): a label wider than its column gets the room by @vrvrv in #173
• fix(scheduler): isolate prefill across waiting admission by @vrvrv in #171
• feat: pyserq, serQ in Python (the IR and a run) by @vrvrv in #174
• chore(release): v0.1.0-rc6 by @vrvrv in #175

Full Changelog: v0.1.0-rc5...v0.1.0-rc6

seQ v0.1.0-rc5

Adds definitions a program writes (def f(x) = e;, def f(x) { … }) and libraries it reads (use "file.seq";); the vLLM engine is written once, as vllm_request in lib/vllm.seq. A hold's body reads the header bindings it names, blocksize(p) reads a pool's block, and tools/metrics.json records the language's size, held by make check.

Breaking: IR version 7 — Choose.key is a list of keys compared in order (choose j in n by (k1, k2, …)), so IR files of version 6 are refused and seq::ir::CStmt::Choose.key is a Vec<CExpr>. An admission is spelled one way, hold … at admission (…) { … } cache (…): enter … keep and admit if … fit where … keep are gone, and enter, admit, keep, where and fit may not name anything. Context variables are renamed for what they are: kvb, kvp, ntok, npre, ndec, nres, attn become kv_decode, kv_prefill, tokens, prefilled, decoders, residents, attention; the eviction variable queued is waiting and the ps variable n is present; an old name is refused with the new one. A transfer names where the KV goes (from P to Q (n)). lecture_pd.seq leaves the examples and llmd_pd.seq is llmd_nixl_pull.seq. Token has a file field.

What's Changed

• feat(report): size the text report's columns to their contents by @vrvrv in #117
• refactor(examples): remove lecture_pd.seq by @vrvrv in #121
• feat(parser): a transfer names where the KV goes by @vrvrv in #123
• refactor(examples): rename llmd_pd.seq to llmd_nixl_pull.seq by @vrvrv in #124
• fix(draw): a loop returns down every arm of its body by @vrvrv in #126
• fix(draw): a hold of no units draws no box by @vrvrv in #127
• docs(visualization): draw the one-engine deployment by @vrvrv in #129
• fix(ir): a label shows a fraction as it would be written by @vrvrv in #130
• feat(frontend): a hold's body sees the header bindings it reads by @vrvrv in #133
• feat(frontend): def — a name for source a program would repeat by @vrvrv in #134
• feat(frontend): use — programs share definitions from a library by @vrvrv in #135
• fix(frontend): the program file counts as read by @vrvrv in #143
• feat(frontend): blocksize(p) — a pool's block, folded at link time by @vrvrv in #144
• fix(interp): a reservation above the cap is rejected by @vrvrv in #146
• refactor(frontend): context variables say what they are by @vrvrv in #147
• fix(examples): a local prefill queues at the decoder's blocks by @vrvrv in #149
• fix(examples): bound the request and unshare the read latency in llmd_nixl_pull by @vrvrv in #150
• docs(design): a transfer uses both ends by @vrvrv in #151
• refactor(frontend): one admission, one spelling by @vrvrv in #152
• feat(tools): the language's size in tools/metrics.json, held by make check by @vrvrv in #153
• docs(api): enter the reference by what you are modelling by @vrvrv in #154
• feat(ir)!: choose compares a tuple of keys (IR v7) by @vrvrv in #155
• chore(release): v0.1.0-rc5 by @vrvrv in #156

Full Changelog: v0.1.0-rc4...v0.1.0-rc5

seQ v0.1.0-rc4

Adds renewal arrivals (arrive renewal(gap)) and finite open workloads (run { arrivals N; }, --arrivals).

Breaking: the crate's modules are regrouped under frontend, engine, ir and view with no re-exports of the old paths (seq::parser is now seq::frontend::parser); programs/ moved to examples/<workload>/; seq-lang draw drops the session view together with --view and --show-set.

What's Changed

• refactor: programs/ → examples/<워크로드>/ 로 재배치 by @vrvrv in #103
• chore: remove editors/ by @vrvrv in #105
• refactor: src/를 frontend/ sim/ view/ ir/ 로 분리 by @vrvrv in #106
• feat: support renewal arrivals and finite open workloads by @vrvrv in #107
• docs: 네 갈래 nav와 구성요소별 API Reference by @vrvrv in #109
• refactor(draw): session view 제거 by @vrvrv in #110
• chore(release): v0.1.0-rc4 by @vrvrv in #111

Full Changelog: v0.1.0-rc3...v0.1.0-rc4