Verificação Formal: Aula 3

Especificação e verificação de algoritmos self-stabilizing

Um algoritmo self-stabilizing tem por objetivo fazer com que um sistema estabilize num estado “legítimo”, qualquer que seja o estado inicial. Estes algoritmos conferem garantias de segurança mesmo na presença de erros tais como alterações no estado da memória. O conceito de self-stabilization e o primeiro algoritmo desta classe foram introduzidos por Edsger Dijkstra em 1973 no manuscrito EWD 391 (e mais tarde publicados num artigo na Communications of the ACM), 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 “legítimo” um estado onde exatamente um dos nós possui o “privilégio” de executar, privilégio esse que vai depois circulando entre eles. Cada nó tem uma variável x que pode conter um valor na gama 0..K-1, e assume-se que um nó consegue de alguma forma ler a variável do vizinho que o precede. Um nó sabe se tem o privilégio de executar através de uma comparação do valor da sua variável com o valor desse vizinho, e quando executa altera o valor da sua variável. As regras para determinar se um nó tem o privilégio e a alteração efetuada na variável x são diferentes para o nó bottom e para os restantes, e podem ser encontradas no artigo da CACM mencionado acima. As propriedades desejadas para um algoritmo self-stabilizing são as seguintes:

• Closure: uma vez atingido um estado legítimo, o sistema fica para sempre num estado legítimo.
• Convergence: o sistema vai inevitavelmente chegar a um estado legítimo.

Assumindo que existe um central daemon a controlar que os nós executam de forma atómica e interleaved, o algoritmo supostamente garante estas duas propriedades desde que K >= N, tal como podemos verificar com a seguinte especificação em TLA+.

------ MODULE SelfStabilizingRing ------

EXTENDS Naturals

CONSTANT N,K
ASSUME N >= 1 /\ K >= N

VARIABLES x

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

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

HasPrivilege(i) == IF i = 0 THEN x[0] = x[N] ELSE x[i] /= x[i-1]

Bottom == HasPrivilege(0) /\ x' = [x EXCEPT ![0] = (@ + 1) % K]

Other(i) == HasPrivilege(i) /\ x' = [x EXCEPT ![i] = x[i-1]]

Next == Bottom \/ \E i \in 1..N : Other(i)

Spec == Init /\ [][Next]_x /\ WF_x(Next)

Legitimate == (\E i \in 0..N : HasPrivilege(i) /\ \A j \in 0..N : j /= i => ~HasPrivilege(j))

Closure == [] (Legitimate => [] Legitimate)

Convergence == <> Legitimate

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

Exercício: Para validar esta especificação, mostre como poderia obter um cenário onde o estado inicial não é legítimo e o sistema converge para um estado legítimo.

Exercício: De facto, para além de existir exatamente um nó com o privilégio, um estado só é legítimo se esse privilégio depois passar por todos os nós. Modifique a propriedade Legitimate por forma a incorporar esta condição e descubra uma configuração para a qual o algoritmo não funciona corretamente.

Desafio: Como poderia usar o TLA+/TLC para encontrar automaticamente essa configuração errada?

Desafio: Como poderia usar o TLA+/TLC para verificar a versão do algoritmo sem o central deamon, onde um ou mais nós com o privilégio podem executar em paralelo? Neste caso o algoritmo só é correto se K > N.

Exercício: Especifique e verifique o algoritmo self-stabilizing proposto por Dijkstra no manuscrito EWD 392 (também publicado no referido artigo da CACM), que funciona para uma sequência de N+1 nós.