非羊 整理自 凹非寺
量子位 | 公眾號(hào) QbitAI

還記得《流浪地球2》里的那臺(tái)550W量子計(jì)算機(jī)嗎？

電影里，MOSS最讓人印象深刻的點(diǎn)，除了其強(qiáng)大算力，還有它可以根據(jù)需求，實(shí)時(shí)生成底層操作系統(tǒng)的能力。

如果現(xiàn)在告訴你，我們已經(jīng)在從“人類(lèi)需求”生成“底層系統(tǒng)”這件事上邁出了關(guān)鍵一步呢？

來(lái)自上海交大IPADS實(shí)驗(yàn)室的研究團(tuán)隊(duì)，面對(duì)自動(dòng)生成操作系統(tǒng)核心組件的難題，做出了全新的嘗試。這項(xiàng)研究成果也即將亮相文件系統(tǒng)與存儲(chǔ)領(lǐng)域頂級(jí)學(xué)術(shù)會(huì)議USENIX FAST’26。

操作系統(tǒng)：與時(shí)俱進(jìn)的沉重負(fù)擔(dān)

操作系統(tǒng)（OS），是整個(gè)數(shù)字世界的基石。

向下，它要管理和調(diào)度硬件資源（CPU、內(nèi)存、硬盤(pán)等）；向上，它要為應(yīng)用軟件提供穩(wěn)定可靠的運(yùn)行環(huán)境。無(wú)論是你手機(jī)上的App，還是云端強(qiáng)大的AI模型，都構(gòu)建在這塊基石之上。

然而，OS必須與時(shí)俱進(jìn)，來(lái)滿足硬件和應(yīng)用的雙重需求：

一方面，硬件的發(fā)展日新月異，例如存儲(chǔ)設(shè)備，在短短數(shù)年內(nèi)，就從機(jī)械硬盤(pán)演進(jìn)到閃存甚至非易失性內(nèi)存，OS必須快速迭代，才能榨干這些新硬件的性能；

另一方面，新應(yīng)用也層出不窮，例如大數(shù)據(jù)分析、AI訓(xùn)練等，每一個(gè)新型應(yīng)用的出現(xiàn)，都可能對(duì)OS的各種功能和性能提出新的要求，例如優(yōu)先級(jí)調(diào)度、I/O性能等等。

這些與時(shí)俱進(jìn)的需求，為操作系統(tǒng)帶來(lái)了極其高昂的人力成本。開(kāi)發(fā)者們往往需要付出巨大的精力來(lái)維護(hù)一個(gè)已經(jīng)開(kāi)發(fā)好的操作系統(tǒng)關(guān)鍵組件。

研究團(tuán)隊(duì)深扒了Linux操作系統(tǒng)的一個(gè)核心組件，Ext4文件系統(tǒng)，分析了其長(zhǎng)達(dá)20年演進(jìn)歷史中的3000多個(gè)commit記錄，并揭示了一個(gè)事實(shí)：
82.4%的代碼提交，都投入到了Bug修復(fù)和代碼維護(hù)中。真正的實(shí)現(xiàn)新功能的代碼提交僅占5.1%左右。

開(kāi)發(fā)一時(shí)爽，維護(hù)火葬場(chǎng)。高人力成本和低產(chǎn)出效率，正成為限制操作系統(tǒng)高效演進(jìn)的重要原因。

“生成式操作系統(tǒng)”：夢(mèng)想是否遙不可及？

既然人類(lèi)維護(hù)不動(dòng)了，讓大模型上行不行？

現(xiàn)在的大模型寫(xiě)代碼確實(shí)越來(lái)越強(qiáng)了，寫(xiě)個(gè)網(wǎng)頁(yè)前端，小游戲，甚至打Codeforces比賽都不在話下。那么很自然的想法來(lái)了：我們能否打造一個(gè)“生成式操作系統(tǒng)”，讓大模型來(lái)接手這項(xiàng)苦差事？

