3685666187

Poprawność programów sekwencyjnych

W przypadku programów sekwencyjnych definicja poprawności wymaga spełnienia dwóch warunków: warunku stopu oraz tego, że dla dowolnych poprawnych danych wejściowych program/algorytm po zatrzymaniu da poprawne wyniki Poprawność programów współbieżnych

•    Bezpieczeństwo - niedopuszczalność do sytuacji niepożądanej (wykluczenie stanu niepożądanego)

•    Żywotność - każdy proces w końcu wykona swoją pracę (w szczególności: otrzyma dostęp do współdzielonego zasobu)

Przejawy braku żywotności

•    Zakleszczenie (deadlock) - globalny brak żywotności; dotyczy blokady całego systemu współbieżnego (zakleszczają się co najmniej dwa procesy/wątki). Jest łatwiejsze do wykrycia (ze względu na swój globalny charakter)

•    Zagłodzenie (wykluczenie, lockout, starvation) - lokalny brak żywotności. W jakich warunkach może dojść do zagłodzenia i jak eliminować takie warunki?

W ogólności klasyczne testowanie programów nie daje dowodu na to, że dany program jest poprawny    13