亂序核心跑起來的當下，內部真的會出現 ISA 規格禁止的狀態——load 讀到還沒退休的 store、分支預測錯了但後面已經有指令在執行。這篇論文證明的不是「這不會發生」，而是「不管 buffer 多大、核心數多少，這些偷跑最後都會被撤乾淨，行為跟一顆逐條執行的順序性 ISA 完全對得上」。
亂序核心先斬後奏、事後撤回——一次 unbounded 的弱記憶體形式驗證
要驗證一顆現代 CPU 是否符合它的指令集規格，最麻煩的不是規格複雜，而是亂序執行本身在正常運作的過程裡，本來就會做出規格不允許的事——這篇 2026 年 7 月 21 日掛上 arXiv 的論文，作者是 Janggun Lee 與 Jeehoon Kang，針對一顆通用亂序多核心設計做了他們稱為首例的形式驗證：證明它的行為 unbounded 地精煉（refine）一個順序性、但骨子裡仍是弱記憶體模型的 ISA 規格。「unbounded」是重點——證明不綁定特定 buffer 大小、核心數或執行長度，對任意參數都成立，跟只檢查有限深度的 bounded model checking 是兩回事。傳統上這類驗證常常退而求其次：鎖定一個固定的 buffer 深度、固定的核心數，在這個範圍內窮舉，看看還找不找得到違規狀態；找不到，只能說「在這個深度以內沒問題」，深度以外的行為仍是未知。這篇論文的主張是把這條界線整個拿掉——證明對任意深度、任意核心數都成立，是工程保證上完全不同的等級。
亂序視窗——ROB、LSQ、store buffer 怎麼讓指令脫序執行
被驗證的核心是一個通用設計，沒有對應到任何特定商用晶片。它由幾個熟悉的元件組成：reorder buffer（ROB）從指令分派到退休全程追蹤程式順序；ALU 執行算術與分支這類「純」指令，允許脫序、也允許投機；load-store queue（LSQ）負責偵測並撤銷讀到舊值的違規 load，撐住 coherence；store buffer（StB）讓寫入可以不照程式順序排空，只要位址不同就能互換；memory unit 讓 load 投機式地提前發射，store 則要拖到退休才真正動到記憶體。整體設計允許 load-load、store-load、store-store 三種重排，但刻意不做 load-store 重排——這一點沿用 RiscyOO 的先例，論文給的理由是這種重排效益有限、又會讓撤銷邏輯更複雜。這個不對稱不是巧合：load 讀錯了可以撤銷重讀，store 一旦真的寫進記憶體就覆水難收，這也是為什麼 store 要等到退休——也就是確定不會再被撤銷的那一刻——才能真正動到記憶體，而 load 可以在還沒退休、還有被撤銷風險的階段就先投機讀取。
這幾個元件放在一起，才是「亂序」這個詞真正的重量所在——不是「調換一下計算順序」這麼簡單，而是核心在還沒退休、還沒真正動到記憶體之前，系統整體其實同時活在好幾個不完全一致的暫時世界裡：有些指令已經算完但還沒退休，有些 load 已經投機讀了一個之後會證明是錯的值，有些 store 已經離開 ROB 但還卡在 store buffer 裡沒真正寫進記憶體。驗證要處理的，正是這些暫時世界最終怎麼一致地收斂回一條 ISA 規格認可的軌跡。這也是為什麼「驗證一顆順序性 ISA」聽起來像是比驗證一顆真正弱記憶體的 ISA 簡單，但被驗證的核心骨子裡完全不是這麼回事——內部同時活著的這些暫時世界，跟弱記憶體系統要處理的問題是同一類問題，只是被藏在單一核心內部，還沒外顯成跨核心的可見性差異。
按播放，看六條指令怎麼脫序完成、卻照程式順序退休 · 6 條指令的參數化模擬
六條指令（I0–I5，I1 寫位址 A、I4 寫位址 B）幾乎同時開始執行；上排是完成順序（完全打散），中排是 ROB…
六條指令幾乎同時開始執行，完成順序完全打散；ROB仍照程式順序退休，store buffer 甚至把兩筆不同位址的寫入用打散的順序送回記憶體。
模擬把六條指令（I0 到 I5，其中 I1 寫位址 A、I4 寫位址 B）擺在一起：執行完成的順序完全打散——I3 可能比 I0 早做完；但 ROB 退休那一排，永遠是 I0、I1、I2 照程式順序推進，卡在前面沒做完的指令會讓後面早就做完的指令一起等。等到 I1 跟 I4 都退休、進了 store buffer，兩者位址不同，寫回記憶體的先後順序又可以再打散一次——這正是 excess out-of-order execution：核心內部同時活著好幾種暫時的順序，證明要處理的就是這些暫時狀態最終怎麼收斂回一條合法軌跡。動畫示範的是 load-load 跟 store-store 這兩種重排；連同 store-load、以及規格層級允許但需要 certify 的 promise，這個設計實際允許哪些重排、禁止哪些、由誰把關，整理成下表。
| 重排情境 | 是否允許 | 誰把關 / 怎麼收場 |
|---|---|---|
| load → load | 允許 | 完成順序可任意打散；LSQ 偵測讀到舊值的違規 load 並撤銷 |
| store → load | 允許 | memory unit 讓 load 提前投機發射；LSQ 事後驗證是否讀對值 |
| store → store | 允許 | store buffer 依位址不同打散排空順序，位址相同則不互換 |
| load → store | 不允許 | 設計刻意維持程式順序——沿用 RiscyOO 先例，效益有限且會複雜化撤銷邏輯 |
| 分支預測後的投機指令 | 允許，但可撤銷 | 每條指令帶 speculation mask；分支解析錯誤時，帶同一分支 tag 的指令整批撤銷 |
| promise（跨核心提前可見的寫入） | 允許，但需可 certify | ISA 規格層級：承諾必須能在之後真的照順序執行到那一步時兌現，兌現不了就從一開始不合法 |
promising semantics——順序性規格骨子裡仍是弱記憶體
這篇論文用來當靶的 ISA 規格，底層是 promising semantics（Pulte 等人 2019 年提出的一套弱記憶體 operational model）。它把記憶體處理成一個帶時間戳的訊息集合，而不是單一個「目前的值」——load 可以讀到集合裡任何一則合法訊息，不一定是最新的那則。這套模型也允許 promise：一個核心可以提前讓其他核心看到一筆還沒真正 retire 的寫入，前提是這個承諾之後必須能被 certify，也就是真正照順序執行到那一步時要能兌現。而每個核心對每個位址各自維護一個 coherence view——一個時間戳上界，決定它現在能看到訊息集合裡的哪些訊息。作者把原始版本裡用樹狀語法描述指令的部分，換成貼近真實 ISA 的位元組序列加上一個 program counter，讓規格跟被驗證的實作長得更像。這個改動看似只是語法上的翻譯，但直接決定了 core refinement 那一步能不能把具體實作的狀態一一對應到規格的狀態——兩邊的指令表示法越接近，寫證明時要處理的「翻譯層」就越薄。
promise 這個機制乍看很危險——核心憑什麼可以讓別人先看到還沒真正發生的寫入？答案在 certify 這個條件上：一個 promise 必須能在假設之後照這個順序真的執行到那一步的前提下自圓其說，如果核心後續的行為證明這個承諾兌現不了，這個 promise 從一開始就不合法。這也是為什麼即使規格允許先斬後奏式的提前可見，整體語意依然收斂在一個定義明確的集合裡，而不是任意亂序都算數。換句話說，promise 只是把「寫入何時對其他核心可見」這件事從「退休那一刻」提前，但提前多少、提前之後站不站得住腳，仍然完全由 certify 這個條件決定。
拖曳圓點調整這顆核心的 coherence view 時間戳 · 3 則訊息
重點在這裡：規格對每個核心來說是 in-order 的——每個核心確實是照程式順序逐條退休指令，沒有規格層級的脫序。但這不等於強記憶體。因為每個核心的 coherence view 不需要是目前最新，它可以停在一個比較舊的時間戳上——上面這個小工具讓你拖動一顆核心的 view 時間戳，看它此刻到底能讀到哪則訊息：往前拖，能看到的訊息就變舊；即使集合裡已經有更新的訊息（可能是別的核心剛寫進去的），這顆核心的檢視沒追上去之前，就是看不到。多核心之間 view 不同步，就是弱記憶體行為的來源——即便每一個核心自己的指令序列從頭到尾都是順序執行。換句話說，即使每個核心自己是嚴格照程式順序退休，A 核心寫入的一筆資料，B 核心不保證馬上看得到——B 的 view 可能還停在較舊的時間戳上，要等它自己的後續指令（尤其是 fence 這類同步點）把 view 往前推，才追得上。跨核心的可見性延遲，才是這個規格「弱」在哪裡的具體位置，而不是某個核心自己亂了執行順序。
兩步精煉證明——core refinement 與 system inclusion
整個證明拆成兩大步。第一步是 core refinement，符號寫成 Core_i ⊑ Core_s：把具體實作（帶著 ROB、ALU、LSQ、StB 這些分開的元件）對照一個中介規格 Core_s。Core_s 刻意只留下推理 excess execution 與核心介面行為所需要的東西，其餘微架構狀態全部抽象掉，把所有指令資訊攤平成一張單一的、按程式順序排列的清單。這樣做的好處是「違規之後怎麼收場」變得非常好證：一旦偵測到某條指令違反 coherence，Core_s 只要把違規指令之後的所有指令整批丟掉，就等於模擬了一次撤銷，不用去追蹤 ROB、LSQ 裡每個元件各自要怎麼復原。Core_i ⊑ Core_s 這個精煉關係的意思是：具體實作能做出的每一步行為，中介規格都要能對應做出一步（或選擇不做）；只要這個對應關係成立，接下來只需要對 Core_s 這個簡化很多的模型講道理，不用再回頭處理 ROB、LSQ、StB 內部各自的狀態機。
按按鈕，看具體實作抽象成中介規格 Core_s 的過程 · 4 個元件收斂成 1 張清單
第二步是 system inclusion，符號寫成 n·Core_s + ShMem ⊆ ISA：把 n 個核心規格加上一個共享記憶體規格組合起來，證明整體行為被 ISA 規格涵蓋。這一步本身又拆成三個子步驟——merging refinement 先拿掉核心跟記憶體之間請求-回應介面的簿記細節；threading inclusion 把語意轉成不需要 certify 的版本，讓多核心交錯先在一個比較寬鬆的世界裡站得住腳；certification inclusion 最後才把完整的 ISA 要求（含 promise 的 certify 條件）加回來。這三個子步驟不是任意切法：merging refinement 先把核心跟記憶體之間那層請求-回應介面的簿記細節拿掉，因為這層只是通訊機制、跟語意本身無關；拿掉之後，threading inclusion 才能把多核交錯轉成一個不需要 certify 的寬鬆版本語意，先確保「交錯本身站得住腳」，還不管 promise 能不能兌現；最後 certification inclusion 才把 promise 的 certify 要求整個加回來，把寬鬆版本收緊回真正符合 ISA 規格的樣子。三步一路把「n 個核心各自的 store buffer 排空順序」跟「跨核心的記憶體交錯」，序列化成一條合乎 ISA 規格的全域軌跡。這個兩步拆法背後的直覺，是把「亂序執行內部有多複雜」跟「怎麼跟外部規格對齊」分開處理：core refinement 一次處理一個核心內部的複雜度，投機、squash 全部關在這一步裡解決；system inclusion 完全不用再管這些細節，只需要面對已經攤平的 Core_s 清單怎麼跟 ISA 對齊。如果不做這個中介規格，直接拿具體實作去對 ISA，證明要同時處理微架構複雜度跟多核交錯，狀態空間會炸開。
投機執行與 squash——分支預測失準、coherence 違規怎麼收場
投機的兩個來源分開處理。第一種是分支預測：每條在未解析分支之後才發射的指令，都會帶一個 speculation mask，記錄它依賴哪些還沒確定結果的分支。分支一旦解析出預測錯誤，核心會撤銷所有 speculation mask 裡含有這個分支 tag 的指令；分支指令本身不撤銷，因為它自己的最終結果已經確定。第二種是 LSQ 抓到的 coherence 違規：當一條較舊 load 原本讀到的位址後來才浮現，LSQ 會往後掃描更晚的指令，把讀到舊值的違規 load 揪出來撤銷。這兩種投機來源都會在核心內部造成違反 ISA 規格的暫時狀態，差別在觸發原因：分支預測是核心自己選錯了要不要執行某段路徑，coherence 違規是等到更舊的 load 位址浮現、才發現一開始讀錯了值——兩者共同點是，違規本身在偵測到之前，已經真的在核心內部發生過。
按按鈕模擬分支預測失準，看哪些指令被 squash · 6 條指令
互動圖表
分支預測失敗時，I2 的結果已確定所以保留，但帶著 I2 投機遮罩標記的 I3、I4 會被整批撤銷，跟 I2 無關的 I5 完全不受影響。
speculation mask 用點陣紀錄依賴關係的好處是精準——只有真的搭上這班錯誤分支順風車的指令會被撤銷，跟它平行、但不依賴這個分支的指令不受影響，不用整個 pipeline 沖掉重來。LSQ 那邊的偵測邏輯類似：一條 load 一旦被證明讀到舊值，往後被撤銷的也只有真正依賴它、或者晚於它的違規指令。兩者用的線索不同——分支撤銷靠每條指令攜帶的 speculation mask 精準定位到指令層級，LSQ 撤銷靠往後掃描時間順序抓出讀到舊值的犯規者——但收尾動作是同一招：把違規之後的東西整批丟掉。這正好呼應 Core_s 中介規格「偵測到違規、丟棄違規指令之後所有指令」的簡化設計：不管觸發撤銷的原因是分支預測錯誤還是 coherence 違規，中介規格都用同一個抽象操作處理，具體實作內部兩種不同的撤銷機制，才需要分開追蹤。這兩種撤銷共用同一套帳本邏輯，但論文額外處理了一個時序上的細節：中介規格裡有一個叫 Core_sf 的版本，在 fence 操作上加了一個 live flag，用來對齊「記憶體退休」跟「ROB 退休」這兩個時間點的落差——acquire fence 的阻塞語意，剛好卡在這兩個時間點之間，沒有這個 flag，證明會在這裡卡住。
LLM agent 寫證明，以及這場驗證證明了什麼、沒證明什麼
機械化證明用的工具是 Rocq。證明的組織方式是由下而上：先把共用的底層元件——排序索引清單、投機標籤管理器、reservation station——各自證完，再往上疊出整個核心的 core refinement，最後才疊 system inclusion。這三個共用元件對應到微架構裡經常重複出現的簿記邏輯——排序索引清單處理「誰在誰前面」這種順序關係，投機標籤管理器處理 speculation mask 的建立與比對，reservation station 處理指令等待運算元就緒的佇列邏輯；把這些獨立元件的正確性先釘死，上層的核心證明才不用每次都從頭處理這些細節。這個順序也是為什麼作者敢把大部分工作交給 agent：每一層的證明目標都定義明確，agent 不需要同時面對整個系統的複雜度。作者的分工方式值得一提：人類負責設計初始規格、不變式與抽象，也就是上面兩步證明的骨架；剩下大部分機械化證明——作者稱是交給 LLM agent 完成，agent 卡住寫不出來才回頭問人類。作者形容 system inclusion 那一步幾乎是 agent 自主完成的。這是作者自己的說法，論文沒有附上證明行數、驗證耗時，也沒有針對某個具體核心數做 benchmark——這幾個數字目前沒有公開，寫這篇文章時也不去猜。
主定理的陳述是：n 個核心實作加上一個共享記憶體規格的組合，行為精煉這個指令集規格。要精確理解這句話，得看清楚三個邊界。第一，這只保 safety：trace 語意能保證的是「不會做出違規的事」，「eventual retirement」這種 liveness 性質——指令保證終究會退休——不在證明範圍內。第二，被驗證的是一個假設常數指令記憶體、不做 load-store 重排的通用單發射設計（論文原文即以「single-issue, out-of-order RISC-V core」描述這個設計），不是任何一顆量產晶片，也不是超純量、多發射那種更貼近今天商用 CPU 的架構。第三，unbounded 指的是 buffer 大小、核心數、執行長度這些設計參數不設界限，不是說這套方法已經套進了一顆真正的 RTL 實作——論文證的是「這個核心規格」跟「這個 ISA 規格」之間的精煉關係，不是「這顆晶片沒有 bug」。這三條邊界不是在貶低這篇論文——unbounded 地處理 excess out-of-order execution 這件事，先前確實少見——但「verified against this ISA spec」跟「silicon 沒有 bug」中間隔著好幾層，論文自己也沒有宣稱跨過去。把這三條邊界跟開頭的 unbounded 主張放在一起看，會更清楚這篇論文的真正貢獻在哪裡：不是「這顆核心沒有 bug」，而是「在這個核心規格跟這個 ISA 規格之間，某個特定意義下的行為對應關係，對任意參數都成立」——貢獻的精確位置，決定了讀者該怎麼引用它。
這場驗證解鎖了什麼：把「亂序核心執行時會短暫做出規格禁止的事，但外部看到的行為終究合規」這件事，從工程師的信任變成一個不綁 buffer 大小、核心數、執行長度的 unbounded 證明——邊界也同樣清楚：保的是 safety 不是 liveness，驗證對象是一個不做 load-store 重排的通用單發射核心規格，不是任何一顆量產晶片。