online kép - Fájl  tubefájl feltöltés file feltöltés - adja hozzá a fájlokat onlinefedezze fel a legújabb online dokumentumokKapcsolat
  
 

Letöltheto dokumentumok, programok, törvények, tervezetek, javaslatok, egyéb hasznos információk, receptek - Fájl kiterjesztések - fajltube.com

 

Online dokumentumok - kep
  

Folyamatabra-programok és -sémak

számítógépes



Fájl küldése e-mail



egyéb tételek

 
Szamítógép halózatok előnyei
Az MS-DOS operaciós rendszer
Logikai algebra, logikai műveletek
Grafikai alapfogalmak
A szamítógéppel létrehozott kép megjelenítő eszközei
Kapcsolat az ügyfél szolgalattal
Input perifériak
IKT ALAPISMERETEK
Az operaciós rendszerek installalasa
A DOS unit fontosabb beépített konstansai, függvényei, eljarasai; hasznalata
 
 

Folyamatábra-programok és -sémák



Egy S folyamatábra-séma SS ábécéje az alábbi szimbólumhalmaz valamely véges részhalmaza:

Konstansok:

fin (i³1, n³0): n-argumentumú függvénykonstansok;



fi -t elemkonstansnak nevezzük, és ai-vel jelöljük.

pin (i³1, n³0): n-argumentumú relációkonstansok;

pi : ítéletkonstans.

2. Elemváltozók:

xi: input változók,

yi: programváltozók,

zi: output változók.

A SS-beli x input változók, y programváltozók és z outputváltozók száma legyen rendre a,b és c, ahol a,b,c³


Egy SS fölötti t term a SS elemváltozóiból, elemkonstansaiból és függvényváltozóiból a szokásos kompozícióval áll elő.


Egy SS fölötti A atomi formula vagy egy pi ítéletkonstans, vagy egy pin(t ,...,tn) alakú kifejezés, ahol n³1 és t ,...,tn SS fölötti termek.


A SS fölötti utasítások a következő alakúak lehetnek:

1. kezdőutasítás:

2. értékadás:

3. vizsgálat:

4. végutasítás:

5. végtelen ciklus utasítás:

Egy SS fölötti folyamatábra-séma olyan véges, SS fölötti utasításokból konstruált folyamatábra, amelyben egy kezdőutasítás van, és minden értékadás és vizsgálat rajta van egy, a kezdőutasításból valamely végutasításhoz vagy végtelen ciklus utasításhoz vezető úton.


Egy S folyamatábra-séma I interpretációi a következőkből állnak:

1. Egy D nemüres halmazból, amelyet az interpretáció alaphalmazának nevezünk;

2. A SS-beli konstansokra vonatkozó hozzárendelésekből:

a) minden SS-beli fin függvénykonstanshoz hozzárendelünk egy Dn-t D-be leképező totális függvényt (ha n=0, az fi elemkonstanshoz D valamely rögzített elemét rendeljük);

b) minden SS-beli pin relációkonstanshoz hozzárendelünk egy Dn-t -ba képező totális relációt (ha n=0, a pi ítéletkonstanshoz az igaz vagy a hamis igazságértéket rendeljük).


A P=<S, I> párt, ahol S folyamatábra-séma, I pedig az S egy interpretációja, folyamatábra-programnak nevezzük. Az S input változóinak x vektorához megadva valamely x Da input értéket, a program végrehajtható.


<P, x> kiszámítása úgy történik, hogy az x programváltozók a x értékeket kapják, a kezdőutasításnál az y programváltozók a t(x) értékeket kapják. A kiszámítás véget ér, mihelyt egy végutasításhoz vagy végtelenciklus-utasításhoz jutunk: az első esetben a végutasítás ere 727g69h dményeképpen az output változók értéke z=z Dc lesz, akkor azt mondjuk, hogy a program értéke (P(x)=val <P, x>) definiált, és P(x z; minden más esetben P(x) definiálatlan. A program tehát egy Da-t Dc-be leképező parciális függvényt reprezentál.


Egy P program

a) megáll, ha P(x) definiált minden x Da-ra;

