jMT: Testing Correctness of Java Memory Models (Extended Version)

開發並驗證一個正確的並行程式記憶體模型極度困難。為了解決 Java 記憶體模型長期的設計缺陷，研究人員正式推出 jMT 測試工具。該工具透過分析 169 個指標性微型測試，不僅首度將多重執行語意自動化，更發現了最新版模型的預期外行為與設計漏洞。

從 JLS04 到 JAM21 的 Java 記憶體模型演進

自 1996 年首個 Java 記憶體模型（JMM）發布以來，業界對其正確性的修補從未停止。Pugh 曾證實最初的規範存在嚴重缺陷，隨後 2004 年由 Manson 等人提出的 JLS04 模型雖然成為官方標準，卻被發現會阻礙編譯器的標準最佳化。這套舊模型在面對現代同步原語時更顯過時，尤其缺乏對 VarHandle API（提供變數多種存取模式、記憶體屏障等進階操作的介面）的完整支援。

為了補足這些現代化功能，2021 年 Bender 等人提出了 JAM21 模型。儘管該模型納入了多數新特性，但研究實測證實，該模型依然會禁止某些理應存在的正常行為，並允許不當的執行結果產生。建構正確 JMM 的最大技術門檻在於，Java 的並行環境需要一套多重執行模型（multi-execution model）。

在這種模型架構下，開發者無法單看單一執行路徑來判斷程式行為的合法性。系統必須在龐大的候選執行集合中，交叉比對並篩選出真正有效的路徑。這導致過去每一次更新模型，都需要投入極高的人工證明成本。

解決無中生有問題與 herd 工具的發展瓶頸

記憶體模型通常包含兩個層次：定義候選集合的單一執行模型（SEM），以及負責驗證執行的多重執行模型（MEM）。如果僅依賴單一執行模型，系統將無法在不限制編譯器最佳化的情況下，防範所謂的「無中生有問題」（thin-air-problem，指變數值在計算過程中產生迴圈依賴的異常現象）。

過去，業界在驗證硬體記憶體模型或編譯方案時，多半仰賴繁瑣的人工形式化證明。這使得每次修改模型都伴隨極高的時間成本，難以快速迭代。現階段最著名的記憶體模型開發工具是 herd，它允許使用者定義獨立於硬體與程式語言的單一執行模型。

然而，herd 最大的極限在於它無法處理多重執行模型。另一套歷史悠久的模擬器 JavaSim 雖然支援 Java，但不僅已知存在多處系統錯誤，其開發時間更早於 VarHandle API，完全無法應對現代語法的測試需求。這正是 jMT 工具誕生的核心契機。

jMT 工具的三大驗證場景與 169 項指標測試

為了填補多重執行模型的自動化驗證缺口，研究團隊開發了 jMT 工具。開發者只需使用 herd 的 .cat 語言定義全新的 Java 單一執行模型，jMT 就能自動計算並行程式的語意，並透過內建的 JLS04 風格多重執行模型找出合法路徑。

該工具的應用涵蓋三大核心場景。首先是產生微型測試（litmus tests，用於觸發特定行為的小型程式碼片段）的語意，並與預期結果比對。其次是透過標準編譯方案將程式編譯至特定硬體架構，再交叉比對新 JMM 與編譯後程式的執行結果。最後則是使用標準 Java 編譯器處理程式，並在執行期捕捉行為差異。

團隊特別彙整了來自多篇頂尖論文的 169 個微型測試，並實作了一個無最佳化的 Intel x86 處理器微型編譯器，讓開發者能單純針對編譯方案進行精準除錯。此外，工具鏈也整合了 jcstress（Java 並行壓力測試工具），確保在動態環境下依然能有效找出模型與真實編譯器之間的不一致。

導入符號執行圖突破無限候選路徑的計算量

傳統的執行圖形會將變數寫死為具體數值，這在處理包含資料競爭的並行 Java 程式時，容易因為數值組合過多而陷入難以窮舉的困境。jMT 摒棄了傳統做法，轉而建構符號執行圖（symbolic execution graphs）。在這種圖形中，讀寫事件的標籤會使用暫存器名稱或常數等符號表達式，並附加邏輯限制式（constraints）來描述變數間的運算關係。

jMT 建構圖形的過程分為多個嚴謹階段。第一階段是建立控制流程語意，工具會根據個別執行緒的循序指令逐步擴展圖形，包含處理賦值、寫入、讀取，甚至針對「比較並交換」（CAX）這類讀取-修改-寫入（RMW）指令，同時建立成功與失敗兩條分支圖形。

第二階段則處理資料流程語意。系統會為每一個讀取事件尋找同位置的寫入事件，藉此建立「讀取來源」（reads-from, rf）的邊界關係與邏輯限制。過程中，jMT 會呼叫 SMT 求解器（能自動判定邏輯公式是否具可滿足性的運算程式）檢查限制式，若發現矛盾便直接剔除該無效圖形。這種手法大幅壓縮了記憶體消耗，讓單一圖形能有效率地代表無限多種潛在的具體數值執行路徑。

因果關係檢查機制與跨執行圖事件等價性

確保執行圖形合法性的最後一關，是多重執行模型專屬的因果關係檢查（causality checking）。過去 JLS04 的規範多為宣告式的概念，而 jMT 首度將其轉化為可執行的「證成序列」（justification sequences）建構演算法。系統會以一個滿足基本 happens-before 規則的圖形為起點，逐步驗證並「提交」（commit）事件。

在增量提交的過程中，jMT 會嚴格核對七大條件。包含已提交事件的圖形結構必須與目標圖形一致、同步順序（synchronization order）必須完全相同，以及尚未提交的讀取事件必須與其寫入來源維持明確的 happens-before 關係。讀取事件唯有在寫入端被證實合理後，才被允許提交。

為了在不同執行圖之間精準比對事件，研究團隊更首度針對「跨執行圖的事件等價性」（cross-execution event equivalence）提出了嚴格的數學定義。系統透過比較事件類型、操作記憶體位置，以及該事件在個別執行緒程式順序中的索引位置（index），來判定兩個事件是否相等。這項突破不僅修補了過往文獻語意模糊的漏洞，更讓團隊成功揪出 Doug Lea 官方 VarHandle 說明文件中的邏輯矛盾，為未來的並行程式語言標準提供了關鍵的測試基石。

jMT 工具將繁瑣的數學證明轉化為自動化的符號執行圖驗證，大幅降低了並行記憶體模型設計迭代的成本與出錯率。