2

弱い順序の同時実行を実験するのに役立つツールは何ですか? つまり、パーシャル フェンス、弱いアトミック、取得/消費/解放セマンティクス、ロックフリー アルゴリズムなどについて学習しながら、どのサンドボックスでプレイできるでしょうか?

必要なツールまたはサンドボックスは、アルゴリズムが理論的に失敗する可能性のあるさまざまな方法を明らかにして、弱く順序付けられたスレッド化されたアルゴリズムを実行および強調します。たとえば、x86 上で物理的に実行されている場合でも、このツールは ARM タイプの障害を公開できます。

オープンソースのツールが望ましいでしょう。お知らせ下さい。

参考文献:

(参照は C++11 に向けられています。なぜなら、これがたまたまこのテーマにアプローチしたからです。しかし、私が知る限り、C++ 以外の回答が最善かもしれません。フィット。）

4

2 に答える 2

3

これは、質問が直接尋ねるものよりもかなり一般的ですが、並行システムの「モデルチェッカー」である「スピン」を見てください。オンライン マニュアルはこちら: http://spinroot.com/spin/Man/Manual.html

少し「古い学校」に感じられるかもしれませんが、興味のある仕事に適していない理由はわかりません。しかし、それは非常に一般的なものなので、ツールに問題空間を教えるには少し手間がかかります。良いニュースは、プラットフォームに依存しないことです。悪いニュースは、おそらく各コンピューター アーキテクチャを明示的にモデル化する必要があることです (たとえば、Spin は ARM と x86 の保証について本質的に認識していません)。しかし、その作業の一部は他の場所で行われている可能性があります (私は確認しませんでした)、および/またはあなたが行っていることの一部を共有して、他の人が利益を得られるようにすることができます。結局のところ、このツールはオープンソースです。

于 2013-01-04T17:32:37.460 に答える
1

http://www.cprover.org/wmm/を見て、そこにあるリンクをたどって、弱いメモリに関するツールや対応する論文、特に CAV 2013 の論文Partial Orders for Efficient BMC of Concurrent Softwareおよび CAV 2014 の論文フェンスに座らないでください: 自動フェンス挿入への静的分析アプローチは、良い出発点かもしれません。そこには、実際のサンプル コードとベンチマークもたくさんあります。

于 2014-05-06T10:55:56.983 に答える