- - - - CENAPAD-MGCO

A seguir: Equidade fraca e equidade Acima: Modelos Formais para Programas Anterior: Atingibilidade: o mais forte

Modelos Formais: Progresso

• Propriedades de progresso têm a forma

  $$P \ensuremath{ \; leads\!{\small -}\!to\;}Q$$

• Esta propriedade é satisfeita por um sistema de transições se em toda computação, toda vez que o estado satisfaz P, mais tarde (ou naquele momento) na computação o sistema satisfará Q.
• Exemplos:
  • $q = q_{0} \ensuremath{ \; leads\!{\small -}\!to\;}q = q_final$: toda computação termina
  • $q = hungry \ensuremath{ \; leads\!{\small -}\!to\;}q = eating$: toda requisição é satisfeita
  • $\left\vert produced \right\vert = n \ensuremath{ \; leads\!{\small -}\!to\;}\left\vert consumed \right\vert = n$: a sequência produzida acaba sendo consumida
• Problema: quanto tempo temos que esperar? Em outras palavras, quando podemos acusar uma computação de violar uma propriedade $P \ensuremath{ \; leads\!{\small -}\!to\;}Q$?
  • num sistema assíncrono, nada obriga um comando com a guarda habilitada a ser executado;
  • a existência de computações finitas, em que uma requisição foi foi feita mas não foi satisfeita, não deveria nos levar a diagnosticar o sistema de transições como sujeito a starvation.