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
@lemmster
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.