Negotiations: Ein Modell für nebenläufige Systeme mit niedriger Komplexität

• Antragsteller: Professor Dr. Javier Esparza
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2015 bis 2019
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 273811150

In der Theorie nebenläufiger Systeme wird viel Energie auf dieUntersuchung von Kommunikationsprimitiven, wie gemeinsam genutzten(shared) Variablen, Punkt-zu-Punkt FIFO-Kanälen, Rendezvous oderzuverlässigen Broadcasts, verwandt. Dies gilt insbesondere für dieKomplexität von Verifikationsproblemen abstrakter Maschinen, die mit Hilfe dieser Primitive kommunizieren.Leider ist die Worst-Case-Komplexität, in der Größe der Systeme, sehrgroß und reicht von PSPACE-schwer bis zu unteren Schranken, die durchPotenztürme dargestellt werden. Selbst nicht-primitiv-rekursiveFunktionen sind möglich.Vor Kurzem begannen wir mit der Analyse eines neuenKommunikationsprimitives ``Verhandlung (Negotiation)''. Dieses ist eineKombination von Synchronisation und nichtdeterministischer Auswahl(der Name ergibt sich, da in einer Verhandlung mehrere Parteienzusammentreffen, d.h. synchronisieren, um sich aus einer Menge vonResultaten auf ein bestimmtes zu einigen, d.h. einenichtdeterministische Auswahl findet statt). Dazu führten wirVerhandlungsdiagramme (negotiation diagrams) ein, einNebenläufigkeitsmodell mit atomarer Verhandlung als Primitiv. DiesesModell ist dabei sehr ähnlich zu 1-sichere High-Level-Petrinetze.In unserer Arbeit haben wir eine Unterklasse dieses Modellsidentifiziert, die herausragende Eigenschaften aufweist:deterministische Verhandlungsdiagramme. Insbesondere können, obwohl dasModell vom Problem der Zustandsexplosion betroffen ist, fundamentaleEigenschaften wie Korrektheit (eine Eigenschaft die ungefähr derAbwesenheit von Deadlocks und Livelocks entspricht) in polynomiellerZeit überprüft werden. Wir haben des Weiteren auch eineProgrammiersprache konzipiert, die gerade diese deterministischenVerhandlungsdiagramme abbildet.Ausgehend von den deterministischen Verhandlungsdiagrammen beabsichtigenwir, weitere Modelle nebenläufiger Systeme mit steigender Mächtigkeit,aber in der Komplexität noch unterhalb der PSPACE-Grenze, zuanalysieren. Auch wenn diese Arbeit vorrangig theoretisch motiviert ist,so werden wir die Resultate nutzen um automatisch verteilteImplementierungen von Programmen zu erzeugen. Dazu werden wir eineProgrammiersprache für parallele Programme entwickeln, zusammen miteiner einfachen Hoare-Logik und dem entsprechenden Toolsupport

• DFG-Verfahren: Sachbeihilfen
• Kooperationspartner: Professor Dr. Jörg Desel