operating system developers

Abstract: hones and laptops now mix several kinds of cores, and each kind sits in its own voltage and clock domain. When a light thread arrives, should it run beside heavy threads on a fast cluster that is already awake, or wake a cluster of efficient cores? We answer with three costs. A thread can \emph{ride} an awake domain at the voltage other threads hold, \emph{raise} that voltage for everyone, or \emph{wake} a sleeping domain and pay its fixed power. From these costs follows a simple rule: ride while the thread's demand is below $r^*=Φ/(e_h-e_l)$, the fixed power of the cluster it would wake over the gap in energy per operation; otherwise wake the smallest tier that can serve it. The best tier is not monotone in demand: tiny threads ride high, medium threads wake a low tier, heavy threads go high again. Two common designs err on opposite sides of the rule: grouping a light thread with the heavy threads of its application overpays above the threshold, and an energy model without idle costs overpays below it. In a model with five tiers, grouping costs 80 to 145\% more energy than the rule, and more as tiers are added. Measurements on an Apple M6 anchor the parameters.

Abstract: We give an O(log k)-competitive randomized algorithm for weighted paging with delay. This improves upon the O(log k log n)-competitive algorithm of Gupta, Kumar, and Panigrahi (STOC 2020, SICOMP 2022) by removing the dependence on the number n of pages. Without delay, the optimal competitive ratio of randomized algorithms is Theta(log k), and since the lower bound carries over, our bound is tight. Our algorithm is fractional and combines mirror descent, used by Bubeck et al. (STOC 2018) for weighted paging without delay, with preemptive service, introduced by Azar et al. (STOC 2017) for online service with delay: when a request is served, an increase in the mirror descent potential is offset by preemptive service to other pending requests, with a budget derived from the mirror descent path. To obtain a randomized algorithm, we use the online rounding of Bansal, Buchbinder, and Naor (FOCS 2007) from classical paging.

Abstract: In this paper, we study online paging with delay or deadlines. In online paging with delay, an online algorithm manages a cache of size $k$ and needs to serve incoming requests by adding the requested pages to the cache. In addition, it has the option to delay serving incoming requests at a cost that depends on the delay. We propose a new online algorithm, which combines a threshold rule with first-in, first-out (FIFO) replacement, and show that it is $(2k+2)$-competitive for cache size $k$. This result corrects a previously published claim that the competitive ratio is exactly $2k+1$ regardless of the number of holes (pages outside the cache). However, in the case of one hole, we show that the FIFO rule with a different threshold is indeed $(2k+1)$-competitive, giving a tight result. In the case of deadlines, the same analysis gives a deadline-triggered algorithm that is $(k+1)$-competitive in general and $k$-competitive if there is only one hole. Moreover, we show that the second hole makes paging with deadlines strictly harder than classical paging, where the competitive ratio is independent of the number of holes. For paging with deadlines, we prove a deterministic lower bound of $k+\tfrac12$, already for two holes. We show that, as a consequence, no threshold-triggered algorithm can achieve a competitive ratio less than $2k+\frac32$ in general.

Abstract: In recent years, information systems have become the social infrastructure, so that their security must be improved urgently. In this paper, we introduce the results of the survey of virtualization, operating system verification and access control technologies in association with the design requirements of the reference monitor. Additionally, we show the prospects and challenges for each technology.

Abstract: Agentic systems use large language models (LLMs) to carry out concrete tasks. Prior work often borrows abstractions such as scheduling, caching or isolation piecemeal from operating systems, so the mechanisms it builds share little common ground, and the shared view of the two forms of agentic system, Workflows and Agents, is limited. We construct an abstract machine that provides both. We treat the LLM as an Oracle and extend a two-stack pushdown automaton with one instruction, which hands the Oracle a whole stack as its query and appends the answer to that same stack. The machine thus performs two computations, the Oracle's and a Turing-complete one that we call the Priestess. A stack that the program only appends to grows autoregressively, as an agent's context does. Two symmetry breakings, S in storage and T in transitions, make a Priestess program the operating system of the programs the Oracle runs, and produce the Agent and the Workflow as the two placements of a task's program. For internally autoregressive Oracles, the two computations synchronize at the end of every answer under certain conditions, and through that synchronization we model caching and analyse scheduling. No guarantee that holds for every Oracle can fix which content crosses between the two computations, but such a guarantee does fix the boundary itself. The construction V fits the machine to a von Neumann computer. To show that it is realizable, we propose ArchNights, an extended RISC-V ISA and a Linux-style operating system implementing the machine by design. ArchNights-SE runs on gem5 as a computer system, becomes an agentic system when it runs an LLM as the Oracle, and will be open source. Agentic systems can then be designed as computer systems are. With a foundation built and a unified view, future work can share invariants and bounds, each with its conditions.

