非羊 整理自 凹非寺
量子位 | 公眾號 QbitAI

還記得《流浪地球2》里的那臺550W量子計算機嗎？

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

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

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

操作系統(tǒng)：與時俱進的沉重負擔

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

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

然而，OS必須與時俱進，來滿足硬件和應(yīng)用的雙重需求：

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

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

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

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

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

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

既然人類維護不動了，讓大模型上行不行？

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

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

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

用大模型寫過代碼的朋友們都知道，如果你真對大模型說：“請幫我生成一個支持高并發(fā)、崩潰一致性的操作系統(tǒng)”，它生成的代碼大概率看起來很合理，但一運行即崩潰。

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

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

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

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

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

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

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

如何破局？

IPADS團隊給出的答案是：如果自然語言的描述對大模型來說太過模糊，那就給它提供更加精確的設(shè)計說明書。

而這份說明書，正是基于計算機科學中的基礎(chǔ)技術(shù)，形式化方法，來實現(xiàn)的。

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

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

基于此，研究團隊有了一個逆向思維的洞察：既然規(guī)約如此精確，我們是否可以直接用它來指導生成，而不是事后驗證呢？

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

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

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

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

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

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

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

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

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

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

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

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

1. SpecCompiler：負責將SysSpec“編譯”成C代碼，通過先寫邏輯、再加鎖的方式大大降低生成難度。

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

3. SpecAssistant：輔助開發(fā)者編寫規(guī)約，降低上手門檻。

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

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

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

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

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

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

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

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

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

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

團隊還對SpecFS的能力進行了仔細的驗證和評估。

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

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

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

研究團隊還招募了實驗室的碩博同學，對使用這套框架進行開發(fā)的效率進行測試：相比手動修改C代碼，使用SysSpec演進能力的開發(fā)效率提升了3-5倍。

從“易錯的底層代碼”中解放出來

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

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

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