26

理論的には、少なくともブルートフォースでロックフリーアルゴリズムの検証を行うことができるはずです（交差する関数呼び出しの組み合わせは非常に多くあります）。ロックフリーアルゴリズムが正しいことを実際に証明するために利用できるツールまたは正式な推論プロセスはありますか（理想的には、競合状態やABA問題もチェックできるはずです）？

注：1つのポイントを証明する方法（たとえば、ABA問題から安全であることを証明するだけ）または私が言及していない問題を知っている場合は、とにかく解決策を投稿してください。最悪のシナリオでは、各メソッドを順番に実行して、完全に検証できます。

4

5 に答える 5

21

あなたは間違いなくスピンモデルチェッカーを試してみるべきです。

プログラムのようなモデルをPromelaと呼ばれる単純なCのような言語で記述します。これは、Spinが内部でステートマシンに変換します。モデルには、複数の並列プロセスを含めることができます。

次に、Spinは、テストする条件（通常、競合状態がない、デッドロックがないなど）について、各プロセスからの命令の可能なすべてのインターリーブをチェックします。これらのテストのほとんどは、ステートメントを使用して簡単に記述できます。アサーションに違反する可能性のある実行シーケンスがある場合は、シーケンスが出力されます。それ以外の場合は、「オールクリア」が与えられます。assert()

（実際には、これを実現するためにはるかに高度で高速なアルゴリズムを使用していますが、それが効果です。デフォルトでは、到達可能なすべてのプログラム状態がチェックされます。）

これは素晴らしいプログラムで、2001年のACMシステムソフトウェア賞を受賞しました（他の受賞者には、Unix、Postscript、Apache、TeXが含まれます）。私はそれを非常に早く使い始め、数日でMPI機能のモデルMPI_Isend()とMPI_Irecv()Promelaを実装することができました。Spinは、テストのためにPromelaに変換した並列コードの1つのセグメントで、いくつかのトリッキーな競合状態を発見しました。

于 2010-01-15T14:05:19.673 に答える
8

スピンは確かに優れていますが、 DmitriyV'jukovによるRelacyRaceDetectorも検討してください。これは、非ブロッキング（待機/ロックフリー）アルゴリズムを含む並行アルゴリズムを検証するために設計されています。それはオープンソースであり、自由にライセンスされています。

RelacyはPOSIXおよびWindows同期プリミティブ（ミューテックス、条件変数、セマフォ、CriticalSections、win32イベント、Interlocked *など）を提供するため、実際のC++実装を検証のためにRelacyにフィードできます。PromelaやSpinのように、アルゴリズムの別のモデルを開発する必要はありません。

RelacyはC++0x std::atomic（winの明示的なメモリ順序付け！）を提供するため、プリプロセッサ#definesを使用して、Relacyの実装と独自のプラットフォーム固有のアトミック実装（tbb :: atomic、boost :: atomicなど）のどちらかを選択できます。

スケジューリングは制御可能です。ランダム、コンテキストバウンド、および完全検索（すべての可能なインターリーブ）が利用可能です。

これがRelacyプログラムの例です。注意すべきいくつかのこと：

  • は$、実行情報を記録するRelacyマクロです。
  • rl::var<T>検証の一部として考慮する必要がある「通常の」（非アトミック）変数にフラグを立てます。

コード：

#include <relacy/relacy_std.hpp>

// template parameter '2' is number of threads
struct race_test : rl::test_suite<race_test, 2>
{
    std::atomic<int> a;
    rl::var<int> x;

    // executed in single thread before main thread function
    void before()
    {
        a($) = 0;
        x($) = 0;
    }

    // main thread function
    void thread(unsigned thread_index)
    {
        if (0 == thread_index)
        {
            x($) = 1;
            a($).store(1, rl::memory_order_relaxed);
        }
        else
        {
            if (1 == a($).load(rl::memory_order_relaxed))
                x($) = 2;
        }
    }

    // executed in single thread after main thread function
    void after()
    {
    }

    // executed in single thread after every 'visible' action in main threads
    // disallowed to modify any state
    void invariant()
    {
    }
};

int main()
{
    rl::simulate<race_test>();
}

