Pith. sign in

REVIEW 2 major objections 6 minor 31 references

A small trusted guard, not the learned admitter, must own the safety-projection part of a tenant's assured SLO; this paper argues and demonstrates that such a guard holds the floor even when the learner is arbitrarily wrong.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-02 07:24 UTC pith:PG37VZ2Q

load-bearing objection A genuinely useful architectural stance with a structurally enforced admission floor; the service floor is honestly conditional on an unproven backlog lemma, so the paper's own scoping is right. the 2 major comments →

arxiv 2607.09992 v2 pith:PG37VZ2Q submitted 2026-07-10 cs.DC

Trusted Floors Under Untrusted Learners: A Runtime Assured-SLO Guard for ML Serving

Hsiu-Chi Tsai This is my paper
classification cs.DC
keywords ML servingassured SLOruntime assuranceadmission controltrust boundarysafety propertylatency deadlinelearned controllers
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Modern ML-serving systems increasingly let learned, unverified components—routers, latency-SLO admitters, admission ladders—decide a tenant's quality of service, so a wrong learner can silently break an assured SLO. This paper argues that learned infrastructure controllers must not directly own contractual tenant entitlements: instead, a small trusted guard should wrap the untrusted learner, with the learner only proposing and the guard disposing. The paper splits an assured SLO into a safety projection (admission floor, service floor, and a doom-sound drop rule) that a guard can enforce at runtime, and a statistical residual (a tail-latency percentile) that can only be screened. A per-class credit reservation plus assured-first priority dispatch holds the admission floor structurally and the service floor conditionally, and real two-GPU experiments show the guarded class missing zero requests across every tested miscalibration where the unguarded stack misses 86–94%.

Core claim

The paper's central claim is that a tenant's assured SLO obligation divides into two parts with different epistemics. The safety projection—a doom-sound drop rule, a per-window assured admission floor, and a per-request service floor—is a safety property a runtime guard can enforce; the aggregate obligation (a population tail-latency percentile such as P95) has no per-request enforcement point and is treated as a statistical residual. The guard implements 'learned proposes, the guard disposes': the untrusted learned admitter outputs admission/class/priority proposals, but floor-entitled requests are admitted from reserved credits on the true authenticated class and dispatched assured-first,

What carries the argument

The load-bearing object is the 'learned proposes, the guard disposes' boundary: the learner's output is a proposal tuple (admit/reject, class/objective selection, priority hint) with no actuation authority over the assured floor. The guard is a Simplex-style runtime-assurance wrapper made of three mechanisms: a per-class, per-window credit reservation that caps assured admission at B requests and reserves capacity (the admission floor, AF, enforced by construction); assured-first non-preemptive priority dispatch (the service floor, SF); and a doom-sound drop rule that drops a request only when start-time plus a lower-bound service estimate exceeds its deadline (DR), an optional optimization

Load-bearing premise

The service-floor guarantee assumes that every request finishes within a fixed service-time ceiling (a calibrated estimate, not a proven worst case) and that assured requests never pile up across time windows; if either fails, the admission floor still holds but the deadline guarantee does not.

What would settle it

