godocreading #10 ノート
Nobishiigodocreading #10
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と矛盾する)
NobishiiGo言語に翻訳してみる
Nobishiiこのプログラムでは、x=2以外はすべて逐次一貫的なアトミクスでreadとwriteが行われる。スレッド1はatomicにx=1として書き込みしているが、スレッド2はatomicではない書き込みでx=2を行う。C++ではデータレースなので何が起きてもおかしくない。Javaではこのプログラムは書けない。xはvolatileかそうでないかどちらかで宣言されないといけないから、あるときだけアトミックにアクセスされることはありえない。ES2017では、メモリモデルがr1 = 0, r2 =1は許さないことになっている。もしr1 = yが0であればスレッド1はスレッド2が始まる前に完了していないといけない。その場合はx = 2はx = 1を上書きする。なのでr2 = xは2となる。これはすべて最もに思えるが、ARMv8プロセッサはこのようには動かない。
NobishiiARMv8命令で等価なシーケンスにおいては、...
NobishiiLitmus Test: ES2017 data-race-free program
| T1 | T2 |
|---|---|
x = 1 |
|
NobishiiES2017スペックのメモリモデルは一方では強すぎて、一方では弱すぎた。
先述のようにこれは修正された。それでも、これはdata race freeなプログラムとそうでないプログラムの両方にセマンティクスをhappens-beforeだけをつかって特定することがいかに微妙で難しいことかということ、そしてプログラム言語めもりもでるとハードウェアモデルをマッチさせることがいかに難しいことかということ、に対するもう一つのリマインダーだ。
Nobishiiいまのところ、JavaScriptは逐次一貫的以外のアトミクスを提供することを避けてきたこととDRF-SC or Catch-Fireを拒否してきた。これは勇気づけられることである。結果として、C/C++のコンパイルターゲットとして有効だがJavaに近いメモリモデルになっている。
Nobishii結論(プログラム言語メモリモデルの）
C, C++, Java, JavaScript, Rust, Swiftをみると、つぎのことがわかる
- すべて、並列なプログラムのnon-atomicな部分を整えるための逐次一貫的な同期アトミクスをていきょうしている。
- すべて、正しい同期によってDRFになったプログラムは逐次一貫的に振る舞うことを保証することを目指している
- Javaは弱い(aquuire/release)atomicsの導入を避けてきたが、Java9でVarHandleを導入した。JavaScriptは今のところまだこれを避けている
- これらはすべて、意図的なデータレースを起こしつつ残りの部分を無効化しないプログラムを書く方法を提供している。C, C++, Rust, Swiftではその仕組とはrelaxed non-synchronizing atomicsである。 Javaでは通常のメモリアクセスかVarHandleのplainアクセスモードである。JavaScriptでは通常のメモリアクセスである。
- どの言語も、out-of-thin-air valuesのようなパラドックスをフォーマルに禁止する方法を見つけることはできておらず、informalにこれを禁止している。
Nobishii英語難しいやつ
They all aim to guarantee that programs made data-race-free using proper synchronization behave as if executed in a sequentially consistent manner.
"I made this program data-race-free using proper synchronization." の受動態
構文木っぽいもの
- They all aim to guarantee
- that (以下that節)
- the programs (that節の主語)
- made data-race-free (過去分詞madeの形容詞用法でthe programsを修飾する)
- using proper synchronization(現在分詞usingでmadeを修飾する)
- made data-race-free (過去分詞madeの形容詞用法でthe programsを修飾する)
- behave (that節の述語)
- as if executed in a sequentially consistent manner.
- the programs (that節の主語)
- that (以下that節)
Nobishii一方で、プロセッサ製造者は、逐次一貫的同期アトミクスの抽象を効率的に実装することは重要であるということを受け入れてきたように見えるし、実際にそうし始めている。ARMv8やRISC-Vは両方とも直接的なサポートを提供している。
Nobishii最後に、これらのシステムを理解し、これらの振る舞いを正確に記述するための本当にすごい量の検証や形式的分析の研究が行われてきた。Watt(2020)がJavaScriptのかなりの部分を占めるサブセットのフォーマルなモデルを与えて、そのARM, POWER, RISC-V, x86-TSOへのコンパイルの正当性の証明に定理証明器を用いたことは特に勇気づけられることだ。
NobishiiはじめのJavaメモリモデルから25年、そして多くの人-世紀にわたる研究の努力をへて、我々はメモリモデル全体を定式化できはじめるかもしれない。もしかしたら、ある日、それを完全に理解することもできるかもしれない。
次のポストは “Updating the Go Memory Model”だ。
NobishiiUpdating the Go Memory Model
今のメモリモデルは2009年に描かれたあとマイナーなアップデートしかしてない
Nobishiiendorsement 裏付け、承認
NobishiiGoのデザイン思想を改めて述べ、現在のメモリモデルをまとめて、私が行うべきだと考えているメモリモデルの比較的小さな修正について概略を述べたい。前の2つのブログを読んでいることを仮定する。
NobishiiHoareのレクチャー
ソフトウェア設計には2つの方法がある:
Nobishiiよくあるプログラムのミスにたいするよく定義されたセマンティクスを持っているということも、Goにとって重要なポイントだ
NobishiiHoareのことば
シンプルに使えることと同じように、ソフトウェアプログラムは間違って使うのが難しくなければいけない。プログラミングの間違いに対して親切でなければいけない、間違いには明確な知らせがあるべきだし、間違いの効果が予測不可能であってはならない
Nobishiiバグのあるプログラムにもよく定義されたセマンティクスがあるべきだというコモンセンスは、思うほど一般的に浸透しているものではない。
C/C++では、未定義動作がある種の自由裁量になっていた。どういう自由裁量かというと、わずかにバグったプログラムを、ぜんぜん違う形でバグったプログラムに変換する自由だ
Nobishii
Integer overflow
For unsigned integer values, the operations +, -, *, and << are computed modulo 2n, where n is the bit width of the unsigned integer's type. Loosely speaking, these unsigned integer operations discard high bits upon overflow, and programs may rely on "wrap around".
For signed integers, the operations +, -, *, /, and << may legally overflow and the resulting value exists and is deterministically defined by the signed integer representation, the operation, and its operands. Overflow does not cause a run-time panic. A compiler may not optimize code under the assumption that overflow does not occur. For instance, it may not assume that x < x + 1 is always true.