Diplomarbeit: Ein Kalkül paralleler Prozesse, Bisimulationen und Korrektheit

Übersicht

In meiner Diplomarbeit wird der parallele Kalkül TCBS von K.V.S.Prasad behandelt. Es werden die Begriffe der Bisimulation und der Äquivalenz und darauf aufbauend der Begriff der Korrektheit eines Programms eingeführt. Es wird eine Möglichkeit angegeben, von der Geschwindigkeit eines Prozesses abzusehen und nur seine eigentliche Funktion in Betracht zu ziehen (Dies ist bei der gewöhnlichen schwachen Bisimulation nicht möglich). Darauf aufbauend wird dann das Alternating Bit Protokoll als korrekt, d.h. als dem One Place Buffer äquivalent (im Sinne einer neu eingeführten Äquivalenz) nachgewiesen.

Hier findet man die Diplomarbeit als PDF-Datei. Das Kapitel 1 mit der Einleitung folgt außerdem im HTML-Format. Desweiteren sind die Thesen und die Folien der Verteidigung als PDF-Dateien verfügbar.

Links

Die Originalarbeiten (in englisch) von K.V.S.Prasad:

Kapitel 1

Kurzüberblick

Eine gegenwärtig explosionsartig an Bedeutung und Verbreitung gewinnende Technologie ist die der weltweiten und lokalen Vernetzung von Rechnern. Bekanntestes Beispiel dafür ist sicherlich das Internet. Für herkömmliche sequentielle Algorithmen bilden klassische Modelle der theoretischen Informatik wie z.B. endliche Automaten und die Turingmaschine eine gut ausgebaute Basis für formale Schlußmethoden.

An der Kommunikation in Rechnernetzen sind aber mehrere Rechner beteiligt, die mit Hilfe eines Protokolls miteinander kommunizieren. Bekannte Beispiele für solche Protokolle sind das HTTP (Hypertext Transfer Protocol), das FTP (File Transfer Protocol) und das SMTP (Simple Mail Transfer Protocol), die alle auf die Internetprotokollfamilie TCP/UDP/IP (Transmission Control Protocol/User Datagram Protocol/Internet Protocol) aufsetzen.

Für diese spezielle Art von parallelen Algorithmen steckt die Erforschung der mathematischen Grundlagen trotz einiger Fortschritte in den letzten Jahren noch in den Anfängen. So ist z.B. nicht bewiesen, daß das Internet Protokoll in jeder Situation funktioniert, daß es korrekt ist.

Für die Modellierung paralleler Probleme hat sich die Verwendung paralleler Kalküle bewährt. Ein solcher paralleler Kalkül ist TCBS (Timed Calculus of Broadcasting Systems) von K.V.S. Prasad. Auf Grundlage dieses Kalküls beschreibe ich in dieser Arbeit einen Weg zum Nachweis der Korrektheit von Protokollen und zeige als Beispiel dazu, wie das Alternatig-Bit-Protokoll, ein einfaches Protokoll, als korrekt nachgewiesen wird.

Der Nutzen paralleler Kalküle

In den letzten Jahren hat die Erforschung des Verhaltens verteilter und paralleler Systeme weltweit an Bedeutung gewonnen. Mit der immer stärkeren Vernetzung der Computer und dem Vordringen von Mikroprozessoren in weitere Felder des alltäglichen Lebens erhält das Verständnis der Kommunikation zwischen verschiedenen Rechnern, aber auch zwischen verschiedenen Programmen auf demselben Rechner eine immer höhere Priorität. Es geht dabei um Fragen der Zuverlässigkeit von Systemen. Um diese zu beantworten, gibt es die Möglichkeit der überprüfung jedes einzelnen Systems mit wenig mehr als Erfahrung, gesundem Menschenverstand und einiger weniger Regeln für die Verhinderung von unerwünschten, immer wieder auftretenden Problemen wie z.B. dem Deadlock, dem gegenseitigen Blockieren von verschiedenen Prozessen.