Run the guard on a real backend, deliver a burst whose assured arrivals straddle a window boundary while the reservation runs at full utilization, and record any assured request that misses its deadline; or instrument per-request service times under sustained full-batch load and find one exceeding the claimed service ceiling. Either observation would falsify the conditional service-floor guarantee.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • If the stance is right, a tenant's assured floor can be guaranteed against an arbitrarily miscalibrated learned admitter—no learner calibration or certification is needed for the safety projection.
  • The service floor is a conditional corollary of the admission floor: given capacity, a service envelope, bounded backlog, and a shared window origin, a per-request deadline guarantee follows from the structural reservation.
  • A cheap static screen is a characterization, not a certifier: it false-accepts near saturation and in deep sub-saturation, so the runtime guard, not the screen, is the only protection at the queueing knee.
  • Request-count reservation is the wrong entitlement meter when request sizes vary; a token-weighted reservation is the identified fix and the predicted way to hold the floor under heterogeneous output lengths.
  • Because the aggregate tail percentile is a statistical residual, it should be screened rather than runtime-enforced; the paper's split gives system builders a principled division of labor.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Editor inference: the safety-vs-statistics split is a design rule that likely generalizes beyond ML serving: any contractual obligation that is a safety property should be enforced by a trusted mechanism, while statistical obligations should be screened; learned controllers belong only on the surplus side of the boundary.
  • Editor inference: the count-meter failure predicts a concrete test—a token-weighted reservation with admission-time weight estimates should hold the floor under bimodal output lengths where the count meter misses; this is a direct, low-cost extension of the reported experiments.
  • Editor inference: the injected mapping fault suggests a broader lesson for serving systems: any layer that dispatches by a priority label handed to it by an unauthenticated mapping is structurally fragile; authenticating the class at the trust boundary is the fix.
  • Editor inference: the backlog lemma is called out as a precondition, not a closed result; finding either a proof or a concrete straddling-burst counterexample at full utilization is the sharpest step toward turning the empirical 0.0 into a theorem.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. The paper's central claim is that learned infrastructure controllers must not directly own contractual tenant entitlements. It proposes a trusted guard that wraps an untrusted learned admitter: the learned component proposes admission/class/priority, while a per-class, per-window reservation (AF), assured-first priority (SF), and a doom-sound drop rule (DR) are enforced by the guard. The paper distinguishes the safety projection {AF, SF, DR} from the aggregate statistical obligation (P95), which it treats as a screenable residual. AF is claimed structural; SF is claimed conditional on capacity, service-envelope, backlog, window-origin, and scheduling preconditions; DR is conditional on an assumed service lower bound. Experiments on 2xV100 show 0/2880 assured misses across a miscalibration sweep where the unguarded stack misses 0.86-0.94; a live GAIE Flow Control fault-injection flips the same assured requests from miss 0.0 to 1.0; and a static timing screen is characterized, with a p99 knob that the paper itself describes as a post-hoc patch. The paper explicitly defers a closed worst-case theorem to future work.

Significance. Strengths: the safety-projection versus statistical-residual split is a useful conceptual contribution; the evaluation uses run-level Clopper-Pearson intervals, three denominators, phase sweeps, and disclosed single-run fault injection; the authors are admirably explicit about conditions they do not prove. The architectural stance—a bounded proposal interface, keying on the true contract class—is clear and implementable. Weakness: the service-floor guarantee is not closed. It depends on the unproven backlog condition Q_A≤B and on a calibrated, not proven, s_max. The paper's own text says this, but the title and abstract risk overclaiming by bundling SF into a 'regardless' safety projection. The empirical 0.0 miss is strong evidence but not a structural guarantee. The significance is therefore real but provisional: the contribution is a promising mechanism plus early evidence, not a proved assured-SLO guard.

major comments (2)
  1. [§2, worst-case sojourn bound] The derivation of T_assured ≤ s_max(1+⌈B/C⌉) relies on the assertion that the assured cohort ahead of a queued request is 'at most B in total, not B besides R.' This is not a consequence of A1-A4; the paper itself calls Q_A≤B 'a precondition, not a closed result' and identifies a boundary-straddling burst at ρ_a=1 as the counterexample. Concretely, with C=4, B=6, W=1.5 s_max and B arrivals at each window boundary, A1-A4 hold, but at the second boundary the assured backlog (queued plus in service) is 8 > B, so the proof step fails. The service floor is therefore not structural; it is an empirical/conditional claim. This is load-bearing because the paper's central 'regardless' statement bundles SF with AF. Please either prove Q_A≤B under an explicit arrival condition, or revise the abstract/conclusion to state that the safety projection's structural floor is AF only, with SF conditional on
  2. [§2, Assumption A3] The service floor also assumes A3, that per-request service is bounded by s_max. The paper reports s_max≈660 ms is a calibrated ceiling, with max observed assured service 601 ms, and that continuous batching makes service load-dependent (386→460 ms). Thus s_max is not a proven WCET, and the response-time bound is not a formal guarantee. The paper discloses this, but the title 'Assured-SLO Guard' and the contribution list present SF as part of the assured safety projection. At minimum, the abstract and conclusion should state in the same breath that the contribution is a conditional runtime assurance, not a closed worst-case guarantee, and that closing A3 and Q_A≤B is open (as §5 already says).
