MFP

Logo

Índice

Métodos Formais em Engenharia de Software
Cálculo de Sistemas de Informação
Programação Ciber-física
Verificação Formal
Calendário | Sumários
Anos anteriores
Alumni

Verificação Formal: Aula 4

Especificação e verificação de algoritmos distribuídos

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):

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 especificado por uma única action, designada node(i). Para modelar a transmissão de mensagens, vamos assumir que cada nó tem uma outbox e uma inbox onde se encontram as mensagens enviadas e recebidas. Dependendo das garantias oferecidas pela rede, ao especificar um algoritmo distribuído estas mailboxes 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 as caixas de mensagens por conjuntos. O envio das mensagens de um nó para o seu sucessor é especificada pela action transmit. 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 outbox, inbox, elected

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

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

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

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

vars == <<outbox, 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.

CONSTANTS N = 4 id <- ring4
SPECIFICATION Spec 
PROPERTIES TypeOK 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: Para reduzir o numero de transições e aumentar a eficiência do model checking, 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.

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 simples, onde temos uma única action onde o nó com o maior identificador se auto-elege como líder.

O protocolo alternating bit tem por objetivo garantir a entrega de mensagens mesmo com perdas. A ideia é o nó transmissor (que iremos designar por nó 0) repetir o envio de uma mensagem até receber o ack(nowledgment) respetivo do nó receptor (o nó 1). Para ter a certeza que recebeu o ack da mensagem que está a tentar enviar, as mensagens enviadas contêm um bit de controlo que deve depois ser incluído no respetivo ack, alternando este bit depois de recebido o ack. Neste protocolo assume-se que os canais de comunicação não trocam a ordem das mensagens e vamos também assumir têm capacidade para no máximo K mensagens. Assume-se também que as mensagens a enviar são valores entre 1 e N escolhido de forma não-determinística. Assumindo que não há perca de mensagens este protocolo pode ser especificado da seguinte forma em TLA+. A função bit contém o bit que cada nó está a usar em cada momento para enviar mensagens (nó 0) ou acks (nó 1). A função msg contém a próxima mensagem que se pretende enviar (nó 0) ou a última mensagem recebida (nó 1). Se não se pretende enviar nenhuma mensagem ou ainda não foi recebida nenhuma mensagem terá o valor 0. A função inbox contém a sequência de mensagens recebida por cada nó. No caso do nó 1 as mensagens são tuplos com o valor enviado e o respetivo bit de controlo. No caso do nó 0 as mensagens recebidas são apenas os bits de ack.

---- MODULE Alternating ----

EXTENDS Naturals, Sequences

CONSTANT N, K

ASSUME N > 0 /\ K > 0

VARIABLES bit, msg, inbox

vars == << bit, msg, inbox >>

TypeOK == 
    /\ bit \in [0..1 -> 0..1] 
    /\ msg \in [0..1 -> 0..N] 
    /\ inbox[1] \in Seq([msg : 1..N, bit : 0..1]) 
    /\ inbox[0] \in Seq(0..1)

Init == 
    /\ bit = [ i \in 0..1 |-> i ] 
    /\ msg = [ i \in 0..1 |-> 0 ]
    /\ inbox = [ i \in 0..1 |-> <<>> ]

ChooseMsg ==
    /\ msg[0] = 0
    /\ msg' \in [0..1 -> 0..N]
    /\ msg'[0] # 0
    /\ msg'[1] = msg[1]
    /\ UNCHANGED << bit,inbox >>

SendMsg ==
    /\ msg[0] # 0
    /\ Len(inbox[1]) < K
    /\ inbox' = [inbox EXCEPT ![1] = Append(@,[msg |-> msg[0], bit |-> bit[0]])]
    /\ UNCHANGED << bit,msg >>

ReceiveMsg ==
    /\ inbox[1] # <<>>
    /\ bit' = [ bit EXCEPT ![1] = Head(inbox[1]).bit ] 
    /\ msg' = [ msg EXCEPT ![1] = Head(inbox[1]).msg ]
    /\ inbox' = [inbox EXCEPT ![1] = Tail(@)]

SendAck == 
    ...

ReceiveAck ==
    ...

Next == ChooseMsg \/ SendMsg \/ ReceiveMsg \/ SendAck \/ ReceiveAck

Fairness == WF_vars(SendMsg) /\ WF_vars(ReceiveMsg) /\ WF_vars(SendAck) /\ WF_vars(ReceiveAck)

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

AllSentReceived == [] (msg[0] # 0 => <> (msg[0] = 0))

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

Para verificar a propriedade AllSentReceived e o invariante TypeOK podemos usar o seguinte ficheiro de configuração.

CONSTANTS N = 3 K = 2
SPECIFICATION Spec
INVARIANT TypeOK
PROPERTY AllSentReceived

Exercício: Complete a especificação do protocolo, especificando as actions SendAck e ReceiveAck.

Exercício: Mostre como poderia usar o TLC para ver um cenário onde uma mensagem é enviada com sucesso (ou seja, o respetivo ack chegou ao nó emissor).

Exercício: Modifique a sua especificação por forma a modelar a perda de mensagens, e verifique se o protocolo continua a ser correto nestas condições.

Exercício: Como poderia verificar a propriedade de safety que diz que todas as mensagens recebidas foram enviadas antes?

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.

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