An Old-Fashioned Recipe for Real Time

As explained in the discussion of [51], it’s been clear for a long time that assertional methods for reasoning about concurrent algorithms can easily handle real-time algorithms. Time just becomes another variable. That hasn’t stopped academics from inventing new formalisms for handling time. (Model checking real-time algorithms does raise new problems, since they are inherently not finite-state.) So, when de Roever held a workshop on formalisms for real-time systems, it was a good opportunity to show off how easily TLA deals with real-time algorithms. We also proved some new results about nonZeno specifications. I believe this paper introduced the terms Zeno and nonZeno, though the notion of Zeno behaviors had certainly occurred to others. It does seem to have been the first to observe the relation between nonZenoness and machine closure. Abadi has the following to say about this paper:

For me, this paper was partly a vindication of some work I had done with [Gordon] Plotkin [A Logical View of Composition, Theoretical Computer Science 114, 1 (June 1993), 3-30], where we explored the definition and properties of the “while” operator (-|>). I believe that you thought that the work was a formal game, so I was pleased to find that we could use it in this paper.

The paper uses as an example a mutual exclusion protocol due to Michael Fischer. This example has an amusing history. When I was working on [73], I sent Fischer email describing my algorithm and asking if he knew of a better solution. He responded

No, I don’t, but the practical version of the problem sounds very similar to the problem of bus allocation in contention networks. I wonder if similar solutions couldn’t be used? For example, how about…
He followed this with a simple, elegant protocol based on real-time delays. Because of its real-time assumptions, his protocol didn’t solve the problem that motivated [73]. I mentioned this algorithm in [73], but had forgotten about it by the time of de Roever’s workshop. Fred Schneider reminded me of it when he used it as an example in his talk at the workshop. We then incorporated the example in our paper. I later mentioned this to Fischer, who had no memory of the protocol and even claimed that it wasn’t his. Fortunately, I happen to have saved his original email, so I had the proof. The message, complete with message number, is cited in the paper–the only instance of such a citation that I know of.