Da die heute auftretenden parallelen und verteilten Systeme aber dazu tendieren, immer komplexer zu werden, gewinnt der formale beweistechnische Ansatz für die Verifikation von Programmen an Bedeutung. Dazu ist natürlich eine Abstraktion der Realität erforderlich. Diese besteht in der Definition eines Kalküls, welcher nur noch ganz wenige, für die Parallelität aber entscheidende Konstrukte aufweist und damit alles andere den bereits bekannten Techniken für die Verifikation von sequentiellen Programmen überläßt. Diese formalen parallelen Kalküle beschränken sich fast ausschließlich auf die Modellierung der Kommunikation zwischen Prozessen. Berechnungen werden in Black-Boxes vorgenommen. Diese sind einfach Funktionen, die als korrekt vorausgesetzt werden.

Andere parallele Modelle sind z.B. Zellularautomaten (wie "Conway's Game Of Life") und die P-RAM (Parallel Random Access Machine) . Erstere jedoch sind im allgemeinen in ihrer Struktur zu starr und deswegen für parallele Probleme weniger geeignet. Bei der P-RAM hingegen erfolgt die Kommunikation implizit über den Speicher. Damit aber lassen sich viele Aussagen der parallelen Kalküle, die ja die Kommunikation zwischen den Prozessen untersuchen, nicht erhalten.

Der Einsatz von parallelen Kalkülen ist auch nicht, wie man leicht denken könnte, einfach nur eine Verschnörkelung der sequentiellen Programmiertechnik, da viele Probleme der Realität wirklich ein paralleles Modell erfordern, um vernünftig beschrieben zu werden. Man denke zum Beispiel an die Telekommunikation, wo verschiedene Ortsvermittlungen zusammenarbeiten müssen, um eine Verbindung herzustellen. Diese arbeiten dabei natürlich echt gleichzeitig und sind außerdem auf die gegenseitige Kommunikation angewiesen.

Parallele Kalküle

Im Jahre 1978 veröffentliche C.A.R. Hoare den Artikel "Communicating Sequential Processes", der einen der ersten parallelen Kalküle vorstellte, und zwar CSP (Communicating Sequential Processes), welcher seitdem häufig verwendet wird. Es basiert auf verschiedenen Kanälen, auf denen Handshaking-übertragung stattfindet, d.h. ein Absender wird seine Botschaft erst los, wenn der Empfänger sie ihm abnimmt, wenn sie sich "die Hand geben". Dasselbe Prinzip verfolgt auch die von Robin Milner in seinem 1980 erschienenen Artikel "A Calculus of Communicating Systems" vorgestellte Sprache CCS (Calculus of Communicating Systems).

Auf beiden Sprachen existiert eine interessante Algebra, und die Tatsache, daß beide Autoren mehr oder minder unabhängig auf ähnliche Sprachen gekommen sind, legt nahe, daß die benutzten Kommunikationskonstrukte grundlegender Natur sind. Bis dahin wurden vorwiegend höher liegende Modelle wie Semaphore, Monitor usw. genutzt, die in der neuen Theorie problemlos modelliert werden konnten. Ein Problem allerdings gibt es bei den Handshaking-Sprachen: Eine Priorisierung ist nur sehr schwer modellierbar. Das liegt vereinfacht gesprochen daran, daß ein Prozeß mit hoher Priorität, der eine Botschaft an einen anderen Prozeß mit niedriger Priorität hat, erst dann fortsetzten kann, wenn ihm seine Botschaft abgenommen wurde, d.h. der "langsame" Prozeß bremst den "schnellen" aus.

Der parallele Kalkül TCBS und seine Bedeutung

Die von K.V.S. Prasad von 1991 an entwickelte Sprache CBS (Calculus of Broadcasting Systems) und deren Erweiterung TCBS (Timed CBS) hat dieses Problem nicht, da sie auf Broadcasting basiert, d.h. die Botschaft eines Prozesses ist im Prinzip für alle anderen hörbar, und der sendende Prozeß kann sofort seine Arbeit fortsetzen. Außerdem ist Broadcast eigentlich das natürlichere Mittel der Kommunikation, auch und vor allem in der praktischen Anwendung, also z.B. in einem Local Area Network, aber auch bei der mobilen Telefonie. Punkt-zu-Punkt-Verbindungen, wie sie von CCS und CSP benutzt werden, sind meist nur auf der Grundlage von Broadcast-Medien implementiert. Insgesamt hat TCBS einige schwerwiegende Vorteile, die eine Beschäftigung mit diesem Kalkül sinnvoll erscheinen lassen.

