AI生成操作系统新突破！上海交大提出文件系统开发新范式：从此只需写规约

还记得《流浪地球2》中的550W量子计算机吗？它不仅能提供强大算力，还能根据需求实时生成底层操作系统。如今，这一科幻场景正逐步成为现实。上海交大IPADS实验室团队提出了一种全新的文件系统开发范式，研究成果即将亮相顶级学术会议USENIX FAST’26。

操作系统是数字世界的基石，向下管理硬件资源，向上为应用软件提供运行环境。然而，随着硬件和应用的快速发展，操作系统维护成本居高不下。研究团队分析了Linux Ext4文件系统的3000多个代码提交记录，发现82.4%的精力用于Bug修复和代码维护，仅5.1%用于实现新功能。这种低效模式严重制约了操作系统的演进。

那么，能否让大模型自动生成操作系统？尽管当前大模型在编写简单代码时表现出色，但面对操作系统这样高度复杂的系统，却难以胜任。主要挑战包括自然语言语义模糊、模块间深度耦合以及并发控制逻辑复杂等问题。

为此，IPADS团队提出了SysSpec——一种基于形式化方法的新范式。开发者无需手写易错的底层代码，而是通过编写精确的规约（Specification），指导大模型生成代码。SysSpec采用霍尔逻辑描述功能规约，明确模块执行前后的状态；通过模块化规约定义模块间依赖；并通过分离业务与并发逻辑，降低生成难度。

为实现从规约到代码的自动化，团队开发了SysSpec Toolchain工具链，包括SpecCompiler（将规约编译为C代码）、SpecValidator（验证生成代码是否符合规约）和SpecAssistant（辅助编写规约）。此外，团队还提出DAG-Structured Spec Patch方法，通过修改规约而非代码，实现系统的高效演进。

基于SysSpec框架，团队构建了一个完整的文件系统SpecFS。SpecFS能够自动生成约四千三百行C代码，并支持根据用户需求进行自我演进。实验表明，SpecFS在正确性测试中媲美人类专家编写系统，且通过引入“延迟分配”等特性，性能显著提升，例如写操作减少了99.9%。相比手动修改代码，使用SysSpec的开发效率提升了3-5倍。

从Ext4文件系统的漫长修补史到SpecFS的自动生成，SysSpec展示了未来操作系统开发的全新范式：“Sharpen the Spec, Cut the Code”。在生成式AI时代，程序员或将从繁琐的底层代码中解放出来，专注于系统设计，让大模型完成剩余工作。

arXiv链接：https://arxiv.org/abs/2512.13047