Softwarekonferenz für parallele, nebenläufige
und asynchrone Programmierung und HPC
Heidelberg, Print Media Academy, 6.-8. März 2018

// Mit TLA+ zum korrekten Parallelprogramm

Parallele Programmierung ist ein zentraler Baustein, um immer leistungsfähigere Software zu entwickeln. Diese Leistungsfähigkeit geht allerdings mit gesteigerter Komplexität einher, wodurch etablierte Werkzeuge zur Sicherstellung von Korrektheit an ihre Grenzen stoßen. Selbst eine überdurchschnittlich hohe Test-Coverage deckt nicht den gesamten Zustandsraum von parallelen (und verteilten) Programmen ab. Und in den dunklen Ecken des Zustandsraums verstecken sich die besonders widerspenstigen Bugs.

Deshalb stellt der Vortrag TLA+ und dessen Werkzeuge vor, mit denen sich der gesamte Zustandsraum von parallelen Programmen testen lässt. Dazu wird die systematische Analyse und das Beheben eines Bugs mit TLA+ gezeigt und ein Vergleich zum traditionellen Debugging gezogen. Anschließend werden weiterführende Fähigkeiten von TLA+ gezeigt, Erfolgsgeschichten aus Forschung und Industrie vorgestellt, aber auch die Grenzen von TLA+ erläutert.

Vorkenntnisse
Es ist kein Vorwissen nötig. Zuhörer können sich vorher das Buffer-Beispiel herunterladen und probieren, selbst das Deadlock zu reproduzieren. Wer die Ursache und die Lösung für das Deadlock sofort erkennt, sollte sich einen parallelen Vortrag anhören.

Lernziele
Ziel dieses Vortrags ist es, den Zuhörern die Möglichkeiten von formalen Methoden wie TLA+ zu zeigen und ihnen einen leichten Einstieg zu geben. 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 sein Werkzeug als auch das Tool, dessen Entwicklung er vorantreibt. Früher wich Markus noch vor formalen Methoden zurück und verließ sich auf Testing und Code-Reviews. Mittlerweile hat er gelernt, dass Berührungsängste mit formalen Methoden im Allgemeinen und TLA+ im Besonderen unbegründet sind. Heute nutzt er TLA+ wie selbstverständlich für die Arbeit, die als Principal Software Development Engineer bei Microsoft Research anfällt.