minor comments (6)
  1. [§2, backlog precondition] Define Q_A formally before using it in the bound: is it the number of queued assured requests, or queued plus in-service, and at which time instant? Currently it appears parenthetically and its exact meaning is inferred.
  2. [§2, learned admitter setup] The β miscalibration multiplier for the least-squares latency predictor is described only informally. Please give the exact predictor form and how β enters, so the 4-condition sweep is reproducible.
  3. [§2, operating envelope] The notation A10/A95 ('assurance ratio') is unexplained. Define these terms where they first appear.
  4. [§2, Table 1] The word 'marquee' is used without definition. Consider replacing with '40-run sweep' or defining it on first use.
  5. [Table 2] The abbreviation 'mech.' is confusing; use 'mechanised' in the caption and legend.
  6. [Figure 2] The caption reports 1320 cells but only 120 hardware runs, with deadlines re-thresholded post-hoc. The text says this, but the caption should repeat it to avoid over-reading the grid.

Circularity Check

0 steps flagged

No significant circularity: the guard's guarantees are either structurally enforced or explicitly conditional, and every fitted or measured input is disclosed as empirical rather than presented as a first-principles prediction.

full rationale

The derivation chain is self-contained. The admission floor (AF) is a property of the mechanism itself: A1 caps admitted assured at B credits per window, so AF 'holds by construction,' and the paper explicitly states the empirical 0.0 miss 'corroborates' rather than grounds the guarantee ('The empirical 0 corroborates the structurally-enforced AF and the conditional SF... it is not the basis of either'). The service floor (SF) is a conditional response-time implication, T_assured ≤ s_max(1+⌈B/C⌉), derived from the window cap and A2–A4; its proof does not depend on the measured value of s_max, only on the conditional assumptions being true. The load-bearing gap is the backlog precondition Q_A≤B, which the paper names as 'a precondition, not a closed result' and even supplies the counterexample ('a burst straddling a window boundary at ρa=1'); that is an honest, disclosed soundness limitation, not a circular reduction, because the SF claim is explicitly made conditional on it. The fitted inputs (calibrated s_max≈660ms ceiling, DR's median lower bound L≈236ms, the static screen's p99 knob) are all disclosed as empirical envelopes, not proven WCETs: 'we do not claim the measured s_max is a formally established WCET'; the screen's accuracy is called 'post-dictive,' the p99 closure 'a post-hoc patch' with held-out degradation (precision 1.000→0.90 at 10% calibration) and 'a characterization, not a pre-deployment certificate.' None of these is renamed as a prediction, and the screen is a subordinate question, not the basis of the guard. There are no self-citations in the reference list; the CBS/Simplex/mixed-criticality/network-calculus lineage is external, classical, and explicitly not claimed as novel ('Scheduling lineage (owned)'). The central claim therefore does not reduce by construction to its inputs; its open conditions (Q_A≤B, calibrated s_max, window-origin alignment) are flagged in the paper itself, so the honest finding is no circularity.

Axiom & Free-Parameter Ledger

4 free parameters · 8 axioms · 0 invented entities

The paper is transparent: A1-A4 plus the backlog, window-origin, class-binding, and lower-envelope preconditions are all stated. The load-bearing unclosed items are the backlog lemma and the service-envelope (A3/s_max, not proven WCET), so the response-time bound is a conditional implication rather than a closed guarantee. No new physical or model entities are postulated; the guard is a composition of classical reservation, priority, and drop mechanisms.

