Atomi műveletek őrfeltételének meghatározása. Konkrét program elkészítése. 1. Példa: Számítógép labor használata

2012.12.27.

Funkcionalitás és szinkronizáció 

SZINKRONIZÁCIÓS KÓD SZINTÉZISE

A konkurens programokkal megoldandó feladatok jelentős részénél a szinkronizációs problémák megoldása (és az ehhez szükséges szinkronizációs kód előállítása) elválasztható a funkcionális probléma megoldásától.

Gregorics Tibor

Szinkronizációs kód szintézisének lépései Feladat

Elemzés Követelmények leírása

Modell

Statikus modell Dinamikus modell

Absztrakt program

Konkrét program

Gregorics Tibor

Kijelöljük a feladat megoldásának folyamatait, és az azok által közösen használt erőforrásokat, a folyamatok egymáshoz viszonyított szerepét (osztálydiagram).  Meghatározzuk a folyamatok és az erőforrások lehetséges állapotait (állapotdiagram). ◦ A folyamatok állapotai aktív állapotok, tehát tevékenységekre (köztük az erőforrásokra irányuló tevékenységekre) utalnak. ◦ Az erőforrások állapotai a folyamatok tevékenységei közötti szinkronizációs feltételeiket tükrözik. ◦ Ha a folyamatoknak különböző prioritásaik is lehetnek, akkor a magasabb prioritásúak számára speciális állapotokat vezetünk be a korrekt ütemezés érdekében. 

Szemaforok bevezetése Egyszerűsítés, ha lehet

4

Gregorics Tibor

Modell alkotás





Meghatározzuk az állapot-átmenetek műveleteit, az előfeltételeikkel együtt különös tekintettel az aktív állapotok be- (entry) és kilépési (exit) fázisaira (ezek őrfeltételes atomi műveletek lesznek majd az absztrakt programban), illetve az erőforrás-igénylést elindító (request) tevékenységre. Töröljük azokat a műveleteket, amelyek nem eredményeznek állapot-átmenetet.

  





Gregorics Tibor

Szintézis és verifikáció

5

Absztrakt program tervezése 



3

Modell alkotás

Változók kezdeti értékei Folyamatok szerkezete Atomi műveletek kijelölése




6

A rendszer állapotait jellemző változókat vezetünk be. Az állapotok invariánsát felírjuk a változók segítségével. Meghatározzuk az így bevezetett változók kezdeti értékeit. Elkészítjük a folyamatok vázát a kezdeti értékadásokkal együtt. Az osztott változókon dolgozó értékadásokat (az állapotdiagram műveleteit) a folyamatokhoz rendeljük úgy, hogy a folyamatok önmagukban helyes eredményt adjanak. Az értékadó utasításokat (ha kell őrfeltételes) atomi tevékenységekké fogjuk össze, ha azok csak kölcsönös kizárással hajthatók végre. (lásd külön a következő dián) Igazoljuk a az egyes folyamatok helyességét.

Gregorics Tibor


7

1

2012.12.27.

Atomi műveletek őrfeltételének meghatározása

Konkrét program elkészítése

1. Az S művelet a modell egy aktív folyamatának művelete, amely olyan, úgynevezett szinkronizációs feltétellel van ellátva, amelyik egy közös erőforrás állapotától függ. Ekkor ez a feltétel lesz a β őrfeltétel. 2. Kezdetben csak az S műveletet és az ahhoz tartozó I invariánst (a közös, osztott változókra hivatkozó predikátum) ismerjük. • Először meghatározzuk a {K} <S> {L} tételt úgy, hogy a K és L csak az S-re lokális változókra hivatkozhatnak. • Ellenőrizzük, hogy az egyes folyamatok bizonyításai ezzel nem interferálnak. • A β őrfeltételre az alábbinak kell teljesülni: K  I  β ⇒ lf(S, L  I) Gregorics Tibor


   

8

1. Példa: Számítógép labor használata 

Egy számítógép laborban számítógépek vannak van.



Hallgatók a tanulmányaikhoz számítógépet is használnak. Ha nincs szabad gép, akkor a laboron kívül várakoznak, amíg fel nem szabadul egy. A számítógép-használat befejeztével elhagyják a labort, és mással foglalkoznak, amíg újra nincs szükségük számítógépre.



Gregorics Tibor


9

Osztály diagram

(Sike Sándor és Varga László esettanulmánya)



Szemaforokat rendelünk az őrfeltételes utasításokhoz. Definiáljuk a szemaforok kezdeti értékeit. Implementáljuk az őrfeltételes utasításokat a szemaforokat használó sémákkal. Ha lehetséges, akkor egyszerűsítjük a programot.

System

*

Crew

maintain 

Lab

0..1

A labor karbantartását rendszergazdák látják el. Bármelyik rendszergazda kezdeményezhet karbantartást, de egy adott pillanatban csak egy végezhet karbantartást. A karbantartás addig nem kezdhető meg, amíg hallgató tartózkodik a laborban.

