Proving Liveness Properties of Concurrent Programs

During the late 70s and early 80s, Susan Owicki and I worked together quite a bit. We were even planning to write a book on concurrent program verification. But this paper is the only thing we ever wrote together.

In [23], I had introduced a method of proving eventuality properties of concurrent programs by drawing a lattice of predicates, where arrows from a predicate P to predicates Q1, …, Qn mean that, if the program reaches a state satisfying P, it must thereafter reach a state satisfying one of the Qi. That method never seemed practical; formalizing an informal proof was too much work.

Pnueli’s introduction of temporal logic allowed the predicates in the lattice to be replaced by arbitrary temporal formulas. This turned lattice proofs into a useful way of proving liveness properties. It permitted a straightforward formalization of a particularly style of writing the proofs. I still use this proof style to prove leads-to properties, though the proofs are formalized with TLA (see [102]). However, I no longer bother drawing pictures of the lattices. This paper also introduced at, in, and after predicates for describing program control.

It’s customary to list authors alphabetically, unless one contributed significantly more than the other, but at the time, I was unaware of this custom. Here is Owicki’s account of how the ordering of the authors was determined.

As I recall it, you raised the question of order, and I proposed alphabetical order. You declined–I think you expected the paper to be important and didn’t think it would be fair to get first authorship on the basis of a static property of our names. On the night we finished the paper, we went out to dinner to celebrate, and you proposed that if the last digit of the bill was even (or maybe odd), my name would be first. And, indeed, that’s the way it came out.