Name: Weeks of debugging can save you hours of TLA+
Start: 2018-06-12T19:00:00+02:00
End: 2018-06-12T21:00:00+02:00
Location: GULP Information Services GmbH

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.

Uwe Sauerbrei

Java User Group Hamburg

Technology

Web Technology

Java

Open Source

Software Development

Web Development

Computer Programming

Programming Languages

Continuous Integration

Java Virtual Machine

DevOps

Weeks of debugging can save you hours of TLA+

GULP Information Services GmbH

Share

Java User Group Hamburg

Weeks of debugging can save you hours of TLA+

Java User Group Hamburg

Details

Members are also interested in