Sisteme Distribuite
Introducere
Capitolul 1. Conceptul de timp
§1.1. Introducere
§1.2. Modelarea sistemelor distribuite
Capitolul 2. Excluderea mutuală
§2.1. Problematica
§ 2.2. Algoritmul lui Lamport
§2.3. Algoritmul lui Ricart și Agrawala
Capitolul 3. Stare globală
§3.1. Tăieturi consistente
§3.2. Instatanee globale ale proceselor
§3.3. Instantanee globale ale proceselor și canalele
Capitolul 4. Predicate globale
§4.1. Problematică
§4.2. Predicate liniare
§5.2. Algoritm centralizat pentru WCP bazat pe vectori ceas
Capitolul 5. Predicate globale conjunctive
§5.1. Predicate conjunctive slabe
§5.2. Algoritm centralizat pentru WCP bazat pe vectori ceas
§5.3. Algoritm centralizat pentru WCP bazat pe dependență directă
§5.4 Algoritm distribuit pentru WCP bazat pe
vectori ceas
§5.5. Un algoritm centralizat pentru predicate conjunctive generalizate
§5.6. Un ceas vector bogat și algoritmul de detecție GCP distribuit
Capitolul 6. Predicate globale relaționale
§6.1 Predicate relaționale cu două variabile întregi
§6.2 Predicate relaționale cu N variabile booleene
§6.3 Predicate pentru sume măginite
Capitolul 7. Predicate globale
§7.1 Secvențe globale
§7.2 Logica predicatelor globale
§7.3 Predicate conjunctive tari
Capitolul 8. Predicate ale fluxului de control
§8.1 Introducere
§8.1 Logica LRDAG
§8.3 Exemple
§8.4 Algoritmul descentralizat pentru detecție
Capitolul 9. Relații de ordine
§ 9.1 Relații de ordine între mesaje
§9.2 Ordinea FIFO a mesajelor
§9.3 Odinea cauzală a mesajelor
§9.5 Ordonarea sincronă a mesajelor
Capitolul 10. Calculul
§10.1. Funcții globale
§ 10.2 Calculări repetate
Concluzii
Referințe bibliografice
=== Programare_paralela ===
Introducere
Evoluția sistemelor de operare moderne este strâns legată de introducerea unor modele și concepte noi, menite să asigure o cât mai bună servire a utilizatorilor și ocupare a resurselor, concomitent cu creșterea siguranței de funcționare a sistemului.
Pentru sistemele de calcul în prezent se cunosc două căi de creștere a vitezei de calcul : prin creșterea vitezei procesorului sau prin creșterea numărului de procesoare.
Un sistem concurent format din procesoare care lucrează în manieră “lock – step” se numește sistem sincron. Un sistem concurent în care procesoarele sunt slab cuplate lucrând independent una de cealaltă se numește sistem asincron. Sistemele asincrone se pot de asemenea departaja în sisteme bazate pe divizarea memoriei și sisteme bazate pe mesaje. Vom numi sistemele bazate pe divizarea memoriei: sisteme paralele. Aceste sisteme realizează comunicarea între procesoare printr-o zonă comună de memorie. Sistemele concurente care constau din mai multe calculatoare conectate printr-o rețea se numesc sisteme distribuite.
Vom preciza câteva dintre avantajele și dezavantajele pe care le oferă sistemele distribuite comparativ cu sistemele paralele.
Avantaje :
Divizarea resurselor : de exemplu un procesor poate fi partajat de mai multe aplicații.
Divizarea datelor : sistemele de baze de date distribuite se definesc ca o colecție de baze de date corelate logic, fiecare bază fiind asociată unui nod al rețelei, împreună cu un mecanism de acces care face această colecție transparentă pentru utilizator. Sistemele distribuite au un comportament similar.
Structura geografică: unele aplicații sunt în sine distribuite geografic.
Simplitate logică : programele distribuite sunt mult mai simple.
Fiabilitate : defectarea unui calculator nu afectează hotărâtor sistemul global.
Modularitatea : destul de ușor pot fi adăugate sau șterse noi procesoare.
Costuri scăzute: rațiunile economice nu pot fi neglijate.
Dezavantaje:
Comunicații greoaie : în special în cazul în care un procesor trebuie să transmită o valoare tuturor celorlalte procesoare.
– Sincronizare greoaie : se folosesc mesajele.
Capitolul 1. Conceptul de timp
§1.1. Introducere
O utilizare importantă a conceptului de timp este aceea de ordonare a evenimentelor. Vom spune că evenimentul apare înaintea evenimentului dacă momentul fizic în care are loc, t, este mai mic decât t, momentul în care se produce. Aceste cereri de acces, ordonate, sunt utilizate la niște mecanisme de ceas care pot înregistra t și t.
Multe aplicații utilizează relații de cauză și efect. Observăm că dacă e este cauza lui f, atunci e trebuie să apară înaintea lui f. Deci, relația de precedență cauzală este o submulțime a relației de “apariție înainte”. Vom construi mecanisme menite să furnizeze informații despre relația cauzală.
Precedența cauzală este o relație mult mai uzitată decât relația de “apare înainte”. O rațiune importantă este că ne interesează de regulă corectitudinea distribuirii programului pe procesoare. Aceasta implică că dacă f apare după e într-o execuție, atunci în afară de e cauzează f, f apare posibil înainte de e în diferite execuții. Astfel relația de precedență cauzală este independentă de viteza de execuție, în timp ce relația de “apariție înainte” nu. Menționăm că vom folosi un singur ceas care să furnizeze ordinea evenimentelor.
§1.2. Modelarea sistemelor distribuite
Vom numi proces un program secvențial în curs de executare, drept urmare, la fiecare moment de timp este executată cel mult o instrucțiune a sa. Un proces include, pe lângă codul programului, o stivă conținând date temporare (parametrii ai procedurilor, adrese de revenire, variabile locale sau temporare) și o secțiune de date, conținând variabile globale. Subliniem că programul în sine nu este un proces: un program este o entitate pasivă (de exemplu conținutul unui fișier de pe disc), în timp ce procesul este o entitate activă, prevăzută cu un indicator care specifică următoarea instrucțiune de executat. Două procese asociate aceluiași program constituie două fire de executare distincte.
Vom numi program concurent un program care creează mai multe procese care se execută într-un paralelism abstract, adică nu neapărat pe procesoare distincte. În permanență trebuie însă gândit ca și când fiecărui proces îi este asociat în mod univoc un procesor fizic; desigur că și implementarea trebuie gândită astfel încât să permită acest lucru.
Aproape întotdeauna, executarea concurentă a proceselor impune o anumită cooperare între ele, deci sunt necesare anumite mecanisme care să asigure comunicarea și sincronizarea între procese. Atenția principală este îndreptată deci asupra modalităților în care pot fi realizate interacțiunile dorite și mai puțin asupra a ceea ce realizează programele secvențiale în parte.
Vom considera un sistem “message – passing” slab cuplat fără memorie partajată sau ceas partajat. Un program distribuit constă dintr-o mulțime de n procese, notată {P1, … , Pn} ce comunică între ele numai via mesaje asincrone. Nu vom presupune nimic despre ordinea sau corectitudinea mesajelor.
La un nivel foarte abstract, execuția unui sistem distribuit poate fi definită ca o mulțime de evenimente. Leslie Lamport a fost primul care a recunoscut importanța relației de ordine dintre evenimente într-un sistem distribuit. El a postulat că această relație, pe care o numește “se întâmplă înainte”, este ireflexibilă și tranzitivă. Vom numi această relație de precedență cauzală.
Ne preocupă o singură rulare r a programului distribuit. Fiecare proces Pi în această rulare generează execuția si 0,ei 0, si 1,ei 1, … , ei l-1,si l care este o secvență finită de stări locale și evenimente în procesul Pi. Starea corespunde valorilor tuturor variabilelor procesului. Mulțimea variabilelor include program counter-ul. Astfel, cu excepția nedeterminismului intern, evenimentul ce urmează a se executa este complet determinat de stare și de mesajul recepționat.
O rulare r este un vector de evoluții cu r[i] evoluția procesului Pi. Vom defini relația de precedență locală, notată cu <im, între stări în evoluția unui singur proces Pi ca: s <im t ddc s este imediat precedent lui t în evoluția r[i]. Cu alte cuvinte: next s = t sau prev t = s de câte ori s<imt. Vom utiliza < pentru închiderea reflexivă și tranzitivă a relației <im. Similar vom defini pentru evenimente. Vom nota s.p procesul în al cărui evoluție apare s. Vom spune că evenimentul e din evoluția r[i] precede slab evenimentul f din evoluția r[j] dacă e este expeditorul mesajului și f este destinatarul acestui mesaj. Aceasta este notat e~~f. Similar stările s și t din evoluțiile r[i] și r[j] sunt în relația ~~ ddc mesajul este transmis din Pi după starea s și este recepționat de Pj rezultând starea t.
Acum, relația de precedență cauzală, notată , poate fi definită ca închiderea tranzitivă a uniunii <im și ~~. Adică :
St doar dacă 1. (s<imt) OR (s~~t) sau
2. n: (S~~n) AND (ut)
În terminologia diagramei timp – proces, se înțelege că există un domeniu de la starea s la starea t. Intuitiv, relația de precedență cauzală este o ordine parțială peste mulțimea de stări locale.
Vom spune că s și t sunt concurente și notăm s||t dacă avem: NOT(st) AND NOT(ts)
Fie Si secvența de stări locale din Pi și . Atunci o execuție a unui program distribuit ce constă din procesele P1, …, PN poate fi modelată cu triplul (S1,…,SN,~~). Vom numi structură deposet (mulțime parțial ordonată decompozată), furnizând (S,), o ordine parțială ce satisface următoarele două condiții naturale : prima, că nu există nici un mesaj de primit (imediat) după starea inițială sau trimis după starea finală în orice secvență Si, a doua : există cel mult un mesaj de trimis sau primit între oricare două stări consecutive. Formalizând definim stările inițială și finală. Init(i):= minSi respectiv Final(i):= max Si. Vom utiliza Init(s) sau Final(s) pentru a nota că s este stare inițială sau stare finală. Deci suntem în măsură să formulăm următoarea:
Definiția 1.1
Un deposet este un triplu (S1, … , SN, ~~) astfel încât (S,) este o ordine parțială ireflexivă care satisface :
(D1) i: NOT(u : u~~Init(i))
(D2) i : NOT(u: Final(i) ~~u)
(D3) S<imt implica |{ u : S~~u OR u ~~t}|1
Vom utiliza deposet-ul ca model formal al execuției programelor distribuite.
Ne propunem să specificăm și să verificăm programe, descriind o metodă bazată pe structura deposet. Pașii metodei sunt :
Programul este specificat utilizând relațiile S<imt și s~~t. Orice poset care satisface această relație este valid pentru program.
Proprietățiile dorite ale programului sunt specificate utilizând , -/ și alte astfel de relații. Este important să notăm conceptele de timp, conceptul de timp global și de stare globală sunt evitate în această abordare, orice variabilă are un unic înțeles într-o stare locală. Astfel, s.v reprezintă valoarea variabilei v în starea s.
Proprietățile dorite sunt deduse utilizând proprietăți ale programului.
Pentru orice pereche de stări consecutive, s<imt, exact un eveniment apare între s și t. Există trei tipuri de evenimente: interne, de trimitere și de recepție, notate : init, snd și rcv.
(s, snd(n),t) := s<imt AND s ~~ n
(s, rcv(n),t) := s<imt AND u~~t
(s, snd, t) := (u: (s, snd(u), t))
(s, rcv, t) := (u: (u, rcv(u), t))
(s, init, t) := s<imt AND NOT(s,snd,t) AND NOT (s,rcv,t)
Un ceas logic C este o funcție definită pe s și cu valori în mulțimea numerelor naturale N, cu următoarele constrângerii :
s,tS: s<imt OR s~~t implică C(s) < C(t).
Notăm cu C mulțimea tuturor ceasurilor logice care satisfac constrângerea de mai sus.
Interpretarea lui C(s), pentru sS, este că procesul s.p intră în starea s când valoarea ceasului este C(s). Astfel, constrângerile pentru ceasurile logice modelează execuția secvențială naturală a oricărui proces și cerințele fizice că orice mesaj transmis să fie recepționat într-un timp nenul. Folosind definiția , această constrângere este echivalenta cu:
s,tS : st implică CC: C(s)<C(t) (CC)
N-am arătat, încă, că C este o mulțime nevidă. Rularea se presupune că este generată de execuția fizică, asignarea timpului fizic fiecărei stări derivă prin posibilitățile ceasului logic. Proprietatea “C este nevidă” este echivalentă cu condiția ca să fie ordine parțială ireflexivă.
Lema 1.1
C este nevidă doar dacă (S, ) este ordină parțială ireflexivă.
Demonstrație:
“implicația directă” suficient să demonstrăm ireflexivitatea
fie DC implică NOT(ss) altfel D(s) < D(s)
“implicația inversă” vom defini D:S->N, D(s) = lung (s0, s1, … , sn)
unde s0 = Init (i), sn=s, sk sk+1 k{0, … , n-1}
Vom presupune de acum înainte că (S,) este o ordine parțială, sau echivalentul că C este o mulțime nevidă. Ne propunem să arătăm că mulțimea C satisface de asemenea reciproca relației (CC), adică :
s,tS : not(st) implică CC : NOT(C(s)<C(t))
În final este suficient să arătăm că :
u,vS: u||v implică CC : (C(u) = C(v))
Aceasta se interpretează că dacă stările locale sunt concurente atunci există un ceas logic care să aibe aceeași valoare pentru ambele stări în cauză. Vom arăta acest rezultat pentru o submulțime oarecare X a lui S care conține doar perechi de stări concurente.
Lema 1.2
Pentru orice XS,
(u,vX: u||v) implică cC : u,vX : c(u) = c(v)
Demonstrație:
Fie C, deci există DC
Presupunem că u,vX, u||v și D(u)D(v)
Altfel nu avem ce demonstra
Vom construi un alt ceas logic C astfel:
(L1): pentru sX: C(s):=
(L2): pentru sS – X astfel încât NOT uX:u->s
definim C(s):=D(s)
(L3) pentru stările neanalizate :
C(s) = D(s) + max { C(u) – D(u) | u s}
Ne propunem să arătăm că C satisface condiția (CC) fie st, deoarece D satisface (CC) avem : D(s) < D(t).
Cazul 1: sX
Deoarece X constă doar din perechi de stări concurente : tX conform (L3):
C(t) D(t) + C(s) – D(s)
D(s) < D(t) deci C(t) > C(s)
Cazul 2: sS – X și uX : u s
st de unde D(s) < D(t)
xS : D(x) C(x) deci C(s) < C(t)
Cazul 3 : sS – X și nX: us
Conform (L3) : C(s) = D (s) + max{ C(u) – D(u)/ us}
us AND ut de unde ut
D(s) < D(t) deci C(s)<D(t) + max{ C(u) – D(u) / us}
Deci C(s)<D(t) + max{ C(u) – D(u) / ut}
Conform (L3) : C(t) = D(t) + max{ C(u) – D(u)/ ut}
Deci C(s) < C(t)
Și s-a arătat că C satisface (CC)
Combinând lema anterioară cu condiția (CC) obținem următoarea caracterizare a relației :
s,tS : st CC : C(s) < C(t)
În continuare descriem un algoritm ce implementează un astfel de ceas logic. Notăm cu s.c. valoarea ceasului c în starea s.
Pentru orice stare inițială s:
Integer s.c = 0
în cazul transmiterii unui mesaj (s, snd, t):
/* s.c este transmis și el în mesaj */
t.c := s.c + 1;
în cazul recepționării unui mesaj (s, rcv(u), t)
t.c := max(s.c, u.c) + 1
în cazul unui eveniment intern (s, int, t)
t.c := s.c + 1
Este foarte ușor de verificat :
s,tS : st implica s.c < t.c
Pentru orice stare s, vom nota cu s.p procesul căruia îi aparține și vom putea construi o ordine totală :
(e.c, e.p) < (f.c, f.p) (e.c < f.c) OR (e.c = f.c) AND (e.p < f.p))
Ne propunem să descriem un mecanism numit ceas vector și care satisface :
st s.v < t.v
Definim următoarea relație de ordine dintre vectori :
x<y = (k : 1 k N : x[k] y[k]) AND
(j : 1 j N : x[j] < y[j]).
xy = (x<y) OR (x=y)
Prezentăm prima versiune a unui algoritm care implementează un astfel de mecanism :
Pentru orice stare inițială s :
(i: is.p : s.v[i] = 0) AND (s.v[s.p] = 1)
în cazul transmiterii unui mesaj (s,snd,t):
t.v := s.v;
t.v[t.p] ++;
în cazul recepționării unui mesaj (s, rcv(u), t):
for i:=1 to N do
t.v[i]:= max (s.v[i], u.v[i]);
t.v[t.p]++;
în cazul unui eveniment intern (s, int, t):
t.v := s.v;
t.v[t.p]++;
Lema 1.3
Fie st. Atunci :
Not( s t ) implică t.v[s.p] < s.v[s.p]
Demonstrație
Dacă t.p = s.p atunci t<s și este evident t.v[s.p] < s.v[s.p].
Presupunem s.p t.p.
Deoarece s.v[s.p] este ceasul local al procesului Ps.p și procesul Pt.p nu cunoaște această valoare pentru că not(st) se deduce : t.v[s.p] < s.v[s.p].
Teorema 1.1
Fie s și t stări ale proceselor Pi și Pj cărora le corespund vectorii s.v și t.v respectiv. Atunci st dacă și numai dacă s.v < t.v.
Demonstrație
(st) implica (s.v < t.v):
dacă st atunci există un drum de la s la t și ținând cont de modul de setare al ceasului la recepționarea unui mesaj sau în cazul unor evenimente interne sau de transmitere de mesaje deducem :
k : s.v[k] t.v[k]
st implică not( t s ) și conform lemei anterioare :
s.v[j] < t.v[j]
rezumând :
(k: s.v[k] t.v[k]) AND (s.v[j] <t.v[j])
deci s.v < t.v
(s.v < t.v) implică (st):
conform Lemei 1.3 : NOT (st) implică t.v[i] < s.v[i] (*)
se observă din algoritm :
(s.v[s.p] < t.v[s.p]) implica (t.v > s.v) și
(t.v > s.v) implica NOT (t.v[i] < s.v[i]) (**)
din (*) și (**) deducem :
(s.v < t.v) implica (st)
Lema 1.4
st (s.v[s.p] t.v[s.p]) AND (s.v[t.p] < t.v[t.p])
Demonstrație
Evidentă.
Vom prezenta în continuare o a doua versiune a algoritmului, în care ceasul păstrează cauzalitatea doar când cele două stări aparțin unor procese distincte :
Pentru orice stare inițială s:
For i:= 1 to N do
s.v[i] := 0;
s.v[s.p]:=1;
{(i: is.p: s.v[i] = 0) AND (s.v[s.p] = 1)}
în cazul transmiterii unui mesaj (s, rcv(u), t):
for i:= 1 to N do
t.v[i] := max(s.v[i], u.v[i]);
{(i: t.v[i] = max(s.v[i], u.v[i]))}
în cazul unui eveniment intern (s, int, t)
t.v := s.v;
{t.v = s.v}
Vom numi lanț în (S, ) o secvență de stări c0, c1,…, cn astfel încât ci<imci+1 sau ci ~~ci+1. Pentru orice lanț c=c0,c1,…, cn vom defini first(c)=c0, last(c)=cn și length(c)=n. Pentru orice pereche de stări s și t astfel încât st vom defini funcția lungime maximă, astfel :
ml(Init,t) = ( max c: first(c)=s and last(c)=t : length(c))
dacă not ( s t ) atunci ml(s,t)=-1,
notăm ml(Init,t) = (max u : Init(u) : ml(u,t)).
Deci dacă st, ml(s,t) desemnează lungimea maximă a unui lanț ce leagă s de t iar ml(Init,t) lungimea maximă a unui element ce leagă o stare inițială de t.
Din definiția lui ml rezultă :
ml (s,t) >0 (u : ml(s,u) = ml(s,t)–1 AND ml(u,t) =1)
Vom defini relația folosind inducția după . Pentru k>0,
dacă și numai dacă s t := ml(s,t) = k
Deci dacă și numai dacă s t și cel mai lung lanț dintre s și t are lungimea k.
Lema 1.5
s t (k : k>0: )
Demonstrație
s t
(folosind definiția lanțului și faptul că este închiderea tranzitivă a ~~ ):
c : first(c) = s AND last(c)=t
(folosim definiția lui ml)
k: k>0 : ml(s,t) = k.
(folosim definiția lui )
k: k>0 :
Lema 1.6
Demonstrație
(folosim definiția lui )
ml(s,t) = 1
(folosim definiția lui ml):
c: first (c) = s AND last(c) = t AND length(c) =1
(folosim definiția lanțului):
s<imt OR s~t
Lema 1.7
AND (k>1) implică (u: su AND ut)
Demonstrație
(folosim definiția lui )
ml(s,t) = k AND k > 1
(folosim proprietatea lanțului)
u: ml(s,n) = k-1 AND ml(u,t) =1
folosim definiția lui )
u: su AND ut
Pentru k0 vom defini:
s t := not ( st ) AND ml(Init,t) = k
adică s t dacă și numai dacă not( st) și cel mai lung lanț de la o stare inițială la t are lungimea k.
Lema 1.8
Not( st) (k: k0 : s t)
Demonstrație
Not( st )
(conform definiției lui ml(Init,t))
not( st ) AND ml(Init,t) 0
(conform definiției lui )
k : k 0 : st
Lema 1.9
Not( st ) dacă și numai dacă Init(t)
Demonstrație
st
(conform definiției lui )
ml(Init,t) = 0 AND not ( st , k)
(conform definiției lui ml(Init,t))
NOT(u: ut) AND not (st)
NOT(u : u t)
(conform definiției lui Init(t))
Init(t)
Lema 1.10
k>0 AND st AND u t implică (j: 0 j k: su)
Demonstrație
k>0 AND st AND u t
(altfel s t):
k>0 AND s-/-> u AND st
(conform definiției lui -/)
k>0 AND s-/-> u AND ml(Init,t) = k
(altfel ml(Init,u)>k)
k>0 AND s-/-> u AND ml(Init,t) < k
(conform definiției lui -/)
j: 0j<k : s-/u
Ne propunem să demonstrăm corectitudinea versiunii a doua a algoritmului ce implementează mecanismul ceas vector. Adică să verifică relația:
s,t : s.p t.p : s.v < t.v s t
Lema 1.11
s t implică s.v t.v
Demonstrație
Este suficient să arătăm că:
k:0 : st implică s.v t.v
Vom utiliza inducția după k:
Pasul inițial (k = 1) :
st
(conform Lemei 1.6 )
s<imt OR s~~t
(conform definițiilor relațiilor <im și ~~)
(s,init,t) OR ((s,snd,t) OR (u:(s,rcv(u),t)) OR (u:(u,rcv(s),v)
(conform comportării ceasului le Snd, Rev și Init)
(s.v=t.v)OR(s.v<t.v)OR(s.vt.v)OR(s.v t.v)
(simplificând)
s.v t.v
Pasul de inducție (k>1):
st AND (k>1)
(conform Lemei 1.7)
u : su AND ut
(aplicând ipoteza inductivă)
u: s.v u.v AND u.v t.v
(simplificând)
s.v t.v
Lema 1.12
s,t: s.pt.p : st implică t.v[s.p] < s.v[s.p]
Demonstrație
Este suficient să arătam pentru orice k0.
st AND s.pt.p implică t.v[s.p] < s.v[s.p]
vom utiliza inducție după k :
Pasul inițial (k=0).
st AND a.p t.p
(conform Lemei 1.9)
Init (t) AND s.pt.p
(fie u starea inițială din s.p)
Init(t) AND s.pt.p AND
(u: Init(u) AND u.p = s.p : u=s OR us)
(conform Lemei 1.11)
Init(t) AND s.pt.p AND
(u: Init(u) AND u.p = s.p : u.v=s.v OR u.vs.v)
(conform setării ceasului de stări inițiale)
t.v[s.p] = 0 AND
(u : u.v[s.p] = 1: u.v = s.v OR u.v s.v)
(simplificând)
t.v[s.p] < s.v[s.p]
Pasul de inducție (k>0)
st AND s.p t.p AND k >0
(fie u ce satisface u<imt, un astfel de u există deoarece avem NOT Init(t))
st AND s.p t.p AND u.ps.p AND u<imt
(conform Lemei 1.10)
j: su AND 0 j<k AND u.p s.pAND u<imt
(aplicăm ipoteza inductivă)
u.v[s.p] < s.v[s.p] AND u<imt
(conform definiției <im)
u.v[s.p] < s.v[s.p] AND ((u,init,t) AND (u,snd,t) AND (u,rcv (w),t))
Vom trata fiecare disjuncție separat:
Cazul 1: (u,int,t)
u.v[s.p] < s.v[s.p] AND (u,int,t)
(conform setării ceasului de evenimente interne )
u.v[s.p] < s.v[s.p] AND t.v=u.v
(simplificând)
t.v[s.p] < s.v[s.p]
Cazul 2: (u,snd,t)
u.v[s.p]< s.v[s.p] AND (u,snd,t)
(ținând cont că s.p t.p)
u.v[s.p]< s.v[s.p] AND t.v[s.p]=u.v[s.p]
(simplificând)
t.v[s.p]<s.v[s.p]
Cazul 3: (u,rcv(w),t)
u.v[s.p]< s.v[s.p] AND (u,rcv(w),t)
(conform setării ceasului la Rcv )
u.v[s.p] < s.v[s.p] AND
(t.v[s.p]=u.v[s.p] OR t.v[s.p]=w.v[s.p])
(simplificând)
t.v[s.p] < s.v[s.p] OR ((u,rcv(w),t) AND t.v[s.p]=w.v[s.p])
Pentru cazul 3 vom trata următoarele două subcazuri :
Cazul 3A: w.p = s.p
t.v[s.p] = w.v[s.p] AND (u,rcv(w),t) AND w.p=s.p
(fie x ce satisface w<imx, x există deoarece w~~t implică NOT Final(w))
t.v[s.p] = w.v[s.p] AND (u,snd,t) AND w.p=s.p
(altfel st)
t.v[s.p]=w.v[s.p]AND (u,snd,t) AND w.p=s.p AND ws
(deoarece w<imx)
t.v[s.p]=w.v[s.p]AND (u,snd,t) AND w.p=s.p AND (xs OR x=s)
(conform setării ceasului la snd)
t.v[s.p]=w.v[s.p]AND(w.v[s.p]< x.v[s.p])AND(xsOR x=s)
(conform lemei 1.11)
t.v[s.p]=w.v[s.p] AND (w.v[s.p]< x.v[s.p]) AND x.v s.v
(simplificând)
t.v[s.p]<s.v[s.p]
Cazul 3B : w.ps.p
t.v[s.p] = w.v[s.p] AND (u,rcv(w),t) AND w.p s.p
(utilizând st, k > 0 și Lema 1.10)
t.v[s.p] = w.v[s.p] AND w.v s.p AND sw AND 0j<k
(folosind ipoteza inductivă)
t.v[s.p] = w.v[s.p] AND w.v[s.p] < s.v[s.p]
(simplificând)
t.v[s.p] < s.v[s.p]
Lema 1.13
s,t> s.p t.p : st implică s.v < t.v
Demonstrație
Este suficient să arătăm că pentru orice k > 0:
st AND s.p t.p implică s.v < t.v
vom utiliza inducția după k.
Pasul inițial (k=1):
st AND s.p t.p
(conform definiției lui și Lemei 1.6)
s~~t AND s.p t.p
(fie u satisfăcând u<imt)
s.p u.p AND (u,rcv(s),t)
(altfel st, deoarece există un singur eveniment între u și t)
us AND s.p u.p AND (u,rcv(s),t)
(conform Lemei 1.12 și Rcv)
s.v[u.p] < u.v[u.p] AND (i : t.v[i] = max (u.v[i], s.v[i]))
s.v < t.v
Pasul de inducție :
st AND k >0 AND s.p t.p
(conform Lemei 1.7)
n: (su AND ut AND s.p t.p
(u.p nu poate avea două valori)
n: (su AND ut AND (u.p t.p OR u.p s.p)
(n: (su AND ut AND u.p t.p) OR (su AND ut AND u.p s.p))
(folosind ipoteza inductivă)
n: (su AND u.v < t.v) OR (ut AND s.v < u.v)
(conform Lemei 1.11)
n: (s.v u.v AND u.v < t.v) OR (s.v < u.v AND u.v t.v)
s.v < t.v
În continuare vom descrie un algoritm pentru ceas foarte folosit în aplicații de sisteme distribuite:
Pentru orice stare inițială s:
(i : is.p : s.v[i] = 0) AND (s.v [s.p] = 1)
Pentru orice eveniment de transmisie (s, snd, t) sau eveniment intern (s, int, t):
t.v[t.p] := s.v[t.p] +1;
Pentru orice eveniment de recepție (s, rcv(u), t) :
t.v[t.p] := max(s.v[t.p], u.v[u.p]) + 1;
t.v[u.p] := max(u.v[u.p], s.v[u.p]);
Următoarele două leme se referă la algoritmul descris mai sus:
Lema 1.14
st implică s.v[s.p] < t.v[t.p]
Demonstrație
Este suficient să arătăm că pentru orice k > 0 :
st implică s.v[s.p] < t.v[t.p]
Vom utiliza inducția după k:
Pasul inițial (k=1):
st
(folosind Lema 1.6)
s<imt OR s~~t
(conform definirii <im și ~~)
(s,int,t) OR (s,snd,t) OR (u : (s,rcv(u),t)) OR (u: (u,rcv(s),t))
(folosind modul de steare al ceasului pentru evenimentele de tip snd, rcv și int)
s.v[s.p] < t.v[t.p]
Pasul de inducție (k > 1):
st AND (k > 1)
(conform )
u: su AND ut
(conform ipotezei inductive)
u: s.v[s.p] < u.v[u.p] AND u.v[u.p] < t.v[t.p]
(simplificând)
s.v[s.p] < t.v[t.p]
Vom defini relația de precedență directă (notată d) ca o submulțime a relației astfel:
sdt s < t OR q,r: s q AND q~~r AND r t
Teorema 1.3
s,t: s.p t.p : (sd t) (s.v[sp] t.v[s.p])
Demonstrație
Implicația directă este evidentă, vom arăta implicația inversă, vom folosi inducția după rank(k) unde :
rank (t) = |{q | q < t}|
Adică : rank(t) este numărul de stări locale care precede t.
Pasul inițial (k=0)
rank(t) = 0
(conform definiției noțiunii rank)
Init(t)
(fie u starea inițială în s.p)
Init (t) AND u: Init(u) AND u.p =s.p : u=s OR us
(conform Lemei 1.14)
Init(t) AND u: Init(u) AND u.p = s.p: u.v = s.v OR u.v[u.p] < s.v[u.p]
(conform setării ceasului în stările inițiale)
t.v[s.p] = 0 AND u> u.v[s.p] = 1: u.v[s.p] s.v[s.p]
(simplificând)
NOT(s.v[s.p] t.v[s.p])
Pasul de inducție (k>0)
sdt AND k>0
(fie u care satisface u<imt, u există deoarece k=rank(t) > 0)
sdt AND u<imt
(sdu implică sdt)
sdu AND rank(u)<k AND u<imt
(folosind ipoteza inductivă)
NOT(s.v[s.p] u.v[s.p]) AND u<imt
(folosind definiția lui <im)
NOT(s.v[s.p] u.v[s.p]) AND ((u,int,t) OR (u,snd,t) OR (u,rcv(w),t))
Vom considera fiecare caz în parte :
Cazul 1: (u,int,t) OR (u,snd,t)
(s.v[s.p] >u.v[s.p]) AND ((u,int,t) OR (u,snd,t))
(folosind definiția pentru Int și Snd)
(s.v[s.p] > u.v[s.p]) AND t.v[s.p] = u.v[s.p]
simplificând
(s.v[s.p] > t.v[s.p])
Cazul 2: (u,rcv(w),t), w.p = s.p
sdt, s.p = w.p, w~~t
(s<w sau s=w implică sdt)
w<s
(folosind algoritmul)
w.v[s.p] < s.v[s.p]
(folosind definiția pentru rcv)
(s.v[s.p] > w.v[s.p]) AND ((w.v[s.p] = t.v[s.p])OR (u.v[s.p]=t.v[s.p]))
deoarece s.v[s.p] > u.v[s.p]
s.v[s.p] > t.v[s.p]
Cazul 3: (u, rcv(w), t), w.p s.p
(s.v[a.p] > u.v[s.p]) AND (u,rcv(w),t) AND w.p s.p
(folosind definiția Rcv)
(s.v[a.p] > u.v[s.p]) AND t.v[s.p] = u.v[s.p]
(simplificând)
s.v[s.p] > t.v[s.p]
Corolar 1.1
s,t: s.pt.p : s-/->t implică NOT(s.v[s.p] > t.v[s.p])
Demonstrație
Este evidentă, se folosește :
s-/->t implică s-/->dt
Prin intervalul de stări înțelegem o secvență de stări dintre două evenimente externe. Formal al n-lea interval din Pi (notat cu (i,u) este un sublanț al lui (si,) între al n-1-lea și al n-lea eveniment extern. Dacă se dă intervalul ml, notat .
Funcțiile predecesor și succesor sunt definite pentru orice uS și 0 i N
Pred. u.i = (max v: vSi AND vu: v)
Succ. u.i = (min v: vSi AND uv: v)
Considerând o stare i în Sj, notat pred i.j este ultima stare din Sj care precede cauzal pe i.
Ne propunem să prezentăm un algoritm pentru ceas matrice.
Prin notăm valoarea ceasului matrice în intervalul (k,n):
Pentru orice stare inițială s:
(i,j: is.p AND js.p: s.v[i,j]=0) AND (s.v[s.p,s.p]=1)
Pentru orice eveniment de transmitere (s, snd,t):
t.v[t.p,t.p]:=s.v[s.p,s.p] + 1
Pentru orice eveniment de recepție (s, rcv(u), t):
t.v:=max(s.v, u.v);
t.v[t.p,]:=max(s.v[s.p,], u.v[u.p,]);
t.v[t.p,t.p]++;
Al k-lea element de pe diagonala, [k,k], reprezintă un număr de interval al procesului Pk. Astfel pentru orice interval (k,n) avem: [k,k] = n. Linia k al matricii este echivalentă cu ceasul vector tradițional. Deoarece ceasul vector implementează funcția pred, linia k a matricii poate utilizată în gasirea predecesorului intervalului (k,n)=(k, [k,k]) după cum urmează predecesorul lui (k,[k,k]) este în procesul j intervalul (j, [k,j]). De fapt, această regulă este valabilă pentru toate liniile : predecesorul lui (i, [i,i]) din procesul j este intervalul (j,[i,j]). Mai mult, linia k din este egală cu diagonala lui . Astfel putem utiliza linia k pentru a găsi pred. (k,n)j pentru jk și atunci utilizăm linia j pentru a găsi pred.(pred.(k,n)j)i pentru ij.
Lema 1.15
(M1) [k,k] = n
(M2) ij implică (j, [i,j])=pred(i, [i,i]).j
(M3) [i,i]= [k,i]
Demonstrație
Toate relațiile le vom demonstra prin inducție. Pentru pasul inițial vom considera n=1 și prin urmare (k,n) va fi intervalul inițial al procesului k. Inducția se va aplica după n>1.
(M1): Pasul inițial (n=1).
Valoarea inițială a lui [k,k] este 1.
Pasul de inducție (n>1):
Vom presupune [k,k] = n și arătăm că [k,k]=n+1. Procesul Pk intră în intervalul (k,n+1) doar după transmiterea sau recepționarea unui mesaj. Conform algoritmului în acest caz al k-lea element diagonal se incrementează. Astfel:
[k,k]= [k,k]+1=n+1
(M2): Pasul inițial (n=1):
Deoarece n=1, este valoarea inițială a ceasului matrice în Pk. Astfel, ij implică [i,j]=0 și (j,[i,j])=(j,0)=.
Vom arăta ca pred.(i, [i,i]).j = . Presupunem ik, atunci prin valoarea inițială a lui , cunoaștem:
(i, [i,i]) = (i,0)
vom calcula :
pred.(i, [i,i]).j = pred(i,0).j =
Acum presupunem i=k, în acest caz avem :
(i, [i,i]) = (i,1)
Deoarece nici un interval nu precede (i,1) avem :
pred(i,1).j = .
Pasul de inducție (n>1):
Presupunem că am verificat afirmația pentru (k,n) și toate intervalele anterioare acestuia.
Presupunem că evenimentul din (k,n+1) este transmiterea unui mesaj, atunci [k,k] = [k,k] cu excepția :
[k,k] = [k,k] + 1
Deoarece evenimentul este transmiterea unui masaj, (k,n) și (k,n+1) au exact aceiași predecesori. Astfel pred.(i,[i,i]).j este egal cu pred.(i,[i,j]).j care datorită ipotezei inductive este egal cu (j,[i,j]) deoarece ij și doar elementul [k,k] se schimbă.
Presupunem că evenimentul din (k,n+1) este recepționarea unui mesaj cu ceasul matrice W. din ipoteza de inducție, W satisface M2. Menționăm de asemenea că m2 creează probleme unei singure linii ai lui M.
Deoarece toate liniile ik din sunt fie copiate din W fie neschimbate. Relația M2 este satisfăcută de toate aceste linii din . Predecesorul lui (k,n+1) al lui Pj este maximul dintre [k,j] și [j,j]. Aceasta este exact valoarea asigurată la [k,j]. Astfel :
(k,[k,j]) = pred(k,[k,k]).j
și M2 este satisfăcută de toate liniile lui .
(M3): Pasul inițial (n=1)
Relația are loc conform inițializării matricii M.
Pasul de inducție (n>1):
Presupunem diag() = [k,], vom arăta :
diag() = [k,]
Procesul Pk intră în intervalul (k,n+1) doar după transmiterea sau recepționarea unui mesaj. În cazul transmiterii, [k,k] este incrementat, astfel diagonala se păsrează egală cu linia k.
În cazul recepționării :
Pentru ik : [k,i] = max{ W[Wp,i], [k,i]}
[i,i] = max{ W[i,i], [k,i]}
unde w.p reprezintă procesul care a transmis masajul aplicând ipoteza inductivă. diag(W) = W[W.p,] și diag()=[k,] rezultă [k,i]= [i,i] pentru i=k raționăm similar.
Capitolul 2. Excluderea mutuală
§2.1. Problematica
Fie un sistem constând într-un număr fixat de procese și dintr-o resursă partajată numită resursa critică.
Un algoritm de coordonare a accesului de secțiunea critică trebuie să satisfacă următoarele condiții :
Safety (siguranță): două procese nu pot avea permisiunea să utilizeze secțiunea critică simultan.
Liveness ( vitalitate ): orice cerere pentru secțiunea critică este eventual garantată.
Fairness (onestitate): diferitele cereri trebuiesc satisfăcute în ordinea în care au fost făcute.
Vom lucra în ipoteza că toate canalele sunt FIFO:
s<t AND s~~u AND t~~v implică NOT(v<n)
Vom introduce pentru orice s predicatele req(s) și cs(s):
cs(s) este adevărată dacă și numai dacă procesul Ps.p are permisiunea de a intra în secțiunea critică .
req(s) este adevărată dacă și numai dacă procesul Ps.p are o cerere de a intra în secțiunea critică.
Atât cs cât și req sunt false în starea inițială.
Presupunem stările t<u<v astfel încât: cererea da a intra în secțiunea critică se face în starea t, permisiunea este obținută în u și realizată în v.
Atunci req(s) este adevărată pentru toate stările s astfel încât: t s v și cs(s) este adevărată pentru u s v.
Vom presupune îndeplinită condiția de cooperare:
cs(s) implică (t: s<t: NOT req(t))
Condițiile de siguranță respectiv de vitalitate pot fi formalizate astfel:
s||t implică NOT (cs(s) AND cs(t))
req(s) implică (t: s < t AND cs(t))
Prima stare locală ulterioară lui s, în care procesul Ps.p are permisiunea de a acccesa secțiunea critică o vom nota prin next_cs(s):
next_cs := min {t | s<t AND cs(t)}
Definim că req_start(s) este adevărată dacă și numai dacă procesul Ps.p face pentru prima dată o cerere de a accesa secțiunea critică în starea s, formal:
req_start(s):= req(s) AND NOT req(prev.s)
Cu aceste noțiuni introduse putem formaliza condiția de onestitate:
(req_start(s) AND req_start(t) AND st) implică next_cs(s) next_cs(t)
Menționăm că next_cs(s) și next_cs(t) există datorită condiției de vitalitate. Mai mult, next_cs(s) și next_cs(t) nu sunt concurente datorită condiției de siguranță.
next_cs(s) next_cs(t) este echivalentă cu NOT(next_cs(t) next_cs(s))
§ 2.2. Algoritmul lui Lamport
Pentru început vom prezenta algoritmul pentru vectori activi:
Pi::
Var q: array [1..n] of elem initially (c, …, c)
(s,event,t):
if t.q[i] s.q[i] tehn
for j: ji do
send(t.q[i]) to Pj as “update” message (s,receive(“update”, n), t):
t.q[u.p] = u.q[u.p]
Vom defini predicatul msg(s,t) după cum urmează:
msg(s,t) q,r: q<s : q~~r AND t<r
ceea ce înseamnă că există un mesaj transmis înainte de s și recepționat după t.
Lema 2.1
În ipoteza FIFO avem:
s,t: s.pt.p : s-/dt AND NOT msg(s,t) implică t.q[s.p]=s.q[s.p]
Demonstrație
Vom defini inducția după k=rangul lui t (numărul de stări ce precede t).
Pasul inițial : (k=0) Init(t)
Dacă Init(s) atunci evident.
Dacă not Init(s) atunci fie u= starea inițială a procesului s.p. Deoarece avem NOT msg(s,t) și t este stare inițială atunci s.q[s.p]=u.q[s.p], deci t.q[s.p] = s.q[s.p].
Pasul de inducție (k>0):
Fie u=prev. t. Dacă event(u)receive atunci NOT msg(s,t) implică NOT msg(s,n). Utilizând ipoteza inductivă avem:
u.q[s.p] = s.q[s.p] și conform algoritmului t.q[s.p]=u.q[s.p]
Acum presupunem event(u)=receive(w).
Dacă w.ps.p ne încadrăm în cazul analizat mai sus.
Deci fie w.p=s.p. deoarece s-/d t avem: w<s.
Fie w’=next.w, conform algoritmului w’.q[s.p] = t.q[s.p]
Vom arăta că s.q[s.p] = w’.q[s.p] din care rezultă imediat ceea ce dorim să demonstrăm. Dacă s.q[s.p]w’.q[s.p] atunci aceasta implică transmiterea unui mesaj, acest mesaj nu poate fi recepționat înainte de t deoarece ar incălca ipoteza FIFO, dar nici după t pentru că ar viola NOT msg(s,t). Prin urmare un astfel de mesaj nu există deci:
s.q[s.p]= w’.q[s.p]
În continuare vom prezenta algoritmul Lamport pentru excluderea mutuală:
Pi::
Var v:ddclock /* ceasul sistemului*/
q: vector activ, vector de întregi având valoarea inițială ss.
(s, request,t)
t.q[i] := s.v[i];
(s,receive(u),t):
if event(u) = request then
send ack to u.p
(s, release, t)
t.q[i] :=
Interpretările vectorilor v și q sunt:
s.q[j] : momentul când Pj face cerere de intrare în secțiunea critică
s.v[j] : dacă ji atunci: momentul când s-a primit ultimul mesaj de la Pj
altfel: valoarea ceasului logic în starea s.
Folosind ordonarea lexicografică putem formaliza:
Req(s) s.q[s.p]
cs(s) (j> js.p : (s.q[s.p], s.p) < (s.v[j],j) AND
(s.q[s.p],s.p) < (s.q[j],j))
Pentru simplificarea noțiunilor vom scrie s.q[s.p]<s.v[j] în loc de (s.q[s.pș, s.p) < (s.v[j], j).
Următoarea Lemă este foarte importantă în demonstrarea proprietății de siguranță.
Lema 2.2
s,t: s.pt.p: s-/->t AND s.q[s.p] < t.v[s.p] implică t.q[s.p]=s.q[s.p]
Demonstrație
Folosind Lema 2.1 este suficient să arătăm că NOTmsg(s,t) fie u< s astfel încât u.v[s.p] = s.q[s.p].
Presupunem că mesajul transmis în starea u este recepționat de procesul t.p în starea w.
Conform mecanismului descris nu există un alt request ori release transmis între stările u și s. (1)
u.v[u.p] = s.q[s.p] și s.q[s.p] < t.v[s.p]
deci u.v[u.p] < t.v[u.p] și conform Teoremei 1.3 avem udt și aplicând ipoteza FIFO deducem wt conform FIFO și a faptului că mesajul transmis din starea u este recepționat înainte de t deducem: NOT msg(s,t) (2)
conform (1) și (2) avem NOTmsg(s,t)
Următoarele teoreme dovedesc că algoritmul satisface proprietățile de siguranță, de vitalitate și onestitate.
Teorema 2.1 (siguranță)
s.p t.p AND s||t implică NOT(cs(s) AND cs(t))
Demonstrație
Vom arăta că (s||t) AND cs(s) AND cs(t) implică fals.
Cazul 1: t.v[s.p] < s.q[s.p] AND s.v[t.p] < t.q[t.p]
s.q[s.p]
< (deoarece cs(s) AND s.p t.p)
s.v[t.p]
< (în acest caz)
t.q[t.p]
< (deoarece cs(t) AND s.pt.p)
t.v[s.p]
< (în acest caz)
s.q[s.p]
Cazul 2 : s.q[s.p] < t.v[s.p] AND s.v[t.p] > t.q[t.p]
s.q[s.p]
< (deoarece cs(s) AND s.p t.p)
s.q[t.p]
= (datorita : t.q[t.p] < s.v[t.p], t-/-> s, Lema 2.2)
t.q[t.p]
< (deoarece cs(t) AND s.pt.p)
t.q[s.p]
= (datorita : t.q[t.p] > s.v[t.p], s-/-> t, Lema 2.2)
s.q[s.p]
Cazul 3: s.q[s.p] < t.v[s.p] AND s.v[t.p] < t.q[t.p]
s.q[s.p]
< (deoarece cs(s) AND s.p t.p)
s.v[t.p]
= (în acest caz)
t.q[t.p]
< (deoarece cs(t) AND s.pt.p)
t.q[t.p]
= (deoarece cs(t) AND s.p t.p)
t.q[s.p]
= (datoriă s.q[s.p] < t.v[s.p], s-/->, Lema 2.2)
s.q[s.p]
Cazul 4: t.v[s.p] < s.q[s.p] AND t.q[t.p] < s.v[t.p]
Se tratează similar cazului anterior.
Teorema 2.2 (vitalitate)
req(s) implică t : s <t AND cs(t)
Demonstrație
req(s) s.p[s.p]
s.q[s.p] implică existența unei stări s1 în procesul s.p astfel încât :
s1.v[s.p] = s.q[s.p] AND event(s1) = request
Vom arăta existența unei stări t ce satisface următoarele condiții:
C1 : t1: js.p: t1.v[j] > s.q.[s.p] AND s.q[s.p]=t1.q[s.p]
C2 : t1: js.p: t2.v[j] > s.q.[s.p] AND s.q[s.p]=t2.q[s.p]
Vom alege t = max(t1,t2) și vom arăta că are loc cs(t). Condiția C1 este îndeplinită datorită confirmărilor mesajelor transmise de starea s1:
j: js.p: wjPj: s1~~wj
j: js.p: ujPj: s1~~uj
t1:= max j: js.p : uj
Pentru a demonstra condiția C2 vom defini pentru orice u:
ureq(u) = |{k|u.q[k] < u.q[u.p]}|
Dacă ureq(t1)=0 atunci s.q[s.p] este minimul din t1.q și prin urmare are loc cs(t1)
Vom folosi inducția: presupunem că s-a verificat pentru
ureq(t1) = k, k0
și vom verifica pentru ureq(t1)=k+1
vom presupune că minimul vectorului t1.q se realizează pe componenta j.
fie u starea procesului j pentru care avem: u.v[j] = t1.q[j]
cazul 1: ureq(u) = 0
Conform celor analizate mai sus, procesul j primește permisiunea să treacă prin secțiunea critică, execută release și deci există t astfel încât :
t1 < t și ureq(t) = k
după care se aplică ipoteza inductivă.
Cazul 2 : ureq(u)0.
Subcazul 2.1: toate procesele care au executat request înainte de u au trecut prin secțiunea critică în cele din urmă.
Deci există u’ astfel încât :
u < u’ și ureq(u) = 0
și ne-am redus la cazul 1.
Subcazul 2.2: există un proces (fie acesta m) care a executat request înainte de u și nu i se permite să intre în secțiunea critică.
Avem :
u.q[m] < u.p[u.p] < s.p[s.p]
deoarece s.q[s.p] < t1.v[m] și ținând cont de FIFO:
t1.q[m] = u.q[m]
deci t1.q[m] < u.p[u.p] = t1.q[u.p]
ceea ce contrazice alegerea procesului j, deci acest subcaz nu va avea loc.
Teorema 2.3 (“de onestitate”)
(req_start(s) AND req_start(t) AND st) implică
(next_cs(s) next_cs(t))
Demonstrație
Fie s’=next_cs(s) starea în care procesul s.p accesează secțiunea critică și s’’ starea în care execută release.
Fir t’=next_cs(T) și r starea în care procesul t.p recepționează mesajul transmis de s.
Sunt adevărate următoarele fapte:
rt, datorită condiției FIFO pentru canalele de comunicație
t.v[t.p] = t.q[t.p], datorită evenimentului request se la starea t
s.v[s.p] < t.v[t.p], deoarece st
s.q[s.p] = s.v[s.p], datorită request-ului în starea s
r.q[s.p] = s.q[s.p], datorită recepționării request-ului în starea r.
r.q[s.p] < t.q[t.p], din 2,3,4,5
t.q[t.p] = t’.q[t.p], conform definiției lui t’
t’.q[t.p] < t’.q[s.p], deoarece cs(t’)
r.q[s.p] < t’.q[t.p] < t’.q[s.p] din 6,7,8.
Aceasta înseamnă că q[s.p] trebuie să crească între r și t’.
Acest lucru nu se poate întâmpla decât dacă procesul t.p recepționează un mesaj release trimis din s’’. astfel s’’ t’, și deoarece s’s’’ tragem concluzia că: s’t’
§2.3. Algoritmul lui Ricart și Agrawala
Acest algoritm folosește două tipuri principale de mesaje: request și ack, de asemenea sunt păstrate vectorii v (ddclock) și q (vector activ).
Pi::
var v.ddclock for “ack” messages
initially v[i] = 1
v[j] = 0 for ji
q: active vector of integer initially
req: boolean initialy false
request :
req:=true
q[i]:=v[i];
receive (u):
if NOT req V ( u.q [u.p] < q[i] ) then
send ack to u.p
release:
req:=false;
for j: j≠i do
if (q[i]<q[j]) then
send ack to the process j
Când se recepționează un ack message (u) în starea s, se va actualiza și s.v[s.p] și s.v[u.p], în timp ce la recepționarea unui mesaj request se va actualiza doar s.v[s.p]
În consecință putem formula următoarele proprietăți:
1. s,t s.p t.p : s t s.v[s.p]<t.v[t.p]
2. s,t : s.p t.p : s.v[s.p] t.v[s.p] implică existența unui ack trimis ulterior lui s și recepționat înainte de $.
Vom defini de asemenea:
cs(s) s.req j : j s.p : s.q[s.p] < s.v[j]
Rezultatele următoare vor demonstra corectitudinea acestor algoritmi.
Lema 2.3
În ipoteza că cs(s) este adevărată și notând:
s := max {x / x s, req_start (x)},
toate procesele j s.p transmit un ack ce este recepționat între stările s și s.
Demonstrație
Conform proprietăților ceasului:
j: j s.p : s.v [s.p] > s.v[j]
s.q[s.p] = s.v[s.p]
prin urmare :
j : j s.p : s.q[s.p] > s.v[j]
dar cs(s) implică :
j : j s.p : s.q[s.p] < s.v[j]
deoarece s.q[s.p] = s.q[s.p], toate celelalte componente s-au schimbat între s și s,
deoarece ddclock este utilizat doar pentru ack rezultă concluzia lemei.
Teorema 2.4 (“de siguranță”)
Fie s și t astfel încât s.p t.p
s || t implică : NOT (cs(s) cs(t))
Demonstrație
Fie s și t astfel:
s := max {x/ x<s, req_start(x)}
t := max {x/ x<t, req_start(x)}
conform algoritmului avem:
s.q[s.p] = s.q[s.p]
t.q[t.p] = t.q[t.p]
s.q[s.p] = s.v[s.p]
t.q[t.p] = t.v[t.p]
Vom analiza separat următoarele cazuri:
Cazul 1: t.q[t.p]<s.q[s.p]
Vom arăta că cs(s) duce la o contradicție.
Demonstrația are doi pași:
vom arăta că există un ack trimis dintr-un w, unde t < w < t și este recepționat înainte de s.
vom arăta că existența unui astfel de mesaj conduce la o contradicție.
cs(s)implică s.q[s.p] < s.v[t.p]
s.q[s.p] < s.v[t.p] implică există un ack de la w
deci w.v[t.p]=s.v[t.p] (*)
t.v[t.p] = (conform definiției lui t)
=(conform definiției lui t’)
t.q[t.p]
<(în acest caz)
s.q[s.p]
<(datorită cs(s))
s.v[t.p]
=(conform relației *)
w.v[t.p]
Deci t’v[t.p] < w.v[t.p], prin urmare: t’ < w.
tw implică t s deci w < t
astfel t’ < w < t
Rămâne de arătat că ack trimis de w este recepționat înainte de s’. notăm cu r starea care a generat mesajul request corespunzător lui ack transmis de w.
t’ < w < t w.req > este adevărată
Deoarece mesajul ack este transmis doar în cazul w.req = false sau w.req = true AND r.q[s.p] < w.q[t.p] deducem :
r.q[s.p] < w.q[t.p]
Deoarece w.q[t.p] = t.q[t.p] < s.q[s.p] vom trage concluzia că r este un request precedent lui s’. deci există u<s’ astfel încât cs(u). Conform Lemei 2.3 mesajul transmis din w este recepționat înainte de u pentru a putea avea cs(u).
În concluzie ack trimis de w este recepționat înainte de s’.
s.q[s.p]
< (conform definiției cs(s))
s.v[t.p]
= (deoarece w este starea care transmite)
w.v[t.p]
< (deoarece w este recepționat înainte de s’)
s’.v[s.p]
=(conform definiției lui s’)
s.q[s.p]
deci s.q[s.p] < s.q[s.p] evident absurd
Cazul 2. s.q[s.p] < t.q[t.p]
Se tratează într-un mod similar.
Deoarece nu reprezintă dificultăți se va renunța la prezentarea demonstrațiilor următoarelor două rezultate.
Teorema 2.5 (vitalitate)
s.req implică t: s < t AND cs(t)
Teorema 2.6 (“de onestitate”)
(req_start(s) AND req_start(t) AND st) implică
(next_cs(s) next_cs(t))
§2.4. Algoritmul centralizat
Algoritmul centralizat introduce un nou proces, numit coordonator, care gestionează mesajele request astfel încât constrângerile de onestitate nu sunt încălcate.
Pi::
var v: array[1..n] of integer initialy 0
havetoken : boolean initialy false
req: boolean initialy false
request :
req:=true;
send(request,v) to Po
v[i] ++;
receive(n,token)
req:= false;
havetoken := true;
release:
send token to Po;
havetoken :=false;
receive(u): /*progran message */
v:=max(v,u.v);
Po::
var reqdove: array[1..n] of integer initialy 0;
reqlast: list of (pid, recvector);
havetoken: boolean initialy true;
receive (u,request):
append(reqlist,u);
if havetoken then checkreq;
receive (u,token)
havetoken :=true;
checkreq;
checkraq:
Eligible:={w reqlist | w.v reqdone}
If eligible {} then
w:= first(eligible);
delete(reqlist,w);
reqdone[w.p]++;
send token to Pw.p;
baretoken=false;
end;
Capitolul 3. Stare globală
§3.1. Tăieturi consistente
Prin stare globală vom înțelege o mulțime de stări locale care sunt oricare două concurente. Vom folosi în acest capitol noțiunea de deposet așa cum a fost definită în Capitolul I.
O tăietură este o submulțime a unui deposet S ce conține exact o stare din fiecare submulțime Si.
Vom nota cu Gs (sau când nu există pericol de confuzie doar cu G) mulțimea tuturor tăieturilor deposet-ului S. Pentru două tăieturi G,H G, vom spune G H dacă și numai dacă i : G[i] H[i], unde G[i]Si sunt stări ale procesului Pi în tăieturile G și H.
Următoarea teoremă este o consecință imediată a definițiilor anterioare:
Teorema 3.1.
Pentru orice deposet S, (GS,) este o latice
O submulțime G S se numește consistentă (și se notează consistent(G) dacă și numai dacă x,y G: xy).
Deoarece fiecare mulțime Si este total ordonată este evident că dacă G=N și avem consistent(G) atunci G trebuie să includă exact o stare din fiecare Si, adică G este o tăietură consistentă.
Teorema 3.2
Pentru orice deposet S, notând cu mulțimea tăieturilor consistente ale lui S, (, ) este o latice.
Lema 3.1.
Pentru orice o stare S și orice proces Pi există o mulțime nevidă de stări numită “interval concurent cu S al lui Pi”, notat prin Ii(s) și satisfăcând condițiile:
Ii(S) Si, adică intervalul este constituit doar din stări ale procesului Pi
t Ii(s): ts, adică toate stările intervalului sunt concurente cu s
Demonstrație
Dacă s aparține procesului Pi atunci lema este trivială, intervalul fiind mulțimea Singleton {x}.
Vom presupune că s nu aparține lui Pi
Definim Ii(s).lo := min {vv Si AND }
Ii(s).lo este bine definit deoarece Final(i)s conform definiției deposet-ului.
Similar vom defini :
Ii(s).hi = max{vvSi 1 sv}
Vom arăta că Ii(s).lo Ii(s).hi. Folosim metoda reducerii la absurd, presupunem contrariul
Cazul 1: Există v, Ii(s). lo Ii(s).hi.
Deoarece v Ii(s).lo implică vs și Ii(s).hi v implică sv obținem vv, contradicție.
Cazul 2: Ii(s).hi im Ii(s).lo
Conform definiției lui Ii(s).lo există un mesaj trimis din starea imediat precedentă lui Ii(s).lo, similar se arată că există un mesaj recepționat în starea imediat ulterioară lui Ii(s).hi. Conform definirii deposetului nu pot exista mai mult de un eveniment între două stări vecine. Deci contradicție.
În concluzie s-a arătat : Ii(s).loIi(s).hi, mai mult, orice stare t astfel încât Ii(s).lo t Ii(s).hi verifică t s și s t.
Teorema 3.3
Orice submulțime consistentă GS poate fi extinsă de o tăietură consistentă, formal:
G: G S: consistent(G) (H : G H: consistent(H) AND H=N)
Demonstrație
Este suficient să arătăm că dacă G N atunci există o tăietură H, GH, astfel încât
consistent(H) și H=G+1
Considerăm un proces Pi care nu contribuie la G. Vom arăta cp există o stare dată în Si care să fie concurentă cu toate stările din G. Fie s și t două stări distincte din G. Vom arăta că Ii(s) Ii(t) 0.
Presupunem contrariul, deci fără a reduce generalitatea:
Ii(s).hi Ii(t).lo
Similar demonstrației Lemei 3.1. se poate arăta că există cel puțin o stare, să zicem v, între Ii(s).hi și Ii(t).lo . Aceasta ar implica s v (deoarece Ii(s).hi precede v) și vt (deoarece precede Ii(t).lo). Astfel s t, ceea ce ar contrazice consistența lui G.
Deci Ii(s) Ii(t) 0
Deoarece orice interval Ii(s) este total ordonat avem:
{Ii(ssG)} 0
Alegând o stare oarecare din {Ii(ssG)} putem extinde G păstrând consistența.
§3.2. Instatanee globale ale proceselor
În această secțiune, vom descrie un algoritm ce furnizează un instantaneu global pentru un sistem distribuit. Algoritmul calculează o tăietură consistentă. Vom lucra în ipoteza că toate canalele sunt unidirecționale și satisfac condiția FIFO.
Vom spune că procesele Pi și Pj sunt vecine dacă există un canal între ele. Vom asocia fiecărui proces o variabilă, numită color, care poate lua valorile alb sau roșu.
Inițial toate procesele sunt albe. După înregistrarea stării locale procesul devine roșu. De îndată ce un proces a devenit roșu, acesta va semnala situația printr-un mesaj, numit marker, la toate procesele vecine.
Pi::
var color: {white, red} initially white;
turn_red:
enabled if (color = white)
color:=red;
save_local_state;
for all neighbors Pj do
send(marker) to Pj;
receive (marker):
if(color=white) then turn_red;
Vom demonstra câteva proprietăți elementare ale programului de mai sus. Pentru început vom defini o relație de ordine pe mulțimea culorilor: albroșu.
Lema 3.2.(de monotonie a culorilor)
s,t : st s.color t.color
Demonstrație
Evidentă, folosind inducția după , precum și FIFO.
Dacă vom utiliza notația:
t.done:=(t.color=red)
atunci programul va satisface:
Teorema 3.4.(vitalitate)
În ipotezÎa că graful corespunzător relației de
vecinătate este puternic conex, avem:
s : s.color = red j: t : t.p=k AND t.done
Demonstrație
Evidentă, utilizând inducție după lungimea drumului de la s.p la t.p
Pentru orice stare S, care îndeplinește condiția s.color = red, fie rstate(s) reprezentând starea maximă în acest proces care este colorată în alb:
rstate(s)= max {tts, t.color=white}
Vom utiliza next(n) starea imediat următoare lui n și relația de dependență directă.
Teorema 3.5. (“de siguranță”)
s,t: s.color =red AND t.color = red
rstate(s) rstate(t)
Demonstrație
Fie u = rstate(s) și v= rstate (t)
Stările u și v sunt bine definite deoarece s.color și t.color sunt red.
Va fi suficient să arătăm că : uv fals
Cazul 1: next(u)v
Din definiție next(u).color=red
Aplicând Lema 2.3. : v.color = red contradicție
Cazul 2: w: u d w AND wv
Deoarece u.color next(u).color mesajul marker a fost transmis din u, astfel w.color = roșu, ceea ce implică
v.color=roșu
§3.3. Instantanee globale ale proceselor și canalele
Vom modifica algoritmul anterior în vederea includerii stării canalelor. Prin stare a unii canal înțelegem secvența de mesaje ce tranzitează între două procese când stările acestor procese sunt conectate. Se poate ușor observa că aceste mesaje sunt transmise de procesele albe și recepționate de procesele roșii. Vom presupune de asemenea că aceste mesaje sunt ordonate FIFO. Vom utiliza chan[k] pentru a nota starea canalului k de intrare și closed[k] pentru a apoi transmiterea de mesaje de-a lungul acestui canal.
Vom folosi de asemenea notația :
s.done = k : s.closed[k] AND s.color = red
Teorema 3.6.(“de siguranță”)
s,t : s.color = red AND t.color t= red AND t.closed [s.p] u & rsate(s): event(u) = send to Pt.p : u rstate(t) OR u t.chan[s.p].
Înainte de a demonstra teorema 3.6. vom prezenta algoritmul lui Chondy și Lanford pentru instantanee:
Pi::
var color : {white, red} initially white;
chan[k] = queues of messages initially empty;
closed[k]: boolean initially false;
turn_red enabled if(color=white)
save_local_state;
color:=red;
for all neighbors Pj do
send(marker) to Pj;
receive(marker) from Pj
if(color =white) then
turn_red;
else closed[j]:=true;
receive(program_message)from Pj
if(color =red) and not closed[j] then
chan[j]:=chan[j]+program_message;
/*append the message*/
Demonstrație (a teoremei 3.6.)
t.closed[s.p] implică faptul că mesajul marker din s.p a fost recepționat de procesul t.p
fie “t” starea în care markerul a fost recepționat de procesul t.p
fie v starea în care mesajul din u a fost recepționat deoarece procesul ce recepționează markerul devine roșu avem: rstate(t)t
dacă u este alb atunci conform FIFO : vt
Dacă vrstate(t) atunci u rstate(t)
Altfel rstate(t)vtt și conform textului programului avem ut.chan[s.p]
Lema 3.3.(vitalitate)
s : s.color=red j : t : t.p=j OR t.done
Demonstrație
Este evidentă.
Capitolul 4. Predicate globale
§4.1. Problematică
Fiecărui proces Pi îi vom asocia o mulțime de variabile locale Xi. Fiecare stare s Si va defini o valoare pentru fiecare variabilă x Xi. Vom nota cu X reuniunea tuturor mulțimilor Xi. Fiecare pereche de stări sSi și tSj definesc o mulțime de tuple, aceste sunt mesaje pentru canalul Cij . Mai mult vom utiliza notația B(G) pentru a indica valoarea predicatului B în starea globală definită de tăietura G={s1,……,sN}.
Definiția 4.1
Un predicat global B este posibil adevărat pentru un deposet S dacă și numai dacă există o tăietură consistentă în S astfel încât B este adevărată în G.
Problema determinării existenței unei tăieturi consistente nu-i trivială, deoarece există mN tăieturi pentru un deposet în care s-a presupus Si = m, i.
§4.2. Predicate liniare
În această secțiune, ne propunem să descriem o clasă de predicate globale pentru care se pot construi algoritmi eficienți de detecție.
Dându-se un deposet S, un predicat B și o tăietură GS, o stare G[i] se numește stare santinelă dacă ea este inclusă în orice tăietură H, unde GH, implică : B este false pentru H.
Definiția 4.2
Dându-se o expresie booleană B, vom defini :
forbidden(G,i):= H: G H : (G[i]H[i]) OR not B(H)
Bazându-ne pe conceptul de stare santinelă, putem defini predicatul B ca fiind liniar cu respectarea deposet-ului S dacă pentru orice tăietură G sin deposet, faptul că B este fals în G implică : G conține o stare santinelă.
Definiția 4.3
Un predicat boolean B este liniar cu respectarea deposet-ului S dacă și numai dacă :
GG: TB(G) i : forbidden (G,i)
Observăm că liniaritatea unui predicat boolean depinde atât de mulțimea G cât și de deposet-ul S.
Rezultatul următor este o consecință imediată a definițiilor.
Lema 4.1
Următoarele aserțiuni sunt proprietăți ale predicatelor liniare:
Dacă B1 și B2 sunt liniare atunci și B1 AND B2 este liniar
Dacă B este definit utilizând variabilele unui singur proces, atunci B este liniar.
Predicatul unei tăieturi consistente este liniar, adică:
(B(G)= i,j : G(i)G(j)) B este predicat liniar
Demonstrație
Vom justifica doar 3:
TB(G implică: i,j : G[i] G[j]
Aceasta implică : pentru toți HG, G[i] H[j]
deci: T(G[i]=H[i]) OR TB(H)
și astfel B: este predicat liniar.
Pentru orice predicat global, B, definim o submulțime (posibil vidă) de tăieturi GB G unde B are loc pentru orice tăieturi din GB.
Se poate arăta că dacă B este liniară atunci GB este o inf-semilatice. Un corolar al acestui rezultat ar fi că cea mai mică tăietură ce satisface B este bine definită.
Lema 4.2
Fie GB G. Atunci GB este o inf-semilatice dacă și
numai dacă este liniară cu respectarea lui G.
Demonstrație
() : vom folosi metoda reducerii la absurd.
Presupunem că B nu-i liniară.
Aceasta implică că există o tăietură G astfel încât :
TB(G) și i : Hi G : (G[i]=H[i]) și B(Hi)
Fie Y:= Ui{Hi}
Se observă că toate elementele lui Y GB
De asemenea inf Y = G și G GB
Deci GB nu-i inf-semilatice, contradicție
(): Vom folosi din nou metoda de reducere la absurd.
Fie Y={H1, H2, ……,HK} o submulțime oarecare a lui GB care admite ca inf G astfel încât G nu aparține lui GB. Deoarece G este inf Y, pentru orice i, există j{1,……,k} astfel încât G[i]=Hj[i]. Deoarece B[Hj] este adevărată pentru orice j, deducem că există un G pentru care liniaritatea este încălcată.
Un exemplu de predicat liniar este predicatul de canal. Vom nota cu C starea unui canal și cu M o mulțime de mesaje.
Definiția 4.4
Un predicat de canal, c(C), se zice că este monoton dacă și numai dacă :
C: not C(C) (M: not C(C U M)) OR (M : not C(S-M))
Aceasta înseamnă că dându-se o stare de canal C, în care predicatul este fals, atunci prin transmiterea mai multor mesaje predicatul se păstrează fals sau prin recepționarea mai multor mesaje predicatul de asemenea se păstrează fals.
Un exemplu de predicat monoton este: “Canalul cij este gol”
Dacă acest predicat este fals, adică : nu este gol canalul, atunci prin transmiterea mai multor mesaje predicatul se păstrează fals.
Vom spune despre un predicat că este Predicat Conjuctiv Generalizat (GCP) dacă și numai dacă poate fi scris ca o conjuncție de predicate locale și predicate de canal monotone. Adică:
GCP=
(l1 AND l2 AND…AND la AND c1 AND c2 AND…ANDce)
Teorema 4,2,
Fie B un predicat conjunctiv generalizat (GCP) astfel încât toate predicatele sale de canal sunt monotone. Fie (G,e) mulțimea tăieturilor consistente globale în care orice GCP este adevărată. Dacă G,H G atunci sup (G,H) este de asemenea în G.
Demonstrație
Amintim că GCP(G) este adevărată dacă și numai dacă
G este o tăietură consistentă, și
Toate predicatele locale sunt adevărate în G, și
Toate predicatele canal sunt adevărate în G
Fiecare din clauzele de mai sus este liniară și se aplică lemele 4.1. și 4.2.
Ne propunem să analizăm detecția unui predicat global liniar dându-se o tăietură, G, trebuie să determinăm în mod eficient dacă B este adevărată pentru G. Speculând liniaritatea lui B, dacă B este evaluat cu fals într-o tăietură G atunci știm că există o stare santinelă în G. Vom presupune de asemenea că există un algoritm eficient de determinare a unei stări santinelă. Cu aceste ipoteze algoritmul de detecție a unui predicat global liniar poate fi:
i : G[i]:= Init(i);
while TB(G) do
find i such that forbidden (G,i);
if (G[i]=Final(i)) then return false
else G[i]:=next.G[i];
end while
return true;
Teorema 4.3.
Dacă B este un predicat liniar atunci există un algoritm eficient pentru detectarea celei mai mici tăieturi care să satisfacă B.
Demonstrație
Vom căuta cea mai mică tăietură pentru care B este adevărată plecând de la starea inițială. Dacă predicatul este fals în starea curentă,(linia 2) atunci vom căuta procesul cu starea santinelă (linia 3). Dacă acesta este ultima stare a procesului atunci se returnează fals altfel avansăm de-a lungul procesului care are starea santinelă.
Exact ca existența celei mai mici tăieturi care solicită liniaritatea predicatului, existența celei mai mari tăieturi solicită o proprietate duală linearității.
Definiția 4.5
Un predicat B este post_liniar dacă și numai dacă : GG: TB(G) i : HG : T(G[i]= H[i])ANDTB(H).
Toate rezultatele prezentate anterior admit rezultate duale pentru predicate post-liniare. Astfel, B este un predicat post-liniar dacă și numai dacă GB este o sup-semilatice.
De asemenea există un algoritm eficient pentru furnizarea unei cele mai mari tăieturi pentru orice predicat post-liniar.
Folosind ambele noțiuni (de predicat liniar / postliniar) putem enunța:
Teorema 4.4
GB este o latice dacă și numai dacă B este liniară cu respectarea lui G și B este de asemenea post-liniară cu respectarea lui G.
Definiția 4.6
Dându-se o expresie booleană B, vom defini semi_forbidden(G,i) :=H: GH : G[i]H[i] OR TB(H) OR kG : B(K) AND G[i] & K[i]
Adică: G[i] este o stare semi-santinelă dacă pentru orice tăietură H mai târziu decât Gm sau H nu include G[i] sau predicatul B este fals în H sau există o altă tăietură K pentru care predicatul B este adevărat și K nu include G[i].
Definiția stării semi-santinelă permite eliminarea lui G[i] sin calcularea tăieturii ce satisface B.
Definiția 4.7
Un predicat B se numește semi-liniar cu respectarea deposet-ului S dacă :
GG : TB(G) i : semi_forbidden(G,i)
Un exemplu de predicat semi-liniar este algoritmul de excludere mutuală. În acest caz ne interesează să determinăm existența unei tăieturi consistente G astfel încât :
B(G) := i,j : CS(G[i]) AND CS(G[j]) AND consistent(G) unde prin CS(G[i]) notăm faptul că procesului Pi i se dă permisiunea de-a intra în secțiunea critică în tăietura G.
O primă utilizare este reducerea teoremei de extensie a unei subtăieturi de problema detecției unui predica:
B(G)=i,j : CS(G[i])ANDCS(G[j])ANDG[i]G[j]
Teorema în cauză implică extinderea subtăieturii {G[i],G[j]} la o tăietură consistentă. Menționăm că dacă B este fals în G avem:
i,j not CS(G[i]) OR not CS(G[j]) OR not (G[i]G[j])
Dacă not CS(G[i]) și există o stare după G[i], atunci G[i] este o stare semi-santinelă . Acum presupunem că CS(G[i]) este adevărată pentru orice i sau G[i] este starea finală a procesului i. Fără să afectăm generalitatea putem presupun că stările tăieturii g care satisfac CS pot fi sortate. După sortare cel mai mic G[i] este stare semi-santinelă.
Capitolul 5. Predicate globale conjunctive
§5.1. Predicate conjunctive slabe
Un predicat conjunctiv slab (WCP) este adevărat pentru o rulare dacă și numai dacă există o tăietură globală consistentă pentru care toate complementele sunt ordonate.
Predicatele conjunctive formează o clasă interesantă de predicate deoarece detecția lor este suficientă pentru detectarea oricărui predicat global care poate fi scris ca o expresie booleană de predicate locale.
Lema 5.1
Fie p un predicat construit cu predicate locale utilizând conectori booleeni. Atunci, p poate fi detectat utilizând un algoritm care poate detecta q, unde q este o conjuncție pară de predicate locale.
Demonstrație
Predicatul p poate fi rescris în forma disjunctivă
P= q1OR……ORqe
unde fiecare qi este o conjuncție pură de predicate locale. Tăietura globală satisface p dacă și numai dacă satisface cel puțin una din qi-uri. Deci problema a fost redusă la rezolvarea detectării unei conjuncții de predicate locale. Demonstrația s-a încheiat.
Vom nota cu LPi predicatul local corespunzător procesului Pi iar cu LPi(s) faptul că predicatul LPi este adevărat în starea s. Vom spune că s r[i] dacă s apare în secvența r[i].
Teorema 5.1
(LP1 AND LP2 AND…AND LPn) este adevărată pentru o rulare r dacă și numai dacă pentru toți i, 1in, si r[i] astfel încât LPi este adevărată în starea si și si și sj sunt concurente pentru ij.
Demonstrație
Evidentă folosind definițiile.
§5.2. Algoritm centralizat pentru WCP bazat pe vectori ceas
În această secțiune vom prezenta un algoritm bazat pe vectori ceas care să furnizeze o mulțime de stări inconfundabile în care predicatele locale sunt adevărate. Mai precis acest algoritm va calcula prima tăietură consistentă pentru care WCP este adevărată.
Deoarece WCP este un predicat liniar, dacă există o tăietură pentru care WCP este adevărată, atunci există și o primă astfel de tăietură.
Algoritmul folosește un proces controlor. Fiecare proces de aplicație posedă un vector local lcmvector (last canal message vector)
Procesul aplicație este următorul:
Pi::
Var lcmvector : array[1..n] of integer;
Initially j : ji : lcmvector[j]=0
lcmvector[i] = 1;
firstflag : boolean initially true;
when send m do
send(lemvector,m);
lcmvector[i]++;
firstflag:= true;
upon receive(mesg_lemvector,m) do
for(all j) do
lcmvector[j]:=max(lem[j],msg_lemvector[j])
upon(local_pred = trueAND fistflag) do
firstflag := false;
send(lcmvector) to the checker process;
Vom defini predicatul first(s) ca fiind adevărat dacă și numai dacă predicatul local este adevărat pentru prima dată de cel mai recent mesaj transmis sau de la demasarea procesului. Vom spune că web(s1,……,sn) este adevărat dacă s1,……,sn sunt stări din procese diferite ce satisfac WCP.
Teorema 5.2
s1,……,sn : wep(s1,……,sn)
s1,……,sn : wep(s1,……,sn) AND : 1i m : first(si)
Demonstrație
(): este evidentă
() : datorită simetriei este suficient să arătăm că s1 astfel încât wcp(s1,s2,……,sn)ANDfisrt(s1) deoarece s1 există, există și s1
pentru a arăta wcp(s1,s2,……,sn) este suficient să arătăm că s1sj pentru q j m.
s1sj s1 sj
sj s1 astfel : sjs1 contradicție
În continuare prezentăm procesul controlor:
var cut: array[1..n] of struct
v : vector of integer;
color: {red, green}
end initially(i : cut[i].color = red);
repeat
/* advance the cut*/
while(i : cut[i]).color=red)AND(q[i]0))do
cut[i]:=receive(q[i]);
paint_state(i);
endwhile
until(i:cut[i].color = green)
detect:=true;
Procesul controlor este responsabil pentru căutarea unei tăieturi consistente ce satisface WCP. O tăietură candidat poate eșua datorită inconsistenței sau a nesatisfacerii unui termen din WCP. Procesul controlor poate elimina starea care a provocat eșuarea tăieturii candidat, avansând de-a lungul procesului în cauză. Procesul controlor recepționează instantanee de la celelalte procese din sistem. Aceste mesaje sunt utilizate pentru crearea și menținerea structurii de date ce descrie starea globală sistemului pentru tăietura curentă. Structura de date cuprinde cozile mesajelor de intrare și informații despre stările proceselor. O stare este verde dacă este concurentă cu toate celelalte stări verzi. O stare este roșie dacă nu poate aparține unei tăieturi consistente ce ar satisface WCP.
În continuare prezentăm procedura paint-state:
procedure paint_state(i)
cut[i].color:=green;
for(j : cut[j].color = green) do
if(cut[i]).v cut[j].v) then
cut[i].color := red;
return
else if(cut[j].v cut[i].v)then
cut[j].color:=red;
endfor
Procedura paint_state lucrează astfel: parametrul i reprezintă procesul de la care s-a recepționat cel mai recent instantaneu local. Culoarea lui cut[i] este inițial verde și poate schimbată în roșu dacă încalcă proprietatea de concurență mutuală cu toate celelalte stări verzi.
Lema 5.2
Proprietatea următoare este un invariant al programului în ipoteza că funcția point_state este atomică.
i,j : (cut[i].color = green) AND (cut[j].color = green) cut[i]cut[j]
Demonstrație
Inițial “invariantul” este adevărat deoarece cut[i].color=red pentru toți i. Culoarea lui cut[i] poate fi schimbat doar de funcția paint_state. În această funcție, cut[i] este comparată cu toate cut[j] ale căror culoare este verde.
Dacă cut[i] nu este concurentă cu cut[j] atunci una din ele este colorată în roșu și în acest mod aserțiunea rămâne invariantă și după trecerea funcției paint_state.
Lema 5.3
Pentru toți i, dacă cut[i].color= red atunci nu există o
tăietură globală ce satisface WCP și care să includă cut[i]. Cu alte cuvinte cut[i] este o stare santinelă.
Demonstrație
Vom folosi inducția după minimul de stări care sunt colorate în roșu. Inițial aserțiunea este adevărată deoarece cut[i] este Init[i] și nu există o tăietură globală care să includă o astfel de stare. Presupunem lema adevărată pentru toate stările colorate în roșu de până acum. Variabila cut[i] este colorată în roșu doar de un proces j astfel încât cut[i].vcut[j].v. Vom arăta că nu există nici o stare a procesului Pj care să facă parte din aceeași tăietură globală cu cut[i] și să satisfacă WCP. Conform programului, o tăietură avansează la starea următoare doar dacă starea curentă este roșie. Aceasta implică faptul că toți predecesorii lui cut[j] sunt roșii și prin urmare, datorită ipotezei de inducție nici unul nu poate aparține unei tăieturi ce satisface WCP. Stările cut[j] și cut[i] nu pot face parte simultan dintr-o stare globală deoarece cut[i] cut[j].
Mai mult, datorită ipotezei FIFO dintre procesele de aplicație și procesul controlor, toate stările mai târzii decât cut[j] din coada procesului Pj sunt mai mari decât cut[i]. Aceasta implică că nici o altă stare candidatelor din Pj nu poate să fie concurentă cu cut[i]. Prin urmare cut[i] poate fi eliminată.
Rezultatul următor ne asigură că algoritmul nu ne furnizează o detecție falsă.
Teorema 5.3 (Corectitudine)
Dacă semaforul detect este true atunci există o tăietură în care WCP este adevărat. Mai mult tăietura produsă de algoritm este prima tăietură pentru care WCP este adevărată.
Demonstrație
(detect=true) i : cut[i].color = green
conform algoritmului aplicației de proces în acest caz avem : LPi (cut[i])
conform Lemei 5.2. : i,j : cut[i]cut[j]
deci tăietura satisface WCP
vom arăta că aceasta este prima tăietură cu această proprietate.
Observăm că tăietura avansează doar când cut[i] este roșie, conform Lemei 5.3., în acest caz, cut[i] nu aparține nici unei tăieturi ce ar satisface WCP.
Deoarece toate tăieturile anterioare celei curente conțin cel puțin o stare roșie rezultă că tăietura detectată este prima ce satisface WCP.
Teorema 5.4. (Completitudine)
Fie C prima tăietură ce satisface WCP. Atunci algoritmul WCP furnizează tăietura C.
Demonstrație
Deoarece C este prima tăietură ce satisface WCP, toate stările anterioare nu pot satisface WCP. Vom arăta că toate aceste stări sunt colorate în roșu. Demonstrația va fi prin inducție după numărul total de stări dinaintea acestei tăieturi. Dacă nu există nici o astfel de stare atunci aserțiunea este adevărată. Presupunem că avem k stări colorate în roșu. Considerăm ultima stare colorată în roșu. Există cel puțin o stare înaintea acesteia. Aceasta satisface condiția while și tăietura avansează la următoarea stare. Dacă această nouă tăietură nu este C atunci există cel puțin o încălcare a rației de concurență. Pentru toate tăieturile ce preced C, cel puțin o stare este colorată în roșu și datorită acesteia tăietura poate avansa. În cele din urmă este atinsă C. Conform Lemei 5.3. toate stările tăieturii curente trebuie să fie verzi. Din acest moment, procesul controlor poate ieși din bucla repeat și seta semnalul detect.
§5.3. Algoritm centralizat pentru WCP bazat pe dependență directă
În această secțiune vom descrie un algoritm de detecție a WCP fără să utilizăm vectori ceas. Vom identifica stările utilizând un contor logic : notația (i, k) reprezentând a k-a stare a procesului Pi. Vom utiliza simplu k atunci când identitatea procesului Pi este evidentă din context. Contorul logic este întreținut de fiecare proces de aplicație. Procesele incrementează contorul la fiecare transmitere a unui mesaj. Deoarece vom presupune că există cel mult m mesaje de orice proces va rezulta cel mult m stări locale distincte pentru fiecare din cele n procese.
Secvența de stări locale care formează execuția unui proces reprezintă un larg volum de informații. Detectarea unui WCP reclamă doar o fracțiune din aceste informații. Vom încapsula acest informații într-un “instantaneu local”.
Procesele de aplicație sunt responsabile de crearea instantaneelor locale și de transmiterea acestora către procesul controlor. Un instantaneu local este creat de fiecare dată când predicatul local este adevărat pentru prima oară de când ceasul local a fost ultima oară schimbat. Acest instantaneu conține valoarea curentă a ceasului local și o listă de dependențe. Dependențele sunt stări locale identificabile de procese izolate și sunt utilizate pentru determinarea concurenței dintre stări. Dependențele sunt codificate ca perechi (i,k). O dependență (i,k) este inclusă într-un instantaneu local dacă ea n-a apărut deja într-o listă de dependență a unui instantaneu local anterior. Secvența de instantanee locale este furnizată de către procesul controlor într-o ordine FIFO.
În continuare vom descrie procesul controlor.
G reprezintă tăietura globală curentă. Tabloul color are aceeași interpretare ca și în algoritmul anterior. O variabilă candidat reprezintă un instantaneu local. Procesul controlor recepționează instantanee locale de la procesele roșii până când toate procesele devin verzi. La recepționarea unui instantaneu , procesul controlor verifică dacă G[i] are o dependență(j, k) astfel încât G[j]k. În acest caz, procesul Pj este colorat în roșu.
Var
candidat : struct
myindex : 1..m;
defend.listof(pid:i..N, stateindex: 1..m);
end;
G:array [1…N] of stateindex initially 0;
color: array[1..N] of {red, green} initially red;
q1,……,qN of candidate;
repeat
while(i : (color[i]=red) AND (q[i]0)) do
candidate:= receive(g[i]);
if(candidate.myindex G[i]) then
G[i]:=candidate.myindex;
color[i]:=green;
end;
for(j, k)candidate.depend do
if(kG[j]) then
G[j]:=k;
color[j]:=red;
end;
endfor
endwhile
until (i : color[i]=green)
detect = true;
Ne propunem să arătăm că găsirea unei tăieturi globale consistente cu respectarea dependențelor indirecte este echivalentă cu găsirea unei tăieturi globale consistente cu respectarea dependențelor directe unde toate procesele sunt implicate. Dependența directă, notată sd t , înseamnă că fie s și t aparțin aceluiași proces și s are loc înainte de t, fie există un singur mesaj transmis după s și recepționat înainte de t.
Lema 5.4
Fie G o tăietură globală. Atunci G este tăietură consistentă (adică : i,j : G[i] G[j]) dacă și numai dacă i,j : G[i] d G[j].
Demonstrație
(): deoarece sdt implică st rezultă
st implică sd t
():
Este suficient să arătăm că :
(i,j : G[i]G[j]) implică
( k,l : G[k]dG[l])
Pentru aceasta vom utiliza inducția după numărul de procese din lanțul cauzal dintre G[i] și G[j], adică nivelul de dependență indirectă dintre G[i] și G[j].
Pasul inițial : este trivial deoarece dacă nu există procese în lanțul cauzal atunci G[i]d G[j] ceea ce și căutam.
Pasul de inducție : presupunem că nivelul de dependență indirectă dintre G[i] și G[j] este k, considerăm că primul proces din lanț este Pi.
Există două cazuri:
dacă acest mesaj este recepționat înainte de G[i] atunci G[i] d G[i] deci k, l : G[k] d G[l]
dacă acest mesaj este recepționat după G[i], acest lucru ar implica G[i]G[j] și folosind ipoteza inductivă k,l : G[k]d G[l]
§5.4 Algoritm distribuit pentru WCP bazat pe
vectori ceas
Vom introduce o nouă mulțime de N procese monitor. Procesele de aplicație transmit un instantaneu local către procesele monitor asociate. Un proces monitor interacționează cu toate celelalte dar nu comunică cu procesele aplicație.
Algoritmul utilizează un unic token. Token-ul conține doi vectori. Primul vector este etichetat G. Acest vector definește tăietura candidată curentă. Dacă G[i] are valoarea k, atunci starea k din procesul Pi face parte din tăietura candidat curentă. Menționăm că toate stările tăieturii candidat satisfac predicatele locale: Tokenul este inițializat cu i : G[i]=0.
Al doilea vector este etichetat color, unde color[i] indică culoarea pentru starea candidat a procesului de aplicație Pi. Culoarea unei stări poate fi roșu sau verde. Dacă color[i] = roșu atunci starea (i, G[i]) și toate cele care o preced pot fi eliminate, neputând niciodată să satisfacă WCP. Dacă color[i] = verde atunci nu există stare în G astfel încât (i, G[i]) să aibe loc înainte de acea stare. Token-ul este inițializat i : color[i]=roșu.
var
candidate : array [1..n] of integer /*vector clock from candidate state*/
on receiving teorema token (G, color)
while(color[i]=red) do
receive candidate from application process Pi;
if(candidate[i]G[i])then
G[i] := candidate[i]
color[j]:=red;
end;
endfor
if(j : color[j] = red) then
send token to Mj;
else detect:=true;
Vom descrie algoritmul procesului monitor prezentat mai sus.
Tokenul este transmis procesului monitor Mi doar când color[i] este roșu. Când este recepționat tokenul, Mi așteaptă recepționarea noii stări candidat de la Pi și atunci verifică dacă se încalcă restricțiile de consistență cu acest nou candidat. Această activitate se repetă până când starea candidată nu precede cauzal orice altă stare a tăieturii candidat. Mai departe, Mi examinează token-ul să vadă dacă celelalte stări încalcă concurența. Dacă es găsește un j astfel încât (j, G[j]) are loc înainte de (i, G[i]) atunci setează color[j] la roșu. În final, dacă toate stările din G sunt verzi, adică G este consistent, atunci Mi detectează WCP.
§5.5. Un algoritm centralizat pentru predicate conjunctive generalizate
În algoritmii prezentați mai devreme pentru eficientizarea detecției predicatelor globale, aceste au fost specificate ca formule booleene de predicate canale. Multe proprietăți din sisteme distribuite utilizează și stările de canal. Ne propunem să prezentăm un algoritm eficient de detecție a unei formule booleene de predicate locale și de predicate de canal.
Un predicat canal este o funcție booleană de stări ale canalului. O stare de canal este definită ca o mulțime diferită de evenimente transmise și evenimente recepționate ale respectivului canal. Deoarece un canal este definit ca o conexiune unidirecțională între două procese, un proces execută toate evenimentele de transmisie și altul pe cele de recepție, aceste sunt mesaje care sunt în tranzit. Notațiile pentru acumulările de evenimente de transmisie sau de recepție sunt :
, stări ale proceselor distincte, Pi și Pj, adică r[i] și r[j].
.test[j] secvența tuturor mesajelor transmise de la procesul i la procesul j până la starea inclusiv.
.Rcvd[i] secvența tuturor mesajelor recepționate de procesul j de la procesul i până la starea inclusiv.
Un predicat de canal poate fi scos sub forma:
c(,) = c(Sent[j] – .Rcvd[i])
Vom utiliza simbolul S pentru reprezentarea unei secvențe arbitrare de evenimente de transmis de la un proces și simbolul R pentru reprezentarea unei secvențe arbitrare de evenimente recepționate.
Vom presupune canalele fără memorie. Pentru eficiență predicatele de canal trebuie să fie cel puțin monotone :
S: TC(S) (S : TC(S U S))OR (R: TC(S-R))
Adică : dându-se o stare de canal, S, în care predicatul este fals, atunci fie prin transmiterea de mai multe mesaje fie prin recepția mai multor mesaje predicatul rămâne fals.
Vom admite că în momentul evaluării predicatului de canal într-o stare S, este cunoscut care din aceste două cazuri se aplică. De exemplu vom defini predicatul canal ca o funcție ce poate lua trei valori:
T – predicatul de canal este adevărat pentru starea de canal curentă.
Fs – predicatul de canal este fals pentru starea de canal curentă. Mai mult, predicatul rămâne fals dacă o mulțime arbitrară de mesaje este transmisă prin canal în absența oricărei recepționări. Un astfel de predicat îl vom numi “monoton la transmisie”
Fr – predicatul de canal este fals pentru starea de canal curentă. Mai mult, predicatul rămâne fals dacă o mulțime arbitrară de mesaje este recepționată prin canal în absența oricărei transmisii. Un astfel de predicat îl vom numi “monoton la recepție”.
Scopul nostru este să dezvoltăm un algoritm de detecție a predicatelor conjunctive generalizate (GCP), care sunt de forma l1 AND l2 AND …… AND ln AND c1 AND c2 AND…… AND cl
Unde li –urile sunt predicate locale iar cj – urile sunt predicate de canal.
Algoritmul procesului de aplicație Pi este următorul:
var
incsend, increcv : array of messages;
initially incsend=increcv=0;
lcmvector: array [1..n] of integer;
initially j : ji: lcmvector [j] = 0;
lcmvector[i] = 1;
firstflag : boolean initially true;
when sending m do
send(lcmvector, m);
lcmvector[i]++;
firstflag := true;
incsend:= incsend + m; /* concatenate */
upon receive (msg_lcmvector,m) do
for(all j) do
lcmvector[j]:=max(lcmvector[j],mesg_lcmvector[j]);
firstflag:= true;
increcv :=increv + m ; /*concatenate*/
upon (local_pred =true AND firstflag) do
firstflag:= false;
send(lcmvector, incsend, increcv) to the checker process;
incsend:= increv :=0;
Procesele aplicație monitorizează predicatele locale. Aceste procese mențin de asemenea informații despre istoria transmisiilor și recepțiilor pentru toate canalele incidente cu acesta, adică conexiunile cu toate procesele pentru care poate trimite sau de la care poate primi mesaje. Procesul de aplicație transmite un mesaj către procesul controlor ori de câte ori predicatul local devine adevărat pentru prima oară de la ultimul mesaj trimis dau primit. Acest mesaj este numit instantaneu local și este de forma:
(lcmvector, incsend, increcv)
unde lcmvector este “last canal message vector” curent și incsend și increcv sunt liste de mesaje transmise sau recepționate de la alte procese de aplicație.
În continuare vom prezenta algoritmul procesului controlor:
var s[1..n,1..n], R[1..n,1..n ]: sequence of message;
cp[1..n,1..n] : {X, F, T};
cut : array[1..n] of struct{
v: vector of integer;
color:{red,green};
incsend, increcv: sequence of messages}
initially
cut[i].v=0;
cut[i].color=red;
S[i,j]=0;
R[i,j]=0;
Repeat
/* advance the cut */
while(i : (cut[i].color = red)AND(q[i]0)) do
cut[i] :=receive(q[i]);
paint_state(i);
update_channels(i)
endwhile
/*evaluate a channel predicate*/
if(i,j : cp[i, j] = X AND cut[i].color = green AND cut[j].color=green)
then
cp[i,j]:=cleanp(S[i,j]);
if(cp[i,j]=Fs) then cut[j].color :=red
else if(cp[i,j]=Fr) then cut[i].color:=red;
end
until(i : cut[i].color=green)AND(i,j : cp[i,j]=T)
detect:=true;
Procesul controlor este responsabil de căutarea unei tăieturi consistente care să satisfacă GCP. Procesul controlor recepționează instantanee locale de la toate celelalte procese din sistem. Aceste mesaje sunt utilizate de controlor pentru crearea și menținerea unei structuri de date ce descriu stări globale ale sistemului pentru tăietura curentă. Structura de date este divizată în trei categorii : cozile mesajelor de intrare, date ce descriu stările proceselor și date ce descriu informațiile despre stările canalelor. Cozile mesajelor de intrare, date ce descriu stările proceselor și date ce descriu informații despre stările canalelor. Cozile mesajelor de intrare și datele ce descriu stările proceselor sunt structurate asemănător algoritmului pentru WCP. În plus sunt menținute trei tipuri de date pentru fiecare canal:
S[1..n,1..n] : secvență de mesaje – lista mesajelor
transmise și nerezolvate, conține în ordine toate mesajele transmise prin canal dar nerecepționate până la tăietura curentă.
R[1..n,1..n] : secvență de mesaje – lista mesajelor de
recepționat și nerezolvate, conține toate mesajele ce trebuiesc recepționate prin canal dar n-au fost încă transmise până la tăietura curentă. Deoarece tăietura curentă nu este în mod necesar consistentă, stările acesteia pot fi în relație de cauzalitate și este posibil ca o stare a tăieturii să fie după ce mesajul a fost recepționat și o altă stare să fie înainte ca mesajul să fie transmis. Dacă tăietura este consistentă, atunci lista R este goală.
cp[1..n,1..n] : {X, Fs, Fr, T} – semaforul stării
predicatului de canal. Când predicatul de canal este evaluat, această valoare este înscrisă în acest semafor. Valoarea predicatului de canal nu poate fi schimbată în lipsa unei activități de-a lungul canalului. Dacă semaforul ia o valoare diferită de X atunci aceasta reprezintă valoarea predicatului de canal pentru tăietura curentă. Valoarea X indică faptul că nu se cunoaște în acel moment valoarea predicatului de canal.
Există două activități ale procesului controlor : prim este avansarea tăieturii curente și a doua este evaluarea predicatelor de canal pentru canale dintre două stări concurente ale tăieturii. Avansul tăieturii este determinat de prioritatea evaluării predicatelor canal. Predicatele canal sunt evaluate doar când tăietura curentă este consistentă și satisface toate predicatele locale sau când procesul controlor nu poate avansa tăietura curentă datorită insuficienței mesajelor primite de procese.
Scopul activităților de avansare a tăieturii este de-a găsi o nouă tăietură candidat. Se poate avansa tăietura doar dacă am eliminat cel puțin o stare a tăieturii curente și dacă un mesaj poate fi recepționat de la procesul corespondent.
Procedura paint_state este similară cu cea a algoritmului pentru WCP. Ne propunem să descriem procedura update_channels:
procedure update_channels(i)
/* for all messages sent by Pi to Pj*/
for(j: cut[i].incsend[j]0) do
S:=S[i, j];
R:=R[i, j];
S[i, j]:= S + (cut[i].incsend[j]-R);/*concatenate*/
R[i, j]:= R – cut[i].incsend[j];
if(cp[i, j] = TOR cp[i, j]= Fr)then cp[i, j]:=X;
endfor
/*for messages received by Pi from Pj*/
for(j: cut[i].increcv[j]0) do
S:=S[i, j];
R:=R[i, j];
R[i, j]:= R + (cut[i].increcv[j]-S);/*concatenate*/
S[i, j]:= S – cut[i].increcv[j];
if(cp[j, i] = TOR cp[j, i]= Fs)then cp[j, i]:=X;
endfor;
Parametrul i este indexul procesului de la care a fost recepționat ultimul instantaneu local. Procesul controlor actualizează valoarea semaforului CP în conformitate cu cut[i].incsend și cut[i].increcv. În cel mai rău caz fiecare mesaj transmis sau recepționat provoacă înscrierea unui X în semaforul CP. Procesul controlor nu poate schimba valoarea X a semaforului CP cât timp tăietura înaintează . Procesul controlor poate beneficia de avantajele monotoniei predicatelor de canal. Dacă un predicat de canal este fals de-a lungul tăieturii curente și în plus este monoton la transmitere atunci rămâne fals când sunt transmise alte mesaje, ca atare nu este necesară evaluarea predicatului până când cel puțin un mesaj este recepționat de canal. Există o optimizare similară pentru stările când predicatele sunt monotone la recepție.
O altă activitate a procesului controlor este evaluarea predicatelor canal. Un predicat canal este evaluat doar pentru canalele dintre două stări verzi. Deoarece se cunoaște că aceste stări sunt concurente este evident că lista R pentru canalul respectiv este goală.
Lema 5.5
i, j (cut[i].color = green) AND(cut[j].color=green) cut[i]cut[j]
Demonstrație
La fel ca și la algoritmul pentru WCP.
Lema 5.6
Pentru toți i, dacă cut[i].color este roșu atunci nu există nici o tăietură globală ce ar satisface GCP și să includă cut[i]
Demonstrație
Demonstrația o facem prin inducție după numărul de stări care sunt colorate în roșu. Afirmația inițială este adevărată deoarece cut[i] este inițializată de o stare fictivă (Init(i)) și nu există nici o tăietură care să includă această stare. Presupune că lema are loc pentru toate stările care să colorate în roșu până în prezent. Variabila cut[i] este colorată roșu fie de funcția paint_state fie după evaluarea unui predicat canal. Vom considera ambele aceste cazuri:
Cazul 1: cut[i] este colorat în roșu de funcția paint_state.
Acest caz se tratează similar algoritmului pentru WCP.
Cazul 2:cut[i] este colorat în roșu în urma unui predicat de canal.
Aceasta implică : fie cp[j, i] este fals și predicatul nu poate deveni adevărat prin transmiterea de noi mesaje de către procesul j (cp[j, i]= Fs), fie cp[i,j] este fals și predicatul nu poate deveni adevărat prin recepționarea de către procesul j de noi mesaje (cp[i,j]=Fr). Vom arăta că nu există stări în procesul Pj care să facă parte dintr-o tăietură globală împreună cu cut[i] și să satisfacă GCP. Ca în cazul anterior, orice predecesor al lui cut[j] este roșu și prin urmare nu poate aparține nici unei tăieturi globale care ar satisface GCP. Stările cut[j] și cut[i] nu pot aparține unei stări globale care ar satisface GCP, deoarece predicatul canal este fals de-a lungul tăieturii ce-ar include aceste stări. Aceasta implică faptul că predicatul de canal este de asemenea fals pentru cut[i] și orice succesor al lui cut[j]. Prin urmare, cut[i] poate fi eliminată.
În continuare vom descrie rolurile lui S[i, j] și R[i, j]. Vom folosi variabilele auxiliare cut[i].Send[j] și cut[i].Recvd[j]. Aceste variabile sunt utilizate doar pentru demonstrație și nu apar în program. Variabila cut[i].Sent[j] este secvența tuturor mesajelor transmise de procesul i către procesul j până la cut[i]. Similar, cut[i].Recvd[j] este mulțimea tuturor mesajelor recepționate de procesul Pi de la procesul Pj până la cut[i].
Lema 5.7
Relațiile următoare sunt invariante pentru program (este vorba despre algoritmul procesului controlor) cu excepția buclei while:
S[i, j] = cut[i].Send[j] – cut[j].Recvd[i]
R[i,j] = cut[j].Recvd[i] – cut[i].Send[j]
Demonstrație
Vom arăta pentru S[i, j], pentru R[i, j] este analog. Relația
din lemă este inițial adevărată deoarece inițial toate canalele sunt goale și S[i, j] de asemenea gol. Presupune relația verificată pentru toate tăieturile anterioare celei curente.
Vom arăta că operația de avansare a tăieturii păstrează valoarea de adevărat a relației. Fie Pi procesul de-a lungul căruia avansează tăietura și cut[i] starea anterioară, care este roșie și cut[i] noua stare. Conform ipotezei inductive avem:
S[i, j] = cut[i].Sent[j] – cut[j].recvd[i]
R[i, j]=cut[j].recvd[i] – cut[i].Sent[j]
Conform programului, cut[i].incsend[j] conține toate mesajele transmise de la Pi la Pj între cut[i] și cut[i], adică:
cut[i].Sent[j] = cut[i].sent[j] U cut[i].incsend[j]
De asemenea, cut[j].Recvd[i] nu este schimbat. Pentru demonstrație vom utiliza reuniunea în loc de concatenare.
cut[i].Sent[j] – cut[j].Recvd[i]=
=(cut[i]).sent[j] U cut[i].incsend[j]) – cut[j].Recvd[i]
=(cut[i]).sent[j] – cut[j].Recvd[i]) U (cut[i].incsend[j] – cut[j].Recvd[i])
folosind ipoteza inductivă pentru S[i, j] avem:
R[i, j] = cut[j].Recvd[i] – cut[i].Sent[j]
= cut[j]. Recvd[i] – (cut[i].Sent[j] cut[j].Recvd[i])
cut[i].Sent[j] – cut[j].Recvd[i]=
=S[i, j] U (cut[i].incsend[j] – (R[i, j] U (cut[i].Sent[j] cut[j].Recvd[i]))) = S[i, j] U (cut[i].incsend[j] – R[i, j])
Lema 5.8
Pentru toți i, j, dacă cut[i] și cut[j] sunt verzi, atunci :
(op[i, j] X) cp[i,j] = chanp(cut[i].Send[j] – cut[i].Recvd[i])
Demonstrație
Folosim din nou inducția matematică.
Aserțiunea este adevărată inițial deoarece cp[i,j]=X.
Aserțiunea poate deveni falsă dacă când fie tăietura avansează, fie valoarea lui cp[i, j] devine T, Fs sau Fr pentru tăietura curentă. Vom analiza fiecare caz în parte:
Cazul 1. Dacă tăietura avansează, un predicat de canal poate fi afectat doar dacă au fost transmise sau recepționate mesaje de la ultima evaluare. Dacă starea canalului n-a fost schimbată datorită transmiterii de mesaje, adică: cut[i].incsend[j]=0, atunci cp[i, j] nu este schimbat. De asemenea dacă cut[j].increcv[i]=0, atunci cp[i, j] nu este schimbat. Altfel aserțiunea se păstrează. Acum presupune că un mesaj a fost transmis. Dacă valoarea anterioară a fost T, atunci noua stare este necunoscută și prin urmare cp[i,j] ia valoarea X. Dacă valoarea anterioară a fost X, ea nu este schimbată și aserțiunea are loc în continuare. Dacă valoarea anterioară a fost Fs, atunci mesajele transmise adiționa nu pot schimba predicatul. În sfârșit, dacă valoarea anterioară a fost Fr atunci cp[i, j] ia valoarea X. Astfel, dacă un mesaj a fost transmis aserțiunea se păstrează. Similar se demonstrează pentru mesajele recepționate.
Cazul 2. Cp[i, j] este setat la o valoare diferită de X doar dacă valoarea curentă este X și atât cut[i] cât și cut[j] sunt verzi. Mai mult, valoarea este dată de expresia:
cp[i, j] := chanp(s[i j])
și conform lemei anterioare aceasta este echivalent cu
cp[i, j]:= chanp(cut[i].Sent[j] – cut[j].Recvd[i])
Teorema 5.5 (corectitudine)
Dacă semaforul detect este adevărat atunci există o tăietură în care GCP este adevărat. Mai mult, tăietura produsă de algoritm este prima tăietură pentru care GCP este adevărată.
Demonstrație
Evaluarea semaforului detect ca adevărat este echivalentă cu:
(i : cut[i].color = green)AND( i,j : cp[i, j]=T)
Conform programului li(cut[i]) sunt ordonate.
Conform lemei 5.5. pentru orice i, j : cut[i] cut[j]
Mai rămâne de arătat că toate predicatele de canal sunt adevărate. De la condiția de detecție i, j : cp[i, j]=T. Aceasta implică faptul că toate predicatele de canal sunt adevărate conform Lemei 5.8. Astfel, tăietura satisface GCP.
Mai rămâne de arătat că aceasta este prima tăietură cu această proprietate. Observăm că tăietura avansează doar când cut[i] este roșu.
Conform Lemei 5.6., cut[i] nu poate face parte unei tăieturi care ar satisface GCP. Deoarece toate tăieturile anterioare celei curente au cel puțin o stare roșie deducem că tăietura furnizată de algoritm este prima tăietură care satisface GCP.
Teorema 5.6 (Completitudine)
Fie C prima tăietură care satisface GCP. Atunci algoritmul GCP setează semaforul detect pe valoarea adevărat cu C ca tăietură.
Demonstrație
Deoarece C este prima tăietură care satisface GC, toate stările anterioare nu pot realiza GCP adevărat. Vom arăta că toate aceste stări sunt colorate în roșu. Vom folosi inducția după numărul de stări dinaintea acestei tăieturi. Dacă nu există astfel de stări atunci afirmația este adevărată. Presupunem k stări vopsite în roșu. Considerăm ultima stare ca fiind roșie. Există cel puțin o stare înaintea acesteia. Aceasta realizează condiția while adevărată și tăietura avansează la noua stare. Dacă această nouă tăietură nu este C atunci există cel puțin o încălcare a relației de concurență sau predicatul de canal nu-i satisfăcut în tăietura curentă. Prin urmare, pentru toate tăieturile precedente lui C, cel puțin o stare este vopsită în roșu și datorită acesteia tăietura poate avansa. În cele din urmă procesul controlor avansează la C. Conform Lemei 5.6. toate stările trebuie să fie verzi și conform Lemei 5.8. nici un semafor CP nu poate fi setat la F. În cele din urmă semafoarele CP vor fi setate la T, deoarece primul controlor nu poate intra în bucla while. În acest moment procesul controlor poate ieși din bucla repeat și seta semaforul detect la valoarea adevărat.
§5.6. Un ceas vector bogat și algoritmul de detecție GCP distribuit
Fiecare proces monitor Pi menține o structură de date de forma: S[j] : vector de mulțimi de mesaje – pentru fiecare j, mulțimea de mesaje transmise de Pi către Pj dar recepționate încă ( adică până la tăietura curentă)
R[j] : vector de mulțimi de mesaje – pentru fiecare j, mulțimea mesajelor recepționate de Pj dat netransmise încă de Pi (adică până la tăietura curentă)
cp[j] : vector cu valori {T, Fs, Fr, X} – pentru fiecare j, valoarea predicatului de canal pentru canalul de la P la Pj sau X dacă valoarea curentă nu-i cunoscută.
IR[j] : vector de mulțimi de mesaje – pentru fiecare j, o submulțime de mesaje recepționate de Pi înainte de tăietura curentă, acele mesaje care n-au fost încă transmise până la tăietura curentă
Count : integer – numărul de date recepționate de Pi
Candidate – instantaneu local corespunzător tăieturii curente
Token-ul este similar celui utilizat de algoritmul pentru WCP. Vom folosi în plus doi vectori de dimensiune n :
updates : vector de întregi – numărul de mesaje transmise către fiecare proces
CP : vectori cu valori {T, X} – dacă CP[i] este true atunci toate canalele prin care procesul i poate transmite mesaje au predicatele de canal adevărate.
Vom prezenta în continuare algoritmul procesului monitor:
on(Pi receiving to token) do
/*Find a candidate local state*/
while(color[i]=red)do
receive candidate from application process Pi
update_channels(i);
if(candidate,vclock[i]G[i]) then
G[i]:=candidate.vclock[i];
color[i]:=green;
endif
endwhile
/*Do all candidates from a consistent cut?*/
for(ji)do
if(candidate.vclock[j]G[j]) then
G[j]:=candidate.vclock[j];
color[j]:=red;
endif
endfor
if(j : color[j]=red) then
send token to Pj
wait(updates[i]=count)
eval_cps();
Algoritmul procesului monitor este asemănător celui pentru WCP, noi vom descrie doar diferențele. Doar procesului cu token i se permite să transmită mesaje. Când un proces recepționează token-ul el trebuie să aștepte până când recepționează toate mesajele înainte de a evalua predicatele de canal.
Subrutinele update_channels și eval_cps mențin structura de date ce descrie starea canalului.
procedure update_channels()
for(all j : candidate.incsend[j] 0) do
S[j]:=S[j]+(candidate.incsend[j]-R[j]);/*concatenate*/
R[j]:=R[j] – candidate.incsend[j];
if(cp[j]=T ORcp[j]=Fr) then cp[j]:=X;
CP[i]:=X;
endfor
for (all j: candidate.increcv[j] 0) do
IR[j]:= IR[j] U candidate.inrecv[j];
CP[j]:=X;
endfor;
Subrutina update_channels actualizează structura de date ca răspuns la recepționarea unui nou instantaneu local de la procesul de aplicație. Procesul monitor este responsabil de menținerea stării canalelor doar pentru acele canale pe care procesele de aplicație pot trimite mesaje. Prin urmare, pentru transmiterea de mesaje, procesul monitor nu va comunica cu celelalte procese monitor date despre starea canalului. Procesul monitor adaugă mesajele listei potrivite din tabloul S sau scoate mesajele din lista potrivită a tabloului R. La recepționări procesul monitor nu poate actualiza direct starea canalului. Toate recepționările sunt plasate într-un mesaj și transmise procesului monitor responsabil cu calculul respectiv. În loc să fie transmise imediat mesajele sunt colectate în tabloul JR. Mesajele sunt transmise înainte ca tokenul să părăsească procesul.
on(pi receiving an update(increcv) from Pj) do
R[j]:=R[j] U (increcv – S[j]);
S[j]:=S[j] – increcv;
Acest mod de lucru reduce numărul de mesaje în cazurile obișnuite. Când se recepționează mesajul se execută secvența prezentată mai sus, iar la transmisie de mesaje:
Procedure send_token(k: integer)
for(all j: IR[j]0) do
updates[j]+=1;
send IR[j] to Pj;
IR[j]:=0
Endfor
Send token to Pk
Vom descrie în continuare subrutina de evaluare a predicatului de canal:
procedure eval_cps();
/*Evaluate channel predicator on the consistent cut*/
while(has_token(i)ANDdetect=false) do
if(j : cp[j]=Fs) then
CP[i]:=X;
color[j]:=red;
send_token(j);
else if ( j : cp[j]=Fr) then
CP[i]:=x;
color[j]:= red;
send-token(i);
else if (j: CP[j]=T)then
CP[i]=T;
if(j: CP[j]=x)then send-token(j);
else detect:=true;
else
let j:=CP[j]=X;
cp[j]:=champ(S[j])
endwhile
Tabloul este utilizat la înregistrarea valorilor predicatelor de canal. Deoarece predicatele de canal se pot schimba doar când există activitate pe canal, utilizând tabloul cp putem evita reevaluările inutile ale predicatelor de canal neschimbate.
Există patru cazuri posibile pentru subrutina eval-cps.
În primul caz, cel puțin un predicat de canal este cunoscut a fi fals sau monoton la transmitere pentru starea de canal curentă. Prin urmare, starea de la procesul care recepționează poate fi ștearsă deoarece GCP n-o să fie niciodată satisfăcut până când cel puțin un nou mesaj este recepționat pe acest canal.
Al doilea caz este analog, dar cu un predicat de canal monoton de recepție pentru starea curentă . Când starea este eliminată, token-ul este transmis către acel proces.
În al treilea caz toate predicatele de canal sunt true. Este important de amintit că eval_cps este apelată doar când tăietura curentă este consistentă și toate predicatele locale sunt adevărate în această stare globală. Prin urmare, dacă toate predicatele de canal sunt true, atunci tăietura curentă satisface GCP. Întotdeauna fiecare proces monitor are acces direct doar la stările unor canale. Token-ul conține un vector, CP , pentru care elementul i este adevărat doar dacă predicatele de canal pentru Pi sunt de asemenea true. Dacă există un proces pentru care vectorul CP nu este true, atunci eval_cps trimite token-ul către acel proces. Dacă vectorul CP este true în totalitate atunci tăietura curentă satisface GCP și semaforul detect este setat pe true. Al patrulea caz este când nici un predicat nu-I cunoscut a fi fals și valoarea a cel puțin unui predicat de canal este necunoscută. În caz, un predicat de canal necunoscut este evaluat. Deoarece tăietura curentă este consistentă și deoarece toate mesajele au fost recepționate înainte de apelarea subrutinei, starea canalului este reflectată cu fidelitate de lista S.
Pentru analiza algoritmului vom prezenta patru invarianți:
Invariant 5.1
Pentru orice proces PI, dacă token-ul nu aparține procesului atunci:
j : jI : Pi.JR[j]=0.
Pe baza acestui invariant putem stabili validitatea vectorilor S și R. Varianta centralizată a algoritmului matrici de liste de înregistrări cu stările canalelor corespunzător tăieturii curente. Aceste matrici au fost notate cu S[i, j] și R[i, j]. Varianta distribuită a algoritmului atribuie câte o linie ale acestor matrici fiecărui proces. S-a arătat că pentru orice i și j astfel încât Pi și Pj sunt concurente în tăietura curentă, S[i,j] este exact starea canalului în tăietura curentă. Vom stabili o proprietate similară:
Invariant 5.2
Fie S și R mulțimi:
i : updates[i] = Pi.count
j : S[i,j] = Pi .S[j] – Pj.JR[i]
j : R[i,j] = Pi.R[j] U (Pj.JR[i]-pi.S[j])
Invariant 5.3
Dacă token-ul aparține procesului PI și tăietura curentă
este consistentă atunci și de câte ori updates[i] = Pi.count avem:
Pi.cp[j]X Pi.cp[j]=champ(G[i],G[j])
Invariant 5.4
CP[i]=T j : champ(G[i],G[j])
Teorema 5.7. (Corectitudine)
Dacă algoritmul distribuit testează semaforul detect pe valoarea true, atunci tăietura curentă satisface GCP.
Demonstrație
În semaforul detect se înscrie valoarea true doar de catre subrutina eval-cps. Această subrutină poate fi invocată când token-ul aparține procesului PI, j : color[j] = grey și Pi.count = updates[i] . Prin urmare : tăietura corectă este constituită, satisface toate predicatele locale și toate mesajele au fost recepționate. Mai mult, semaforul detect este setat la valoarea true doar când j : CP[j]=T. Prin urmare, conform Invariantului 5.4. toate predicatele de canal trebuie să fie adevărate. Rezultă că tăietura curentă satisface GCP.
Teorema 5.8. (Completitudine)
Dacă H este prima tăietură care satisface GCP, atunci
algoritmul setează semaforul detect la true și furnizează G=H.
Demonstrație
În demonstrație vom folosi doi pași. În primul pas vom arăta că dacă tăietura curentă este un predecesor al lui H atunci tăietura poate avansa. În al doilea pas vom arăta că dacă tăietura curentă satisface GCP, atunci semaforul defect va fi setat la valoarea true.
Presupunem că tăietura curentă, G, este un predecesor al lui H. Există două cazuri :
Cazul 1: i,j: (i,G[i]) (j,G[j]): adică tăietura nu-i consistentă. Prin urmare color[i] este roșu. Token-ul va fi transmis procesului Pi care avansează tăietura.
Cazul 2: i,j : clanp(G[i], G[j]): adică există cel puțin un predicat de canal nesatiafăcut, conform Invariantului 5.3, Pi.cp[j] T și conform Invariantului 5.4, CP[i] = X. Prin urmare token-ul este trimis către Pi. Subrutina eval_cps evaluează predicatul de canal până când găsește cel puțin un predicat fals sau până când toate predicatele sunt adevărate. Când predicatul fals este găsit, Pi vopsește în roșu starea și trimite token-ul . predicatul care recepționează token-ul avansează tăietura.
Prin urmare, dacă G este un predecesor al lui H, atunci tăietura poate avansa.
Vom arăta că dacă tăietura curentă este chiar H, atunci semaforul defect va fi setat la true. Conform rezultatelor anterioare avem:
i: color[i] = green.
Deoarece nici un predicat de canal nu-i fals, conform Invariantului 5.3 avem că i,j: Pi.cp[j] nu este nici F3 nici Fr. Dacă token-ul aparține lui Pi, j: Pi.cp[j] va fi setat la T. Prin urmare CP[i] va fi setat la T. La fiecare vizitare a token-ului a unui proces Pi pentru care CP[i] este X, este setat la T. Când token-ul a vizitat ultimul astfel de proces, semaforul defect va fi setat la true.
Capitolul 6. Predicate globale relaționale
§6.1 Predicate relaționale cu două variabile întregi
Vom nota valoarea unei variabile x în starea s prin s.x. Problema detecției unui predicat relațional poate fi stabilită formal astfel:
s0S0 and s1S1 and s0s1: s0x+s1x < C
unde s-a folosit deposet – ul (S0,S1,…,SN-1,~~).
Vom discuta două versiuni ale algoritmului pentru două variabile întregi – versiunea centralizată și cea descentralizată. Versiunea centralizată se poate executa concurent cu programul țintă sau după terminarea programului țintă. Versiunea descentralizată se poate executa concurent cu programul țintă și poate fi utilizat pentru detecție online a predicatelor.
Rezultatul următor este important în dezvoltarea algoritmilor eficienți pentru detecția predicatelor globale relaționale, ne arată că nu-i necesar să calculăm valoarea variabilei x în toate stările, dar este necesară recalcularea minimului valorii lui x în fiecare interval de stare. Vom utiliza notația min. x.(i, mi) care să prezinte valoarea minimă a lui x în intervalul (i, mi). Formal:
min. x.(i, mi)=(min. s:s(i, mi):sx)
Lema 6.1
( s,s0: s0S0 and s1S1 and s0s1: s0x+s1x < C)
( m0,m1:(0,m0)(1,m1): min. x.(0,m0)+min. x.(1,m1)< C)
Demonstrație
Se folosește congruența dintre intervale și stări.
Lema 6.2
(p, i)=pred.(w, j).p ( k:k> i:(p,k) (q, j) and (p, i)(q, j)
(p, i)=succ.(q, j).p ( k:k<i:(q, j)(p,k) and (q, j)(p, i)
Demonstrație
Se aplică definițiile pentru pred. și succ.
Lema 6.3
Fie up=i și vp=j
v pred. u.jsucc. v.iu
u pred.(succ. u.j).i
Demonstrație
Este evident.
Rezultatul următor furnizează un mecanism pentru monitorizarea tuturor intervalelor din P0 și P1 care sunt concurente: două intervale (0,i) și (1,j) sunt concurente dacă și numai dacă există o secvență de intervale în P0 care include (0,i), și o secvență de intervale în P1 care include (1,j). Mai mult, aceste secvențe pot fi obținute utilizând aplicațiile funcției pred. pe un interval numit KEY. Amintim că aceste secvențe de intervale sunt ele însele secvențe de stări.
Vom presupune că fiecare stare din P1 are loc înaintea unei stări din P0, deoarece presupunem că procesul P1 va transmite mesajul final <FINAL> la terminare, acest mesaj va fi recepționat de P0 înainte de terminare.
Lema 6.4
Două cicluri (0,i) și (1,j) sunt concurente dacă și numai dacă există un interval KEY în procesul P0 sau P1 astfel încât loo<ihio și lo1<ihi1, unde:
(0,hio): =pred. KEY.0
(1,hi1): =pred. KEY.1
(0,loo): =pred. (1,hi1). 0
(1,lo1): =pred. (0,hio). 1
Demonstrație
(): Presupunem (0,i)(1,j), altfel: (0,i)-/-> (1,j) și (1,j)-/-> (0,i).
Din presupunerea că fiecare stare din P1 are loc înaintea uneia din P0:succ. (1,j).0 există.
Cazul A: succ. (0,i)1-/-> succ.(1,j)0 sau succ.(0,i).1 nu există.
Fie KEY= succ.(1,j)0, atunci (1,j)KEY
Deoarece KEY este în P0 și (0,hio)=pred.KEY.0 atunci KEY=(0,hio+1). Astfel (1,j)(0, hio+1).
Deoarece (1,j)(0, hio+1) și (1,j)-/->(0,i) avem ihio
Observăm că (1,hi1)=pred.KEY.1=pred.(succ.(1,j).0).1 conform Lemei 6.3:(1,j)(1,hi1).
Prin urmare jhi1.
Deoarece (1,lo1)=pred.(0,hio).1 și (0,hio+1)=succ.(1,j).0 din definițiile noțiunilor pred și succ și conform Lemei 6.2:
(1,lo1)(0,hio) and (k:k<hio+1:(1,j)-/->(0,k))
Prin urmare: (1,lo1)(0,hio) și (1,j)-/->(0,hio)
Aceasta implică l01<j
Vom arăta că iloo nu-i posibil. Observăm că iloo implică succ.(0,i).1(1,hi1).
Aceasta implică: succ.(0,i)succ.(1,j).0 contradicție.
Cazul B: succ.(0,i).1succ.(1,j).0
Aceasta implică succ.(1,j).0-/->succ.(0,i).1
Fie KEY= succ.(0,i).1 și se tratează similar cazului A.
(): 1. (0,loo)=pred.(1,hi1).0 and loo<i and jhi1
(aplicând Lema 6.2)
(k:k>loo:(0,k)-/->(1,hi1)) and loo<i and jhi1
(0,i)-/->(1,hi1) and jhi1
(0,i)-/->(1,j)
2. similar (1,j)-/->(o,i)
Altfel (0,i)(1,j)
Un corolar al lemei anterioare ar fi că intervalul KEY este inițiat de mesajele recepționate. Intervalele inițiale de mesaje recepționate le putem numi: intervale de recepție iar dintre intervalele de recepție acelea care satisfac proprietățile lui KEY din Lema 6.4 le putem numi intervale cheie.
Atât algoritmul centralizat cât și cel descentralizat culeg informații despre execuția programului țintă. Ele diferă după modul cum sunt prelucrate acestea. Pentru început vom explica despre ce informații este vorba și cum sunt ele obținute.
Fiecare proces Pi, pentru i{0,1} trebuie să evalueze min.(i,m) pentru fiecare interval (i,m). în plus pentru ca algoritmul să fie complet trebuiesc îndeplinite următoarele: 1) P1 transmite mesajul <FINAL> către P0 imediat înainte ca P1 să se termine, 2) furnizarea acestui mesaj este așteptată de P0 înainte de a se termina și 3) P0 trebuie să recepționeze acest mesaj înainte de terminare.
Algoritmii se bazează pe Lema 6.4. Fiecare mesaj recepționat de P0 sau P1 inițiază un interval de recepție care este un potențial interval cheie. Fiecare interval cheie definește valori pentru loo, hio, lo1 și hi1. Valorile loo și hio definesc o secvență de intervale pentru P0. Fiecare interval din această secvență este concurent cu fiecare interval din secvența corespunzătoare a lui P1. Conform Lemei 6.4 fiecare pereche de intervale concurente ale lui P0 și P1 ce apar în secvențe rezultă din intervale de recepție. Altfel dacă P0 și P1 verifică predicatele pentru toate perechile de stări în aceste secvențe de fiecare dată când recepționează mesajul, atunci predicatul este detectat corect și complet.
Vom arăta cum sunt determinate valorile pentru l0o, hio, l01 și hi1 în fiecare interval de recepție. Conform Lemei 6.4 pentru orice interval cheie:
(0,hio)=pred.KEY.0 (0,loo)=pred.(pred.KEY.1).0
(1,hi)=pred.KEY.1 (1,lo1)=pred.(pred.KEY.0).1
Aceste informații pot fi obținute utilizând o matrice ceas 2×2. Fie Mx matricea ceas a procesului Pk. Fie (0,n) un interval în P0 și M0 valoarea matricei ceas a lui P0 în intervalul (0,n):
(0,hio) =pred.(0,n).0
=(0,n-1)
=(0,M0[0,0]-1)
(1,hi1) =pred.(0,n).1
=(0, M0[0,0]).0
=(1,M0[0,1])
(0,hio) =pred.(1, M0[0,1]).0
=(1, M0[1,1]).1
=(0,M0[1,0])
(0,hio) =pred.(0,n-1).1
=(0, M0n-1[0,0]).1
=(1, M0n-1[0,1])
unde M0n-1 este valoarea lui M0 în intervalul exterior lui (0,n-1). Expresiile valorilor corespunzătoare lui P1 se pot determina similar.
În continuare vom descrie algoritmul descentralizat. Datorită simetriei ne vom ocupa doar de P0. De fiecare dată când un mesaj este recepționat sunt evaluate loo, hio, lo1 și hi1. Aceste definesc o secvență de intervale în P0 și P1. Secvența lui Pi începe din (i, loi+1) și se sfârșește în (i,hii). Conform Lemei 6.4 fiecare interval din secvența lui P0 este concurent, vom nota această valoare cu min_x0 și similar pentru min_x1. Dacă suma acestor două valori este mai mică decât C atunci predicatul este satisfăcut. Mai mult, conform Lemei 6.4, dacă predicatul este satisfăcut atunci această metodă îl va detecta.
min_x0=(min. i:loo<ihio: min. x.(0,i))
min_x1=(min. j:lo1<ihi1: min. x.(1,j))
if (min_x0+min_x1<C) then PREDICATE_DETECTED
Valoarea min_x0 va fi calculată local, P0 va transmite mesaj către P1 conținând (min_x0, loo, hi1) și P1 va finaliza calculul. Acest mesaj este intern, el nu va fi considerat eveniment extern (adică nu va iniția un nou interval), astfel de mesaje se numesc mesaje de aplicație.
Versiunea centralizată a algoritmului poate fi utilizată de un proces controlor care s-ar executa concurent cu programul țintă sau poate fi utilizată după terminarea execuției programului țintă. Vom descrie varianta utilizată după terminarea execuției programului țintă care citește datele din fișiere urmă generate de P0 și P1. Deoarece fișierul urmă este acceptat secvențial, algoritmul poate fi ușor adoptat să se execute concurent cu programul țintă prin înlocuirea fișierului I/O cu mesaje I/O. pentru început vom explica ce date sunt stocate în fișierele urmă, după care vom arăta cum predicatul poate fi detectat de un proces care accesează ambele fișiere urmă.
Fie R0 numărul de intervale de recepție din P0 și Q0[k], 1kR0, o înregistrare ce conține valorile loo, hio, lo1 și hi1din al k- lea interval de recepție. Definim R1 și Q1[1..R1] similar. Elementele din Q0 și Q1 trebuie să fie verificate dacă reprezintă intervale cheie.
Atât Q0 cât și Q1 sunt forțate, adică, pentru Q=Q0 sau Q=Q1 și pentru fiecare componentă x{ loo, hio, lo1, hi1}.Q[].x este forțat. Acesta rezultă din faptul că elementele sunt generate în ordine de singur proces, astfel intervalele de recepție reprezentate de Q[k] au loc înainte de Q[k+1].
Fișierul urmă a lui P0 conține două tablouri de date: min.(0,i) pentru fiecare interval (0,i) și Q0[1,R0]. La fel fișierul urmă a lui P1 conține min. x.(1,j) și Q1[1,R1]. Mai devreme s-a arătat cum pot fi evaluate l0o, hio, l01 și hi1 pentru orice interval din P0 sau P1. Generarea valorilor pentru min. x este ușoară.
Fișierele urmă le analizăm în continuare. Vom descrie funcția check(Q) astfel încât predicatul este satisfăcut dacă și numai dacă check(Q0) sau check(Q1) returnează true. Check utilizează două heap-uri: heap0 și heap1. Heapp conține tople de forma < n, min x.(p,n)>, unde (p, n) este un interval din Pp. primul element al toplului h este accesat via h.value. Heap-ul este sortat după câmpul value.
Algoritmul satisface următoarele proprietăți (heap are loc tot timpul, I1 și I2 au loc în stările S4 și S5, k este o variabilă program):
heap(h,p:h heapp: heapp.top().value h.value)
I1( i,p:Q[k].lop<iQ[k].hip:<i,min x.(p,i)> heapp)
I2( p:Q[k].lop< heapp. top().intervalQ[k].hip)
function check(Q[1..R])
n0:=1; n1:=1;
for k:=1 to R do
S1: while (n0Q[k].hio) do
heap0.insert( <n0, min x.(0,n0)> );
n0:=n0+1;
endwhile
S2: while (n1Q[k].hi1) do
heap1.insert( <n1, min x.(1,n1)> );
n1:=n1+1;
endwhile
S3: while (heap0.top().intervalQ[k].l0o) do
heap0. removetop();
endwhile
S4: while (heap1.top().intervalQ[k].l01) do
heap1. removetop();
endwhile
S5: if ( heap0.top().value+heap1.top().value<C) then
return TRUE;
endfor;
return false
Lema 6.5
Există o valoare pentru variabila program k astfel încât la instrucțiunea Si (heap0.top().value+ heap1.top().value<C) dacă și numai dacă s0,s1:s0S0 and s1S1 and s0s1: s0.x+s1.x<C
Demonstrație
():
Fie: <i,min.(0,i)>=heap0.top() și <j, min x.(1,j)>= heap1.top(). heap0.top().value+heap1.top().value<C
(simplificând și aplicând I2)
min.(0,i)+min x.(1,j)<C and Q[k].loo<iQ[k].hio and Q[k].loo<jQ[k].hi1
(aplicând Lema 6.4)
min x.(0,i) + min x.(i,j)<C and (0,i) (1,j)
(aplicând Lema 6.1)
( s0,s1:s0S0 and s1S1 and s0s1:s0.x+s1.x<C)
():
( s0,s1:s0S0 and s1S1 and s0s1:s0.x+s1.x<C)
(aplicând Lema 6.1)
( i,j:(0,j)(1,j):min x.(0,i)+min x.(1,j)<C)
(conform Lemei 6.4, dacă KEY este în P0 atunci fie Q=Q0 și fie k numărul de mesaje recepționat de P0 înainte de KEY. La fel pentru KEY în P1. Atunci Q[k] corespunde la KEY)
Q[k].loo<iQ[k].lio and Q[k].lo1<iQ[k].li1 and min x.(0,1) + min x.(1,j)<C
(conform invariantului I1):
< i, min x.( 0, i) > heap0 and < j, min x.( 1, j) > heap0 and min x.(0,i)+min x.(1,j)<C
(conform invariantului HEAP):
heap0.top().value min x.(0,i) and heap0.top().value min x.(1,j) and min x.(0,i)+min x.(1,j) < C
heap0.top().value+ heap1.top().value < C
§6.2 Predicate relaționale cu N variabile booleene
În această secțiune vom considera cazul când există N variabile booleene de N procese și ne propunem să determinăm dacă există o stare globală în care cel puțin k din cele N variabile sunt adevărate. Vom nota cu xi variabila booleană a procesului i. Dacă eliminăm toate stările s ale lui Si pentru care s.xi sunt false atunci vom reduce mulțimea stărilor procesului i:
Ri={ ssSi and s.xi }
Vom defini (R,) poset-ul rezultant din reuniunea tuturor Ri-urilor. Problema găsirii unor probleme globale în S astfel încât cel puțin k din variabilele xi sunt adevărate este echivalentă cu găsirea unei tăieturi, sau antilanț, în (R,) de mărime cel puțin k. astfel revizuită problema devine de a determina dacă pentru o execuție dată există relația:
( c: c lo: c k) (PS2)
unde lo reprezintă mulțimea tuturor tăieturilor poset-ului redus (R ,).
Tehnica utilizată pentru rezolvarea problemei (PS2) se bazează pe teorema lui Dilworth care spune că mărimea maximă a unui antilanț într-un poset este egală cu numărul minim de lanțuri ale poset-ului.
Dându-se R deja partiționat în N lanțuri, Ri, ne propunem să determinăm dacă există un antilanț de mărime cel puțin k. conform teoremei lui Dilworth R poate fi partiționată în k-1 lanțuri dacă și numai dacă nu există un antilanț de mărime cel puțin k. Prin urmare, vom putea rezolva PS2 încercând să partițonăm R în k-1 lanțuri. Dacă avem succes atunci PS2 este falsă, atunci este adevărată. Ne apropiem de soluție dacă alegând k lanțuri încercăm să le fuzionăm și să obținem k-1 lanțuri. După un astfel de pas ne mai rămân k-1 lanțuri. Vom aplica acest pas de N-k+1 ori. Dacă eșuăm la o iterație atunci Rnu poate fi partiționat în k-1 lanțuri. Astfel există un antilanț c astfel încât c>k. Dacă avem succes atunci putem reduce R de k-1 lanțuri și deci nu există un antilanț c astfel încât c>k.
Algoritmul utilizează cozile pentru a reprezenta lanțurile. Fiecare coadă este constituită în ordine crescătoare, deci capul cozii este cel mai mic element din coadă. Un element reprezintă o stare, și o stare mai mică “se întâmplă înaintea” unei stări mai mari (acest lucru poate fi determinat prin compararea vectorilor (ceas al stărilor). Algoritmul utilizează operațiile curente cu cozi: insert (q,e), deletehead (q), empty (q), head (q).
Algoritmul FindAntiChain apelează funcția Merge de N-k+1 ori. Funcția Merge primește la intrare k cozi și returnează k cozi: Q1,…,Qk. Dacă Qk este returnat gol, atunci Merge a avut succes (rezultatul va fi în Q1,…,Qk-1) și Merge continuă o nouă iterație. Dacă Qk nu-i gol atunci un antilanț a fost găsit și este format din capetele cozilor.
function FindAntiChain (k: integer, Qlist: list of quenes of vector clocks): antichain
begin
assume: 1KQlist
assume: qQlist NOT empty (q)
for (n:= Qlist , nk, n:=n-1) do
(p1,…,pN):= Qlist;
(q1,…,qk):= Merge (p1,…,pk)
if (empty (qk)) then
Qlist:= (pk+1,…,pN,q1,…,qk-1) / rotate list/
else return ({head (qi)/1ik});
end
endfor;
return ()
end;
Există două decizii importante în acest algoritm. Prima este cum să alegem cele k lanțuri pentru operația de fuziune. Răspunsul este dat de tehnica clasică de fuziune folosită pentru sortare. Vom alege lanțurile care au participat la fuziune de cele mai puține ori. Din această cauză executăm rotația lui Qlist după fiecare operație de fuziune. Acest lucru reduce numărul de comparații reclamat de algoritm.
A doua și cea mai importantă decizie este cum să implementăm funcția Merge. Aceasta extrage un element de la una din intrările celor k lanțuri și îl inserează într-una din ieșirile celor k-1 lanțuri utilizate în acest scop. Ieșirea lanțului Qk este utilizată doar dacă funcția Merge eșuează, astfel când vom spune “ieșirea lanțurilor” ne vom referi doar la acele lanțuri folosite în cazul de succes: Q1,…,Qk-1. Va fi mutat elementul cel mai mic. Problema este să decidem la ieșirea cărui lanț plasăm acest element.
function Merge (P1,…,Pk:quenes):Q1,…,Qk:quenes;
const all={1,…,k};
var ac, move: subsets of all;
bigger: array [1..k] of 1..k;
G: initially any acyclic grople on k-1 vertices;
begin
ac:=
while (ack and NOT ( i:1ik: empty (Pi))) do
move:={}
for iall-ac and jall do
if head (Pi)<head(Pj) then
move:= move {i};
bigger [i]:= j;
end;
if head (Pj)<head(Pi) then
move:= move {j};
bigger [i]:= j;
end;
endfor
for i move do
dest:= Find Q(G, i, bigger[i]);
x:= deletehead (Pi)
insert (Qdest,x);
endfor
ac:= all-move;
endwhile
if ( i: empty (Pi)) then
FinishMerge (G,P1,…,PK,Q1,…,QK-1);
R1: return (Q1,…,QK-1,)
else
R2: return (P1,…,Pk);
end.
Subrutina FindQ rezolvă problema deciderii alegerii lanțului la ieșirea căruia plasăm elementul pe care trebuie să-l mutăm. Această funcție utilizează trei parametrii:
G= un graf neorientat numit “graful cozilor de inserție”
i= intrarea cozii de la care elementul i va fi șters
j= coada în care toate elementele sunt mai mari ca x
G este folosit pentru a se deduce coada în care următorul element este inserat. G are k noduri și k-1 muchii. O muchie corespunde la ieșirea unei cozi și un nod la intrarea unei cozi. Prin urmare fiecare muchie (i,j) are o etichetă, label (i,j){1,…,k-1} care identifică coada căreia îi corespunde. Nu există etichete duplicat, deci fiecare ieșire de coadă este reprezentată exact o singură dată. Similar fiecare intrare de coadă este reprezentată exact o dată.
O muchie (i,j) între nodurile i și j înseamnă că capetele lui Pi și Pj sunt mai mari decât elementele lui Qlabel(i,j). Scopul nostru este să na asigurăm că pentru fiecare intrare de coadă (adică: nod) există o ieșire de coadă (adică: muchie) în care capul intrării cozii poate fi inserat. Această constrângere este echivalentă cu cererea ca profilul să fie arbore.
Când apelăm FindQ(G,i,j), elementul de șters este ei=head(Pi) și este mai mic decât ej=head(Pj), adică: bigger [i]=j. FindQ adaugă muchia (i,j) la G. deoarece G era arbore de dinainte prin adăugarea muchiei (i,j) se poate crea un ciclu. (dacă muchia (i,j) nu aparținea și înainte lui G). Fie (i,k) o altă muchie incadentă cu nodul i care să aparțină acestui ciclu. FindQ șterge (i,k) și adaugă (i,j) și etichetează muchia (i,j) cu eticheta lui (i,k). FindQ returnează această etichetă care va indica cărei cozi ei va fi atașat.
function FindQ (G:graph; i,j:1..k):label;
add edge such that (i,j) to G;
(i,k):= the edge such that (i,j) and (i,k) are part of tha same
cycle in G;
remove edge (i,k) from G;
label (i,j):=label (i,k);
return label (i,j);
end.
Lema 6.6
Dacă (i,k)G atunci
empty (Qlabel(i,k))(e:ePiPk:tail (Qlabel(i,k))e)
Demonstrație
Inițial lema are loc deoarece toate ieșirile cozilor sunt goale.
Vom presupune că lema are loc și că trebuie să inserăm elementul ei=head(Pi) în ieșirea cozii Ql unde l=FindQ (G,i,j) și j=bigger [i]. Deoarece j=bigger [i] avem eihead (Pj). Deoarece Pi și Pj sunt sortate, avem eie pentru orice ePiPk. După mutarea lui ei în Ql, tail(Ql)=e și lema are loc din nou.
Lema 6.7
Dacă elementele sunt inserate în ieșirile cozilor utilizând FindQ, atunci acestea sunt de asemenea sortate.
Demonstrație
Inițial ieșirile cozilor sunt goale. Vom presupune că fiecare ieșire de coadă este sortată și că vom avea nevoie să mutăm ei=head(Pi) în ieșirea unei cozi. Procedura FindQ returnează Qlabel(i,j) unde (i,j) este o muchie din G. Conform lemei anterioare tail (Qlabel(i,j))ei, astfel inserând ei în Qlabel(i,j), Qlabel(i,j) rămâne sortată. Nici o altă ieșire de coadă nu-i modificată și prin urmare lema are loc.
Lema 6.8
Presupunem (Qi,…,Qk)=Merge (P1,…,Pk) și că fiecare coadă Pi este sortată. Atunci:
empty (Qk)P1,…,Pk pot fi formate în k-1 cozi Q1,…,Qk-1
NOT empty (Qk){ head (Pi)1ik} este un antilanț de mărime k
NOT empty (Qk) există un antilanț de mărime k.
Demonstrație
Vom utiliza următorul invariant al buclei while:
iac and jac and NOT empty(Pi) AND NOT empty(Pj) head (Pi)head (Pj)
(A): Presupunem empty (Qk).
Atunci subrutina Merge se termină la instrucțiunea R1 și înainte de-a se termina există i astfel încât empty (Pi). Pentru simplitate vom presupune Pk goală. Elementele vor fi în acest moment în P1,…,Pk-1 sau Q1,…,Qk-1 și folosindu-ne de conexitatea lui G putem trage concluzia că P1,…,Pk au fuzionat în cozile Q1,…,Qk-1. Lema anterioară ne asigură că Q1,…,Qk-1 sunt sortate.
(B): Presupunem NOT empty (Qk).
Atunci subrutina Merge se termină la instrucțiunea R2 și înainte terminare nu există i astfel încât empty (Pi). Atunci conform invariantului și faptului că all=ac deducem că head (Pi) sunt concurente i. Astfel {head(Pi)1ik} este un antilanț de mărime k.
(C): Se aplică (A), (B) și teorema Dilworth.
q.e.d
Teorema 6.1
Există un antilanț de mărime k dacă și numai dacă FindAntiChain (P1,…,Pk) returnează un antilanț de mărime k.
Demonstrație
Presupunem că există un antilanț de mărime k, atunci conform teoremei Dilworth nu poate fi fuzionat în k-1 lanțuri. Aplicând Lema 6.8 deducem că funcția Merge returnează un antilanț de mărime k.
Presupunând că nu există un astfel de antilanț, poate fi fuzionat în k-1 lanțuri și funcția Merge se termină cu Pk goală după N-k+1 iterări ale buclei while, din care cauză FindAntiChain returnează mulțimea vidă.
§6.3 Predicate pentru sume măginite
în această secțiune, vom descrie o tehnică care poate fi utilizată în calcularea predicatelor definite ca margini de sume variabile ale unor programe distribuite. Predicatul (x1+x2+…+xN<k) aparține acestei clase de predicate, notațiile fiind cele obișnuite.
Formal procedeul poate fi scris astfel:
G: consistent(G):
și compararea acestuia cu valoarea constantei k.
Vom transforma deposet-ul într-un flux astfel încât fluxul maxim să fie egal cu valoarea minimă a deposet-ului. Modul de constituire a fluxului este următorul:
G:=(V;E) unde V= Si {source, sin k}
Arcele fluxului vor fi constituite astfel:
Pentru început, tratăm arce între source și toate stările inițiale s, cu capacitate .
Pentru oricare două stări s și t astfel încât … adaugă un arc între ele de capacitate sx
Pentru oricare două stări s și t astfel încât …, vom identifica succesorul lui s, …, după care adăugăm un arc
Teorema 6.2
Valoarea minimă a unui deposet S este egală cu tăietura minimă al fluxului asociat G.
Demonstrație
Vom asocia o tăietură din flux unei tăieturi din deposet după cum urmează: Dacă arcul e leagă nodurile s și t din G și e face parte din tăietura fluxului G, atunci starea corespunzătoare lui s face parte din tăietura deposet-ului S.
Vom observa că orice tăietură consistentă a deposet-ului partiționează fluxul astfel încât source și sin k sunt izolate.
De asemenea se observă că o tăietură din G are valoare finită dacă și numai dacă tăietura corespunzătoare din S este consistentă.
Capitolul 7. Predicate globale
§7.1 Secvențe globale
O rulare r definește o ordine parțială () peste mulțimea stărilor, unde r[i] desemnează secvența stărilor lui Pi. În general, există mai multe ordini totale constituite cu această ordine parțială. O secvență globală corespunde unei singure liniarizări ale acestei rulări, este o secvență de stări globale, unde o stare globală este un vector de stări locale. Vom nota mulțimea secvențelor globale consistente cu o rulare r ca linear (r). o secvență globală g este o secvență finită de stări globale notată g=g1 … gl, unde gk este o stare globală pentru 1kl. un prefix sfârșind cu gk (adică g1g2…gk) este notat cu gk. putem observa că restricția acestuia la un singur proces Pi este r[i] sau o “bâlbâială” a lui r[i]. Printr-o bâlbâială a lui r[i] vom înțelege o secvență finită de stări ale lui r[i], în care anumite stări se pot repeta de un număr de ori, adică printr-o compactare vom obține r[i].
Definiția 7.1
g este o secvență globală a unei rulări r (și notăm glinear (r)) dacă și numai dacă:
S1: i: g restricționat la Pi este r[i] sau o bâlbâială a lui r[i] (notăm stutter (r[i]))
S2: k: gk[i]gk[j] unde prin gk[l] s-a notat starea lui Pl din starea globală gk.
§7.2 Logica predicatelor globale
Logica predicatelor globale operează cu trei categorii sintactice: bool, lin și form. Sintaxa logicii noastre este:
form::=A : lin E : lin
lin::= lin lin lin lin AND lin NOT lin bool
bool::= un predicat peste o stare globală
Un “bool” este o expresie booleană definită peste o singură stare globală a sistemului. Valoarea sa poate fi determinată dacă respectiva stare globală este cunoscută.
Un “lin” este o expresie temporală definită peste o secvență globală. Un “bool” este adevărat pentru o secvență globală dacă este adevărată pentru ultima stare a lui g.
Un “form” este definit pentru o rulare și este un “lin” cuantificat cu unul dintre cuantificatorii A (cuantificatorul universal) sau E (cuantificatorul exostențial).
Semantica în logica predicatelor globale este:
gbool dnd gmbool, unde gm= ultima stare a lui g
gNOT lin dnd NOT (glin)
glin1 AND lin2 dnd glin1 AND glin2
glin1 OR lin2 dnd glin1 OR glin2
g lin dnd i: gilin
g lin dnd i: gilin
r A: lin dnd g:glinear (r): glin
r E: lin dnd g:glinear (r): glin
Vom numi formulele care încep cu A: ca formule tari și cele care încep cu E: formule slabe.
§7.3 Predicate conjunctive tari
Un predicat conjuctiv tare este adevărat dacă și numai dacă sistemul poate atinge o stare globală pentru care toate predicatele locale sunt adevărate. Formal: A: (LP1 AND…AND LPn).
Un interval, I1 este o secvență de stări consecutive ale unei urme având o stare de început (notat I.lo) și o stare de sfârșit (notat I.hi). Vom conveni I.lo<I.hi.
O mulțime de intervale, I1,…,In, aparținând diferitelor procese se numește overlap, notăm overlap (I1,…,In), dacă și numai dacă:
i,j: i,j{1,…,m}: Ii.loIj.hi
Vom nota cu LPi predicatul local al procesului Pi și cu LPi(s) notăm că predicatul LPi este adevărat în starea s. Vom presupune că predicatele locale LPi sunt constituite cu variabile locale ale procesului Pi. Aceasta înseamnă că valoarea de adevăr al predicatului LPi poate fi schimbată doar de un eveniment intern. Adică:
(A1) Dacă (LP(s) AND NOT LP(next.s)) OR (NOT LP(S) AND LP(next.s)) atunci:
ts dnd tnext.s și
st dnd next.s t pentru toți t diferiți de s sau next.s.
Vom folosi i ca valoare santinelă a procesului Pi, starea de dinaintea începerii execuției procesului Pi și cu Ti, valoarea santinelă, starea de după terminarea execuției procesului Pi.
(A2) Vom presupune că LPi este falsă în i sau Ti pentru orice i.
Lema 7.1
I1,…,In: LP1(I1) AND…AND LPn(In) AND overlap (I1,…,In) A: (LP1 AND…AND LPn)
Demonstrație
Evident, folosind definițiile.
Definiția 7.2
O secvență globală g=g1,…,gm se numește pură dacă și numai dacă k: NOT gk=LP1 AND…LPm
Fie x o stare globală coexistentă. Vom nota cu first(x) un m-tuplu de intervale (I1(x),…,Im(x)), unde Ik(x) este primul interval din r[k] care sfârșește după starea x[k] în care LPk este adevărată.
Definiția 7.3
x se numește stare globală intermediară admisibilă dacă și numai dacă:
first (x) nu există sau
k,l: Ik(x).lo-/->Il(x).hi AND NOT LPk(x[k]) AND (I: X[I]=i OR ( j: prev.x[i] x[j]=next.(I.hi) pentru un interval I oarecare))
A doua disjuncție spune că există două intervale Ik și Il astfel încât să nu formeze overlap(Ik(x).b-/->Il(x).hi) și LPk să nu fie adevărată în starea x[k]. Mai mult, x este minimal cauzal cu respectarea stării next.(I.hi) pentru un interval I.
Lema 7.2
not I1 ,…,Im : LP1(I1) and … and LPm(Im) and overlap(I1,…,Im)
not A : ◊ ( LP1 and … and LPm )
Demonstratie
Pentru o stare globala x , notăm cu I(x) mulțimea tuturor m-tuplelor de intervale în care LPi este adevarată , după starea locală x[i] .
Obiectivul nostru este să construim o secvență globală pură g de la start=( 1,…,m ) la stop=( T1,…,Tm ) . Fie x o stare globală astfel încât am construit o secvență globală pură de la start la x , rămane să construim o secvență globală pură de la x la stop.
Inițial, alegem x=start. Vom construi o secvență globală pură de la x la un y astfel încât card(I(y))<card(I(x)). Continuând în această maniera vom atinge o stare globală z în care card(I(z))=0. Din acest punct toate secvențele globale sunt pure.
Se observă imediat că starea start este pură.
Vom presupune că avem o stare globala admisibilă x pentru care card(I(x))>0. Pentru 1≤j ≤m, fie Ij primul interval în r[j] în are LPj este adevarat și se sfârșește dupa starea x[j]. Deoarece x este admisibilă și first(x) există ( card(I(x))>0 ), atunci există k,l astfel încât Ik(x).lo –/ Il(x).hi si NOTLPk(x[k]). Vom defini s ca starea locala next.( Il(x).hi ). Conform ipotezei ( A2 ) aceasta stare există. Vom construi o secvență globală de la x la o alta stare globală admisibilă y, unde y este definita ca fiind starea globală consistentă minimă după x astfel încât y[l]=s. O astfel de stare există deoarece mulțimea tuturor tăieturilor consistente este o latice.
Vom arata că LPk nu este adevarat niciodată între x[k] și y[k]. Pentru aceasta este suficient să arătăm că y[k]< Ik(x).lo. Cunoaștem că Ik(x).lo –/ Il(x).hi, aplicând ( A1 ) rezultă prev.( Ik(x).lo ) –/next.( Il(x).hi ). Astfel există o stare globală consistentă z conținând s astfel încât z[k] prev.( Ik(x).lo ). Deoarece y este starea globală consistentă minimă cu y[l]=s, avem că y[k] ] prev.( Ik(x).lo ). Aceasta implică faptul că LPk nu este niciodată adevarat între x[k] si y[k]. Astfel, toate secvențele globale dintre x si y sunt pure.
Vom arata că y este admisibil. Dacă first(y) nu există atunci evident. Presupunem că first(y) există. Din ipoteză avem că exista k’, l’ astfel încât Ik’(y).lo –/ Il’(y).hi. Dacă NOTLPk’(y[k’] ), atunci y este admisibil. Presupunem y[k’] Ik’(y). Deoarece y este minimal cauzal cu respectarea lui s, avem : prev.y[k’] s sau y[k’]=x[k’].
Cazul 1: prev.y[k’] s
Conform ( A1 ) aceasta este echivalent cu Ik’ (y).lo Il(x).hi.
Vom arata că Il(y).lo –/ Il’(y).hi AND NOT LPl(y[l]). NOT LPl(y[l]) este evident. Deoarece Ik’ (y).lo Il(x).hi și Il(x).hi < Il(y).lo avem Ik’ (y).lo Il(y).lo. Prin urmare, Il(y).lo Il’(y).hi este in contradicție cu Il(y).lo –/ Il’(y).hi. Astfel am arătat că Il(y).lo –/ Il’(y).hi. Din construcție y este cauzal minimal.
Cazul 2: y[k’]=x[k’]
Deoarece x este admisibil, există j astfel încât prev.x[k’] x[j] AND x[j]=next.(I.hi). Dacă x[j]=y[j], atunci y este admisibil deoarece Ij(y).lo –/ Il’(y).hi AND NOT LPj(y[j]). Ij(y).lo Il’(y).hi, prev.x[k’] x[j], x[k’]=y[k’] și x[j]=y[j] contrazice Ik’(y).lo –/ Il’(y).hi. Dacă x[j] y[j], atunci prev.y[j] s. Din y[k’]=x[k’], prev.x[k’] x[j], x[j] < y[j] și prev.y[j] s avem prev.y[k’] s, și se tratează similar cazului anterior.
Vom spune că predicatul firstlmr(I) este adevărat dacă și numai dacă predicatul local este adevarat în I pentru prima dată de la ultimul mesaj recepționat ( sau de la inceputul procesului ). Vom spune că scp( I1 ,…,Im ) este adevărat dacă I1 ,…,Im sunt intervale in diferite procese și realizeaza SCP adevărat.
Teorema 7.1
I1 ,…,Im : scp( I1 ,…,Im )
J1,…,Jm : scp( J1,…,Jm ) AND k : 1 k m : firstlmr( Jk )
Demonstratie
Datorită simetriei este suficient să demonstrăm existența unui J1 astfel încât scp( J1,…,Jm ) AND firstlmr( J1 ).
Fie J1 astfel încât firstlmr( J1 ). Vom arăta overlap( J1, Ik ) pentru 2 k m. Pentru orice k, I1.lo Ik.hi si J1.lo I1.lo implică J1.lo Ik.hi. Deoarece avem overlap( Ik , I1 ) : Ik .lo I1.hi și deoarece nici un mesaj nu a fost recepționat după J1.hi și înainte de I1.hi , mesajul care a provocat Ik .lo I1.hi trebuie să fi avut loc inainte de J1.hi. Prin urmare avem Ik .lo J1.hi.
Deci overlap( J1, Ik ).
Procesul controlor , al unui algoritm de detecție a SCP, asociază fiecarui proces câte o coadă , unde va stoca mesajele provenite de la respectivele procese . Fie I si J intervale în procesele PI si Pj cu vectorii pereche x si y. Atunci este usor de văzut că overlap( I , J ) este echivalent cu ( x.lo < y.hi ) AND ( y.lo < x.hi ).
Lema 7.3
Fie x si y doi vectori pereche din vârfurile cozilor respective. Daca ei nu formează overlap , atunci cel putin unul dintre ei poate fi eliminat dintre candidații pentru satisfacerea SCP.
Demonstratie
x si y nu formează overlap NOT ( x.lo < y.hi ) sau NOT ( y.lo < x.hi )
Vom presupune că există un x’ distinct de x din coada lui x astfel încât sa formeze overlap cu y , adică overlap(x’,y) ,deci x’.lo y.hi.
Deoarece x.lo x’.lo rezultă x.lo y.hi , contradicție.
Capitolul 8. Predicate ale fluxului de control
§8.1 Introducere
In acest capitol vom folosi o structura de date numită “arbust etichetat “ ( LRDAG – label rooted directed acyclic graph ). Pentru a ințelege această structură considerăm subposet-ul format din starea locala s S si toate starile care preced cauzal s. Acest subposet , numit past ( prefix closure ) a lui s si notat dag(s) formează un arbust ( DAG – rooted direct acyclic graph ) a cărui rădăcină este s , arcele fiind orientate către rădăcină :
dag(s) := S restricționat la { s } { s’ : s’ s }
Fie A o multime de etichete si λ o functie de la S la 2A ( multimea parților lui A ). Fiecarei stari locale s îi asociem o etichetă λ(s). Aceste etichete reprezintă expresii booleene evaluate in starea locală s ; prezența unei etichete in λ(s) inseamnă că expresia booleană asociată , predicatul local , evaluată in s este adevarată. Dacă o stare locala s nu satisface nici un predicat , atunci λ(s) = {}. Predicatele locale pot fi asociate cu astfel de etichete. Aceste structuri le vom numi LRDAG.
§8.1 Logica LRDAG
Pentru inceput prezentăm sintaxa acestei logici :
p A
x X
f = p | ◊l x | ◊m x | ( NOT f ) | ( f AND f )
B := card( X ) , X := { x1,…, xB }
O proprietate este descrisă de o mulțime de B ecuații care definesc fiecare variabilă logică din X ( fI sunt formule ).
x1 := f1
…
xB := fB
Semantica logicii LRDAG :
Fie s S ,
s |= xj s |= fj
s |= ◊l xj ( s’ : s’ <im s : s’ |= xj )
s |=◊m xj ( s’ : s’ ~~> s : s’ |= xj )
s |= p p λ(s)
s |=f AND f’ ( s |= f ) AND ( s |= f’ )
s |=( NOT f ) NOT ( s |= f )
s |= initial NOT ( s’ : s’ <im s )
s |= receive ( s’ : s’ ~~> s )
s |= external ( s |= send ) OR ( s |= receive )
§8.3 Exemple
Exemplul 1 : Invarianța si Existența in Past-ul local
Dacă definim x1 astfel :
x1:= p AND ( NOT initial ◊l x1 )
atunci x1 este adevărat în s dacă și numai dacă :
s |= ( p AND ( initial OR ◊l x1 ) ) .
Dacă s este o stare inițială , atunci x1 este adevărată dacă și numai dacă p este eadvărat , altfel x1 este adevărată dacă și numai dacă p este eadvărat si x1 este adevărată pentru starea locală imediat precedentă lui s. Urmează , prin inducție , că x1 este adevărată în s dacă și numai dacă p este adevărată in toate stările locale care preced pe s. Deci termenul de invariant se justifică.
Duala invariantei , existența , se poate formaliza :
x1:= p OR ◊l x1 .
Exemplul 2 : Invarianța si Existența in Past-ul global
Past-ul global al unei stări locale s este multimea :
{ s’ : s’ dag(s) }.
O eticheta p este invariantă in past-ul global al lui s dacă și numai dacă p λ(s’) pentru toți s’ dag(s) . Aceasta se poate formaliza:
x1:= p AND(NOT initial ◊l x1 ) AND ( receive ◊m x1 )
Duala invarianței , existența , se poate formaliza :
x1:= p OR ◊l x1 OR ◊m x1
Exemplul 3 : Intervale abstracte
Vom spune că external este true dacă și numai dacă a evenimentul precedent stării în care se evaluează este sent sau receive. Considerăm secvența de stări ale procesului Pi : ( s0i…snI). Această secvența este partiționată în subsecvențe de către evenimentele externe. Aceste subsecvențe se numesc intervale.
Considerând specificația :
x1:= p OR (NOT external AND ◊l x1 )
x1 este adevărată în s dacă și numai dacă p este adevărat în cel puțin o stare locală de la ultimul eveniment external.
Exemplul 4 : Expresii regulate
Fie un limbaj peste un alfabet finit ( de etichete ). Pentru o stare locală s , vom spune că proprietatea asociată limbajului , este satisfacută dacă unul din drumurile etichetate a lui dag(s) aparține limbajului. Mulțimea tuturor drumurilor etichetate ale lui dag(s) este notată STRINGS(s). Formal șirul ( α0α1 … αn ) este în STRINGS(s) dacă și numai dacă exista o secvență de stări (σ0σ1…σn) astfel încât :
σ0 este stare inițiala
pentru 0 k < n , σk <im σk+1 OR σk ~~> σk+1
σn = s
pentru 0 k n , dacă λ( σk ) { } atunci αk λ( σk )
altfel αk = ε
Reamintim definiția automatului finit determinist :
M = ( Q , A , q1 , QF , δ )
unde Q = { q1,…,qB } , B = card(Q) , mulțimea stărilor
A = mulțimea ( etichetelor ) simbolurilor de intrare
q1 Q starea inițiala
QF Q mulțimea stărilor finale
δ : Q X A 2Q funcția de tranziție
Vom spune că xj este adevărat în s dacă și numai dacă există un șir din STRINGS(s) care va plasa automatul în starea qj.
Vom nota ◊ xk expresia ◊l xk OR ◊l xk.. Fie
Tj = { ( α AND ◊ xk ) : qj δ( qk , α ) AND α A AND k { 1,…,B} }
Tj reprezintă toate tranzițiile automatului care intră în starea qj. Cele B ecuații ce definesc xj sunt urmatoarele :
x1 := initial OR f1
xj := fj j { 2,…,B } cu fj := V { t : t Tj }
Exemplul 5 : Proprietați non-secvențiale
Presupunem ca avem o matrice D , partiționată în N submatrici Di , pentru j { 1, … , N }. Matricea , care inițial a fost atribuită procesului P1 , este distribuită proceselor PI , după care este din nou colectată în P1.
i.owns.Dj λ(s) sSi AND s are în sarcină Dj
1.owns.D λ(s) sS1 AND s are în sarcină D.
Ecuațiile sunt :
y1:=1.owns.D
x1 := 1.owns.D1 AND ◊y1
…
xN := N.owns.DN AND ◊y1
z1 := 1.owns.D AND ( i : 1 i N : ◊xI )
§8.4 Algoritmul descentralizat pentru detecție
Algoritmul utilizează macroinstructiunea evalj care expandează fj :
evalj(◊lx1,…,◊lxB,◊mx1,…,◊lxB)
Local Variables
Boolean : Xj , Xlj , Xmj for j { 1,…,B } ;
Initially
(S1) for j := 1 to B do
Xj := evalj( false ,…, false )
Upon sending a message
(S2) Tag message with ( X1 ,…, XB ) ;
Upon entering new local state s
(S3) if ( previous event was message receive ) then
( Xm1 ,…, XmB ) := message tag
else
( Xm1 ,…, XmB ) := ( false ,…, false )
(S4) ( Xl1 ,…, XlB ) := ( X1 ,…, XB )
/* evaluation of each fj in state s */
(S5) for j := 1 to B do
Xj := evalj( Xl1 ,…, XlB , Xm1 ,…, XmB )
Teorema 8.1
( P ) s |= xj variabila locala Xj este adevărată în starea s
Demonstratie
Vom folosi inducția după rangul stării s. Prin rang(s) înțelegem lungimea maximă a unui drum in dag(s) de la o stare inițială la s.
Pasul inițial :
rang(s) = 0 s este stare inițială ( P ) se verifică
Pasul inductiv :
Vom admite că ( P ) este adevărată pentru toate stările v astfel încăt rang(v) k și considerăm s stare în procesul PI astfel încăt rang(s) = k+1. Pentru început vom arăta că Xl si Xm au valori corecte.
s are un predecesor local s’ al cărui rang este cel mult k , deci folosind ipoteza inductivă și instrucțiunea ( S4 ) obținem:
s’ |= xj Xlj este adevărat in starea s
dacă un mesaj a fost receptionat exact înainte de s atunci s are un predecesor îndepărtat s” al cărui rang este cel mult k , deci folosind ipoteza inductivă și instrucțiunea
( S3 ) obținem:
s” |= xj Xmj este adevărat în starea s
dacă nici un mesaj nu a fost recepționat atunci s nu are predecesor îndepărtat și conform ( S3 ) toate variabilele Xmj sunt false în starea s.
Deoarece Xl si Xm au valori corecte și datorită definiției lui evalj instrucțiunea ( S5 ) calculează noua valoare astfel :
s |= xj variabila locală Xj este adevarată în starea s
Capitolul 9. Relații de ordine
§ 9.1 Relații de ordine între mesaje
Relațiile de ordine dintre mesaje se bazează pe relațiile de precedență cauzală. Vom utiliza urmatoarele notații :
S = mulțimea tuturor evenimentelor de transmitere
R = mulțimea tuturor evenimentelor de recepție
I = mulțimea tuturor evenimentelor interne
E = mulțimea tuturor evenimentelor din sistem
S[ i , j ] = mulțimea evenimentelor de transmitere de la procesul Pi către procesul Pj .
Modurile de comunicație sunt următoarele :
FIFO : Oricare două mesaje transmise de la procesul Pi către procesul Pj sunt recepționate în ordinea transmiterii lor :
s’ < s” NOT ( r” < r’ ) ( FIFO )
Ordonarea cauzală : Dacă avem două evenimente de transmisie în care primul îl precede cauzal pe cel de-al doilea, atunci mesajul al doilea nu poate fi receptionat înainte de primul.
Sincronizare : Mesajele sunt transmise și recepționate la
același moment de timp. Adică există funcția T
T : E N : s,r,e,f E-I
s ~~> r T(s) = T(r) si
e < f T(s) < T(r) ( SYNC )
Teorema 9.1
Ierarhia asociată modurilor de comunicație este
SYNCCO FIFO ASYNC
Demonstratie
Evidenta.
§9.2 Ordinea FIFO a mesajelor
Vom presupune că fiecare canal este unidirecțional și că de la un proces către alt proces nu există mai mult de un canal. Vom admite că există C canale în sistem.
Fiecare proces menține un vector v de întregi, s.v[j] reprezintă numarul de mesaje transmise/recepționate de către procesul s.p pe canalul j.
PI : :
Var
v : array[1..C] of integer initially 0;
( F1 ) ( s, send(u) along channel j, t )
t.v[j]:=s.v[j] + 1
( F2 ) ( s, receive(u) along channel j, t ) : enabled when s.v[j]=u.v[j]
t.v[j]:=s.v[j] + 1
Lema 9.1
Fie s’ , s” S , r’ R , e ,f E , atunci :
s’ < s” s’.v[c] < s”.v[c]
e < f e.v < f.v
s’ ~~> r’ r’.v[c] = s’.v[c] + 1
Demonstratie
Evidentă.
Teorema 9.2 ( siguranța )
Considerând două mesaje s’ ~~> r’ și s” ~~> r” , avem
s’ < s” NOT( r” < r’ )
Demonstratie
Dacă r’.p r”.p atunci este evident.
Presupunem r’.p = r”.p , aceasta implică faptul că s’ si s” folosesc același canal, să zicem c. Fară să pierdem din generalitate putem presupune că s’ și s” sunt mesaje consecutive. Conform lemei anterioare s’ < s” implica s’.v[c] < s”.v[c]. Mai departe, s’~~>r’ implică r’.v[c] = s’.v[c] + 1 și s”~~>r” implică r”.v[c] = s”.v[c] + 1. Prin urmare, r’.v[c] < r”.v[c]. Aceasta implică NOT( r”.v r’.v ) deci NOT( r” r’ ) .
Teorema 9.3 ( vitalitate )
În ipoteza că nici un mesaj transmis nu este pierdut, în cele din urmă toate mesajele transmise sunt recepționate.
Demonstratie
Fie chainn[r,s] mulțimea tuturor mesajelor canalului dintre procesele Pr.p si Ps.p transmise înainte de starea r și recepționate înainte de starea s. Fie g mesajul cu minimul g.v[c] în chann[r,s]. Vom arăta că g va fi recepționat. Deoarece g are v[c] minim din chann[r,s], toate celelalte mesaje cu v[c] mai mici decât g și care s-au vehiculat pe același canal cu g, au fost deja recepționate. Deoarece v este incrementat după fiecare recepție avem s.v[c]=g.v[c]. Prin urmare, g este recepționat în starea s.
Fapt
Presupunând că protocolul pentru ordonarea FIFO se bazează pe întârzierea recepționărilor, acest protocol va trebui să folosească identificatori distincți pentru mesaje distincte.
Demonstratie
Altfel nu s-ar putea cunoaște despre care mesaj este vorba.
§9.3 Odinea cauzală a mesajelor
Fiecare proces menține o matrice m de intregi, s.m[j,k] reprezintă numarul de mesaje transmise de la procesul j la procesul k, cunoscut de procesul s.p in strea s.
Pi : :
Var
m : array[1..N,1..N] of integer initially 0;
( C1 ) ( s, send(u), t ) : m[s.p, u.p]++;
( C2 ) ( s, recv(u), t ) : enabled when k : s.[k,i] u.m[k,i]
m[u.p,s.p]++;
t := max(s,u)
Lema 9.2
Fie e, f E , atunci
1. e f e.m f.m
2. fie s’, s” S[ i , j ], atunci
s’ < s” s’.m[ i , j ] < s”.m[ i , j ]
3. fie s’ S , w E , s’ w s’.m[s.p,w.p]<w.m[s.p,w.p]
Demonstratie
Evidentă, folosind inducția.
Vom defini o variabilă auxiliară, pred , astfel :
s.pred[k,l] := card{ u S[k,l] : u s }
astfel s.pred[k,l] este egal cu numarul de evenimente de transmitere de la k la l care preced cauzal s.
Lema 9.3
s.m[k,l] = s.pred[k,l]
Demonstratie
Evident.
Teorema 9.4 ( siguranța )
s’ s” NOT( r” < r’ )
Demonstratie
Dacă r’.p r”.p atunci este evident.
Presupunem că r’.p = r”.p. Vom folosi inducția după n, numarul total de mesaje recepționate de procesul r’.p.
Dacă n=0 , atunci este evident.
Vom presupune că proprietatea de siguranța este satisfacută pentru primele n-1 mesaje și vom arăta că și al n-lea mesaj menține proprietatea adevărată. Vom folosi metoda reducerii la absurd , vom arăta că ( s’ s” ) AND ( r” < r’ ) conduce la o contradictie. Vom presupune că r” corespunde celui de-al n-lea mesaj și că mesajul r’ nu a fost încă recepționat. Fie w starea în care al n-lea mesaj este recepționat. Deoarece s’ s” , avem s’.m[s’.p,r’.p] < s”.m[s’.p,r’.p]. Până la starea w, procesul r’.p a recepționat cel mult s’.m[s’.p,r’.p] mesaje de la s’.p. Vom presupune că s’ n-a fost recepționat. Nici un mesaj transmis după s’ nu este recepționat pentru că s-ar încălca ipoteza inductivă. Din program deducem w.m[s.p,r’.p] s’.m[s’.p,r’.p], ceea ce implică w.m[s’.p,r’.p] s”.m[s’.p,r’.p]. Conform condiției de recepție, cunoaștem că în acest punct nu este posibilă recepția de la s”, ceea ce contrazice alegerea lui w.
Teorema 9.5 ( vitalitate )
În ipoteza că nici un mesaj transmis nu este pierdut, în cele din urma toate mesajele transmise au fost receptionate.
Demonstratie
Fie chann(G,s) mulțimea tuturor mesajelor transmise către procesul s.p care traverseaza tăietura consistentă G ( care include starea s ).
Fie M = min(chann(G,s)) mulțimea mesajelor minimale din chann(G,s) cu respectarea relației de precedența cauzală. Fie gM. Vom arăta că g este recepționat. Folosim metoda reducerii la absurd. Dacă g nu este recepționat în s atunci există k astfel încât s.m[k,s.p] < g.m[k,s.p]. Fie g.m[k,s.p] = y , deci există y mesaje transmise de procesul k către procesul s.p care preced cauzal mesajul g. Dacă toate aceste mesaje sunt recepționate înainte de starea s , atunci s.m[k,s.p] = g.m[k,s.p], contradicție. Astfel ar exista un mesaj care ar precede cauzal g și nu este recepționat înainte de s, cea ce ar insemna g M.
§9.5 Ordonarea sincronă a mesajelor
Pentru început vom introduce noțiunea de coroană.
Definitie
O coroană ( de mărime k ) este o secvență
< ( si,ri ) , i { 0,1,…,k-1 } : si~~>ri > astfel încât :
s0 r1, s1 r2, sk-2 rk-1, sk-1 r0
Teorema 9.6
Un calcul este sincron dacă și numai dacă nu admite coroane.
Demonstratie
SYNC NOT CROWN :
Deoarece calculul este sincron există o funcție T satisfăcând SYNC, și pentru oricare două evenimente e și f astfel încât ( ef ) AND NOT( e~~>f ) avem T(e) < T(f). Presupunând prin absurd că avem o coroană de mărime k, s0 r1, s1 r2, sk-2 rk-1, sk-1 r0 , aceasta implică :
i { 0, 1,…,k-1 } T(sI) < T( r(i+1) mod k ) ( * )
i { 1, 2,…,k-1 } T(si) = T(ri) ( **)
Prin urmare, ( * ) si ( ** ) implică : T(s0) < T(r0) care contrazice ipoteza SYNC : T(s0) = T(r0)
NOT CROWN SYNC :
Dându-se un calcul, vom construi un graf orientat G(E,V) după cum urmează. Mulțimea de noduri V va consta din toate mesajele , vi = { si, ri }. Vom trasa un arc de la vi la vj dacă există un eveniment e vi și un eveniment f vj astfel încât e f. Adică, ( vi vj ) E dacă și numai dacă ( si sj ) OR (si rj ) OR ( ri sj ) OR ( ri rj ). Deci , ( vi vj ) E , dacă și numai dacă si rj .
Deoarece calculul nu admite coroane, graful G astfel construit este aciclic și prin urmare poate fi etichetat topologic. Deci există o funcție T : E N care satisface ( SYNC ).
Definitie
O coroana tare ( de marime k ) este o secvență
< ( si,ri ) , i { 0,1,…,k-1 } : si~ri > astfel încât :
s0 < r1, s1 < r2, sk-2 < rk-1, sk-1 < r0
Algoritmul care implementează ordonarea sincronă are trei componente : execuția cu priorități ( PR – priority rule ), condiția de transmitere ( SC – send condition ) și condiția de recepție ( RC – receive condition ) . Pentru realizarea ordonarii sincrone sunt utilizate mesaje de control. Aceste mesaje, de control , nu reclamă satisfacerea ordonării sincrone. Vom nota cu E evenimentele care satisfac ordonarea sincronă și cu Ec transmiterea și recepționarea mesajelor de control.
O descriere neformală a algoritmului este urmatoarea:
Când un proces Pi dorește să interacționeze cu un proces Pj:
trimite un mesaj request lui Pj, dacă i<j sau
trimite un mesaj commit lui Pj și devine pasiv până când recepționează un mesaj corespunzător : commit reply.
Un proces poate iniția o interacție doar dacă este activ. Când recepționează un mesaj commit procesul Pj realizează interacțiunea și trimite înapoi la Pi mesajul commit reply când este activ (adică întârzie trimiterea mesajului commit reply până când devine activ). Când recepționează mesajul request procesul Pi inițiază interacția (pi,pj) la o etapă ulterioară.
Vom defini o ordine totală peste procesele sistemului distribuit: Pi < Pj dacă și numai dacă i < j. De asemenea vom defini funcția P:EN astfel încât P(e)=1 dacă și numai dacă e este un eveniment în procesul Pi. Bazându-ne pe funcția P, orice mesaj (s~r) poate fi clasificat în două tipuri (în ipoteza că un proces nu poate să-și trimită mesaje sieși):
Tip1: un mesaj trimis de către un proces mai mic, adică : P(s) > P(r)
Tip2: un mesaj trimis de către un proces mai mare, adică : P(r) > P(s)
Un mesaj de tipul 1 este realizat la trimiterea mesajului de către procesul care execută send pentru un mesaj de tipul 2, procesul mai mic trimite un mesaj request către procesul mai mare, acesta, când este posibil execută mesajul și transmite mesajul (cu același conținut) către procesul mai mic.
Condiția de transmitere, pentru orice mesaj (s2, r2) E este: s1, r1E : s1 < s2 => r1 r2
Neformal, condiția pune restricții unui proces de-a transmite un mesaj până când nu cunoaște că au fost recepționate toate transmisiile precedente, adică există o secvență de mesaje în E Ec astfel încât r1 r2.
Lema 9.4.
Mesajele commit satisfac SC (condiția de transmitere).
Demonstrație
Fie m1 = (s1,r1) și m2 = (s2,r2) două mesaje cu (s1 < s2). Când procesul trimite mesajul m1 devine pasiv, și nu execută s2 până când nu recepționează mesajul commit reply corespunzător prin urmare r1s2 deci r1r2.
Condiția de recepție întârzie recepționarea mesajelor. Formal pentru un mesaj (s2,r2)E avem:
s1,r1E : s1<r2 => NOT (r2r1).
Lema 9.5
Mesajele commit satisfac RC (condiția la recepție).
Demonstrație
Fie m1 = (s1,r1) și m2=(s2,r2) două mesaje cu s1 < r2. Când procesul transmite mesajul m1 devine pasiv. Procesul nu transmite nici un mesaj până nu recepționează mesajul commit reply corespunzător și deci NOT(r2r1).
Intercațiunea ddintre două procese este dată de transmiterea și recepționarea mesajelor commit. Prin urmare, mulțimea E constă din mesajele commit și mulțimea Ec din mesajele commit reply și request. Relația de cauzalitate trebuie să respecte aceste două mulțimi. Prin urmare, calculul este sincron dacă și numai dacă nu există coroane,
s0 r1, s1 r2, …, sk-2 rk-1, sk-1 r0
unde toate relațiile de cauzalitate sunt restricționate la E. De exemplu pentru si ri+1, există o serie de evenimente astfel încât si = e0, ri+1 = en și ej~~ej+1 sau ej < ej+1. Două evenimente sunt în relație cauzală dacă există între ele o serie de evenimente cu primul mesaj aparținând lui E.
Pi::
Var
messageQueue : Queue of messages
replyQueue : Queue of messages
state : {active, pasive} initially active
SendIntent(<m,Pi,Pj>)
If (i<j) then send (<m,Pi,Pj>) /* message to bigger process PR */
Else if (state=active) then /*commit and send the message */
State = pasive
send(<m,Pi,Pj>)
commit(<m,Pi,Pj>)
else /*wait for the reply message : SC */
Enqueue (messageQueue, <m,Pi,Pj>)
Receive (<m,Pj,Pi>)
If (i>j) then SendIntent(<m,Pi,Pj>) /*message from smaller process PR */
Else
Commit (<m,Pj,Pi>)
If (state =active) then send (<reply,Pi,Pj>)
Else Enqueue (messageQueue, <reply,Pi,Pj>)
/* wait for the previous reply : RC */
Receive (<reply,Pj,Pi>)
State = active
While (notEmpty(replyQueue)) do /* send replies if active : RC */
<reply,Pj,Pi> := Dequeue (replyQueue)
send (<reply,Pj,Pi>)
if (notEmpty(messageQueue)) then
state = pasive
<m,Pj,Pi>=Dequeue(messageQueue)
send(<m,Pj,Pi>)
commit(<m,Pj,Pi>)
Definiție (a relației de precedență cauzală tare)
e,f E : e|f ((e~~f) OR (e<f)) OR(s1E: e<s1 AND r1f)).
Pentru exemplu, e<si~~ri < sj~~rj < f, implică e|f dacă {e,si,ri,f} E, adică prima transmisie aparține lui E.
Definiția este motivată de faptul că restricția la mulțimea de evenimente E a calculului nu este sincronă dacă există o coroană, adică lanțul cauzal este format din relația |:
s0|r1, s1|r2, …, sk-2|rk-1, sk-1|r0.
Lema 9.6
Dacă (e|f) AND NOT(e~~f) atunci
(e<f) OR ((s1,r1)E : (e<s1 AND r1f)OR (g> (e~~g AND gf))
Lema 9.7
Fie (s1~~r1) AND (s2~~r2). Dacă s1 |r2 și SC, atunci r1r2 OR s1<r2.
Demonstrație
Dacă s1 |r2 atunci (conform lemei anterioare):
s1 < r2 OR
s1~~r1 AND r1r2 OR
s3 E> s1 < s3 AND r3r2.
Primele două cazuri satisfac imediat lema, în al treilea caz din SC deducem r1r3 și deoarece r3r2 rezultă r1r2
Lema 9.8
Dacă un calcul distribuit satisface SC și RC și nu are o coroană tare de dimensiune 2 formată din evenimente din E atunci nu are coroană (de dimensiune 2).
Demonstrație
Presupunem că există o coroană de dimensiune 2, deci s1|r2, s2|r1.
Deoarece coroana nu este tare (fără să afectăm generalitatea) putem presupune NOT(s1 < r2). Folosind Lema 9.7 obținem r1r2 (*).
Din (r1r2) și utilizând RC obținem NOT(s2 < r1). Aplicând Lema 9.7 încă o dată pentru NOT(s2 <s1) și (s2|r1), obținem r2r1, ce contrazice (*).
Lema 9.9
Dacă un calcul distribuit satisface RC și SC ai are o coroană (de dimensiune k) :
s0|r1, s1|r2, …, sk-2|rk-1, sk-1|r0
atunci de asemenea conține o coroană tare de dimensiune k’ k astfel încât :
s0’|r’1, s’1|r’2, …, s’k’-2|r’k’-1, s’k’-1|r’0.
Demonstrație
Dacă k2 atunci teorema rezultă imediat din lema anterioară.
Presupunem k>2. Lucrând cu indicii modulo k, vom presupune si-1|ri, si|ri+1 (*), astfel încât NOT (si<ri+1), un astfel de i există, altfel deja avem coroană tare.
Deoarece si|ri+1 (din Lema 9.7) rezultă riri+1.
Din si-1|ri și ri ri+1 ecuația (*) poate fi redusă la si-1|ri+1, obținând o coroană mai mică. Repetând procedeul ori de câte ori este posibil, teorema rezultă.
Teorema 9.8
Orice calcul distribuit care satisface SC, RC și PR este sincron.
Demonstrație
Vom folosi metoda reducerii la absurd. Fie un calcul distribuit nesincron. Atunci conform Teoremei nu există coroană și conform Lemei 9.9 avem o coroană tare.
s0 < r1, s1 < r2, … , sk-1 < r0.
i{0,2,3,… k-1} : P(si)=P(ri+1 mod k) (*).
i{1,2,3,… k-1} : P(si)>P(ri) (**) (din PR).
(*) și (**) => P(si)<P(r0) contradicție cu PR.
Teorema 9.9 (vitalitate)
Într-un calcul distribuit (care implementează acest algoritm), orice proces Pk care vrea să transmită un mesaj, în cele din urmă reușește.
Demonstrație
Folosim inducția după k.
Cazul k=1. Procesul P1 fiind cel mai mic este întotdeauna activ.
Pasul de inducție: Presupunem că cele mai mici k procese pot deveni active și vom demonstra că și procesul Pk+1 poate deveni activ.
Procesul Pk+1 este pasiv la momentul t dacă:
există un mesaj transmis (s1,r1) la momentul t0 < t
procesul este pasiv între t0 și t-.
Dacă mesajul este în tranzit atunci procesul Pk+1 poate recepționa commit reply și va deveni activ. Dacă transmiterea mesajului se poate realiza când P(r1) este activă, deoarece P(r1) < Pk+1, P(r1) devine activă și execută commit reply și Pk+1 devine activ.
Capitolul 10. Calculul
§10.1. Funcții globale
O dificultate în calculul distribuit o constituie faptul că procesele n-au acces la starea globală. Această dificultate poate fi depășită prin dezvoltarea unui mecanism de calcul a funcțiilor de stări globale. Aceste funcții le vom numi funcții globale.
Vom prezenta un algoritm ce calculează o funcție globală realizat de Konig, Bermond și Raynal. Printre calitățile acestui algoritm putem aminti: simetria; nu presupune cunoașterea topologiei rețelei de comunicație, fiind suficient că fiecare proces își cunoaște vecinii; la sfârșitul algoritmului toate procesele cunosc valoarea funcției f.
În fiecare fază un proces învață o nouă informație. Dacă un proces nu recepționează o nouă informație într-o fază, atunci se termină.
Vom utiliza variabila OPEN pentru a desemna mulțimea de canale deschise la o fază.
Structura inițială de date este următoarea:
Init: d:=0; inf:= {initial data}
new:=inf; OPEN := set of channels
c: received(c) :=
Algoritmul este următorul:
Phases: while OPEN do
d:= d+1
for cOPEN do
sent(c):= new – received(c)
sent<send(c)> on c
endfor
new:=
for cOPEN do
received <received(c)> on c
if (received(c) = send(c)) then OPEN :=OPEN – {c}
new:= new (received(c) – inf )
call compute
endfor
inf:=inf new
Algoritmul prezentat este sincron, lucrează utilizând noțiunea de fază. Pentru verificarea unui algoritm sincron se poate folosi o metodă bazată pe ecuații relative la variabile în fazele d și d-1. Mesajul transmis pe canalul c în faza d este privit ca o stare a variabilei sentd(c). utilizăm pentru a desemna reversul canalului c, adică: receivedd(c) = sentd(). Aplicând o astfel de metodă algoritmului de mai sus obținem:
copend-1 : sentd(c) := newd-1 – received d-1(c)
copend-1 : received d(c):= sentd()
newd := received d(c) – inf d-1
opend:=opend-1– { c| sentd(c) = receivdd(c)}
infd := infd-1 newd.
Notăm cu Ni(P) informația nodului aflat la distanța i de P.
N-1(P) = , Ti(P)=
Variabila Ti(P) desemnează informația nodurilor aflate la distanțe mai mici sau egale cu i de P. Valorile inițiale ale variabilelor din algoritm sunt:
Inf0 = N0(P)
New0 = N0(P)
Open0 = all
c: received0 (c)= .
Lema 10.1
Fie P și Q două procese adiacente.
Td-1(P) = Td-1(Q)
dacă și numai dacă
Nd-1(P)- Nd-2(Q) = Nd-1(Q) – Nd-2(P)
Demonstrație
Implicația inversă:
Td-1(P) = Td-2(Q) Nd-1(P) Nd-2(P)
= Td-2(Q) (Nd-1(P) – Nd-2(Q)) Td-2(Q) Nd-2(P)
= Td-2(Q) (Nd-1(Q) – Nd-2(P)) Nd-2(P)
= Td-2(Q) Nd-1(Q)
= Td-1(Q)
Implicația directă:
Vom arăta :
Nd-1(P) – Nd-2(Q) = Nd-1(Q) – Nd-2(P)
Din simetrie este suficient să arătăm :
Nd-1(P) – Nd-2(Q) Nd-1(Q) – Nd-2(P)
Fie x Nd-1(P) – Nd-2(Q). Aceasta implică : x la distanța d-1 de P și nu se află pe raza d-2 de Q. Distanța față de Q nu poate fi mai mică decât d-2, altfel distanța față de P ar fi strict mai mică decât d-1. Deoarece Td-1(P) = Td-1(Q) deducem că x este la distanța d-1 de Q, deci xNd-1(Q) – Nd-2(P).
Teorema 10.1
Pentru orice d1, avem :
sentd(c) = Nd-1(P) – Nd-2(Q)
receivedd(c) = Nd-1(Q) – Nd-2(P)
newd = Nd(P)
opend = {Pi(P,Q)Pi | Td-1(P) Td-1(Q)}
infd = Td(P)
Demonstrație
Folosim inducția după d, pentru d=1 avem:
sent1(c) = N0(P)
received1(c) = N0(Q)
new1 = N1(P)
open1 = {Pi(P,Q)Pi | T0(P) T0(Q)} = all
inf1 = T1(P)
Aceste ecuații se verifică imediat prin substituirea valorilor de la faza 0 din program.
Acum vom verifica cazul general, d >1
sendd
sendd(c) = newd-1 – receivedd-1(c) (conform programului)
= Nd-1(P) –(Nd-2(Q) – Nd-3(P)) (din inducție)
= Nd-1(P) – Nd-2(Q) (Ni(P) Nj(P) = , ij)
receivedd
receivedd(c) = sentd() (conform programului)
= Nd-1(Q) – Nd-2(P)
newd
newd =
= (conform ipotezei de inducție)
= Nd(P) (după simplificare)
opend
opend = opend-1 – {c | sentd(c) = receivedd(c)} (conform programului)
={Pi(P,Q)Pi | Td-2(P) Td-2(Q)} – {c| Nd-1(P)-Nd-2(Q) = Nd-1(Q) – Nd-2(P)} (conform ipotezei de inductie)
= {Pi(P,Q)Pi | Td-1(P) Td-1(Q)} (aplicand Lema 10.1)
infd
infd = infd-1 newd (conform programului)
= Td-1(P) Nd(P) (din ipoteza de inducție)
= Td(P)
§ 10.2 Calculări repetate
În sistemele distribuite, mulți algoritmi calculează repetat o funcție globală ce reclamă informații de la toate procesele. Dacă vom folosi algoritmul prezentat în secțiunea anterioară, pentru k repetări, atunci vom avea O(kNlog(N)) mesaje, unde N este numărul de procese din sistem. Vom prezenta o schemă ierarhică care reclamă doar O(kN) mesaje. În această schemă locul procesului este schimbat la fiecare pas, informațiile ierarhiei anterioare fiind utilizate pentru reorganizarea ierarhiei curente.
Fie N procese, etichetate în mod unic: P = { 1,…, N} și organizate sun forma unui k – arbore. Acest arbore are de asemenea N poziții. Cu pos(x,t) vom nota poziția procesului x la momentul t. Pentru simplitate, pos(x,0) = x pentru toți xP. Reconfigurarea ierarhiei constă din reorganizarea proceselor pe diferite poziții, pentru aceasta vom utiliza o funcție next : PP care furnizează noua poziție a procesului, adică dacă pos(y,t) = x atunci pos(y,t+1) = next(x). Este evident că next este o funcție bijectivă, adică o permutare. Orice permutare poate fi scrisă ca un produs de cicluri disjuncte. Pentru orice permutare f definită peste mulțimea P, orbita unui element xP este definită ca :
orbit(x) = {fi(x) | i0}
Adică orbit(x) conține toate elementele ciclului care îl conține pe x, f se numește primitivă dacă există xP astfel încât orbit(x) = P. Vom impune ca next să fie primitivă pentru ca orice proces să ocupe toate pozițiile în N unități de timp.
Secvența de arbori logici T1, T2, …, reprezintă evoluția în timp a atribuirii celor N procese la pozițiile din schemă.
Pentru a genera ierarhia, next(x) trebuie să satisfacă următoarele două constrângeri:
constrângerea de arbore de adunare: nodurile interioare ale lui Ti trebuie să formeze un subarbore pentru Ti+1. Această restricție asigură că secvența de mesaje cerută de procesul rădăcină la fiecare instantaneu nu este perturbată de reorganizarea ierarhiei.
În cazul unei etichetări în inordine această constrângere se poate formaliza :
Next(x) = x/2 pentru even(x).
constrângerea de onestitate: Permutarea trebuie să fie primitivă. Aceasta ne asigură că fiecare proces vizitează fiecare poziției din arbore exact o singură dată în N pași.
În continuare vom prezenta o pernutare ce satisface cele două condiții. Vom defini lead0(x) funcția ce returnează numărul de zerouri principale din n – reprezentarea binară a lui x (pe n biți).
Funcția next este aplicată pentru a determina poziția următoare a procesului în arborele binar complet etichetat în inordine. Cele N noduri pot fi organizate în patru grupe disjuncte:
RInt: even(x) AND (x2n-1)
LInt : even(x) AND (x<2n-1)
LLeaf : odd(x) AND (x<2n-1)
RLeaf : odd(x) AND (x2n-1)
function next(x)
/* Type I move */
if even (x) then x’:=x/2
/* Type II move */
if (odd(x) AND (x<2n-1)) then x’:= x*2lead0(x)+1
/*Type III move */
if (odd(x) AND (x>2n-1)) then x’:= x+1
if (x=N+1) then x’:=x’/2
return(x’)
Lema 10.3
Fie f: P P o permutare. Fie P0, … , Pn-1 o partiție a lui P în m mulțimi disjuncte astfel încât f(Pi) = P(i+1)mod m .
Atunci, f este primitivă dacă și numai dacă :
xP0: P0 orbit(x).
Demonstrație
Dacă f este primitivă, orbit(x) = P și prin urmare include Po. Rămâne să arătăm reciproca. Pentru orice xP0, P0 orbit(x) implică: j: fj(P0) fj(orbit(x)). Deoarece f(orbit(x)) orbit(x). avem : j: fj(P0) orbit(x); din f(Pi) = P(i+1)mod m urmează : j: Pj orbit(x), deci P orbit(x).
Vom spune că Q P este nucleul lui P relativ la f dacă și numai dacă pentru xP – Q , există un i astfel încât fi(x)Q. Intuitiv, Q este o submulțime a lui P a cărei intersecție cu orice ciclu al lui P este nevidă. Vom defini restricția permutării f:PP la nucleul QP (notat prin fQ:QQ) astfel: fQ(x) = fj(x), unde j = .
Lema 10.4
Dacă f:PP este o permutare, atunci fQ: QQ este de asemenea o permutare pentru orice Q nucleu al lui P cu respectarea lui f.
Demonstrație
Este suficient să arătăm injectivitatea. Fie x,y Q astfel încât xy dar fQ(x) = fQ(y). Fie k = min{i| i1, fi(x) Q} și l=min{i | i1, fi(y) Q}, k și l există deoarece Q este nucleu. Vom presupune, fără să afectăm generalitatea : kl. atunci din definiția lui fQ : fk(x) = fl(y), f fiind permutare este inversabilă., deci fk-l(x) = y. Dacă k=l atunci x=y deci contradicție, dacă k > l atunci am găsit un număr strict mai mic decât k astfel încât fk-l(x)Q, din nou contradicție.
Lema 10.5
O permutare f:PP este primitivă dacă și numai dacă există un nucleu QP astfel încât fQ este primitivă.
Demonstrație
Presupunem că f nu e primitivă, aceasta implică: f are un ciclu C de lungime strict mai mică decât card(P). Deoarece Q este nucleu, nu există ciclu în P-Q. Aceasta implică : C Q este o submulțime proprie nevidă a lui Q. Fie xC Q, orbita sa, relativă la fQ, este de asemenea în CQ. Prin urmare, fQ are un ciclu mai mic decât card(Q), ceea ce arată că fQ nu este primitivă.
Teorema 10.2
Funcția next() este o permutare primitivă care satisface constrângerea de arbore de adunare.
Demonstrație
Pentru început vom arăta că next este o permutare.
Fie x,y{ 1, …, N} astfel încât xy. Se verifică faptul că dacă același tip de mișcare se aplică atât lui x cât și lui y obținem next(x) next(y). și că de asemenea dacă se aplică diferite tipuri de mișcări lui x și lui y din nou obținem next(x) next(y).
Pentru a demondtra că next este primitivă, vom observa mai întâi că Q = LLeaf RLeaf RInt formează un nucleu al lui P relativ la next. Conform Lemei 10.4, nextQ este o permutare și prin aplicarea Lemei 10.3 se arată că nextQ este primitivă.
Deoarece Q este un nucleu al lui P și nextQ este primitivă aplicând Lema 10.5 obținem că next este de asemenea primitivă.
Menționăm că arborele de adunare este doar un instrument pentru determinarea secvenței de mesaje de transmis. Obiectivul este de a găsi la orice moment de timp t, pentru un proces dat, dacă trebuie să transmită mesaj și dacă da atunci cui.
Vom nota cu parent(x) părintele nodului x și cu msg(x,t) numărul procesului căruia procesul x îi trimite mesaj la momentul t. Dacă x nu trimite nici un mesaj la momentul t atunci msg(x,t) = nil. Pentru o etichetare în inordine, un nod este impar dacă și numai dacă el este frunză. Deoarece numai nodurile frunză transmit mesaje, obținem :
msg(x,t) := if odd(nextt(x)) then next-t(parent(nextt(x)))
else nil
Pentru simplificarea calculării lui nextt(x) și next-t(x) putem renumerota nodurile arborelui în secvența traversată de un proces. Acest lucru conduce la transformarea funcțiilor next() și parent() în new_next() și new_parent(), respectiv. Vom avea :
new_nextt(x) = x+t
msg(x,t) = if x + t LEAF then new_parent(x+t)-t
else nil
Vom defini mulțimea distanțelor de comunicare CDS (communication distance set) ca:
CDS = { i| i=new_parent(j) – j, jLEAF}
Lema 10.6
Procesul x poate transmite un mesaj (la un anumit moment de timp) procesului y dacă și numai dacă y-xCDS.
Demonstrație
Implicația directă:
y-xCDS înseamnă că există un nod frunză j1 astfel încât y-x = new_parent(j1) – j1. Fie t1 = j1 – x. Atunci
y-x = new_parent(x+t1) – (x+t1) sau y= new_parent(x+t1) –t1.
Deoarece x+t1 = j1 este o frunză, din definirea lui msg obținem că procesul x transmite un mesaj procesului y la momentul t1.
Implicația inversă:
Fie x transmite un mesaj procesului y la momentul t2, conform definirii lui msg avem: y = new_parent(x+t2) –t2 și că x+t2 este o frunză. Substituind j2 = x + t2, obținem
y =new_parent(j2) – (j2 – x) sau y-x = new_parent(j2) – j2CDS deoarece j2 este o frunză.
Vom presupune că arborele este etichetat în inordine. Fie n=log2(N+1). Vom partiționa mulțimea celor 2n-2 frunze din stânga, LLeaf, în n-1 grupe distincte astfel:
LLeaf(i) = {xLLeaf| lead0(x) = i}
Avem card (LLeaf(i)) = 2n-2-i pentru 1 i n-2 și card(LLeaf (n-1))=1. Importanța acestei partiționări este aceea că ciclul permutării next vizitează un nod din LLeaf(i) după vizitarea a exact i noduri interne.
Vom partiționa ciclul permutării next în 2n-2 segmente. Fiecare segment începe de la un nod din RLeaf și sfârșește într-un nod din LLeaf. Primul segment începe din cea mai din stânga frunză a lui RLeaf, care este etichetată cu 1. Astfel vom partiționa cele N elemente în 2n-2 segmente numărate de la 1 la 2n-2.
Lema 10.7
Mărimea segmentului m este trail0(m) + 3, unde trail0(m) furnizează numărul celor mai puțin semnificative zerouri din reprezentarea binară a lui m.
Demonstrație
Nodurile din RInt sunt vizitate în inordine prin definirea lui next. În segmentul m, vom vizita un nod din RLeaf, un nod la înălțimea trail0(m) din RInt, trail0(m) noduri în LInt și un nod din LLeaf , deci un total de trail0(m)+3 noduri.
Prin V(m) vom nota eticheta frunzei din stânga a segmentului m.
V(m) =
Fie S(k) =. Ne propunem să arătăm câteva proprietăți remarcabile pentru S(k).
Lema 10.8
S(a2i) = a2i – a + S(a), pentru orice i,a >0;
S(2a2i-1) – S((2a-1)2i-1) = 2i-1 pentru orice a impar.
Demonstrație
Vom utiliza inducția după i.
Pasul inițial: i=1. Trebuie să arătăm că S(2a) = a + S(a).
Vom folosi din nou inducția, de data aceasta dupa a.
a=1: S(21) = 1 = S(1)+1.
Presupunem adevărat pentru a<k. Atunci :
S(2k) = S(2k-2) + trail0(2k-1) + trail0(2k).
Astfel utilizând ipoteza inductivă :
S(2k) = S(k-1) + (k-1) + trail0(2k-1) + trail0(2k).
Deoarece trail0(2k-1) = 0 și trail0(2k) = trail0(k)+1 avem: S(2k) = S(k-1) + (k-1) + trail0(k) +1 = S(k) + k.
Pasul de inducție: Presupunem afirmația adevărată pentru i<k. S(a2k) = S(2a2k-1). Utilizând ipoteza inductivă:
S(a2k) = 2a2k-1 – 2a+S(2a). Utilizând cazul de bază prin înlocuirea lui S(2a) obținem :
S(a2k) = a2k-2a + S(a) + a = a2k –a + S(a)
Utilizând partea 1 avem:
S(2a2i-1) – S((2a-1)2i-1)=2i-1 –1 + S(2a) – S(2a-1) =
2i-1 – 1 + trail0(2a) = 2i-1
Lema 10.9
Nodurile din LLeaf(i) sunt etichetate cu V((2a-1)2i-1), unde a=1,2,3,…, 2n-2-i. Mai mult, pentru orice valoare impară a lui a (corespunzând unui copil stânga) etichetele corespunzătoare părintelui și fratelui drept sunt date de V(a2i+1)-1 și V(a2i+1 + 2i) respectiv.
Demonstrație
Un segment m sfârșește în LLeaf(i) dacă și numai dacă el vizitează exact i noduri interne. Conform Lemei 10.7, segmentul m vizitează exact trail0(m) + 1 noduri interne. Astfel avem relația trail0(m)+1 = i, de unde deducem forma lui m: (2a-1)2i-1 pentru un a din {1,…, 2n-2-i}. Ne vom concentra atenția pe acele LLeaf(i) care au mai mult de o frunză, deci 1 i n-3.
Atunci, valorile impare ale lui a desemnează etichetele pentru copiii din stânga și cele pare pentru copiii din dreapta din LLeaf. Deoarece nodurile din RInt la orice nivel sunt vizitate de la stânga la dreapta, părintele unui copil stânga din LLeaf(i) este vizitat de un segment următor care se termină în grupul LLeaf(i+1). El se termină în grupul LLeaf(i+1) deoarece părintele copilului are același număr de zerouri principale ca și copilul și elementul următor al segmentului trebuie să aibe un zero principal în plus decât părintele. Indicele acestui segment este (2a-1)2i-1 + 2i-1 = a2i. Fratele drept este vizitat de următorul segment ce se termină în grupul LLeaf(i). Indicele acestui segment este (2a+1)2i-1.
Teorema 10.3
Pentru N=2n-1, avem CDS pentru next(x) de forma:
CDS =
Demonstrație
Conform Lemei 10.9, contribuțiile la CDS sunt date de diferențele dintre etichetele părinților și frunzelor. Considerând nodurile din grupul LLeaf(i), 1 i n-3, care sunt copii stânga avem:
V(a2i) –1 – V((2a-1)2i-1)
= S(a2i) + 3a2i – 1 – S((2a-1)2i-1) – 3(2a-1)2i-1
= 2i-1 –1 + 32i-1 = 2i+1 – 1
Considerând nodurile din grupul LLeaf(i), 1 i n-3, care sunt copii dreapta avem:
V(a2i+1) – 1 – V (a2i+1 + 2i) unde a este impar, prin simplificare obținem –2i+1.
LLeaf(n-2) și LLeaf(n-1) contribuie cu –1 și 2n-1 – 1. În final nodurile din RLeaf adaugă 1 și –2 la mulțimea CDS. Prin urmare, mulțimea CDS pentru next(x) este de forma cerută.
Dacă vom impune o constrângere suplimentară : k=1, atunci este convenabilă abordarea pe care urmează s-o prezentăm.
Fie N=2n. De această dată o reprezentare de tip listă este mai convenabilă. Pozițiile listei vor fi numerotate de la 0 la 2n-1. Mesajele transmise la pasul următor pot fi determinate de o permutare convenabilă, snext(x). Fie bn-1, …, b0 reprezentarea binară a lui x și cn-1,…,c0 cea a lui x’ = snext(x). Vom utiliza operațiile RS0, RS1, LS0 și LS1 de deplasare dreapta sau stânga cu introducerea de biți 0 sau 1 pe cea mai (puțin) semnificativă poziție.
Constrângerea arbore de adunare devine constrângerea turneu:
b0 = 1 => cn-1 = 0; /*câștigătorii joacă între ei */
(b0 = 1) AND (bn-1,…,bi = 0,…,0)=> cn-1, …, ci-1=0,…,0; /*până când rămâne un singur câștigător */
Vom prezenta o funcție snext care satisface constrângerile de tip turneu și onestitate. Cu l vom nota numărul de zerouri consecutive după cel mai semnificativ bit.
function snext(x)
/* Type S1 move */
if (b0 = 1) then x’:= RS0(x)
/* Type S2 move */
if ((b0 = 1) AND (bn-1=0)) then x’:= 1bn-2…b0
/* Type S3 move */
if ((b0 = 0) AND (bn-1=1)) then
if (x= N-2) then x’:= x + 1
else x’:= LS1l+1(x+2)
return (x’).
Similar rezultatelor anterioare pot fi demonstrate :
Teorema 10.4
Funcția snext() satisface constrângerile de onestitate și de turneu.
Teorema 10.5
Pentru N = 2n, mulțimea CDS pentru n_snext2(x) este de forma:
CDS =
unde n_snext2(x) este dată de :
if b0=1 then x’:=RS0(x)
else if (b0=0) AND (bn-1=1) then x’ := x +1
else x’:= first available position în REven
(from lesft to right).
Concluzii
În această lucrare se trec în revistă o mare parte din problematica sistemelor distribuite, insistându-se asupra unora dintre rezultatele mai interesante.
În Introducere s-a preyentat o motivație pentru sistemele distribuite, s+a făcut o comparație cu sistemele paralele, scoțându-se în evidență avantajele și dezavatajele acetora. Deasemenea se face o introducere în conceptul de mulțime parțial ordonată, necesară pentru dezvoltările ulterioare.
Capitolul 1 dezvoltă noțiunea de timp în sistemele distribuite. Pune în evidență conceptul de cauzalitate, care este mai utilizat decât timpul fizic. Sunt preyentate mecanisme specifice de detectare a informațiilor de cauzalitate în calculul distribuit.
Capitolul 2 pune în discuție o problemă mult studiată în sistemele distribuite – excluderea mutuală. În particular, sunt prezentate diverse metode de specificare și verificare bazate pe structura de ordine parțială generată de programele distribuite.
În Capitolul 3 sunt descriși algoritmi pentru calculul stării globale a sistemelor distribuite. Sunt preyentați algoritmii lui Chandy și Lamport, și Mattern. Demonstrarea corectitudinii algoritmului lui Chandy și Lamport se bazează pe structura de mulțime parțial ordonată a calculului distribuit.
În următorele trei capitole se prezintă problema detectării unor proprietăți care sunt posibil adevărate în calculul distribuit. Adică se caută un scenariu de execuție a proceselor pentru care aceste proprități devin adevărate. În Capitolul 4 sunt dezvoltate rezultate fundamentale în detectarea predicatelor definite pe o singură stare globală. În Capitolul 5 sunt prezentate o clasă importantă de predicate – predicatele conjunctive. Sunt evidențiați algoritmi eficienți pentru predicate care pot fi exprimate ca o conjuncție de predicate locale a unui singur proces sau a unui singur canal. Capitolul 6 introduce predicatele care nu se pot exprima ca o conjucție de predicate locale. Această clasă include predicate de forma ( x1 + … + xN > C ) unde xi este o variabilă locală și C o constantă.
Capitolul 7 prezintă proprietăți inevitabile ale programelor distribuite. Un predicat definit pe o stare globală este inevitabil dacă este adevărat pentru toate execuțiile posibile ale proceselor.
Capitolul 8 prezintă proprietăți bazate pe fluxul de control în calculul distribuit și se prezintă o metodă de specificare și detecție.
Capitolul 9 introduce problema ordonării mesajelor în sistemele distribuite. Sunt definite ordonarea FIFO, ordonarea cauzală și ordonarea sincronă. Deasemenea sunt prezentați algoritmi ce asigură o anume ordonare.
În Capitolul 10 se dezvoltă problema funcțiilor de calcul globale.
Referințe bibliografice
K.P. Birman, T.A. Joseph. Reliable communication in the presence of failures. ACM Transactions on Computer Systems, 5(1):47-76,1987.
J.C. Bermond, J.C. Konig, M. Raynal. General and efficient descentralized consensus protocols. În 2nd International Workshop on Distributed Algorithms, pg. 41-56. Springer-Verlag, Lecture Note în Computer Science 312, 1987.
O. Babaoglu, K. Marzullo. Consistent global states of distributed systems: fundamental concepts and mechanisms, chapter 4. ACM Press, Frontier Series. (S.J. Mullender Ed.), 1993.
L. Bouge. Repeated snapshots in distributed systems with synchronouscommunication and their implementation in CSP. Theoretical Computer Science, 49:145-169, 1987.
O. Babaoglu, M. Raynal. Specification and detection of behavioral patterns in distributed computations. În Proc. of 4th IFIP WG 10.4 Int. Conference on Dependable Computing for Critical Applications, San Diego, C.A., January 1994. Springer Verlag Series in Dependable Computing.
B. Charron-Bost. Concerning the size of logical clocs in distributed systems. Information Processing Letters, 39:11-16, July 1991.
B. Charron-Bost, F. Mattern, G. Tel. Synchronous and asynchronous communication in distributed computations. Tehnical Report TR91.55, LITP, University Paris 7, September 1991.
G. Couloris, J. Dollimore, T. Kindberg. Distributed Systems: Concepts and Design. Addison-Wesley, 1994.
C. Chase, V. K. Garg. On techniques and their limitationsfor the global predicate detection problem. În Proc. of Workshop on Distributed Algorithms, France, September 1995.
H. Chiou, W. Korfhage. Efficient global event predicate detection. În 14th Intl. Conference on Distributed Computing Systems, Poznan, Poland, June 1994.
K. M. Chandy, L. Lamport. Distributed snapshots: Determining global states of distributed systems. ACM Transactions on Computer Systems, 3(1):63-75, February 1985.
R. Cooper, K. Marzullo. Consistent detection of global predicates. În Proc. of the Workshop on Parallel and Distributed Debugging, pg. 163-173, Santa Cruz, CA, May 1991. ACM/ONR.
E. W. Dijkstra. Self- stabilizing systems in spite of distributed control. Communications of the ACM, 17:643-644, 1974.
E. W. Dijkstra. The distributed snapshot of K.M. Chandy and L. Lamport. În M. Broy, editor, Control Flow and Data Flow: Concepts of Distributed Programming, vol. F14. NATO ASI Series, Springer-Verlag, New York, NY,1985.
B. A. Davey, H. A. Priestley, Introduction to Lattices and Order. Cambridge University Press, Cambridge, UK, 1990.
E. W. Dijkstra, C. S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag, New York Inc., New York, NY, 1990.
S. Mullender (editor). Distributed Systems. Addison-Wesley, Reading, MA, 1994.
C. J. Fidge. Partial orders for parallel debugging. Proceedings of the ACM SIGPLAN/SIGOPS Workshop on Parallel and Distributed Debugging, ACM SIGPLAN Notices, 24(1):183-194, January 1989.
E. Fromentin, M. Raynal, V. K. Garg, A. I. Tomlinson. On the fly testing of regular patterns in distributed computations. În Proc. of the 23rd Intl. Conf. On Parallel Processing, St. Charles, IL, August 1994.
V. K. Garg. Some optimal algorithms for decomposed partially ordered sets. Information Processing Letters, 44:39-43, November 1992
V. K. Garg, C. Chase. Distributed algorithms for detecting conjunctive predicates. În Proc. of the IEEE International Conference on Distributed Computing Systems, Vancouver, Canada, June 1995.
V. K. Garg. Principles of distributed szstems, Kluwer Academic Publishers, 1996
Index
Admisibilitate 100
Antilanț 92
Bâlbâială 100
Ceas de dependență directă 19
Ceas logic 7
Cas matrice 23
Concurență 4
Constrângerea de arbore de adunare 132
Constrângerea de onestitate 133
Constrângerea turneu 140
Coroană 120
Dilwort, teoremă 92
Deposet 6
Funcții globale 128
Forma normală disjunctivă 54
Fuziune 93
Interval 40
Interval de stări 23
Lanț 92
Lamport, algoritm 27
Logică 100
Mulțimea distanțelor de comunicare 76
Onestitate 27
Ordonarea mesajelor 114
Ordonare cauzală 114
Ordonare FIFO 114
Ordonarea sincronă 114
Overlap 102
Precedență cauzală 4
Precedență directă 21
Precedență locală 4
Predicat conjunctiv slab 54
Predicat conjunctiv tare 102
Predicat de canal 65
Predicat de canal monoton 48
Ricart și Agrawala, algoritm 34
Secțiune critică 27
Secvență globală 100
Secvență globală pură 102
Siguranță 27
Stare globală 40
Stare santinelă 48
Tăietură 40
Tăietură critică 40
Vitalitate 27
UNIVERSITATEA din BUCUREȘTI
DIZERTAȚIE
Temă: SISTEME DISTRIBUITE
CONDUCĂTOR AUTOR
Conf. Dr. GHEORGHE ȘTEFĂNESCU VICTOR ISPAS
1999
Copyright Notice
© Licențiada.org respectă drepturile de proprietate intelectuală și așteaptă ca toți utilizatorii să facă același lucru. Dacă consideri că un conținut de pe site încalcă drepturile tale de autor, te rugăm să trimiți o notificare DMCA.
Acest articol: Sisteme Distribuite (ID: 161640)
Dacă considerați că acest conținut vă încalcă drepturile de autor, vă rugăm să depuneți o cerere pe pagina noastră Copyright Takedown.