Folyamatabra-programok és -sémak

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

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

Konstansok:

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

f_i -t elemkonstansnak nevezzük, és a_i-vel jelöljük.

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

p_i : ítéletkonstans.

2. Elemváltozók:

x_i: input változók,

y_i: programváltozók,

z_i: output változók.

A S_S-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 S_S fölötti t term a S_S elemváltozóiból, elemkonstansaiból és függvényváltozóiból a szokásos kompozícióval áll elő.

Egy S_S fölötti A atomi formula vagy egy p_i ítéletkonstans, vagy egy p_iⁿ(t ,...,t_n) alakú kifejezés, ahol n³1 és t ,...,t_n S_S fölötti termek.

A S_S 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 S_S fölötti folyamatábra-séma olyan véges, S_S 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 S_S-beli konstansokra vonatkozó hozzárendelésekből:

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

b) minden S_S-beli p_iⁿ relációkonstanshoz hozzárendelünk egy Dⁿ-t -ba képező totális relációt (ha n=0, a p_i í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 D^a 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 D^c 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 D^a-t D^c-be leképező parciális függvényt reprezentál.

Egy P program

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

b) divergál, ha P(x) definiálatlan minden x D^a-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 D^a 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 (H_S) a következő halmaz:

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

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

Vagyis: H_S

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

1. S minden a_i elemkonstansához az "a_i" H_S-beli elem legyen rendelve;

2. S minden f_iⁿ függvénykonstansához az a H_S fölötti n-argumentumú függvény, amely tetszőleges "t ",...,"t_n" H_S-beli jelsorozatokat az "f(t ,...,t_n)" H_S-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 S_T véges ábécé fölötti T faséma olyan (esetleg végtelen), S_T 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 D_x feletti j(x) relációt, amely leírja D_x inputként használható elemeit.

A Y(x,z) output feltétel egy D_x×D_z 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 R_a(x,y) azt a feltételt, amely mellett a vezérlés végighalad az a úton, az r_a(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 p_i(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[p_i(x,y) Ù R_a(x,y) p_j(x, r_a(x,y))].

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

"x,y[p_i(x,y) Ù R_a(x,y) Y(x, r_a(x,z))]

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

"x j(x) Ù R_a(x) p_j(x, r_a(x))].

Ez a helyességi feltétel egyszerűen azt állítja, hogy ha p_i igaz x és y olyan értékeire, amelyek mellett az a útban leírt programrészlet végrehajtódik, akkor p_j 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: p_i(x,y) q_i(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 [p_j(x, r_a(x,y)) q_j(x, r_a(x,y),z) Ù R_a(x,y) (p_i(x, r_a(x,y)) q_i(x, y,z))];

b) kezdőpontból belső pontba:

"x,z [p_j(x, r_a(x,y)) q_j(x, r_a(x,y),z) Ù R_a(x,y) j(x)®Y(x,z))];

c) belső pontból végpontba:

"x,y [ R_a(x,y) (p_i(x, r_a(x,y)) q_i(x, y,z))];

d) kezdőpontból végpontba:

"x [ R_a(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 q_i(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)ÙR_a(x) q_j(x, r_a(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[q_i(x,y)ÙR_a(x,y) q_j(x, r_a(x,y))]

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

"x,y[q_i(x,y) u_i(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 ;...; B_n, ahol

B

START

y f(x),

B_n

z h(x)

HALT

És minden B_i (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⁽ⁱ⁾ 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: p_i, ahol p_i 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.

p_i ØtÙq

p_i+1 = tÙwp(B, p_i

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

j®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 S_S ábécéje az alábbi szimbólumhalmaz valamely véges részhalmaza:

1. konstansok:

f_iⁿ függvénykonstansok

p_iⁿ relációkonstansok

2. változók:

x ,..., x_a, y ,...,y_b, z elemváltozók

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

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

konstans term: olyan term, amelyben F_i 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),

F_n(y) ¬ t_n(x, y, F).

ahol t t_n S_S feletti feltételes termek.

Interpretáció

- alaphalmaz (D) megadása;

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

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

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

Egyszerűsítő műveletek

- f_iⁿ 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 a_i, F) az összes lehetséges egyszerűsítés után.

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

Ha (a_i) 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 t_n B_n fi

ahol t_i őrfeltétel, B_i 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 t_n B_n 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 t_n B_n fi, q) =

- wp(do t B t_n B_n od, q) = i³0: p_i

ahol p_i 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;

p_i+1 = p_i wp(IF, p_i

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Ùt_i 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 ||...|| B_n coend,

ahol B_i 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 ,..., B_n induktív kifejezéseket interferencia mentesnek nevezzük, ha minden i-re B_i minden await vagy await-en kívüli S értékadó utasítása nem interferál a B_j 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