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

A seguir: Modelos Formais: Conclusões Acima: Modelos Formais - Continuação Anterior: Modelos Formais - Continuação

Buffer Limitado: Progresso

Vamos precisar de ter como hipótese a execução de $\gamma_{1}$ e de $\gamma_{2}$ com equidade fraca.

Seja

$$P \equiv \left\vert produced \right\vert \geq l \wedge \left\vert consumed \right\vert = k < l$$

Temos

$$P = P \wedge (consumerState = hungry \vee consumerState = thinking)$$

Mas

$$consumerState = thinking \ensuremath{ \; leads\!{\small -}\!to\;}consumerState = hungry$$

via $\gamma_{1}$.Como $\left\vert produced \right\vert = \left\vert buffer \right\vert + \left\vert consumed \right\vert$P implica em $n = \left\vert buffer \right\vert \gt$, e portanto $P \ensuremath{ \; leads\!{\small -}\!to\;}\left\vert consumed \right\vert = k+1$ (via $\gamma_{2}$), como queríamos demonstrar.