#godocreading 第9回のおさらい
Nobishii
C++
C++のメモリモデルはDRF-SC or Catch Fire、つまりDRFではない場合は何が起きてもおかしくない
atomicsは3種類提供されている
- sequentially consistent atomics
- aquire/release(coherence) atomics
- relaxed atomics
relaxed atomics
synchronizingではないatomicsも導入した。それがrelaxed atomicsとよばれる。(memory_order_relaxed)
これは同期する効果を一切持たない(つまりhappens-before edgeを作らない）し順序の保証も全く持たない。通常変数との唯一の違いはdata raceとみなされないのでcatch fireが許されないことである。
Java(2004)メモリモデルの複雑性はraceのあるプログラムの振る舞いを定義したことからきている。C++はDRF-SC or Catch Fireを採用して実質的にdata raceのあるプログラムを禁止したことになるので、以前にみた複雑な例をほうりなげることができてJavaよりもシンプルな言語仕様になるという期待もあった。しかし実際にはそうならなかった。relaxed atomicsがあるから。
Non-Racy Out Of Thin Air ValuesテストはC++11の通常変数ではnoになるがrelaxed atomicsではYesになってしまう。
C++11モデルはOut Of Thin Air Valuesを禁止するためのformalな定義とinformalな文章を持っていたが、このformalな部分に問題があったので、C++14モデルでは取り除かれた。
まとめると、Javaはformalに非因果的振る舞いを除外しようとしてうまくいかなかった。C++11はそれをふまえて非因果的振る舞いの一部だけをformalに除外しようとしてやはり失敗した。C++14はformalな規定を何も置かなくなった。正しい方向には向かっていない。
TBW
C, Rust and Swift Memory Models
C11はC++11メモリモデルを採用した。→C/C++11メモリモデル
Rust 1.0.0とSwift5.3もC/C++メモリモデル
これらはC/C++コンパイラツールチェイン(LLVM)の上で作られていてC/C++コードとのインテグレーションを謳っているので不思議ではない
Hardware Digression: Efficient Sequentially Consistent Atomics
効率的な逐次一貫的アトミクス
初期のマルチプロセッサアーキテクチャは様々な同期機構、様々なメモリモデルがあり、使いやすさも様々だった。この多様性のなかで、異なる同期抽象の効率性は、それがアーキテクチャが提供するものへとどれくらいうまく対応付けられているか次第だった。逐次一貫的なアトミック変数の抽象を構築するには、あるときにはバリアをつかうのが唯一の選択肢であり、それはきっちりと必要とされるよりも余分なことをしており、はるかに高価だった。特にARMやPOWERにおいては。
C, C++, Javaはいずれも逐次一貫的な同期アトミクスという同一の抽象を提供しているので、ハードウェア設計者にとってはその抽象を効率的にするのが当然のこととなった。ARMv8アーキテクチャ(32bitと64bit両方)はldarとstlrというload/store命令を導入して、(注：逐次一貫的アトミクスの）直接的な実装を提供した。2017年のトークにおいて、Herb SutterはIBMが将来のPOWER実装は逐次一貫的アトミクスのより効率的な何らかのサポートを行うので、プログラマにとってrelaxed atomicsを使う理由は少なくなるだろう、ということを彼が言うことをIBMが承認した、と述べた。ただ2021年においてPOWERはARMv8よりもrelevantではなくなっており、私はこれが実際に起ったかどうかわからない。
この収束の結果、逐次一貫的アトミクスは現在ではより良く理解されており、すべての主要なハードウェアプラットフォームで効率的に実装されることができる。なので、プログラム言語メモリモデルにとって良いターゲットとなった。
JavaScript Memory Model(2017)
JavaScriptはシングルスレッド言語だからメモリモデルの心配はない、
そう考えていたころが私にもありました。
JavaScriptにはweb workerがあるので、異なるスレッドでコードを走らせることができる。最初のころは、workersはJavaScriptのメインスレッドと、明示的なメッセージコピーによってのみ通信していた。しかし、ES2017はSharedArrayBufferobjectを追加して、メインスレッドとワーカーとが書込み可能なメモリブロックを共有できるようになった。なぜこうしたのか？プロポーザルの初期のドラフトでは、最初の理由としてあげられていたのはC++のマルチスレッドコードをJavaScriptにコンパイルするためだった。
もちろん、共有された書き込み可能メモリは、同期のためのアトミック演算とメモリモデルを要求する。そのメモリモデルにおいて、JavaScriptはC++といくらかの点で違う:
- 逐次一貫的atomicsしかない
- DRF-SC or Catch Fireではなくracyなプログラムに対する振る舞いも定義されている
- atomic/non-atomicアクセスが同じメモリ位置に行われたときや、異なるサイズのアクセスが行われたときの振る舞いも定義されている
正確にracy programの振る舞いを定義することは、緩和されたメモリ意味論や、どのようにout-of-thin-air読み込みを禁止するか、などといったことについてのよくある複雑性をもたらす。これらの難しさにくわえて、ほかのメモリモデルと同様に、ES2017における定義は2つの興味深いバグがあった。これはあたらしいARMv8のアトミック命令のセマンティクスとのミスマッチから生まれたものだ。これらの例はConrad Wattなどの2020年の論文"Repairing and Mechanising the JavaScript Relaxed Memory Model"から翻案されたものだ。
前のセクションで触れたように、ARMv8はldarとstlr命令を追加して、逐次一貫的なアトミック読み込み・書き込みを提供した。これらはC++をターゲットにしていたが、C++はdata raceのあるプログラムの振る舞いを定めていない。だとすれば驚くには当たらないが、racy programでのこれらの命令の振る舞いは、ES2017の作者の期待とは合わなかった。特に、ES2017のracy programの振る舞いに対するES2017の要請を満たさない。
<Litmus Test: ES2017 racy reads on ARMv8>
r1 = 0, r2 = 1は起こりうるか？
| Thread 1 | Thread 2 |
|---|---|
| x = 1 | y = 1 |
| r1 = y | x = 2(non-atomic) |
| r2 = x |
- C++: yes
- Java: このプログラムは書けない
- ARMv8で
ldar/stlrを使う Yes - ES2017: no! (ARMv8と矛盾する)
NobishiiJavaでこのプログラムは書けないのなんでかとおもったけどatomic関数がなくてatomic変数だけあるからな気がする。Go1.19でいうとatomic.Int64とかはあるけどatomic.LoadInt64/StoreInt64はない状態。だとすると1箇所の書き込みだけnon-atomicにするのは確かにむり
Nobishii勘違いで、再現できてなかった
Nobishii- Goのメモリモデル上起きうる結果をすべて挙げる
- とくにdata raceを発生しないexecutionが存在するかどうか
というような追加の問いかけができる。暇なとき考える