Sharpen the Spec, Cut the Code: A Case for Generative File System with SYSSPEC
Qingyuan Liu, Mo Zou, Hengbin Zhang, Dong Du, Yubin Xia, Haibo Chen
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
它引用的顶会 Paper16
- AutoCodeRover: Autonomous Program ImprovementYuntong Zhang, Haifeng Ruan, Zhiyu Fan, Abhik RoychoudhuryISSTA 2024 · 被引用 96 次
- CodeT: Code Generation with Generated TestsBei Chen, Fengji Zhang, Anh Nguyen, Daoguang Zan 等ICLR 2023 · 被引用 64 次
- Anvil: Verifying Liveness of Cluster Management ControllersXudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma 等OSDI 2024 · 被引用 50 次
- SpecGen: Automated Generation of Formal Program Specifications via Large Language ModelsLezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie 等ICSE 2025 · 被引用 25 次
- API-Driven Program Synthesis for Testing Static Typing ImplementationsThodoris Sotiropoulos, Stefanos Chaliasos, Zhendong SuPOPL 2024 · 被引用 15 次
相关 Paper
- From Commands to Prompts: LLM-based Semantic File System for AIOSZeru Shi, Kai Mei, Mingyu Jin, Yongye Su 等ICLR 2025
- OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System VerificationShangyu Li, Juyong Jiang, Tiancheng Zhao, Jiasi ShenAAAI 2026 · 被引用 10 次
- SpecAgent: A Speculative Retrieval and Forecasting Agent for Code CompletionGeorge Ma, Anurag Koul, Qi Chen, Yawen Wu 等ACL 2026 · 被引用 3 次
- Automated Repair of Ambiguous Problem Descriptions for LLM-Based Code GenerationHaoxiang Jia, Robbie Morris, He Ye, Federica Sarro 等ASE 2025 · 被引用 6 次
- SpecMind: Cognitively Inspired, Interactive Multi-Turn Framework for Postcondition InferenceCuong Chi Le, Minh V. T. Pham, Tung Duy Vu, Cuong Duc Van 等ACL 2026 · 被引用 2 次
