arXiv subjects

Hengbin Zhang

Publications and source records attributed to Hengbin Zhang.

6 recordsLinked to original sources

arXiv2026

OSFoundry: Building and Evolving Operating Systems with Specification-Guided Agents

Operating systems must evolve continuously. Yet their development remains code-centric and largely manual: even a localized change can require recovering implicit assumptions, coordinating multiple subsystems, and repeatedly building, booting, testing, and debugging the complete system. General-purpose coding agents automate individual edits, but their prompt-centric workflows repeatedly reconstruct task boundaries and OS semantics from scattered context, limiting their reliability for sustained OS evolution. This paper presents OSFoundry, an OS-specialized agent harness that makes design intent persistent throughout OS development. Its key insight is to separate stable intent from diverse implementation. Instead of relying on free-form natural-language prompts to convey design intent, OSFoundry uses SysSpec*, a shared development blueprint comprising a task-bounding Plan and an OS-specific Specification: the Plan bounds what a change should achieve, while the Specification records the interfaces, modular dependencies, and concurrency semantics that its implementation must preserve. Agents implement and validate code against this same blueprint, refining both SysSpec* and the implementation when execution or review exposes a mismatch. We evaluate OSFoundry along three ways. First, OSFoundry generates SpecOS from SysSpec*; the resulting complete OS boots and passes all 70 functional tests. Second, specification patches evolve SpecOS with a GUI and three performance optimizations that improve performance by up to 4.41x. Third, across 11 recent Linux-kernel bug-fix tasks, OSFoundry achieves 1.8x the accuracy of Codex using GPT-5.5. These results show that persistent specifications can shift OS construction and evolution from repeated manual kernel engineering toward specification-guided development.

cs.OS↗

arXiv2026

Sharpen the Spec, Cut the Code: A Case for Generative File System with SYSSPEC

File systems are critical OS components that require constant evolution to support new hardware and emerging application needs. However, the traditional paradigm of developing features, fixing bugs, and maintaining the system incurs significant overhead, especially as systems grow in complexity. This paper proposes a new paradigm, generative file systems, which leverages Large Language Models (LLMs) to generate and evolve a file system from prompts, effectively addressing the need for robust evolution. Despite the widespread success of LLMs in code generation, attempts to create a functional file system have thus far been unsuccessful, mainly due to the ambiguity of natural language prompts. This paper introduces SYSSPEC, a framework for developing generative file systems. Its key insight is to replace ambiguous natural language with principles adapted from formal methods. Instead of imprecise prompts, SYSSPEC employs a multi-part specification that accurately describes a file system's functionality, modularity, and concurrency. The specification acts as an unambiguous blueprint, guiding LLMs to generate expected code flexibly. To manage evolution, we develop a DAG-structured patch that operates on the specification itself, enabling new features to be added without violating existing invariants. Moreover, the SYSSPEC toolchain features a set of LLM-based agents with mechanisms to mitigate hallucination during construction and evolution. We demonstrate our approach by generating SPECFS, a concurrent file system. SPECFS demonstrates equivalent level of correctness to that of a manually-coded baseline across hundreds of regression tests. We further confirm its evolvability by seamlessly integrating 10 real-world features from Ext4. Our work shows that a specification-guided approach makes generating and evolving complex systems not only feasible but also highly effective.

cs.OS↗

arXiv2022

Symplectic inner product graphs and their automorphisms

A new graph, called the symplectic inner product graph $Spi\big(2ν,q\big)$, over a finite field $\mathbb{F}_q$ is introduced. We show that $Spi\big(2ν,q\big)$ is connected with diameter $4$ if and only if $ν\geq2$ and the automorphism group of $Spi\big(2ν,q\big)$ is determined. Two necessary and sufficient conditions for two vertices of $Spi\big(2ν,q\big)$ and two edges of $Spi\big(2ν,q\big)$ respectively are in the same orbit under the action of the automorphism group of $Spi\big(2ν,q\big)$ are obtained.

math.CO↗

arXiv2022

Orthogonal inner product graphs of odd characteristic and their automorphisms

Let $\mathbb{F}_q$ be a finite field of odd characteristic and $2ν+δ\geq2$ an integer number with $δ=0,1$ or $2$. The orthogonal inner product graph $Oi\big(2ν+δ,q\big)$ over $\mathbb{F}_q$ is defined and the automorphism groups of $Oi\big(2ν+δ,q\big)$ are determined. We show that $Oi\big(2ν+δ,q\big)$ is a disconnected graph if $2ν+δ=2$; otherwise it is not. Moreover, we have two necessary and sufficient conditions for two vertices of $Oi\big(2ν+δ,q\big)$ and two edges of $Oi\big(2ν+δ,q\big)$ respectively are in the same orbit under the action of the automorphism group of $Oi\big(2ν+δ,q\big).$

math.CO↗

arXiv2020

A note on the zero divisor graph of the ring of Lipschitz integers modulo $n$

In a recent paper, Grau et al. (2017) studied the zero divisor graphs of the ring of Lipschitz integers modulo $n$, and computed the domination number of the undirected zero divisor graph of the ring of Lipschitz integers modulo $n$. But the case $n$ is a power of prime numbers remained open. In this note, this problem is solved. We also show the automorphism group of the zero divisor graph of the ring of Lipschitz integers modulo $2^s$.

math.CO↗

arXiv2015

Modeling Multi-wavelength Pulse Profiles of Millisecond Pulsar PSR B1821-24

PSR B1821$-$24 is a solitary millisecond pulsar (MSP) which radiates multi-wavelength pulsed photons. It has complex radio, X-ray and $γ$-ray pulse profiles with distinct peak phase-separations that challenge the traditional caustic emission models. Using the single-pole annular gap model with suitable magnetic inclination angle ($α=40^\circ$) and viewing angle ($ζ=75^\circ$), we managed to reproduce its pulse profiles of three wavebands. It is found that the middle radio peak is originated from the core gap region at high altitudes, and the other two radio peaks are originated from the annular gap region at relatively low altitudes. Two peaks of both X-ray and $γ$-ray wavebands are fundamentally originated from annular gap region, while the $γ$-ray emission generated from the core gap region contributes somewhat to the first $γ$-ray peak. Precisely reproducing the multi-wavelength pulse profiles of PSR B1821$-$24 enables us to understand emission regions of distinct wavebands and justify pulsar emission models.

astro-ph.SR↗