Generative File Systems: Specification-Driven Synthesis and Evolution via LLMs

Le résumé fourni par la source

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 that facilitate the full lifecycle of file system generation with mechanisms to mitigate hallucination. We demonstrate our approach by generating SpecFS , a concurrent file system, in both C and Rust. 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.

Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.