b) divergál, ha P(x) definiálatlan minden x Da-ra.


Egy S séma

a) megáll, ha <S,I> megáll S minden I interpretációja esetén;

b) divergál, ha <S,I> divergál S minden I interpretációja esetén.


Az S és S' sémát kompatibilisnek nevezzük, ha az input változók x vektora és az output változók z vektora megegyezik. Az <S,I> és <S',I'> programot kompatibilisnek nevezzük, ha S és S' kompatibilis, továbbá az I és I' interpretációk alaphalmaza megegyezik.


A P és P' programok ekvivalensek, ha kompatibilis, és P(x ºP x). Az S és S' kompatibilis sémák ekvivalensek, ha S és S' minden I interpretációja esetén <S,I> és <S',I> ekvivalensek.


A P és P' programok izomorfak, ha kompatibilisek, és minden x Da esetén P(x) és P'(x) kiszámítási sorozata megegyezik.Az S és S' kompatibilis sémák izomorfak, ha S és S' minden közös I interpretációja esetén <S,I> és <S',I> izomorf.


Egy S séma Herbrand-univerzuma (HS) a következő halmaz:

1. ha xi input változója S-nek, és ai az S-ben szereplő elemkonstans, akkor "xi" és "ai" elemei HS-nek;

2. ha fin az S-ben előforduló n-argumentumú függvénykonstans, és "t ",...,"tn" HS-beli elemek, akkor "fin(t ,...,tn)" is eleme HS-nek.

Vagyis: HS


Egy S séma Herbrand-interpretációja (I ) az a HS alaphalmazú interpretáció, amelyre teljesülnek a következő feltételek:

1. S minden ai elemkonstansához az "ai" HS-beli elem legyen rendelve;

2. S minden fin függvénykonstansához az a HS fölötti n-argumentumú függvény, amely tetszőleges "t ",...,"tn" HS-beli jelsorozatokat az "f(t ,...,tn)" HS-beli jelsorozatra képez le.

(Az S relációkonstansaira nincs semmiféle megkötés.)


Luckham-Park-Paterson tétel:

1. Tetszőleges S séma akkor és csak akkor áll meg/divergál, ha val <S,I "x"> definiált/definiálatlan S minden I Herbrand-interpretációja esetén.

2. Tetszőleges S és S' kompatibilis séma akkor és csak akkor ekvivalens egymással, ha val<S,I "x">ºval<S',I "x"> S és S' minden I Herbrand-interpretációja esetén.

3. Tetszőleges S és S' kompatibilis séma akkor és csak akkor izomorf egymással, ha S és S' minden I Herbrand-interpretációja esetén <S,I "x"> és <S',I "x"> kiszámítási sorozata megegyezik.


Egy S sémát szabadnak nevezünk, ha folyamatábráján minden, a kezdőutasításból kiinduló véges út kezdőszelete valamely kiszámításnak.


1. A szabad sémák megállási problémája megoldható: egy szabad séma pontosan akkor nem áll meg, ha szerepel benne végtelenciklus-utasítás, vagy folyamatábrája tartalmaz ciklust.)

2. A szabad sémák divergálási problémája megoldható: egy szabad séma pontosan akkor nem divergál, ha tartalmaz végutasítást.

3. Az, hogy egy séma szabad, parciálisan sem dönthető el.

4. Nem ismeretes, hogy a szabad sémák ekvivalenciaproblémája megoldható-e.

5. A szabad sémák izomorfizmus-problémája megoldható.


Egy ST véges ábécé fölötti T faséma olyan (esetleg végtelen), ST fölötti utasításokból álló folyamatábra, amelynek gráfja fa, azaz:

1. pontosan egy kezdőutasítást tartalmaz;

2. minden egyes utasítása pontosan egy útból érhető el a kezdőutasításból (nincs benne csomópont);

3. levelei végutasítások vagy végtelenciklus-utasítások.


