The PlusCal Tutorial

Leslie Lamport

Last modified on 3 December 2021

Programming = Algorithms + Coding. Algorithms are not just found in textbooks. Even if you find an algorithm you can use in a textbook, you may have to modify it for your application. Concurrent processesing problems should be solved with algorithms. Trying to solve them at the code level leads to concurrency bugs. Tools for finding coding errors are ineffective at finding errors in concurrent algorithms.

PlusCal is a language for writing algorithms—especially concurrent and distributed ones. It looks like a toy programming language with constructs for describing concurrency and nondeterminacy, but its rich expression language makes it well-suited for describing algorithms. PlusCal algorithms can be checked with the TLA+ tools, the most commonly used tool being the TLC model checker.

The PlusCal Tutorial will teach you to write and check PlusCal algorithms. It assumes only a basic knowledge of programming concepts, though PlusCal will be most useful for describing multi-threaded programs and distributed systems. Some knowledge of simple math, as taught at universities to first-year computer science students, will be helpful but is not necessary.

Tutorial Begins Here Table of Contents