Weeks of debugging can save you hours of TLA+

This is a past event

48 people went

Location image of event venue

Details

Nebenläufigkeit und Verteilung sind zentrale Bausteine, 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 kann nicht den gesamten Zustandsraum von nebenläufigen und verteilten Programmen abdecken. Und in den dunklen Ecken des Zustandsraums verstecken sich die besonders widerspenstigen Bugs.

Seht euch bspw. das folgende Snippet einer Implementierung [1] eines BlockingQueue an. Selbst darin versteckt sich ein Deadlock:

public synchronized void put(final E e) throws InterruptedException {
while (isFull()) {
wait();
}
notifyAll();
append(e);
}

public synchronized E take() throws InterruptedException {
while (isEmpty()) {
wait();
}
notifyAll();
return tail();
}

Deshalb stellt der Vortrag TLA+ und dessen Werkzeuge vor, mit denen sich der gesamte Zustandsraum von Programmen "testen" lässt. Dazu wird die systematische Analyse und das Beheben des obigen Deadlocks mit TLA+ gezeigt und ein Vergleich zum traditionellen Debugging gezogen.
Anschließend werden weiterführende Features von TLA+ ausprobiert, Erfolgsgeschichten aus Forschung und Industrie vorgestellt, aber auch die Grenzen von TLA+ genannt.

Ziel ist es, die Möglichkeiten von TLA+ zu zeigen und euch einen leichten Einstieg zu geben. Der Fokus liegt dabei auf dem praktischen Einsatz, der akademische Unterbau wird nur am Rande behandelt.

Referent:

Markus Kuppe beschäftigt sich mit nebenläufiger und verteilter Programmierung, um diese handhabbarer zu machen. TLA+ ist dabei sowohl Zweck als auch Mittel. 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 seine Arbeit und Forschung bei Microsoft Research.