Terminierung und Deadlocks

Enkhbat Daginaa

Betreuerin Prof. Heike Wehrheim

Totale Korrektheit

1/21

Übersicht

Einleitung await – Statement Totale Korrektheit Deadlocks Terminierung

2/21

Einleitung

● Warum ist Programmverifikation so wichtig?

2/21

Einleitung

● Warum ist Programmverifikation so wichtig?

– Zuverlässigkeit der Software

– Erstellung der Dokumentation einfacher

– Kompatibilität besser überprüfbar

3/21

Einleitung

1969 Hoare axiomatische Methode für sequentielle Programme

1976 Owicki und Gries erweiterten Hoare‘s Methode für parallele Programme

3/21

Einleitung

1969 Hoare axiomatische Methode für sequentielle Programme

1976 Owicki und Gries erweiterten Hoare‘s Methode für parallele Programme

-Nicht nur partielle Korrektheit-Sondern auch die anderen Eigenschaften (z.B. Deadlockfreiheit, gegenseitiger Ausschluss)

4/21

await - Statement

Formal: await B then S end await wird für die Synchronisation von Prozessen

verwendet.

B true => S atomar (unteilbar) ausgeführt werden

B false => S blockiert und andere Komponenten können ausgeführt werden.

5/21

Totale Korrektheit

{p} S {q} heißt partiell korrekt, wenn jede

terminierende Berechnung von S, die in einem p- Zustand startet, in einem q-Zustand terminiert.

{p} S {q} heißt total korrekt, wenn jede

Berechnung von S, die in einem p-Zustand

startet, terminiert und ihren Endzustand q erfüllt.

6/21

Totale Korrektheit

Um totale Korrektheit von Parallelen Programmen zu zeigen, müssen wir

1. Deadlockfreiheit

2. Divergenzfreiheit

beweisen.

7/21

Beispiel

Beispielprogramm für Deadlock:

x := 1;

y := 2;

await (x=2) then y := 1;

//

await (y=1) then x := 2;

8/21

Deadlock:

Def: Ein Programm S mit Beweisskizze {p} S {q} ist deadlockfrei, falls es keinen Zustand x gibt (der p erfüllt), von dem aus S in einen Deadlock geraten kann.

8/21

Deadlock

Def: Ein Programm S mit Beweisskizze {p} S {q} ist deadlockfrei, falls es keinen Zustand x gibt (der p erfüllt), von dem aus S in einen Deadlock geraten kann.

d.h. Es liegt ein noch nicht terminiertes Programm/Teilprogramm vor, das keinen Schritt weiter ausführen kann.

9/21

Deadlock

Methode von Owicki und Gries:

1. Zähle alle potentiellen Deadlocks auf.

2. Zeige, dass keiner dieser potentiellen Deadlocks eintreten kann.

9/21

Deadlock

Methode von Owicki und Gries:

1. Zähle alle potentiellen Deadlocks auf.

2. Zeige, dass keiner dieser potentiellen Deadlocks eintreten kann.

Wenn keiner der potentiellen Deadlocks eintreten kann, tritt somit kein echter Deadlock ein => Das Programm ist Deadlock-Frei

10/21

Deadlock

Def: Sei ein paralleles Programm

(i) heißt potenzieller Deadlock von S, falls die folgenden zwei Bedingungen erfüllt sind:

- Für jedes i ist entweder eine await- Anweisung in oder die leere Anweisung E, für die Terminierung von steht.

