非羊 整理自 凹非寺
量子位 | 公众号 QbitAI

还记得《流浪地球2》里的那台550W量子计算机吗？

电影里，MOSS最让人印象深刻的点，除了其强大算力，还有它可以根据需求，实时生成底层操作系统的能力。

如果现在告诉你，我们已经在从“人类需求”生成“底层系统”这件事上迈出了关键一步呢？

来自上海交大IPADS实验室的研究团队，面对自动生成操作系统核心组件的难题，做出了全新的尝试。这项研究成果也即将亮相文件系统与存储领域顶级学术会议USENIX FAST’26。

操作系统：与时俱进的沉重负担

操作系统（OS），是整个数字世界的基石。

向下，它要管理和调度硬件资源（CPU、内存、硬盘等）；向上，它要为应用软件提供稳定可靠的运行环境。无论是你手机上的App，还是云端强大的AI模型，都构建在这块基石之上。

然而，OS必须与时俱进，来满足硬件和应用的双重需求：

一方面，硬件的发展日新月异，例如存储设备，在短短数年内，就从机械硬盘演进到闪存甚至非易失性内存，OS必须快速迭代，才能榨干这些新硬件的性能；

另一方面，新应用也层出不穷，例如大数据分析、AI训练等，每一个新型应用的出现，都可能对OS的各种功能和性能提出新的要求，例如优先级调度、I/O性能等等。

这些与时俱进的需求，为操作系统带来了极其高昂的人力成本。开发者们往往需要付出巨大的精力来维护一个已经开发好的操作系统关键组件。

研究团队深扒了Linux操作系统的一个核心组件，Ext4文件系统，分析了其长达20年演进历史中的3000多个commit记录，并揭示了一个事实：
82.4%的代码提交，都投入到了Bug修复和代码维护中。真正的实现新功能的代码提交仅占5.1%左右。

开发一时爽，维护火葬场。高人力成本和低产出效率，正成为限制操作系统高效演进的重要原因。

“生成式操作系统”：梦想是否遥不可及？

既然人类维护不动了，让大模型上行不行？

现在的大模型写代码确实越来越强了，写个网页前端，小游戏，甚至打Codeforces比赛都不在话下。那么很自然的想法来了：我们能否打造一个“生成式操作系统”，让大模型来接手这项苦差事？

想象一下，你只需要告诉大模型：“我需要一个为新型网卡优化的、支持超低延迟网络的操作系统”，然后大模型就能自动生成一个完整的操作系统，不需要人力干预。如果这一美好幻想能实现，将给软件行业提供一种颠覆性的新范式。

然而，现实往往事与愿违。

用大模型写过代码的朋友们都知道，如果你真对大模型说：“请帮我生成一个支持高并发、崩溃一致性的操作系统”，它生成的代码大概率看起来很合理，但一运行即崩溃。

这是因为，操作系统往往高度复杂，而现有的大模型还难以应对这样的复杂性。

研究团队观察到，想用大模型生成操作系统，必须解决下面的三个关键挑战：

自然语言语义的局限性：自然语言提示词天生是模糊的。如果只说“要线程安全”，大模型理解和生成的锁机制可能漏洞百出。作为整个计算机系统的基座，操作系统难以容忍这样的不准确性。

系统架构模块的深度耦合性：操作系统模块繁多，模块间交互逻辑复杂，耦合极深。大模型受限于上下文窗口，只能管中窥豹，难以进行全局一致的设计，容易出现模块间的逻辑或接口对不上等问题。

并发控制逻辑的复杂性：实现细粒度的并发控制是操作系统面临的重要挑战，也是大部分操作系统开发者的噩梦。让大模型一边写功能逻辑，一边处理复杂的“避免死锁”的并发要求，这直接超出了现有大模型的能力上限。

用朴素的自然语言指导大模型生成操作系统，就像是纯靠工头用嘴巴指挥建筑工人造摩天大楼，倒塌是必然的。

SysSpec：给大模型的操作系统设计说明书

如何破局？

IPADS团队给出的答案是：如果自然语言的描述对大模型来说太过模糊，那就给它提供更加精确的设计说明书。

而这份说明书，正是基于计算机科学中的基础技术，形式化方法，来实现的。

形式化方法通常是一套用纯数学语言给程序定义严格语义约束的方法。在传统用法中，开发者需要写一份Specification（规约），用严谨的公式描述程序“必须做什么”以及“绝对不能做什么”，然后通过数学推导证明程序代码和规约是等价的。

只要证明通过，程序就在数学层面上被判定为Bug-free。这也是保障航空航天、核能、芯片等领域可靠性的关键技术。

