Osztott rendszer • Osztott rendszer informális definíciója • Egymástól elkülönülten létező program-komponensek egy halmaza. • A komponensek egymástól függetlenül dolgoznak saját erőforrásukkal. • A komponensek időről-időre egymásnak üzeneteket küldenek a közös feladat megoldása érdekében. • Osztott programrendszer végrehajtása • Párhuzamosan futó folyamatoknak egy halmaza. • Minden folyamat rendelkezik saját változókkal. • A különböző folyamatokhoz tartozó változók halmazai diszjunktak. • A folyamatok egymással üzenetek révén kommunikálnak.
Osztott rendszer folyamat1
folyamat2
folyamatn
lokális
lokális
lokális
változók
változók
változók
csatorna
üzenetek
• Üzenet formában történő kommunikáció • Szinkron kommunikáció • Aszinkron kommunikáció • Kommunikáció csatornán keresztül • A kommunikációs csatorna nem irányított • A kommunikációs csatornának nincsen típusa
Kommunikációs csatorna • Input utasítás • Szintaxis: C?x • C∈ csat, csat csatornák halmaza • x egyszerű változó. • Jelentés • Azt fejezi ki, hogy az utasítást kiadó program x változója egy értéket fogadjon a C csatornán keresztül. Ha ez teljesül, akkor x változó felveszi az értéket. • Output utasítás • Szintaxis: C!e • C∈ csat, ahol csat a csatornák halmaza • e: a C!e utasítást kiadó programnak lokális változóival képezett aritmetikai kifejezés, • Jelentés • Azt fejezi ki, hogy az utasítást kiadó program az e kifejezés értékét elküldje a C csatornán keresztül.
Kommunikációs csatorna • Őrfeltétellel ellátott csatornautasítás • Szintaxis • b;C?x; illetve b;C!e, ahol b logikai kifejezés. • Jelentés • Az I/O csatorna utasítás kiegészül egy tesztelési függvénnyel, amely folyamatosan vizsgálja, hogy lehetséges-e a kommunikáció a C csatornán keresztül. • Amíg ez nem következik be, a b kifejezés kiértékelése "false” értéket eredményez. • Ha bekövetkezik, "true" értéket eredményez. • Jelölések • A "true";C?e illetve "true"; C!e rövid jelölése: C?e C!e • var(S):
összes változó + csatorna nevek
• channel(S):
csatornanevek S-ben
Kommunikációs csatorna • b1;C?u és b2;C!e utasítások egymáshoz illeszthetőek • azonos csatornára hivatkoznak • e kifejezés és u változó típusa azonos • b1 és b2 őrfeltételek kiértékelése igaz értéket szolgáltat • Az α1:C?u, α2: C!e illesztés eredménye:
u ← e;
• Szinkron kommunikáció jelentése C csatornán keresztül a b1;C?u , b2;C!e egymáshoz illeszthető utasítás pár esetén • Várakozás • Mindkét kérés teljesítésének várnia kell, amíg a másik nem jelenik meg. • Egyidejűség • Mindkét kérés végrehajtása egyszerre történik meg. • Értékadás • A kommunikáció eredménye az, hogy az u ← e értékadás megtörténik.
Osztott rendszer • Definíciók • Az osztott rendszer S1 és S2 folyamatai diszjunktak, ha change(S1) ∩ var(S2) = var(S1) ∩ change(S2) = { } • Az Si és Sj (i ≠ j) folyamatokat a C csatorna összeköti, ha C ∈ channel(Si) ∩ channel(Sj) • A S1, ... , Sn folyamatok pontról pontra összekötöttek, ha ∀ 1 ≤ i < j < k ≤ n : channel(Si) ∩ channel(Sj) ∩ channel(Sk) ≠ { } • Osztott program • parbegin S1 || ... || Sn parend; • S1, ..., Sn folyamatok páronként diszjunktak • Bármely 1≤ i < j < k ≤ n esetén az Si, Sj, Sk folyamatok pontról pontra összekötöttek • S végrehajtása befejeződik, ha mindegyik Sj befejeződik.
Komponens elvű programfejlesztés • C. B. Jones • A pre/post specifikációkat minden sc komponens (shared component) esetén egészítsük ki „megbízhatósági / garancia” (rely / garantee) előírással is: { p, r } sc { g, q } • Előfeltétel: • Utófeltétel: • Megbízhatósági feltétel: • Garancia feltétel:
p: Σ →Σ q: Σ × Σ → Σ r: Σ × Σ → Σ g: Σ × Σ → Σ
• Probléma • A programfejlesztés alávetése a szekvencializációs szabályoknak!
Komponens elvű programfejlesztés • Modellalkotás • 1990-es évek végén: Warmer J., Kleppe A.: • The Object Constraint Language – Precise Modelling with UML • Lényege: Probléma megoldásának modelljei + korlátozások • „Forgatókönyv” (scenario) készítésekor rögzítjük a komponensekre vonatkozó megállapodásokat: contracts, scenario, prototype. • Probléma megoldás számítógépes hálózaton keresztül • A problémát ágensek oldják meg úgy, hogy összehangolt akciókkal kívánják a közös célt elérni.
Komponens elvű programfejlesztés • Ágens • Felhasználó, program, rendszer, stb. • Akció • Tevékenységek végrehajtása. • Például: Gomb megnyomása, üzenet, algoritmus végrehajtása, stb. • Cél • A rendszer kívánt állapotának elérése egy jövőbeli időpontban. • Összehangolás • Kontraktus alapján (komponensek közötti szerződés) • Kontraktus, megállapodás • Dokumentum, specifikáció, program szövege • Probléma • Adott a kontraktus, és az ágensek egy halmaza. • Kérdés: Egy adott célt képesek-e elérni az ágensek az adott kontraktussal?
Kontraktus felhasználó és gép között • Batch feldolgozás • Választás a számítógépé (belső nem determinisztikus választás) • Dijkstra: abort = {false}user • Ha abort-ot hajtott végre a felhasználó, jelzi, hogy a felhasználó megsértette a megállapodást. Ugyanis a számítógép felhatalmazást kapott a további rész akár hibás végrehajtásra is. • Interaktív program • A felhasználónak van választási lehetősége a végrehajtásnál. (Alternatívák közül választhat) • A számítógép belső döntéseket hozó mechanizmus szerint dolgozik. • Példa • S = S1; S2 • a ∈ felhasználó • b ∈ számítógép • S1 = (x : = x + 1 a x: = x + 2 ); • S2 = (x : = x - 1 b x: = x - 2 );
Kontraktus a felhasználó és a gép között • S = S1; S2 • a ∈ felhasználó • b ∈ számítógép • S1 = (x : = x + 1 • S2 = (x : = x - 1
A felhasználó választása attól függ, hogy mit akar elérni: x ≤ 0 vagy x ≥ 0 x: = x + 2 ); b x: = x - 2 );
a
a x:= x+1
x:= x+2 b
x:= x - 1
x=0
b
x:= x - 2
x = -1
x:= x-1
x=1
x:= x-2
x=0
Ágens rendszerek • Legyen Ω az ágensek egy összessége, A az ágensek egy halmaza és a, b, c ∈ A. Ekkor az ágens rendszer = (A, S, Ict, Q). •A:
a rendszer ágenseinek véges halmaza
•S:
S0; do b1→ S1
a
...
a
bn → Sn
a
SE ; exit; od;
• S0, S1,..., Sn; nem determinisztikus programok. • S0 : •
rendszer indulása előtt elvégzendő feladatok végrehajtására szolgáló program (inicializálás).
• Ict :
kontraktust rögzítő invariáns
•a∈A:
ágens a megfelelő komponens kiválasztásáért felelős
•Q:
az ágens rendszer végrehajtása során elérendő célállítás
Példa:
Kecske, farkas és káposzta átszállítása a folyón
• Kontraktus • A farkas a kecskével csak akkor lehet együtt, ha a hajós is ott van:
fa = ke ⇒ ha = fa
• A kecske a káposztával csak akkor lehet együtt, ha a hajós is ott van:
ke = ká ⇒ ha = ke
• A kontraktus invariánsa ( lct ): (fa = ke ⇒ ha = fa) ∧ (ke = ká ⇒ ha = ke) ∧ (∀n∈{ fa, ke, ká, ha })(n∈bool) • Kiindulási állapot:
ha = F ∧ fa = F ∧ ke = F ∧ ká = F
• Q Cél állapot:
ha = T ∧ fa = T ∧ ke = T ∧ ká = T
• Ágens(ek): a hajós
Példa:
Kecske, farkas és káposzta átszállítása a folyón • átkelés = ha := F; fa := F; ke := F; ká := F; do ha = fa → (ha, fa) := (¬ha, ¬fa); a ha = ke → (ha, ke) := (¬ha, ¬ke); a ha = ká → (ha, ká) := (¬ha, ¬ká); a ha = ¬ha; a skip; exit od; • a: hajós;
Példa:
Raktár szimuláció
• Egy raktárban háromféle áru raktározható • Áruféleségek: • Raktár kapacitása:
A, B, C N
• Kikötések • B és C áru vegyesen tárolható. • A és C áru vegyesen tárolható. • A és B áru nem tárolható vegyesen. • Nem determinisztikus módon érkeznek/távoznak az árúk. • Készítsük el a helyes működésének szimulációját. • Adott áruból raktáron lévő mennyiség • nA = cont(A,ent) - count(A,ex) • nB = cont(B,ent) - count(B,ex) • nC = cont(C,ent) - count(C,ex)
Példa:
Raktár szimuláció
• Kontraktus • B és C áru vegyesen tárolható, ha nincs a raktárban A áru N ≥ nB + nC ≥ 0 ∧ nA = 0 • A és C áru vegyesen tárolható, ha nincs a raktárban B áru N ≥ nA + nC ≥ 0 ∧ nB = 0 • Komponensek közötti megállapodást rögzítő Ict(N, nA, nB, nC) invariáns ((N ≥ n ≥ 0 ∧ nA = 0) ∨ (N ≥ n ≥ 0 ∧ nB = 0)) ∧ (n = nA + nB + nC )
Példa:
Raktár szimuláció
• raktár = (nA ← 0; nB ← 0; nC ← 0; n ← N; raktároz; • raktároz = do beszállít a elszállít a skip; exit od; • a, b, c ∈ A' , ágenshalmaz beszállít = if b b
(N > n ≥ 0 ∧ nB = 0) → (〈binsert(R, A); (nA, n) ← ( nA + 1, n + 1) 〉 ) (N > n ≥ 0 ∧ nA = 0) → (〈binsert(R, B); (nB, n) ← ( nB + 1, n + 1) 〉 ) (N > n ≥ 0) → (〈binsert(R, C); (nC, n) ← ( nC + 1, n + 1) 〉 )
fi; elszállít = if c c
fi;
(nA > 0) → ( 〈 bdelete(R, A); (nA, n) ← ( nA - 1, n - 1) 〉 ) (nB > 0) → ( 〈 bdelete(R, B); (nB, n) ← ( nB - 1, n - 1) 〉 ) (nC > 0) → ( 〈 bdelete(R, C); (nC, n) ← ( nC - 1, n - 1) 〉 )
Fair tulajdonság • Példa nem fair programra S1 ≡ jel:= "false"; do ~ jel → következő sor nyomtatása // nyomtatás ~ jel → jel:= "true" // kilépés od; • A nem determinisztikus program szemantikája nem garantálja, hogy a második sor megkapja a vezérlést. • Gyenge fair követelmény A do…od ciklusban minden olyan őrfeltételes utasítás, amely valamely időponttól folyamatosan készen áll a végrehajtásra, annak végtelen sokszor aktiválódni kell. • Az első komponens ilyen feltétel esetén nem aktiválódhatott volna kizárólagosan, ha a második komponens kész a végrehajtásra.
Fair tulajdonság • Példa erősen fair programra S2 ≡ jel:= "false"; lap := "false"; i := 0; do ~ jel → következő sor nyomtatása; i := (i+1) mod 30; lap := (i=0) ~ jel ∧ lap → jel:= "true" od; • Most is az első tud aktiválódni először, de 30 nyomtatás után a második komponens indulásának feltétele folyamatosan teljesül, így a második ág végrehajtásra kerül. • A második ág végrehajtása után egyik komponens belépési feltétele sem teljesül, ezért az iteráció befejeződik. • Ezt az esetet nevezik erős fair (strong fairness) tulajdonságnak.
Fair tulajdonság • Egyszerű, egyszintű nem determinisztikus program • S0; do α1→S1 ... αn→Sn od; • S0, S1, ..., Sn determinisztikus komponensek. • Fair nem determinisztikus szemantika definíciója S egyszintű, nem determinisztikus program esetén σ ∈ Σ kezdőállapot mellett Mfair[S](σ) = { τ | < S, σ > →* < E, τ > } ∪ { ⊥ | S divergálhat σ kezdő állapotból egy fair kiszámítás esetén } ∪ { fail | S hibás eredményre juthat σ kezdő állapotból }
Mtot[S](σ σ) és Mfair[S](σ σ) közötti különbség