hrvatski

Dinamičke algebre i korektnost paralelnih programa

U ovom radu je razvijena semantika nekoliko različitih tipova paralelnih programskih jezika (nezavisni ili disjunktni programi, programi sa zajedničkom memorijom i kritičnim područjima i programi sa sinkronizacijom) utemeljene na dinamičkim algebrama Y.Gurevicha. U toj semantici je interpretiran postojeći račun dokazivanja parcijalne, odnosno totalne korektnosti. Rezultati posljednjih četiriju poglavlja su novi i predstavljaju doprinos matematičkoj semantici paralelnih programskih jezika i metodologiji dinamičkih algebri. Ti rezultati pokazuju da pojam distribuirane dinamičke algebre i njezinog hoda imaju dovoljnu semantičku snagu da elegantno interpretiraju semantički najneugodnije konstrukte paralelnih programa sa zajedničkom memorijom. U prvoj glavi "Uvod" su dana uvodna razmatranja i kratak pregled ciljeva rada. U drugoj glavi "Uvodne leme" su dane pomoćne tvrdnje koje se koriste u ostalim glavama. Treća glava, "Hod", je posvećena definiranju i opisu glavnog 'oruđa' u radu - hodovima. Dobivanju jednostavnijih hodova pojednostavnjivanjem pripadnog parcijalnog uređaja je posvećeno četvrto poglavlje - "Kidanje veze". Nakon što promijenimo pripadni parcijalni uređaj hoda, moramo provjeriti da je struktura koju dobijemo na taj način opet hod s istim završnim stanjem. To je napravljeno u sljedećoj, petoj glavi - "Nova funkcija stanja". U šestoj glavi, "Sintaksa i semantika programa", se daju uvodne napomene o stablima izvoda kojima se predočuju programi te o načinu kojim će semantika pojedinih vrsta programa biti obrađivana uz pomoć 'montaža'. U sedmoj glavi, "Sekvencijalni deterministički programi", obrađene su programske konstrukcije sekvencijalnog determinističkog programskog jezika s petljom, zajedničkog za sve daljnje paralelne inačice. U njoj, kao i u sljedeće tri glave, prvo je dana sintaksa, zatim pridružena stabla izvoda i semantika odgovarajućeg programskog jezika. Potom slijede dokazi valjanosti pravila i na kraju su obrađene pridružene skice dokaza. U osmoj glavi, "Nezavisni paralelni programi", je opisan najjednostavniji oblik paralelizma u kojem se paralelne komponente izvode neovisno jedna o drugoj - jedna ne može utjecati na rad druge. U devetoj glavi, "Paralelni programi sa zajedničkim varijablama", su obrađeni paralelni programi u kojima paralelne komponente mogu međusobno komunicirati preko varijabli kojima one imaju pristup. Uvodi se atomarno područje, kojim se postiže ekskluzivno pravo raspolaganja varijablama za jednu paralelnu komponentu, što znači da ostale komponente tada ne mogu mijenjati vrijednost tih varijabli. U desetoj glavi "Paralelni programi sa sinkronizacijom, su obrađeni paralelni programi obogaćeni naredbom 'await' kojom se omogućuje sinkronizacija različitih paralelnih komponenti tako da jedne komponente bivaju zaustavljene (blokirane) u svom radu sve dok im druge komponente ne dozvole nastavak rada. Jedanaesta glava, "Zastoj", je posvećena nepoželjnoj situaciji u kojoj se dvije komponente međusobno blokiraju onemogućavajući na taj način normalan završetak rada. Pravila koja se odnose na totalnu korektnost su dana u posljednjem, dvanaestom poglavlju, "Totalna korektnost".

dinamičke algebre; paralelno programiranje; korektnost programa

nije evidentirano