A véges fasémák megállási problémája, divergálási problémája, valamint ekvivalencia- és izomorfia-problémája megoldható.


Minden folyamatábra-sémához megadható vele ekvivalens szabad faséma.

Minden megálló folyamatábra-sémához megadható vele ekvivalens véges szabad faséma.


Input feltételnek nevezzük azt a Dx feletti j(x) relációt, amely leírja Dx inputként használható elemeit.

A Y(x,z) output feltétel egy Dx×Dz feletti reláció; leírja azt az input és output változók közötti összefüggést, amelyet az input és output változók értékeinek a program befejeződésekor ki kell elégíteniük.


P parciálisan helyes j-re és Y-re nézve, ha minden olyan x inputra, amelyre j x) teljesül és P(x) definiált, Y x,P(x)) teljesül.

P totálisan helyes j-re és Y-re nézve, ha minden olyan x inputra, amelyre j x) teljesül, P(x) definiált, és Y x,P(x)) teljesül.

P megáll j-re nézve, ha minden olyan x inputra, amelyre j x) teljesül, P(x) definiált.


Ha egy program totálisan helyes, akkor parciálisan is helyes.


A parciális helyességből és a megállásból következik a totális helyesség.



Parciális helyesség bizonyítása


Floyd-féle induktív állítások módszere:

1. vágási pontokat helyezünk el a programban

a) a kezdőutasításból induló élen (kezdőpont);

b) a végutasításokhoz vezető éleken (végpontok);



c) minden ciklusban elhelyezünk legalább egy vágási pontot (belső pontok).

Csak azokat a szakaszokat vesszük figyelembe, amelyek vágási ponttól vágási pontig terjednek, és nincs rajtuk közbenső vágási pont (közvetlen út). Legyen a egy i-ből j-be vezető út.

Jelentse Ra(x,y) azt a feltételt, amely mellett a vezérlés végighalad az a úton, az ra(x,y) függvény pedig azt a transzformációt, amelyet az a út által leírt programrész okoz az y változókon. Ezek előállítására a visszafelé helyettesítés módszere szolgál.

2. A program minden i vágási pontjához hozzárendelünk egy pi(x,y) induktív állítást, amely jellemzi a változók közötti összefüggést az i pontban. A kezdőponthoz az input feltételt, míg a végpontokhoz az output feltételt rendeljük.

3. Minden a úthoz megszerkesztjük a megfelelő helyességi feltételt:

"x,y[pi(x,y) Ù Ra(x,y) pj(x, ra(x,y))].

Ha j végpont, akkor a helyességi feltétel

"x,y[pi(x,y) Ù Ra(x,y) Y(x, ra(x,z))]

lesz, míg ha i kezdőpont, akkor

"x j(x) Ù Ra(x) pj(x, ra(x))].

Ez a helyességi feltétel egyszerűen azt állítja, hogy ha pi igaz x és y olyan értékeire, amelyek mellett az a útban leírt programrészlet végrehajtódik, akkor pj igaz lesz a programszakasz végrehajtásával kapott x, y értékekre.


Ha P-re, j-re és Y-re elvégezzük az 1-3. lépéseket és minden helyességi feltétel igaz, akkor P parciálisan helyes j-re és Y-re.

Mivel minden közvetlen útra bebizonyítottuk a helyességi feltételt, ezért a kezdőpontból a végpontba vezető út sorozat esetén a végponthoz rendelt Y helyességi feltétel is igaz lesz.


Manna-féle részcél-módszer:

1. Vágási pontok elhelyezése a Floyd-módszerrel megegyező módon.

2. Részcélok vágási pontokhoz rendelése:

a) a kezdőponthoz: j(x)®Y(x,z);

b) belső pontokhoz: pi(x,y) qi(x,y,z);

c) végponthoz: T.

3. Helyességi feltételek meghatározása a közvetlen utakra:

a) belső pontból belső pontba:

"x,y,z [pj(x, ra(x,y)) qj(x, ra(x,y),z) Ù Ra(x,y) (pi(x, ra(x,y)) qi(x, y,z))];

