Softwarekonferenz für parallele
und hochperformante Programmierung
Heidelberg, Print Media Academy, 19.–22. Februar 2019

// Mit TLA+ zum korrekten Parallel-Programm

Parallele Programmierung ist ein zentraler Baustein, um immer leistungsfähigere Software zu entwickeln. Parallele Programmierung ist aber auch komplex und fehleranfällig. Das Finden von Concurrency Bugs gleicht einer Suche nach der Nadel im sprichwörtlichen Heuhaufen; ein Heuhaufen der mit jeder Ausführung des Programms durchgewirbelt wird.

Nachdem auf der Parallel18 mit Hilfe von TLA+ bereits ein sporadisch auftretendes Deadlock in einem BoundedBuffer analysiert und behoben wurde, werden in diesem Jahr – nach einer kurzen Einführung in die Grundlagen von TLA+ – die weiterführenden Konzepte von TLA+ vorgestellt. Insbesondere werden neben den Korrektheitsanforderungen, auch Lebendigkeitsanforderungen an den BoundedBuffer formuliert.

Dies erfordert die Einführung von Fairness-Garantien. Kurzum, im Rahmen eines exemplarischen Entwicklungsablaufs wird der typische Einsatz von TLA+ anhand eines einfachen Programms gezeigt. Es werden sowohl der Einstieg als auch die weiterführenden Möglichkeiten von TLA+ vermittelt.

Vorkenntnisse
Es wird kein Vorwissen vorausgesetzt. Kenntnis des Vortrags der Parallel18 erleichtert das Verständnis, ist aber ebenfalls keine Voraussetzung.

Lernziele
Ziel dieses Vortrags ist es, den Zuhörern die Möglichkeiten von formalen Methoden wie TLA+ zu zeigen um einen leichten Einstieg zu ermöglichen.
Der Fokus liegt dabei auf dem praktischen Einsatz von TLA+, der akademische Unterbau wird nur am Rande behandelt.


// Markus Kuppe Markus Kuppe

beschäftigt sich mit nebenläufiger und verteilter Programmierung, um diese handhabbarer zu machen. TLA+ ist dabei sowohl Mittel als auch Zweck. Markus ist bei Microsoft Research als Principal Engineer hauptverantwortlich für den TLA+ Model Checker zuständig.