Treść książki
Przejdź do opcji czytnikaPrzejdź do nawigacjiPrzejdź do informacjiPrzejdź do stopki
1.3.Poprawnośćprogramuwspółbieżnego
7
wykonywaniupewnejliczbystrumieniinstrukcji.Wszystkiewątkirealizowanewra-
machprocesuwspółdzieląprzyznanemuzasoby,wszczególnościprzestrzeńadresową
określonegoobszarupamięcioperacyjnej.Wprzestrzenitejwątkiumieszczająwyniki
obliczeń,którenastępniemogąbyćodczytaneprzezinnewątki.Pamięćwspólnastanowi
więcmediumdokomunikowaniasięwątków.Każdywątekmateżzasobydoswego
wyłącznegoużytku,np.stos,rejestrlicznikainstrukcji.
Wielewątkówmożebyćwykonywanychwjednymprocesorzelubrdzeniumetodą
podziałuczasu(por.s.5),mówimywówczasowykonaniuwielowątkowym(ang.
multithreading).Wątkimogąbyćtakżerealizowanerównolegleprzezwieleprocesorów
lubrdzeni,jeślidostępnajestpamięćwspólna.
1.3.Poprawnośćprogramuwspółbieżnego
Poprawnośćprogramuwspółbieżnegojesttrudniejszadoudowodnienianiżprogramu
sekwencyjnego.Należybowiemwykazaćdodatkowewłasności,jakiepowinienmieć
programwspółbieżny,amianowiciewłasnościdotyczącebezpieczeństwaiżywotności.
Własnościteomówimypóźniej.Dowodypoprawnościkończącychsięprogramów
współbieżnychprzeprowadzanesąpodobniejakdlaprogramówsekwencyjnych6.Mó-
wiącogólnie,programsekwencyjnyjestpoprawny,jeślizachodząpożądanerelacje
międzyjegodanymiwejściowymiiwyjściowymi,tj.wynikamiobliczeń.Poprawność
programusekwencyjnegowyrażanajestzapomocązdaniaopostaci:
{p}S{q}7
gdzieSjestprogramem,apiqasercjamizwanymi,odpowiednio,warunkiem
wstępnym(ang.precondition)ikońcowym(ang.postcondition).Warunekwstępny
precyzujewarunki,jakiespełniajądanewejściowe,alboinaczejstanpamięci,zktórym
wykonanieprogramusięrozpoczyna.Warunekkońcowyprecyzujepożądanewarun-
ki,jakiepowinnyspełniaćwynikiobliczonewprogramie,alboinaczejstanpamię-
cipowykonaniuprogramu.Możnawięcuważać,żeprogramtransformujepamięć
komputerazzadanegostanupoczątkowegowpożądanystankońcowy.Poprawność
programusekwencyjnegoformułowanajestwdwóchetapach.Zdanie{p}S{q}jest
prawdziwewsensieczęściowejpoprawności(ang.partialcorrectness),jeżelikaż-
dekończącesięwykonanieprogramuSzdanymiwejściowymispełniającymiaser-
cjępkończysięzdanymiwyjściowymispełniającymiasercjęq.Zdanie{p}S{q}
jestprawdziwewsensiepełnejpoprawności(ang.totalcorrectness),jeżelikażde
wykonanieprogramuSzdanymiwejściowymispełniającymiasercjępkończysię,
adanewyjściowespełniająasercjęq.Takwięcwprzypadkuczęściowejpopraw-
nościniebierzesiępoduwagę,czyobliczeniaprogramuSkończąsię,czynie.
6Wniniejszympodrozdzialeanalizujemywarunkipoprawnościprogramówwspółbieżnychisekwen-
cyjnych.Warunkiteodnosząsięrównieżdoalgorytmówstanowiącychpodstawętychprogramów.Można
bowiemprzyjąć,żealgorytmyorazprogramybędąceichimplementacjamisąsemantycznierównoważne.