- Es gibt ein i, so dass eine await-Anweisung in ist.

]S//...//S[ n1

)R...R( n1

iR iSiS

iSiR

11/21

Deadlock

(ii) Gegeben seien interferenz-freie Standard Beweisskizzen i € {1,…,n} , für schwache totale Korrektheit. Zu jedem potentiellen

Deadlock gibt es ein Tupel von Zusicherungen:

• falls await B then S end,• falls

)r,...,r( n1

iR,B)R(prer ii ,qr ii .ER i

},q{S}p{ i*ii

11/21

Deadlock

(ii) Gegeben seien interferenz-freie Standard Beweisskizzen i € {1,…,n} , für schwache totale Korrektheit. Zu jedem potentiellen

Deadlock gibt es ein Tupel von Zusicherungen:

• falls await B then S end,• falls

)r,...,r( n1

iR,B)R(prer ii ,qr ii .ER i

},q{S}p{ i*ii

Keine potentiellen Deadlocks können eintreten. in1i r

12/21

Deadlock

Parallelismus mit Deadlock-Freiheit:

(1) Die Standard-Beweisskizzen

für schwache totale Korrektheit sind interferenzfrei.

(2) Für jeden potentiellen Deadlock von erfüllt das zugehörige Tupel von Zusicherungen die Formel.ri

n1i

},n,...,1{i},q{S}p{ i*ii

)R...R( n1 ]S//...//S[ n1

}q]{S//...//S}[p{ in1in1i

n1i

13/21

Beispiel:

{x=0}

await x = 1 then skip end

//

x:=1

{x=1}

13/21

Beispiel:

{x=0} await x = 1 then skip end // x:=1 {x=1} {x=0 x=1} await x=1 then skip end {x=1} und {x=0} x:=1 {x=1}.

13/21

Beispiel:

{x=0} await x = 1 then skip end // x:=1 {x=1} {x=0 x=1} await x=1 then skip end {x=1} und {x=0} x:=1 {x=1}.

Potentielle Deadlock:(await x=1 then skip end, E).

13/21

Beispiel:

{x=0} await x = 1 then skip end // x:=1{x=1} {x=0 x=1} await x=1 then skip end {x=1} und {x=0} x:=1 {x=1}.

Potentielle Deadlock:(await x=1 then skip end, E).

Als Zusicherung:((x=0 x=1) x 1, x=1)

14/21

Divergenz

Eine Berechnung von S divergiert, falls sie unendlich ist. S kann von x aus divergieren, falls es eine unendliche Berechnung von S gibt, die in x startet.

15/21

Terminierung

Um die Terminierung für totale Korrektheit zu zeigen, reicht while - Schleife von partielle Korrektheit nicht aus.

  Hierbei gilt die Nachbedingung allerdings nur,

wenn die Schleife verlassen wird, wenn sie also terminiert.

}Bp{S)B(while}p{

}p{S}Bp{

Bp

16/21

Terminierung

while-Schleife:

}Bp{S)B(while}p{

}zt{S;tz}Bp{,0tBp},p{S}Bp{

16/21

Terminierung

while-Schleife:

}Bp{S)B(while}p{

}zt{S;tz}Bp{,0tBp},p{S}Bp{

-Diese Schleifenregel ist korrekt für sequentielle Programme.

-Aber Parallele Programme können gegenseitig beeinflussen.

17/21

Terminierung

Zur zeigen:

t nimmt auf jedem möglichen Pfad durch den Schleifenrumpf S abnimmt.

17/21

Terminierung

Zur zeigen:

t nimmt auf jedem möglichen Pfad durch den Schleifenrumpf S abnimmt.

Unter einem Pfad versteht man eine möglicherweise leere Folge von normalen Wertzuweisung und atomaren Bereichen.

18/23

Terminierung

Neue Schleifenregel:

1) ist eine Standart-Beweisskizze,

2) für jede normale Wertzuweisung und jeden atomaren Bereich T in S,

3) für jeden Pfad gibt es eine normale Wertzuweisung oder einen atomaren Bereich T in mit

4)

}p{S}Bp{ *

)S(path

}zt{T}zt)T(pre{ 0tp

}Bp{S}Bp{whileBdo}p{ *

}zt{T}zt)T(pre{

19/21

Terminierung

Zusätzlich müssen wir Interferenzfreiheit für totale Korrektheit zeigen:

Interferenzfreiheit für partielle Korrektheit + t nimmt nicht zu.

}zt{T}zt)T(pre{

20/21

Beispiel

S1:

while (x>0) do

y := 0;

if (y=0)

x := x-1;

else

y := 0

od

S2:

while (x>0) do

y := 1;

if (y=1)

x := x-1;

else

y := 1

od

]S//S[S 21

21/21

Zusammenfassung

totale Korrektheit = partielle Korrektheit + garantierte Terminierung.

Deadlockfreiheit und Divergenzfreiheit Aber es gibt auch Programme, die nicht

unbedingt terminiert werden müssen.