Programming Languages
《滲漏的分號》
Author
Venue
ACM 程式語言研討會論文集 2021
Abstract
程式邏輯與語義學為序列組合描繪了一幅美好的圖景：執行 (S1; S2) 時，我們會先執行 S1，再執行 S2。然而，為了提升效能，處理器會以非順序方式執行指令，而編譯器對程式的重新排序更是劇烈。根據設計，單執行緒系統無法察覺這些重新排序；但多執行緒系統卻能察覺，這使得上述圖景變得遠不如想像中美好。 為理解由此產生的混亂局面，學界提出了一種稱為「寬鬆記憶體模型」的正式嘗試。過往的模型要麼未能直接處理順序組合，要麼過度限制處理器與編譯器，要麼允許在實務中無法觀察到的荒謬「虛空行為」。為了在支援現代硬體的同時維持順序組合，我們透過預條件與一組謂詞轉換器，來擴充標準的事件導向方法。 在計算 (S1;S2) 的含義時，針對 S2 中事件 e 的先決條件所應用的謂詞轉換器，是根據 e 所依賴的 S1 事件集合來選擇的。我們將此方法應用於兩種現有的記憶體模型。
