JCStress 實戰：在 Java 記憶體模型下驗證並發程式正確性

並發程式的微妙 Bug 往往難以透過傳統測試發現。本文介紹 OpenJDK 官方工具 JCStress，它能系統性探索所有可能的執行交錯組合，驗證並發代碼在 Java 記憶體模型（JMM）下的真實行為。

動機：一個看似簡單的 BitSet 並發問題

public class AnExample {
    public static void main(String[] args) throws Exception {
        BitSet bs = new BitSet();
        CountDownLatch latch = new CountDownLatch(1);
        
        Thread t1 = new Thread(() -> {
            try { latch.await(); Thread.sleep(1000); } catch (Exception e) {}
            bs.set(1);
        });
        
        Thread t2 = new Thread(() -> {
            try { latch.await(); Thread.sleep(1000); } catch (Exception e) {}
            bs.set(2);
        });
        
        t1.start(); t2.start();
        latch.countDown(); // 同時啟動
        t1.join(); t2.join();
        
        System.out.println(bs.get(1)); // true?
        System.out.println(bs.get(2)); // true?
    }
}

BitSet 非線程安全，兩線程並發 set() 可能導致其中一個更新丟失。但實際輸出會是什麼？JMM 允許哪些結果？手工推導極其困難。

JCStress 解決方案

測試類別實作

@JCStressTest
@State
@Actor2_Arbiter1_Test
public class AnExampleTest implements Actor2_Arbiter1_Test<BitSet, BooleanResult2> {
    @Override public void actor1(BitSet s, BooleanResult2 r) { s.set(1); }
    @Override public void actor2(BitSet s, BooleanResult2 r) { s.set(2); }
    @Override public void arbiter1(BitSet s, BooleanResult2 r) { 
        r.r1 = s.get(1); r.r2 = s.get(2); 
    }
    @Override public BitSet newState() { return new BitSet(); }
    @Override public BooleanResult2 newResult() { return new BooleanResult2(); }
}

結果描述檔

<test name="org.openjdk.jcstress.tests.custom.AnExampleTest">
  <case>
    <match>[true, true]</match>
    <expect>ACCEPTABLE</expect>
    <description>Seeing all updates intact.</description>
  </case>
  <case>
    <match>[true, false]</match>
    <expect>ACCEPTABLE_INTERESTING</expect>
    <description>T2 overwrites T1 result.</description>
  </case>
  <case>
    <match>[false, true]</match>
    <expect>ACCEPTABLE_INTERESTING</expect>
    <description>T1 overwrites T2 result.</description>
  </case>
  <unmatched>
    <expect>FORBIDDEN</expect>
    <description>All other cases are unexpected.</description>
  </unmatched>
</test>

執行命令

java -XX:+UnlockDiagnosticVMOptions -XX:+WhiteBoxAPI -XX:-RestrictContended \
     -jar tests-custom/target/jcstress.jar -t=".*AnExampleTest"

測試報告解讀

JCStress 會自動探索：

• 並行 vs 串行執行
• 有/無負載干擾
• 單次 vs 循環數萬次執行
• 不同 CPU 架構、JVM 版本、編譯器優化層級

報告會列出所有觀測到的結果組合及其發生頻率，標註 ACCEPTABLE（預期內）、ACCEPTABLE_INTERESTING（預期內但揭露競態）、FORBIDDEN（違反規範）等分類。

實際發現：BitSet 競態確認

測試證實：

• [true, true]：雙線程更新均可見（理想情況）
• [true, false] / [false, true]：其中一線程更新被覆蓋（實際發生）

這確認了 BitSet 非線程安全的特性在 JMM 下的具體後果。

修正方案

// 方案一：同步塊
synchronized (bs) { bs.set(1); }

// 方案二：使用 ConcurrentHashMap 或 LongAdder 替代（視場景而定）

// 方案三：Java 9+ 可考慮 VarHandle 配合原子操作

JCStress 核心優勢

適用場景

• 自定義無鎖資料結構驗證
• 並發演算法正確性證明
• JVM/JDK 開發者回歸測試
• 關鍵業務並發邏輯的形式化驗證補充

JCStress 將並發測試從「碰運氣」提升為「科學驗證」。對於構建高可靠並發系統的團隊，它是不可或缺的工具鏈組件。