Exercícios

1.

Considere o algoritmo de Peterson para resolver o problema da exclusão mútua apresentado na figura 5.4.

(a)

Qual o significado da seguinte propriedade sobre este algoritmo:

(b)

Prove esta propriedade utilizando o STeP.

2.

Considere o algoritmo da figura 5.7, proposto por Dekker, para resolver o problema da exclusão mútua.

(a)

Utilizando o STeP, prove a seguinte propriedade deste algoritmo:

  

Figure 5.7: Algoritmo de Dekker para exclusão mútua

local y1, y2 :bool where y1 = false, y2 = false
local t :int where t = 1

P1:: [
    l0: loop forever do [
        l1: noncritical;
        l2: y1 := true;
        l3: while (y2) do
            l4: if (t = 2) then [
                l5: y1 := false;
                l6: await (t = 1);
                l7: y1 := true
            ];
        l8: critical;
        l9: t := 2;
        l10: y1 := false
    ]
]

||

P2:: [
    m0: loop forever do [
        m1: noncritical;
        m2: y2 := true;
        m3: while (y1) do
            m4: if (t = 1) then [
                m5: y2 := false;
                m6: await (t = 2);
                m7: y2 := true
            ];
        m8: critical;
        m9: t := 1;
        m10: y2 := false
    ]
]