Czy można udowodnić bezpieczeństwo wątków?

Biorąc pod uwagę program składający się ze zmiennych i instrukcji, które modyfikują te zmienne, oraz operację podstawową synchronizacji (monitor, mutex, Java zsynchronizowany lub blokada C #), czy można udowodnić, że taki program jest bezpieczny dla wątków?

Czy istnieje nawet formalny model opisujący takie rzeczy, jak bezpieczeństwo wątków lub warunki wyścigowe?

Trudno jest udowodnić, że program jest „wątkowo bezpieczny”. Możliwe jest jednak konkretne i formalne zdefiniowanie terminu „wyścig danych”. Możliwe jest określenie, czy ślad wykonania określonego uruchomienia programu ma wyścig danych w czasie proporcjonalnym do wielkości śledzenia. Ten rodzaj analizy sięga co najmniej 1988 roku: Barton P. Miller, Jong-Deok Choi, „Mechanizm skutecznego debugowania programów równoległych”, Conf. na Prog. Lang. Dsgn. i Impl. (PLDI-1988): 135-144 .

Biorąc pod uwagę ślad wykonania, najpierw definiujemy zdarzenie przed częściowym porządkiem między zdarzeniami w śladzie. Biorąc pod uwagę dwa wydarzenia$a$ i $b$ które występują wtedy w tym samym wątku $a < b$ lub $b < a$. (Zdarzenia w tym samym wątku tworzą całkowitą kolejność nadaną przez semantykę sekwencyjną języka programowania.) Zdarzenia synchronizacji (mogą to być na przykład mutex rejestrujące i zwalniające), dają dodatkowy interwątek przed częściowym uporządkowaniem. (Jeśli wątek$S$ uwalnia muteks, a następnie wątek $T$ nabywa ten muteks, który mówimy, że wydanie następuje - zanim przejdzie.)

Następnie dane dwa dostępu do danych (odczytuje lub zapisuje zmienne, które nie są zmiennymi synchronizacyjnymi)$a$ i $b$ które znajdują się w tej samej lokalizacji w pamięci, ale według różnych wątków i gdzie $a$ lub $b$ to operacja zapisu, o której mówimy, że pomiędzy nimi odbywa się wyścig danych $a$ i $b$ jeśli żaden $a < b$ ani $b < a$.

Standard C ++ 11 jest dobrym przykładem. (Odpowiednia sekcja to 1.10 w specyfikacjach wersji roboczych dostępnych online). C ++ 11 rozróżnia obiekty synchronizacji (muteksy i zmienne zadeklarowane z atomic<>typem) i wszystkie inne dane. Specyfikacja C ++ 11 mówi, że programista może uzasadnić dostęp do danych na podstawie śladu programu wielowątkowego, tak jakby był sekwencyjnie spójny, jeśli dostęp do danych jest wolny od wyścigu danych.

Narzędzie Helgrind (część Valgrind) wykonuje tego rodzaju wykrywanie oparte na danych zdarzeniowych, podobnie jak kilka komercyjnych narzędzi (np. Intel Inspector XE). Algorytmy w nowoczesnych narzędziach polegają na utrzymywaniu zegarów wektorowych związanych z każdym wątkiem i synchronizacją obiekt. Myślę, że tę technikę wykorzystania zegarów wektorowych do wykrywania wyścigów danych zapoczątkował Michiel Ronsse; Koen De Bosschere: „RecPlay: w pełni zintegrowany praktyczny system nagrywania / odtwarzania”, ACM Trans. Comput. Syst. 17 (2): 133–152, 1999 .

Od strony praktycznej istnieje system weryfikacji VCC, który może być użyty do formalnego udowodnienia bezpieczeństwa wątków programów C.

Oto cytat ze strony internetowej:

VCC obsługuje współbieżność - możesz użyć VCC do weryfikacji programów, które używają zarówno współgrubnej, jak i drobnoziarnistej współbieżności. Możesz go nawet użyć do weryfikacji operacji podstawowych kontroli współbieżności. Weryfikacja funkcji niejawnie gwarantuje bezpieczeństwo wątków w każdym współbieżnym środowisku, które szanuje kontrakty dotyczące jej funkcji i struktur danych.

Jest to bardzo trudny obszar, aby zapewnić poprawność programu w zakresie wykluczającym warunki wyścigu, rodzaj „pięty achillesowej” równoległego przetwarzania. Najlepszym podejściem do poprawności programu jest na ogół unikanie podstawowych operacji niskiego poziomu i praca z wzorcami projektowymi wyższego poziomu (np. Z bibliotek), które zapewniają synchronizację wątków. Istnieje jeden model CSP, komunikujący sekwencyjne procesy przez Hoare, który ma pewne dowody poprawności, biorąc pod uwagę, że programiści ograniczają się do „frameworka”. Ma pewne podobieństwo koncepcyjne i chronologiczne pochodzenie / nakładanie się na uniksowe „potoki i filtry”, chociaż nie udało się (jeszcze?) Znaleźć bezpośredniego związku między nimi.

Dwa inne frameworki, które próbują poprawić poprawność równoległości poprzez wzorce projektowe i które mają większość standardowych / znanych algorytmów / wzorców projektowych do tego celu:

• Bloki konstrukcyjne wątku Intel
• Biblioteka współbieżności Java [nieco niedawno zintegrowana z głównym językiem]