Sistemas Operacionais

Aula 10: Verificação

Verificação de Programas Paralelos

Extremamente difícil:

Extremamente importante:

Porque tão difícil ?

Composição paralela de processos é cara:

Se P1 tem m estados e P2 tem n estados, P1 X P2 tem m * n estados!

Explosão de estados.

Teste

Implementa-se o programa e executa-se o mesmo ad nauseam.

Vantagem: simples, eficiente

Desvantagem: cobertura de falhas muito baixa.

Verificação Formal

Prova-se que o programa está correto:

Métodos matemáticos que derivam propriedades do sistema baseado em assunções e teoremas.

Necessários se você quer confiar no seu programa!

Provadores de Teoremas

Provadores de teoremas são programas que dado:

Provadores de Teoremas

Prova Manual por Invariantes

Prova Manual por Invariantes

better_lock(k) {
  lock(k->mutex);
  if (!k->free)
    sleep(k->bed, k->mutex);
  k->free = 0;
  unlock(k->mutex);
}

better_unlock(k);
  lock(k->mutex);
  k->free = 1;
  wakeup(k->bed);
  unlock(k->mutex);
}

Prova Manual por Invariantes


Last Modified: 01:49pm , December 16, 1998