free parameters (4)
  • assured floor B (request credits per tumbling window) = 6 (marquee), 3 (BurstGPT), 4-8 in sweeps
    Contractual reservation size; the AF/SF guarantee is scoped by stability condition A4 (rho_a = B*s_max/(C*W) <= 1), so the central claim depends on this chosen parameter.
  • calibrated service ceiling s_max = ≈660 ms (Qwen 35B, ~16-token regime; observed max 601 ms)
    Measured from the same 2xV100 backend and used as the service envelope in A3. The paper explicitly does not claim this is a proven WCET (§5).
  • doom-sound service lower bound L for DR = ≈236 ms (batch-1 median service, 12 probes)
    Median service used as an assumed lower envelope L <= s for the drop rule; the paper states this is assumed, not established. DR is optional and near-inert, so this is not central to AF/SF.
  • p99 service percentile knob for the static screen = p99 (≈660 ms padded ceiling)
    Post-hoc conservative input chosen to drive the 1320-cell grid's false accepts to zero (§3); the paper discloses held-out degradation and calls it a characterization, not a certificate.
axioms (8)
  • domain assumption A1: reservation caps admitted assured at B request credits per tumbling window W and reserves a >=B capacity floor
    Introduced in §2; the admission floor is enforced by construction only if the reservation is actually realized by the scheduler and capacity.
  • domain assumption A2: assured-first non-preemptive fixed-priority dispatch with arrival-order tie-break
    Scheduling precondition for SF in §2; vLLM's stock priority scheduler does not preempt running requests (issue #40004), so this is not automatic.
  • domain assumption A3: per-request service time (assured and opportunistic) bounded by s_max
    Used for the sojourn bound; continuous batching strains load-independence and s_max is calibrated, not a proven WCET (§2, §5).
  • domain assumption A4: reservation stability rho_a = B*s_max/(C*W) <= 1
    Sufficient, not necessary; empirical break sits beyond the guaranteed boundary (§2).
  • domain assumption Backlog lemma Q_A <= B: assured backlog does not accumulate across windows
    Explicitly a precondition, not a closed result (§2); a counterexample would be a burst straddling a window boundary at rho_a=1.
  • domain assumption Shared window origin: contract and guard use the same epoch t0
    AF entitlement is defined on tumbling windows; phase sweep shows attainment can drop to 0.67/0.73 if offset (§2).
  • domain assumption Authenticated end-tenant class key bound before any learned component runs
    Trust boundary: absent an authenticated class, no reservation can distinguish mislabel from truth (§2).
  • domain assumption Service lower bound L <= s for the doom-sound drop rule
    DR is sound only under an assumed service lower envelope; L is a measured median, not established (§2).

pith-pipeline@v1.3.0-alltime-deepseek · 17961 in / 14000 out tokens · 148408 ms · 2026-08-02T07:24:48.470090+00:00 · methodology

0 comments
read the original abstract

Modern ML serving increasingly lets learned, unverified components (routers, latency-SLO admitters, admit ladders) decide a tenant's quality of service; when one is wrong, the assured SLO can silently break, and the Kubernetes layers beneath (Kueue, DRA, the Gateway-API Inference Extension, GAIE) add cross-layer surprises. Rather than trust the learner to be right, we bound the damage a wrong one can do: a small trusted guard wraps the untrusted learner (learned proposes, the guard disposes). A tenant's assured-SLO obligation splits into two parts with different epistemics. Its safety projection, a per-class, per-window assured floor (with an optional drop rule, doom-sound only under an assumed service lower envelope), is a controllable obligation a guard enforces at runtime, holding it regardless of a learned admitter that is arbitrarily wrong within a bounded proposal interface. The admission floor is enforced structurally; given the stated assumptions, the service floor follows as a conditional response-time implication. Its aggregate obligation (the population tail-latency percentile) has no per-request enforcement point, so we treat it as a statistical residual and screen it. On real 2xV100 the guard (a Simplex-style assured-floor gate plus assured-first priority) holds assured-class miss 0.0 across every tested miscalibration of a learned admitter that, unguarded, misses 0.86-0.94; against a live deployment of the GAIE Flow Control, an injected mapping fault (emulating an untrusted mapper) flips the same assured requests from miss 0.0 to 1.0 (a mechanism-level trust-boundary test, not a head-to-head), while our guard reserves by the true class. As a Frontiers submission we evaluate the stance on commodity 2xV100 and a serving simulator, scoping datacenter scale, real-model Flow Control, and a closed worst-case theorem as the agenda.

