21.3.Pártatlan ütemezés fogalma

A megoldás definíciója kimondja majd, hogy a feladatban megfogalmazott feltételeknek csak azokra a végrehajtási utakra kell teljesülni, amelyekre teljesül a feltétlenül pártatlan ütemezés axiómája.

21.23. Definíció (Feltétlenül pártatlan ütemezés).

Egy végrehajtási útról azt mondjuk, hogy teljesül rá a feltétlenül pártatlan ütemezés axiómája, ha az út mentén a feltételes értékadások halmazából minden utasítás végtelen sokszor kerül kiválasztásra, azaz a címkefüggvény az út mentén a indexhalmaz minden elemét végtelen sokszor rendeli az élekhez Megkövetelhetünk azonban kevesebbet is, pl.: hogy a feladatban megfogalmazott feltételeknek csak azokra a végrehajtási utakra kell teljesülni, amelyekre teljesül az utófeltételekre vonatkozóan pártatlan ütemezés axiómája..

Ha a konkrét, adott architektúrára leképezett programra teljesül, hogy feltétlenül pártatlan ütemezés mellett kerül végrehajtásra, akkor a többi utat valóban nem kell figyelembe venni a megoldás helyessége szempontjából. Ebben az esetben a program működése nemdeterminisztikus módon kiválasztott transzformációk iterációjával írható le, ahol a nemdeterminisztikusság véges de nem korlátos hasonló értelemben, ahogy relációk nem korlátos lezártjáról beszéltünk [[???Fót 83, ???Hor 90]]. Több utasítás közül ugyanaz az utasítás véges, de nem korlátos sokszor nem kerül kiválasztásra közvetlenül egymás után.

Utasítások pártatlan kiválasztására sokféle feltételt lehet megfogalmazni [[???Fra 86, ???And 91]], ezek közül az egyik leggyengébb a pártatlan ütemezés axiómája. Így feltétlenül pártatlan ütemezés mellett jól működő programok az általában szigorúbb ütemezési feltételek esetén is megoldják a feladatot.

Az ún. őrfeltételek [[???Dij 75, ???Hoa 78, ???And 91]] hasonlítanak a feltételes értékadásokban szereplő feltételekhez. A feltételes értékadások hatásrelációi azonban akkor is definiáltak, ha az adott állapotra a feltétel nem teljesül. Ezért a generált fában mindig megjelenik az értékadás hatásrelációjának megfelelő él. A hamis őrfeltételű műveletek azonban nem generálnak éleket.

21.24. Definíció (Utófeltételekre pártatlan ütemezés).

Nem teljesül egy végrehajtási útra az utófeltételekre vonatkozóan pártatlangyengén pártatlan ütemezés axiómája, ha - egy adott pontjától kezdődően minden pontjában kiválasztható olyan utasítás, amely az adott pontnak megfelelő állapotból egy adott logikai függvény igazsághalmazába visz és - sohasem kerül ilyen utasítás kiválasztásra.

A feltételes értékadások halmazaként definiált absztrakt program nem tartalmaz őrfeltételeket. A továbbiakban feltételezzük, hogy az implementált program végrehajtása feltétlenül pártatlan.

21.7. Megjegyzés.

Belátható, hogy feltétlenül pártatlan ütemezéssel nem pártatlan ütemezés is modellezhető [[???Cha Mis 89]].