*

 use 0..cap

Student

cap {exclude}

Szimuláljuk ennek a rendszernek a működését!

Gregorics Tibor


10

Dinamikus modell 

Gregorics Tibor


12

Hallgatók dinamikus modellje

Állapotok: a rendszer állapotát a rendszergazdák állapota, a



hallgatók állapota és a labor állapota együttesen határozza meg.

Egy hallgató kétféle állapotban lehet: o

Számítógépet használ (do/use).

o

Egyéb tevékenységet folytat (do/work).

system state studentj state …

crewi state

…

lab state

…

studentj state

…

use.ent[φ1] do / work

do / use use.ex

Gregorics Tibor


13

Gregorics Tibor


14

2

2012.12.27.

Rendszergazdák dinamikus modellje 

Labor dinamikus modellje

Egy rendszergazda háromféle állapotban lehet: o

Pihen (do/rest)

o

Karbantartási igénye van (requesting).

o

Karbantart (do/maintain)



A labor állapotát a benn tartózkodó hallgatók száma (t), a karbantartási igényt benyújtó rendszergazdák száma (r), és a karbantartást végző rendszergazdák száma (w) határozza meg.



Az állapot átmeneteket a Student és a Crew műveletek végzik. lab state

crewi state

do / rest

use.ent

requesting

do / maintain

maintain.ent[φ2]

OK

use.ent[φ3]

0
maintain.ex[φ6]

request

use.ex[φ4] normal

maintain.ex

r=0  w=0

t=0

empty

request

full

maintain.ex[φ5]

maintained t=cap

Gregorics Tibor


15

Állapot-átmenetek feltételei 



φ1(use.ent) :  in full  in OK

o

φ2 (maintain.ent) : in empty   in maintained

o

φ3 (use.ent) : t = cap‒1

o

φ4 (use.ex) : t = 1

o

φ5 (maintain.ex) : r>0

o

φ6 (maintain.ex) : r = 0 φ1(use.ent) :t≠cap  w=0  r=0

o

φ2 (maintain.ent) : w=0  t=0

i

változók t, r, w : ℕ tevékenység


maintain.ent use.ent

18

φ1 φ2

atomi utasítás igaz

w=0  t=0

igaz

<w := w1>

t≠cap  w=0  r=0

igaz

Gregorics Tibor


19

Absztrakt program

t, r, w :=0, 0, 0; parbegin crew1‖ … ‖ crewn‖ student1‖ …‖ studentm parend

crewi: loop rest; await igaz then r := r+1 ta; await w=0  t=0 then r := r1; w := w+1 ta; maintain; await igaz then w := w1 ta; end

A rendszer invariánsa: I ≡ 0≤t ≤ cap  r≥0  (w=0  w=1)

crewi: loop rest; <w=0  t=0 → r := r1; w := w+1> maintain; studentj: loop <w := w1> work; end use; end Gregorics Tibor

work; use; end

feltétel

maintain.ex

Megoldás váza



17

j

rest; request; maintain; end

request

use.ex Gregorics Tibor

w=1 Szintézis és verifikáció

t, r, w :=0, 0, 0; parbegin crew1‖ … ‖ crewn‖ student1‖ …‖ studentm parend crew : loop student : loop

A fentiek közül a φ1 és φ2 szinkronizációs feltétel is egyben. o

Gregorics Tibor

Megoldás váza

A diagrammokban feltüntettük, hogy hol van szükség őrfeltételre: o

r>0  w=0

requested maintain.ent


studentj: loop work; await t≠cap  w=0  r=0 then t := t+1 ta; use; await igaz then t := t1 ta; end 20

Gregorics Tibor


21

3

2012.12.27.

Helyesség

I ≡ 0≤t ≤ cap  r≥0  (w=0  w=1)

Új annotáció

 wi = 0  ri = 0 crewi: loop { I } rest;  wi = 0  ri = 0 Kisegítő változók: {I} ri:=1 wk, rk : {0,1} k=1..n await igaz then r := r+1 ta;  wi = 0  ri = 1 { I  r>0 } tk : {0,1} k=1..m await w=0  t=0 then r := r1; w := w+1 ta; Új invariáns: maintain;  wi = 1  ri = 0 Irégi  w = Σk=1..nwk { I  t =0  w=1}  t = Σk=1..m tk await igaz then w := w1 ta; ri:=0; wi:=1 { I} wi:=0  r = Σk=1..n rk end  wi = 0  ri = 0 studentj: loop { I }  tj = 0 work;

Parciális helyesség: 

crewi: loop { I } rest; {I} • crewi⟷ crewj ? await igaz then r := r+1 ta; { I  r>0 } • studenti⟷ studentj ? await w=0  t=0 then r := r1; w := w+1 ta; • crewi⟷ studentj ? maintain; { I  t =0  w=1} await igaz then w := w1 ta; studentj: loop { I } {I} work; end {I} Interferencia-mentesség:

