21.2.Állapotátmenetfák

21.2.Állapotátmenetfák
Előző	21. fejezet - Párhuzamos absztrakt program	Következő

Az absztrakt programot egy olyan bináris relációként definiáljuk, amelyik egy kezdeti feltételes értékadás hatásrelációja, illetve véges sok feltételes értékadás hatásrelációjának diszjunkt uniója által generált fák ekvivalenciaosztályait rendeli az állapottér egyes pontjaihoz (. def.).

21.10. Definíció (Címkézett állapotátmenetfa).
A címkézett állapotátmenetfa egy rendezett ötös, ahol a fa gyökere, a csúcsok halmaza, az élek halmaza, a gráf csúcsaihoz állapotokat rendelő címkefüggvény, az élekhez természetes számokat rendelő címkefüggvény, és pontosan egy út vezet -ből minden csúcsba.

21.11. Definíció (Izomorf állapotátmenetfák).
Izomorfnak mondjuk a és a fát, ha van olyan bijekció, amelyre

21.1. Tétel.
(Az izomorfia reláció ekvivalenciareláció) Az . definícióban megfogalmazott izomorfia reláció ekvivalenciareláció az felett generált fák halmazán.

Biz.: A reláció reﬂexív, mert minden fához létezik adott tulajdonságú leképezés, az identitás. A reláció szimmetrikus, mert a bijekció inverze rendelkezik az adott tulajdonságokkal, ha a bijekció rendelkezett vele. Végül a reláció tranzitív, mert két adott tulajdonságú bijekció kompozíciója is rendelkezik a megkövetelt tulajdonságokkal.

21.12. Definíció (Állapotátmenetfák ekvivalenciaosztályai).
jelölje az felett generált fák ekvivalenciaosztályainak halmazát.

21.13. Definíció (Generált állapotátmenetfa).
Legyenek az relációk mindenütt értelmezve az állapottér felett, azaz . . Tetszőlges pontra az relációpár által az ponthoz generált fának nevezzük a irányított fát, ha
,
,
.

Reprezentáljuk az reláció által az ponthoz generált gráfok ekvivalenciaosztályait annak egy elemével.

Legyen egy feltételes értékadás és véges sok feltételes értékadás nem üres halmazának rendezett párja. J={1,..,m}, a relációk diszjunkt uniója.

21.14. Definíció (Helyesen címkézett állapotátmenetfa).
Az relációpár által generált fa címkézése helyes, ha minden -ből induló él címkéje és minden -vel címkézett élre amely -val címkézett csúcsból -vel címkézett csúcsba mutat teljesül, hogy .

21.1. ábra -

21.1. ábra. Címkézett állapotátmenetfa

21.2. Lemma.
(Helyes címkézés és ekvivalencia) Ha egy állapotátmenetfa címkézése helyes, akkor a vele ekvivalens állapotátmenetfák címkézése is helyes. Biz.: a . def. következménye.

21.15. Definíció (Absztrakt program).
Absztrakt programnak nevezzük az relációt, ha az állapottér pontjaihoz a relációpár által generált azon állapotátmenetfák ekvivalenciaosztályait rendeli, amelyek címkézése helyes. Az által definiált programot röviden -sel jelöljük, és azt mondjuk, hogy .

21.3. Megjegyzés (Műveleti szemantika).
A . definíció megadja a párhuzamos absztrakt program szemantikai jelentését. Ez a szemantika műveleti jellegű, a programnak megfelelő gráf valójában a műveleti szemantika címkézett állapotátmenet gráfjával azonosítható (. fejezet). Megjegyezzük, hogy ez a szemantika olyan programok között is különbséget tesz, amelyek egyaránt megoldásai (. def.) ugyanannak a feladatnak, de más-más végrehajtási utakat definiálnak.

21.16. Definíció (Végrehajtási út).
A ekvivalenciaosztály reprezentánsának bármelyik útját végrehajtási útnak nevezzük.

21.17. Definíció (Elérhető állapotok halmaza).
Az halmaz elemeinek végrehajtási útjain elhelyezkedő csúcsok címkéinek halmazát jelöljük -val. az állapotból elérhető állapotok halmazaEzen állapotok az absztrakt program állapotátmenetfájában érhetőek el, de valamely ütemezési kikötés mellett a konkrét program által már nem feltétlenül elérhetőek..

21.18. Definíció (Absztrakt program változói).
Jelöljük -sel az program utasításainak baloldalán álló változók (. def.) halmazát, azaz . Jelöljük a jobboldalon álló változók (. def.) halmazát -sel. .

