Verificação Formal: Teste

Verificação de algoritmos concorrentes

Considere o seguinte algoritmo concorrente, onde se pretende implementar uma “barreira” entre N processos. O objetivo da barreira é que depois de um process iniciar a execução apenas termine quando todos os N processos já tiverem também iniciado.

   var n : 0..N = 0;
       lock : boolean = true;
       waiting : array 1..N of boolean = [N of false];

   procedure process(i : integer);
   begin
0:   repeat until lock;
     lock := false;
     n := n + 1;
1:   while (n < N) do
     begin
       waiting[i] := true;
       lock := true;
2:     repeat until (lock and not waiting[i]);
       lock := false;
     end;
     waiting = [N of false];
     lock := true;
3:   
   end;

   process(1) || ... || process(N)

Exercício (8 pontos): especifique este algoritmo em TLA+.

Exercício (4 pontos): mostre como pode especificar e verificar as seguintes propriedades (no caso das propriedades de liveness tente encontrar as condições de justiça mais fracas que permitem a sua verificação).

• As variáveis partilhadas têm sempre valores do tipo correto.
• Não é possível que todos os processos estejam bloqueados à espera no program counter 2.
• Todos os processos vão terminar a execução.
• O algoritmo realmente implementa uma barreira entre os N processos, ou seja um processo apenas pode terminar a execução quando todos os N processos já tiverem iniciado.

Exercício (2 pontos): mostre como poderia verificar que as propriedades acima são válidas mesmo que a qualquer momento aconteça um erro e um dos bits do array waiting seja colocado a false.

Verificação de algoritmos distribuídos

Considere o seguinte algoritmo distribuído onde dois processos trocam mensagens com o objetivo de conseguirem sortear um valor entre 1 e 2 que seja diferente para os dois processos (quando o algoritmo termina, o valor sorteado estará guardado na variável result).

  var inbox : array 0..1 of channel;

  procedure (i : integer);
    var result : 0..2 = 0;
        try : 1..2;
  begin
    send(inbox[1-i],try);    
0:  while true do
    begin
      if result = 0 and not empty(inbox[i]) then
        if receive(inbox[i]) = try
        then
        begin
            try := 1..2;
            send(inbox[1-i],try)
        end
        else result = try 
    end
  end;

  procedure(0) || procedure(1)

Exercício (3 pontos): especifique este algoritmo em TLA+, assumindo que as mensagens são entregues por ordem e não há perdas de mensagens.

Exercício (3 pontos): mostre como pode especificar e verificar as seguintes propriedades (no caso das propriedades de liveness tente encontrar as condições de justiça mais fracas que permitem a sua verificação).

• Sempre que um dos processos tiver um result diferente de 0 o outro processo terá necessariamente um valor diferente.
• Os canais de comunicação nunca têm mais do que 2 mensagens.
• Mal um processo tenha um result diferente de 0 o outro irá inevitavelmente ter um valor de result diferente de 0.