Hoje continuaremos o estudo da verificação de modelos com PROMELA e SPIN. O resumo a seguir foi escrito a partir do capítulo 4 do livro The SPIN Model Checker, e o capítulo 6 do livro Design and Validation of Computer Protocols.

Verificação de propriedades

Do ponto de vista de um sistema distribuído ou concorrente, podem-se identificar dois requisitos para a correção de um sistema:

Segurança (safety): segurança diz respeito ao que não deve ser possível ocorrer no sistema, ou ao conjunto de propriedades que não podem ser violadas. Isso inclui estados que nunca devem ser alcançados, ou sequências de estados as quais não podem ocorrer.
Vivacidade (liveness): vivacidade diz respeito ao que sempre deve valer para o sistema, ou ao conjunto de propriedades que sempre devem ser satisfeitas.

Para fins de verificação de propriedades, PROMELA/SPIN definem dois tipos de reivindicações de correção:

alcançabilidade: esse tipo de reivindicação se baseia em estados alcançáveis ou inalcançáveis. Isso também se chama propriedades de estado.
factibilidade: esse outro tipo de reivindicação se baseia na executabilidade ou não de sequências de estados. Isso também é chamado de propriedades de caminho.

Verificação de condições (assertions)

A verificação de uma condição pode ser feita com o comando assert. Esse comando verifica se uma expressão avalia para verdadeiro e, caso contrário, interrompe a execução do programa. Isso pode ser usado para a verificação pontual de uma propriedade do sistema.

chan canal1 = [1] of {int}
chan canal2 = [1] of {int}

active proctype p1() {
  int msg
  int n1 = 0
  int n2 = 0
 
  do
  :: canal1?msg -> n1++; assert(n1 < 10)
  :: canal2?msg -> n2++; assert(n2 < 15)
  od
}

active proctype p2() {
  do
  :: canal1!1
  :: canal2!1
  od
}

No exemplo acima, o processo p1 aceita que sejam recebidas no máximo 10 mensagens pelo canal1 e 15 mensagens pelo canal2.

Para verificar condições em um modelo, deve-se compilá-lo da seguinte forma:

# opção -a: usada para gerar um verificador, que estará no arquivo pan.c
./spin -a djikstra.pml

# Compila o verificador, que será o programa "pan"
gcc -o pan pan.c

# Executa o verificador
./pan

Meta-rótulos (meta labels)

Três tipos especiais de rótulos podem ser inseridos em um programa para orientar o verificador a identificar certos estados no sistema:

end: rótulos com prefixo end marcam estados finais de um processo. Inicialmente, o estado final de um processo é criado implicitamente na chave final de sua declaração }. Porém há situações em que um processo nunca termina, porém isso não se configura um erro. Assim, rótulos end possibilitam informar que outros estados do processo são finais.
progress: rótulos com prefixo progress informam que certos estados, se visitados, indicam que um processo está progredindo sua execução. Em outras palavras, que a execução não está presa em algum laço indefinidamente.
accept: rótulos com prefixo accept marcam estados que não devem ser visitados infinitamente frequente. Isso pode ser usado para identificar ciclos de visitação de estados os quais não devem ocorrer indefinidamente.

O meta-rótulo end

O exemplo a seguir mostra dois processos que trocam mensagens entre si. O processo ping envia uma mensagem para o processo pong, que a devolve como resposta. Após o envio de dez mensagens, o processo ping termina. O processo pong fica então indefinidamente aguardando uma mensagem que não será recebida. Uma situação como essa é interpretada pelo spin como um estado final indesejado.

chan c1 = [1] of {int}
chan c2 = [1] of {int}

active proctype ping() {
  int x,y

  do
  :: x < 10 ->
    c1!x
    printf("%d enviou %d\n", _pid, x)
    x++
    c2?y
    printf("%d recebeu resposta: %d\n", _pid, y)
  :: else -> break
  od
}


active proctype pong() {
  int x

loop:

  c1?x
  printf("%d recebeu %d\n", _pid, x)
  c2!x
  printf("%d devolveu: %d\n", _pid, x)
  
  goto loop
}

Para experimentar o diagnóstico do spin sobre esse modelo, deve-se compilar o verificador da seguinte forma:

aluno@M1:~$ spin -a ping.pml
aluno@M1:~$ gcc -DSAFETY -o pan pan.c

A execução do verificador, e o resultado por ele apresentado, são mostrados a seguir:

