Verificação Formal: Aula 5

Especificação de propriedades sobre o passado

Por vezes podemos querer especificar propriedades que se referem ao passado. Existe uma versão da lógica temporal linear que possui operadores temporais de passado e que facilita a escrita destas propriedades. Em particular, dada um predicado $P$, a fórmula $\square^{-1}\ P$ significa que $P$ foi sempre verdade e a fórmula $\lozenge^{-1}\ P$ significa que $P$ foi alguma vez verdade. Por exemplo, num algoritmo de exclusão mútua a fórmula $\square (pc_0 = 2 \Rightarrow \lozenge^{-1}\ pc_0 = 1)$ especifica que o processo $0$ só pode estar na região crítica se antes pediu para aceder à mesma.

O TLA não possui operadores temporais de passado, mas podemos especificar essas propriedades recorrendo a variáveis auxiliares no modelo que memorizam os factos relevantes do passado. Estas variáveis são designadas de variáveis de história. Por exemplo para especificarmos a propriedade acima podemos acrescentar uma variável booleana $wanted_0$ que memoriza se alguma vez foi verdade que $pc_0 = 1$. Com esta variável, a propriedade pode ser especificada como $\square (pc_0 = 2 \Rightarrow wanted_0)$. Para especificar a evolução do valor desta variável podemos no predicado que define o valor inicial incluir a fórmula $wanted_0 = (pc_0 = 1)$ e em todas as actions atualizar o seu valor da seguinte forma $wanted_0’ = wanted_0 \vee (pc_0’ = 1)$. Isto garante que a variável $wanted_0$ irá ficar com o valor verdadeiro mal a condição $pc_0 = 1$ seja verdadeira.

No caso geral para substituir uma fórmula $\lozenge^{-1}\ P$ iremos usar uma variável $h_P$, cujo valor inicial é $h_P = P$ e que evolui de acordo com a especificação $h_P’ = h_P \vee P’$. Para substituir uma fórmula $\square^{-1}\ P$ iremos usar uma variável $h_P$, cujo valor inicial é $h_P = P$ e que evolui de acordo com a especificação $h_P’ = h_P \wedge P’$ (neste caso a variável de história ficará com o valor falso mal o predicado $P$ deixe de ser verdade).

Exercício: utilize esta técnica para verificar que na sua especificação TLA+ no algoritmo de exclusão mútua com semáforos se os processos estão na região crítica é porque antes pediram para entrar.

Exercício: adapte a especificação TLA+ do algoritmo de eleição de líder num anel para verificar que qualquer mensagem recebida por um nó foi antes enviada pelo nó predecessor.

Exercício: no exemplo dos filósofos, como pode obter um exemplo de execução onde um filósofo repete o almoço depois de todos já terem comido?

Exercício: como se poderiam usar variáveis de história para verificar a propriedade $P\ \mathbf{until}\ Q$, onde $\mathbf{until}$ é o operador temporal que significa que $Q$ vai inevitavelmente ser verdade e até lá $P$ tem que ser verdade (ou, alternativamente, $P$ só pode deixar de ser verdade quando $Q$ se verificar)?

Introdução ao refinamento

Uma técnica comum para obter implementações com garantias de correção é através de refinamento de especificações mais abstratas. Essencialmente, o refinamento consiste em adicionar mais “detalhe” a uma especificação, tipicamente acrescentando mais variáveis e novos eventos que afetem essas variáveis. Um exemplo simples de refinamento consiste em acrescentar um ponteiro dos minutos a um relógio que só tinha ponteiro das horas. Tecnicamente, diz-se que um sistema refina outro se todos os comportamentos do primeiro são admitidos pelo segundo. Ao acrescentar variáveis e novos eventos, os comportamentos do sistema mais refinado podem ter passos que não são visíveis no sistema mais abstrato (porque afetam apenas as novas variáveis). Esses passos irão corresponder a passos de stuttering no sistema mais abstrato. Como no TLA somos obrigados a permitir sempre o stuttering na especificação de um sistema, podemos verificar que um sistema é um refinamento de outro com uma simples fórmula. Se a especificação do sistema mais abstrato for a fórmula $Spec$ e a especificação do sistema mais refinado for $Impl$, então para verificar que o segundo é realmente um refinamento do primeiro basta verificar a fórmula $Impl \Rightarrow Spec$.

Quando queremos verificar que a especificação abstrata satisfaz uma propriedade $Prop$ verificamos a fórmula $Spec \Rightarrow Prop$. Por consequência lógica teremos então que $Impl \Rightarrow Prop$. Ou seja, qualquer propriedade válida para o sistema mais abstrato também será válida para os seus refinamentos. Desta forma podemos garantir que as implementações obtidas por refinamento são corretas por construção. Muitas vezes também se usa o refinamento simplesmente como técnica de verificação e não para derivar implementações. Por vezes pode ser muito ineficiente verificar uma propriedade numa especificação (em particular, isto é frequentemente verdade para propriedades de liveness). Nesses casos podemos tentar verificar essas propriedades numa versão abstrata do algoritmo, onde a verificação seja eficiente, e depois simplesmente verificar que o algoritmo é um refinamento dessa versão mais abstrata.

