- - - - CENAPAD-MGCO

A seguir: Um Request visita um Acima: O Algoritmo de Naimi-Trehel Anterior: Theorem 1: ``Proof'' for

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 \ensuremath{\mathbf{T}} \in IN[i]$.É fácil ver que (por hipótese de equidade fraca na execução da Regra 9)

$$hungry \wedge \ensuremath{\mathbf{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₀ estava 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}$ j.

Se no instante t₀ tínhamos Next[i] $\neq NIL$, 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₂.

Observe que estamos considerando que um Request R[j] visita um sítio i tanto quando i recebe um request originado por j, ou quando i recebe um token com j em sua ReqList.

Por ${\cal D} _{3}$ ou ${\cal D} _{4}$, teremos i i₁ 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 existê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, e como ${\cal D}$ é um grafo acíclico, esta sequência não pode conter repetições, e $\kappa$ não pode existir.