Processes are in the Eye of the Beholder

The notion of a process has permeated much of the work on concurrency. Back in the late 70s, I was struck by the fact that a uniprocessor computer could implement a multiprocess program, and that I had no idea how to prove the correctness of this implementation. Once I had realized that a system was specified simply as a set of sequences of states, the problem disappeared. Processes are just a particular way of viewing the state, and different views of the same system can have different numbers of processors.

A nice example of this is an N-buffer producer/consumer system, which is usually viewed as consisting of a producer and a consumer process. But we can also view it as an N-process system, with each buffer being a process. Translating the views into concrete programs yields two programs that look quite different. It’s not hard to demonstrate their equivalence with a lot of hand waving. With TLA, it’s easy to replace the hand waving by a completely formal proof. This paper sketches how.

I suspected that it would be quite difficult and perhaps impossible to prove the equivalence of the two programs with process algebra. So, at the end of the paper, I wrote “it would be interesting to compare a process-algebraic proof … with our TLA proof.” As far as I know, no process algebraist has taken up the challenge. I figured that a proof similar to mine could be done in any trace-based method, such as I/O automata. But, I expected that trying to make it completely formal would be hard with other methods. Yuri Gurevich and Jim Huggins decided to tackle the problem using Gurevich’s evolving algebra formalism (now called abstract state machines). The editor processing my paper told me that they had submitted their solution and suggested that their paper and mine be published in the same issue, and that I write some comments on their paper. I agreed, but said that I wanted to comment on the final version. I heard nothing more about their paper, so I assumed that it had been rejected. I was surprised to learn, three years later, that the Gurevich and Huggins paper, Equivalence is in the Eye of the Beholder, appeared right after mine in the same issue of Theoretical Computer Science. They chose to write a “human-oriented” proof rather than a formal one. Readers can judge for themselves how easy it would be to formalize their proof.