想象一下，你只需要告訴大模型：“我需要一個(gè)為新型網(wǎng)卡優(yōu)化的、支持超低延遲網(wǎng)絡(luò)的操作系統(tǒng)”，然后大模型就能自動(dòng)生成一個(gè)完整的操作系統(tǒng)，不需要人力干預(yù)。如果這一美好幻想能實(shí)現(xiàn)，將給軟件行業(yè)提供一種顛覆性的新范式。

然而，現(xiàn)實(shí)往往事與愿違。

用大模型寫(xiě)過(guò)代碼的朋友們都知道，如果你真對(duì)大模型說(shuō)：“請(qǐng)幫我生成一個(gè)支持高并發(fā)、崩潰一致性的操作系統(tǒng)”，它生成的代碼大概率看起來(lái)很合理，但一運(yùn)行即崩潰。

這是因?yàn)?，操作系統(tǒng)往往高度復(fù)雜，而現(xiàn)有的大模型還難以應(yīng)對(duì)這樣的復(fù)雜性。

研究團(tuán)隊(duì)觀察到，想用大模型生成操作系統(tǒng)，必須解決下面的三個(gè)關(guān)鍵挑戰(zhàn)：

自然語(yǔ)言語(yǔ)義的局限性：自然語(yǔ)言提示詞天生是模糊的。如果只說(shuō)“要線程安全”，大模型理解和生成的鎖機(jī)制可能漏洞百出。作為整個(gè)計(jì)算機(jī)系統(tǒng)的基座，操作系統(tǒng)難以容忍這樣的不準(zhǔn)確性。

系統(tǒng)架構(gòu)模塊的深度耦合性：操作系統(tǒng)模塊繁多，模塊間交互邏輯復(fù)雜，耦合極深。大模型受限于上下文窗口，只能管中窺豹，難以進(jìn)行全局一致的設(shè)計(jì)，容易出現(xiàn)模塊間的邏輯或接口對(duì)不上等問(wèn)題。

并發(fā)控制邏輯的復(fù)雜性：實(shí)現(xiàn)細(xì)粒度的并發(fā)控制是操作系統(tǒng)面臨的重要挑戰(zhàn)，也是大部分操作系統(tǒng)開(kāi)發(fā)者的噩夢(mèng)。讓大模型一邊寫(xiě)功能邏輯，一邊處理復(fù)雜的“避免死鎖”的并發(fā)要求，這直接超出了現(xiàn)有大模型的能力上限。

用樸素的自然語(yǔ)言指導(dǎo)大模型生成操作系統(tǒng)，就像是純靠工頭用嘴巴指揮建筑工人造摩天大樓，倒塌是必然的。

SysSpec：給大模型的操作系統(tǒng)設(shè)計(jì)說(shuō)明書(shū)

如何破局？

IPADS團(tuán)隊(duì)給出的答案是：如果自然語(yǔ)言的描述對(duì)大模型來(lái)說(shuō)太過(guò)模糊，那就給它提供更加精確的設(shè)計(jì)說(shuō)明書(shū)。

而這份說(shuō)明書(shū)，正是基于計(jì)算機(jī)科學(xué)中的基礎(chǔ)技術(shù)，形式化方法，來(lái)實(shí)現(xiàn)的。

形式化方法通常是一套用純數(shù)學(xué)語(yǔ)言給程序定義嚴(yán)格語(yǔ)義約束的方法。在傳統(tǒng)用法中，開(kāi)發(fā)者需要寫(xiě)一份Specification（規(guī)約），用嚴(yán)謹(jǐn)?shù)墓矫枋龀绦颉氨仨氉鍪裁础币约啊敖^對(duì)不能做什么”，然后通過(guò)數(shù)學(xué)推導(dǎo)證明程序代碼和規(guī)約是等價(jià)的。

只要證明通過(guò)，程序就在數(shù)學(xué)層面上被判定為Bug-free。這也是保障航空航天、核能、芯片等領(lǐng)域可靠性的關(guān)鍵技術(shù)。