Em TLA+ para verificar que um algoritmo refina outro podemos começar por especificar os dois algoritmos em módulos diferentes. Por exemplo, podemos ter a especificação de um relógio só com horas num módulo.

----- MODULE HourClock -----

EXTENDS Naturals

VARIABLES h

Init == h \in 0..23

Next == h' = (h + 1) % 24

Spec == Init /\ [][Next]_h /\ WF_h(Next)

Midnight == []<> (h = 0)

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

A especificação do comportamento deste relógio está na definição Spec (que inclui uma condição de justiça que obriga o relógio a avançar). O módulo inclui também a propriedade Midnight que é válida nesta especificação e que especifica que recorrentemente o relógio irá passar pela meia-noite.

Num módulo separado podemos ter a especificação do relógio com ponteiro dos minutos.

----- MODULE HourMinuteClock -----

EXTENDS Naturals

VARIABLES h,m

Init == h \in 0..23 /\ m \in 0..59

Next == 
    /\ IF m = 59 THEN h' = (h + 1) % 24 ELSE h' = h
    /\ m' = (m + 1) % 60

Spec == Init /\ [][Next]_<<h,m>> /\ WF_<<h,m>>(Next)

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

Este refinamento simplesmente acrescenta variável m que corresponde ao ponteiro para os minutos.

Para verificar que este relógio é um refinamento do anterior, bastaria importar o módulo HourClock e verificar que a propriedade Spec desse módulo é válida. No entanto se fizermos essa importação com a keyword EXTENDS iremos ter uma colisão de nomes, pois o módulo HourMinuteClock também tem uma definição chamada Spec e uma variável chamada h. Em vez de usarmos o EXTENDS para fazer a importação podemos usar a keyword INSTANCE que permite fazer a importação para um namespace diferente. Podemos depois aceder a uma definição do módulo importado prefixando o respetivo nome pelo namespace (com o separador !). No caso do nosso exemplo, podemos então acrescentar as seguintes linhas ao módulo HourMinuteClock, para importar o módulo HourClock para o namespace Mapping e definir a propriedade Refinement como uma abreviatura a propriedade Spec do módulo HourClock.

Mapping == INSTANCE HourClock

Refinement == Mapping!Spec

Para verificar que HourMinuteClock é um refinamento de HourClock basta então verificar com o TLC que a propriedade Refinement é válida se assumirmos que o HourMinuteClock se rege pela especificação Spec. Como consequência, teremos que o relógio com minutos também satisfaz a propriedade Midnight já verificada para o relógio apenas com horas.

Exercício: verifique que o sistema com N processos que incrementam uma variável partilhada é um refinamento de um algoritmo sequencial que simplesmente incrementa essa variável de 0 até N.

Refinement mappings

Nalguns casos, para além de acrescentar detalhe podemos também querer mudar a forma como o algoritmo armazena determinada informação. Por exemplo, no exemplo do relógio, para além de acrescentar os minutos poderíamos querer que as horas passassem a ser representadas no formato AM/PM. Nestes casos, ao verificar o refinamento temos que especificar como é que a informação no algoritmo mais abstrato pode ser obtida a partir da informação no algoritmo mais refinado. Esta transformação designa-se por refinement mapping e o TLA+ permite definir essa transformação usando a palavra reservada WITH após o INSTANCE. O exemplo do relógio com horas AM/PM e minutos poderia então ser especificado da seguinte forma.

----- MODULE HourMinuteClockAMPM -----

EXTENDS Naturals

VARIABLES h,m,am

Init == h \in 0..11 /\ am \in BOOLEAN /\ m \in 0..59

Next == 
    /\ IF m = 59 THEN /\ h' = (h + 1) % 12 
                      /\ IF h = 11 THEN am' = ~am ELSE am' = am
       ELSE h' = h /\ am' = am
    /\ m' = (m + 1) % 60

Spec == Init /\ [][Next]_<<h,am,m>> /\ WF_<<h,am,m>>(Next)

Mapping == INSTANCE HourClock WITH h <- IF am THEN h ELSE h+12

Refinement == Mapping!Spec

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

Note como na definição Mapping se especifica como é que o valor da variável h na especificação HourClock deve ser calculado à custa do valor das variáveis h e am na implementação HourMinuteClockAMPM.

Exercício: de facto nos relógios AM/PM o meio dia é representado como 12PM e a meia-noite como 12AM - altera a especificação acima para que o relógio se comporte desta forma e verifique que continua a ser um refinamento do HourClock.

Exercício: verifique que o seguinte algoritmo concorrente com N processos que incrementam uma variável partilhada, copiando antes o seu valor para uma variável local, mas onde o acesso à variável partilhada é controlado por um semáforo, é um refinamento do algoritmo de incremento concorrente sem variável local e sem semáforos.

   var x : integer = 0;
       sem : boolean = true;

   procedure increment(i : integer);
     var y : integer = 0;
   begin
0:   repeat until sem;
     sem := false;   
1:   y := x;
2:   x := x + y;
3:   sem := true
4: end;

   increment(1) || ... || increment(N)