Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2608.01135

Themis: A Filesystem Model Checker That Owns the Machine

Daeyeon Son
View original source ↗Read source document ↗Export metadata ↓

Abstract

Filesystem model checkers explore an unmodified in-kernel filesystem's state space to find bugs that escape unit tests. The state of the art, Metis, runs inside the OS: it drives syscalls, and, lacking a cheap way to snapshot in-kernel state from user space, it hand-codes a reference filesystem (RefFS) as its differential oracle and sets time aside as noise. Where a checker sits shapes what it can see. I present Themis, a filesystem model checker built beneath an unmodified in-kernel filesystem on a bare-metal Type-1 AMD-V hypervisor. Themis owns the machine: the virtual block device and the virtual clock under a stock Linux/ext2 guest. Ownership buys four things. (1) A machine-layer epsilon-copy fork whose restore cost is proportional to dirtied pages, not filesystem image size, so every unmodified filesystem becomes its own differential reference and no hand-coded reference is required. (2) Below-filesystem observation and byte-level whole-disk diffs with nuisance-field normalization. (3) Control of the clock, turning time into an explored search dimension. (4) The same fork, made re-armable, doubling as a checkpoint for bit-exact deterministic replay. Over a campaign of 40+ hardware runs on an AMD Zen5 9800X3D, the mechanism is proven end-to-end: a real ext2 write is served inside a fork window and fully reverted (DRAM, disk, and device state) in 9 microseconds for the dirtied set. The principal result is the clock: Themis drives real ext2 across a clock sweep and witnesses a real Y2038 defect, a 128-byte-inode clamp that a time-excluded fingerprint cannot register. A real ext2 workload replays whole-DRAM and whole-disk bit-exact across nine passes, and a timing-flaky outcome (nine distinct hashes raw) becomes reproducible when the clock is served (nine identical).

Explore related subjects

cs.OScs.SE

Keep this discovery

BibTeXRIS

Daeyeon Son. 2026-08-02. Themis: A Filesystem Model Checker That Owns the Machine. https://arxiv.org/abs/2608.01135

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Violet: Enabling Full Virtualization for M-mode RTOS on RISC-V

In embedded systems, complex configurations may be required, such as the simultaneous execution of a real-time operating system (RTOS) and a general-purpose operating system (GPOS), or the operation of multiple RTOS instances. Embedded system hypervisors have been studied and developed to meet these requirements for architectures like ARM and x86. RISC-V is experiencing growing adoption in embedded systems and faces similar needs. However, RISC-V's virtualization support targets only U-mode (where applications run) and S-mode (where general-purpose OSs run) as virtualization levels. The M-mode, where RTOSs like FreeRTOS or Zephyr run, is excluded from virtualization. This means that, similar to architectures like ARM, running an RTOS on a Virtual Machine (VM) using methods based on virtualization support features is impossible. Therefore, this paper proposes the Violet hypervisor. Violet combines RISC-V's virtualization features with software-based emulation, enabling the execution of unmodified M-mode RTOSs. Evaluation verified the validity of the M-mode emulation functionality using RISC-V architecture tests. Furthermore, this was implemented on the SiFive HiFive Premier P550 hardware, demonstrating that existing RTOSs can run on Violet's VM and that coexistence with GPOSs like Linux is also possible. The performance evaluation also quantified the overhead introduced by M-mode emulation on M-mode CSR accesses, timer interrupt latency, and context switching.

cs.OS↗
arXiv2026

AutoUVM: Automated Prefetching Framework for LLMs under UVM Oversubscription

Large language models (LLMs) increasingly exceed the memory capacity of commodity GPUs, making memory oversubscription common in practical deployments. NVIDIA Unified Virtual Memory (UVM) provides transparent access to host memory, but its page-fault-driven migrations introduce severe performance overhead. While UVM exposes primitives (e.g., prefetching and placement hints) to mitigate these costs, they require low-level CUDA modifications, limiting their applicability for most LLM users. Meanwhile, existing UVM optimizations operate at coarse managed-object granularity and fail to capture deep learning frameworks' internal tensor-level memory behavior, leading to excessive data movement and CPU-GPU interconnect bottlenecks. We propose AutoUVM, an automated, framework-aware UVM prefetching system for efficient LLM execution under memory oversubscription. AutoUVM bridges the semantic gap between deep learning frameworks and UVM by exposing tensor-level access information and enabling policy-driven prefetching at fine granularity. Implemented as a transparent extension, AutoUVM requires no changes to model code and dynamically adapts to runtime memory pressure. We instantiate AutoUVM with a roofline-inspired policy to identify performance-critical data transfers. Across ten LLMs, AutoUVM achieves an average 3.1x speedup over baseline UVM and consistently surpasses the best-performing prior UVM prefetcher by 1.9x, with improvements of up to 4.7x over object-level prefetchers, while significantly reducing page faults.

cs.OS↗
arXiv2026

Adaptive Context Parallelism for Production LLM Serving

As LLM context windows expand and input sequences grow longer, serving systems face increasing computational and memory demands. Context parallelism (CP), which partitions the input sequence across multiple ranks to parallelize the computation, has therefore become increasingly important for efficient LLM serving. However, existing CP-enabled systems either rely on static CP configurations or adjust the CP degree only for active requests or batches. In this paper, we present Vertumnus, an adaptive CP serving system designed for heterogeneous and evolving workloads. At the request level, Vertumnus routes requests among workers with different CP degrees using a placement cost that combines predicted queuing delay, cache-aware prefill time, and GPU-time cost. At the cluster level, Vertumnus adapts the worker composition through seconds-scale split and merge operations as workload demand changes. Vertumnus further introduces a global prefix-cache management policy that coordinates cache placement and replication among workers with the same or different CP degrees, preserving cache locality as request assignments and worker composition change. Experiments on a 64-GPU cluster with public and production workloads show that, under the highest evaluated loads, Vertumnus reduces mean TTFT by up to 28.1% and improves token-weighted SLO attainment by up to 13.3 percentage points over the strongest baseline.

cs.OS↗