Verificação Formal: Aula 2

Especificação e verificação de algoritmos concorrentes

Considere o seguinte algoritmo onde dois processos concorrentes incrementam uma variável partilhada.

   var x : integer = 0

   procedure increment;
   begin
     x := x + 1 
   end;

   increment || increment

Para simplificar a modelação vamos assumir que todas as instruções de um processo executam de forma atómica, isto é sem interrupção de outros processos. Por vezes, para tornar a análise mais eficiente (porque o número de traços possíveis diminui significativamente) vamos assumir que várias instruções executam de forma atómica. Para sinalizar isso iremos usar etiquetas no algoritmo para assinalar diferentes pontos de execução e assumir que todas as instruções entre duas etiquetas executam de forma atómica. Há situações em que podemos assumir isso sem mascarar problemas, nomeadamente agrupar sequências de instruções que apenas referem variáveis locais. Noutros casos é preciso ter muito cuidado com essas simplificações. Por exemplo, no algoritmo acima só temos dois possíveis pontos de execução em cada processo (antes ou depois da atribuição), o que pode ser tornado explícito acrescentando as referidas etiquetas.

   var x : integer = 0

   procedure increment;
   begin
0:   x := x + 1 
1: end;

   increment || increment

Para verificar a correção parcial deste algoritmo (quando termina a variável partilhada tem o valor 2) e a sua terminação podemos usar a seguinte especificação em TLA+.

----- MODULE Increment2 -----

EXTENDS Naturals

VARIABLES x,pc0,pc1

vars == <<x,pc0,pc1>>

Init == x = 0 /\ pc0 = 0 /\ pc1 = 0

Increment0 == pc0 = 0 /\ x' = x + 1 /\ pc0' = 1 /\ UNCHANGED pc1

Increment1 == pc1 = 0 /\ x' = x + 1 /\ pc1' = 1 /\ UNCHANGED pc0

Next == Increment0 \/ Increment1

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

TypeOK == [](x \in Nat /\ pc0 \in 0..1 /\ pc1 \in 0..1)

Finish == pc0 = 1 /\ pc1 = 1

PartialCorrectness == [](Finish => x = 2)

Termination == <> Finish

=============================

Como este é um algoritmo que termina obviamente também terá um deadlock, logo devemos indicar ao TLC que não queremos verificar a ausência do mesmo.

SPECIFICATION Spec 
PROPERTIES TypeOK PartialCorrectness Termination
CHECK_DEADLOCK FALSE

Este algoritmo pode ser generalizado para um número arbitrário de processos.

   var x : integer = 0

   procedure increment;
   begin
0:   x := x + 1 
1: end;

   increment || ... || increment

Para especificar esta versão em TLA+ devemos declarar uma constante que diz quantos processos temos e assumir que essa constante é estritamente positiva. Para além disso, como temos agora um número arbitrário de processos, para guardar os program counters teremos que usar uma função finita que mapeia cada identificador de processo para a etiqueta que identifica o respetivo ponto de execução.

----- MODULE IncrementN -----

EXTENDS Naturals

CONSTANT N

ASSUME N > 0

VARIABLES x,pc

vars == <<x,pc>>

Init == x = 0 /\ pc = [i \in 1..N |-> 0]

Increment(i) == pc[i] = 0 /\ x' = x + 1 /\ pc' = [pc EXCEPT ![i] = 1]

Next == \E i \in 1..N : Increment(i)

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

TypeOK == [](x \in Nat /\ pc \in [1..N -> 0..1])

Finish == \A i \in 1..N : pc[i] = 1

PartialCorrectness == [](Finish => x = N)

Termination == <> Finish

=============================

Para verificar este algoritmo, no ficheiro de configuração temos que indicar qual é o valor da constante declarada.

CONSTANT N = 6
SPECIFICATION Spec
PROPERTIES TypeOK PartialCorrectness Termination
CHECK_DEADLOCK FALSE 