基于此，研究團(tuán)隊(duì)有了一個(gè)逆向思維的洞察：既然規(guī)約如此精確，我們是否可以直接用它來(lái)指導(dǎo)生成，而不是事后驗(yàn)證呢？

沒(méi)錯(cuò)，SysSpec就是這樣的一種全新范式。開(kāi)發(fā)者不需要再手搓容易出錯(cuò)的C語(yǔ)言代碼，而是直接編寫(xiě)高維度的Specification。這套過(guò)程實(shí)際上是形式化方法的“逆過(guò)程”：不再由規(guī)約驗(yàn)證實(shí)現(xiàn)，而是由規(guī)約生成實(shí)現(xiàn)。

△SysSpec規(guī)約設(shè)計(jì)示意圖

SysSpec提出了一整套結(jié)構(gòu)化的規(guī)約編寫(xiě)框架，用數(shù)學(xué)般的邏輯告訴大模型如何實(shí)現(xiàn)一個(gè)操作系統(tǒng)模塊：

功能規(guī)約（Functional Specification）：

引入霍爾邏輯（Hoare Logic），明確告訴大模型每個(gè)模塊的功能是什么，包括執(zhí)行前系統(tǒng)是什么狀態(tài)（Pre-condition），執(zhí)行后必須變成什么狀態(tài)（Post-condition）等。

模塊化規(guī)約（Modularity Specification）：

描述模塊之間接口層面的依賴關(guān)系。大模型在生成A模塊時(shí)，明確告訴它能依賴B模塊提供的哪些保證。

并發(fā)規(guī)約（Concurrency Specification）：

SysSpec將業(yè)務(wù)邏輯與并發(fā)邏輯進(jìn)行分離，先讓大模型生成正確的串行代碼，再根據(jù)專(zhuān)門(mén)的并發(fā)規(guī)約，把死鎖、競(jìng)態(tài)條件等邏輯完成。讓大模型一次只做一件事，效率反而更高。

SysSpec Toolchain：從規(guī)約到代碼的自動(dòng)化工具鏈

有了規(guī)約作為說(shuō)明書(shū)，還需要工具實(shí)現(xiàn)從規(guī)約到代碼的轉(zhuǎn)換。研究團(tuán)隊(duì)為SysSpec配套了3個(gè)基于Agent的工具鏈：

△SysSpec工具鏈的執(zhí)行過(guò)程

1. SpecCompiler：負(fù)責(zé)將SysSpec“編譯”成C代碼，通過(guò)先寫(xiě)邏輯、再加鎖的方式大大降低生成難度。

2. SpecValidator：專(zhuān)門(mén)對(duì)抗大模型“幻覺(jué)”。它會(huì)反復(fù)迭代驗(yàn)證生成的代碼是否符合SysSpec的規(guī)約，直到生成結(jié)果符合預(yù)期（或失敗次數(shù)觸發(fā)閾值）為止。

3. SpecAssistant：輔助開(kāi)發(fā)者編寫(xiě)規(guī)約，降低上手門(mén)檻。

那么，最讓人頭疼的“系統(tǒng)演進(jìn)”怎么辦？

研究團(tuán)隊(duì)在SysSpec的基礎(chǔ)上，提出了一項(xiàng)新的系統(tǒng)演進(jìn)方法：DAG-Structured Spec Patch（基于有向無(wú)環(huán)圖結(jié)構(gòu)的規(guī)約補(bǔ)?。?。

系統(tǒng)演進(jìn)中，我們需要對(duì)代碼進(jìn)行修改，過(guò)去讓大模型改代碼是越改越亂，而現(xiàn)在，改代碼變成了改規(guī)約，修改的規(guī)約被組織成了一個(gè)有向無(wú)環(huán)圖（DAG），每一個(gè)模塊的修改本質(zhì)上是一個(gè)圖中的節(jié)點(diǎn)：

