Especificação e verificação de algoritmos distribuídos com TLA+

Eleição de um líder num anel

Considere o 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-elege como líder. O algoritmo funciona da seguinte forma. Cada nó começa por enviar para o 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 sucessor; se for igual então auto elege-se como líder.

A propriedade fundamental que queremos verificar num 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. Os parâmetros desta especificação são o número N > 0 de nós no anel e uma função id que diz qual o identificador de cada nó.

Na modelação de algoritmos distribuídos tipicamente assume-se 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). Sendo assim, o comportamento do nó i vai ser normalmente especificado por uma action por cada tipo de mensagem que pode ser recebida.

Para modelar a transmissão de mensagens, vamos assumir que entre cada dois nós existe um canal de comunicação onde estão as mensagens já enviadas por um nó mas ainda não recebidas pelo seu sucessor. Dependendo das garantias oferecidas pela rede, ao especificar um algoritmo distribuído estes canais podem ser representadas 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 estes canais usando conjuntos de mensagens. Na especificação seguinte o canal de comunicação entre um nó e o seu sucessor é designado como sendo a inbox deste último. Para simplificar a especificação do protocolo vamos assumir que no estado inicial já enviou para o seu sucessor o seu identificador.

Para da inbox temos também uma variável booleana elected por cada nó que será verdade sse o nó for o líder eleito. A especificação também inclui um exemplo de uma função id, designada ring4, que será usada no ficheiro de configuração.

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

EXTENDS Naturals,TLC

CONSTANTS N, id

Node == 0..N-1

ring4 == 0 :> 35 @@ 1 :> 10 @@ 2 :> 5 @@ 3 :> 20

ASSUME 
    /\ N > 0
    /\ id \in [Node -> Nat]
    /\ \A i,j \in Node : i /= j => id[i] /= id[j]
    
VARIABLES inbox, elected

succ(i) == (i + 1) % N
pred(i) == (i - 1) % N

TypeOK == inbox \in [Node -> SUBSET Nat] /\ elected \in [Node -> BOOLEAN]

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

Next == \E i \in Node : receive(i)

vars == <<inbox, elected>>

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

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

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

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

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

Para verificar as propriedades especificadas para um anel com 4 nós e com os identificadores indicados na função ring4 podemos usar o seguinte ficheiro de configuração. Neste caso a opção de verificar a existência de deadlocks é desativada porque este algoritmo pode terminar quando todas as mensagens em todas os canais de comunicação já tiverem sido lidas.

CONSTANTS N = 4 id <- ring4
SPECIFICATION Spec 
INVARIANT TypeOK
PROPERTIES AtMostOneLeader LeaderStaysLeader AtLeastOneLeader
CHECK_DEADLOCK FALSE

Exercício: Como poderia usar o TLC para mostrar um traço onde num anel com 5 com ids decrescentes um dos nós é eleito líder?

Exercício: Em vez de assumir que no estado inicial todos os nós já iniciaram o protocolo, como poderia especificar uma versão onde temos explicitamente uma action onde um nó inicia a execução?

Exercício: Como poderia usar o TLA+/TLC verificar que o protocolo é correto quaisquer que sejam os identificadores dos nós no anel?

Exercício: Verifique que este protocolo é um refinamento de uma especificação muito abstrata onde não há sequer troca de mensagens e onde temos uma única action onde o nó com o maior identificador se auto-elege como líder.

Exercício: Verifique que o protocolo não funciona corretamente se os nós puderem re-iniciar a execução do protocolo. Verifique que também não funciona corretamente mesmo que as mensagens sejam entregues por ordem (para tal modele as inboxes como sequências de capacidade limitada, usando uma constante K para definir a capacidade das mesmas).

Exercício: Modifique o protocolo acrescentando uma segunda fase onde o nó eleito informa os restantes de que é o líder. Para tal altere a variável elected para passar a conter qual o nó que é líder (ou um valor especial None quando um nó ainda não sabe quem é o líder). Também será necessário passar a ter dois tipos de mensagens (mensagens de eleição vs comunicação do líder). Para modelar as mensagens sugere-se que use records com um campo que indica qual o tipo da mensagem e outro com o respetivo payload (neste caso o identificador de um nó). O valor None pode ser especificado com o operador CHOOSE da seguinte forma:

None == CHOOSE x \in Nat : x \notin {id[i] : i \in Node}

Ou seja, None é um natural qualquer que seja distinto dos identificadores dos nós. Para ser possível fazer model-checking, no ficheiro de configuração este valor terá que ser redefinido com uma constante apropriada.

Two-phase commit

Exercício: O protocolo two-phase commit tem por objetivo garantir a execução atómica de transações numa base de dados distribuída. Neste protocolo temos um nó coordenador que gere a execução do protocolo e N nós trabalhadores que tentam executar as transações. Todos os nós começam num estado idle. O nó coordenador começa por enviar para os nós trabalhadores um pedido para iniciarem o commit, e fica num estado waiting. Após receberem este pedido, os nós trabalhadores podem passar para o estado prepared se for possível executar a transação ou para o estado aborted se não for possível e respondem ao coordenador com uma mensagem de sucesso ou falha, respetivamente. Se o nó coordenador receber mensagens de sucesso de todos os trabalhadores envia uma mensagem a todos a pedir para finalizarem o commit, passando depois para o estado committed. De igual forma, os nós trabalhadores passam para o estado committed após receberem esta mensagem. Se o nó coordenador receber uma mensagem de falha, envia imediatamente uma mensagem para todos os nós a pedir para fazerem abort, passando depois para o estado aborted. De igual forma, os nós trabalhadores passam para o estado aborted após receberem esta mensagem.

Especifique este protocolo em TLA+ e use o TLC para verificar que garante as seguintes propriedades:

• 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.

Protocolo echo para formação de uma spanning tree

Exercício: Modele o protocolo echo para formação de uma spanning tree numa rede conectada, proposto por Ernest Chang no artigo Echo Algorithms: Depth Parallel Operations on General Graphs, e verifique as propriedades fundamentais de terminação e correção parcial (quando o protocolo termina a relação first que é construída pelo protocolo contém de facto uma spanning tree com raiz no nó initiator). Sugere-se que use como ponte de partida o seguinte modelo das possíveis configurações do protocolo, onde a constante adj contém a configuração da rede, representada por uma função que para cada nó devolve o conjunto dos seus adjacentes. Para especificar que a rede é conectada (todos os nós estão acessíveis a partir do initiator) é usada a definição auxiliar reachable que calcula o conjunto dos nós acessíveis a partir de um determinado nó. Por sua vez, esta definição recorre a uma função definida recursivamente para calcular o conjunto de nós acessível a partir de um dado nó num determinado número máximo de passos.

------ MODULE Echo ------

EXTENDS Naturals, FiniteSets

CONSTANTS Node, Initiator, adj

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

ASSUME /\ Initiator \in Node
       /\ adj \in [ Node -> SUBSET Node ]
       \* no self loops
       /\ \A n \in Node : n \notin adj[n]
       \* undirected graph
       /\ \A x,y \in Node : y \in adj[x] <=> x \in adj[y]
       \* all nodes reachable from initiator
       /\ Node \ {Initiator} \subseteq reachable(Initiator)

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