Personal Observations on the Workshop Leslie Lamport Here are some random thoughts about what went on. * I and others expected that differences among the solutions would reflect the different underlying formalisms. It turned out that the differences were based on the approach chosen by the specifiers, which in many cases were independent of the formalisms they used. I identified the following different approaches: Pure Axiomatic: Expressing the desired properties of the memory in terms only of the observable operations. Impure Axiomatic: Expressing the desired properties of the memory by relating the observable operations to internal operations of a simple memory, which is specified in a purely axiomatic fashion. A Few Processes: Specifying the memory as some sort of abstract automaton/program involving a few processes, each with a large number of internal states. Many Processes: Specifying the memory as some sort of abstract automaton/program involving many processes, each with a small number of internal states. * Purely axiomatic specifications became popular In the late 1970's, when people were all excited about temporal logic. The idea was to write down a list of axioms that mention only externally observable quantities, eschewing any kind of internal state. By talking only about things that are observable and avoiding any unnecessary mechanism, the specification would be general and not biased towards any implementation. For example, one would specify a memory by talking only about read and write operations, never mentioning the contents the memory. You could then implement the memory any way you wanted, without being biased by the particular representation used in the specification. This seemed like a great idea at the time. However, trying to write axiomatic specifications and watching other people writing them, I soon came to the conclusion that they just didn't work. People would work for hours trying to come up with a set of axioms to characterize a simple system, and would never be sure that they had succeeded. It became clear to me that this method had no chance of scaling to real specifications. It was just too hard to figure out what sorts of behaviors were and were not allowed by a set of axioms. This realization led me to develop the transition axiom method, which in turn led to TLA. Four of the presentations used purely axiomatic specifications of the memory component. I would have thought that, after 15 years, people would at least be able to write an axiomatic specification of something as simple as the high-level memory of the problem. I was wrong. Every one of the four axiomatic specifications was wrong. More precisely, they all allowed behaviors that everyone, including the authors of the specifications, agreed should not be allowed. The "impure axiomatic" specifications seemed to be correct. It is possible to specify a trivial memory axiomatically. * The specification problem was based on a procedure-calling interface. A large number of the participants felt that a procedure call, being unlike CSP and CCS communication, was an unnatural and esoteric form of interface that must have been chosen to bias the problem in favor of certain approaches. I wondered aloud what planet those participants had come from. * One syndrome I've long observed among computer scientists is a belief that, if the programming language doesn't give you a way of mentioning something, then it doesn't exist. A popular symptom of this was the feeling among many computer scientists that it was immoral to mention the control state of a program in a correctness proof. Since you can't verify concurrent programs without mentioning the control state, people introduced dummy variables to capture it, the dummy variables serving as euphemisms that allowed you to talk about the control state in polite company. This syndrome appeared in the following form at the workshop. The problem statement says that the procedure return should identify the the invoking process. However, in keeping with the normal practice in concurrent programming languages, the process identifier was not made an explicit parameter of the procedure call. It is obviously impossible for a procedure to return an identifier that it has not been given, so the identifier must be an implicit parameter of the call. Yet, several of the participants felt obliged to apologize for including such a parameter in their specifications. * A process algebra provides a simple, elegant language for writing finite-state automata. Process algebras allow recursive definitions of processes, so they can be used to write unbounded-state automata too. But only tail recursion, which produces finite-state automata, seem to be used in practice. (I suspect that nontrivial recursive definitions of processes are hard to understand.) I thought it would be hard to solve the problem using process algebra. I was wrong. The problem was easier for process algebras to handle than I had realized because the data dependence is so simple. The only inherent data structure is a simple memory--an array of memory values indexed by memory locations. I learned how easy it is to represent such a memory with a process algebra: A memory is the parallel composition of a whole bunch of simple automata--one for each pair. The automaton for the pair has two states: one for memory[l] = v and the other for memory[l] /= v. I doubt that this sort of trick is practical for more complicated data structures, but I could be wrong about that too. As a test, I would propose a memory that includes a protection mechanism, based on the Unix file system's. There are users and groups of users. Each memory element has an owner, a group, and a protection status indicating whether it can be read and/or written by the owner, by members of the group, and by everyone. The commands are read, write, chmod (change protection status), and chgrp (change file's group). It would be interesting to see how such a process algebraic specification of this system would look. * The high point of the workshop for me was the presentation of Bernhard Steffen, who had the following beautiful idea. Suppose you use the process algebra approach of writing the specification as a parallel composition of processes P(v) for values v in some set S: Spec == ||_{v \in S} P(v) Suppose the implementation is also in that form: Impl == ||_{v \in S} Q(v) To prove that the implementation satisfies the specification, it suffices to prove that Q(v) implements P(v), for each v. But if Q(v) and P(v) are finite state automata, then this proof can be done automagically by model checking. That's what Steffen did. This trick should work very nicely in TLA. In TLA, one would normally write the spec in the form Spec == /\ \forall v \in S : Init(v) /\ [][\exists v \in S : Next(v)]_... /\ Fairness By using the fact that /\ distributes over [], and essentially rewriting the next-state action from disjunctive to conjunctive form, one can rewrite the spec so it has the form \forall v \in S : /\ Init(v) /\ [][Next(v)]_... /\ Fairness There's a big waving of hands here. See Section 4.2 of "Conjoining Specifications" to see how it actually works. The spec is then the conjunction (in TLA, composition is conjunction) of finite-state specifications that can be handled by a model checker--for example, the TLA to COSPAN translator that Marc Foissott wrote at Bell Labs. People doing automatic verification have developed a number of ways of factoring out data dependence to reduce problems to finite-state ones that they can throw a model checker at. I suspect that, by using this trick, one can formalize those methods in TLA. Instead of applying ad hoc methods for reducing the problem to a finite-state one, we can use TLA reasoning. Moreover, we aren't restricted to the case in which Q(v) implements P(v). Applying the Decomposition Theorem of "Conjoining Specifications" might yield a more powerful method. * Jozef Hooman wrote his specifications in PVS (the mechanical verification system developed by Shankar at SRI) and did all his proofs with PVS. He said that it took a total of one week. I found that very impressive. I think it would take much more time to do that in LP. This makes me feel that we should check out PVS as a possible back end for TLP, the TLA proof checking system.