Abstract: Address translation is a major bottleneck in data-intensive workloads. TLB prefetching can hide translation latency, but existing spatial prefetchers struggle with irregular accesses, while temporal prefetchers store address deltas in fixed-capacity hardware that cannot scale with application memory footprints. Our characterization of 200 translation-intensive workloads reveals that each virtual memory region has a small, recurring set of deltas, and over 94% of deltas fit in 18 signed bits. We introduce Trail, a temporal TLB prefetcher that stores deltas in unused bits of leaf page table entries (PTEs). When a region triggers a page table walk, Trail identifies the region that last triggered a walk from the same instruction and records their delta in that source region's PTE. When a later walk fetches the source region's PTE cache block, Trail retrieves its deltas without additional memory accesses and prefetches translations for likely destination regions into the TLBs and cache hierarchy. Storing multiple deltas per PTE cache block improves coverage, while using existing PTE bits allows metadata capacity to scale with the application's memory footprint without additional metadata storage. Across 200 workloads and 100 multiprogrammed mixes, Trail improves single-core (four-core) performance by 5.7% (11.5%) on average over a baseline without TLB prefetching, outperforming the best prior standalone TLB prefetcher by 1.7% (2.5%). Trail requires only a 64-entry hardware table to track per-instruction page table walk history. Trail is freely available at https://github.com/CMU-SAFARI/Virtuoso/tree/trail-artifact-release.

Abstract: Translation Lookaside Buffers (TLBs) play a critical role in hardware-supported memory virtualization. To speed up address translation and reduce costly page table walks, TLBs cache a small number of recently-used virtual-to-physical address translations. TLBs must make the best use of their limited capacities. Thus, TLB entries with low potential for reuse should be replaced by more useful entries. This paper contributes to an aspect of TLB management that has received little attention in the literature: replacement policy. We show how predictive replacement policies can be tailored toward TLBs to reduce miss rates and improve overall performance. We begin by applying recently proposed predictive cache replacement policies to the TLB. We show these policies do not work well without considering specific TLB behavior. Next, we introduce a novel TLB-focused predictive policy, Control-flow History Reuse Prediction (CHiRP). This policy uses a history signature and replacement algorithm that correlates to known TLB behavior, outperforming other policies. For a 1024-entry 8-way set-associative L2 TLB with a 4KB page size, we show that CHiRP reduces misses per 1000 instructions (MPKI) by an average 28.21% over the least-recently-used (LRU) policy, outperforming Static Re-reference Interval Prediction (SRRIP), Global History Reuse Policy (GHRP) and SHiP, which reduce MPKI by an average of 10.36%, 9.03% and 0.88%, respectively.

Abstract: Modern cache replacement designs saturate because they operate within fixed representational structures, hand-crafted and heuristic based feature-engineered predictors, or offline imitation models that cannot generate new decision logic on their own. At the same time, replacement is shaped by the causal interaction of prefetching, thrashing, spatial locality, and access-type behavior, producing an enormous design space that is difficult to traverse manually. Prior approaches typically rely on heuristics, parameter tuning, or imitation of an offline optimal policy, capturing correlations rather than synthesizing new mechanisms. As a result, their performance gains often plateau and they overfit under dynamic workload conditions. CACHEFORGE is the first framework to evolve cache-replacement policies end-to-end by embedding a large language model inside a governed hardware-aware loop. In each iteration, the LLM proposes new C++ replacement logic, the policy is evaluated under a trace-based CRC-2 ChampSim simulator, and the framework enforces feasibility through reward shaping, structural checks, dynamic mutation, temperature scheduling, and cross-policy crossover. This closed-loop generation-evolution loop specifically designed for cache replacement policy enables the discovery of compact policies that satisfy hardware constraints while exploring algorithmic transformations beyond fixed predictor structures. Across SPEC CPU2006, CACHEFORGE outperforms all CRC-2 baselines. It improves the total hit rate by 27.36%, 19.69%, 13.72%, 13.15%, 11.83%, and 5.73% over MPPPB, ReD, Hawk-eye, SHiP++, LIME, and LRU, respectively. On memory-intensive workloads, it increases IPC by 10.15%, 7.89%, 6.34%, 3.64%, 3.12%, and 2.71% over LRU, MPPPB, LIME, ReD, SHiP++, and Hawkeye.

