This document is a sort of scientific autobiography. It not only lists the papers I have written, but also describes them and explains how I came to write some of them. I have included almost all my technical papers and electronic versions of many of them for downloading. Omitted are some papers for which I no longer have copies and papers that are incomplete. I have also omitted early versions of some of these papers--even in cases where the title changed. Included are some initial drafts of papers that I abandoned before fixing errors or other problems in them. A table of contents precedes the descriptions. I also include a brief curriculum vitae. A printable version of this document is available as a pdf file.
Each description attempts to explain the genesis of the work. However, I have forgotten how I came to write most of my papers. Even when I discourse at length about the development of the ideas, I am giving only a subjective view based on my unreliable memory. Whenever possible, I have asked other people involved to check the accuracy of what I've written. However, what I have most often forgotten is the work of others that influenced my own work. This may give the impression that I am claiming more credit for ideas than I deserve, for which I apologize.
Where I think it's interesting, I give the story behind the publication or non-publication of a paper. Some of the stories read like complaints of unfair treatment by editors or referees. Such cases are bound to arise in any activity based on human judgment. On the whole, I have had little trouble getting my papers published. In fact, I have profited from the natural tendency of editors and referees to be less critical of the work of established scientists. But I think it's worth mentioning the cases where the system didn't work as it should.
I would like to have ordered my papers by the date they were written. However, I usually have no record of when I actually wrote something. So, I have ordered them by date of publication or, for unpublished works, by the date of the version that I have. Because of long and variable publication delays, this means that the order is only approximately chronological.
Whenever possible, I have included electronic versions of the works. I have electronic versions of most works written after about 1985. For journal articles, these may be "preprint" versions, formatted differently and sometimes differing slightly from the published versions. I have been scanning papers for which I don't have source files as I find copies of them.
Anyway, this paper was my first pass at writing up the complete
version of the theory for publication. I strongly suspect that it has
never been read. No one seems to have noticed that, because of a
text-editing error, the description of the algorithm is missing the
punch line that says what can be executed in parallel. This paper is
superseded by the unpublished [20].
To justify my attendance at Sagamore, I always submitted a paper.
But once I discovered that it was not a first-rate conference, I did not
submit first-rate papers. However, I don't republish old material
(except as necessary to avoid forcing people to read earlier papers),
so this paper must have included some new results about the hyperplane
method for parallelizing sequential loops. However, I don't have a
copy of the paper and don't remember what was in it.
I don't know how many people realize how remarkable this algorithm is. Perhaps the person who realized it better than anyone is Anatol Holt, a former colleague at Massachusetts Computer Associates. When I showed him the algorithm and its proof and pointed out its amazing property, he was shocked. He refused to believe it could be true. He could find nothing wrong with my proof, but he was certain there must be a flaw. He left that night determined to find it. I don't know when he finally reconciled himself to the algorithm's correctness.
Several books have included emasculated versions of the algorithm in which reading and writing are atomic operations, and called those versions "the bakery algorithm". I find that deplorable. There's nothing wrong with publishing a simplified version, as long as it's called a simplified version.
What is significant about the bakery algorithm is that it implements mutual exclusion without relying on any lower-level mutual exclusion. Assuming that reads and writes of a memory location are atomic actions, as previous mutual exclusion algorithms had done, is tantamount to assuming mutually exclusive access to the location. So a mutual exclusion algorithm that assumes atomic reads and writes is assuming lower-level mutual exclusion. Such an algorithm cannot really be said to solve the mutual exclusion problem. Before the bakery algorithm, people believed that the mutual exclusion problem was unsolvable--that you could implement mutual exclusion only by using lower-level mutual exclusion. Brinch Hansen said exactly this in a 1972 paper. Many people apparently still believe it. (See [91].)
The paper itself does not state that it is a "true" mutual exclusion algorithm. This suggests that I didn't realize the full significance of the algorithm until later, but I don't remember.
For a couple of years after my discovery of the bakery algorithm, everything I learned about concurrency came from studying it. Papers like [25], [33], and [70] were direct results of that study. The bakery algorithm was also where I introduced the idea of variables belonging to a process--that is, variables that could be read by multiple processes, but written by only a single process. I was aware from the beginning that such algorithms had simple distributed implementations, where the variable resides at the owning process, and other processes read it by sending messages to the owner. Thus, the bakery algorithm marked the beginning of my study of distributed algorithms.
The paper contains one small but significant error. In a
footnote, it claims that we can consider reads and writes of a single
bit to be atomic. It argues that a read overlapping a write must
get one of the two possible values; if it gets the old value, we can
consider the read to have preceded the write, otherwise to have
followed it. It was only later, with the work eventually described in
[70], that I realized the fallacy in this reasoning.
The note contains the intriguing sentence: "There is a complicated
modified version of the bakery algorithm in which the values of all
variables are bounded." I never wrote down that version, and I'm not
sure what I had in mind. But I think I was thinking of roughly the
following modification. As a process waits to enter its critical
section, it keeps reducing its number, not entering the critical
section until its number equals one. A process p can reduce
its number by at most one, and only when the next lower-numbered
process's number is at least two less than p's number, and the
next higher-numbered process is within one of p's number. I
think I intended to use the techniques of [25] to allow
reading and writing of numbers to remain non-atomic while maintaining
the order of waiting processes. (If eventually all processes stop
changing their numbers, then all processes will eventually read the
correct numbers, allowing some process to progress.) At one time, I
convinced myself that this algorithm is correct. But I never wrote a
rigorous proof, so I don't know if it really works. Filling in the
details and proving correctness should be a nice exercise.
A referee said of the initial submission that the proofs were too
long, tediously proving the obvious. In fact, there was a bug in the
initial version, and at least one of those obvious proofs was of a
false statement. Needless to say, I corrected the algorithm and wrote
more careful proofs.
The basic proof that an arbiter cannot have a bounded response time uses continuity to demonstrate that, if there are two inputs that can drive a flip-flop into two different states, then there must exist an input that makes the flip-flop hang. At the time, it was very difficult to convince someone that this argument was valid. They seemed to believe that, because a flip-flop has only discrete stable states, continuity doesn't apply.
I described the arbiter problem to Palais, who had been my de jure thesis adviser and afterwards became a colleague and a friend. He recognized that the correct mathematical way to view what was going on is in terms of the compact-open topology on the space of flip-flop behaviors. So, we wrote this paper to explain why the apparently discontinuous behavior of an arbiter is actually continuous in the appropriate topology.
This paper was rejected by the IEEE Transactions on Computers
because the engineers who reviewed it couldn't understand the
mathematics. Six years later, the journal apparently acquired more
mathematically sophisticated reviewers, and it published a less
general result with a more complicated proof. I believe someone has
finally published a paper on the subject that does supersede ours.
In the course of my work on parallelizing sequential code (see [10]), I essentially rediscovered Floyd's method as a way of extracting properties of a program. When I showed a colleague what I was doing, he went to our library at Massachusetts Computer Associates and gave me a copy of the original tech report version of Floyd's classic paper Assigning Meanings to Programs. I don't remember when I read Hoare's An Axiomatic Basis for Computer Programming, but it was probably not long afterwards.
In the mid-70s, several people were thinking about the problem of verifying concurrent programs. The seminal paper was Ed Ashcroft's Proving Assertions About Parallel Programs, published in the Journal of Computer and System Sciences in 1975. That paper introduced the fundamental idea of invariance. I discovered how to use the idea of invariance to generalize Floyd's method to multiprocess programs. As is so often the case, in retrospect the idea seems completely obvious. However, it took me a while to come to it. I remember that, at one point, I thought that a proof would require induction on the number of processes.
This paper introduced the concepts of safety and liveness as the proper generalizations of partial correctness and termination to concurrent programs. It also introduced the terms "safety" and "liveness" for those classes of properties. I stole those terms from Petri nets, where they have similar but formally very different meanings. (Safety of a Petri net is a particular safety property; liveness of a Petri net is not a liveness property.)
At the same time I was devising my method, Susan Owicki was writing her thesis at Cornell under David Gries and coming up with very much the same ideas. The generalization of Floyd's method for proving safety properties of concurrent programs became known as the Owicki-Gries method. Owicki and Gries did not do anything comparable to the method for proving liveness in my paper. (Nissim Francez and Amir Pnueli developed a general proof method that did handle liveness properties, but it lacked a nice way of proving invariance properties.) My method had deficiencies that were corrected with the introduction of temporal logic, discussed in [47].
The Owicki-Gries version of the method for proving safety properties differed from mine in two ways. The significant way was that I made the control state explicit, while they had no way to talk about it directly. Instead, they introduced dummy variables to capture the control state. The insignificant way was that I used a flowchart language while they used an Algol-like language.
The insignificant syntactic difference in the methods turned out to have important ramifications. For writing simple concurrent algorithms, flowcharts are actually better than conventional toy programming languages because they make the atomic actions, and hence the control state, explicit. However, by the mid-70s, flowcharts were passé and structured programming was all the rage, so my paper was forgotten and people read only theirs. The paper was rediscovered about ten years later, and is now generally cited alongside theirs in the mandatory references to previous work.
More important though is that, because they had used a "structured" language, Owicki and Gries thought that they had generalized Hoare's method. To the extent that Floyd's and Hoare's methods are different, it is because Hoare's method is based on the idea of hierarchical decomposition of proofs. The Owicki-Gries method doesn't permit this kind of clean hierarchical decomposition. Gries, commenting in 1999, said: "We hardly ever looked at Floyd's work and simply did everything based on Hoare's axiomatic theory." I suspect that, because they weren't thinking at all about Floyd's approach, they didn't notice the difference between the two, and thus they didn't realize that they were generalizing Floyd's method and not Hoare's.
The result of presenting a generalization of Floyd's method in Hoare's clothing was to confuse everyone. For a period of about ten years, hardly anyone really understood that the Owicki-Gries method was just a particular way of structuring the proof of a global invariant. I can think of no better illustration of this confusion than the EWD A Personal Summary of the Owicki-Gries Theory that Dijkstra wrote and subsequently published in a book of his favorite EWDs.( Throughout his career, Edsger Dijkstra wrote a series of notes identified by an "EWD" number.) If even someone as smart and generally clear-thinking as Dijkstra could write such a confusing hodge-podge of an explanation, imagine how befuddled others must have been. A true generalization of Hoare's method to concurrent programs didn't come until several years later in [40].
I think it soon became evident that one wanted to talk explicitly about the control state. Susan Owicki obviously agreed, since we introduced the at, in, and after predicates for doing just that in [47]. Quite a bit later, I had more to say about dummy variables versus control state in [78].
Dummy variables were more than just an ugly hack to avoid control variables. They also allowed you to capture history. Adding history variables makes it possible to introduce behavioral reasoning into an assertional proof. (In the limit, you can add a variable that captures the entire history and clothe a completely behavioral proof in an assertional framework.) What a program does next depends on its current state, not on its history. Therefore, a proof that is based on a history variable doesn't capture the real reason why a program works. I've always found that proofs that don't use history variables teach you more about the algorithm. (As shown in [92], history variables may be necessary if the correctness conditions themselves are in terms of history.)
When we developed our methods, Owicki and I and most everyone else thought that the Owicki-Gries method was a great improvement over Ashcroft's method because it used the program text to decompose the proof. I've since come to realize that this was a mistake. It's better to write a global invariant. Writing the invariant as an annotation allows you to hide some of the explicit dependence of the invariant on the control state. However, even if you're writing your algorithm as a program, more often than not, writing the invariant as an annotation rather than a single global invariant makes things more complicated. But even worse, an annotation gets you thinking in terms of separate assertions rather than in terms of a single global invariant. And it's the global invariant that's important. Ashcroft got it right. Owicki and Gries and I just messed things up. It took me quite a while to figure this out.
Sometime during the '80s, Jay Misra noticed that the definition
of well-foundedness (Definition 8 on page 136) is obviously incorrect.
The origin of this paper was the note The Maintenance of Duplicate Databases by Paul Johnson and Bob Thomas. I believe their note introduced the idea of using message timestamps in a distributed algorithm. I happen to have a solid, visceral understanding of special relativity (see [5]). This enabled me to grasp immediately the essence of what they were trying to do. Special relativity teaches us that there is no invariant total ordering of events in space-time; different observers can disagree about which of two events happened first. There is only a partial order in which an event e1 precedes an event e2 iff e1 can causally affect e2. I realized that the essence of Johnson and Thomas's algorithm was the use of timestamps to provide a total ordering of events that was consistent with the causal order. This realization may have been brilliant. Having realized it, everything else was trivial. Because Thomas and Johnson didn't understand exactly what they were doing, they didn't get the algorithm quite right; their algorithm permitted anomalous behavior that essentially violated causality. I quickly wrote a short note pointing this out and correcting the algorithm.
It didn't take me long to realize that an algorithm for totally ordering events could be used to implement any distributed system. A distributed system can be described as a particular sequential state machine that is implemented with a network of processors. The ability to totally order the input requests leads immediately to an algorithm to implement an arbitrary state machine by a network of processors, and hence to implement any distributed system. So, I wrote this paper, which is about how to implement an arbitrary distributed state machine. As an illustration, I used the simplest example of a distributed system I could think of--a distributed mutual exclusion algorithm.
This is my most often cited paper. Many computer scientists claim to have read it. But I have rarely encountered anyone who was aware that the paper said anything about state machines. People seem to think that it is about either the causality relation on events in a distributed system, or the distributed mutual exclusion problem. People have insisted that there is nothing about state machines in the paper. I've even had to go back and reread it to convince myself that I really did remember what I had written.
The paper describes the synchronization of logical clocks. As something of an afterthought, I decided to see what kind of synchronization it provided for real-time clocks. So, I included a theorem about real-time synchronization. I was rather surprised by how difficult the proof turned out to be. This was an indication of what lay ahead in [62].
This paper won the 2000 PODC Influential Paper Award (later
renamed the Edsger W. Dijkstra Prize in Distributed Computing).
It won an ACM SIGOPS Hall of Fame Award in 2007.
TECO stands for Text Editing and Correction. It was the command language for the TECO editor, and it was the underlying macro language on which the original version of Emacs was built. It was an obscure, low-level language whose goal was to perform powerful text editing operations with the minimum number of keystrokes. A programming language designed to make verification easy would be completely unlike TECO. The paper shows that you verify a TECO program the same way you verify a program written in a more conventional language.
The proof is perhaps also of some historical interest because it was an
early example of a proof of an interactive program--that is, one that
interacts with the user instead of just producing an answer. Thus,
correctness had to be asserted in terms of the sequence of input
actions. The paper generalizes the Floyd/Hoare method to deal with
the history of environment actions.
To my knowledge, this is the first published paper to discuss
arbitrary failures (later called Byzantine failures). It actually
considered malicious behavior, not using such behavior simply as a
metaphor for completely unpredictable failures. Its algorithm was the
inspiration for the digital signature algorithm of [41].
With its use of real-time, this paper presaged the ideas in
[55].
This paper gives an overview of the complete SIFT project, which included designing the hardware and software and formally verifying the system's correctness. It announces the results that appear in [41]. It also is a very early example of the basic specification and verification method I still advocate: writing a specification as a state-transition system and showing that each step of the lower-level specification either implements a step of the higher-level one or is a "stuttering" step that leaves the higher-level state unchanged. The paper doesn't mention the use of an invariant, but that was probably omitted to save space.
This paper was a group effort that I choreographed in a final frenzy
of activity to get the paper out in time for the issue's deadline. I
don't remember who wrote what, but the section on verification seems
to be my writing.
I received an early version of the paper from Dijkstra, and I made a couple of suggestions. Dijkstra incorporated them and, quite generously, added me to the list of authors. He submitted the paper to CACM. The next I heard about it was when I received a copy of a letter from Dijkstra to the editor withdrawing the paper. The letter said that someone had found an error in the algorithm, but gave no indication of what the error was. Since Dijkstra's proof was so convincing, I figured that it must be a trivial error that could easily be corrected.
I had fairly recently written [23]. So, I decided to write a proof using that proof method, thinking that I would then find and correct the error. In about 15 minutes, trying to write the proof led me to the error. To my surprise, it was a serious error.
I had a hunch that the algorithm could be fixed by changing the order in which two operations were performed. But I had no good reason to believe that would work. Indeed, I could see no simple informal argument to show that it worked. However, I decided to go ahead and try to write a formal correctness proof anyway. It took me about two days of solid work, but I constructed the proof. When I was through, I was convinced that the algorithm was now correct, but I had no intuitive understanding of why it worked.
In the meantime, Dijkstra figured out that the algorithm could be fixed by interchanging two other operations, and he wrote the same kind of behavioral proof as before. His fix produced an arguably more efficient algorithm than mine, so that's the version we used. I sketched an assertional proof of that algorithm. Given the evidence of the unreliability of his style of proof, I tried to get Dijkstra to agree to a rigorous assertional proof. He was unwilling to do that, though he did agree to make his proof somewhat more assertional and less operational. Here are his comments on that, written in July, 2000:
I, too, have always been most interested in showing that something could be done, rather than in finding a better algorithm for doing what was known to be possible. Perhaps that is why I have always been so impressed by the brilliance of Dijkstra's work on concurrent algorithms.There were, of course, two issues at hand: (A) a witness showing that the problem of on-the-fly garbage collection with fine-grained interleaving could be solved, and (B) how to reason effectively about such artifacts. I am also certain that at the time all of us were aware of the distinction between the two issues. I remember very well my excitement when we convinced ourselves that it could be done at all; emotionally it was very similar to my first solutions to the problem of self-stabilization. Those I published without proofs! It was probably a period in my life that issue (A) in general was still very much in the foreground of my mind: showing solutions to problems whose solvability was not obvious at all. It was more or less my style. I had done it (CACM, Sep. 1965) with the mutual exclusion.
David Gries later published an Owicki-Gries style proof of the algorithm that was essentially the same as the one I had sketched. He simplified things a bit by combining two atomic operations into one. He mentioned that in a footnote, but CACM failed to print the footnote. (However, they did print the footnote number in the text.)
The lesson I learned from this is that behavioral proofs are
unreliable and one should always use state-based reasoning for
concurrent algorithms--that is, reasoning based on invariance.
Like everyone else at the time, when I began studying concurrent algorithms, I reasoned about them behaviorally. Such reasoning typically involved arguments based on the order in which events occur. I discovered that proofs can be made simpler, more elegant, and more mathematical by reasoning about operations (which can be composed of multiple events) and two relations on them: precedes (denoted by a solid arrow) and can affect (denoted by a dashed arrow). Operation A precedes operation B if all the events of A precede all the events of B; and A can affect B if some event in A precedes some event in B. These relations obey some simple rules that can reduce behavioral reasoning to mathematical symbol pushing.
This paper introduced the method of reasoning with the two arrow relations and applied it to a variant of the bakery algorithm. In the spring of 1976 I spent a month working with Carel Scholten at the Philips Nat Lab in Eindhoven. Scholten was a colleague and friend of Dijkstra, and the three of us spent one afternoon a week working, talking, and drinking beer at Dijkstra's house. The algorithm emerged from one of those afternoons. I think I was its primary author, but as I mention in the paper, the beer and the passage of time made it impossible for me to be sure of who was responsible for what.
The solid and dashed arrow formalism provides very elegant proofs for tiny algorithms such as the bakery algorithm. But, like all behavioral reasoning, it is hard to make completely formal, and it collapses under the weight of a complex problem. You should use assertional methods to reason about complex algorithms. However, standard assertional reasoning requires that the algorithm be written in terms of its atomic operations. The only assertional approach to reasoning directly about nonatomic operations (without translating them into sequences of atomic operations) is the one in [86], which is not easy to use. The two-arrow formalism is still good for a small class of problems.
The formalism seems to have been almost completely ignored, even among
the theoretical concurrency community. I find this ironic. There is
a field of research known by the pretentious name of "true
concurrency". Its devotees eschew assertional methods that are based
on interleaving models because such models are not truly concurrent.
Instead, they favor formalisms based on modeling a system as a partial
ordering of events, which they feel is the only truly concurrent kind
of model. Yet, those formalisms assume that events are atomic and
indivisible. Atomic events don't overlap in time the way real
concurrent operations do. The two-arrow formalism is the only one I
know that is based on nonatomic operations and could therefore be
considered truly concurrent. But, as far as I know, the true
concurrency community has paid no attention to it.
(I think it's at the bottom right of page 650.)Whitfield Diffie and Martin E. Hellman. New Directions in Cryptography. IEEE Transactions on Information Theory IT-22, 6 (1976), 644-654.
In 1978, Michael Rabin published a paper titled Digitalized Signatures containing a more practical scheme for generating digital signatures of documents. (I don't remember what other digital signature algorithms had already been proposed.) However, his solution had some drawbacks that limited its utility. This report describes an improvement to Rabin's algorithm that eliminates those drawbacks.
I'm not sure why I never published this report. However, I think it
was because, after writing it, I realized that the algorithm could be
fairly easily derived directly from Rabin's algorithm. So, I didn't
feel that it added much to what Rabin had done. However, I've been
told that this paper is cited in the cryptography literature and is
considered significant, so perhaps I was wrong.
I realized that there are two types of temporal logic: the one Pnueli used I called linear time logic; the one most computer scientists seemed to find natural I called branching time. (These terms were used by temporal logicians, but they distinguished the two logics by the axioms they satisfied, while I described them in terms of different kinds of semantics.) Pnueli chose the right kind of logic--that is, the one that is most useful for expressing properties of concurrent systems. I wrote this paper to explain the two kinds of logic, and to advocate the use of linear-time logic. However, I figured that the paper wouldn't be publishable without some real theorems. So, I proved some simple results demonstrating that the two kinds of logic really are different.
I submitted the paper to the Evian Conference, a conference on
concurrency held in France to which it seems that everyone working in
the field went. I was told that my paper was rejected because they
accepted a paper by Pnueli on temporal logic, and they didn't feel
that such an obscure subject merited two papers. I then submitted the
paper to FOCS, where it was also rejected. I have very rarely
resubmitted a paper that has been rejected. Fortunately, I felt that
this paper should be published. It has become one of the most
frequently cited papers in the temporal-logic literature.
When I wrote this paper, I sent a copy to Tony Hoare thinking that he
would like it. He answered with a letter that said, approximately:
"I always thought that the generalization to concurrent programs
would have to look something like that; that's why I never did it."
(Unfortunately, I no longer have the letter.) At the time, I
dismissed his remark as the ramblings of an old fogey. I now think he
was right--though probably for different reasons than he does. As I
indicated in the discussion of [23], I think Ashcroft was
right; one should simply reason about a single global invariant, and
not do this kind of decomposition based on program structure.
I am often unfairly credited with inventing the Byzantine agreement problem. The problem was formulated by people working on SIFT (see [30]) before I arrived at SRI. I had already discovered the problem of Byzantine faults and written [29]. (I don't know if that was earlier than or concurrent with its discovery at SRI.) However, the people at SRI had a much simpler and more elegant statement of the problem than was present in [29].
The 4-processor solution presented in this paper and the general
impossibility result were obtained by Shostak; Pease invented the
3
My other contribution to this paper was getting it written. Writing is hard work, and without the threat of perishing, researchers outside academia generally do less publishing than their colleagues at universities. I wrote an initial draft, which displeased Shostak so much that he completely rewrote it to produce the final version.
Over the years, I often wondered whether the people who actually build airplanes know about the problem of Byzantine failures. In 1997, I received email from John Morgan who used to work at Boeing. He told me that he came across our work in 1986 and that, as a result, the people who build the passenger planes at Boeing are aware of the problem and design their systems accordingly. But, in the late 80s and early 90s, the people at Boeing working on military aircraft and on the space station, and the people at McDonnell-Douglas, did not understand the problem. I have no idea what Airbus knows or when they knew it.
This paper was awarded the 2005 Edsger W. Dijkstra Prize in
Distributed Computing.
On the trip back home to California, I got on an airplane at Laguardia
Airport in the morning with a snowstorm coming in. I got off the
airplane about eight hours later, still at Laguardia Airport, having
written this paper. I then sent it to Fischer for his comments. I
waited about a year and a half. By the time he finally decided that
he wasn't going to do any more work on the paper, subsequent work by
others had been published that superseded it.
There is a problem in distributed computing that is sometimes called the Chinese Generals Problem, in which two generals have to come to a common agreement on whether to attack or retreat, but can communicate only by sending messengers who might never arrive. I stole the idea of the generals and posed the problem in terms of a group of generals, some of whom may be traitors, who have to reach a common decision. I wanted to assign the generals a nationality that would not offend any readers. At the time, Albania was a completely closed society, and I felt it unlikely that there would be any Albanians around to object, so the original title of this paper was The Albanian Generals Problem. Jack Goldberg was smart enough to realize that there were Albanians in the world outside Albania, and Albania might not always be a black hole, so he suggested that I find another name. The obviously more appropriate Byzantine generals then occurred to me.
The main reason for writing this paper was to assign the new name to
the problem. But a new paper needed new results as well. I came up
with a simpler way to describe the general
3
In [23], I had introduced a method of proving eventuality properties of concurrent programs by drawing a lattice of predicates, where arrows from a predicate P to predicates Q1, ..., Qn mean that, if the program reaches a state satisfying P, it must thereafter reach a state satisfying one of the Qi. That method never seemed practical; formalizing an informal proof was too much work.
Pnueli's introduction of temporal logic allowed the predicates in the lattice to be replaced by arbitrary temporal formulas. This turned lattice proofs into a useful way of proving liveness properties. It permitted a straightforward formalization of a particularly style of writing the proofs. I still use this proof style to prove leads-to properties, though the proofs are formalized with TLA (see [103]). However, I no longer bother drawing pictures of the lattices. This paper also introduced at, in, and after predicates for describing program control.
It's customary to list authors alphabetically, unless one contributed significantly more than the other, but at the time, I was unaware of this custom. Here is Owicki's account of how the ordering of the authors was determined.
As I recall it, you raised the question of order, and I proposed alphabetical order. You declined--I think you expected the paper to be important and didn't think it would be fair to get first authorship on the basis of a static property of our names. On the night we finished the paper, we went out to dinner to celebrate, and you proposed that if the last digit of the bill was even (or maybe odd), my name would be first. And, indeed, that's the way it came out.
I have in my files a letter from David Harel, who was then an editor
of Information and Control, telling me that the paper was
accepted by the journal, after revision to satisfy some concerns of
the referees. I don't remember why I didn't submit a revised version.
I don't think I found the referees' requests unreasonable. It's
unlikely that I abandoned the paper because I had already developed
the method in [86], since that didn't appear as a SRC
research report until four years later. Perhaps I was just too busy.
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 [103]).
Schneider agreed with me that invariance was the central
concept in reasoning about concurrent programs. He was also an expert
on all the different flavors of message passing that had been
proposed. We demonstrated in this paper that the basic
approach of [40] worked just was well with CSP; and we
claimed (without proof) that it also worked in other "distributed"
languages. I found it particularly funny that we should be the ones
to give a Hoare logic to CSP, while Hoare was using essentially
behavioral methods to reason about CSP programs. I'm still waiting
for the laughter.
The paper contains one figure--copied directly from a
transparency--with an obviously bogus algorithm. I tried to recreate
an algorithm from memory and wrote complete nonsense. It's easy to
make such a mistake when drawing a transparency, and I probably didn't
bother to look at it when I prepared the paper. To my knowledge, it
is the only incorrect algorithm I have published.
A little research revealed that psychologists are totally unaware of the phenomenon. I found one paper in the psychology literature on the time taken by subjects to choose between two alternatives based on how nearly equal they were. The author's theoretical calculation yielded a formula with a singularity at zero, as there should be. He compared the experimental data with this theoretical curve, and the fit was perfect. He then drew, as the curve fitting the data, a bounded continuous graph. The singularity at zero was never mentioned in the paper.
I feel that the arbiter problem is important and should be made known to scientists outside the field of computing. So, in December of 1984 I wrote this paper. It describes the problem in its classical formulation as the problem of Buridan's ass--an ass that starves to death because it is placed equidistant between two bales of hay and has no reason to prefer one to the other. Philosophers have discussed Buridan's ass for centuries, but it apparently never occurred to any of them that the planet is not littered with dead asses only because the probability of the ass being in just the right spot is infinitesimal.
I wrote this paper for the general scientific community. I probably could have published it in some computer journal, but that wasn't the point. I submitted it first to Science. The four reviews ranged from "This well-written paper is of major philosophical importance" to "This may be an elaborate joke." One of the other reviews was more mildly positive, and the fourth said simply "My feeling is that it is rather superficial." The paper was rejected.
Some time later, I submitted the paper to Nature. I don't like the idea of sending the same paper to different journals hoping that someone will publish it, and I rarely resubmit a rejected paper elsewhere. So, I said in my submission letter that it had been rejected by Science. The editor read the paper and sent me some objections. I answered his objections, which were based on reasonable misunderstandings of the paper. In fact, they made me realize that I should explain things differently for a more general audience. He then replied with further objections of a similar nature. Throughout this exchange, I wasn't sure if he was taking the matter seriously or if he thought I was some sort of crank. So, after answering his next round of objections, I wrote that I would be happy to revise the paper in light of this discussion if he would then send it out for review, but that I didn't want to continue this private correspondence. The next letter I received was from another Nature editor saying that the first editor had been reassigned and that he was taking over my paper. He then raised some objections to the paper that were essentially the same as the ones raised initially by the first editor. At that point, I gave up in disgust.
I had no idea where to publish the paper, so I let it drop. In 2011, a reader, Thomas Ray, suggested submitting it to Foundations of Physics. I did, and it was accepted. For the published version, I added a concluding section mentioning some of the things that had happened in the 25 years since I wrote the original version and citing this entry as a source of information about the paper's history.
My problems in trying to publish this paper and [22] are part of a long tradition. According to one story I've heard (but haven't verified), someone at G. E. discovered the phenomenon in computer circuits in the early 60s, but was unable to convince his managers that there was a problem. He published a short note about it, for which he was fired. Charles Molnar, one of the pioneers in the study of the problem, reported the following in a lecture given on February 11, 1992, at HP Corporate Engineering in Palo Alto, California:
Another amusing example occurred in an article by Charles Seif titled Not Every Vote Counts that appeared on the op-ed page of the New York Times on 4 December 2008. Seif proposed that elections be decided by a coin toss if the voting is very close, thereby avoiding litigious disputes over the exact vote count. While the problem of counting votes is not exactly an instance of Buridan's Principle, the flaw in his scheme will be obvious to anyone familiar with the principle and the futile attempts to circumvent it. I submitted a letter to the Times explaining the problem and sent email to Seif, but I received no response.One reviewer made a marvelous comment in rejecting one of the early papers, saying that if this problem really existed it would be so important that everybody knowledgeable in the field would have to know about it, and "I'm an expert and I don't know about it, so therefore it must not exist."
The 3-bit algorithm described in this paper came about because of a visit by Michael Rabin. He is an advocate of probabilistic algorithms, and he claimed that a probabilistic solution to the mutual exclusion problem would be better than a deterministic one. I believe that it was during his brief visit that we came up with a probabilistic algorithm requiring just three bits of storage per processor. Probabilistic algorithms don't appeal to me. (This is a question of aesthetics, not practicality.) So later, I figured out how to remove the probability and turn it into a deterministic algorithm.
The first part of the paper covers the formalism for describing
nonatomic operations that I had been developing since the 70s, and
that is needed for a rigorous exposition of mutual exclusion. (See
the discussion of [70].)
Writing the proofs turned out to be much more difficult than I had expected (see [27]). I worked very hard to make them as short and easy to understand as I could. So, I was rather annoyed when a referee said that the proofs seemed to have been written quickly and could be simplified with a little effort. In my replies to the reviews, I referred to that referee as a "supercilious bastard". Some time later, Nancy Lynch confessed to being that referee. She had by then written her own proofs of clock synchronization and realized how hard they were.
Years later, John Rushby and his colleagues at SRI wrote mechanically
verified versions of my proofs. They found only a couple of minor
errors. I'm rather proud that, even before I knew how to write
reliable, structured proofs (see [102]), I was
sufficiently careful and disciplined to have gotten those proofs
essentially correct.
We generalized this work to handle arrays and pointers, and even cited
a later paper about this generalization. But, as has happened so often
when I write a paper that mentions a future one, the future paper
was never written.
In 2012, a reader noticed that the paper's reference list includes a
paper by Chandy and me titled On Partially-Ordered Event Models
of Distributed Computations, claiming it had been submitted for
publication. Several times I have made the mistake of referencing a
paper of mine "to appear" that never appeared. But I can't imagine
that I would have claimed that a nonexistent paper had been submitted for
publication. However, neither Chandy nor I have any memory of that
paper or the reference. My guess is that we inserted the reference
in a preliminary version when we expected to write and submit the
other paper, and then we forgot to remove it.
Meanwhile, I still haven't written the Great American Concurrency Book.Our primary mission was to gather information for Addison-Wesley "to publish a computer-based document processing system specifically designed for scientists and engineers, in both academic and professional environments." This system was to be part of a series of related products (software, manuals, books) and services (database, production). (La)TeX was a candidate to be at the core of that system. (I am quoting from the original business plan.) Fortunately, I did not listen to your doubt that anyone would buy the LaTeX manual, because more than a few hundred thousand people actually did. The exact number, of course, cannot accurately be determined, inasmuch as many people (not all friends and relatives) bought the book more than once, so heavily was it used.
With the discovery of the bakery algorithm (see [12]), I began considering the question of how two processes communicate. I came to the conclusion that asynchronous communication requires some object whose state can be changed by one process and observed by the other. We call such an object a register. This paper introduced three classes of registers. The weakest class with which arbitrary synchronization is possible is called safe. The next strongest is called regular and the strongest, generally assumed by algorithm writers, is called atomic.
I had obtained all the results presented here in the late 70s and had described them to a number of computer scientists. Nobody found them interesting, so I never wrote them up. Around 1984, I saw a paper by Jay Misra, motivated by VLSI, that was heading in the general direction of my results. It made me realize that, because VLSI had started people thinking about synchronization from a more physical perspective, they might now be interested in my results about registers. So, I wrote this paper. As with [61], the first part describes my formalism for describing systems with nonatomic operations. This time, people were interested--perhaps because it raised the enticing unsolved problem of implementing multi-reader and multi-writer atomic registers. It led to a brief flurry of atomic register papers.
Fred Schneider was the editor who processed this paper. He kept having trouble understanding the proof of my atomic register construction. After a couple of rounds of filling in the details of the steps that Schneider couldn't follow, I discovered that the algorithm was incorrect. Fortunately, I was able to fix the algorithm and write a proof that he, I, and, as far as I know, all subsequent readers did believe.
Some fifteen years later, Jerry James, a member of the
EECS department at the University of Kansas, discovered a small error
in Proposition 1 when formalizing the proofs with the PVS mechanical
verification system. He proved a corrected version of the proposition
and showed how that version could be used in place of the original
one. A pdf file containing a note by James describing the
error and its correction can be obtained by clicking here.
I find it remarkable that, 20 years after Dijkstra first posed the
mutual exclusion problem, no one had thought of trying to find
solutions that were fast in the absence of contention. This
illustrates why I like working in industry: the most interesting
theoretical problems come from implementing real systems.
A distributed system is one in which the failure of a computer you didn't even know existed can render your own computer unusable.
The people responsible for DEC's network systems were the Network and Communications group (NAC). Around 1987, NAC asked for my help in designing a network time service. I decided that there were two somewhat conflicting requirements for a time service: delivering the correct time, and keeping the clocks on different computers closely synchronized. This paper describes the algorithms I devised for doing both.
I withdrew the paper because Tim Mann observed that the properties I
proved about the algorithms were weaker than the ones needed to make
them interesting. The major problem is that the algorithms were
designed to guarantee both a bound epsilon on the
synchronization of each clock with a source of correct time and an
independent bound delta on the synchronization between
any two clocks that could be made much smaller than
epsilon. Mann observed that the bound I proved on
delta was not the strong one independent of
epsilon that I had intended to prove. We believe
that the algorithms do satisfy the necessary stronger properties, and
Mann and I began rewriting the paper with the stronger results. But
that paper is still only partly written and is unlikely ever to see
the light of day.
There were three proofs of the minimum spanning-tree algorithm presented at PODC that year: ours, one by Willem-Paul de Roever and his student Frank Stomp, and the third by Eli Gafni and his student Ching-Tsun Chou. Each paper used a different proof method. I thought that the best of the three was the one by Gafni and Chou--not because their proof method was better, but because they understood the algorithm better and used their understanding to simplify the proof. If they had tried to formalize their proof, it would have turned into a standard invariance proof. Indeed, Chou eventually wrote such a formal invariance proof in his doctoral thesis.
The Gallager, Humblet, and Spira algorithm is complicated and its
correctness is quite subtle. (Lynch tells me that, when she lectured
on its proof, Gallager had to ask her why it works in a certain case.)
There doesn't seem to be any substitute for a standard invariance
proof for this kind of algorithm. Decomposing the proof the way we
did seemed like a good idea at the time, but in fact, it just added
extra work. (See [125] for a further
discussion of this.)
The original version, which I no longer have, quoted all the sources cited in support of the "correct" answer, showing how all those experts in the field had no idea that the mutual exclusion problem had been solved. However, the editor of CACM took it upon himself to handle my submission personally. He insisted that all this material be deleted, along with the accompanying sarcasm. Although I didn't like this editorial bowdlerization, I didn't feel like fighting.
I was appalled at how this note finally appeared. I have never seen a
published article so effectively hidden from the reader. I defy
anyone to take that issue of CACM and find the note without
knowing the page number.
This paper was my first collaboration with Abadi. Here's my recollection of how it was written. I had a hunch that history and prophecy variables were all one needed. Abadi had recently joined SRC, and this seemed like a fine opportunity to interest him in the things I was working on. So I described my hunch to him and suggested that he look into proving it. He came back in a few weeks with the results described in the paper. My hunch was right, except that there were hypotheses needed that I hadn't suspected. Abadi, however, recalls my having had a clearer picture of the final theorem, and that we worked out some of the details together when writing the final proof.
I had just developed the structured proof style described in [102], so I insisted that we write our proofs in this style, which meant rewriting Abadi's original proofs. In the process, we discovered a number of minor errors in the proofs, but no errors in the results.
This paper won the LICS 1988 Test of Time Award (awarded in 2008).
Among the presentations at the workshop session on the
challenge problem, there were only two serious attempts at solving the
problem. (As an organizer, I felt that I shouldn't present my own
solution.) After a long period of review and revision, these two and
a third, subsequently-written solution, appeared in a special issue of
Distributed Computing. This note is a critique of the three
solutions that I wrote for the special issue.
My tiny example convinced me that we want to reason in TLA, not in LP. To do this, we need to translate a TLA proof into the language of the theorem prover. The user should write the proof in the hierarchical style of [102], and the prover should check each step. One of the advantages of this approach turned out to be that it allows separate translations for the action reasoning and temporal reasoning. This is important because about 95% of a proof consists of action reasoning, and these proofs are much simpler if done with a special translation than in the same translation that handles temporal formulas. (In action reasoning, x and x' are two completely separate variables; x' is handled no differently than the variable y.) So, I invited Urban Engberg and Peter Grønning, who were then graduate students in Denmark, to SRC for a year to design and implement such a system. The result of that effort is described in this paper. For his doctoral research, Engberg later developed the system into one he called TLP.
Georges Gonthier demonstrated how successful this system was in his mechanical verification of the concurrent garbage collector developed by Damien Doligez and hand-proved in his thesis. Gonthier estimated that using TLP instead of working directly in LP reduced the amount of time it took him to do the proof by about a factor of five. His proof is reported in:
TLP's input language was essentially a very restricted subset of TLA+ (described in [128])--a language that did not exist when TLP was implemented. I regarded TLP as a proof of concept and I did not use it after it was built. Around 2006, work began on a theorem prover for real TLA+ specifications. It led to TLAPS, the TLA+ proof system. TLAPS uses several back-end theorem provers, including Isabelle, Zenon, and SMT solvers.Georges Gonthier, Verifying the Safety of a Practical Concurrent Garbage Collector, in Rajeev Alur, Thomas A. Henzinger (Ed.): Computer Aided Verification, 8th International Conference, CAV '96. Lecture Notes in Computer Science, Vol. 1102, Springer, 1996, 462-465.
This is the second paper in which we used structured proofs, the first
being [92]. In this case, structured proofs were
essential to getting the results right. We found reasoning about
realizability to be quite tricky, and on several occasions we
convinced ourselves of incorrect results, finding the errors only by
trying to write structured proofs.
I cornered you after your invited address at CAV92. At CAV, you talked about indenting (and TLA, and its Larch support). I challenged you with a matter I had been thinking about since at least 1990, the year of the first CAV. In the preface to the CAV90 proceedings, I stated as a paramount challenge to the CAV community, to create a beneficial interface between automated theorem proving, and model checking.I asked you if you thought that linking TLA/Larch with S/R (which should be simple to do on account of their very close syntax and semantics for finite-state models), could be useful. I suggested the (artificial) problem of verifying a multiplier constructed from iterated stages of a very complex 8x8 multiplier. The 8x8 multiplier would be too complex to verify handily with a theorem prover. A (say) 64x64 multiplier could be built from the 8x8 one. We'd use the model checker (cospan) to verify the 8x8, and Larch/TLA to verify the induction step. You liked the idea, and we did it, you working with Urban and I working with Mark [Foissoitte].
Sadly, with the interface in place, I was unable to come up with a non-artificial feasible application. To this day, although there have been a succession of such interfaces built (I believe ours was the first), none has really demonstrated a benefit on a real application. The (revised) challenge is to find an application in which the combination finds a bug faster than either one could by itself.
The correctness conditions given in the problem statement included an
ad hoc set of rules about how long the gas could be on if the
flame was off. The purpose of those conditions was obviously to
prevent a dangerous build-up of unburned gas. To demonstrate the
power of TLA+, and because it made the problem more fun,
I wrote a higher-level requirement stating that the concentration of
gas should be less than a certain value. Assuming that the
dissipation of unburned gas satisfied a simple differential equation,
I proved that their conditions implied my higher-level
specification--under suitable assumptions about the rate of diffusion
of the gas. This required, among other things, formally specifying
the Riemann integral, which took about 15 lines. I also sketched a
proof of the correctness of the next implementation level. All of
this was done completely in TLA+. The introduction to the
volume says that I
"extend[ed] ... TLA+ with explicit variables
that denote continuous states and clocks."
That, of course, is nonsense. Apparently, by their logic, you have
extended C if you write a C program with variables named time
and flame instead of t and f.
I first presented these ideas in a talk at a celebration of the 60th
birthday of Richard Palais, my de jure thesis advisor,
collaborator, and friend. I was invited along with all of Palais'
former doctoral students, and I was the only non-mathematician who
gave a talk. (I believe all the other talks presented that day appear
among the articles in the volume edited by Uhlenbeck.) Lots of people
jumped on me for trying to take the fun out of mathematics. The
strength of their reaction indicates that I hit a nerve. Perhaps they
really do think it's fun having to recreate the proofs themselves if
they want to know whether a theorem in a published paper is actually
correct, and to have to struggle to figure out why a particular step
in the proof is supposed to hold. I republished the paper in the
AMM Monthly so it would reach a larger audience of
mathematicians. Maybe I should republish it again for computer
scientists.
The moral of TLA is: if you're not writing a program, don't use a programming language. Programming languages are complicated and have many ugly properties because a program is input to a compiler that must generate reasonably efficient code. If you're describing an algorithm, not writing an actual program, you shouldn't burden yourselves with those complications and ugly properties. The toy concurrent programming languages with which computer scientists have traditionally described algorithms are not as bad as real programming languages, but they are still uglier and more complicated than they need to be. Such a toy program is no closer to a real C or Java program than is a TLA formula. And the TLA formula is a lot easier to deal with mathematically than is a toy program. (Everything I say about programming languages applies just as well to hardware description languages. However, hardware designers are generally more sensible than to try to use low-level hardware languages for higher-level system descriptions.) Had I only realized this 20 years ago!
The first major step in getting beyond traditional programming languages to describe concurrent algorithms was Misra and Chandy's Unity. Unity simply eliminated the control state, so you just had a single global state that you reasoned about with a single invariant. You can structure the invariant any way you want; you're not restricted by the particular programming constructs with which the algorithm is described. The next step was TLA, which eliminated the programming language and allowed you to write your algorithm directly in mathematics. This provides a much more powerful and flexible way of describing the next-state relation.
An amusing footnote to this paper is that, after reading an earlier
draft, Simon Lam claimed that he deserved credit for the idea of
describing actions as formulas with primed and unprimed variables. A
similar notation for writing postconditions dates from the 70s, but
that's not the same as actually specifying the action in this way. I
had credited Rick Hehner's 1984 CACM article, but I figured
there were probably earlier instances. After a modest amount of
investigation, I found one earlier published use--in [50].
TLA assumes an underlying logic for writing actions. The next step was obvious: devise a language for specifying concurrent systems that extends Z with the operators of TLA. Equally obvious was the name of such a language: TLZ.
In the Spring of 1991, I visited Oxford and gave a talk on TLA, pointing out how naturally it could be combined with Z. The idea was as popular as bacon and eggs at Yeshiva University. Tony Hoare was at Oxford, and concurrency at Oxford meant CSP. The Z community was interested only in combining Z with CSP--which is about as natural as combining predicate logic with C++.
A couple of years later, I was invited to give a talk at the Z User's Meeting. I dusted off the TLZ idea and presented it at the meeting. Again, I encountered a resounding lack of interest.
Had TLA been adopted by the Z community, it might have become a lot
more popular. On the other hand, not being attached to Z meant that I
didn't have to live with Z's drawbacks and was free to design a more
elegant language for specifying actions. The result was
TLA+, described in [128].
The paper uses as an example a mutual exclusion protocol due to Michael Fischer. This example has an amusing history. When I was working on [73], I sent Fischer email describing my algorithm and asking if he knew of a better solution. He respondedFor me, this paper was partly a vindication of some work I had done with [Gordon] Plotkin [A Logical View of Composition, Theoretical Computer Science 114, 1 (June 1993), 3-30], where we explored the definition and properties of the "while" operator (-|>). I believe that you thought that the work was a formal game, so I was pleased to find that we could use it in this paper.
He followed this with a simple, elegant protocol based on real-time delays. Because of its real-time assumptions, his protocol didn't solve the problem that motivated [73]. I mentioned this algorithm in [73], but had forgotten about it by the time of de Roever's workshop. Fred Schneider reminded me of it when he used it as an example in his talk at the workshop. We then incorporated the example in our paper. I later mentioned this to Fischer, who had no memory of the protocol and even claimed that it wasn't his. Fortunately, I happen to have saved his original email, so I had the proof. The message, complete with message number, is cited in the paper--the only instance of such a citation that I know of.No, I don't, but the practical version of the problem sounds very similar to the problem of bus allocation in contention networks. I wonder if similar solutions couldn't be used? For example, how about...
The proofs in this paper are in an appendix that was published
by ACM only online. It is on their web site, but in a separate file
from that containing the paper. The link above is to a version of the
paper containing the appendix.
However, there were few computer scientists capable of doing this straightforward engineering exercise. Stephan Merz was one of them. So, I asked him to write the proof, which he did with his usual elegance and attention to detail. I think I provided most of the prose and the initial version of the TLA specification, which Merz modified a bit. The proof was all Merz's.We formally specify a well known solution to the Byzantine generals problem and give a rigorous, hierarchically structured proof of its correctness. We demonstrate that this is an engineering exercise, requiring no new scientific ideas.
This paper contains two major theorems, one for decomposing closed-system specifications and another for composing open-system specifications. A preliminary conference version of the result for closed systems appeared in [104]. A preliminary conference version of the second appeared in [105].
Although the propositions and theorems in this paper are not in principle difficult, it was rather hard to get the details right. We couldn't have done it without writing careful, structured proofs. So, I wanted those proofs published. But rigorous structured proofs, in which all the details are worked out, are long and boring, and the referees didn't read them. Since the referees hadn't read the proofs, the editor didn't want to publish them. Instead, she wanted simply to publish the paper without proofs. I was appalled that she was willing to publish theorems whose proofs hadn't been checked, but was unwilling to publish the unchecked proofs. But, I sympathized with her reluctance to kill all those trees, so we agreed that she would find someone to referee the proof and we would publish the appendix electronically. The referee read the proofs carefully and found three minor errors, which were easily corrected. Two of the errors occurred when we made changes to one part of the proof without making corresponding changes to another. The third was a careless mistake in a low-level statement. When asked, the referee said that the hierarchical structure, with all the low-level details worked out, made the proofs quite clear and easy to check.
Almost all the proofs in this paper are in an appendix that was published
by ACM only online. It is on their web site, but in a separate file
from that containing the paper. The link above is to a version of the
paper containing the appendix.
Not wanting to be outdone, I wrote this paper to show that you can write TLA specifications by drawing pictures. It describes how to interpret as TLA formulas the typical circles and arrows with which people describe state transitions. These diagrams represent safety properties. I could also have added some baroque conventions for adding liveness properties to the pictures, but there's a limit to how silly I will get. When I wrote the paper, I actually did think that pictures might be useful for explaining parts of specifications. But I have yet to encounter any real example where they would have helped.
This paper contains, to my knowledge, the only incorrect "theorem" I
have ever published. It illustrates that I can be as lazy as anyone
in not bothering to check "obvious" assertions. I didn't published
a correction because the theorem, which requires an additional
hypothesis, was essentially a footnote and didn't affect the main
point of the paper. Also, I was curious to see if anyone would notice
the error. Apparently, no one did. I discovered the error in
writing [116]
There is an interesting footnote to this workshop. As explained in
the discussion of [50], I don't believe in writing
specifications as a conjunction of the properties that the system
should satisfy. Several participants used this approach. I thought
that the high-level specification was sufficiently trivial that by
now, people would be able to specify it in this way. However, Reino
Kurki-Suonio noticed an error that was present in all the "purely
axiomatic" specifications--that is, ones that mentioned only the
interface, without introducing internal variables.
This is the only example I've encountered in which the pictures of TLA
formulas described in [114] were of some use. In
fact, I discovered the error in [114] when I
realized that one of the pictures in this paper provided a
counterexample to its incorrect theorem.
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.
I thought, and still think, that Paxos is an important algorithm. Inspired by my success at popularizing the consensus problem by describing it with Byzantine generals, I decided to cast the algorithm in terms of a parliament on an ancient Greek island. Leo Guibas suggested the name Paxos for the island. I gave the Greek legislators the names of computer scientists working in the field, transliterated with Guibas's help into a bogus Greek dialect. (Peter Ladkin suggested the title.) Writing about a lost civilization allowed me to eliminate uninteresting details and indicate generalizations by saying that some details of the parliamentary protocol had been lost. To carry the image further, I gave a few lectures in the persona of an Indiana-Jones-style archaeologist, replete with Stetson hat and hip flask.
My attempt at inserting some humor into the subject was a dismal failure. People who attended my lecture remembered Indiana Jones, but not the algorithm. People reading the paper apparently got so distracted by the Greek parable that they didn't understand the algorithm. Among the people I sent the paper to, and who claimed to have read it, were Nancy Lynch, Vassos Hadzilacos, and Phil Bernstein. A couple of months later I emailed them the following question:
None of them noticed any connection between this question and the Paxos algorithm.Can you implement a distributed database that can tolerate the failure of any number of its processes (possibly all of them) without losing consistency, and that will resume normal behavior when more than half the processes are again working properly?
I submitted the paper to TOCS in 1990. All three referees said that the paper was mildly interesting, though not very important, but that all the Paxos stuff had to be removed. I was quite annoyed at how humorless everyone working in the field seemed to be, so I did nothing with the paper. A number of years later, a couple of people at SRC needed algorithms for distributed systems they were building, and Paxos provided just what they needed. I gave them the paper to read and they had no problem with it. Here is Chandu Thekkath's account of the history of Paxos at SRC.
So, I thought that maybe the time had come to try publishing it again.When Ed Lee and I were working on Petal we needed some sort of commit protocol to make sure global operations in the distributed system completed correctly in the presence of server failures. We knew about 3PC and studied a description of it in Bernstein, Hadzilacos, and Goodman's book Concurrency Control and Recovery in Database Systems. We found the protocol a bit difficult to understand and therefore abandoned our attempts at implementing it. At around this time, Mike Schroeder told us about a protocol for consensus that Leslie Lamport had invented and suggested we ask him about it. Leslie gave Ed a copy of the Part-Time Parliament tech report, which we both enjoyed reading. I particularly liked its humour and to this day, cannot understand why people don't like that tech report. Paxos had all the necessary properties we wanted for our system and we figured we could implement it. Leslie provided essential consulting help as well, which resulted in the first implementation of the Paxos algorithm (including dynamic reconfiguration) as far as I am aware. A year later, when we needed a distributed lock server for the Frangipani file system we used Paxos again.
Meanwhile, the one exception in this dismal tale was Butler Lampson, who immediately understood the algorithm's significance. He mentioned it in lectures and in a paper, and he interested Nancy Lynch in it. De Prisco, Lynch, and Lampson published their version of a specification and proof. Their papers made it more obvious that it was time for me to publish my paper. So, I proposed to Ken Birman, who was then the editor of TOCS, that he publish it. He suggested revising it, perhaps adding a TLA specification of the algorithm. But rereading the paper convinced me that the description and proof of the algorithm, while not what I would write today, was precise and rigorous enough. Admittedly, the paper needed revision to take into account the work that had been published in the intervening years. As a way of both carrying on the joke and saving myself work, I suggested that instead of my writing a revision, it be published as a recently rediscovered manuscript, with annotations by Keith Marzullo. Marzullo was willing, Birman agreed, and the paper finally appeared.
There was an amusing typesetting footnote to this. To set off Marzullo's annotations, I decided that they should be printed on a gray background. ACM had recently acquired some wonderful new typesetting software, and TOCS was not accepting camera-ready copy. Unfortunately, their wonderful new software could not do shading. So, I had to provide camera-ready copy for the shaded text. Moreover, their brilliant software could accept this copy only in floating figures, so Marzullo's annotations don't appear quite where they should. Furthermore, their undoubtedly expensive software wasn't up to typesetting serious math. (After all, it's a computing journal, so why should they have to typeset formulas?) Therefore, I had to provide the camera-ready copy for the definitions of the invariants in section A2, which they inserted as Figure 3 in the published version. So, the fonts in that figure don't match those in the rest of the paper.
This paper won an ACM SIGOPS Hall of Fame Award in 2012.
Meanwhile, Ernie Cohen had been working on reduction using
Kleene algebra, obtaining elegant proofs of nice, general results for
safety properties. I showed him the TLA version and my preliminary
results on liveness, and we decided to collaborate. This paper is the
result. We translated his more general results for safety into TLA
and obtained new results for liveness properties. The paper promises
a complete proof and a more general result in a later paper. The
result exists, but the later paper is unlikely ever to appear.
A draft of the complete proof is available
as a
Postscript,
compressed Postscript, or
pdf file.
I have long felt that this whole approach is rather silly. You don't design a mutual exclusion algorithm by first designing the individual processes and then hoping that putting them together guarantees mutual exclusion. Similarly, anyone who has tried to deduce mutual exclusion from properties proved by considering the processes in isolation knows that it's the wrong way to approach the problem. You prove mutual exclusion by finding a global invariant, and then showing that each process's actions maintains the invariant. TLA makes the entire reasoning process completely mathematical--the specifications about which one reasons are mathematical formulas, and proving correctness means proving a single mathematical formula. A mathematical proof is essentially decompositional: you apply a deduction rule to reduce the problem of proving a formula to that of proving one or more simpler formulas.
This paper explains why traditional compositional
reasoning is just one particular, highly constrained way of
decomposing the proof. In most cases, it's not a very natural way and
results in extra work. This extra work is justified if it can
be done by a computer. In particular, decomposition along processes
makes sense if the individual processes are simple enough to be
verified by model checking. TLA is particularly good for doing
this because, as illustrated by [120],
it allows a great deal of flexibility in choosing what constitutes
a process.
People sometimes argue that possibility properties are important by using the ambiguities of natural language to try to turn a liveness property into a possibility property. For example, they may say that it should be possible for the user of a bank's ATM to withdraw money from his account. However, upon closer examination, you don't just want this to be possible. (It's possible for me to withdraw money from an ATM, even without having an account, if a medium-sized meteorite hits it.) The real condition is that, if the user presses the right sequence of buttons, then he must receive the money.
Since there is no reason to prove possibility properties of a system, I was surprised to learn from Bob Kurshan--a very reasonable person--that he regularly uses his model checker to verify possibility properties. Talking to him, I realized that although verifying possibility properties tells you nothing interesting about a system, it can tell you something interesting about a specification, which is a mathematical model of the system. For example, you don't need to specify that a user can hit a button on the ATM, because you're specifying the ATM, not the user. However, we don't reason about a user interacting with the ATM; we reason about a mathematical model of the user and the ATM. If, in that mathematical model, it were impossible for the button to be pushed, then the model would be wrong. Proving possibility properties can provide sanity checks on the specification. So, I wrote this paper explaining how you can use TLA to prove possibility properties of a specification--even though a linear-time temporal logic like TLA cannot express the notion of possibility.
I originally submitted this paper to a different journal.
However, the editor insisted that, to publish the paper, I had to add
a discussion about the merits of branching-time versus linear-time
logic. I strongly believe that it's the job of an editor to judge the
paper that the author wrote, not to get him to write the paper that
the editor wants him to. So, I appealed to the editor-in-chief.
After receiving no reply for several months, I withdrew the paper and
submitted it to TCS.
It was a lovely idea that required no infrastructure and
anyone could just use it. Unfortunately, vandals soon invaded the Web
and, with the intellectual sophistication of people who deface
street signs, they put such a string on lots of other web pages.
Fortunately, web search engines have gotten better and web pages can
simply be given descriptive titles.
Gafni devised the initial version of the algorithm, which didn't look much like Paxos. As we worked out the details, it evolved into its current form. Gafni wanted a paper on the algorithm to follow the path with which the algorithm had been developed, starting from his basic idea and deriving the final version by a series of transformations. We wrote the first version of the paper in this way. However, when trying to make it rigorous, I found that the transformation steps weren't as simple as they had appeared. I found the resulting paper unsatisfactory, but we submitted it anyway to PODC'99, where it was rejected. Gafni was then willing to let me do it my way, and I turned the paper into its current form.
A couple of years after the paper was published, Mauro J. Jaskelioff
encoded the proof in Isabelle/HOL and mechanically checked it. He
found about a dozen small errors. Since I have been proposing Disk
Paxos as a test example for mechanical verification of concurrent
algorithms, I have decided not to update the paper to correct the
errors he found. Anyone who writes a rigorous mechanically-checked
proof will find them.
I sent it to Idit Keidar who told me that the bounds I derived were already known, so I forgot about it. About a year later, she mentioned that she had cited the note in:We derive lower bounds on the number of messages and the number of message delays required by a nonblocking fault-tolerant consensus algorithm, and we show that variants of the Paxos algorithm achieve those bounds.
I then asked why they had cited my note if the results were already known. She replied,Idit Keidar and Sergio Rajsbaum. On the Cost of Fault-Tolerant Consensus When There Are No Faults - A Tutorial. MIT Technical Report MIT-LCS-TR-821, May 24 2001. Preliminary version in SIGACT News 32(2), Distributed Computing column, pages 45-63, June 2001 (published in May 15th).
There are a few results in the literature that are similar, but not identical, because they consider slightly different models or problems. This is a source of confusion for many people. Sergio and I wrote this tutorial in order to pull the different known results together. Hopefully, it can help clarify things up.
There was one detail of the protocol that struck me as particularly
subtle. I had the idea of publishing an incorrect version of the
specification with that detail omitted as a challenge problem for the
verification community. I did that and put it
on
the Web in June, 2000. To further disseminate the problem, we
wrote this description of it for the CAV (Computer Aided Verification)
conference.
In 2015, Michael Deardeuff of Amazon informed me that one
sentence in this paper is ambiguous, and interpreting it the wrong way
leads to an incorrect algorithm. Deardeuff found
that a number of Paxos implementations on Github implemented
this incorrect algorithm. Apparently, the implementors did not bother
to read the precise description of the algorithm in
[123].
I am not going to remove this ambiguity or reveal where it is. Prose
is not the way to precisely describe algorithms.
Do not try to implement the algorithm
from this paper. Use [123] instead.
In Petri nets, arbitration appears explicitly as conflict. A class of Petri nets called marked graphs, which were studied in the early 70s by Anatol Holt and Fred Commoner, are the largest class of Petri nets that are syntactically conflict-free. Marked-graph synchronization is a natural generalization of producer/consumer synchronization. It was clear to me that marked-graph synchronization can be implemented without an arbiter, though I never bothered writing down the precise algorithm. I assumed that marked graphs describe precisely the class of synchronization problems that could be solved without an arbiter.
That marked-graph synchronization can be implemented without an arbiter is undoubtedly obvious to people like Anatol Holt and Chuck Seitz, who are familiar with multiprocess synchronization, Petri nets, and the arbiter problem. However, such people are a dying breed. So, I thought I should write up this result before it was lost. I had been procrastinating on this for years when I was invited to submit an article for a special issue of Distributed Computing celebrating the 20th anniversary of the PODC conference. The editors wanted me to pontificate for a few pages on the past and future of distributed computing--something I had no desire to do. However, it occurred to me that it would be fitting to contribute some unpublished 25-year-old work. So, I decided to write about arbiter-free synchronization.
Writing the paper required me to figure out the precise arbiter-free implementation of marked graphs, which wasn't hard. It also required me to prove my assumption that marked graphs were all one could implement without an arbiter. When I tried, I realized that my assumption was wrong. There are multiprocess synchronization problems not describable by marked graphs that can be solved without an arbiter. The problem was more complicated than I had realized.
I wish I knew exactly what can be done without an arbiter, but I
don't. It turns out that I don't really understand arbiter-free
synchronization. Lack of understanding leads to messy exposition. I
understand the results about the equivalence of registers, and I have
nice, crisp ways of formalizing and proving these results. But the
other results in the paper are a mess. They're complicated and I
don't have a good way of formalizing them. Had I written this
twenty-five years ago, I would probably have kept working on the
problem before publishing anything. But I don't have the time I once
did for mulling over hard problems. I decided it was better to
publish the results I have, even though they're messy, and hope that
someone else will figure out how to do a better job.
I then looked for applications of consensus in which there is a single special proposer whose proposed value needs to be chosen quickly. I realized there is a "killer app"--namely, distributed transaction commit. Instead of regarding transaction commit as one consensus problem that chooses the single value commit or abort, it could be presented as a set of separate consensus problems, each choosing the commit/abort desire of a single participant. Each participant then becomes the special proposer for one of the consensus problems. This led to what I call the Paxos Commit algorithm. It is a fault-tolerant (non-blocking) commit algorithm that I believed had fewer message delays in the normal (failure-free) case than any previous algorithm. I later learned that an algorithm published by Guerraoui, Larrea, and Schiper in 1996 had the same normal-case behavior.
Several months later, Jim Gray and I got together to try to understand
the relation between Paxos and the traditional Two-Phase Commit
protocol. After a couple of hours of head scratching, we figured out
that Two-Phase Commit is the trivial version of Paxos Commit that
tolerates zero faults. That realization and several months of
procrastination led to this paper, which describes the Two-Phase
Commit and Paxos Commit algorithms and compares them. It also
includes an appendix with TLA+ specifications of the
transaction-commit problem and of the two algorithms.
References [4] and [5] are no longer at the URLs given in the reference
list. Reference [5] no longer seems to be on the Web. Reference [4]
seems to be the document now available
here.
However, that paper seems to be a revised version of the one on which
we based our formal spec, and it could have been influenced by our spec.
It then occurred to me that, in the state-machine approach (introduced in [27]), such conflicting proposals arise because two different commands are issued concurrently by two clients, and both are proposed as command number i. This conflict is necessary only if the two proposed commands do not commute. If they do, then there is no need to order them. This led me to a new kind of agreement problem that requires dynamically changing agreement on a growing partially ordered set of commands. I realized that generalizing from partially ordered sets of commands to a new mathematical structure I call a c-struct leads to a generalized consensus problem that covers both ordinary consensus and this new dynamic agreement problem. I also realized that Fast Paxos can be generalized to solve this new problem. I wrote up these results in March 2004. However, I was in the embarrassing position of having written a paper generalizing Fast Paxos without having written a paper about Fast Paxos. So, I just let the paper sit on my disk.
I was invited to give a keynote address at the 2004 DSN conference, and I decided to talk about fast and generalized Paxos. Fernando Pedone came up after my talk and introduced himself. He said that he and André Schiper had already published a paper with the same generalization from the command sequences of the state-machine approach to partially ordered sets of commands, together with an algorithm that achieved the same optimal number of message delays in the absence of conflict. It turns out that their algorithm is different from the generalized Paxos algorithm. There are cases in which generalized Paxos takes only 2 message delays while their algorithm takes 3. But the difference in efficiency between the two algorithms is insignificant. The important difference is that generalized Paxos is more elegant.
I've been sitting on this paper for so long because it doesn't seem
right to publish a paper on a generalization of Fast Paxos before
publishing something about Fast Paxos itself. Since generalized Paxos
is a generalization, this paper also explains Fast Paxos. But
people's minds don't work that way. They need to understand Fast
Paxos before they can really understand its generalization. So, I
figured I would turn this paper into the second part of a long paper
or monograph whose first part explains Fast Paxos. However, in recent
years I've been discovering new Paxonian results faster than I can
write them up. It therefore seems silly not to release a paper that
I've already written about one of those results. So, I added a brief
discussion of the Pedone-Schiper result and a citation to
[154] and am posting the paper here. Now that I have
written the Fast Paxos paper and submitted it for publication, I may
rewrite this paper as part two of that one.
Since you can't publish a new paper about an old idea, no matter how good the idea may be, I needed to find something new to add. The TLC model checker provided the opportunity I needed. The method described in [107] and [145] is good for specifying and reasoning about real-time systems, but it produces specifications that TLC can't handle. TLC works only with the simpler approach, so I had an excuse for a new paper.
There's a naive approach for checking real-time specifications with TLC that I had thought for a while about trying. It involves checking the specification for all runs up to some maximum time value that one hopes is large enough to find any bugs. So I did that using as examples two versions of Fischer's mutual exclusion protocol, which is mentioned in the discussion of [107].
One possible reason to use a special real-time approach is for model checking. I figured that model checkers using special algorithms for real time should do much better than this naive approach, so I wanted some justification for using TLA+ and TLC instead. Looking through the literature, I found that all the real-time model checkers seemed to use low-level languages that could describe only simple controllers. So I added the example of a distributed algorithm that they couldn't represent. Then I discovered that, since the papers describing it had been published, the Uppaal model checker had been enhanced with new language features that enabled it to model this algorithm. This left me no choice but to compare TLC with Uppaal on the example.
I asked Kim Larsen of Aalborg University, the developer of Uppaal, for help writing an Uppaal spec of the algorithm. Although I really did this because I'm lazy, I could justify my request because I had never used Uppaal and couldn't see how to write a nice model with it. Larsen got his colleague Arne Skou to write a model that was quite nice, though it did require a bit of a "hack" to encode the high-level constructs of TLA+ in Uppaal's lower-level language. Skou was helped by Larsen and his colleague, Gerd Behrmann. As I expected, Uppaal was much faster than TLC--except in one puzzling case in which Uppaal ran out of memory.
I put the paper aside for a while. When I got back to it, I realized that there's a simple way of using TLC to do complete checking of these real-time specifications that is much faster than what I had been doing. The idea is so simple that I figured it was well known, and I kicked myself for not seeing it right away. I checked with Tom Henzinger, who informed me that the method was known, but it had apparently not been published. It seems to be an idea that is obvious to the experts and unknown to others. So this provided another incentive for publishing my paper, with a new section on how to use an explicit-time model checker like TLC to check real-time specs. Henzinger also corrected a basic misunderstanding I had about real-time model checkers. Rather than trying to be faster, most of them try to be better by using continuous time. He wrote:
I was then inspired to do some more serious data gathering. I discovered the explanation of that puzzling case: Uppaal runs out of memory when the ratio of two parameters becomes too large. The results reported in the paper show that neither TLC nor Uppaal comes out clearly better on this example.If you are happy with discrete time, I doubt you can do any better [than my naive approach]. Uppaal, Kronos etc. deal with real-numbered time, and therefore rely on elaborate and expensive clock region constructions.
The Uppaal distribution comes with a model of a version of Fischer's algorithm, and I decided to get some data for that example too. Uppaal did clearly better than TLC on it. However, I suspected that the reason was not because real-time model checkers are better, but because TLC is less efficient for this kind of simple algorithm than a model checker that uses a lower-level language. So I got data for two ordinary model checkers that use lower-level languages, Spin and SMV. I was again lazy and got the developers of those model checkers, Gerard Holzmann and Ken McMillan, to do all the work of writing and checking the models.
I submitted this paper to the journal Formal Methods in Systems
Design. I thought that the part about model checking was interesting
enough to be worth putting into a separate conference paper. I
therefore wrote [158], which was accepted at the 2005
Charme conference. However, the journal submission was rejected
because it didn't contain enough new ideas.
An earlier version was rejected from POPL 2007. Based on the reviews
I received and comments from Simon Peyton-Jones, I revised the paper
and submitted it to TOPLAS, but it was again rejected. It may be
possible to write a paper about PlusCal that would be considered
publishable by the programming-language community. However, such a
paper is not the one I want to write. For example, two of the three
TOPLAS reviewers wanted the paper to contain a formal
semantics--something that I would expect people interested in using
PlusCal to find quite boring. (A formal TLA+ specification of the
semantics is available on the Web.) I therefore decided to publish it
as an invited paper in the ICTAC conference proceedings.
Because the example is so simple and involves no concurrency, its
TLA+ specification is neither interesting nor
enlightening. However, my comments about the specification process
may be of some interest.
By around 1980, I knew that the producer/consumer algorithm introduced
in [23] should generalize to an arbitrary marked graph,
but I never thought it important enough to bother working out the
details. (Marked graphs, which specify dataflow computation, are
described in the discussion of [142].) I realized
that these new barrier synchronization algorithms should also be
instances of that generalization. The fact that the barrier
algorithms worked well on a real multiprocessor made the general
algorithm seem more interesting. Further thought revealed that the
good performance of these barrier algorithms was not an accident.
They have optimal caching behavior, and that optimal behavior can be
achieved in the general case. All this makes the general
synchronization algorithm relevant for the coming generation of
multicore processor chips.
This paper was rejected by the 2008 PODC conference. Idit Keidar
invited us to submit it as a tutorial to her distributed computing
column in SIGACT News.
The development
of
TLAPS, the TLA+ proof system,
inspired me to write formal TLA+ specifications of the
two algorithms and a TLAPS-checked proof that the Castro-Liskov
algorithm refines ordinary Paxos. This paper describes the results.
The complete specifications and proof are
available
here.
My experience preparing and giving the talk made me realize it was
time for a new paper on the subject. This paper is built around a
simple example--a lemma from Michael Spivak's calculus text. I tried
to show how a mathematician can easily transform the proofs she now
writes into structured proofs. The paper also briefly describes how
formal structured proofs are written in TLA+, and an
appendix contains a machine-checked proof of Spivak's lemma. While
mathematicians will not write formal proofs in the
foreseeable future, I argue that learning how to write them is a good
way to learn how to write rigorous informal proofs.
(x = y) => (x' = y')
is a tautology if it were to treat priming
( ' ) as an ordinary
mathematical operator. We call this kind of hiding
coalescing.
This paper shows that coalescing is somewhat more subtle than one
might think, and explains how to do it correctly in some important
cases.
A 2015 paper by Martín Abadi introducing a method for making prophecy variables easier to use inspired me to take a new look at them. I came up with a completely new kind of prophecy variable--one that I find quite easy to use. I believe that Abadi and I did not discover this kind of variable in 1988 because I had not yet invented TLA+, so we were thinking only in terms of states and not in terms of actions (predicates on pairs of states). After I had the initial idea, I asked Stephan Merz to work with me to get the details right.
This paper is written for engineers. It contains a TLA+ module for each type of auxiliary variable and shows how to use operators defined in that module to add such an auxiliary variable to a specification. These modules, along with the modules for all the examples in the paper, are available on the Web.
There are three types of auxiliary variables, each with its own module. In addition to history variables that record the past and prophecy variables that predict the future, there are stuttering variables that add stuttering steps (steps that do nothing). Paper [92] used prophecy variables to add stuttering steps, but we have long known that it's better to use a separate kind of variable for that purpose.
The auxiliary variables described in the paper can be defined
semantically; they are not specific to the TLA+ language.
We hope in a later paper to define them in a language-independent
fashion, and to prove a completeness result similar to that of paper
[92]. We believe that the new kind of prophecy
variable is more powerful than the original one, and that completeness
does not require the hypothesis of finite internal nondeterminism
needed for the original prophecy variables.
A system specification can be written as a TLA formula that is true just on possible executions of the system. When listening to Schneider's talk, it occurred to me that for a hyperproperty depending on only a finite number of executions, the assertion that a system satisfies the hyperproperty can can be written as a TLA formula containing multiple copies of the system's specification.
Schneider and I spent part of the following two years figuring out how to make the idea work and writing this paper about it. We found that TLA and the TLA+ tools can in principle check if high-level system designs satisfy all the security hyperproperties we saw in the literature. However, TLA had to be used in a new way that was not needed for verifying ordinary properties. This paper won the USA National Security Agency's 2022 Annual Best Scientific Cybersecurity Paper Competition.
TLA+ files (and their pretty-printed versions) containing
the examples in the paper and their verifications are available
here.
These are mutual exclusion algorithms. A version of the paper
containing an appendix proving that an algorithm which generalizes the
starting point satisfies mutual exclusion is available
here.
While the data proves nothing, it does strongly suggest that there are lots of errors in published mathematics paper. Since the frequency of such errors is an interesting topic, and this very short paper (less than one page in a journal format) presents the only data on this topic, I think that it's worth publishing.
The reasons for rejection given by the editors and reviewers seemed
reasonable. However, the reaction to my proposals in
[102] and [179] for writing proofs
taught me that mathematicians become irrational when I point out that
the proofs they write are not the paradigms of logical rigor they
pretend them to be. So, I am suspicious. I will let the reader
decide whether this paper should have been rejected.