De facto, os processadores não garantem que a instrução x := x + 1 executa de forma atómica, pois a execução desta instrução implica uma leitura da memória do valor actual de x e uma posterior escrita de x + 1, e entre estas duas instruções máquina o processo poderia ser interrompido. Continuando a assumir que as instruções executam de forma atómica, podemos simular este comportamento substituindo a instrução x := x + 1 pelas instruções y := x; x := y+1, onde y é uma variável local de cada processo. Isto corresponderia ao seguinte algoritmo.

   var x : integer = 0;

   procedure increment;
     var y : integer = 0;
   begin
0:   y := x; 
1:   x := y + 1 
2: end;

   increment || ... || increment

Exercício: Especifique este algoritmo em TLA+ e verifique se continua a cumprir as propriedades esperadas.

Neste caso, para garantir que a atribuição em cada processo executa de forma atómica podemos usar um semáforo, que terá de ser adquirido por cada processo antes de começar a executar e libertado no final. Em termos abstratos podemos ver um semáforo como uma simples variável booleana partilhada, onde a ação de adquirir o semáforo corresponde à execução atómica de uma espera ativa seguida uma atribuição. O algoritmo com o semáforo seria o seguinte.

   var x : integer = 0;
       sem : boolean = true;

   procedure increment;
     var y : integer = 0;
   begin
0:   repeat until sem;
     sem := false;
1:   y := x; 
2:   x := y + 1;
3:   sem := true;
4: end;

   increment || ... || increment

Exercício: Especifique este algoritmo em TLA+ e verifique se volta a cumprir as propriedades esperadas.

Exercício: Verifique que esta versão do algoritmo é um refinamento da versão inicial onde se assumia que a atribuição executava de forma atómica.

Especificação e verificação de algoritmos de exclusão mútua

Exercício: Verifique se o seguinte algoritmo de exclusão mútua para um número arbitrário de processos usando um semáforo garante de facto a exclusão mútua e a ausência de starvation (neste caso identifique as condições de justiça mais fracas necessárias para que a propriedade se verifique). Valide a sua especificação verificando se um cenário onde todos os processos entram na região crítica é possível.

   var 
     sem : boolean = true;

   procedure process;
   begin
   while true do
     begin
idle:  (* idle *)
want:  repeat until sem;
       sem := false;
crit:  (* critical *)
       sem := true;
     end
   end;

   process || ... || process

Exercício: Verifique se o seguinte algoritmo de exclusão mútua para 2 processos proposto por Peterson garante de facto a exclusão mútua e a ausência de starvation (neste caso identifique as condições de justiça mais fracas necessárias para que a propriedade se verifique).

   var 
     turn : 0..1;
     want0 : boolean = false;
     want1 : boolean = false;

   procedure process0;
   begin
     while true do                           
     begin
idle:  (* idle *) 
       want0 := true;
want:  turn := 1;
wait:  repeat until (not want1 or turn = 0);
crit:  (* critical *) 
       want0 := false 
     end
   end;

   procedure process1;
   begin
     while true do                           
     begin
idle:  (* idle *) 
       want1 := true;
want:  turn := 0;  
wait:  repeat until (not want0 or turn = 1);
crit:  (* critical *) 
       want1 := false
     end 
   end;

   process0 || process1

Exercício: Verifique a seguinte versão do algoritmo de Peterson para N > 1 processos.

   var
     level : array [0..N-1] of -1..N-2 = [N of -1];
     last  : array [0..N-2] of  0..N-1;

   procedure process(i : integer);
     var l : integer = 0;
   begin
     while true do
     begin
idle:  (* idle *)
want:  while l < N-1 do
       begin
         level[i] := l;
         last[l]  := i;
wait:    repeat until (last[l] != i or ∀ k != i . level[k] < l));
         l := l+1
       end
       (* critical *)
crit:  level[i] := -1;
       l := 0
     end
   end;

   process(0) || ... || process(N-1)

Exercício: Verifique o algoritmo Bakery de exclusão mútua proposto por Leslie Lamport.