Verificação Formal: Aula 4

Verificação de propriedades de liveness

Há uma classe de algoritmos distribuídos que se designa de self-stabilizing, e cujo objetivo é fazer com o sistema estabilize num estado “válido”, qualquer que seja o estado inicial. O conceito de self-stabilization e o primeiro algoritmo desta classe foram introduzidos por Edsger Dijkstra em 1974, já depois de ter recebido o seu prémio Turing em 1972 pelas suas várias contribuições na área da programação e da algoritmia. Nesse algoritmo temos um anel de N+1 nós, em que o nó 0 é um nó especial (o nó bottom), sendo um estado “válido” um estado onde apenas um dos nós possui um token, que vai depois circulando entre eles. Cada nó tem uma variável de estado que pode tomar K valores diferentes, e assume-se que um nó consegue ler o estado do vizinho que o precede. Um nó sabe se tem o token através de uma comparação do seu estado com o estado desse vizinho. Este algoritmo pode ser descrito da seguinte forma.

   var state : array [0..N] of 0..K-1;

   function hasToken(i : integer) : boolean;
   begin
     hasToken := (i = 0 and state[i] = state[N]) or (i != 0 and state[i] != state[i-1])
   end;

   procedure bottom;
   begin
0:   while true do
     begin
       repeat until hasToken(0);
       state[0] := mod (state[0] + 1) K
     end
   end;

   procedure other(i : integer);
   begin
0:   while true do
     begin
       repeat until hasToken(i);
       state[i] := state[i-1]
     end
   end;

   bottom || other(1) || ... || other(N)

As propriedades desejadas para algoritmo self-stabilizing são as seguintes:

• Closure: uma vez atingido um estado válido, o sistema fica para sempre num estado válido.
• Convergence: o sistema vai chegar a um estado válido.

A primeira é uma propriedade de safety e a segunda é uma propriedade de liveness. O algoritmo de Dijskstra garante estas duas propriedades desde que K >= N.

Podemos especificar este algoritmo em TLA+ da seguinte forma. Note que no estado inicial o valor da variável state é arbitrário. Note também que neste caso não precisamos de declarar um program counter pois os nós repetem constantemente o mesmo comportamento, que é executado de forma atómica.

------------------------------ MODULE Dijkstra ------------------------------

EXTENDS Naturals

CONSTANTS N, K
ASSUME N > 0 /\ K >= N
VARIABLE state

TypeOK == [] (state \in [0..N -> 0..K-1])