Feltételezzük, ha több processzor hajtja végre a konkrét programot, akkor ez hatékonysági szempontoktól eltekintve hatásában megegyezik azzal, mintha egyetlen processzor válogatott volna valamilyen nemdeterminisztikus sorrendben az utasításhalmaz elemei közül. Megengedjük ugyan, hogy két vagy több processzor időben átfedve hajtsa végre ugyanazon utasítás különböző elemi lépéseit vagy különböző utasításokat, de az így kapott eredménynek meg kell egyeznie valamelyik eredménnyel azok közül, amelyet valamelyik végrehajtási út mentén egyetlen processzor állított volna elő. Feltételezzük tehát, hogy az absztrakt programot oly módon implementáljuk, hogy elemi építőköveire, a szimultán feltételes értékadásokra párhuzamos végrehajtás esetén teljesül a sorbarendezhetőség [[???Lam Lyn 90]] követelménye. Egy-egy sorrendet egy-egy végrehajtási út ír le.

21.4. Megjegyzés.
Az . definíció alapján megállapíthatjuk, hogy a modellben szimultán feltételes értékadások valós aszinkron párhuzamos végrehajtását nem tudjuk kifejezniValós párhuzamosság esetén összetett feladatok megoldását általában nem lehet modulokból előállítani (. fejezet). A modell programfogalma összefésüléses szemantikán (. fejezet) alapszik. A szinkron párhuzamos végrehajtás leírására a szimultán értékadás alkalmas.

Az utasítások halmazát sok esetben halmazműveletek segítségével állítjuk majd elő a megoldás logikai struktúrájának megfelelő modulokból. Egy-egy modul leírhatja például egy-egy objektum viselkedését [[???Cha Mis 89, ???Sin 91]]. A modulok uniójaként vagy szuperpozíciójaként kapott program [[???Cha Mis 89]] utasításait hatékonysági szempontok figyelembevételével képezhetjük le logikai vagy fizikai processzorokra. A modul tehát programtervezési, a folyamat pedig implementációs fogalom.

21.2.1.Utasítások kiterjesztése, szuperpozíciója

Definiáljuk az állapottér egy altere felett definiált utasítás kiterjesztettjét oly módon, hogy abban a kiegészítő altér változói ne álljanak egyetlen utasítás baloldalán és jobboldalán sem és a kiterjesztett utasítás -re vett vetülete éppen legyen [[???Fót 83, ???Fót 88]].

21.19. Definíció (Utasítás kiterjesztése).
Legyen altere az állapottérnek, a altér kiegészítő altere az -ra. Az utasítás kiterjesztése -ra: .

21.3. Lemma.
Legyen az tér az állapottér altere. Legyen az altér felett definiált utasítás kiterjesztése az utasítás. Ekkor: .

Biz.: Az utasítás kiterjesztésének definíciója szerint , így . Felhasználva, hogy egy utasítás hatásrelációjának (. def.) kiszámítása és a vetítés kommutatív, a lemma állításához jutunk.

Gyakran alkalmazzuk egyes utasítások definíciójánál azt a módszert, hogy egy meglévő és ismert hatásrelációjú feltételes értékadást módosítunk.

21.20. Definíció (Értékadás kiegészítése feltétellel).
.

21.4. Lemma.
= . Biz.: A . def. közvetlen következménye.

21.21. Definíció (Feltételes értékadások szuperpozíciója).
Legyen és azonos állapottéren adott két feltételes értékadás és legyen . Ekkor .

21.5. Megjegyzés.
Tegyük fel, hogy nem szerepel az értékadás baloldalán (. def.). Ekkor az előző definíció értelmében speciális esetként definiálhatjuk az feltételes értékadás és a egyszerű értékadás szuperpozícióját: .

21.5. Lemma.
(Szuperpozíció hatásrelációja) Legyen és azonos állapottéren adott két feltételes értékadás és legyen . Ekkor .

Biz.: Jelöljük -val azt a relációt, amelyik minden ponthoz önmagát rendeli ( ). Legyen . , így . , tehát , így .

21.2.2.Program kiterjesztése

Definiáljuk az program -ra való kiterjesztettjét utasításonként.

21.22. Definíció (Program kiterjesztése).
Legyen az és tér az állapottér két egymást kiegészítő altere. Legyen program az altér, az tér felett definiálva. Az programot az program -ra való kiterjesztésének nevezzük, ha minden utasítása kölcsönösen egyértelműen megfeleltethető az program egy utasítása kiterjesztésének.

21.6. Megjegyzés.
A . lemma és az absztrakt program definíciója alapján könnyen belátható, hogy és .