A regra G-WAIT

A primeira versão da regra B-WAIT é muito restritiva pois obriga a que p=q e, tal como acontecia no caso das propriedades de invariância, as premissas quase nunca são fórmulas de estado válidas. A solução para ambos os problemas passa, mais uma vez, pela tentativa de fortalecer q com uma propriedade $\varphi$, tal que as premissas originadas por sejam fórmulas de estado válidas. Esta estratégia é sintetizada na regra G-WAIT apresentada na figura 5.3.

  

Figure 5.3: Versão simples da regra G-WAIT

Para demonstrar a aplicação desta regra vamos utilizar um exemplo ligeiramente mais complicado. Considere o algoritmo da figura que resolve o problema da exclusão mútua segundo Peterson.

  

Figure 5.4: Algoritmo de Peterson para exclusão mútua

local y1, y2 : bool where y1 = false, y2 = false
local      s : [1..2]

P1:: [
    l0: while (true) do [
        l1: noncritical;
        l2: (y1, s) := (true, 1);
        l3: await (!y2 \/ s = 2);
        l4: critical;
        l5: y1 := false
    ]
]

||

P2:: [
    m0: while (true) do [
        m1: noncritical;
        m2: (y2, s) := (true, 2);
        m3: await (!y1 \/ s = 1);
        m4: critical;
        m5: y2 := false 
    ]
]

Para além de permitir a exclusão mútua, este algoritmo garante que o primeiro processo a chegar à instrução await é o primeiro a entrar na região crítica. Esta propriedade pode ser expressa pela seguinte fórmula:

Como esta propriedade não pode ser provada com a regra B-WAIT. Assim, é necessário utilizar a regra G-WAIT e encontrar uma fórmula $\varphi$ mais forte que que verifique as premissas dessa regra. Essa fórmula deverá ser válida em todos os estados possíveis desde que se verifica até que se verifique l4. Dito de outra forma, a fórmula $\varphi$deve expressar uma propriedade que seja válida deste que P1 está à espera para entrar na região crítica até que lá entre.

Uma possível hipótese para $\varphi$ seria a própria . No entanto, com esta fórmula não conseguimos provar a premissa correspondente à transição de m3 para m4 (todas as outras premissas são triviais), expressa pela seguinte propriedade:

Não sendo possível usar é necessário arranjar uma hipótese mais forte. Se utilizarmos todas as premissas podem ser provadas e, consequentemente, a propriedade pode ser verificada.