Verificação Formal: Exame

Considere o seguinte algoritmo concorrente, onde temos N processos que tentam fazer push do seu identificador numa queue partilhada de capacidade K (implementada com um array circular) e N processos que tentam fazer pop dessa mesma queue. Assuma que a queue não tem capacidade para todos os processos, ou seja 0 < K < N.

   var front : 0..K-1 = 0;
       size  : 0..K = 0;
       queue : array 0..K-1 of 0..N = [K of 0];
       lock  : boolean;

   procedure pop(i : integer);
     var val : 0..N = 0;
   begin
0:   repeat until lock;
     lock := false;
     if size = 0 then
     begin
       lock := true;
1:     repeat until lock and size > 0;
       lock := false;
     end
2:   val := queue[front];
     front := mod (front + 1) K;
     size := size - 1;
     lock := true;
3:
   end;

   procedure push(i : integer);
   begin
0:   repeat until lock;
     lock := false;
     if size = K then
     begin
       lock := true;
1:     repeat until lock and size < K;
       lock := false;
     end
2:   queue[mod (front+size) K] := i;
     size := size + 1;
     lock := true;
3:
   end;

   pop(1) || push(1) || ... || pop(N) || push(N)

Exercício (5 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.
• Todos os pops retiram valores diferentes da queue.
• O primeiro pop só termina depois do primeiro push terminar.
• Todos os identificadores pushed vão ser inevitavelmente popped.

Exercício (1 pontos): mostre como poderia encontrar um cenário onde todos os pushes são feitos por ordem do identificador do processo (mas não necessariamente seguidos, podendo haver pops intercalados).