メモリモデル
以下のGo のメモリモデルの正式な定義は、PLDI 2008 で発表された Hans-J. Boehm と Sarita V. Adve による “Foundations of the C++ Concurrency Memory Model” で提示されたアプローチに密接に従っています。データレースフリープログラムの定義と、レースフリープログラムの逐次一貫性の保証は、その研究と同等です。
メモリモデルは、プログラム実行の要求を記述します。プログラム実行はゴルーチン実行で構成され、ゴルーチン実行はさらにメモリ操作で構成されます。
メモリ操作は、4つの詳細によってモデル化されます：
- その種類（通常のデータ読み取り、通常のデータ書き込み、またはアトミックデータアクセス、ミューテックス操作、チャネル操作などの同期操作であるかどうかを示す）
- プログラム内での位置
- アクセスされるメモリ位置または変数
- 操作によって読み取りまたは書き込まれる値
一部のメモリ操作は読み取り様で、読み取り、アトミック読み取り、ミューテックスロック、チャネル受信が含まれます。他のメモリ操作は書き込み様で、書き込み、アトミック書き込み、ミューテックスアンロック、チャネル送信、チャネルクローズが含まれます。アトミック比較・交換など、読み取り様と書き込み様の両方の性質を持つものもあります。
ゴルーチン実行は、単一のゴルーチンによって実行されるメモリ操作の集合としてモデル化されます。
要求 1：各ゴルーチンのメモリ操作は、メモリから読み取りおよび書き込みされた値を考慮して、そのゴルーチンの正しい逐次実行に対応しなければなりません。その実行は、逐次先行関係と一貫していなければなりません。逐次先行関係は、Go言語仕様によって設定されたGo の制御フロー構造の部分順序要求と、式の評価順序によって定義されます。
Go のプログラム実行は、ゴルーチン実行の集合として、各読み取り様操作がどの書き込み様操作から読み取るかを指定するマッピング W とともにモデル化されます。（同じプログラムの複数の実行は、異なるプログラム実行を持つことができます。）
要求 2：与えられたプログラム実行について、マッピング W は、同期操作に限定された場合、順序付けとそれらの操作によって読み取りおよび書き込みされた値と一貫性のある同期操作の暗黙の全順序によって説明できなければなりません。
同期先行関係は、W から導出される同期メモリ操作の部分順序です。同期読み取り様メモリ操作 r が同期書き込み様メモリ操作 w を観測する場合（つまり、W(r) = w の場合）、w は r の前に同期されます。非公式には、同期先行関係は、前の段落で言及された暗黙の全順序のサブセットであり、W が直接観測する情報に限定されます。
事前発生関係は、逐次先行関係と同期先行関係の和集合の推移的閉包として定義されます。
要求 3：メモリ位置 x での通常の（非同期）データ読み取り r について、W(r) は r に対して可視な書き込み w でなければなりません。可視とは、以下の両方が成り立つことを意味します：
- w は r の前に事前発生します。
- w は、r の前に事前発生する（x への）他の書き込み w’ の前に事前発生しません。
メモリ位置 x での読み取り・書き込みデータレースは、x での読み取り様メモリ操作 r と x での書き込み様メモリ操作 w で構成され、そのうち少なくとも一方は非同期であり、事前発生によって順序付けられていません（つまり、r が w の前に事前発生することも、w が r の前に事前発生することもありません）。
メモリ位置 x での書き込み・書き込みデータレースは、x での2つの書き込み様メモリ操作 w と w’ で構成され、そのうち少なくとも一方は非同期であり、事前発生によって順序付けられていません。
メモリ位置 x で読み取り・書き込みまたは書き込み・書き込みデータレースがない場合、x での任意の読み取り r は、W(r) に対して1つの可能性しかありません：事前発生順序でそれの直前にある単一の w です。
より一般的には、データレースフリーである Go プログラム（読み取り・書き込みまたは書き込み・書き込みデータレースを持つプログラム実行がない）は、ゴルーチン実行の逐次一貫性のあるインターリーブによってのみ説明できる結果を持つことが示されます。（証明は、上で引用された Boehm と Adve の論文のセクション 7 と同じです。）この特性は DRF-SC と呼ばれます。
正式な定義の意図は、C、C++、Java、JavaScript、Rust、Swift を含む他の言語によってレースフリープログラムに提供される DRF-SC 保証と一致することです。
ゴルーチン作成やメモリ割り当てなど、特定の Go 言語操作は同期操作として機能します。これらの操作の同期先行部分順序への影響は、以下の「同期」セクションで文書化されています。個々のパッケージは、独自の操作について同様の文書を提供する責任があります。