Termelő-fogyasztó modell • A probléma absztrakt megfogalmazása • Adott egy N ≥ 1 kapacitású közös tároló. • Adott a folyamatok két csoportja, amelyek a tárolót használják. • n ≥ 1 termelő folyamat, • m ≥ 1 fogyasztó folyamat. • A termelő a tároló használatakor egy-egy terméket helyez el a tárolóban. • A fogyasztó a tároló használatakor egy-egy terméket vesz ki a tárolóból.
Termelő-fogyasztó modell • Termelő és fogyasztó közötti sorrendiség • A fogyasztó ugyan abban a sorrendben veszi ki a termékeket a tárolóból, amilyen sorrendben a termelő azt lehelyezte. • Termelő folyamatok közötti kölcsönös kizárás • A termelő folyamatok közül egyszerre csak egy folyamat használhatja a tárolót. • Fogyasztó folyamatok közötti kölcsönös kizárás • A fogyasztó folyamatok közül egyszerre szintén csak egy folyamat • használhatja a tárolót. • Termelők és a fogyasztók közötti termék esetében példányonkénti kölcsönös kizárás • Ugyanazt a termék példányt a termelő nem helyezheti el, a fogyasztó pedig nem veheti ki egyszerre.
Termelő-fogyasztó modell • A megállapodás formális megfogalmazása • Tároló: q ∈ sor, length(q) = N, N ≥ 1 • Termelő műveletei: x←a[i]; 〈q ← add(q,x)〉; i = 0, ..., M - 1 • Fogyasztó műveletei: 〈(q,y) ← (rem(q), read(q))〉; b[j]←y; j = 0, ..., M - 1 • A sorrendiségi követelmények teljesülnek! • i ← 0; j ← 0; • { ( i, j ∈ integer) ∧ q ∈ queue ∧ 0 ≤ length(q) ≤ N ∧ ( a[0, M -1], b[0, M -1] ∈ vector) ∧ M ≥ 1 ∧ N ≥ 1 } • parbegin producer || consumer parend;
Termelő-fogyasztó modell Producer while i < M do x ← a[i]; wait length(q) < N ta; 〈q ← add(q,x)〉; i ← i + 1; od;
Consumer while j < M do wait length(q) > 0 ta; 〈(y,q) ← (read(q), rem(q))〉; b[j] ← y; j ← j + 1; od;
A kölcsönös kizárások teljesülnek.
Termelő-fogyasztó modell • Megvalósítás • q buffer[0…N-1] ciklikus elhelyezéssel mod(N) • Behelyezésnél az index: in • Kiemelésnél az index:
out
• Előfeltétel: • Inicializálás:
{M≥1∧N≥1} i ← 0; j ← 0; in ← 0; out ← 0;
• S program:
parbegin producer || consumer parend;
• {(∀k, 0 ≤ k < M)(a[k] = b[k])}; wait length(q) < N ta: wait in - out < N ta; q ← add(q,x): wait length(q) > 0 ta: (y,q) ← (read(q), rem(q));
buffer[in mod N] ← x; in ← in + 1; wait in - out > 0 ta; y ← buffer[out mod N]; out ← out + 1;
Termelő-fogyasztó modell producer
consumer
while i < M do
while j < M do
x ← a[i]; wait in - out < N ta; 〈 buffer[in mod N] ← x; in ← in + 1〉; i ← i + 1; od;
wait in - out > 0 ta; 〈 y ← buffer[out mod N]; out ← out + 1〉 b[j] ← y; j ← j + 1; od;
Közös erőforrás-használat problémái • Informális leírás • Adott egy S : parbegin S1 || ... || Sn parend párhuzamos rendszer és egy e erőforrás. Az e erőforrás felhasználási módjai • A folyamatok egy csoportjának tagjai csak kizárólagosan használhatják az erőforrást. • A folyamatok egy másik csoportjának tagjai egyidejűleg akárhányan is használhatják az erőforrást. • A két csoport tagjai vegyesen nem használhatják az erőforrást. • Probléma • Erőforrás monopolizálása, • Kiéheztetés.
Kiéheztetés (starvation), monopolizálás • Adott egy S : parbegin S1 || ... || Sn parend párhuzamos rendszer. • Informális definíció: Kiéheztetés • a párhuzamos program végrehajtása nem fejeződik be, mert a folyamatok egy csoportja monopolizálja a párhuzamos rendszer közös erőforrását. • Informális definíció: Erőforrás monopolizálása • a párhuzamosan futó folyamatok között mindig van legalább egy olyan folyamat, amely lekötve tartja az erőforrást, • miközben a velük párhuzamos folyamatok nem üres csoportjának tagjai folyamatosan várakoznak az erőforrásra. erőforrást használók;
erőforrásra várakozók;
lefutottak.
Kiéheztetés-mentesség • Adott egy erőforrás, n ≥ 3 folyamat, amelyek az erőforrást használják, és egy párhuzamos rendszer p(σ) előfeltétele. • Kiéheztetés-mentes vezérlés • A folyamatok legalább két diszjunkt csoportot alkotnak • Csoportok között teljesül a kölcsönös kizárás • Egy adott időpontban különböző csoporthoz tartozó folyamatok az erőforrást nem használhatják. • Csoporton belüli közös használat • Létezik legalább egy olyan csoport, amelyben a folyamatok egy adott időpontban többen is használhatják az erőforrást. • Kiéheztetés-mentesség • Ne fordulhasson elő az, hogy az egyik csoportbeli folyamatok végtelen hosszú ideig várnak az erőforrásra, a másik csoport folyamatai közül mindig van legalább egy olyan, amely lekötve tartja azt.
Kiéheztetés-mentes szinkronizáció • A rendszer formális megfogalmazása végtelenített rendszer esetén • S: inicializálás; parbegin S1 || ... || Sn parend; n ≥ 3. Si Folyamatok szerkezete while B do NKi: EIi: EHi: EFi: od;
Nem kritikus szakasz; Erőforrás igénylése; Erőforrás használata; Erőforrás felszabadítása;
ahol ∀ i, k, 1 ≤ i, k ≤ n ∧ i ≠ k -ra: [ változó (NKi) ∪ változó (EHi) ] ∩ [ változó(EIk) ∪ változó(EFk) ] = { } • Feltevés: NKi és EHi nem tartalmaz megvárakoztató utasítást.
Kiéheztetés-mentesség feltételei • Formális megfogalmazás • Legyen adott • a párhuzamos rendszer p(σ) előfeltétellel • egy, a folyamatok által közösen használt erőforrás. • A folyamatok két csoportot alkotnak. • Legyenek az A csoport folyamatainak azonosítói: 1, 2, ..., n1 n1 ≥ 2. • Legyenek a B csoport azonosítói: n1+1, n1+2, ... , n; n ≥ 3. • A csoportok közötti kölcsönös kizárás • Nem létezik olyan < parbegin R1 || . . . || Rn parend , σ> konfiguráció, amelyre valamilyen i ∈ { 1, ... , n1 } és k ∈ { n1+1, ... , n } esetén Ri ≡ at(EHi in Si) és Rk≡ at(EHk in Sk).
Kiéheztetés- és holtpont-mentesség • Csoporton belüli közös használat • Adott p(σ) mellett létezhet olyan < parbegin R1 || . . . || Rn parend , σ> konfiguráció, amelyre Ri ≡ at(EHi in Si) és Rk ≡ at(EHk in Sk), ha i, k ∈ {1, ... , n1 } • Végtelen igénylés • Adott p(σ) mellett nem létezik olyan < parbegin R11 || . . . || Rn1 parend , σ1> → < parbegin R12 || . . . || Rn2 parend , σ2> → ... végtelen végrehajtási sorozat, ahol minden < parbegin R1i || . . . || Rni parend , σi> konfiguráció esetén (~∃i∈{1, ..., n1} ∧ ~∃k∈{n1+1,..., n})( Rji≡at(EHj in Sj) ∧ Rk ≡ at(EIk in Sk)) • Holtpont-mentesség • Adott p(σ) mellett a párhuzamos program végrehajtása nem végződik holtpont állapotban: ∆ ∉ M(S)[{p}]
Holtpont-mentesség feltételei • Végtelen igénylés • Adott p(σ) mellett nem létezik olyan < parbegin R11 || . . . || Rn1 parend , σ1 > → < parbegin R12 || . . . || Rn2 parend , σ2 > → ... végtelen végrehajtási sorozat, ahol minden < parbegin R1i || . . . || Rni parend , σi> konfiguráció esetén ~∃ i ∈ { 1, ... , n1 } ∧ ~∃ k ∈ { n1+1, ... , n} : Ri ≡ at(EHi in Si) és Rk ≡ at(EIk in Sk) • Holtpont-mentesség • Adott p(σ) mellett a párhuzamos program végrehajtása nem végződik holtpont állapotban: ∆ ∉ M(S)[{p}].
Holtpont-mentesség feltételei • S: inicializálás; parbegin S1 || ... || Sn parend; n ≥ 3. Si Folyamatok szerkezete while B do NKi: Nem kritikus szakasz; EIi: Erőforrás igénylése; EHi: Erőforrás használata; EFi: Erőforrás felszabadítása; od; ahol ∀ i, k, 1 ≤ i, k ≤ n ∧ i ≠ k -re: [változó(NKi) ∪ változó(EHi)] ∩ [változó(EIk) ∪ változó(EFk)] = {} • Feltevés: NKi és EHi nem tartalmaz megvárakoztató utasítást.
Példa • Feladat • Készítsük el az adatbázis egy absztrakt modelljét a következő specifikáció alapján, majd végezzük el a modell tulajdonságainak elemzését a kiéheztetés-mentesség szempontjából. • Legyen n > 0 felújító és m > 1 lekérdező folyamat. • A felújító folyamatok egymással, valamint a lekérdező folyamatokkal is kölcsönös kizárásban vannak az adatbázis használatakor. • A lekérdező folyamatok egyszerre többen használhatják az adatbázist. • Megoldás • A lekérdező folyamatok számolják, hogy hányan használják az adatbázist egyidejűleg. • Számláló: rcnt, kezdőértéke: 0, (számláláshoz kölcsönös kizárás kell) • Szemafor: sr, kezdőértéke: 1 • Kölcsönös kizárás szemaforja: w • w ←1; rcnt ←0; sr ←1; parbegin writer1|| ... || writern || reader1 || ... || readerm parend;
Példa w ← 1; rcnt ← 0; sr ← 1; parbegin writer1|| ... || writern || reader1 || ... || readerm parend; writeri while "true" do Információ gyűjtés; P(w); Adatbázis felújítás; V(w); od;
readerk while "true" do P(sr); rcnt←rcnt+1; if rcnt = 1 then P(w) fi; V(sr); Adatbázis lekérdezés; P(sr); rcnt ← rcnt - 1; if rcnt = 0 then V(w) fi; V(sr); Válasz kiértékelése; od;
Példa • Követelmények • A reader és a writer folyamatnak is legyen esélye hozzáférni az adatbázishoz. • A writer folyamatok ne monopolizálhassák az adatbázist. • A reader folyamatok ne monopolizálhassák az adatbázist. • Megoldás • A writer folyamatok továbbra is egy kapun keresztül léphetnek be az erőforráshoz, ahova akadály nélkül eljuthatnak, de belépéskor lezárják a külső kaput a reader folyamatok előtt. • A reader két kapun keresztül léphet be az erőforráshoz. A külső kaput a writer nyitja ki a reader előtt a felújítás befejeztekor, amikor megkezdi az erőforrás elengedését. • A belső kapu közös, ezért a writer és a reader egyforma eséllyel léphet be az erőforráshoz. • Szemafor: who ∈ { w, r }, kezdőértéke: w
• Ha felújító folyamat használni akarja az adatbázist, akkor újabb lekérdező folyamat már ne férhessen az adatbázishoz. • Megoldás • Szemafor: who ∈ { w, r }, kezdőértéke: w w ← 1; sr ← 1; rcnt ← 0; r ←1; who ← w; parbegin writer1 || ... || writern || reader1 || ... || readerm parend; while "true" do Információ gyűjtés; who ← w; P(w); Adatbázis felújítás; await "true" then V(w) who ← r ta; od;
while "true" do wait who = r tw; P(sr); rcnt ← rcnt + 1; if rcnt = 1 then P(w) fi; V(sr); Adatbázis lekérdezés; P(sr); rcnt ← rcnt - 1; if rcnt = 0 then V(w) fi; V(sr); Válasz kiértékelése; od;
