Terminierung und Deadlocks Enkhbat Daginaa Betreuerin Prof. Heike Wehrheim Totale Korrektheit.
An Axiomatic Proof Technique for Parallel Programs (S. Owicki und D. Gries) Hendrik Pfeiffer...
-
Upload
rosamund-appenzeller -
Category
Documents
-
view
104 -
download
1
Transcript of An Axiomatic Proof Technique for Parallel Programs (S. Owicki und D. Gries) Hendrik Pfeiffer...
An Axiomatic Proof Technique for Parallel Programs
(S. Owicki und D. Gries)
Hendrik Pfeiffer
Betreuerin: Prof. Dr. Heike Wehrheim
Proseminar Assertions
Themeninhalt
Beweisidee von Hoare auf parallele Programme erweitern Verständnis der Parallelität Befehle für Parallelität
Seite 2 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Themenabgrenzung
Partielle Korrektheit
Terminierung
Totale Korrektheit
nach der Ausführung gilt eine bestimmte Eigenschaft
das Programm hält bei korrekter Eingabe
Seite 3 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Motivation
• Komplexität der Programme
• Einsatz in kritischen Bereichen
• Verifikation bei parallelen Programmen schwierig informeller Beweis reicht nicht aus
Seite 4 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
• Hoare-Triple:(Standard-Beweisskizze)
• Ableitungsregel:
Notationen nach Hoare
{P} Anweisung {Q}
Annahmen (bekannt) Folgerung
Seite 5 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
AtomaritätVerständnis der ParallelitätBefehle für parallele Abschnitte BeweisideeInterferenz-Freiheit
Parallelität
Seite 6 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Eine Aktion A heißt atomar, wenn die in A vorkommenden Variablen während der Ausführung nur von A verändert werden.
Atomarität
Seite 7 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Atomarität
Beispiel: x := 1;y := 2;S = [x := y || y := x ];
Seite 8 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Atomarität
Beispiel: x := 1;y := 2;S = [x := y || y := x ];
Zuweisungennicht atomar
Zuweisungenatomar
1. x = y = 12. x = y = 23. x = 2 und y = 1
1. x = y = 12. x = y = 2
Seite 8 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
atomar bei Owicki und Gries:
Atomarität
Auswertungen von Ausdrücken
Wertzuweisungen
Atomare Bereiche
Seite 9 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Owicki/Gries:InterleavingVerzahnung statt ParallelitätSehr ähnlich zum sequentiellen Ablauf
Verständnis der Parallelität
Zeit
S1 S3S2
T1 T2 T3
Seite 10 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Verständnis der Parallelität
Zeit
S1 S3S2T1 T2 T3
Owicki/Gries:InterleavingVerzahnung statt ParallelitätSehr ähnlich zum sequentiellen Ablauf
Seite 10 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Interleaving Parallelität
Interleaving:einzelne Anweisungen können sich nicht
beeinflussenBeweisverfahren vereinfacht
Seite 11 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
parallele Ausführung:
Befehle für Parallelität
Synchronisation und Atomarität:
cobegin S1//S2//…//Sn coend
await B then S
Seite 12 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Ziel:
Cobegin-Anweisung
Seite 13 von 22
S1 Sn…{P1} {Q1} {P…} {Q…} {Pn} {Qn}
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Ziel:
folgt
Cobegin-Anweisung
Seite 13 von 22
S1 Sn…{P1} {Q1} {P…} {Q…} {Pn} {Qn}
{P1 Λ P… Λ Pn}
S1
…
Sn
{Q1 Λ Q… Λ Qn}
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Cobegin-Anweisung: Beispiel 1
Seite 14 von 22
x:=2;{x=1} {x=2}
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Beispiel: x := 1;y := 2;S = [x := 2 || y := 1 ];
{y=1}y:=1;{y=2}
Cobegin-Anweisung: Beispiel 1
Seite 14 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Beispiel: x := 1;y := 2;S = [x := 2 || y := 1 ];
x:=1;
y:=2;{x=1 Λ y=2}
{x=1} x:=2; {x=2} {y=2} y:=1; {y=1}
{x=2 Λ y=1}
Cobegin-Anweisung: Beispiel 2
Seite 15 von 22
x:=y;{x=1 Λ y=2}
{x=1 Λ y=2}
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Beispiel: x := 1;y := 2;S = [x := y || y := x ];
{x=1 Λ y=1}y:=x;
{x=2 Λ y=2}
Cobegin-Anweisung: Beispiel 2
Seite 15 von 22
x:=y;{x=1 Λ y=2}
{x=1 Λ y=2}
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Beispiel: x := 1;y := 2;S = [x := y || y := x ];
{x=1 Λ y=1}y:=x;
x:=y;
y:=x;
{(x=1 Λ y=2) Λ
(x=2 Λ y=2)}
{(x=2 Λ y=2) Λ
(x=1 Λ y=1)}
{x=2 Λ y=2}
Ziel:
Cobegin-Anweisung
Seite 16 von 22
{P1} S1 {Q1},…, {Pn} Sn {Qn}
{P1 Λ…Λ Pn} cobegin S1||…||Sn coend {Q1 Λ…Λ Qn}
kein Unterschied zwischen sequentieller und paralleler Ausführung
funktioniert bei Verzicht auf gemeinsame Variablen
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Beweisidee für parallele Programme:
1. Korrektheit für Teilprogramme beweisen2. Zeigen, dass sich Beweise der
Teilprogramme gegenseitig nicht beeinflussen
Interferenz-Freiheit beweisen
Beweisidee
Seite 17 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Interferenz-Freiheit: einzelne Anweisungen
Seite 18 von 22
Anweisung T interferiert nicht mit Beweis{P} S {Q}, falls gilt:
{Q Λ pre(T)} T {Q}
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Interferenz-Freiheit: einzelne Anweisungen
Seite 18 von 22
Anweisung T interferiert nicht mit Beweis{P} S {Q}, falls gilt:
{Q Λ pre(T)} T {Q}
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
{x=1}
x:=2;
{x=2}
S: {y=2}
y:=1;
T:
{y=1}
Interferenz-Freiheit: einzelne Anweisungen
Seite 18 von 22
Anweisung T interferiert nicht mit Beweis{P} S {Q}, falls gilt:
{Q Λ pre(T)} T {Q}
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
{x=1}
x:=2;
{x=2}
S: {y=2}
y:=1;
T:
{y=1}
{x=2 Λ y=2}
{x=2}
Interferenz-Freiheit: Standard-Beweisskizzen
Seite 19 von 22
Die Standardbeweisskizzen {P} S {Q}und {U} T {V} sind interferenzfrei,falls gilt:
Es existiert keine Anweisung Ti in T,
die mit einer Beweisskizze {Pj} Sj {Qj}in S interferiert
und andersherum
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
Interferenz-Freiheit: Standard-Beweisskizzen
Seite 20 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
{P1}
S1
{Q1}
{P2}
S2
{Q2}
{U1}
T1
{V1}
{U2}
T2
{V2}
T
{U}
{V}
S
{P}
{Q}
Interferenz-Freiheit: Standard-Beweisskizzen
Seite 20 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
{P1}
S1
{Q1}
{P2}
S2
{Q2}
{U1}
T1
{V1}
{U2}
T2
{V2}
T
{U}
{V}
S
{P}
{Q}
Interferenz-Freiheit: Standard-Beweisskizzen
Seite 20 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
{P1}
S1
{Q1}
{P2}
S2
{Q2}
{U1}
T1
{V1}
{U2}
T2
{V2}
T
{U}
{V}
S
{P}
{Q}
Interferenz-Freiheit: Standard-Beweisskizzen
Seite 20 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
{P1}
S1
{Q1}
{P2}
S2
{Q2}
{U1}
T1
{V1}
{U2}
T2
{V2}
T
{U}
{V}
S
{P}
{Q}
Interferenz-Freiheit: Standard-Beweisskizzen
Seite 20 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
{P1}
S1
{Q1}
{P2}
S2
{Q2}
{U1}
T1
{V1}
{U2}
T2
{V2}
T
{U}
{V}
S
{P}
{Q}
Interferenz-Freiheit: Standard-Beweisskizzen
Seite 20 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
{P1}
S1
{Q1}
{P2}
S2
{Q2}
{U1}
T1
{V1}
{U2}
T2
{V2}
T
{U}
{V}
S
{P}
{Q}
Interferenz-Freiheit: Standard-Beweisskizzen
Seite 20 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
{P1}
S1
{Q1}
{P2}
S2
{Q2}
{U1}
T1
{V1}
{U2}
T2
{V2}
T
{U}
{V}
S
{P}
{Q}
Interferenz-Freiheit: Standard-Beweisskizzen
Seite 20 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
{P1}
S1
{Q1}
{P2}
S2
{Q2}
{U1}
T1
{V1}
{U2}
T2
{V2}
T
{U}
{V}
S
{P}
{Q}
Interferenz-Freiheit: Standard-Beweisskizzen
Seite 20 von 22
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
{P1}
S1
{Q1}
{P2}
S2
{Q2}
{U1}
T1
{V1}
{U2}
T2
{V2}
T
{U}
{V}
S
{P}
{Q}
Beweisidee formal
Seite 21 von 22
{P1} S1 {Q1},…, {Pn} Sn {Qn} sind interferenzfrei
{P1 Λ…Λ Pn} cobegin S1||…||Sn coend {Q1 Λ…Λ Qn}
{P1} S1 {Q1}
,…, {Pn} Sn {Qn}
Korrektheitsbeweis (sequentiell)1.
2.
ProblemstellungSequentiell (Hoare)
Parallel (Owicki/Gries)
• Beweismethode für parallele Programme mit gemeinsamen Variablen
• Methode beruht auf Hoare´s Beweisschema für sequentielle Programme
• In den 70er Jahren entwickelt
• Problem: sehr aufwendig (exponentiell)
Zusammenfassung
Vielen Dank für Eure Aufmerksamkeit