Modellierung eines verteilten Algorithmus

14.10.2004

Modellierung einesverteilten Algorithmus

Luhme X

Niels Lohmann

[email protected]://www.informatik.hu-berlin.de/~nlohmann/arbeit

Luhme X

2

Übersicht

1. Mutex-Algorithmus

2. Modellierung als Petrinetz

3. Überführung in TLA+-Formel

4. Neue Modellierung in TLA+

5. Model Checking

Luhme X

3

Mutex-Algorithmus

§ „global mutual exclusion in networks“§ als Baum organisiertes Netzwerk§ globaler wechselseitiger Ausschluss§ Token als Semaphor§ Tokenlines

Szenario

c a

b

T

T

Die Tokenlines bilden stets einen gerichteten Baum mit dem Token-Besitzer als Wurzel.

Mutex-Algorithmus

Modellierung als Petrinetz

Überführung inTLA+-Formel

Neue Modellierungin TLA+

Model Checking

Luhme X

4

Mutex-Algorithmus

c a

bbesitze Token

T

Ablauf

Mutex-Algorithmus




Model Checking

Luhme X

5

Mutex-Algorithmus

c a

b

Request!

besitze Token

T

Ablauf

Mutex-Algorithmus




Model Checking

Luhme X

6

Mutex-Algorithmus

c a

b

Request!

besitze Token

leite Requestweiter

T

Ablauf

Mutex-Algorithmus




Model Checking

Luhme X

7

Mutex-Algorithmus

c a

bT

besitze Token

gebe Tokenan b

Request!

Ablauf

Mutex-Algorithmus




Model Checking

Luhme X

8

Mutex-Algorithmus

c a

b

cT

Request!

besitze Token

gebe Tokenan c

Ablauf

Mutex-Algorithmus




Model Checking

Luhme X

9

Mutex-Algorithmus

a

b

Ablauf

cc

kritischMutex-Algorithmus




Model Checking

Luhme X

10

Mutex-Algorithmus

a

b

Ablauf

cT

Mutex-Algorithmus




Model Checking

besitzeToken

Luhme X

11


Menge aller Sites Token-Lines erster Token-Besitzer

Mutex-Algorithmus




Model Checking

Netz Σ

Anfangsmarkierung:

Luhme X

12


x fragt für sich selbst nach

z fragt für x nach

z ist näher am Token-Besitzer als x

Netz Σ

Mutex-Algorithmus




Model Checking

Luhme X

13


In Elements of Distributed Algorithmswurde die Eigenschaft

bewiesen.

„Jeder, der kritisch werden möchte, wird auch irgendwann kritisch.“

Korrektheit

Mutex-Algorithmus




Model Checking

Luhme X

14

Überführung in TLA+-Formel

TLA+ ist eine Kombination aus§ der temporalen Logik TLA

§ der klassischen Mengenlehre

→ TLA+ ist eine Spezifikationssprache für verteilte Systeme.

Was ist TLA+?

Mutex-Algorithmus




Model Checking

Luhme X

15


§ Abläufe

§ TLA-Formeln

TLA – The Temporal Logic of Actions

Zustandsprädikat

TLA-Aktionen

neuer Wert für x

Mutex-Algorithmus




Model Checking

Zustand

Luhme X

16


§ Stottern

§ Spezifikation

TLA – The Temporal Logic of Actions

Initialisierungs-bedingung

Fairness-annahmen

Tupel allerVariablen

Mutex-Algorithmus




Model Checking

Luhme X

17


§ in TLA+ dürfen Variablen Mengen sein§ Fairness und Progress von Aktionen

kann ausgedrückt werden

→ Idee: „kanonische“ Überführung des Petrinetzes in eine TLA+-Formel:

§ Plätze → Mengen§ Transitionen → Aktionen

Idee

Mutex-Algorithmus




Model Checking

Luhme X

18


Mutex-Algorithmus




Model Checking

Variablen

Luhme X

19

Überführung in TLA+-FormelAktionen

Mutex-Algorithmus




Model Checking

Luhme X

20

Überführung in TLA+-FormelAktionen

Mutex-Algorithmus




Model Checking

Luhme X

21

Überführung in TLA+-FormelSpezifikation

Mutex-Algorithmus