{I}  tj = 0 await t≠cap  w=0  r=0 then t := t+1 ta; use;  tj = 1 tj:=1 { I  t>0  w=0} tj:=0 await igaz then t := t1 ta; {I}  tj = 0 end

await t≠cap  w=0  r=0 then t := t+1 ta; use; { I  t>0  w=0 } await igaz then t := t1 ta; { I  t < cap } end

Gregorics Tibor


Parciális helyesség

22

I ≡ 0≤t ≤ cap  (w=0  w=1) 

Gregorics Tibor


•

maintaini⟷ maintainj 

•

legfeljebb cap darab usej 

24

crewi⟷ crewj 

•

studenti⟷ studentj 

•

crewi⟷ studentj




Holtpontmentesség

25

I ≡ 0≤t ≤ cap  (w=0  w=1) 

w = Σk=1..n wk  t = Σk=1..m tk  r = Σk=1..n rk crewi: loop rest; await igaz then r:=r+1 ta; { I  wi=0 } await w=0  t=0 then r:=r1; w:=w+1; wi:=1 ta; maintain; await igaz then w:=w1; wi:=0 ta; end

studentj: loop work; { I  tj=0 } await t≠cap  w=0  r=0 then t:=t+1; tj:=1 ta; use; await igaz then t:=t1; tj:=0 ta; end

j

work; await t≠cap  w=0  r=0 then t:=t+1; tj:=1 ta; { I  t>0  w=0  tj=1} use; await igaz then t:=t1; tj:=0 ta; end Szintézis és verifikáció

crewi: loop { I  wi=0  ri = 0 } rest; { I  wi=0  ri = 0 } await igaz then r:=r+1; ri:=1 ta; { I  r>0  wi=0  ri = 1 } await w=0  t=0 then r:=r1 ; ri:=0; w:=w+1; wi:=1 ta; maintain; { I  t=0  w=1  wi=1  ri = 0 } await igaz then w:=w1; wi:=0 ta; end

Gregorics Tibor

Kiéheztetés lehet

crewi: loop rest; await igaz then r:=r+1 ta; await w=0  t=0 then r:=r1; w:=w+1; wi:=1 ta; { I  t=0  w=1  wi=1} maintain; await igaz then w:=w1; wi:=0 ta; end student : loop

Gregorics Tibor

23

studentj: loop { I  tj=0 } work; { I  tj=0 } await t≠cap  w=0  r=0 then t:=t+1; tj:=1 ta; use; { I  t>0  w=0  tj=1} await igaz then t:=t1; tj:=0 ta; end

I ≡ 0≤t ≤ cap  (w=0  w=1) 

use ⟷ maintain 

•



w = Σk=1..n wk  t = Σk=1..m tk  r = Σk=1..n rk

•


Interferencia mentesség

w = Σk=1..n wk  t = Σk=1..m tk  r = Σk=1..n rk

crewi: loop { I  wi=0  ri = 0 } rest; { I  wi=0  ri = 0 } await igaz then r:=r+1; ri:=1 ta; { I  r>0  wi=0  ri = 1 } await w=0  t=0 then r:=r1 ; ri:=0; w:=w+1; wi:=1 ta; maintain; { I  t=0  w=1  wi=1  ri = 0 } await igaz then w:=w1; wi:=0 ta; end studentj: loop { I  tj=0 } work; { I  tj=0 } await t≠cap  w=0  r=0 then t:=t+1; tj:=1 ta; use; { I  t>0  w=0  tj=1} await igaz then t:=t1; tj:=0 ta; end

Kölcsönös kizárás

Gregorics Tibor

⋀i=1..n ( I  wi=0  (w≠0  t≠0))  ⋀j=1..m (I  tj=0  (t=cap  w ≠ 0  r ≠ 0 )) 26

Gregorics Tibor


 w=0  t≠0  t=0 ≡↓ 27

4

2012.12.27.

Implementálás szemaforokkal 

Implementálás szemaforokkal crewi: loop rest; P(s); r := r+1; schedule; P(s); if w≠0  t ≠ 0 then cw := cw+1; V(s); P(sw) fi; r := r1; w := w+1; schedule; crewi: maintain; loop P(s); rest; w := w1; await igaz then r := r+1 ta; schedule; await w=0  t=0 then r := r1; w := w+1 ta; end maintain; await igaz then w := w1 ta; end

Három szemafor (s, bw, bt) , két egész típusú változó (cw, ct): • s ~ univerzális célú, • sw, cw ~ await w=0  t=0 then r := r1; w := w+1 ta • st, ct ~ await t≠cap  w=0  r=0 then t := t+1 ta s, sw, cw, st, ct, t, r, w :=1, 0, 0, 0, 0, 0, 0, 0; parbegin crew1‖ … ‖ crewn‖ student1‖ …‖ studentm parend



Használjuk majd az alábbi ütemezőt: if w =0  t =0  cw>0  cw := cw  1; V(sw)  t≠cap  w =0  r =0  ct>0  ct := ct1; V(st) else V(s) fi;

