SPECIAL POPL ISSUE的數據競爭示例Java Memory Model混淆

Question

我對SPECIAL POPL ISSUE The Java Memory Model論文中的圖3感到困惑。

實施例（第5頁，圖3）：

Initially, x == y == 0  

Thread 1 -> r1 = x; y = r1; 

Thread 2 -> r2 = y; r3 = r2 | 1; x = r2; 

r1 == r2 == r3 == 1 is legal behavior. 

說明1（第5頁，1.2休閒循環）： 因果循環的另一個例子 - 此時，一個描述了一種可接受的行爲 - 可以如圖3所示。爲了看到結果r1 == r2 == r3 == 1，其中一個線程在執行讀操作之前必須執行寫操作。但是每個寫都似乎依賴於上面的閱讀。雖然這個值也許看起來很簡單，但它不會也可能來自標準的編譯器轉換，正如2.2.2節所討論的那樣。

解釋2（第10頁，2.2.2依賴打破分析和轉換）： 圖3顯示了一個類似但更令人驚訝的行爲。在這種情況下， 編譯器將不得不執行更深入的分析，以確定x和y的值保證爲0或1.一個可能的此類分析 將是一個分析，它確定所需的位寬在程序中表示整數 值[Stephenson et al。 2000。

在這個例子中，R1和R2可以== 1僅if x or y == 1和x or y could be == 1只有if r1 and r2 == 1。但1任務，我可以找到只有在r3 = r2 | 1;所以，在我看來是沒有辦法讓1到r1，r2，x或y。

那麼，這個例子是錯的還是我弄錯了？

Answer 1

你是對的。這個例子是錯誤的。它應該是：

Initially, x == y == 0 
Thread 1 -> r1 = x; y = r1; 
Thread 2 -> r2 = y; r3 = r2 | 1; x = r3; 

您可以在圖1.3的Jeremy Manson's PhD dissertation中看到正確的示例。