• 葉子節(jié)點(diǎn)負(fù)責(zé)定義局部的新邏輯；
• 中間節(jié)點(diǎn)層層向上，利用下層提供的新保證（Guarantee）來(lái)構(gòu)建更復(fù)雜的功能；
• 根節(jié)點(diǎn)負(fù)責(zé)最終的一鍵集成。

這意味著，開(kāi)發(fā)者只需要提交一個(gè)規(guī)約補(bǔ)丁，工具鏈就會(huì)自動(dòng)計(jì)算依賴關(guān)系，把新的規(guī)約合并到原有實(shí)現(xiàn)里。這樣，我們就只需重構(gòu)代碼中受影響的模塊，從而確保生成的新功能不會(huì)破壞原有的系統(tǒng)實(shí)現(xiàn)。

△DAG結(jié)構(gòu)化規(guī)約補(bǔ)丁

SpecFS：基于規(guī)約，實(shí)現(xiàn)系統(tǒng)軟件的自動(dòng)生成和演進(jìn)

基于這套框架，研究團(tuán)隊(duì)以操作系統(tǒng)中的重要組成部分文件系統(tǒng)為例，構(gòu)建了一個(gè)基于SysSpec規(guī)約的完整的文件系統(tǒng)：SpecFS。

SpecFS能夠在開(kāi)機(jī)時(shí)自動(dòng)通過(guò)工具鏈，生成基于C語(yǔ)言的操作系統(tǒng)文件系統(tǒng)（無(wú)需人工干預(yù)），并且還支持根據(jù)用戶特定需求和規(guī)約補(bǔ)丁實(shí)現(xiàn)自我演進(jìn)。

生成的SpecFS實(shí)現(xiàn)，包含各種優(yōu)化，總共約四千三百行代碼。在Linux 6.1.10版本內(nèi)核中的82個(gè)文件系統(tǒng)中，能夠排到第42位。

團(tuán)隊(duì)還對(duì)SpecFS的能力進(jìn)行了仔細(xì)的驗(yàn)證和評(píng)估。

首先是正確性驗(yàn)證：在xfstests測(cè)試套件下，SpecFS的正確性表現(xiàn)可與人類(lèi)專(zhuān)家耗時(shí)許久手寫(xiě)的系統(tǒng)相媲美。

更值得一提的是它的演進(jìn)能力。研究團(tuán)隊(duì)嘗試給SpecFS添加了Ext4文件系統(tǒng)的10個(gè)復(fù)雜特性（如Extent、延遲分配、文件加密等）。

這些特性的引入只需要在SpecFS的規(guī)約層通過(guò)規(guī)約補(bǔ)丁的方式進(jìn)行擴(kuò)展。實(shí)驗(yàn)顯示，新引入的特性能夠有效提升文件系統(tǒng)性能。例如引入“延遲分配”（Delayed Allocation）特性后，SpecFS在完成編譯xv6的任務(wù)時(shí)，寫(xiě)操作直接減少了99.9%！

研究團(tuán)隊(duì)還招募了實(shí)驗(yàn)室的碩博同學(xué)，對(duì)使用這套框架進(jìn)行開(kāi)發(fā)的效率進(jìn)行測(cè)試：相比手動(dòng)修改C代碼，使用SysSpec演進(jìn)能力的開(kāi)發(fā)效率提升了3-5倍。

從“易錯(cuò)的底層代碼”中解放出來(lái)

從Ext4文件系統(tǒng)的20年修補(bǔ)之路，到SpecFS的自動(dòng)生成和演進(jìn)，SysSpec展示了一種操作系統(tǒng)開(kāi)發(fā)的未來(lái)范式（也是研究論文的標(biāo)題）：
Sharpen the Spec, Cut the Code.

在生成式AI時(shí)代，程序員也許不再需要逐行敲擊那些易錯(cuò)的底層代碼，而是可以更多地關(guān)注在有趣的系統(tǒng)設(shè)計(jì)上，剩下的，就交給大模型去做吧！

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