非羊 整理自 凹非寺
量子位 | 公眾號 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