So wird dieser Kalkül an der Universität Göteborg, wo K.V.S. Prasad Dozent ist, nicht nur in der Forschung von der renommierten Concurrency Group behandelt, sondern auch in der Ausbildung verwendet. Während meines Studiums in Göteborg im Studienjahr 1994/95 belegte ich den Kurs "Rechnernetze und Rechnerkommunikation", der auf Grundlage des Buches "Principles of Protocol Design" von Robin Sharp detailliert Netzprotokolle der Rechnerkommunikation behandelte. Zum erfolgreichen Bestehen des Kurses war eine Reihe von Protokollen in einer simulierten Umgebung in TCBS zu implementieren. Die Sprache TCBS war auf Grundlage der funktionalen Programmiersprache Haskell implementiert. Es gibt aber auch andere Implementationen, z.B. eine physisch verteilte, aber auch eine von mir programmierte Implementation auf Grundlage von C++.

Motivation und Aufbau der Arbeit

Durch theoretische Überlegungen, aber auch die praktische Arbeit mit diesem Kalkül angeregt, begann mein Interesse für dieses Gebiet der theoretischen Informatik. In meiner Praktikumsarbeit für den oben genannten Kurs entwarf und programmierte ich ein fiktives Netz von Wetterstationen, die über unsichere Medien verbunden waren und miteinander kommunizieren mußten. Ich war aber nicht in der Lage zu beweisen, daß die von mir verwendeten Protokolle bzw. deren Implementationen korrekt waren.

Ein großer Teil der heutzutage verwendeten Netzprotokolle ist ebenfalls nicht als korrekt nachgewiesen. Man hofft, daß sie funktionieren, und in praxi arbeiten sie zuverlässig. Aber bei vernetzten Rechnern, die ja ein verteiltes System darstellen, kann man nicht überblicken, welche Konstellationen auftauchen können, und wie sich das System in diesen verhält.

Aus diesem Grunde wählte ich das Thema dieser Arbeit. Sie ist ein kleiner Schritt hin zum automatischen Nachweis der Korrektheit von Protokollen, z.B. der Internet-Protokoll-Familie (TCP/UDP/IP), bietet aber auch Ansatzpunkte für andere parallele Algorithmenklassen.

Die vorliegende Arbeit benutzt also TCBS, um Beweistechniken für den Nachweis der Korrektheit von Protokollen vorzustellen. Dabei wird in Kapitel 2 eine anschauliche Darstellung des Kalküls TCBS anhand von Beispielen gegeben. Dieser Kalkül wird dann in Kapitel 3 formal eingeführt. Dazu verwende ich im Gegenteil zur Originalarbeit eine formale Definition mit Hilfe von Grammatiken. Diese etwas kompliziertere Vorgehensweise sichert faktisch erst die Beweisbarkeit von Sätzen über dieser Sprache. In Kapitel 4 gehe ich auf die vorhandenen Bisimulationsbegriffe ein. Diese definieren äquivalenzrelationen auf TCBS, welche eine erste Form der Entsprechung zweier Prozesse bieten. In diesen zwei Kapiteln werden verschiedene in den Originalarbeiten lediglich intuitiv begründete Sätze bewiesen und einige neue formuliert (insbesondere Satz 3.4 zur Aktionsbereitschaft).

In Kapitel 5 wird die Bedeutung von Bisimulationen für den Beweis der Korrektheit speziell für eine Klasse von Protokollen dargestellt. Ich beschreibe, wann ein Protokoll als korrekt zu gelten hat und stelle die dabei mit den herkömmlichen Bisimulationen auftretenden Probleme dar. Ausgehend davon führe ich in Kapitel 6 einen diese Probleme lösenden erweiterten Kalkül ein. Damit kann ich dann in Kapitel 7 die in Kapitel 5 gegebene Beschreibung, wann ein Protokoll korrekt heißt, in eine vollständige Definition umwandeln. In Kapitel 7 wird außerdem als Beispiel dafür das Alternating-Bit-Protokoll kurz erläutert und dessen Implementation angegeben. Ein Weg zum Beweis der Korrektheit dieser Implementation wird vorgestellt und wichtige Teile bewiesen.

Insgesamt stellt diese Arbeit neben der formalen Einführung von TCBS auf Grundlage der theoretischen Informatik einen erweiterten Kalkül TCBS' vor, der zusammen mit der herkömmlichen schwachen Bisimulation die Abstraktion von der Zeit zuläßt und damit für die Behandlung von Protokollen als günstig erscheint.