https://arxiv.org/api/5z4IxYj7WD/A5qzHAsYxIJLh7MQ 2026-09-10T20:14:47Z 1464 60 15 http://arxiv.org/abs/2607.26927v1 Deductive Verification for Earliest Deadline First Scheduler Implementations 2026-07-29T13:56:07Z Real-Time Operating Systems (RTOSes) rely on scheduler implementations to provide predictable task execution. For safety-critical systems, it is therefore not sufficient to reason only about the abstract scheduling policy; the concrete implementation must also preserve the intended scheduling semantics. This is particularly challenging for Earliest Deadline First (EDF) scheduling, because EDF introduces dynamic, deadline-derived priorities that are often realized by reusing kernel infrastructure originally designed for fixed-priority scheduling. In this work, we formalize EDF correctness through three essential properties that any implementation of the Earliest Deadline First (EDF) scheduler must satisfy. Based on these properties, we propose a framework utilizing deductive verification, that applies to any EDF-based scheduler realization. We instantiate the framework in Frama-C/ACSL and apply it to three structurally different EDF scheduler realizations: RTEMS 5, RTEMS 6, and an EDF extension of FreeRTOS. 2026-07-29T13:56:07Z Daniel Kuhse Junjie Shi Jan Duy Thien Pham Kay Heider Marcus Völker Kuan-Hsun Chen Jian-Jia Chen http://arxiv.org/abs/2607.23900v1 KernelScript: Cross-Boundary Typed DSL for eBPF Applications 2026-07-27T00:14:33Z eBPF lets developers extend Linux with custom packet processing, tracing, and scheduling logic, and a verifier proves before execution that the code will not crash the kernel. The programming model, however, is fragmented: a single application spans kernel code, a userspace loader, and shared maps, yet the relationships among these pieces go unchecked. E.g. A map or event type defined differently on each side silently corrupts shared state. We observe that these cross-boundary relationships duplicate information that a type system can unify. We present KernelScript, a DSL that types maps, program handles, and execution domains in one source, then compiles to standard C through the original toolchain. We evaluate KernelScript on 43 eBPF workloads covering XDP, TC, kprobe, tracepoint, and struct_ops. KernelScript rejects cross-boundary bugs at compile time that standard C/libbpf still builds and loads, a unified source shrinks the diffs for cross-boundary changes by 5x, and generated code remains compatible with the existing toolchain. 2026-07-27T00:14:33Z Cong Wang Siyuan Sun Yusheng Zheng http://arxiv.org/abs/2606.00552v3 Edge-Based QoS-Aware Adaptive Task Placement: A Closed-Loop Control in Multi-Robot Systems 2026-07-25T02:21:12Z Multi-robot systems (MRS) increasingly offload compute-intensive perception tasks to edge nodes to meet strict time-sensitive Quality-of-Service (QoS) constraints. However, static task orchestration on a shared edge node can severely degrade QoS due to network latency, jitter, and edge-resource contention. We present a pilot edge-centric MRS testbed using Raspberry Pi nodes to evaluate a camera-to-manipulator pipeline under three modes: local execution, static offloading, and a QoS-aware Adaptive Task Placement (ATP) controller. ATP scores candidate placements using a multi-metric cost (normalized latency, CPU utilization, and switching overhead) over two-second control windows. The closed-loop visual servoing testbed is instrumented with sub-millisecond clock synchronization, network emulation, and detailed monitoring of multiple metrics across nodes to capture realistic jitter. Experimental results under compute-stress and network-fault scenarios show that static edge offloading reduces on-board CPU load but amplifies tail latency and deadline misses. In contrast, the QoS-aware ATP controller, by switching task placement based on measured latency and utilization thresholds, consistently lowers deadline violations and tail latency. Overall, the results position ATP as a practical edge-side control primitive for MRS and concrete design guidelines for Cloud-Edge Robotics deployments within the broader cloud-fog automation, while motivating QoS-aware multi-objective workload orchestration for industrial cyber-physical systems. 2026-05-30T05:54:44Z 6 pages, 2 figures, 2 tables, 1 algorithm, accepted paper on the 24th IEEE International Conference on Industrial Informatics (INDIN), 26-29 July, 2026, Melbourne, Australia Thien Tran Jonathan Kua Thuong Hoang Minh Tran Honghao Lyu Jiong Jin http://arxiv.org/abs/2607.21659v1 Defining AI-Native Systems: Autonomy as Revision Authority 2026-07-22T22:58:18Z AI has begun to write systems code: agents now synthesize, verify, and deploy system components. Despite this shift, "AI-native" remains a marketing term with no precise technical definition. This paper gives it one. We define AI-nativeness along a single axis---authority over the system's own decisions rather than by the capability of the underlying AI models. Building on a decision-level model of a system, we distinguish occupancy (who executes a decision) from revision authority (who may change it), organize revision authority into a ladder---self-tuning, self-rewriting, self-architecting and define a system as AI-native when an AI autonomously rewrites the system's own implementations. The definition further requires an escalation detector, a verification procedure, and a verified fallback, while leaving purpose and correctness human-owned. 2026-07-22T22:58:18Z Cheng Tan http://arxiv.org/abs/2602.09345v3 AgentCgroup: Understanding and Controlling OS Resources of AI Agents 2026-07-22T10:05:25Z AI agents are increasingly deployed in multi-tenant cloud environments, where they execute diverse tool calls within sandboxed containers, each call with distinct resource demands and rapid fluctuations. We present a systematic characterization of OS-level resource dynamics in sandboxed AI coding agents, analyzing 144 software engineering tasks from the SWE-rebench benchmark across two LLM models. Our measurements reveal that (1) OS-level execution (tool calls, container and agent initialization) accounts for 55-60% of end-to-end task latency; (2) memory, not CPU, is the concurrency bottleneck; (3) memory spikes are tool-call-driven with a up to 15.4x peak-to-average ratio; and (4) resource demands are highly unpredictable across tasks, runs, and models. Comparing these characteristics against serverless, microservice, and batch workloads, we identify three mismatches in existing resource controls: a granularity mismatch (container-level policies vs. tool-call-level dynamics), a responsiveness mismatch (user-space reaction vs. sub-second unpredictable bursts), and an adaptability mismatch (history-based prediction vs. non-deterministic stateful execution). We propose AgentCgroup, an intent-driven eBPF-based resource controller that exploits agents ability to declare resource needs and reconstruct execution strategies, using hierarchical cgroup structures aligned with tool-call boundaries, in-kernel enforcement via sched_ext and memcg_bpf_ops, and runtime-adaptive policies. Preliminary evaluation demonstrates improved multi-tenant isolation and reduced resource waste. AgentCgroup is open-source at https://github.com/eunomia-bpf/agentcgroup 2026-02-10T02:37:42Z Yusheng Zheng Jiakun Fan Quanzhi Fu Yiwei Yang Wei Zhang Andi Quinn http://arxiv.org/abs/2606.16924v3 Single-Connection Mixed-Criticality Transport with CATS: Bounded Guarantees, Three Structural Limits, and a QUIC Escape 2026-07-22T09:10:52Z Satellite terminals, industrial telemetry-and-control, embedded systems, tactical networks often multiplex a small, latency-critical message class with bulk traffic over one connection. A single FIFO connection can starve the critical class. Parallel connections cost another five-tuple (often blocked by carrier-grade NAT, port budgets, and operator policy), are not always available, and when the critical class is light are bandwidth-fair only in aggregate. We present CATS (Conductor-driven Asymmetric Transport Scheme), a sender-side, receiver-transparent TCP priority scheme in which a Conductor assigns each message a priority class and just-in-time sequence numbers under a credit-based shaper. CATS provides deterministic non-starvation, single-flow fairness, and a provable bounded per-class delay. We then show CATS-over-TCP is not a tail-latency mechanism. Three structural barriers bound single-connection in-band priority: the in-order sequence space, the shared congestion window, and per-flow network QoS. These barriers explain why fair queuing and L4S fail to help a single connection and can worsen it by granting a parallel-connection competitor per-flow isolation while leaving in-band priority unserved, and why two parallel connections reduce tail latency by 4-8 times at the cost of another flow. We give CATS-over-QUIC as the principled escape: independent sequence spaces with per-stream isolation under aggregate-coupled congestion control attain the guarantees on one fair flow. A proof of concept shows unreliable datagrams achieve a flat tail (approx. 27 ms p99.9 vs. approx. 307 ms over TCP) by never retransmitting lost messages, while reliable streams still require an aggregate-coupled congestion controller; we frame this standards gap as a research program. An ns-3 evaluation across loss, contention, and handover regimes supports every claim, including the negative ones. 2026-06-15T16:27:07Z 10 pages, 4 figures, 1 table Syed Muhammad Aqdas Rizvi http://arxiv.org/abs/2607.17518v2 Isolation Failure From Shared Storage: Characterizing and Exploiting Page-Cache SCA Leakage Across Containers and VMs 2026-07-21T19:51:20Z Modern cloud platforms increasingly combine strong software isolation mechanisms with shared hardware resources to improve performance and resource efficiency. Conventional containers do this by sharing the host kernel directly, whereas sandboxed runtimes (e.g., gVisor) and VM-based runtimes (e.g., Kata, QEMU/KVM) provide progressively stronger isolation. In all cases, when tenants access host-backed filesystem state, the host page cache can remain shared and observable. Although OS-managed, this page-cache channel forms an OS-mediated microarchitectural timing side channel whose signal is shaped by the processor microarchitecture, memory and storage hierarchies, and virtualization mechanisms. We thus investigate whether unprivileged timing measurements can reveal page-cache residency across these isolation boundaries. Our evaluation covers Docker; gVisor with systrap and KVM; Kata Containers using QEMU and Cloud Hypervisor with shared host filesystems; Kata using QEMU, Cloud Hypervisor, and Firecracker with block-device-backed storage; and QEMU/KVM virtual machines under multiple host cache policies. Our results show that the timing signal persists whenever the I/O path exposes shared, host-cacheable file-backed objects, including under OverlayFS layers, virtio-fs exports, and loop-backed block devices. However, direct I/O and dedicated block devices substantially attenuate or eliminate the signal. Virtualization therefore reshapes leakage through added latency and algorithmic noise but does not remove the underlying dependence on shared hardware and cache state. We showcase this through a case study in which we recover coarse-grained activity from a WordPress deployment backed by MySQL. These results place page-cache attacks within the broader class of OS-mediated microarchitectural timing channels and motivate coordinated hardware, virtualization, and OS support for timing isolation. 2026-07-20T03:47:34Z 22 pages, 6 figures, 8 tables Alon Abudraham Bar-Ilan University Xingyu Chen Boston University Itamar Levi Bar-Ilan University Ari Trachtenberg Boston University http://arxiv.org/abs/2607.18097v2 SuperPass: Fast-Tracking Blocking Threads to Mitigate Priority Inversion on Mobile Devices 2026-07-21T09:27:37Z Priority inversion occurs when a high-priority thread is delayed by a lower-priority one. Although well studied in real-time systems, its impact in general-purpose OSes (e.g., Android) remains underexplored. On Android, we find that priority inversions happen frequently and can delay latency-critical threads, degrading user experience. For example, the foreground app's UI thread is frequently blocked by low-priority threads, with blocking durations of up to 210 ms, enough to cause dropped frames. Existing solutions designed for real-time systems fail to eliminate long priority-inversion blockings on latency-critical threads and may introduce high overhead on Android. To solve this problem, we uncover two insights on Android: 1) long blockings are mainly due to the accumulated CPU waiting time of low-priority blocking threads rather than their critical-section latency; and 2) although latency-critical threads can be blocked by many concurrent readers, tracking a limited number of them is sufficient to achieve good responsiveness with low overhead in most cases. Guided by these insights, we propose SuperPass, a lightweight kernel mechanism that mitigates priority inversion by fast-track scheduling of low-priority threads blocking latency-critical threads. It introduces a scheduler fast track that grants immediate CPU access to threads blocking latency-critical threads, and employs a lock-level detector that effectively identifies most such blocking threads. We evaluate SuperPass on a Google Pixel 8 smartphone. Taking UI thread as a case study, SuperPass decreases the 99.9th-percentile blocking duration by 72.0% and blocking count by 47.7% on average compared to the default scheduler, and reduces janky frames by 29.2% with a system-wide CPU overhead of only 0.74%. SuperPass also outperforms existing approaches including priority inheritance, real-time UI promotion, and Proxy Execution. 2026-07-20T15:59:26Z Lei Li Yu Liang Riwei Pan Youcheng Sun Nan Guan Tei-Wei Kuo Chun Jason Xue http://arxiv.org/abs/2504.21394v2 Concurrency Testing in the Linux Kernel via eBPF 2026-07-21T07:52:13Z Concurrency is indispensable for modern software systems to meet performance and scalability demands, yet concurrency bugs remain notoriously difficult to detect and reproduce. Controlled Concurrency Testing (CCT) mitigates this challenge by systematically exploring thread interleavings through scheduling control. However, existing CCT approaches for OS kernels largely rely on external enforcement mechanisms, such as custom hypervisors or invasive kernel patches, resulting in substantial overhead and limited maintainability and extensibility. In this work, we present SECT, the first kernel-native concurrency fuzzing framework that rethinks scheduling as a first-class exploration mechanism. SECT introduces a novel CCT scheduler with temporal isolation scheduling and embeds programmable scheduling policies directly into the kernel dispatch path via eBPF, enabling fine-grained control over thread interleavings without customized hypervisors or extensive kernel core modification. In addition, SECT provides a preemption-safe instrumentation mechanism for injecting scheduling points at critical kernel events and incorporates a two-phase fuzzing workflow to jointly explore both sequential and concurrent behaviors. Our evaluation demonstrates that SECT achieves 38% more branches, 57% overhead reduction and 11.4$\times$ speed-up in bug exposure compared to a leading state-of-the-art kernel concurrency fuzzer. Moreover, SECT discovers eight previously unknown concurrency-related bugs in the Linux kernel, six of which have already been confirmed and fixed by developers. 2025-04-30T07:48:52Z This work has been accepted by USENIX Security 2026 Jiacheng Xu Dylan Wolff Xing Yi Han Jialin Li Abhik Roychoudhury http://arxiv.org/abs/2607.18161v1 TRIM: Reducing AI-Generated CodeSlop via Agent Trajectory Minimization 2026-07-20T17:06:19Z Coding agents are increasingly used to accelerate code generation in many downstream tasks, such as fixing bugs, building applications, and prototyping. However, despite their value as coding assistants, agent-generated code tends to be larger and more verbose than the corresponding human-written implementation. In this work, we show that the cause lies in the agent's own search process: while iterating toward a passing solution, an agent accumulates speculative edits, abandoned hypotheses, and temporary changes that persist into the final patch. This may seem harmless for a single patch, but the problem compounds as agents take responsibility for ever-larger portions of a codebase-a codebase that was once minimal and well-maintained slowly accumulates redundancy faster than it can be cleaned up, drifting to a state that is harder to maintain. Given the magnitude of this problem, we take a step towards alleviating this issue. First, we formally define this phenomenon as CodeSlop-the residual and functionally unnecessary edits commonly seen in AI-generated code. We then introduce our algorithm TRIM (Trajectory-guided Redundancy Identification and Minimization). Rather than minimizing CodeSlop directly, TRIM instead minimizes agent trajectories. As we show empirically, this indirect technique of minimizing CodeSlop is highly effective: TRIM cuts CodeSlop by 17.9%-32.9% across agentic scaffolds, with negligible performance regression. TRIM is also highly efficient, requiring roughly half the validation cost of algorithmic baselines such as Delta Debugging. 2026-07-20T17:06:19Z Alex Mathai Shobini Iyer Aleksandr Nogikh Petros Maniatis Franjo Ivancic Junfeng Yang Baishakhi Ray http://arxiv.org/abs/2607.17299v1 WAR: Workload-Aware Rollouts for Synchronous Agentic Reinforcement Learning 2026-07-19T15:31:13Z Long-horizon rollout generation has become the dominant systems bottleneck in agentic reinforcement learning (RL). As agents interact with environments over many turns, trajectories rapidly grow to tens of thousands of tokens, making synchronous RL training increasingly constrained by rollout. We propose WAR, a workload-aware rollout system that substantially accelerates synchronous agentic RL by jointly optimizing decoding and scheduling. WAR is built on a key observation: the optimal rollout optimization strategy depends on runtime load: (1) Under low load, WAR enables model-free speculative decoding with SuffixDecoding, which reuses suffix patterns from previously completed trajectories as speculative drafts for future rollouts. Unlike model-based drafters, SuffixDecoding introduces no additional draft model and avoids GPU contention with rollout generation. (2) Under high load, where saturated batched decoding leaves limited room for speculative speedup, WAR shifts the optimization focus to cache-aware scheduling. A global scheduler places requests across rollout replicas based on cache locality, trajectory progress and server load, reducing redundant KV-cache recomputation and mitigating load imbalance. By combining decoding-level suffix reuse with system-level rollout scheduling, WAR delivers robust throughput improvements across workload regimes without changing the underlying RL algorithm. WAR improves long-context agentic rollout throughput by 1.4x under low load and up to 1.6x under high load. These results show that WAR removes a major rollout bottleneck in synchronous agentic RL and provides a practical path toward scalable long-context agent training. 2026-07-19T15:31:13Z Ryan Xu Atlas Zhao David Bao Frank Du http://arxiv.org/abs/2607.16784v1 Roomie: Interference-Aware Colocation for Efficient Model Serving 2026-07-18T11:35:59Z As demand for DNN inference grows, GPU capacity is increasingly oversubscribed, forcing operators to colocate multiple models on the same device in both cloud and edge deployments. Whether colocation succeeds or violates SLOs depends on the temporal overlap of kernels from concurrently executing models -- an effect that existing serving systems either ignore or approximate using aggregate resource profiles that fail to capture temporal dynamics. This paper presents Roomie, a model serving orchestration architecture that predicts and avoids kernel-level interference between colocated DNNs. Roomie decouples offline kernel profiling from online interference prediction. It uses profiling only to extract per-kernel resource configurations, and predicts interference with an occupancy-based analytical model immune to profiler-induced timing distortion. A pairwise greedy heuristic then approximates multi-model interference in polynomial rather than exponential time, and an online placement algorithm then uses these estimates to assign each incoming model to the GPU that minimizes predicted slowdown. Our experimental evaluation compares Roomie against state-of-the-art solutions across both cloud-grade server clusters and embedded edge devices, demonstrating that Roomie reduces SLO violations (i.e., inference latency) by up to 3x, while maintaining comparable, and in many cases superior, goodput relative to existing approaches. 2026-07-18T11:35:59Z Youssouph Faye Francescomaria Faticanti Shubham Jain Francesco Bronzino http://arxiv.org/abs/2607.16578v1 Hardware-Transparent I/O Governance in Disaggregated Heterogeneous Storage 2026-07-18T01:31:03Z Shared-nothing disaggregated storage clusters that serve both latency-sensitive databases and opaque block-volume workloads face two governance problems unsolved by existing schedulers: maintaining consistent performance across heterogeneous hardware generations, and enforcing global I/O limits when access patterns skew to a subset of storage nodes. We present the I/O Resource Manager (IORM), a multi-stage distributed scheduler deployed in production within Oracle Exadata Exascale. IORM combines three mechanisms: a hardware-aware cost modeler that normalizes I/O accounting using datasheet-derived fixed costs to make limits invariant across hardware generations; a quantum-based rate limiter with bounded carry-forward credits that accommodates database micro-bursts while enforcing long-term SLOs; and a distributed adaptive feedback controller that redistributes unused entitlements across the cluster to resolve topological access skew. Beyond design, we share operational lessons from production deployment. On an 8-node test cluster running up to 100 concurrent tenant volumes, IORM converges within 5\% of provisioned limits under extreme sequential skew, scales without inter-tenant interference, and recovers full throughput within 15 seconds of a storage-node failure. 2026-07-18T01:31:03Z 10 pages, 5 figures. Accepted at the IEEE International Conference on Cloud Engineering (IC2E) 2026 Rajarshi Chowdhury Akshay Shah Sue K. Lee http://arxiv.org/abs/2607.16408v1 Rethinking Polling Efficiency in Service Core Network Stacks 2026-07-17T18:02:05Z Idle network service cores are treated as wasted compute. This assumption motivates increasingly sophisticated mechanisms that reclaim idle cores at microsecond timescales. We argue that this view no longer matches modern server hardware. On contemporary multicore processors, active cores compete for a shared package level power and thermal budget. Once that budget becomes the limiting resource, an idle core that waits efficiently returns compute capacity that hardware can redistribute to productive work. Measurements on a recent AMD EPYC processor show how waiting strategy, processor topology, and idle duration determine this tradeoff. Our results suggest that reclaiming idle cores often yields less benefit than commonly assumed while introducing substantial scheduling complexity. We propose a budget centric view of service core systems in which power, rather than core occupancy, becomes the fundamental resource and waiting policy becomes a first class systems design choice. 2026-07-17T18:02:05Z Matheus Stolet Simon Peter Antoine Kaufmann http://arxiv.org/abs/2607.15569v1 Scaling Unmodified Multithreaded Applications with Elastic CXL-based Distributed Shared Memory 2026-07-17T02:24:47Z While CXL presents a promising hardware substrate for Distributed Shared Memory (DSM), seamlessly scaling multithreaded applications across multiple nodes remains a formidable challenge. Existing CXL-based DSMs fall short: they require manual code modifications to share non-heap data, employ rigid data placement policies that fail under diverse and dynamic workloads, and suffer from severe page-fault processing overheads in sub-microsecond ($μ\mathrm{s}$) environments. We present xDSM, a full-space, elastic DSM system built over CXL that transparently scales unmodified multithreaded applications. To eliminate the burden of manual code rewrites, xDSM employs an OS-runtime co-design that establishes a globally coordinated address space, seamlessly sharing all memory segments. To mask CXL access penalties, xDSM abandons static placement rules in favor of a dynamic, latency-driven policy that actively balances data between local DRAM and CXL memory. Finally, to resolve the fundamental tension between high base-page fault overheads and severe huge-page false sharing, xDSM introduces spatial locality-aware elasticity, dynamically coalescing and splitting pages on the fly to amortize processing costs. Evaluated across diverse workloads using 15 system configurations, xDSM outperforms CXL-only baselines by 1.5$\times$ to 2.2$\times$ and state-of-the-art hybrid DSMs by 1.1$\times$ to 2.2$\times$, while achieving near-linear scalability. 2026-07-17T02:24:47Z 15 pages, 8 figures Guowei Liu Kang Chen Laiping Zhao Yiming Li Hanwen Liu Chen Peng Yichi Chen Sheng Chen Zhiyuan Su Wenyu Qu