Treść książki
Przejdź do opcji czytnikaPrzejdź do nawigacjiPrzejdź do informacjiPrzejdź do stopki
8
1.Procesywspółbieżne
Kończeniesięobliczeńprogramudlawszystkichprawidłowychdanychwejściowych,
tj.spełniającychasercjęp,zwanejestrównieżwarunkiemstopu(ang.stopcon-
dition).Jegoudowodnieniesprowadzasiędowykazania,żeobliczeniawszystkich
instrukcjiiteracyjnychprogramuzawszesiękończą.Przyjmujesiębowiem,żeczas
wykonaniapozostałychinstrukcjiskładającychsięzelementarnychoperacjijestskoń-
czony.Azatemwpraktycedowódpełnejpoprawnościprogramusekwencyjnego
obejmujewykazanie,żeprogramjestczęściowopoprawnyorazżespełniawarunek
stopu.
Jakstwierdziliśmywcześniej,programwspółbieżnyskładasięzkomponentów
zwanychzadaniami.Komponentymającharakterprogramówsekwencyjnych,takwięc
dowodzącpoprawnościprogramuwspółbieżnego,należynajpierwwykazaćpełnąpo-
prawnośćjegokomponentów.Ponieważprocesywspółbieżneskładającesięnawy-
konanieprogramuwspółbieżnegozreguływspółpracujązesobą,należywykazać
jeszczedodatkowewłasności,któredotycząbezpieczeństwa(ang.safety)orazży-
wotności(ang.liveness).Własnościzwiązanezbezpieczeństwemtowarunki,któ-
repowinnybyćzawszespełnione,tj.dlawszystkichmożliwychrealizacjiprocesów
współbieżnych.Zkoleiwłasnościżywotnościtowarunki,którepowinnybyćnwkoń-
cu”spełnione.Oznaczato,żejeślipowinnozajśćpewnezdarzenie,todlakażdej
możliwejrealizacjiprocesówwspółbieżnychwpewnymmomencieonorzeczywiście
zachodzi.
Procesywspółbieżnewtrakciewykonywaniaczęstorywalizujązesobą,próbując
uzyskaćdostępdowspólnieużytkowanychzasobów.Mogątobyćzmiennewpamięci
wspólnej,pliki,urządzeniawe/wy,np.drukarkalubmonitorkomputera.Wtakimprzy-
padkumamydoczynieniazwłasnościąbezpieczeństwapolegającąnatym,bywżad-
nymmomenciewykonywaniaprogramuwspółbieżnegozdanegozasobuniekorzystał
więcejniżjedenproces.Tęwłasnośćbezpieczeństwaokreślasięmianemwzajemnego
wykluczania(ang.mutualexclusion).Innąwłasnościąbezpieczeństwajestbrakblo-
kady.Występujeonawtedy,gdyjedenlubwięcejprocesówsięniekończy7.Blokada
możepowstaćpodczassynchronizowaniaprzezprocesyswoichdziałań.Załóżmy,żedo
synchronizacjisłużyinstrukcjawait(z),gdziezmiennazoznaczazdarzenie.Wykonanie
instrukcjipoleganaczekaniuprzezproces,ażzajdziezdarzeniez.Oczywiście,jeśli
zdarzenieniezajdzie,toprocesbędziezablokowanyisięnieskończy.Blokadamoże
takżedotyczyćzbioruprocesów,zwanajestwówczaszakleszczeniem(ang.deadlock).
Pojawiasięonowtedy,gdykażdyzprocesównależącychdodanegozbioruprocesów
jestwstrzymanywoczekiwaniunazdarzenie,któremożebyćspowodowanetylko
przezjakiśinnyprocesztegozbioru.Wpodanychsytuacjachwarunekpoprawnego
zakończeniaobliczeńprogramuwspółbieżnegopolegającynatym,abywszystkiejego
procesyzakończyłyswojedziałanie,niebędziespełniony.Dowodzącbrakublokady,
7Rozważamytutajprogramywspółbieżne,którychprocesypowinnysiękończyć.Istniejątakżepro-
gramyskładającesięzprocesówdziałającychnieskończeniedługo.Przykłademmogąbyćprocesysystemu
operacyjnegokomputeralubprocesyprogramu,którymonitorujestanbezprzerwypracującegourządzenia,
odbierająciprzetwarzającdanewysyłaneprzezjegoczujniki.
