Introduction to TLA+

Concurrent and distributed programs are notoriously difficult to get right. Even tiny variations of algorithms like Peterson’s lock for mutual exclusion lead to significantly different behaviours and errors that are complex to locate.

TLA+ is a high-level language for modelling such programs and specifying their behaviour in a rigorous way. In this tutorial, you will learn how to write concurrent and distributed algorithms in PlusCal, a pseudo-code like interface for TLA+, and how to specify correctness conditions using temporal logic. We will further apply the model-checker TLC and discuss typical pitfalls when working with TLA+.

Preparation

Please install the TLA Toolbox on your machine by following the instructions on this page.

Annette Bieniusa

@anne_biene

Annette is a lecturer and senior researcher at the TU Kaiserslautern. Her research interests are the semantics of concurrent and distributed programming, with a focus on replication and synchronization, and how they are reflected on a programming language level. Annette was involved in several national and international research projects, most recently in the EU-Projects “SyncFree: Large-scale Computation without Synchronization” and “Lightkone: Lightweight computation for networks at the edge“. She is further leading the development of AntidoteDB, a transactional CRDT-key value store.