hasToken(i) == (i = 0 /\ state[i] = state[N]) \/ (i # 0 /\ state[i] # state[i-1])

bottom == hasToken(0) /\ state' = [state EXCEPT ![0] = (@+1) % K]

other(i) == hasToken(i) /\ state' = [state EXCEPT ![i] = state[i-1]]
           
Next == bottom \/ \E i \in 1..N : other(i)

Init == state \in [0..N -> 0..K-1]

Spec == Init /\ [][Next]_state

Valid == \E i \in 0..N : hasToken(i) /\ \A j \in 0..N : hasToken(j) => j = i
           
Closure == [] (Valid => [] Valid)

Convergence == <> Valid

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

Usando o TLC podemos verificar as duas propriedades fundamentais. No entanto para a propriedade de liveness o TLC vai apresentar um contra-exemplo, onde o sistema simplesmente faz stuttering permanentemente e, por isso, nunca atinge um estado válido. Obviamente, isto é permitido pela especificação do comportamento do algoritmo, dado que a fórmula [][Next]_state especifica precisamente que em qualquer estado o sistema pode evoluir pela relação Next ou fazer stuttering.

Embora permitir o stuttering seja desejável, não é razoável que o sistema, tendo possibilidade de executar uma action opte por fazer stuttering para sempre. Para eliminar estes comportamentos não razoáveis, ou não “justos” para os nós na medida em que estes não tem oportunidade de executar, podemos impor o que designa de condições de justiça no sistema. O objetivo destas condições de justiça é garantir que quando uma action está “permanentemente” enabled ela irá inevitavelmente ocorrer. Dependendo da definição de “permanentemente” podemos ter duas variações das condições de justiça: a justiça fraca, onde “permanentemente” significa continuamente; e a justiça forte, onde “permanentemente” significa recorrentemente.

Dada uma action $A$ a condição de justiça fraca pode ser especificada da seguinte forma:

\[\square (\square \mathsf{ENABLED} A \Rightarrow \lozenge A)\]

Esta fórmula é equivalente à seguinte:

\[\lozenge \square \mathsf{ENABLED} A \Rightarrow \square \lozenge A\]

Infelizmente esta fórmula não pode ser usada diretamente para impor a justiça fraca porque não é uma fórmula TLA (relembre que as actions não podem ser usadas de forma arbitrária). No entanto, a seguinte variante já é uma fórmula em TLA, onde $\langle A \rangle_t \doteq A \wedge t’ \neq t$ significa que $A$ ocorreu e teve algum efeito no estado.

\[\lozenge \square \mathsf{ENABLED} \langle A \rangle_t \Rightarrow \square \lozenge \langle A \rangle_t\]

Esta variante é fórmula em TLA devido à dualidade entre os operadores $\square$ e $\lozenge$, pois $\square \lozenge \langle A \rangle_t \equiv \neg \lozenge \square [\neg A]_t$.

A justiça forte pode ser especificada da seguinte forma.

\[\square \lozenge \mathsf{ENABLED} \langle A \rangle_t \Rightarrow \square \lozenge \langle A \rangle_t\]

Como estas condições são muito comuns, o TLA tem abreviaturas para as mesmas, nomeadamente $\mathsf{WF}_t(A)$ e $\mathsf{SF}_t(A)$.

No caso do algoritmo de Dijkstra, para garantir a propriedade de convergência basta impor a justiça fraca sobre toda a relação Next, para garantir que enquanto houver pelo menos um nó que consiga progredir (enquanto houver pelo menos um nó que tenha o token) então algum deles terá que executar. Isto pode ser feito alterando a especificação do sistema para Spec == Init /\ [][Next]_state /\ WF_state(Next) ou, se quisermos apenas usar as condições de justiça para verificar a propriedade de convergência, alterando a definição da mesma para Convergence == WF_state(Next) => <> Valid. Com uma destas alterações a propriedade já é verificada.

Exercício: identifique as condições de justiça mais fracas necessárias para verificar as propriedades de liveness dos exemplos especificados na aula anterior.

Considere o problema clássico dos N filósofos sentados numa mesa circular com N garfos entre eles, e que alternam constantemente entre as atividades de pensar e comer. Para comer, o filósofo i precisa de pegar nos dois garfos diretamente à sua esquerda e à sua direita. Sem um mecanismo de controlo de concorrência, este sistema tem um possível deadlock onde, por exemplo, todos os filósofos pegam “simultaneamente” no garfo à sua esquerda. Uma forma de evitar este deadlock consiste em introduzir um empregado de mesa que um filósofo tem que requisitar para o ajudar a pegar nos garfos. Este problema pode ser modelado pelo seguinte algoritmo concorrente.

   var
     waiter : boolean = true;
     fork   : array [0..N-1] of boolean = [N of true];
   
   function left(i : integer) : integer;
   begin
     left := i;
   end;

   function right(i : integer) : integer;
   begin
     right := mod (i-1) N;
   end;

   procedure phil(i : integer);
   begin
     while true do
     begin
0:     (* think *)
       repeat until waiter;
       waiter := false;
1:     repeat until fork[left(i)];
       fork[left(i)] := false;
2:     repeat until fork[right(i)];
       fork[right(i)] := false;
       waiter := true;
3:     (* eat *)
       fork[left(i)] := true;
       fork[right(i)] := true;       
     end
   end;

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

Exercício: especifique este algoritmo em TLA+ e verifique que filósofos vizinhos nunca comem ao mesmo tempo.

Exercício: como verificar que qualquer filósofo que já requisitou o empregado vai inevitavelmente comer?

Verificação de algoritmos distribuídos

Considere agora o seguinte algoritmo (ou protocolo) distribuído para eleição de um líder numa rede organizada num anel introduzido por Chang e Roberts em 1979. Assume-se que cada um dos nós tem um identificador numérico único, sendo que o algoritmo garante que o nó com o identificador mais alto se auto-eleja como líder. O algoritmo funciona da seguinte forma. Cada nó começa por enviar para o ser sucessor o seu identificador. Depois, sempre que um nó recebe um identificador compara-o com o seu próprio identificador: se for menor então é ignorado; se for maior ou igual então propaga-o para o nó sucessor; adicionalmente, se for igual então auto-elege-se como líder. Este algoritmo pode ser descrito da seguinte forma, onde se assume que succ(id) devolve o identificador do nó sucessor de id no anel. Para armazenar as mensagens enviadas iremos canais de comunicação representados pelo tipo channel, sendo que send é um procedimento que envia uma mensagem para um canal, receive é uma função que bloqueia até que um canal tenha uma mensagem, que depois é devolvida e apagada, e empty é uma função que testa se um canal está vazio.

   var 
     outbox : array [1..N] of channel;
     inbox  : array [1..N] of channel;

   procedure node(id : integer);
     var 
       elected : boolean = false;
       msg : integer;
   begin
     send(id,outbox[id]);
0:   while true do
     begin
       msg := receive(inbox[id]);
       if msg >= id then send(msg,outbox[id]);
       if msg =  id then elected := true
     end
   end;

   procedure transmit;
     var 
       msg : integer;
       id : integer; 
   begin
0:   while true do
     begin
       repeat id := 1..N until not empty(outbox[id]);
       msg := receive(outbox[id]);
       send(msg,inbox[succ(id)])
     end
   end;

   node(1) || ... || node(N) || transmit

Note que, tal como na maioria dos algoritmos distribuídos, se assume que cada nó processa uma das mensagens recebidas de forma atómica (como não temos memória partilhada não é relevante analisar os possíveis interleavings entre a execução dos diferentes nós), daí apenas ser usada uma etiqueta no ciclo infinito que os caracteriza.

A propriedade fundamental de um algoritmo de eleição de um líder, de que um e um só líder vai inevitavelmente ser eleito, pode ser decomposta em propriedades mais simples (as duas primeiras de safety e a última de liveness):

• No máximo é eleito um líder
• Se um nó é eleito líder então continua líder para sempre
• Será eleito pelo menos um líder

A especificação TLA+ deste protocolo é apresentada de seguida. Note que neste caso (tal como na maioria dos protocolos distribuídos) não é preciso uma variável para o program counter, porque os nós repetem o mesmo comportamento atómico indefinidamente. Neste caso concreto também não iremos precisar de declarar a variável msg nem a variável id do transmit, pois usaremos quantificação existencial para escolher o canal e a mensagem a processar. Dependendo das garantias oferecidas pela rede, ao especificar um algoritmo distribuídos os canais de comunicação podem ser modeladas por sequências ou conjuntos, caso a rede garanta ou não a entrega de mensagens por ordem. Neste caso, vamos verificar que o protocolo é correto mesmo que as mensagens não sejam entregues por ordem, pelo que vamos modelar as caixas de mensagens por conjuntos.

O TLA+ não tem operadores de fecho transitivo nativos, mas permite definir funções de forma recursiva, pelo que, para testar que a função succ de facto representa um anel com todos os nós (a rede é fortemente ligada), podemos calcular os nós alcançáveis com uma definição recursiva.

------------------------- MODULE LeaderElectionRing -------------------------

EXTENDS Naturals

CONSTANTS N, succ

Node == 1..N

reachable(n) ==
  LET aux[i \in Nat] == 
    IF i = 1 THEN { succ[n] }
    ELSE aux[i-1] \cup { x \in Node : \E y \in aux[i-1] : x = succ[y] }
  IN aux[N]

ASSUME 
    /\ N > 0
    /\ succ \in [Node -> Node]
    /\ \A x \in Node : Node \subseteq reachable(x)
    
VARIABLES outbox, inbox, elected

TypeOK == [] (outbox \in [Node -> SUBSET Node] /\ inbox \in [Node -> SUBSET Node] /\ elected \in [Node -> BOOLEAN])

Init ==
    /\ outbox  = [id \in Node |-> {id}]
    /\ inbox   = [id \in Node |-> {}]
    /\ elected = [id \in Node |-> FALSE]
    
transmit == \E id \in Node : \E m \in outbox[id] :
    /\ outbox' = [outbox EXCEPT ![id] = @ \ {m}]
    /\ inbox'  = [inbox  EXCEPT ![succ[id]] = @ \cup {m}]
    /\ UNCHANGED elected
    
node(id) == \E m \in inbox[id] :
    /\ inbox'   = [inbox EXCEPT ![id] = @ \ {m}]
    /\ outbox'  = IF m >= id 
                  THEN [outbox EXCEPT ![id] = @ \cup {m}]
                  ELSE outbox
    /\ elected' = IF m = id
                  THEN [elected EXCEPT ![id] = TRUE]
                  ELSE elected

Next == transmit \/ \E id \in Node : node(id)

vars == <<outbox, inbox, elected>>

Spec == Init /\ [][Next]_vars

AtMostOneLeader == [] (\A x,y \in Node : elected[x] /\ elected[y] => x = y)

LeaderStaysLeader == \A x \in Node : [] (elected[x] => [] (elected[x]))

AtLeastOneLeader == WF_vars(Next) => <> (\E x \in Node : elected[x]) 

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

Exercício: como poderia usar o TLC para mostrar um traço onde num anel com 5 nós ordenados de forma decrescente um dos nós é eleito líder?

Exercício: para reduzir o numero de transições e aumentar a eficiência do model checking altere a especificação do transmit por forma a que transmita simultaneamente todas as mensagens que estejam em qualquer outbox (desde que haja alguma mensagem para transmitir). Como sugestão, sugere-se que comece por definir uma função que para cada nó devolve o seu predecessor no anel, usando o operador CHOOSE do TLA+.

Exercício: para aumentar ainda mais a eficiência, especifique uma versão deste protocolo sem a outbox e sem o transmit, onde sempre que uma mensagem é enviada é diretamente colocada na inbox do nó sucessor.

O protocolo alternating bit permite garantir a entrega de mensagens mesmo com perdas. A ideia é o nó transmissor repetir o envio de uma mensagem até receber o acknowledgment respetivo do nó receptor. Para ter a certeza que recebeu o acknowledgment da mensagem que está a tentar enviar, as mensagens enviadas contêm um bit de controlo que deve ser incluído no acknowledgement, alternando este bit quando este acknowledgment é recebido. Neste protocolo assume-se que os canais de comunicação não trocam a ordem das mensagens e que tem capacidade para no máximo K mensagens. Assume-se também que a mensagem a enviar é um valor entre 1 e N escolhido de forma não-determinística. Este protocolo pode ser descrito pelo seguinte algoritmo.

   type message = record
     msg: 1..N;
     bit: 0..1;
   end;

   var msgs : channel;
       acks : channel;

   procedure transmitter;
     var bit : 0..1 = 0;
         data : 1..N;
         m : message;
   begin
0:   while true do
     begin
       (* receive ack *)
       if not empty(acks) then
       begin
         if receive(acks) = bit then
         begin
           bit := 1 - bit;
           data := 1..N;
         end
       end
       or else
       (* send msg *)
       begin
         m.msg := data;
         m.bit := bit;
         send(m,msgs)
       end;
     end
   end;

   procedure receiver;
     var bit : 0..1 = 1;
         rcvd : 1..N;
         m : message;
   begin
0:   while true do
     begin
       (* receive msg *)
       if not empty(msgs) then
       begin
         m := receive(msgs);
         rcvd := m.msg;
         bit := m.bit;
       end
       or else
       (* send ack *)
       begin
         send(bit,acks)
       end;
     end
   end;

   procedure dropper;
   begin
0:   while true do
     begin
       (* drop msg *)
       if not empty(msgs) then receive(msgs)
       or else
       (* drop ack *)
       if not empty(drop) then receive(acks)
     end
   end;

   transmitter || received || dropper

Exercício: especifique este algoritmo em TLA+ e verifique que realmente garante que todos os valores enviados são recebidos (desde que as mensagens não sejam sempre perdidas). Use sequências para representar os canais e records para representar as mensagens enviadas. Sugere-se que especifique actions diferentes para os diferentes fluxos possíveis em cada nó.

Considere agora o seguinte protocolo distribuído centralizado para controlo de transações. Cada um dos nós trabalhadores começa a trabalhar numa tarefa. Quando esta é concluída com sucesso o trabalhador comunica o resultado ao nó mestre. Um trabalhador pode também abortar a sua tarefa espontaneamente. Quando o nó mestre já recebeu mensagens de todos os trabalhadores a informar que concluíram a sua tarefa, envia uma mensagem para todos a informar que podem fazer commit da mesma. O nó mestre pode também a qualquer momento mandar abortar a execução. Este protocolo pode ser descrito pelo seguinte algoritmo distribuído, onde se assume que os canais não perdem mensagens mas podem trocar a ordem de entrega.

   type status = (Working,Prepared,Aborted,Committed);

   type message = record
     from: 0..N;
     type: status;
   end;

   var inbox : array [0..N] of channel;

   procedure worker(id : integer);
     var state : status = Working;
         msg : message; 
   begin
0:   while true do
     begin
       (* Finish task *)
       if state = Working then
       begin 
         state := Prepared; 
         msg.from = id;
         msg.type = Prepared;
         send(msg,inbox[0])
       end
       or else
       (* Abort task *)
       if state = Working then 
       begin
         state := Aborted
       end
       or else
       (* Receive message *)
       if not empty(inbox[id]) then
       begin
         msg := receive(inbox[id]); 
         if msg.type = Aborted or msg.type = Committed then state := msg.type;
       end
     end
   end;

   procedure broadcast(msg : message);
     var id : integer = 1;
   begin
     while id <= N do
     begin
       send(msg,inbox[id]);
       id := id + 1
     end
   end;

   procedure master;
     var state : status = Working;
         prepared : array 1..N of boolean = [N of false];
         msg : message;
     procedure 
   begin
0:   while true do
     begin
       (* Abort transaction *)
       if state = Working then
       begin 
         state := Aborted; 
         msg.from = 0;
         msg.type = Aborted;
         broadcast(msg)
       end
       or else
       (* Receive message *)
       if not empty(inbox[0]) then
       begin
         msg := receive(inbox[0]);
         prepared[msg.from] := true; 
         if state = Working and prepared = [N of true] then 
         begin 
           msg.from = 0;
           msg.type = Committed;
           state := Committed; 
           broadcast(msg) 
         end
       end
     end
   end;

   master || worker(1) || ... || worker(N)

Exercício: especifique este algoritmo em TLA+ e verifique as seguintes propriedades. Sugere-se que especifique actions diferentes para os diferentes fluxos possíveis em cada nó.

• Consistência, nunca é possível que dois nós estejam nos estados Aborted e Committed simultaneamente.
• Estabilidade, uma vez Committed ou Aborted um nó fica nesse estado para sempre.
• Progresso, depois de um nó ficar Committed todos vão inevitavelmente ficar Committed.