Abstract: We give a new multiplication algorithm for tristate numbers improving upon the state-of-the-art implementation from the Linux kernel in terms of precision and formal proofs. Our algorithm is significantly more precise as shown by experimental evaluation (at the peak, giving better results in 95.59% cases compared to the previous work for 31-bit samples). Importantly, we achieve this additional precision with performance comparable to the previous algorithm, as demonstrated by benchmarks. Finally, we formalize and prove the soundness of the algorithm in the Rocq proof assistant, adding to the trust in the resulting implementation. Our algorithm is now part of the upstream Linux kernel. Our soundness proof in Rocq for the new multiplication algorithm works for all bit widths, while the SAT/SMT-based machine-checked proof accompanying the previous algorithm was restricted to 8 bits. We also provide Rocq proofs for the soundness and optimality of the newly added tnum union operation and the existing tnum addition algorithm from the Linux kernel. Our optimality proof for tnum addition presents a simpler and straightforward lemma compared to prior work.

Abstract: We present an efficient linkage-based model for in-process compartmentalization built on CHERI memory safety, which enables fine-grained compartmentalization of the entire UNIX user-space, scaling to 10K+ compartments on desktop systems. The model's "push-button" compartmentalization along existing library boundaries regularly hosts 500+ compartments per process for large applications such as Chromium, far exceeding the number of concurrently available protection domains supported by other mechanisms (e.g., up to 16 for Intel MPK). Custom policies can further subdivide libraries. Of the thousands of C/C++ programs tested, only the V8 JavaScript engine required source-level adaptation (<300 lines of changed code concerning garbage collection and JIT compilation). We implement the model for CHERI-extended versions of Armv8-A and RISC-V through support in the compiler toolchain and operating system. Case studies illustrate the smooth delegation of memory between compartments, compartment-aware debugging and visualization, as well as extensibility to a complex managed language runtime, demonstrating the benefits of our single-address-space model. We evaluate using multiple processors, including Arm's superscalar Morello and, notably, the first commercial CHERI-enabled RISC-V application core---Codasip's in-order dual-issue X730.

Abstract: Large language model agents are now privileged principals that take consequential actions: editing code repositories, operating inboxes, completing purchases. Their authority is kernel-grade, but it comes without what classical systems security requires: a trusted mediator interposed on every access. Operating-system vendors are now rebuilding the platform around this de-facto agent kernel, inheriting complete mediation as a design problem. We systematize the security of such systems around a single distinction: a crossing mediated over provenance admits a deterministic check, while one over content semantics does not. A trust-boundary taxonomy locates where mediation must occur and isolates the central mediation gap at two kinds of semantic judgment: distinguishing data from instruction in untrusted input, and an authorized action from an unauthorized one. We argue that this gap leaves an irreducible residual of undetected attacks wherever inputs and actions are not restricted in advance to an enumerated set. The same distinction makes attack-success statistics actionable, placing each number on a spectrum from deployment debt (a sound deterministic mediator left unused) to a structural gap (no such mediator known). We systematize defenses across runtime monitoring, architectural separation, and authorization, and show that current evaluations tend to overstate deployed security through evaluation-validity failures. Finally, we carry that analysis forward beyond the de-facto kernel, to an architecture in which the model itself becomes the arbitration core, and derive the design constraints, open challenges, and research agenda for a security-first AI-native OS.

Abstract: Commercial security gateways repeatedly ship implementation bugs in the code path between the network and the policy decision: hand-written enforcement logic that diverges from the policy author's intent, and ad-hoc request parsers at the network boundary that introduce memory-safety flaws of their own. In both cases the bug is in the deployed enforcement code, not in the policy. Existing approaches either leave the enforcement runtime unverified or connect a formal model to a hand-written engine only by differential testing. Our contribution is a class result: a forward-only, backtrack-free EverParse validator is a verified recognizer for a bounded, finite-state class, and access-control decision functions with fixed-offset fields and bounded disjunction belong to it, so one machine-checked proof transfers to every policy in the class rather than being re-established per policy. Concretely, we encode a bounded policy language's decision function into a fixed-size byte buffer and verify the enforcement code once---covering all byte values---with an SMT solver, proving the validator accepts if and only if the decision function accepts, for every policy, request, and session. Editing rule content over a fixed endpoint set then needs no new proof; adding endpoints reruns the toolchain; extending the language needs new proofs. We establish faithful enforcement of a policy, not that a policy is itself secure. The verified gate is platform-independent, requiring only EverParse/Z3 and a C compiler, whose correctness we assume. We demonstrate a deployment on the seL4 microkernel, which ensures every request passes through the gate and that unverified components cannot corrupt the verified enforcement chain.