Model Checking

Luhme X

22

Neue Modellierung in TLA+

§ in der Petrinetz-Modellierung unrealistisch/zu abstrakt:

§ pending als öffentlicher Nachrichtenplatz§ compass als globale Netzinfrastruktur§ Entnahme von compass-Kanten

§ besser/realistischer:§ agentenbasierte Sicht§ Mailboxen§ lokale Nachrichtenkanäle

Mutex-Algorithmus




Model Checking

Ansatz

Luhme X

23


§ jede Site/Agent besitzt…§ eine Mailbox für Anfragen§ Nachrichtenkanäle zu seinen Nachbarn§ eine „Vater-Site“ oder das Token§ einen Zustand (idle, requesting, critical)

§ … und sieht§ seine Nachbarn§ sonst nichts

Szenario

cb

T

Mutex-Algorithmus




Model Checking

Luhme X

24

c a

b


Tb

a

Ablauf

baa

father

;idlec;idleb;idlea

mailboxstate

Mutex-Algorithmus




Model Checking

hier per Definition deterministisch

Luhme X

25

c a

b


Tb

a

Ablauf

baa

father

requestcidlebidlea

mailboxstate

Mutex-Algorithmus




Model Checking

;

;

;

Luhme X

26

c a

b


c

Tb

a

Ablauf

baa

father

requestc{c}idleb

idleamailboxstate

Mutex-Algorithmus




Model Checking

;

;

Luhme X

27

c a

b


b

c

Tb

a

Ablauf

baa

father

requestc{c}idleb{b}idlea

mailboxstate

Mutex-Algorithmus




Model Checking

;

Luhme X

28

c a

b


c

T

b b

Ablauf

bbb

father

requestc{c}idleb

idleamailboxstate

Mutex-Algorithmus




Model Checking

;

;

Luhme X

29

c a

b


Tb

c

Ablauf

ccb

father

requestcidlebidlea

mailboxstate

Mutex-Algorithmus




Model Checking

;

;

;

Luhme X

30

c a

b


Tb

c

Ablauf

ccb

father

criticalcidlebidlea

mailboxstate

Mutex-Algorithmus




Model Checking

;

;

;

Luhme X

31

c a

b


Tb

c

Ablauf

ccb

father

idlecidlebidlea

mailboxstate

Mutex-Algorithmus




Model Checking

;

;

;

Luhme X

32


Spezifikation

Mutex-Algorithmus




Model Checking

nur den Agentenbetreffend

die Umweltbetreffend

Luhme X

33

Model Checking

die erwartete Zustandsraumexplosion:

§ Petrinetz-Modellierung (n Sites):§

§ Agentenversion (n Agenten):§

→ zu viel für einen Model Checker?

Zustandsraum

Mutex-Algorithmus




Model Checking

Luhme X

34

Model Checking

§ TLC akzeptiert eine Teilklasse von TLA+ (hier keine Einschränkung)

§ explizites Model Checking fürendliche Systeme

§ kaum Reduktionstechniken (nur Symmetrie – hier nicht anwendbar)

§ sehr große Schwächen, Lebendigkeit zu beweisen

Model Checker TLC

Mutex-Algorithmus




Model Checking

Luhme X

35

Model Checking

§ in keiner der Modellierung (Petrinetz, Agenten) Ergebnisse für mehr als zwei Sites

§ Lebendigkeitsformeln wie z. B.

ließen sich nicht mit TLC beweisen

§ bewiesen: Mutex, Typinvarianten§ die Ergebnisse von TLC sind teilweise

recht eigenartig

Ergebnisse

Mutex-Algorithmus




Model Checking

Luhme X

36

Model Checking

Speicherüberlauf bei drei Sites: 4 GB RAM in 30 Minuten…Mutex-Algorithmus




Model Checking

Ergebnisse

Erfolgreiche Verifikation (bei vier Sites) jeder Lebendigkeitsformel der Form

14.10.2004

Modellierung einesverteilten Algorithmus

Luhme-Workshop 2004

Vielen Dank!

Niels Lohmann

[email protected]://www.informatik.hu-berlin.de/~nlohmann/arbeit

Modellierung eines verteilten Algorithmus

Education

Transcript of Modellierung eines verteilten Algorithmus