Kryteria poprawności programów współbieżnych

Przykład przetwarzania współbieżnego


W przedstawionym programie instrukcja podstawienia n := n + 1 wykonywana jest współbieżnie przez 2 wątki: A oraz B, a n jest zmienną współdzieloną przez te wątki. Innymi słowy, zmienna n znajduje się w obszarze pamięci współdzielonym przez te wątki i jest dla nich zmienną wejściowo-wyjściową. Instrukcja podstawienia wymaga wykonania operacji arytmetycznej, w związku z czym może być różnie przetłumaczona na kod maszynowy, czyli na sekwencję instrukcji wykonywanych atomowo.

W procesorach o architekturze RISC operacje arytmetyczne wykonywane są wyłącznie na rejestrach procesora, wobec czego podstawienie takie wymaga wcześniejszego załadowania zawartości komórki pamięci, przechowującej wartość zmiennej n, do odpowiedniego rejestru, dodania wartości 1 do zawartości tego rejestru, a następnie umieszczenia zmodyfikowanej wartości ponownie w pamięci pod adresem przypisanym zmiennej n. W tym celu wątek A korzysta z jakiegoś rejestru procesora, oznaczonego RA , a wątek B z rejestru RB. W szczególności może to być ten sam rejestr, ale raz występujący w kontekście wątku A, a raz w kontekście wątku B.

W procesorach o architekturze CISC powszechne są rozkazy typu odczyt ­ modyfikacja ­ zapis (ang. read-modify-write). Przykładem może być 16- lub 32-bitowa architektura intelowska z rozkazem inc , którego operand może być w pamięci. Rozkaz ten może być zatem użyty w przekładzie na kod maszynowy wysokopoziomowej instrukcja podstawienia n := n + 1.

slajd 15

Przykład przeplotu instrukcji RISC


Dwa różne przeploty operacji wątków A i B prowadzą do innych wyników. Przeplot pierwszy daje wynik zgodny z oczekiwaniami, a w przeplocie drugim wątek B czyta zmienną n po jej modyfikacji w wątku A, ale przed udostępnieniem zmodyfikowanej wartości dla otoczenia. Można zatem powiedzieć, że w momencie pobrania wartości zmiennej n przez wątek B modyfikacja miała lokalny charakter w wątku A. Innymi słowy, przedstawiony sposób modyfikacji nie jest wykonaniem instrukcji atomowej i po dwóch pierwszych operacjach wątku A nastąpiło przełączenie kontekstu na wątek B.

slajd 16

Przykład przeplotu instrukcji CISC


W przypadku procesora typu CISC można wykonać atomowo operację zwiększenia o 1 bez ryzyka niepożądanego przeplotu. Niezależnie od kolejności wykonania operacji przez oba procesy wynik jest zgodny z oczekiwaniami. Wykonanie takiej operacji w systemie wieloprocesorowym wymagałoby jednak użycia prefiksu LOCK przed instrukcją inkrementacji w programie dla wątków. W przeciwnym przypadku istnieje ryzyko, że w trakcji realizacji operacji przez jeden procesor, drugi procesor rozpocznie wykonywanie konfliktowej operacji.

slajd 17

Istota synchronizacji


Jak wydać na przedstawionym wcześniej przykładzie, nie wszystkie przeploty operacji współbieżnych procesów (wątków) są dopuszczalne z punktu widzenie oczekiwań programisty. Swobodę przeplotu należy zatem czasami ograniczyć poprzez zastosowanie mechanizmów synchronizacji w celu kontroli przepływu sterowania pomiędzy współbieżnymi procesami.

Synchronizacja na najniższym poziomie polega na wykonaniu określonych (często specjalnych) instrukcji, które powodują zablokowanie postępu przetwarzania do czasu wystąpienia określonego zdarzenia w systemie, związanego również z instrukcją synchronizującą, ale w innym wątku.

Synchronizacja na wyższym poziomie polega na użyciu w programie specjalnych konstrukcji lub odpowiednim zdefiniowaniu struktur danych, które kompilator zamienia na właściwe instrukcje synchronizujące, udostępniane przez system operacyjny lub architekturę procesora.

  • Celem synchronizacji jest kontrola przepływu sterowania pomiędzy procesami tak, żeby dopuszczalne stały się tylko przeploty instrukcji zgodne z intencją programisty.
  • Synchronizacja na najniższym poziomie polega na wykonaniu specjalnych instrukcji, które powodują zatrzymanie postępu przetwarzania.
  • Synchronizacja na wyższym poziomie polega na użyciu specjalnych konstrukcji programotwórczych lub odpowiednich definicji struktur danych.

Poprawność programów współbieżnych


Problem wyspecyfikowania intencji programisty odnośnie dopuszczalnych przeplotów wiąże się z warunkami poprawności programów współbieżnych. Ogólnie formułuje się dwie podstawowe własności:

  • bezpieczeństwo — w każdym stanie przetwarzania współbieżnego (niezależnie od przeplotu) spełniony będzie pewien warunek, zwany od nazwy własności warunkiem bezpieczeństwa,
  • żywotność — w wyniku przetwarzania, po skończonej liczbie zdarzeń, zajdzie określony (oczekiwany) warunek.
  • Własność bezpieczeństwa (ang. safety) — w każdym stanie przetwarzania muszą być spełnione pewne warunki.
  • Własność żywotności (ang. Iiveness) — w wyniku przetwarzania muszą w końcu zajść pewne warunki.

Własność uczciwości programów współbieżnych


Dodatkowo sformułować można własność uczciwości (lub inaczej sprawiedliwości, ang. fairness) programów współbieżnych. Własność ta jest uszczegółowieniem własności żywotności i precyzuje czas oczekiwania na wystąpienie określonego stanu.

Własność uczciwości zostaje tylko zasygnalizowana i nie będzie w dalszej części analizowana w prezentowanych algorytmach.

  • Uczciwość słaba — nieprzerwanie zgłaszane żądanie procesu będzie kiedyś obsłużone.
  • Uczciwość mocna — nieskończenie wiele razy zgłaszane żądanie procesu będzie kiedyś obsłużone.
  • Oczekiwanie liniowe — żądanie proces będzie obsłużone po najwyżej jednokrotnym obsłużeniu żądań innych procesów.
  • FIFO — żądania będą realizowane w kolejności zgłoszeń.