Introduction

1  What is PlusCal?

PlusCal is an algorithm language—a language for writing and debugging algorithms.  It is especially good for algorithms to be implemented with multi-threaded code.  Instead of being compiled into code, a PlusCal algorithm is translated into a TLA+ specification.  An algorithm written in PlusCal is debugged using the TLA+ tools—mainly the TLC model checker.  Correctness of the algorithm can also be proved with the TLAPS proof system, but that requires a lot of hard work and is seldom done.

2  Why PlusCal?

From 1974 to 2010, I was an author of over 25 papers introducing new concurrent algorithms.  To my knowledge, only one error was ever found in any of those published algorithms: I failed to state that a particular algorithm was correct only if the number of processes is finite.  A few of those algorithms, including the first one I published, are taught in university courses.

Concurrent algorithms are not something you learn about in school and then find in a textbook when you need one.  Errors in concurrent programs occur when multiple processes concurrently access shared data.  Those errors can be prevented by not allowing a process to access the data while another process is using it.  However, that is usually too inefficient because it makes processes spend too much time waiting to access the data.  An algorithm is then needed to allow different processes to access different parts of the data concurrently.  Textbooks do not have algorithms for sharing every kind of data.  Programmers must often invent the algorithms they need. They might just need a small change to a textbook's algorithm, but even a small change to a concurrent algorithm can introduce errors that are hard to detect.

My experience writing concurrent algorithms taught me that programming languages are not good for thinking about concurrency.  They force you to think at too low a level of detail, obscuring the forest with too much underbrush.  Programming languages lead you to try solving a concurrency problem by coding rather than by designing an algorithm; and this often produces concurrency bugs. 

Tools for debugging code are ineffective at finding concurrency bugs in the algorithm implemented by the code.  So, the code is left with bugs that are hard to find and hard to fix when found, since patching the code often introduces new bugs.  Concurrency bugs should be fixed at the algorithm level, before writing the code.

PlusCal is the language I wish I had realized that I needed when I began writing concurrent algorithms.

3  Prerequisites

This tutorial assumes some familiarity with an imperative programming language—one with statements that assign values to variables.  While not necessary, it also helps to understand simple mathematical concepts like sets and functions.  The math you will use is quite elementary and will all be explained here, but you will find the tutorial easier if you have seen that math before.

To use the tutorial, you will need to install a program on your computer and download files where the program can find them.