Gregorics Tibor


28

Implementálás szemaforokkal

r-t elimináljuk, mert

30

Egyszerűsítés

itt nem teljesülhet r =0 (r:=r+1 miatt), sem w =0  t =0  cw>0 (ennek már a megelőző kritikus szakasz végén is fenn kellene állnia, ami nem lehet. Tfh lehet, de ekkor r>0 miatt az ottani schedule a V(sw) révén újabb kritikus szakaszt indít.

Gregorics Tibor


31

Konkrét program

studentj: loop work; cw ≠ 0 P(s); if t=cap  w ≠ 0  r ≠ 0 then ct := ct+1; V(s); P(st) fi; t := t+1; schedule; use; if w =0  t =0  cw>0  cw := cw  1; V(sw) P(s);  t≠cap  w =0  r =0  ct>0  ct := ct1; V(st) t := t1; elsif V(s) schedule; fi; end if w =0  t =0  cw>0  cw := cw  1; V(sw)  t≠cap  w =0  r =0  ct>0  ct := ct1; V(st) else V(s) fi; cw = 0 Gregorics Tibor

29

crewi: r és cw jelentése loop azonos 3 rest; P(s); schedule helyett V(s) 1 3 r := r+1; schedule; V(s);P(s) helyett skip 2 P(s); if w≠0  t ≠ 0 then cw := cw+1; V(s); P(sw) fi; 3 r := r1; w := w+1; rendszergazda igényét rögtön elégítsük ki vagy álljon be sw-hez schedule; V(s) maintain; itt nem teljesülhet w =0 4 P(s); 3 w := w1; cw =0 schedule; if w =0  t =0  cw>0 cw cw:=:=cw cw 1;1;V(sw) V(sw) end  t≠cap  w =0  r =0  ct>0 ctct :=:= ct1; ct1; V(st); V(st) else V(s) 5 fi;

use; await igaz then t := t1 ta; end Szintézis és verifikáció


Egyszerűsítés

studentj: loop work; P(s); if t=cap  w ≠ 0  r ≠ 0 then ct := ct+1; V(s); P(st) fi; t := t+1; schedule; use; P(s); studentj: t := t1; loop schedule; work; end await t≠cap  w=0  r=0 then t := t+1 ta;

Gregorics Tibor

Gregorics Tibor


32

s, sw, cw, st, ct, t, w :=1, 0, 0, 0, 0, 0, 0; parbegin crewi: crew1‖ … ‖ crewn‖ student1‖ …‖ studentm loop parend rest; P(s); if w≠0  t ≠ 0 then cw := cw+1; V(s); P(sw) fi; w := w+1; V(s); maintain; P(s); w := w1; if cw>0  cw := cw  1; V(sw)  r =0  ct>0  ct := ct1; V(st) else V(s) fi; end Gregorics Tibor


33

5

2012.12.27.

Egyszerűsítés

2. Példa: kritikus szakaszok

studentj: loop work; P(s); if t=cap  w ≠ 0  cw ≠ 0 then ct := ct+1; V(s); P(st) fi; t := t+1; if t≠cap  ct>0  ct := ct1; V(st) else V(s) fi; use; P(s); t := t1; if t =0  cw>0  cw := cw  1; V(sw)  r =0  ct>0  ct := ct1; V(st); else V(s) fi; end Gregorics Tibor


Egymással párhuzamosan hajtsunk végre olyan tevékenységeket, amelyekben lehetnek • olyan (kritikus) szakaszok, amelyek egy erőforrást kizárólagos módon használnak, és • olyan (nem kritikus) szakaszok, amelyek csak lokális adatokat használnak.  Egy konkurens program minden folyamata ismétlődően hajtson végre egy kritikus és egy nem kritikus szakaszból álló tevékenységet. 

34

Statikus modell

Gregorics Tibor


35

Dinamikus modell system state

System clienti state

…

…

server state

2 .. *

Server

 use 0..1

clienti state

Client

server state

do / otherjob use.ent[ in unused]

use.ex

unused use.ent

do / use

Gregorics Tibor


36

37

Tekintsük az atomi utasítást. lf(ini :=1; ini =1  I) = (1=1  in1+ … +ini‒1 +1+ini+1+ … +inn 1 ) =(in1+ … +ini‒1 +ini+1+ … +inn=0 ) • Ez nem következik az I-ből, ezért kell őrfeltétel: β= in1+ … +ini‒1 +ini+1+ … + inn=0 • vagy helyette β = in1 + … + inn =0  Tekintsük az atomi utasítást. • lf(ini :=0; ini =0  I) = (0=0  in1+ … +ini‒1 +0+ini+1+ … +inn=0  1 ) • Ez következik az I-ből, tehát nem kell őrfeltétel. 

•

• ink =1 ~ clientk kritikus szakaszában (use) van A rendszer invariánsa: I ≡ Σk=1..n ink ≤ 1 Kritikus szakaszba lépés őrfeltétele (use.ent): Σk=1..n ink = 0

in :=0 parbegin client1‖ … ‖ clientn parend clienti: loop otherjob; use; end Gregorics Tibor


KIβ ⇒lf(S, LI)

clienti: loop otherjob; parbegin client1‖ … ‖ clientn parend use; end  Legyen in:{0,1}n egy tömb,



used

Atomi értékadások őrfeltételei

Megoldás váza



Gregorics Tibor

use.ex


38

Gregorics Tibor


39

6

2012.12.27.

Absztrakt algoritmus

Konkrét algoritmus in :=0; s, sc, cc:= 1, 0, 0; parbegin client1‖ … ‖ clientn parend

I ≡ Σk=1..n ink ≤ 1

in :=0 { I  Σk=1..n ink = 0 } clienti: loop parbegin otherjob; crew1‖ … ‖ crewn { I  ini = 0 } parend await Σ k=1..n ink = 0 then ini:=1 ta ; { I  ini = 1 } use; await igaz then ini :=0 ta ; { I  ini = 0 } end •

helyes (interferencia-mentes)

•

kölcsönös kizárás, holtpontmentesség

•

kiéheztetés lehet

Gregorics Tibor

Vezessük be az s ≡ 1 ‒ Σ k=1..n ink mutexet, amelynek segítségével a várakozó utasításokat

clienti: loop másképpen is írhatjuk. otherjob; <s>0 → s:=s‒1; ini :=1>; use; Ekkor ink (k=1…n) kisegítő változók <s:=s+1; ini :=0>; feleslegessé válnak, és end az < s>0 → s:=s‒1>-t P(s)-sel,

clienti: loop az <s:=s+1>-t a V(s)-sel implementálhatjuk. otherjob; P(s) ; use; V(s) ; end


40

Gregorics Tibor

3. Példa: termelő fogyasztó probléma 


Osztály diagram

Kétféle fajtájú párhuzamosan futó tevékenység egyetlen egyelemű puffert használ:

System

az egyik fajta beletesz (deposit) egy újabb elemet, feltéve hogy az üres (elem nem írható felül) A másik fajta kivesz (fetch) egy elemet, feltéve hogy nem üres (egy elemet csak egyszer lehet kivenni).

• •

41

1 .. n

Producer

1 .. m deposit  0..1

Buffer

 fetch 0..1

Consumer

0 ≤ v ≤ cap {exclude}

Gregorics Tibor


43

Gregorics Tibor

Dinamikus modell

Megoldás váza

system state produceri state

do/ produce d.ex …

d.ent [ in full] do/ deposit

Gregorics Tibor

…

d.ent [v=0]



buffer state

consumerj state

empty

do/ process

f.ent [v=1] normal

d.ent f.ent [v+1=cap] [v=cap ] full


f.ent [ in empty]

44

Pi: loop Cj: loop produce; ‖ fetch; deposit; process; end end

Változók: vol:ℕ, free:{0,1}, p :{0,1}n, c:{0,1}m vol: a puffer feltöltöttsége. free: 0, ha valamelyik folyamat használja a puffert, különben 1. pi : 1, ha Pi folyamat használja a puffert, különben 0. cj : 1, ha Cj folyamat használja a puffert, különben 0.



f.ex …


…

Invariáns: I ≡ 0  vol  cap  free=1‒Σk=1..n pk ‒ Σl=1..m cl

p, c, vol, free := 0, 0, 0, 1; parbegin P1‖ … ‖ Pn‖ C1‖ …‖ Cm parend Pi: loop produce; ; deposit; end

do/ fetch

45

Gregorics Tibor

Cj: loop ; fetch; process; end Szintézis és verifikáció

46

7

2012.12.27.

Atomi értékadások őrfeltételei (termelő)

Atomi értékadások őrfeltételei (termelő)

QIβ ⇒lf(S, RI)

QIβ ⇒lf(S, RI)

{pj =0  vol=v’} {pj =1  free=0  vol=v’+1} • lf(pj :=1 ; free:=0; vol:=vol+1; pj =1  free=0  vol=v’+1  I)= 1=1  0=0  vol+1=v’+1  0vol+1cap  0=1‒Σk=1..n pk‒Σl=1..m cl • Ez nem következik az pj =0  vol=v’  I-ből, ezért kell őrfeltétel: β= vol {pj =0  free=1 } 

• •

lf(pj :=0 ; pj =0  free=1  I)= 0=0  1=1  0vol cap  1=1‒Σk=1..n pk‒Σl=1..m cl Ez következik az I-ből, tehát itt nem kell őrfeltétel.

{cj=0  vol=v’} {cj =1  free=0  vol=v’‒1} • lf(cj :=1 ; free:=0; vol:=vol+1; cj =1  free=0  vol=v’+1  I)= 1=1  0=0  vol‒1=v’‒1  0vol ‒1cap  0=1‒Σk=1..n pk‒Σl=1..m cl • Ez nem következik az cj=0  vol=v’  I-ből, ezért kell őrfeltétel: β= vol>0  free=1  {cj =1} {cj =0  free=1 } 

lf(cj :=0 ; cj =0  free=1  I)= 0=0  1=1  0vol cap  1=1‒Σk=1..n pk‒Σl=1..m cl Ez következik az I-ből, tehát itt nem kell őrfeltétel.

• •

I ≡ 0  vol  cap  free=1‒Σk=1..n pk‒ Σl=1..m cl Gregorics Tibor


I ≡ 0  vol  cap  free=1‒Σk=1..n pk‒ Σl=1..m cl 47

Gregorics Tibor

Absztrakt program


48


p, c, vol, free:= 0, 0, 0, 1; Pi : loop {I  pi =0} parbegin P1‖ … ‖ Pn‖ C1‖ …‖ Cm parend e:= produce(); await vol0  free=1 then helyes (interferencia) cj:= 1; free:=0; vol:=vol‒1 ta; free=0  pi =1  cj =1  {I  cj=1  free=0} e:=fetch();  kölcsönös kizárás await igaz then cj:= 0; free:=1 ta; pi =1  cj =1  {I  cj=0} holtpontmentesség process(e); free=0  pi =0  cj =0  end



Három szemafor (s, bw, bt) és két egész típusú változó (cw, ct): • s ~ univerzális célú, •

sp, cp

~ await vol
•

sc, cc

~ await vol>0  free=1

s, sp, cp, sc, cc, p, c, vol, free :=1, 0, 0, 0, 0, 0, 0, 0, 1; parbegin P1‖ … ‖ Pn‖ C1‖ …‖ Cm parend 

Használjuk majd az alábbi ütemezőt: if vol0  cp := cp1; V(sp)  vol>0  free=1  cc>0  cc := cc1; V(sc)  igaz  V(s) fi;

kiéheztetés lehet

Gregorics Tibor


49




50

Implementálás szemaforokkal Cj: loop P(s); if vol=0  free=0 then cc:=cc+1; V(s); P(sc); fi cj := 1; free:=0; vol:=vol‒1; schedule; e:=fetch(); P(s); cj := 0; free:=1; schedule; process(e); Cj : loop end await vol>0  free=1 then cj := 1; free:=0; vol:=vol‒1 ta; e:=fetch(); await igaz then cj := 0; free:=1 ta; process(e); end

Pi : loop e:= produce(); P(s); if vol=cap  free=0 then cp:=cp+1; V(s); P(sp); fi pi := 1; free:=0; vol:=vol+1; schedule; deposit(e); P(s); pi := 0; free:=1; schedule; Pi : loop end e:= produce(); await vol
Gregorics Tibor

51

Gregorics Tibor


52

8

2012.12.27.

Egyszerűsítés

Egyszerűsítés

Pi : loop e:= produce(); P(s); if vol=cap  free=0 then cp:=cp+1; V(s); P(sp); fi pi := 1; free:=0; vol:=vol+1; schedule; deposit(e); V(s); P(s); pi := 0; free:=1; schedule; V(s); end if vol0  cp := cp1; V(sp)  vol>0  free=1  cc>0  cc := cc1; V(sc) else V(s) fi;

Gregorics Tibor

Cj: loop P(s); if vol=0  free=0 then cc:=cc+1; V(s); P(sc); fi cj := 1; free:=0; vol:=vol‒1; schedule; e:=fetch(); V(s); P(s); cj := 0; free:=1; schedule; process(e); end if vol0  cp := cp1; V(sp)  vol>0  free=1  cc>0  cc := cc1; V(sc); else V(s) fi;


53

Gregorics Tibor

4. Példa: Étkező filozófusok


54

Osztály diagram

Adott számú filozófus ül egy kör alakú asztal körül, az asztal közepén egy nagy tál étel, minden filozófus előtt egy tányér, attól jobbra illetve balra egy-egy villa, amelyet jobb illetve baloldali szomszédjukkal közösen, de nem egyszerre használhatnak.  A filozófusok felváltva esznek és gondolkodnak. Ha enni akarnak, meg kell várniuk, hogy a tőlük jobbra illetve balra eső villa is szabad legyen, ezután megkezdhetik az evést, majd az evés végeztével visszateszik az asztalra villáikat. 

Gregorics Tibor


System

n

Fork

55



philosopheri state

forkj state

do/ think

free

eat.ex …

…

eati.ex eati⊕1.ex

eati.ent eati⊕1.ent





56

Pi: loop think; eat; end

Változók: p :{0,1}n, pk=1 ↔ k. filozófus eszik f :{0,1}n, fk=1 ↔ k. filozófustól balra eső villa használatban Invariáns: I ≡ k∊{1…n}: (pk=0  pk⊕1=0)  pk=1↔(fk=1  fk⊕1=1)  fk=1→(fk⊝1=1  fk⊕1=1) p, f := 0, 0; parbegin P1‖ … ‖ Pn parend

…

used

do/ eat

Gregorics Tibor

Philosopher

Megoldás váza

system state

…

0, 2

Gregorics Tibor

Dinamikus modell

eat.ent [ in freei  in freei⊕1 ]

n  use

57

Pi: loop think; < fi=0  fi⊕1=0 →pi := 1; fi:=1; fi⊕1:=1>; eat; < pi := 0; fi:=0; fi⊕1:=0 > end Gregorics Tibor


58

9

2012.12.27.



Absztrakt program

I ≡ k∊{1…n}: (pk=0  pk⊕1=0 )  pk=1↔(fk=1  fk⊕1=1)  fk=1→(fk⊝1=1  fk⊕1=1)

Pi: loop { I  pi =0 } think; p , f := 0, 0; await fi=0  fi⊕1=0 then parbegin P1‖ … ‖ Pn parend pi := 1; fi:=1; fi⊕1:=1 ta; { I  pi = 1  fi=1  fi⊕1=1 } eat; await igaz then pi := 0; fi:=0; fi⊕1:=0 ta; { I  pi =0  fi=0  fi⊕1=0 } end

Implementálás szemaforokkal 

Három szemafor (s, bw, bt) és két egész típusú változó (cw, ct): • s ~ univerzális célú, •

sf, cf

~ await fi=0  fi⊕1=0

p , f , s, se, ce:= 0, 0, 1, 0, 0, 0, 0; parbegin P1‖ … ‖ Pn parend 

Használjuk majd az alábbi ütemezőt: if fi=0  fi⊕1=0  cf>0 then cf := cf1; V(sf) else V(s) fi;

helyesség (interferencia) {(I  pj =0)  pre(uik)} uik {I  pj =0} {(I  pj = 1  fj=1  fj⊕1=1 )  pre(uik)} uik {I  pj = 1  fj=1  fj⊕1=1 }

kölcsönös kizárás (csak a szomszédos filozófusokra) (I  pi = 1  fi=1  fi⊕1=1)  (I  pi⊕1 = 1  fi⊕1=1  fi⊕2=1)

holtpontmentesség (kiéheztetés lehet) i∊{1…n}: I  pi = 0  (fi=1  fi⊕1=1) Gregorics Tibor


59


60

Példa (adatbázis)

Implementálás szemaforokkal Pi: loop think; P(s); if fi≠0  fi⊕1≠0 then cf:=cf+1; V(s); P(se) fi; pi := 1; fi:=1; fi⊕1:=1; schedule; eat; P(s); Pi: loop pi := 0; fi:=0; fi⊕1:=0; think; schedule; await fi=0  fi⊕1=0 then end pi := 1; fi:=1; fi⊕1:=1 ta; eat; await igaz then pi := 0; fi:=0; fi⊕1:=0 ta; end Gregorics Tibor

Gregorics Tibor



Egy adatbázist kétféle folyamat használhat • • • •

n>0 darab író (writer) és m>0 darab olvasó (reader) Az író folyamatok egymást kölcsönösen kizárják az adatbázis használatából. Az olvasó folyamatok közül tetszőleges számú folyamat használhatja egyidejűleg az adatbázist. Egy író és egy olvasó folyamat kölcsönösen kizárja egymást az adatbázis használatából.

parbegin W1|| … || Wn || R1|| … || Rm parend


61

Osztály diagram

Gregorics Tibor


62

Dinamikus modell system state

System

…

1 .. n

Writer

writeri state

1 .. m write  0..1

Database

 read *

…

database state

…

do / read

read.ent[φ1]

…

database state

readerj state read.ex

Reader

readerj state

do / work unused write.ent read.ent

{exclude} writeri state do / work

Gregorics Tibor


63

Gregorics Tibor

write.ent[φ2] write.ex

write.ex read.ex[φ4]

used do / write read.ex[φ3] Szintézis és verifikáció

64

10

2012.12.27.

Példa (adatbázis): segédváltozók

Megoldás váza 

Az adatbázis állapotát az olvasás illetve írás flagjei (r, w : {0,1}), és az olvasást végző folyamatok száma (c : ℕ) jellemzi. tevékenység

feltétel

write.ent

φ1

write.ex read.ent

φ2

read.ex



atomi utasítás w=0  r=0 <w := 1> igaz

<w := 0>

w=0

igaz



Vezessünk be megfelelő annotáláshoz kisegítő változókat: • wi :{0,1} ~ 1, ha az i-dik folyamat éppen ír (i=1...n) • rj : {0,1} ~ 1, ha a j-dik folyamat éppen olvas (j=1...m) Invariáns állítás: I ≡ w=sgn(k=1..n wk )  c = k=1..m rk  r=sgn(c)  (w=0  r=0) w, r, c, w, r:=0, 0, 0, 0, 0; {I} parbegin W1‖ … ‖ Wn‖ R1‖ …‖ Rm parend {↓}

w, r, c := 0, 0, 0; parbegin W1‖ … ‖ Wn‖ R1‖ …‖ Rm parend Wi: loop work; write; end Gregorics Tibor

Rj: loop work; read; end Szintézis és verifikáció

65

Példa (adatbázis): annotálás és helyesség

{ I  rj =0 } await w=0 then c:=c+1; r:=1; rj:=1 ta; { I  rj=1  r=1  cr>0 } await igaz then c:=c‒1; if c=0 then r := 0 fi; rj :=0 ta;

{ I  wi=1  w=0 } await igaz then w:=0; wi:=0 ta



Gregorics Tibor





I ≡ w=sgn(k=1..n wk )  c = k=1..m rk  r=sgn(c)  (w=0  r=0) Szintézis és verifikáció

{ I  rk=1  r=1  c>0 } { I  rk=1  r=1  c>0 } { I  rk=0 } { I  wk=0 } { I  wk=1  w=1 } { I  wk=1  w=1 }


68

Példa (adatbázis): holtpontmentesség

Egy író és egy olvasó folyamat kölcsönösen kizárják egymást az adatbázis használatából, azaz bármelyik i∊{1…n}-re és bármelyik j∊{1…m}-re: prewritei  prereadj ≡ ↓ o [ I  wi=1  w=1]  [I  rj=1  r=1  c>0] Az író folyamatok kölcsönösen kizárják egymást az adatbázis használatából, azaz bármelyik i,j∊{1…n}-re, ahol i≠j : prewritei  prewritej ≡ ↓ o [ I  wi=1  w=1]  [ I  wj=1  w=1]

Gregorics Tibor

{ I  rk=1  r=1  c>0 } { I  rk=1  r=1  c>0 } { I  rk=0 }

I ≡ w=sgn(k=1..n wk )  c = k=1..m rk  r=sgn(c)  (w=0  r=0) 67

Példa (adatbázis): kölcsönös kizárás 

66

{ I  wk=0 } { I  wk=1  w=1 } { I  wk=1  w=1 }

{ I  wi=0 } await w=0  r=0 then w:=1; wi:=1 ta;

I ≡ w=sgn(k=1..n wk )  c = k=1..m rk  r=sgn(c)  (w=0  r=0) Szintézis és verifikáció


Példa (adatbázis): interferencia-mentesség

Rj:loop { I  rj=0 } await w=0 then c:=c+1; r:=1; rj:=1 ta; { I  rj=1  r=1  c>0 } read; { I  rj=1  r=1  c>0 } await igaz then c:=c‒1; if c=0 then r := 0 fi; rj :=0 ta; { I  rj=0 } Wi:loop { I  wi=0 } work; work; end { I  wi=0 } await w=0  r=0 then w:=1; wi:=1 ta; { I  wi=1  w=1 } write; { I  wi=1  w=1 } await igaz then w:=0; wi:=0 ta; end Gregorics Tibor

Gregorics Tibor

A holtpontmentességhez bizonyítani kell, hogy: ⋀ i=1..n D(Wi)  ⋀ j=1..m D(Rj) ≡ ↓ ahol D(Wi) = I  wi=0  (w=1  r=1) és D(Rj) = I  rj=0  w=1 ⋀ i=1..n D(Wi)  ⋀ j=1..m D(Rj)  I  k=1..n wk =0  w=1 ≡ ↓

I ≡ w=sgn(k=1..n wk )  c = k=1..m rk  r=sgn(c)  (w=0  r=0) 69

Gregorics Tibor


70

11

2012.12.27.

Példa (adatbázis): koplaltatás 


A rendszer nem mentes a koplaltatástól. Lehet olyan helyzet hogy o minden író folyamat várakozik: ⋀ i=1..n ( I  wi =0  (w=1  r=1)) o mert az adatbázist olvasó folyamatok használják: I  r=1 o és további olvasó folyamatok részére szabad az út a belépéshez: I  rj=0  w=0

Wi:loop work; P(s); if w≠0  r ≠ 0 then cw:=cw+1;V(s); P(sw) fi; w:=1; schedule; write; P(s); w:=0; Wi:loop schedule; work; end await w=0  r=0 then w:=1 ta; write; await igaz then w:=0 ta end

I ≡ w=sgn(k=1..n wk )  c = k=1..m rk  r=sgn(c)  (w=0  r=0) Gregorics Tibor


71

Gregorics Tibor


72

Implementálás szemaforokkal Rj:loop P(s); if w≠0 then cr:=cr+1; V(s); P(sr) fi; c:=c+1; r:=1; schedule; read; P(s); c:=c‒1; if c=0 then r := 0 fi; schedule; work; Rj:loop end await w=0 then c:=c+1; r:=1 ta; read; await igaz then c:=c‒1; if c=0 then r := 0 fi ta; work; end Gregorics Tibor


73

12

Atomi műveletek őrfeltételének meghatározása. Konkrét program elkészítése. 1. Példa: Számítógép labor használata

Recommend Documents