In the beginning...
My PhD advisor was Professor
Gérard Padiou. I started to work with him in September
1992, in the school of engineering ENSEEIHT, part of the university
INPT.
Gérard was the head of a group
working on distributed operating systems and distributed
algorithms in general. At the time I joined the group, they were
interested in starting to look at distributed algorithms with a
rather formal view. They had chosen the logical framework UNITY,
proposed in 1988 by K. Mani
Chandy and Jayadev Misra.
UNITY is a framework composed of four parts:
- A (simple) programming notation, in which fair
transition systems can be described in a human readable way;
- A (simple) logic, which can be seen as a
fragment of linear temporal logic: only a limited number of
operators, rather easy to understand intuitively, and that
cannot be nested;
- A proof system that can be used to prove
that programs, described with the programming notation,
satisfy properties, expressed in the logic;
- A (quite famous) substitution axiom,
that introduces inconsistencies in the logic, which allow
you to prove properties much more easily (you start by
proving that true=false, and the
rest follows...).
To quote Jay Misra, who was paraphrasing Mark Twain, "The
unsoundness of the the substitution axiom has been greatly
exaggerated" (note 14
on UNITY). Well, in spite of Jay's early
explanations, the unsoundness is undeniable, and has really been
a bad publicity for UNITY (especially among people
who didn't read the book). However, one must keep in mind that:
- Once the problem is solved, UNITY is clearly a
novel and influential approach, described in a very
well-written book, in which dozens of nontrivial examples,
from different areas of concurrent programming, are treated in
details.
- The statement and the study of the problem itself helped
understand tons of things, especially with respect to
composition.
In conclusions, the substitution axiom problem is solved by adding
10 pages to a 516 page book. Once this is done, the book is
definitely worth reading. As Beverly A. Sanders
(who presented the first nice answer to the substitution axiom
problem) once wrote (in an email):
"As a practical matter, one can use UNITY for proving programs
exactly as described in the book.". From now on, let's assume
that UNITY is composed only of three parts: a programming notation, a logic
and a proof system. If you are curious, you can read more on UNITY's substitution
axiom, or check UNITY books and
papers. Note that everything I say here reflects my
own ideas about UNITY. If you want to know what Mani,
Jay or Beverly think of it, ask 'em.
Gérard and the other members of the group were ready to
describe algorithms using UNITY notation, as well as to
specify properties in UNITY logic. However, they were lazy
people, and they didn't want to write all proofs by hand. (Maybe
they would prefer to say that they wanted to focus on
distributed algorithms design and not on proofs details.) Anyway,
they decided to hire a student to write a proof
assistant for them. And that's how I started my DEA work
(a French DEA is a kind of Masters)...
Next
Michel Charpentier <
>
Last modified: Thu Feb 24 15:37:51 EST 2000