还记起《流浪地球 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 时间，方法员也许不再需要逐行敲击那些易错的底层代码，而是不错更多地温雅在真谛的系统计算上，剩下的，就交给大模子去作念吧！

SpecFS 生成演示视频：

arXiv 一语气：https://arxiv.org/abs/2512.13047

一键三连「点赞」「转发」「防御心」

迎接在驳斥区留住你的见识！

—  完  —

咱们正在招聘又名眼疾手快、温雅 AI 的学术裁剪实习生  � �

感酷好的小伙伴迎接温雅 � �  了解细目

� � 点亮星标 � �

科技前沿进展逐日见