b) kezdőpontból belső pontba:

"x,z [pj(x, ra(x,y)) qj(x, ra(x,y),z) Ù Ra(x,y) j(x)®Y(x,z))];

c) belső pontból végpontba:

"x,y [ Ra(x,y) (pi(x, ra(x,y)) qi(x, y,z))];

d) kezdőpontból végpontba:

"x [ Ra(x,y) Ù j(x)®Y(x,z)].


Ha P-re, j-re és Y-re elvégezzük az 1-3. lépéseket és minden helyességi feltétel igaz, akkor P parciálisan helyes j-re és Y-re.



Megállás bizonyítása


Egy (W,<) parciálisan rendezett halmaz egy W nemüres halmazból és egy < bináris relációból áll, mely W elemein van értelmezve és tranzitív, aszimmetrikus és irreflexív.

Egy (W,<) parciálisan rendezett halm,azt megalapozottnak nevezünk, ha nincs benne végtelen csökkenő sorozat.


Megalapozott halmazok módszere:

1. Vágási pontokkal vágjuk fel a programban szereplő hurkokat, és minden i vágási ponthoz rendeljünk hozzá egy qi(x,y) állítást, amely

a) minden olyan a, a kezdőpontból valamely j vágási pontba vezető közvetlen útra fennáll:

"x j(x)ÙRa(x) qj(x, ra(x))]

b) minden olyan a, a i vágási pontból a j vágási pontba vezető közvetlen útra fennáll:

"x,y[qi(x,y)ÙRa(x,y) qj(x, ra(x,y))]

2. Válasszunk egy (W, <) megalapozott halmazt és minden i vágási ponthoz rendeljünk egy ui(x,y) parciális függvényt, amely Dx×Dy-ból W-be képez és

"x,y[qi(x,y) ui(x,y) W]

3. Minden olyan a, a i vágási pontból a j vágási pontba vezető közvetlen útra, amely része egy programhuroknak írjuk fel a megállási feltételt:

"x,y


Egy adott P folyamatábra-programra és j(x) inpput feltételre végezzük el az 1-3. lépéseket. Ha az összes megállási feltétel igaz, akkor P megáll j mellett.


2. While-programok



Egy while-program véges sok, egymástól pontosvesszővel elválasztott utasításból áll: B ; B ;...; Bn, ahol

B

START

y f(x),

Bn

z h(x)

HALT

És minden Bi (0<i<n) utasítás a következő utasítástípusok valamelyike:

1. értékadó utasítás:

y g(x)

2. feltételes utasítás:

if t(x,y) then B else B'

vagy

if t(x,y) do B,

ahol B és B' tetszőleges utasítás.

3. ciklusutasítás:

while t(x,y) do B,

ahol B tetszőleges utasítás.

4. összetett utasítás:

begin B';...;B(k) end,

ahol B(i) tetszőleges utasítás.



Parciális helyesség (Hoare módszer)


Induktív kifejezés

B ,

ahol p, q relációk és B egy programszegmens. Az induktív állítás azt jelenti, hogy ha p(x, y) fennáll az x, y értékekre B végrehajtása előtt, és B végrehajtása befejeződik, akkor q(x, y) fenn fog állni a B végrehajtása után kapott x, y értékekre.


A P program helyességének bizonyítása a

P

induktív kifejezés levezetéséből áll, amelyhez levezetési szabályok állnak rendelkezésre a következő alakban:

ahol a és a azok a feltételek, amelyek mellett a szabály alkalmazható, b a levezetett induktív kifejezés. A feltételek vagy már korábban levezetett induktív kifejezések vagy logikai kifejezések lehetnek, ezeket mint lemmákat külön kell bizonyítani.


Levezetési szabályok:

1. értékadás-axióma:

y g(x, y)

2. feltételes szabályok:

3. while-szabály:

4. kompozíciós szabály:

5. következmény-szabályok:

Adott egy P while-program, j(x) input feltétel Y(x, z) output feltétel. Ha az előbbiekben leírt szabályok alkalmazásával sikerül levezetni a