Abstract: GPU-backed LLM servers often multiplex interactive requests with background batch work on the same CPUs. During a request burst, the scheduler should protect time-to-first-token; between bursts, it should let background work make progress. A fixed kernel policy leaves one of these objectives on the table, so agentic OS control needs a way to switch scheduler behavior as the workload changes. The hard part is not deciding that a switch is useful, but applying it safely and fast enough for the kernel. Scheduler events occur every 1-10 $μ$s, and any code that runs there must satisfy the eBPF verifier. Scalar knobs are fast but expose only limited policy behavior, while generating new eBPF policy code is expressive but puts compilation, verification, loading, and possible verifier rejection on the runtime path. We present AKTS, which verifies a policy library once, at load time, and reduces the agent's runtime action to writing an integer index into an in-kernel array of preverified policies. An in-kernel tail call resolves that index. Because the agent emits an index rather than code, verifier failure is not a runtime outcome. On Linux 6.14, AKTS applies a policy switch in 920 ns (p50), matching scalar writes while switching whole policies; makes an invalid index inert across 60,217 invocations on an attached scheduler; and switches policies in a vLLM workload to capture 97% of a throughput policy's batch work while matching a latency policy's burst response.

Abstract: We propose CHERI-D Reincarnate (Reinc), an architectural extension to CHERI for scalable and efficient temporal memory safety. Prior work CHERI-D has a finite-width generation ID stored at a fixed location, requiring an object to be quarantined when its ID is exhausted. Reinc further provides use-after-free mitigation while permitting immediate freed memory reuse for objects through allocation reincarnation: rather than quarantining an allocation slot upon ID exhaustion, Reinc dynamically assigns a new ID to that slot when its current ID is exhausted. Exhausted IDs are quarantined and later reclaimed, while the underlying memory remains available for immediate reuse. By quarantining IDs rather than memory, Reinc enables continuous reuse of memory in the common case, substantially reducing both memory-sweep frequency and quarantine memory overhead. Reinc further introduces coherent ID caching while retaining a fully decentralized ID organization. Temporal metadata remains colocated with the memory it protects, preserving locality while avoiding centralized metadata structures. To support multicore execution, Reinc connects physical coherence events to the virtually addressed ObjID buffer using lightweight reverse-map and filter-based mechanisms. We implement Reinc as a hardware-software co-design spanning CHERI-Toooba (superscalar FPGA softcore), QEMU, LLVM/Clang and CheriBSD. Across our evaluated workloads, Reinc substantially reduces memory-sweep frequency and memory quarantine while incurring low performance and hardware overhead.

Abstract: Off-path network attacks against TCP and DNS (over UDP) client-server connections are generally considered impractical nowadays, due to built-in security features in these protocols, e.g. randomized TCP (initial) sequence numbers and randomized UDP source ports, respectively. In this work, we refute this presumption by demonstrating that an unprivileged malicious application running on the client (but practically off-path), when combined with a remote off-path adversary, can enable powerful network attacks against such connections. We show how such a local--remote collaboration between the malicious application and a remote adversary allows inference of sensitive connection state, including TCP sequence numbers and DNS stub-resolver UDP source ports. Our attacks exploit standard socket API calls such as bind(), protocol mechanisms such as IP options, and operating system features such as cBPF and procfs to infer the TCP initial sequence number (ISN) and the UDP source port in use by the connection of interest. Specifically, we take advantage of certain properties of the ISN generation algorithm as implemented in major operating systems. We demonstrate TCP connection hijacking in Linux, Android, Windows, macOS and iOS, and DNS cache poisoning against Windows, Android and the popular systemd-resolved DNS stub resolver in Linux. We evaluate our techniques across multiple operating systems and realistic deployment settings, including environments behind port-preserving NAT-integrated routers. We disclosed our techniques to Microsoft, Apple, Linux and Google, which led to the release of several patches.

Abstract: Caching systems often rely on simple eviction policies such as Least Recently Used (LRU) and Least Frequently Used (LFU), which perform well in complementary request regimes. Recent policies such as LeCar and Cacheus combine LRU and LFU using ideas from the experts problem in online learning. Specifically, upon a miss, they randomize between the two eviction rules using probabilities derived from scores updated by tracking the history of past evictions. While these policies exhibit strong empirical performance, it remains unclear whether they are guaranteed, on every request sequence, to perform asymptotically as well as the better of LRU and LFU, i.e., whether they achieve sublinear regret with respect to this benchmark. We first show that LeCar suffers linear regret against an oblivious adversary, even with unbounded history. We then propose H-MC, a Hedge-based mixture of virtual LRU and LFU caches that preserves Hedge's selection probabilities, and hence its regret guarantees, while minimizing the switching cost among all joint selection rules with these marginals.