"Click and Prove!"

The Grammatech Synthesizer Generator (or, in short, the synthesizer) was shipped, at that time, with several examples of codes, including a code by Bill Pugh that showed how the tool could be used to prove properties on programs (pre/post-conditions on Dijkstra guarded commands language). My job was simple: modify and extend that code to handle UNITY syntax and logic.

It seemed so easy that I remember thinking at that time: "Let's spend a month on UNITY language and safety properties, and then we'll have time to focus on liveness, which may be more difficult." In other words, the whole thing should be ready for Christmas. I was young, I was wrong...

Seven years later, the safety properties part is still not completely solved. Actually, I spent that first month digging in Pugh's code, which was not of the cleanest kind. Also, I had to learn UNITY and the synthesizer language at the same time.

What I got first was inconsistent results, including the ability to prove properties that were not true (something that should definitely be avoided in program verification). After a month or so, I finally discovered that Pugh's code was able to prove

A \/ B => A /\ B

We quickly decided that to debug that code would be too difficult a task, and that we should instead find another existing procedure to check basic logical properties (again, the laziness of the group: "Let's find someone who has already done the job..."). This happened to be a little more difficult that it may seem at first.

At that time (early 1993, since the project was not completed for Christmas, as expected), we could easily find two families of tools.

• Firstly, theorem provers that can handle very complex logics, but that won't do anything more than just what you tell them to do (some people would badmouth them and call them proof editors instead of theorem provers). The first and best known of them is HOL. Others appeared later, like Coq or Isabelle.
• Secondly, theorem provers that can only handle more elementary logics, but that can do (parts of) the job by themselves. The most popular, at that time, was Otter.

Because we were lazy, ... Ok, you got the point.

So, I started to learn how to make Otter do proofs for me. Otter can work automatically, as soon as its hundreds of parameters are correctly chosen, which requires some expertise that none of us had (and still have not). Anyhow, mostly by trying random configurations, I managed to make Otter prove interesting things.

I had then to connect Otter to the editor generated by the synthesizer (nasty things, like side effects in attribute evaluation to write and read in pipes and sockets...). This was the first piece of C code in my programmer's life, and it was quite famous in the lab, at some point. I was writing C code in an unconventional way: go to the next line only when you reach the end of the current line (80 characters or so), use explicit numbers instead of macros from files like fcntl.h, choose a, b, c, d,... as identifiers, don't waste time writing comments, etc. (kind of ioccc code without even looking for it). And of course, once the program seems to work, throw the source away, since it is clear that it would become unreadable after a week or two (this is why, unfortunately, I can't show the source). Shame on me. Note that, a couple of years later, I was teaching C programming in operating systems labs. If students had known...

Anyway, I finally obtained a tool that was able to prove some elementary properties on a UNITY program, as long as very few arithmetic was involved. Otter, as a tool built by and for logicians, didn't like arithmetic very much. For instance, a rule like:

(x < y) /\ (x' < y') => (x+x' < y+y')

My tool was called DADA, for Distributed Algorithm Design Assistant. The name was found by Philippe Mauran and, as of today, this remains his most remarkable contribution to the project (just kiddin', Philippe...). I'm afraid you need to speak French to understand why we liked the name (In my dictionary, the French "dada" in translated into the English "horsie" or "gee-gee").

If you think of it (and at first, we didn't), when you describe distributed algorithms in UNITY, using array indexes, event counters and logical clocks for instance, the kind of formulas you obtain are much more arithmetic than logic. I think a lot of people now understand the importance of arithmetic in program verification. This is why Coq was later extended with arithmetic procedures. This is also probably one of the reasons that made the theorem prover PVS so popular. But this is also why Otter would never be able to fully solve our problems, and why I started to look for a tool more inclined to work with numbers.

The tool we found is called Omega Calculator. Omega is not a theorem prover at all, and was not intended to be used as such. Omega only does one thing, and it does it well: arithmetic. It's a decision procedure for Presburger arithmetic (linear integer arithmetic), written by a group led by... Bill Pugh! The return of the guy who was able to prove A \/ B => A /\ B scared us a little, but we decided to trust him. And we were right: Omega has been very useful and has helped improve Dada's proving capabilities. (Note that a tool able to prove A \/ B => A /\ B would also improve proving capabilities, but that's not the point.)

Helped by Adbellah El Hadri from EMI, I managed to find a way to verify UNITY properties with Omega. What we did there was kind of a makeshift job, but it was later extended and properly formalized by Xavier Thirioux (no web page that I know of) in his PhD work. Another (better) piece of C code, and Dada then offered to the user two ways to check properties. Depending on how much arithmetic is involved, a user could choose to use Otter or Omega to check a specific property. Omega was good with arithmetic (obviously), while Otter was good for large formulas (Omega, as a decision procedure, requires a lor of memory). The choice was made by "clicking" on an Omega button, or on an Otter button, and then wait for the answer. No further interaction was required. The concept of "click and prove!" was born.

Using Dada actually involved a recurrent pattern in the process. After the UNITY program and its specification are written in the tool, "finding the invariant" is the name of the game. You have to guess one and try it. Then Dada would tell you which transitions do not satisfy the invariant, and this would usually be enough to understand why the predicate is not an invariant. You have then to modify the predicate and try again, until the predicate is claimed by Dada to actually be an invariant. In reality, our dream of "click and prove!" was more something like "click and... wait and... try again!".

The process can be short (when you are good at finding invariants, or lucky in general), or it can be long (when the invariant is especially tricky). For instance, the worst case in our experiments was the invariant in Mattern's termination detection algorithm: it took us almost two years to find that nasty half-a-page predicate. Nevertheless, most of the time, using a tool like Dada to check the inductiveness of invariants saves time. Other forms of interaction with assistants are possible, but this basic principle of "guess and check" is still one of the most effective (especially when using current tools, much faster and more powerful than good old Dada).

The last thing to do was to publish a couple of papers. In order to help with this task, Dada was extended to be able to generate LaTeX from UNITY programs and specifications (as a matter of fact, that's finally what Dada was doing best).

This is what a Dada window would look like:

Besides this problem of proving formulas with arithmetic, our work on the Dada assistant made us understand (believe?) that we would need to improve some of the proof techniques used in UNITY before automatic tools like Otter or Omega can be used efficiently. In some sense, either you use a high-level tool, like HOL or Isabelle, capable of handling your whole verification problem, but then, you have to interact a lot with the tool, in its own world and its own language. Or you choose to use more elementary and more automatic tools, but then you have to simplify the proof obligations at the logical level, before attempting to use a prover. Also, we knew that going more deeply into the design of a proof assistant would require an expertise in theorem proving that we did not have (remember that we were interested in distributed algorithms in the first place).

For all these reasons, while I was still working on developing Dada during the first years, the search for proof techniques specific to distributed algorithms started to become my real PhD work (as well as a domain of interest for most of the group). The idea was to find a number of abstractions, specific to distributed computing, that can be used to simplify proof obligations by reusing a generic form of reasoning related to these abstractions. The project Dada became Distributed Algorithm Design and Analysis (you don't throw away a name like that...)

Michel Charpentier <>