Specifying Concurrent Program Modules

The early methods for reasoning about concurrent programs dealt with proving that a program satisfied certain properties–usually invariance properties. But, proving particular properties showed only that the program satisfied those properties. There remained the possibility that the program was incorrect because it failed to satisfy some other properties. Around the early 80s, people working on assertional verification began looking for ways to write a complete specification of a system. A specification should say precisely what it means for the system to be correct, so that if we prove that the system meets its specification, then we can say that the system really is correct. (Process algebraists had already been working on that problem since the mid-70s, but there was–and I think still is–little communication between them and the assertional verification community.)

At SRI, we were working on writing temporal logic specifications. One could describe properties using temporal logic, so it seemed very natural to specify a system by simply listing all the properties it must satisfy. Richard Schwartz, Michael Melliar-Smith, and I collaborated on a paper titled Temporal Logic Specification of Distributed Systems, which was published in the Proceedings of the 2nd International Conference on Distributed Computing Systems, held in Paris in 1981. However, I became disillusioned with temporal logic when I saw how Schwartz, Melliar-Smith, and Fritz Vogt were spending days trying to specify a simple FIFO queue–arguing over whether the properties they listed were sufficient. I realized that, despite its aesthetic appeal, writing a specification as a conjunction of temporal properties just didn’t work in practice. So, I had my name removed from the paper before it was published, and I set about figuring out a practical way to write specifications. I came up with the approach described in this paper, which I later called the transition axiom method. Schwartz stopped working on specification and verification in the mid-80s. He wrote recently (in June 2000):

[T]he same frustration with the use of temporal logic led Michael, Fritz Vogt and me to come up with Interval Logic as a higher level model in which to express time-ordered properties of events. [See [44].] As you recall, interval logic expressed constraints forward and backward around significant events in order to more closely capture the way that people describe event-driven behavior. Ultimately, I remain unsatisfied with any of our attempts, from the standpoint of reaching practical levels.

This paper is the first place I used the idea of describing a state transition as a boolean-valued function of primed and unprimed variables. However, by the early 80s, the idea must have been sufficiently obvious that I didn’t claim any novelty for it, and I forgot that I had even used it in this paper until years later (see the discussion of [102]).