基于此，研究团队有了一个逆向思维的洞察：既然规约如此精确，我们是否可以直接用它来指导生成，而不是事后验证呢？

没错，SysSpec就是这样的一种全新范式。开发者不需要再手搓容易出错的C语言代码，而是直接编写高维度的Specification。这套过程实际上是形式化方法的“逆过程”：不再由规约验证实现，而是由规约生成实现。

△SysSpec规约设计示意图

SysSpec提出了一整套结构化的规约编写框架，用数学般的逻辑告诉大模型如何实现一个操作系统模块：

功能规约（Functional Specification）：

引入霍尔逻辑（Hoare Logic），明确告诉大模型每个模块的功能是什么，包括执行前系统是什么状态（Pre-condition），执行后必须变成什么状态（Post-condition）等。

模块化规约（Modularity Specification）：

描述模块之间接口层面的依赖关系。大模型在生成A模块时，明确告诉它能依赖B模块提供的哪些保证。

并发规约（Concurrency Specification）：

SysSpec将业务逻辑与并发逻辑进行分离，先让大模型生成正确的串行代码，再根据专门的并发规约，把死锁、竞态条件等逻辑完成。让大模型一次只做一件事，效率反而更高。

SysSpec Toolchain：从规约到代码的自动化工具链

有了规约作为说明书，还需要工具实现从规约到代码的转换。研究团队为SysSpec配套了3个基于Agent的工具链：

△SysSpec工具链的执行过程

1. SpecCompiler：负责将SysSpec“编译”成C代码，通过先写逻辑、再加锁的方式大大降低生成难度。

2. SpecValidator：专门对抗大模型“幻觉”。它会反复迭代验证生成的代码是否符合SysSpec的规约，直到生成结果符合预期（或失败次数触发阈值）为止。

3. SpecAssistant：辅助开发者编写规约，降低上手门槛。

那么，最让人头疼的“系统演进”怎么办？

研究团队在SysSpec的基础上，提出了一项新的系统演进方法：DAG-Structured Spec Patch（基于有向无环图结构的规约补丁）。

系统演进中，我们需要对代码进行修改，过去让大模型改代码是越改越乱，而现在，改代码变成了改规约，修改的规约被组织成了一个有向无环图（DAG），每一个模块的修改本质上是一个图中的节点：

叶子节点负责定义局部的新逻辑；中间节点层层向上，利用下层提供的新保证（Guarantee）来构建更复杂的功能；根节点负责最终的一键集成。

这意味着，开发者只需要提交一个规约补丁，工具链就会自动计算依赖关系，把新的规约合并到原有实现里。这样，我们就只需重构代码中受影响的模块，从而确保生成的新功能不会破坏原有的系统实现。

△DAG结构化规约补丁

SpecFS：基于规约，实现系统软件的自动生成和演进

基于这套框架，研究团队以操作系统中的重要组成部分文件系统为例，构建了一个基于SysSpec规约的完整的文件系统：SpecFS。

SpecFS能够在开机时自动通过工具链，生成基于C语言的操作系统文件系统（无需人工干预），并且还支持根据用户特定需求和规约补丁实现自我演进。

生成的SpecFS实现，包含各种优化，总共约四千三百行代码。在Linux 6.1.10版本内核中的82个文件系统中，能够排到第42位。

团队还对SpecFS的能力进行了仔细的验证和评估。

首先是正确性验证：在xfstests测试套件下，SpecFS的正确性表现可与人类专家耗时许久手写的系统相媲美。

更值得一提的是它的演进能力。研究团队尝试给SpecFS添加了Ext4文件系统的10个复杂特性（如Extent、延迟分配、文件加密等）。

这些特性的引入只需要在SpecFS的规约层通过规约补丁的方式进行扩展。实验显示，新引入的特性能够有效提升文件系统性能。例如引入“延迟分配”（Delayed Allocation）特性后，SpecFS在完成编译xv6的任务时，写操作直接减少了99.9%！

研究团队还招募了实验室的硕博同学，对使用这套框架进行开发的效率进行测试：相比手动修改C代码，使用SysSpec演进能力的开发效率提升了3-5倍。

从“易错的底层代码”中解放出来

从Ext4文件系统的20年修补之路，到SpecFS的自动生成和演进，SysSpec展示了一种操作系统开发的未来范式（也是研究论文的标题）：
Sharpen the Spec, Cut the Code.

在生成式AI时代，程序员也许不再需要逐行敲击那些易错的底层代码，而是可以更多地关注在有趣的系统设计上，剩下的，就交给大模型去做吧！

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