Jak mogę zweryfikować algorytmy bez blokady?

Spin jest rzeczywiście doskonały, ale rozważmy również Relacy Race Detector autorstwa Dmitrija V ' Żukowa. Jest przeznaczony do weryfikacji algorytmów współbieżnych, w tym nieblokujących (wait-/lock-free) algorytmów. Jest open source i licencjonowany.

Relacy zapewnia podstawowe funkcje synchronizacji POSIX i Windows (muteksy, zmienne warunkowe, semafory, krytyczne sekcje, zdarzenia win32, Interlocked*, itp.), więc Twoja aktualna implementacja C++ może zostać przekazana do Relacy w celu weryfikacji. Nie. potrzeba opracowania osobnego modelu algorytmu, jak w przypadku Promeli i spinu.

Relacy dostarcza C++0x std::atomic (explicit memory ordering for the win! możesz więc użyć pre-procesora #defines, aby wybrać pomiędzy implementacją Relacy A własną implementacją atomową (TBB::atomic, boost:: atomic , etc).

Planowanie jest sterowalne: dostępne są losowe, związane z kontekstem i pełne wyszukiwanie (wszystkie możliwe interleavingi).

Oto przykład relacji program. Kilka rzeczy do zapamiętania:

• $ jest makrem relacyjnym, które rejestruje informacje o wykonaniu.
• rl::var<T> oznacza zmienne" normalne " (nieatomowe), które również należy rozważyć jako część weryfikacji.

Kod:

#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>();
}

Skompiluj z normalnym kompilatorem (Relacy jest tylko nagłówkiem) i uruchom plik wykonywalny:

struct race_test
DATA RACE
iteration: 8

execution history:
[0] 0:  atomic store, value=0, (prev value=0), order=seq_cst, in race_test::before, test.cpp(14)
[1] 0:  store, value=0, in race_test::before, test.cpp(15)
[2] 0:  store, value=1, in race_test::thread, test.cpp(23)
[3] 0:  atomic store, value=1, (prev value=0), order=relaxed, in race_test::thread, test.cpp(24)
[4] 1:  atomic load, value=1, order=relaxed, in race_test::thread, test.cpp(28)
[5] 1:  store, value=0, in race_test::thread, test.cpp(29)
[6] 1: data race detected, in race_test::thread, test.cpp(29)

thread 0:
[0] 0:  atomic store, value=0, (prev value=0), order=seq_cst, in race_test::before, test.cpp(14)
[1] 0:  store, value=0, in race_test::before, test.cpp(15)
[2] 0:  store, value=1, in race_test::thread, test.cpp(23)
[3] 0:  atomic store, value=1, (prev value=0), order=relaxed, in race_test::thread, test.cpp(24)

thread 1:
[4] 1:  atomic load, value=1, order=relaxed, in race_test::thread, test.cpp(28)
[5] 1:  store, value=0, in race_test::thread, test.cpp(29)
[6] 1: data race detected, in race_test::thread, test.cpp(29)

Najnowsze wersje Relacy zapewniają również modele pamięci Java i CLI, jeśli lubisz tego typu rzeczy.

Wykrywanie rasy danych jest trudnym problemem NP [Netzer & Miller 1990]

Słyszałem o tools Lockset, i DJit+ (oni uczą go w kursie CDP). Spróbuj przeczytać slajdy i googlować, do czego się odnoszą. Zawiera kilka ciekawych informacji.

Nie wiem, jakiej platformy lub języka używasz - ale na platformie.Net istnieje projekt badawczy Microsoftu o nazwie Chess, który wygląda bardzo obiecująco, pomagając tym z nas, którzy robią wielowątkowe komponenty - w tym bez blokady.

Nie używałem go zbyt wiele, umysł.

To działa (prymitywne Wyjaśnienie) poprzez jawne przeplatanie wątków w najściślejsze możliwe sposoby, aby faktycznie zmusić swoje błędy do dziczy. Analizuje również kod, aby znaleźć wspólne błędy i złe wzorce-podobne do analizy kodu.

W przeszłości zbudowałem również specjalne wersje danego kodu (poprzez bloki # if itp.), które dodają dodatkowe informacje o śledzeniu stanu; liczniki, wersje itp., które mogę następnie zanurzyć w teście jednostkowym.

Problem polega na tym, że pisanie kodu zajmuje dużo więcej czasu i nie zawsze można dodawać tego typu rzeczy bez zmiany struktury kodu, który już tam jest.

Jeśli chcesz naprawdę zweryfikować kod bez blokady (w przeciwieństwie do wyczerpującego testowania małej instancji), możesz użyć VCC ( http://vcc.codeplex.com ), dedukcyjny weryfikator dla współbieżnego kodu C, który został użyty do weryfikacji ciekawych algorytmów bez blokady (np. listy bez blokady i Hashtable z możliwością zmiany rozmiaru za pomocą wskaźników zagrożeń, optymistyczne przetwarzanie transakcji wielowersowych, wirtualizacja MMU, różne prymitywy synchronizacji itp.). Ma modułową weryfikację i został użyty weryfikacja nietrywialnych fragmentów kodu przemysłowego(do ok. 20KLOC).

Zauważ jednak, że VCC jest weryfikatorem, a nie narzędziem do polowania na błędy; będziesz musiał zrobić znaczną adnotację na swoim kodzie, aby go zweryfikować, a krzywa uczenia się może być nieco stroma. Zauważ również, że zakłada spójność sekwencyjną(jak większość narzędzi).

BTW, peer review nie jest dobrym sposobem na weryfikację algorytmu współbieżnego (a nawet sekwencyjnego). Jest długa historia sławnych ludzi publikujących algorytmy współbieżne w ważnych czasopismach, tylko po to, aby błędy zostały odkryte po latach.