aluno@M1:~$ ./pan
pan:1: invalid end state (at depth 90)
pan: wrote end.pml.trail

(Spin Version 6.4.3 -- 16 December 2014)
	+ Partial Order Reduction

O verificador informou que o modelo termina ou bloqueia em um estado final inválido, e a demonstração de uma sequência de execução onde o problema ocorre está gravada no arquivo end.pml.trail. Para reproduzi-lo usa-se o spin assim (obs: o resultado copiado omite as linhas iniciais):

aluno@M1:~$ spin -t end.pml
spin: trail ends after 91 steps
#processes: 2
		queue 1 (c1): 
		queue 2 (c2): 
 91:	proc  1 (pong:1) end.pml:24 (state 1)
 91:	proc  0 (ping:1) end.pml:16 (state 12) <valid end state>
2 processes created

O diagnóstico mostra que o processo 1 (pong) parou no estado inválido correspondente à linha 24, que contém a sentença c1?x. O processo 0 (ping) terminou em um estado válido na linha 16 (o fim do processo).

No sistema representado por esse modelo, pode-se considerar que o processo pong terminar aguardando por uma mensagem seja um estado final válido. Afinal, o processo pong apenas reage a mensagens recebidas do processo ping. Para descrever isso no modelo, deve-se informar ao spin que a espera por mensagem no processo pong é um estado final válido. Isso pode ser feito com um meta-rótulo end:

chan c1 = [1] of {int}
chan c2 = [1] of {int}

active proctype ping() {
  int x,y

  do
  :: x < 10 ->
    c1!x
    printf("%d enviou %d\n", _pid, x)
    x++
    c2?y
    printf("%d recebeu resposta: %d\n", _pid, y)
  :: else -> break
  od
}


active proctype pong() {
  int x

loop:

end:  c1?x
  printf("%d recebeu %d\n", _pid, x)
  c2!x
  printf("%d devolveu: %d\n", _pid, x)
  
  goto loop
}

Após essa alteração no modelo, deve-se gerar um novo verificador. A execução desse verificador agora informa que o modelo é válido:

aluno@M1:~$ spin -a end.pml
aluno@M1:~$ gcc -DSAFETY -o pan pan.c
aluno@M1:~$ ./pan
(Spin Version 6.4.3 -- 16 December 2014)
	+ Partial Order Reduction

O meta-rótulo progress

Usando o exemplo apresentado no caso do meta-rótulo end, faz-se uma alteração para que ambos processos nunca terminem. O processo ping fica eternamente enviando mensagens para pong, que simplesmente as responde. Esse novo modelo está mostrado a seguir:

chan c1 = [1] of {int}
chan c2 = [1] of {int}

active proctype ping() {
  int x,y

loop:
    c1!x
    printf("%d enviou %d\n", _pid, x)
    x = !x
    c2?y
    printf("%d recebeu resposta: %d\n", _pid, y)

    goto loop
}


active proctype pong() {
  int x

loop:

  c1?x
  printf("%d recebeu %d\n", _pid, x)
  c2!x
  printf("%d devolveu: %d\n", _pid, x)
  
  goto loop
}

Nitidamente não há um deadlock, uma vez que os processos não trancam em disputa por recursos, e tampouco algum processo termina porque não pode mais prosseguir. Por outro lado, ambos processos executam indefinidamente um ciclo de instruções, e isso pode significar um funcionamento anômalo chamado de livelock. O spin é capaz de detectar esse comportamento, e informá-lo como resultado do verificador. No caso do modelo em questão, o uso do verificador deve ser feito desta forma (observe a opção -l passada ao verificador):

aluno@M1:~$ spin -a ping.pml
aluno@M1:~$ gcc -DNP -o pan pan.c
aluno@M1:~$ ./pan -l
pan:1: non-progress cycle (at depth 14)
pan: wrote prog.pml.trail

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
	+ Partial Order Reduction

Nem todo ciclo que não termina é um livelock. O verificador pode ser informado de que, se um processo passar de forma infinitamente frequente por um ciclo, isso significa que o processo está progredindo. Para esas finalidade existe o meta-rótulo progress. No exemplo dos processos ping e pong, esse meta-rótulo pode ser usado assim:

chan c1 = [1] of {int}
chan c2 = [1] of {int}

active proctype ping() {
  int x,y

loop:

progress:    c1!x
    printf("%d enviou %d\n", _pid, x)
    x = !x
    c2?y
    printf("%d recebeu resposta: %d\n", _pid, y)

    goto loop
}


