Weak Memory Modelについてもう少し知識をつけたかったので、論文を読んでみることにした。

基本的にDeepLに翻訳してもらったものを、自分で読み直しながら直しているだけなので、自分でまとめているわけではない。冗長なのは無編集でブログに貼っている、ということで。

概要

ウィーク・メモリ・モデルは、共有メモリ・マルチプロセッサを構築する際に、ユニプロセッサの最適化をすべて維持したいというアーキテクト側の要望の結果である。

過去数十年にわたるARMやPOWERのウィーク・メモリ・モデルを形式化する努力は、そのほとんどが経験的なものであり、経験的に観察された動作を捕らえようとするもので、結局、ウィーク・メモリ・モデルの本質的な性質についての洞察は得られなかった。

本論文では、ウィーク・メモリ・モデルの共通基盤を見出すための建設的なアプローチをとる。すなわち、ユニプロセッサの最適化をすべて維持するという明確な目標を掲げてウィーク・メモリを構築した場合、どのようなものになるかを探る。プログラマの直感を非常に予期せぬ形で壊すような最適化は認めないことにする。一般原子メモリモデル（General Atomic Memory Model: GAM）と呼ぶこのモデルは、4つのロード／ストアの並べ替えをすべて許容する。GAMの構築手順を示し、その操作的意味論と公理的意味論を定義するための洞察を提供する。GAMを既存のウィーク・メモリモデルと比較する試みは行っていないが、シミュレーションによりGAMが他のモデルと同等の性能を持つことを示す。この論文を読むのにメモリモデルに関する深い知識は必要ない。

I. はじめに

ソフトウェア・プログラマは、ウィーク・メモリ・モデルを求めたことはない。しかし、ARMやPOWERのような重要な商用マシンでは、ウィークメモリ・モデルの結果として生じる動作に対処しなければならない。高級言語（C++11 など）の複雑な機能の多くは、ウィークメモリモデルを持つ ARM や POWER 向けに効率的なコードを生成する必要性から生じている[1]。

アーキテクチャ・コミュニティがウィーク・メモリ・モデルの亡霊を世に解き放った以上、以下の2つの問いに答えるべきである：

ウィーク・メモリ・モデルはストロングモデルよりも PPA（性能/消費電力/面積）を向上させるか？
ウィーク・メモリ・モデルには共通の意味論的基盤があるのか？この疑問は実用上重要である。というのも、専門家でさえ、さまざまな弱いモデルの正確な定義や、モデル間の違いについて合意できないからである。

最初の質問に答えるのは、2番目の質問よりもはるかに難しい。ARMやPOWERがウィーク・モデルを持っているのに対し、数十年にわたってCPU市場を支配してきたインテルはTSOを堅持している。ISCA/MICRO/HPCA[2]～[20]には、ストロング・メモリ・モデルの実装がウィーク・モデルの実装と同程度に高速である可能性を主張する論文が多数ある。この問題については、特に各社の利害が凝り固まっているため、短期的にコンセンサスが得られる可能性は低い。また、あるウィーク・メモリ・モデルがPPAの点で他のモデルより優れていることを示す研究は、我々が知る限り存在しない。

本稿では、2つ目の疑問、すなわちウィーク・メモリ・モデルに共通する基盤を見出そうとするものである。これまでの研究では、経験的なアプローチ、つまり、既存のマシンから出発して、メモリモデルの開発者がマシンの観測可能な動作にマッチする公理やルールのセットを考え出そうとしてきた。しかし、このアプローチでは、すべてのウィーク・モデルに共通する固有の性質についての洞察を得ることなく、市販のマシンで観察される微妙に異なる動作に研究者が溺れてしまっていることが観察される。例えば、Sarkar ら[21]は 2011 年に POWER の運用モデルを発表し、Mador-Haim ら[22]は 2012 年に運用モデルと一致することが証明された公理モデルを発表した。しかし、2014 年に Alglave ら[23]は、対応する公理モデルと同様に、元の運用モデルも POWER マシンで新たに観測された動作を除外することを示した。別の例としては、2016年にFlurら[24]がARMの運用モデルを示したが、対応する公理モデルはなかった。その1年後、ARMはISAマニュアルの改訂を発表し、Flurのモデルで許容される動作を明示的に禁止した[25]。

ウィーク・メモリ・モデルを経験的に定式化することは、明らかにエラーが発生しやすく、困難である。

本稿では、ウィーク・メモリ・モデルの共通基盤を見つけるために、異なる、より建設的なアプローチをとる。

マルチプロセッサは、原子共有メモリシステムにユニプロセッサを接続することで形成されると仮定し、すべてのプロセッサが従わなければならない最小制約を導出する。

同じアドレスのロード・ロード順序や依存ロード順序のような選択肢がまだ残っており、それぞれがわずかに異なるメモリモデルになることを示す。驚くことではないが、ARM、Alpha、RMOはこれらの選択において異なっている。

これらの選択肢の中には、モデルの運用定義と公理的定義を一致させることを困難にし、混乱を招くものもある。これらの選択肢を慎重に評価した結果、我々は一般的な原子メモリモデル（GAM）を導き出した。この洞察が、アーキテクトが実装前にメモリ・モデルを選択する際に役立ち、ISAがサポートするモデルのリバース・エンジニアリングに数え切れないほどの時間を費やすことを回避できることを期待している。

また、GAMの正式な演算定義と公理的定義を示すが、これらは等価であることが証明されている。

公理的定義は、すべての正当なプログラム動作が満たさなければならない公理の集合であり、充足可能性モジュロ理論ソルバーと組み合わせて、特定のプログラム動作が許されるか許されないかをチェックすることができる[23]、[27]、[28]。プログラムを実行する抽象的なマシンである演算定義は、実際のハードウェア動作の非常に自然な表現であり、プログラム[29]とハードウェア[30]の両方について、帰納法に基づく形式的証明で使用できる。

GAMを既存のモデルと完全に一致させることは試みないが、GAMが他のモデルに匹敵する性能を持つことをシミュレーションによって示す。

要約すると、本論文は以下の貢献をする：