Figures

Figures reproduced from arXiv: 2607.09992 by Hsiu-Chi Tsai.

Figure 1
Figure 1. Figure 1: The guard holds the assured floor as a property of its structure, not the learner’s calibration. (a) CDF of assured completion, worst miscalibration (𝛽=0), real 2×V100: every guard-admitted request completes ≤855 ms here (≤924 across the 𝛽 sweep), far inside the 1856 ms deadline (miss 0.0); unguarded spreads past 20 s (miss 0.93). (b) Same CDF, a tighter fault-injection run (deadline 1544 ms), byte-identic… view at source ↗
Figure 1
Figure 1. Figure 1: Reservation and priority, not the learner’s calibration, hold the assured floor in the tested operating region (AF structurally, SF under the stated service assumptions). (a) CDF of assured completion, worst miscalibration (𝛽=0), real 2×V100: every guard-admitted request completes ≤855 ms here (≤924 across the 𝛽 sweep), far inside the 1856 ms deadline (miss 0.0); unguarded spreads past 20 s (miss 0.93). (b… view at source ↗
Figure 2
Figure 2. Figure 2: Where the cheap static screen is unsound: the hardware grids, aggregated. (a) Each (𝜌ˆ × deadline) bin is orange where the screen proved a config the hardware missed (unsound), white where proved held, grey where it rejected all (n/a). The 𝜌ˆ axis now spans both grids (0.45–4.06, reps-10 sub-saturation + reps-3 overload, unmixed); unsound cells sit on both sides of the 𝜌ˆ =1 knee (dashed)—the overload knee… view at source ↗
Figure 2
Figure 2. Figure 2: Where the cheap static screen is unsound: the hardware grids, aggregated. (a) Each (𝜌ˆ × deadline) bin is orange where the screen accepted a config the hardware then missed (a false accept, so unsound there), white where an accepted config held, grey where it rejected all (n/a). The 𝜌ˆ axis now spans both grids (0.45–4.06, reps-10 sub-saturation + reps-3 overload, unmixed); false-accept cells sit on both s… view at source ↗
Figure 3
Figure 3. Figure 3: The guard is the only evaluated arm at both max￾imum assured-SLO attainment and maximum goodput under this grid, at every deadline (2×V100; 24 req/s offered, backend ≈6.8/s, so the guard’s 6/s is near-ceiling). The WCRT admitter (re-implemented Chronos Alg. 1) matches attainment at loose deadlines but at lower goodput and collapses at the tight knee; admit-all loses goodput to self-congestion. Its reject-∼… view at source ↗
Figure 3
Figure 3. Figure 3: The guard is the only evaluated arm at both the maximum assured on-time fraction and maximum goodput under this grid (offered basis, met / offered, so a rejected assured request counts against an arm), at every deadline (2×V100; 24 req/s offered, backend ≈6.8/s for this figure’s mixed-size/deadline workload—distinct from §2’s ∼16-token saturation 𝜇sat =9.6–9.7/s—so the guard’s 6/s is near-ceiling; reps 8, … view at source ↗

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

31 extracted references · 11 linked inside Pith

  1. [1]

    Integrating multimedia applications in hard real-time systems

    Luca Abeni and Giorgio Buttazzo. Integrating multimedia applications in hard real-time systems. InIEEE Real-Time Systems Symposium (RTSS), 1998. Constant Bandwidth Server

    1998

  2. [2]

    Schneider

    Bowen Alpern and Fred B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, 1985

    1985

  3. [3]

    Enforceable security policies revisited.ACM Trans

    David Basin, Vincent Jugé, Felix Klaedtke, and Eugen Zăli- nescu. Enforceable security policies revisited.ACM Trans. Inf. Syst. Secur., 16(1), 2013. controllable vs. only-observable actions; POST 2012

    2013

  4. [4]

    Position: A three-layer probabilistic assume– guarantee architecture is structurally required for safe LLM agent deployment.arXiv preprint arXiv:2605.18672, 2026

    Saddek Bensalem, Yi Dong, Martin Fränzle, Xiaowei Huang, Janis Kröger, Dejan Nickovic, Ayoub Nouri, Rajarshi Roy, and Changshun Wu. Position: A three-layer probabilistic assume– guarantee architecture is structurally required for safe LLM agent deployment.arXiv preprint arXiv:2605.18672, 2026

    Pith/arXiv arXiv 2026

  5. [5]

    From inference routing to agent orchestration: Declarative pol- icy compilation with cross-layer verification.arXiv preprint arXiv:2603.27299, 2026

    Huamin Chen, Xunzhuo Liu, Bowei He, and Xue Liu. From inference routing to agent orchestration: Declarative pol- icy compilation with cross-layer verification.arXiv preprint arXiv:2603.27299, 2026

    arXiv 2026

  6. [6]

    Siyuan Chen, Zhipeng Jia, Samira Khan, Arvind Krishna- murthy, and Phillip B. Gibbons. SLOs-Serve: Optimized servingofmulti-SLOLLMs.arXivpreprintarXiv:2504.08784, 2025

    Pith/arXiv arXiv 2025

  7. [7]

    Clarkson and Fred B

    Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157–1210, 2010. Also CSF 2008

    2010

  8. [8]

    Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints

    Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. InPOPL, 1977

    1977

  9. [9]

    Rene L. Cruz. A calculus for network delay, part I: Network elements in isolation.IEEE Transactions on Information Theory, 37(1):114–131, 1991

    1991

  10. [10]

    Tokenmanagementinmulti-tenantAI inference platforms.arXiv preprint arXiv:2603.00356, 2026

    WilliamJ.Cunningham. Tokenmanagementinmulti-tenantAI inference platforms.arXiv preprint arXiv:2603.00356, 2026

    arXiv 2026

  11. [11]

    Henzinger

    Thomas A. Henzinger. Sooner is safer than later.Information Processing Letters, 43(3):135–141, 1992

    1992

  12. [12]

    J. F. C. Kingman. The single server queue in heavy traffic. Proc. Cambridge Phil. Soc., 57(4):902–904, 1961

    1961

  13. [13]

    Wiley, 1975

    Leonard Kleinrock.Queueing Systems, Volume 1: Theory. Wiley, 1975. Pollaczek–Khinchine; M/M/1 sojourn

    1975

  14. [14]

    Krasnovsky

    Anatoly A. Krasnovsky. Emergence-as-code as a founda- tion for self-governing reliable systems.arXiv preprint arXiv:2602.05458, 2026

    Pith/arXiv arXiv 2026

  15. [15]

    Edit automata: Enforcement mechanisms for run-time security policies.Inter- national Journal of Information Security, 4(1–2):2–16, 2005

    Jay Ligatti, Lujo Bauer, and David Walker. Edit automata: Enforcement mechanisms for run-time security policies.Inter- national Journal of Information Security, 4(1–2):2–16, 2005

    2005

  16. [16]

    Large- scale LLM inference with heterogeneous workloads: Prefill- decode contention and asymptotically optimal control.arXiv preprint arXiv:2602.02987, 2026

    RuihanLin,ZeanHan,ZezhenDing,andJihengZhang. Large- scale LLM inference with heterogeneous workloads: Prefill- decode contention and asymptotically optimal control.arXiv preprint arXiv:2602.02987, 2026

    Pith/arXiv arXiv 2026

  17. [17]

    Brighten Godfrey.Kivi: Verificationforclustermanagement.InUSENIX ATC, 2024

    Bingzhe Liu, Gangmuk Lim, Ryan Beckett, and P. Brighten Godfrey.Kivi: Verificationforclustermanagement.InUSENIX ATC, 2024. arXiv:2311.02800; verifies controllers AND their configurations

    Pith/arXiv arXiv 2024

  18. [18]

    insufficient unused quota

    BenjaminLivshitsetal. Indefenseofsoundiness: Amanifesto. Communications of the ACM, 58(2):44–46, 2015. 11 Hazard Layer pair Composed cross-layer surprise (each artifact valid alone) Checker C1 Kueue cohort↔kubePriorityClass a user-reported cross-ClusterQueue preemption despitereclaimWithinCohort:Never; kubePriorityClass involved, root cause not definitive...

    2015

  19. [19]

    Formal schedulability analysis for LLM inference: TTFT and TBT deadline guarantees via response-time theory.Frontiers in Computer Science, 8, 2026

    Amine Marref, Khaled Tarmissi, and Hassene Chaibi. Formal schedulability analysis for LLM inference: TTFT and TBT deadline guarantees via response-time theory.Frontiers in Computer Science, 8, 2026. 10.3389/fcomp.2026.1873627

    arXiv 2026

  20. [20]

    Smolka, and Scott D

    Usama Mehmood, Sanaz Sheikhi, Stanley Bak, Scott A. Smolka, and Scott D. Stoller. The black-box simplex archi- tecture for runtime assurance of autonomous CPS. InNASA Formal Methods (NFM), 2022. arXiv:2102.12981

    Pith/arXiv arXiv 2022

  21. [21]

    Parekh and Robert G

    Abhay K. Parekh and Robert G. Gallager. A generalized processorsharingapproachtoflowcontrolinintegratedservices networks: The single-node case.IEEE/ACM Transactions on Networking, 1(3):344–357, 1993

    1993

  22. [22]

    Smolka, and Scott D

    Dung Phan, Radu Grosu, Nils Jansen, Nicola Paoletti, Scott A. Smolka, and Scott D. Stoller. Neural simplex architecture. In NASA Formal Methods (NFM), 2020. arXiv:1908.00528

    Pith/arXiv arXiv 2020

  23. [23]

    Schneider

    Fred B. Schneider. Enforceable security policies.ACM Trans. Inf. Syst. Secur., 3(1):30–50, 2000

    2000

  24. [24]

    LuiSha.Usingsimplicitytocontrolcomplexity.IEEESoftware, 18(4):20–28, 2001

    2001

  25. [25]

    Anvil: Verifying liveness of cluster management controllers

    Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. Anvil: Verifying liveness of cluster management controllers. InOSDI, 2024

    2024

  26. [26]

    Executionenvelopes: Asharedadmissioncontract for backend AI execution requests

    KrtiTallam. Executionenvelopes: Asharedadmissioncontract for backend AI execution requests. arXiv:2605.08267, 2026

    Pith/arXiv arXiv 2026

  27. [27]

    SCORPIO: Serving the right requests at the right time for heterogeneous SLOs in LLM inference.arXiv preprint arXiv:2505.23022, 2025

    Yinghao Tang, Tingfeng Lan, Xiuqi Huang, Hui Lu, and Wei Chen. SCORPIO: Serving the right requests at the right time for heterogeneous SLOs in LLM inference.arXiv preprint arXiv:2505.23022, 2025

    Pith/arXiv arXiv 2025

  28. [28]

    InIEEE Real-Time Systems Symposium (RTSS), 2007

    SteveVestal.Preemptiveschedulingofmulti-criticalitysystems with varying degrees of execution time assurance. InIEEE Real-Time Systems Symposium (RTSS), 2007

    2007

  29. [29]

    Statistical model checking for hyperproperties

    Yu Wang, Siddhartha Nalluri, Borzoo Bonakdarpour, and Miroslav Pajic. Statistical model checking for hyperproperties. arXiv preprint arXiv:1902.04111, 2019

    Pith/arXiv arXiv 1902

  30. [30]

    BurstGPT: A real-world workload dataset to optimize LLM serving systems

    Yuxin Wang et al. BurstGPT: A real-world workload dataset to optimize LLM serving systems. InACM SIGKDD (KDD),

  31. [2025]

    arXiv:2401.17644. 12

    Pith/arXiv arXiv