通常のコンパイラ（Relacyはヘッダーのみ）でコンパイルし、実行可能ファイルを実行します。

struct race_test
データレース
反復：8

実行履歴：
[0] 0：アトミックストア、value = 0、（prev value = 0）、order = seq_cst、race_test :: before、test.cpp（14）
[1] 0：store、value = 0、race_test :: before、test.cpp（15）
[2] 0：ストア、値= 1、race_test :: thread、test.cpp（23）
[3] 0：アトミックストア、value = 1、（prev value = 0）、order = Relaxed、race_test :: thread、test.cpp（24）
[4] 1：アトミックロード、value = 1、order = Relaxed、race_test :: thread、test.cpp（28）
[5] 1：store、value = 0、race_test :: thread、test.cpp（29）
[6] 1：race_test :: thread、test.cpp（29）でデータ競合が検出されました

スレッド0：
[0] 0：アトミックストア、value = 0、（prev value = 0）、order = seq_cst、race_test :: before、test.cpp（14）
[1] 0：store、value = 0、race_test :: before、test.cpp（15）
[2] 0：ストア、値= 1、race_test :: thread、test.cpp（23）
[3] 0：アトミックストア、value = 1、（prev value = 0）、order = Relaxed、race_test :: thread、test.cpp（24）

スレッド1：
[4] 1：アトミックロード、value = 1、order = Relaxed、race_test :: thread、test.cpp（28）
[5] 1：store、value = 0、race_test :: thread、test.cpp（29）
[6] 1：race_test :: thread、test.cpp（29）でデータ競合が検出されました

Relacyの最近のバージョンでは、そのようなことに興味がある場合は、JavaおよびCLIメモリモデルも提供されています。

于 2010-02-02T11:29:52.873 に答える
4

使用しているプラ​​ットフォームや言語はわかりませんが、.Netプラットフォームには、ロックフリーを含むマルチスレッドコンポーネントを実行する私たちを支援することを非常に期待しているChessというMicrosoftResearchプロジェクトがあります。

私はそれをあまり使用していません、気に。

これは、スレッドを可能な限り厳密な方法で明示的にインターリーブして、バグを実際に野生に追い出すことによって機能します（大まかな説明）。また、コードを分析して、コード分析と同様に、よくある間違いや悪いパターンを見つけます。

過去に、状態追跡情報を追加する特別なバージョンのコードを（#ifブロックなどを介して）作成しました。カウント、バージョンなど、単体テスト内で調べることができます。

それに関する問題は、コードを書くのにもっと時間がかかることです。そして、すでにそこにあるコードの基礎となる構造を変更せずに、この種のものを常に追加できるとは限りません。

于 2010-01-15T13:46:43.070 に答える
4

データ競合の検出はNP困難な問題です[Netzer＆Miller 1990]

LocksetツールとDJit+ツールについて聞いたことがあります（CDPコースで教えています）。スライドを読んで、それらが参照しているものをグーグルで検索してみてください。いくつかの興味深い情報が含まれています。

于 2010-01-15T13:54:12.380 に答える
4

（小さなインスタンスを徹底的にテストするのではなく）ロックフリーコードを実際に検証したい場合は、検証に使用された同時Cコードの推論ベリファイアであるVCC（ http://vcc.codeplex.com ）を使用できます。いくつかの興味深いロックフリーアルゴリズム（たとえば、ハザードポインター、楽観的なマルチバージョントランザクション処理、MMU仮想化、さまざまな同期プリミティブなどを使用したロックフリーリストとサイズ変更可能なハッシュテーブル）。モジュール式の検証を行い、重要な産業用コードのチャンク（最大約20KLOC）を検証するために使用されています。

ただし、VCCは検証ツールであり、バグハンティングツールではないことに注意してください。コードを検証するには、コードにかなりの注釈を付ける必要があり、学習曲線は少し急になる可能性があります。また、（ほとんどのツールと同様に）逐次一貫性を前提としていることにも注意してください。

ところで、ピアレビューは並行アルゴリズム（または順次アルゴリズム）を検証するための良い方法ではありません。有名な人々が重要なジャーナルで並行アルゴリズムを公開してきた長い歴史がありますが、数年後にバグが発見されました。

于 2013-11-05T09:42:40.673 に答える