Distributed algorithms in TLA (abstract)

ABSTRACT

TLA (the temporal logic of actions) is a simple logic for describing and reasoning about concurrent systems. It provides a uniform way of specifying algorithms and their correctness properties, as well as rules for proving that one specification satisfies another. TLA+ is a formal specification language based on TLA, and TLC is a model checker for TLA+ specifications. TLA+ and TLC have been used to specify and check high-level descriptions of real, complex systems. Because TLA+ provides the full power of ordinary mathematics, it permits simple, straightforward specifications of the kinds of algorithms presented at PODC. This tutorial will try to convince you to describe your algorithms in TLA+. You will then be able to check them with TLC and use TLA to prove their correctness as formally or informally as you want. (However, TLA proofs do have one disadvantage that is mentioned below.) The tutorial will describe TLA+ through examples and demonstrate how to use TLC. No knowledge of TLA is assumed. TLA does have the following disadvantages: It can describe only a real algorithm, not a vague, incomplete sketch of an algorithm. You can specify an algorithm's correctness condition in TLA only if you understand what the algorithm is supposed to do. TLA makes it harder to cover gaps in a proof with handwaving. Some researchers may find these drawbacks insurmountable.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

General Terms:
Documentation, Experimentation