active proctype pong() {
  int x

loop:

  c1?x
  printf("%d recebeu %d\n", _pid, x)
  c2!x
  printf("%d devolveu: %d\n", _pid, x)
  
  goto loop
}

O verificador criado a partir desse modelo fornece um diagnóstico sem livelock:

aluno@M1:~$ spin -a ping.pml
aluno@M1:~$ gcc -DNP -o pan pan.c
aluno@M1:~$ ./pan -l

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
	+ Partial Order Reduction

Um exemplo baseado num semáforo

O exemplo a seguir mostra o uso de um rótulo end, em um modelo sobre semáforos. O processo Djikstra nunca termina, pois ele implementa um semáforo e deve estar sempre disponível para atender pedidos de entrada em seção crítica. Assim, o estado em que inicia a verificação do semáforo é um estado final.

mtype { p, v };

chan sema = [0] of { mtype };

active proctype Dijkstra()
{       byte count = 1;
end:    do
        :: (count == 1) ->
                sema!p; count = 0
        :: (count == 0) ->
                sema?v; count = 1
        od
}

active [3] proctype user()
{       do
        :: sema?p;        /* enter */
critical: skip;           /* leave */
          sema!v;
        od
}

Uma pequena alteração no exemplo demonstra o uso de um rótulo progress. Neste caso, marca-se o estado em que se libera o semáforo como sendo um estado indicador de progresso. Se o processo Djikstra passar frequentemente por esse estado, o verificador conclui que o processo está em progresso.

active proctype Dijkstra()
{       byte count = 1;
end:    do
        :: (count == 1) ->
progress:       sema!p; count = 0
        :: (count == 0) ->
                sema?v; count = 1
        od
}

Como gerar um verificador com SPIN

Os exemplos anteriores mostram como simular modelos escritos em PROMELA. A verificação desses modelos envolve a criação de um verificador, o que deve ser feito desta forma:

Execute o spin instruindo-o a gerar um verificador:
```
./spin -a modelo.pml
```
O comando anterior deve gerar um arquivo de programa pan.c. Compile-o com este comando:
```
gcc -o pan pan.c
```
Execute o verificador:
```
./pan
```
Pode-se executar o verificador de formas alternativas. Por exemplo, para buscar ciclos sem progresso no modelo:
```
./pan -l
```
Outras opções do verificador podem ser vistas com:
```
./pan -h
```

Atividade

Para exercitar a verificação de protocolos, faça o seguinte:

Verifique os modelos para o problema do produtor e consumidor, de forma que:
- Toda mensagem produzida seja efetivamente consumida
- Toda mensagem deva ser consumida uma única vez
(OPCIONAL) Verifique o modelo para o problema dos filósofos glutões, supondo a existência de 5 filósofos, de forma que:
- Não exista deadlock
- Nenhum filósofo morra de fome
- Um garfo é pego por um único filósofo a cada vez
Verifique o modelo para um protocolo do tipo pare-e-espere em um ambiente de execução em que erros são possíveis, tais como perdas de mensagens (tanto dados quanto ack). As seguintes propriedades devem ser verificadas:
- Uma nova mensagem é transmitida somente se a mensagem anterior for devidamente entregue
- Toda mensagem transmitida é entregue em algum momento futuro
- Toda mensagem recebida é consumida uma única vez
- Ausência de livelock
Verifique o modelo para um protocolo que faça autenticação de usuário, de forma que:
- Mensagens são transmitidas somente após cliente autenticado
- Mensagens recebidas são aceitas apenas após cliente autenticado

Verifique o modelo para o enquadramento que foi implementado no protocolo ponto-a-ponto, de forma que:

Flags aparecem somente como delimitadores de quadro
Não há byte especial dentro de um quadro, a não ser que seja um ESC

Perda de sincronismo acarreta descarte de bytes recebidos

// modelo para o transmissor ... falta o receptor !!

mtype = {flag, esc, comum}
chan serial = [1] of {mtype}

active proctype TX() {
  int bytes

envia:
  serial!flag
  bytes = 0  
  do
  :: bytes < 4 ->
     if
     :: serial!comum
     :: serial!esc -> serial!comum
     fi
     bytes++
  :: else -> break
  od

  serial!flag
  
  goto envia
}

PTC29008: Verificação de Protocolos: Propriedades

Índice