P

kifejezést, akkor P parciálisan helyes j-re és Y-re nézve.





Totális helyesség (Dijkstra-féle leggyengébb előfeltétel-kalkulus)


wp(B, q): az a leggyengébb előfeltétel, amely mellett B megáll és a megállás után q teljesül.


B totálisan helyes p-re és q-ra nézve, ha p wp(B, q).


Alaptulajdonságok:

a) wp(B, F) = F;

b) wp(B, pÙq) = wp(B, p) Ù wp(B, q);

c) wp(B, p q) = wp(B, p) wp(B, q);

d) ha p q, akkor wp(B, p) wp(B, q).


Utasítások leggyengébb előfeltételei:

a) wp(skip, q) = q;

b) wp(B ;B , q) = wp(B , wp(B , q));

c) wp(y f(x, y), q(x, y)) = q(x, f(x, y));

d) wp(if t then B else B , q) = wp(B , q)Ùt wp(B , q)ÙØt = t wp(B , q) Ù Øt wp(B , q);

e) wp(while t do B, q) = i³0: pi, ahol pi annak a leggyengébb előfeltétele, hogy B-t pontosan i-szer végrehajtva t már nem teljesül, de q teljesül.

pi ØtÙq

pi+1 = tÙwp(B, pi

wdec(B, u) annak a leggyengébb előfeltétele, hogy B csökkenti u-t (u Z


Ha pÙt wp(B , q) és pÙØt wp(B , q), akkor p wp(if t then B else B , q).


Ha pÙt wp(B, q) és u³0 és wdec(B, u), akkor p wp(while t do B, pÙØt).


Ha pÙt wp(B, p) és p wp(while t do B, T), akkor p wp(while t do B, pÙØt).


A totális helyesség bizonyításához a

wp(P, Y

kifejezést kell levezetni a fenti szabályok segítségével.


3. Rekurzív programok és sémák

Egy S rekurzív séma SS ábécéje az alábbi szimbólumhalmaz valamely véges részhalmaza:

1. konstansok:

fin függvénykonstansok

pin relációkonstansok

2. változók:

x ,..., xa, y ,...,yb, z elemváltozók

Fi b-változós függvényváltozók.


A SS feletti term és atomi formula ugyanaz, mint a folyamatábra-sémák esetén.

konstans term: olyan term, amelyben Fi nem szerepel.

Csak olyan atomi formulák megengedettek, amelyek konstans termekből állnak.


Feltételes term

- minden term feltételes term

- w (a definiálatlanság szimbóluma) nem term, de feltételes term

- ha A egy atomi formula, t t feltételes termek, akkor az

if A then t else t

szöveg feltételes term.


S rekurzív séma

z t (x, F), ahol

F (y) ¬ t (x, y, F),


Fn(y) ¬ tn(x, y, F).

ahol t tn SS feletti feltételes termek.


Interpretáció

- alaphalmaz (D) megadása;

- minden fin függvénykonstanshoz hozzárendelünk egy j: Dn D totális függvényt;

- minden pin relációkonstanshoz hozzárendelünk egy p: Dn totális függvényt.


Kiszámítási sorozat a an elemei fin-ből, Fi-ből és D elemeiből álló termek, melyek tovább már nem egyszerűsíthetők.


Egyszerűsítő műveletek

- fin kiszámítása, ha értéke D-beli;

- az if A then t else t feltételes term esetén A kiszámítása után a kifejezés helyettesíthető t -gyel vagy t -vel.


a t ai, F) az összes lehetséges egyszerűsítés után.

ai+1-et ai-ből úgy kapjuk, hogy vesszük a legelső, legbaloldalabbi Fi előfordulást, elvégezzük a programban előírt helyettesítést (az yi-k helyére a megfelelő argumentumok, az xi-k helyére pedig a xi-k kerülnek. Ezek csak D-beli elemek lehetnek!), majd az így kapott termet egyszerűsítjük.


Ha (ai) véges, és az utolsó eleme D-beli, akkor P(x) definiált, és értéke ez az utolsó elem; minden más esetben P(x) nem definiált.


Minden folyamatábra-sémához megadható vele ekvivalens rekurzív séma.

(Csak 1 outputos folyamatábra-sémára)

Vágási pontokat helyezünk el, és minden belső ponthoz hozzárendelünk egy függvényváltozó-értéket, melynek értéke a leendő output érték, argumentumai pedig a programváltozók tartalma.


A következő rekurzív sémához nem adható meg vele ekvivalens folyamatábra-séma:

z = F(a), ahol

F(y) if p(y) then f(y) else h(F(g (y)), F(g (y))).


4. Nemszekvenciális (párhuzamos) programok



Általában több erőforrás (proceszor, memória, perifériák, háttértárak stb.) áll rendelkezésre, mint amennyire egy programnak szüksége van. Ezért lehetőség van arra, hogy egyszerre több program is jelen legyen. Ezek a programok osztoznak az erőforrásokon; váltakozva jutnak hozzá a központi egységhez, szinte párhuzamosan hajtódnak végre. Az ilyen programok rendszere egyetlen virtuális párhuzamos rendszert képez. Ez a rendszer igen laza rendszer, az erőforrások megosztását az operációs rendszer végzi; az egyes programok úgy készíthetők el, mintha egyedül lennének jelen a gépen.

Az olyan rendszerek, amelyek komponensei között sokkal szorosabb a kapcsolat (pl. folyamatvezérlési programrendszer) az erőforrások megosztását feltételezve jöttek létre, egymással üzenetet váltanak, egymás szolgáltatásait igénybe veszik, szolgáltatásokra várnak. Ha egy ilyen programrendszer egyprocesszoros gépen fut, akkor a párhuzamosság virtuális, míg többprocesszoros gépen a rendszer bizonyos részei ténylegesen párhuzamosan hajtódnak végre.


A párhuzamos program egy rendszer, amely az erőforrások ls a szekvenciális programok egy egysége. A végrehajtás alatt lévő programot folyamatnak nevezzük. A párhuzamos renszer állapotát a folyamatok és az erőforrások viszonya határozza meg. A folyamatok ezt az állapotot utasításokon keresztül megváltoztatják.

A folyamatnak azon részei, amelyek nem tartalmaznak rendszerállapotot megváltoztató utasításokat, egymással párhuzamosan végrehajthatók.


Az erőforrások a használat szempontjából lehetnek:

1. kizárólagos használatú;

2. megosztható.

A megosztható erőforrásokat egyidejűleg több folyamat is használhatja. A kizárólagos használatú erőforrások belső állapotát a folyamatok megváltoztatják, ezért egyszerre egynél több folyamat nem használhatja. Az erőforrások használatának ajánlott rendje:

1. az erőforrás igénylése;

2. az erőforrás lekötése;

3. az erőforrás felszabadítása.


A folyamatoknak két állapota lehet:

1. aktív állapot: minden olyan erőforrást lekötve tart, amelyre igényét bejelentette;

2. blokkolt állapot: erőforrás felszabadulására vár.



Alapproblémák


Holtpont-mentesség: A holtpont olyan állapot, amikor a rendszert alkotó folyamatok közül kettő vagy több folyamat várakozik a végtelenségig egy olyan eseményre, amelyik soha nem következik be. Holtpont esetén a rendszer működésképtelenné válik, csak külső (pl. operátori) beavatkozással indítható tovább. Az olyan rendszert, amelyben holtpont-állapot nem következhet be, holtpont-mentesnek nevezzük.

Példa: Adott két folyamat és két erőforrás. Az első folyamat az 1., a második folyamat a 2. erőforrást tartja lekötve. Ha mindkét folyamat bejelenti igényét a másik által lekötve tartott erőforrásra mielőtt a sajátját elengedné, előáll a holtpont-állapot.


Kölcsönös kizárás: Vannak olyan erőforrások, amelyeket egyidejűleg egynél több folyamat nem használhat. A rendszernek olyannak kell lennie, hogy a folyamatok kölcsönösen kizárják egymást az ilyen erőforrások használatából. A folyamatoknak vannak kritikus szakaszaik. A kölcsönös kizárás azt jelenti, hogy legfeljebb egy folyamat tartózkodhat kritikus szakaszban.

Primitív utasítás: olyan utasítás, amelynél a kölcsönös kizárást a hardver végzi. Jele: [ ].




Szinkronizáció: A rendszer folyamatai általában közös feladatot oldanak meg, és ennek érdekében együttműködnek. Ez együttműködés során egymásnak jelzéseket, üzeneteket küldenek. Rendszerint vannak olyan szakaszok, amelyekbe a folyamatok csak akkor léphetnek be, ha erre egy másik folyamattól engedélyt kapnak. Ily módon a rendszert alkotó folyamatoknak szinkronban kell működniük.



Dijkstra-féle szemaforok


A Dijkstra-féle szemafor (s) a folyamatok egy egész értékű közös változója, amelyet a folyamatok várakozó sorához (például egy adott tipusú erőforrásra várakozók sorához) kölcsönösen és egyértelműen hozzárendelünk. Az s szemafor kezdeti értéke a folyamatok indulásakor pozitív érték, rendszerint 1.

A folyamatok egymásnak jelzéseket küldhetnek a rendszer állapotát megváltozztató utasítások kiadása előtt és után a szinkronizációs utasításokkal:

1. P(s) beléptető művelet:

[ s s-1;

ha s<0, akkor a folyamat belép a várakozók sorába]

2. V(s) kiléptető művelet:

[ s s+1;

ha s³0, akkor egy folyamat kilép a várakozók sorából]

A kiléptető műveletben nem rögzített az a stratégia, amellyel a várakozók sorából a folyamat kiválasztható. A sorrendet a beütemező stratégiák rögzítik.


A kölcsönös kizárás megvalósításához minden közös erőforráshoz felveszünk egy szemafort, s=1 kezdőértékkel, majd minden folyamatot a következő elv szerint valósítunk meg:

...; P(s); kritikus szakasz; V(s); ...

A szemafor felhasználható szinkronizálásra is.


Példa: termelő-fogyasztó rendszer. Adott egy n-elemű puffer, egy termelő és egy fogyasztó folyamat. A termelő nem termelhet többet a puffer méreténél, a fogyasztó nem fogyaszthat gyorsabban a termelésnél.

Megvalósítása:

s szemafor: a pufferben lévő elemek száma (s=0 kezdőérték);

r szemafor: a pufferben lévő üres helyek száma (r=n kezdőérték).

termelés:

...termelés; P(r); az adat elhelyezése; V(s);...

fogyasztás:

P(s); elem kiolvasása és törlése; V(r); fogyasztás...


5. Dijkstra-féle nemdeterminisztikus programok



A nemdeterminisztikus programok a while-programok bővítései a következő két utasítással:

1. szelekciós utasítás:

if t B tn Bn fi

ahol ti őrfeltétel, Bi tetszőleges programszegmens. Kiválasztunk egy igaz értékű őrfeltételt és végrehajtjuk a hozzá tartozó programszegmenst. A kiválasztás véletlenszerű, általunk ismeretlen. Ha nincs igaz értékű őrfeltétel, a program abortál.

2. repetatív utasítás:

do t B tn Bn od

Kiválasztunk egy igaz értékű őrfeltételt és végrehajtjuk a hozzá tartozó programszegmenst. Ezt addig ismételjük, amíg az összes őrfeltétel hamissá nem válik.



Leggyengébb előfeltétel-kalkulus nemdeterminisztikus programokra


wp(B, q) annak a leggyengébb előfeltétele, hogy B végrehajtását elkezdve a végrehajtás biztosan befejeződik és q biztosan teljesül.


Alaptulajdonságok

- wp(B, F) = F;

- ha q q , akkor wp(B, q wp(B, q

- wp(B, q Ùq ) = wp(B, q Ùwp(B, q

- wp(B, q q wp(B, q wp(B, q


Utasítások wp értékei:

- wp(skip, q) = q;

- wp(y f(x, y), q) = q(x, f(x, y));

- wp(B ;B , q) = wp(B , wp(B , q));

- wp(if t B tn Bn fi, q) =

- wp(do t B tn Bn od, q) = i³0: pi

ahol pi annak a leggyengébb előfeltétele, hogy a végrehajtás legfeljebb i lépésen belül befejeződik és q biztosan teljesül.

p Øtt Ù q;

pi+1 = pi wp(IF, pi

ahol IF ugyanaz mint a do...od, csak if...fi-vel.


Ha pÙt wp(B , q) és pÙØt wp(B , q), akkor p wp(if t then B else B , q).


Ha "i: pÙti wp(B, q), akkor pÙtt wp(IF, q).


Ha pÙt wp(B, p) és wdec(B, u) és u³0, akkor p wp(while t do B, pÙØt), ahol wdec(B, u) annak a leggyengébb előfeltétele, hogy B biztosan csökkenti u-t legalább 1-gyel.


6. Owicki-Gries-féle párhuzamos programok



A while-programot két utasítással bővítjük:

1. párhuzamosan végrehajtható utasítások:

cobegin B ||...|| Bn coend,

ahol Bi párhuzamos programszegmens. Az n ág szimultán hajtódik végre, a végrehajtás sebessége nemdeterminisztikus.

2. várakoztató utasítás:

await t then B,

ahol t feltétel, B szekvenciális programszegmens. Addig várakozik, amíg t igazzá nem válik, majd végrehajtja B-t.


Egy szekvenciális programszegmens végrehajtását oszthatatlannak nevezzük, ha biztosítani tudjuk a végrehajtásának más ágak végrehajtásától való függetlenségét. Kifejezések kiértékelése és az értékadó utasítások oszthatatlanok. Ezért kifejezésben vagy értékadó utasításban olyan változó, amelyre más ágakban értékadó utasítás vonatkozik, egyféle, és legfeljebb egyszer szerepelhet.



Levezetési szabályok


1. A megvárakoztatás következtetési szabálya:

A párhuzamosság következtetési szabálya:

Legyen S egy utasítás, pre(S) egy előfeltétel, B egy igaz induktív kifejezés a levezetésével. Azt mondjuk, hogy S nem interferál pre(S) mellett a B levezetésével, ha

S

S a B minden olyan B' részutasítására, amely nem része await utasításnak, és p' pre(B') p


A B ,..., Bn induktív kifejezéseket interferencia mentesnek nevezzük, ha minden i-re Bi minden await vagy await-en kívüli S értékadó utasítása nem interferál a Bj j¹i induktív kifejezések levezetésével a pre(S) előfeltétel mellett.


A B programszegmensben szereplő X változó-halmazt segédváltozó-halmaznak nevezzük, ha X elemei B-ben csak olyan kifejezésekben szerepelnek, amelyek X elemeire vonatkozó értékadások jobboldalai.


Legyen X egy segédváltozó-halmaz B-ben; p, q elő- és utófeltételek, amelyek nem tartalmaznak X-beli változókat. Ekkor:

ahol B'-t B-ből úgy kapjuk, hogy az X elemeit tartalmazó utasításokat töröljük.

Szemaforok implementálása


Egyszerű szemafor:

P(s): await s>0 then s:=s-1; belépés

V(s): await T then s:=s+1; kilépés.


Dijkstra-szemafor:

w[i]: folyamatonként egy-egy tömbelem, amely a folyamatok várakozását fejezi ki. Kezdetben minden i-re w[i]=F.

P(s): await T then begin

s:=s-1;

if s>0 then w[ez a folyamat]:=T

end

await Øw[ez a folyamat] then skip;

V(s): await T then begin

s:=s-1;

if s<0 then begin

egy w[i]=T kiválasztása;

w[i]:=F

end

end




Találat: 1078