Tartalom
Számos programozási feladat megoldása lehet szekvenciális, elosztott vagy párhuzamos program is. A programozási feladatok egy része azonban olyan jellegű, amelynek megoldásához térben elosztva elhelyezkedő adatok, erőforrások felhasználása szükséges [[???Lyn 02, ???Tan Ste 02]]. Ilyen feladatokat egyetlen számítógépen futó, szekvenciális program nem oldhat meg.
Párhuzamos feldolgozás esetén megkülönböztethetünk adatintenzív, illetve számításintenzív feladatosztályokat. Adatintenzív feladat például fizikai kísérletekből származó nagyszámú mérési adat kiértékelése, vagy diagnosztikai eljárásokkal előállított adatok elemzése. Általában számításigényes feladatok közé tartoznak a modellezési feladatok, pl. időjárás előrejelzés, szélcsatorna kísérletek szimulációja, stb. Ezekben az esetekben elvileg egyetlen számítógép is elvégezhetné az adatok feldolgozását, de párhuzamos algoritmusok segítségével az eredmény gyorsabban előállítható. Az is gyakori eset, hogy az eredmény kiszámítását adott időkorláton belül kell elvégezni és ehhez egyetlen processzor számítási kapacitása nem elegendő. Több processzor alkalmazásával nemcsak a számításhoz szükséges idő rövidíthető le, de az időkorlátra vonatkozó követelmény is teljesíthető [[???Ivá 03]].
Programozási feladatok specifikációjának és megoldásának alkalmas módszereit keressük párhuzamos és elosztott rendszerek esetén.
Elosztott és párhuzamos programok fejlesztése során a program helyességének bizonyítása azért is fontos lehet, mert teszteléssel nehezebben lehet a hibákat felfedezni mint szekvenciális programok esetén. Elosztott és párhuzamos programok ismételt futtatása gyakran vezet eltérő eredményre. Ennek az az oka, hogy a komponensek kölcsönhatása annak függvényében változik, hogy az adott futtatás során az egymástól független események közül melyik következik be előbb. Ha a program tesztelése érdekében nyomkövetési utasításokat helyezünk el, akkor ezzel megváltoztatjuk az egyes folyamatok között fennálló időzítési viszonyokat, így könnyen előfordulhat, hogy a tesztelés során a hiba nem jelentkezik.
Biztonságkritikus alkalmazások készítése során tehát csak bizonyítottan helyes komponenseket használhatunk fel és az elosztott program összetevőit csak az összetett program tulajdonságait garantáló programkonstrukciók segítségével szerkeszthetjük össze.
Feladatok megfogalmazása, programok kódolása mindig valamilyen nyelvi eszköz segítségével valósul meg. A feladat specifikációja egy jelsorozat, ahogy egy adott programozási nyelven írt program is betűk, szimbólumok, esetleg grafikus elemek sorozata. Ahhoz, hogy válaszolni tudjunk arra a kérdésre, hogy egy specifikáció valójában milyen feladatot ír le, hogy egy program futása során mi történhet, meg kell adnunk ezen jelsorozatok jelentését. Programok jelentésének pontos meghatározására matematikai modelleket használunk.
Párhuzamos és elosztott programok tervezésének egy matematikai modelljére teszünk javaslatot oly módon, hogy kiterjesztjük a nemdeterminisztikus szekvenciális programok relációs alapú szemantikai modelljét [[???Fót 83]] és a programozási feladatok megfogalmazására és megoldására korábban sikeresen alkalmazott módszereket [[???Dij 76, ???Fót Hor 91]] párhuzamos programokra is.
Célunk, hogy a modell eszközei segítségével a feladat specifikációját helyettesíteni tudjuk olyan feladatok specifikációival, amely feladatok megoldása esetén a rendelkezésre álló matematikai eszközökkel belátható az eredeti feladat megoldásának helyessége [[???Var 81, ???Fót Hor 91, ???Cha Mis 89]].
Arra törekszünk, hogy a megoldás előállításával párhuzamosan a megoldás helyességének bizonyítását is előállítsuk. Nem célunk az automatikus programszintézis [[???Lav 78]],[[???Eme Sri 88]]/4.1.3., és nem akarjuk kész algoritmusok helyességét utólag igazolni [[???Eme Sri 88]]/4.2. Ennek elsősorban az az oka, hogy párhuzamos programokat a legtöbb esetben részben vagy kizárólag azért írunk, hogy a megoldás hatékonyabb legyen a szekvenciális architektúrán elérhető megoldásnál. A hatékonyság lényeges szempont lehet természeténél fogva párhuzamos programmal megoldandó feladatok esetén is, pl. valós idejű alkalmazásoknál, folyamatszabályozó vagy on-line tanácsadó rendszerek esetén [[???Hor 88]]. Talán csak egyes szimulációs feladatok vagy prototípus szoftver fejlesztése során másodlagos a megoldás hatékonysága. Hatékony megoldás előállítására az automatikus programszintézis bonyolultabb feladatok esetén általában nem alkalmas. Az [[???Eme Sri 88]]-ban ismertetett eredmények meggyőzően mutatják azt is, hogy a szintetizáló algoritmusok általában nagyon rossz hatékonyságúak, a megoldás előállításához a specifikáció hosszával exponenciálisan arányos időre van szükség. Hasonló állítások igazak a programbizonyításra is. A programbizonyítási eljárás sikertelensége esetén nincs elegendő támpont a program javításához sem.
A UNITY [[???Cha Mis 89]] lineáris idejű temporális logikára támaszkodó operátorait újrafogalmazzuk a leggyengébb előfeltétel és más predikátumtranszformerek segítségével. Megvizsgáljuk a bevezetett specifikációs módszer kifejezőerejét és az általánosítási lehetőségeket.
A -. fejezetben megadjuk a relációs modell alapfogalmainak definícióit. A két legfontosabb bevezetett fogalom a feladat és az absztrakt program fogalma.
Az . fejezetben adjuk meg, hogy egy absztrakt program mikor old meg egy feladatot. Kimondunk néhány tételt is, amelyek igazolják, hogy a bevezetett megoldásfogalom megfelel elvárásainknak.
A . fejezetben több hasznos tételt bizonyítunk, amelyek segítségével a későbbiek során könnyebben igazolhatjuk feladatok és programok tulajdonságait.
A . fejezetben összetett problémák megoldása során alkalmazható eszközöket vezetünk be. A megoldást modulokból állítjuk össze. Az absztrakt programokat egyesítjük és szuperponáljuk, támaszkodunk az ún. nyitott specifikáció fogalmára [[???Cha Mis 89]]. Megvizsgáljuk programok szekvenciális ill. valós párhuzamos kompozíciójának lehetőségét.
A . fejezetben megvizsgáljuk a bevezetett modell tulajdonságait, kifejezőerejét.
A modell eszközkészletének ismertetése után programozási tételeket mondunk ki és összetett problémák megoldása során alkalmazható eszközöket vezetünk be.
A . fejezetben általánosan megfogalmazott programozási feladatokat oldunk meg. A kapott megoldásokat programozási tételeknek nevezzük, mert széles körben alkalmazhatóak konkrét feladatok megoldása során. Az egyik ilyen alapfeladat asszociatív művelet eredményének párhuzamos kiszámítása. A másik az elemenként feldolgozható, ill. a sorozatokon többszöros függvénykompozícióval definiált függvény értékének kiszámítása. Példát mutatunk csatornaváltozók használatára és adatcsatornás megoldási módszerekre is. Megvizsgáljuk, hogy a kapott megoldások milyen architektúrákon implementálhatók hatékonyan. Olyan megoldásokat dolgozunk ki, amelyek osztott és aszinkron osztott memóriás rendszerekre is könnyen leképezhetőek.
A -. fejezetben megvizsgáljuk, hogy a párhuzamos programok leírására alkotott modellek milyen lényeges tulajdonságokban térnek el egymástól. Megadjuk, hogy az általunk javasolt modell milyen jelenségek leírására alkalmas.
A . fejezetben ismertetjük azokat a matematikai eszközöket, amely a bevezetett modell mélyebb matematikai hátterét tisztázzák. Összefoglaljuk a leképezések fixpontjaira vonatkozó eredményeket és bevezetjük az olvasót a temporális logikák világába. A temporális logikákról szóló bekezdésben bevezetett fogalmakra és tételekre a II. részben általában csak egyes megjegyzésekben és lábjegyzetekben utaltunk, így a II. rész fejezeteinek megértéséhez ez a bekezdés nem feltétlenül szükséges.
A . fejezetben összefoglaljuk és értékeljük a leírt módszereket.
A függelékben megvizsgáljuk, hogy az absztrakt programokat hogyan kódoljuk C-PVM segítségével.
A könnyebb tájékozódást kereszthivatkozások, tárgymutató és jelölések jegyzéke, a legfontosabb fogalmak definíciói, stb. segíti. Az érdeklődő olvasó gyakorló feladatok megoldásásával ellenőrizheti tudását.
Egyes megjegyzéseket lábjegyzetben helyeztünk el. A lábjegyzetekben általában más modellek rokon fogalmaira utalunk röviden. Ezek a megjegyzések elsősorban azoknak az olvasóknak szólnak, akik ezekben a modellekben járatosak.