UFMG - Pós-graduação em Ciência da Computação - Programação Paralela

A seguir: Visited nodes invariant Acima: Programação Paralela Anterior: Theorem 1: ``Proof'' for

(postscript)

Aula 18 - O Algoritmo de Naimi-Trehel - Progresso

Queremos mostrar que s[i] = hungry leads-to s[i] = eating. Vamos começar mostrando que

$$P1 \equiv s[i] = hungry \wedge root(i) \ensuremath{ \; leads\!{\small -}\!to\;}s[i]=eating.$$

Pelo invariante A4, $root(i) \Longrightarrow$ Hastoken[i] $\vee {\bf T}\in IN[i]$.É fácil ver que (por hipótese de equidade fraca na execução da Regra 9)

$$hungry \wedge {\bf T}\in IN[i] \ensuremath{ \; leads\!{\small -}\!to\;}Hastoken[i]$$

Como

$$hungry \wedge Hastoken[i] \ensuremath{ \; leads\!{\small -}\!to\;}s[i] = eating,$$

temos o resultado que queríamos.

Consideremos agora uma computação infinita $\kappa$ em que um sítio i₀ ficou com fome em um certo instante t₀, e permaneceu com fome até o fim dos tempos. Pelo que acabamos de demonstrar, sabemos que no instante t₀ tínhamos root(i₀) = F, e portanto que para todo instante $t \geq t_{0}$, $\exists j, i_{0} \ensuremath{\leftrightarrow} j$. Se no instante t₀ tínhamos Next[i] = j₀, a regra 5 certamente terá sido executada em um instante t₁ > t₀. Um Request terá sido enviado por i₀. Este Request não pode ter visitado um número ilimitado de sítios , como veremos a seguir. Portanto, teremos um sítio i₁ onde o Request de i terá se estabilizado a partir de um instante t₂. Por ${\cal D} _{3}$ ou ${\cal D} _{4}$,teremos $i \ensuremath{\leftrightarrow} i_{1}$ para todo instante $t \geq t_{2}$ Isto só é possível se i₁ também nunca chegou a comer na computação $\kappa$, a partir do instante t₂. Pelo mesmo raciocínio, existe um sítio i₂ que a partir de um certo instante reteve o Request de i₁, e que nunca chegou a comer. Portanto, a única possibilidade de existência de $\kappa$ é a exitência de uma sequência infinita de sítios $i_{0}, i_{1}, i_{2}, \ldots$ tal que, a partir de um certo instante, o Request de i_k esteja retido em i_k+1. Mas como i_k i_k+1, esta sequência não pode conter repetições, e $\kappa$ não pode existir.

Para provar que um Request não pode visitar um número ilimitado de sítios, vamos demonstrar o seguinte invariante:

• A7 $\equiv$ if [i] = $v_{1}v_{2}\ldots v_{m}$,then for $j, k \in [1\ldots m]$, $v_{j} \neq$ i, and $j \neq k \Longrightarrow v_{j} \neq v_{k}$.
• Em outras palavras, todos os elementos em [i] são distintos, e seu comprimento não pode crescer indefinidamente.

A7 não é indutivo, e precisamos reforçá-lo com o seguinte predicado:

$$A8 = j \in \ensuremath{ \cal V} [i] \Longrightarrow j \ensuremath{ \ensuremath{\leftrightarrow} ^{+}} i$$

onde $j \ensuremath{ \ensuremath{\leftrightarrow} ^{+}} i$ significa que existe uma rota de j para i de comprimento maior ou igual a 1 no grafo .

Como para todo i $\ensuremath{ \cal V} [i]$ é inicialmente vazio, A8 é válido inicialmente. Precisamos agora varrer todas as regras do algoritmo, demonstrando que se A8 for válido antes da execução da regra, A8 será válido também após a sua execução.

A8 corre o risco de ser invalidado por regras que modifiquem o valor de algum $\ensuremath{ \cal V} [i]$ ou que eliminem relações $j \ensuremath{ \ensuremath{\leftrightarrow} ^{+}} i$para algum par de sítios.