非羊 整理自 凹非寺

量子位 | 公众号 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

— 完 —

量子位 QbitAI

关爱咱们云开体育，第一时辰获知前沿科技动态