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