Using TLA+ in the Real World to Understand a Glibc Bug
Using TLA+ in the Real World to Understand a Glibc Bug by Malte Skarupke TLA+ is a formal specification language that you can use to verify programs. It’s different from other formal verification systems in that it’s very pragmatic. Instead of writing proofs, it works using the simple method of running all possible executions of a program. You can write assertions and if they’re not true for any p
GCCの組込みアトミック命令の使い方 | Everyday Deadlock
ちょっと使うことがあったので、備忘録的にGCCの組込みアトミック命令の使い方についてまとめておきます。 前提知識 マルチスレッドプログラムにおいて、共有データを更新する際の定石は spin lock や mutex でデータを保護することです。 これらの道具は多くの場面において十分便利なのですが、例えば共有データが1個の int 変数のみであり、更に高頻度で更新が行われるといった場合にはやや同期のコストが高くついてしまいます。 そのような場合には、アトミック命令を用いることで同期オーバーヘッドを抑えることができます。 アトミック命令とは、複数のスレッドから実行されても、個々の命令が一つ一つ順番に適用されてゆくことが保証されている命令のことです。 (より正確には、個々の命令がとある順番で一つ一つ適用された時と同じ結果を得られることが保証されている命令のことです) 例えば、とある変数 X の値
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
