メモリ一貫性モデル

メモリ一貫性モデルは、並行スレッドが共有メモリにアクセスする際に、読み取りが観測できる値を指定し、プログラマが信頼できる順序付けの保証を定義します。

Definition

メモリ一貫性モデルとは、並行実行において読み取り操作が返す可能性のある値の形式的な仕様であり、言語、コンパイラ、およびハードウェアが尊重しなければならないメモリアクセスの順序付けを定めます。

Scope

このトピックでは、逐次一貫性から緩和された（relaxed）および弱い（weak）モデルまでの一貫性モデルの範囲、happens-before関係とデータ競合フリー（data-race-free）の保証、ハードウェアメモリ順序付け（全ストア順序など）、およびC++とJavaの言語レベルのメモリモデルについて説明します。緩和されたモデルが存在する理由、フェンスとアトミック操作が順序付けをどのように回復させるか、そして並行メモリについて健全に推論する方法についても扱います。

Core questions

• プログラムはメモリオペレーションのどの順序付けを合法的に観測できますか？
• 緩和されたメモリモデルはなぜ存在し、何を許容しますか？
• データ競合フリーの保証は、推論をどのように簡素化しますか？
• フェンスとアトミック操作はどのように順序付けを強制しますか？

Key theories

逐次一貫性

Lamportは逐次一貫性を定義しました。これは、マルチプロセッサの実行が、各プロセッサのプログラム順序を尊重する単一の操作のインターリーブとして現れる必要があるというもので、最も直感的で強力なベースラインモデルです。

緩和された一貫性とSC-for-DRF保証

AdveとGharachorlooは、緩和されたモデルと、データ競合フリーのプログラムが逐次一貫性があるかのように振る舞うという原則を説明し、性能とプログラマビリティを両立させました。

言語レベルのメモリモデル

Manson、Pugh、およびAdveは、happens-before関係を用いてJavaメモリモデルを形式化し、合法的な最適化と、競合のあるプログラムでさえも受けられる保証を定義しました。

Clinical relevance

マルチコアプロセッサと最適化コンパイラはメモリ操作を並べ替えるため、言語メモリモデルは、正しく移植性の高い並行コードを作成するために不可欠です。これらは、同期が必要な時期をプログラマに伝え、ライブラリとランタイムが提供できる保証を定義します。

History

Lamportは1979年に逐次一貫性を形式化しました。ハードウェアが性能向上のために緩和された順序付けを採用するにつれて、AdveとGharachorlooによる1996年のチュートリアルは、一貫性モデルの状況とデータ競合フリーのフレームワークを体系化しました。その後、言語設計者はメモリモデルを仕様に組み込み、Javaメモリモデル（2005年）とC++11メモリモデルが現代的なアプローチを確立しました。

Debates

競合のあるプログラムのセマンティクス

データ競合を含むプログラムに対して、もしあればどのような保証を与えるべきかという難しい問題があります。言語モデルは、「何もないところから生じる」値を防ぎつつ、積極的なコンパイラとハードウェアの最適化を許容する必要があります。

Key figures

• Leslie Lamport
• Sarita Adve
• Kourosh Gharachorloo
• William Pugh
• Jeremy Manson

Seminal works

• lamport1979
• adve1996
• manson2005

Frequently asked questions

なぜすべてのシステムが逐次一貫性を使用しないのですか？

逐次一貫性は、性能を向上させる多くのコンパイラおよびハードウェアの最適化を禁止するため、ほとんどの実際のシステムは緩和されたモデルを採用し、必要な場合にのみより強力な順序付けを回復するために同期プリミティブを提供します。

データ競合フリーの保証とは何ですか？

多くの言語メモリモデルの下では、データ競合を含まないプログラム（すべての競合するアクセスが適切に同期されている）は、メモリが逐次一貫性であるかのように振る舞うことが保証されます。