Reasoning About Nonatomic Operations

From the time I discovered the bakery algorithm (see [12]), I was fascinated by the problem of reasoning about a concurrent program without having to break it into indivisible atomic actions. In [33], I described how to do this for behavioral reasoning. But I realized that assertional reasoning, as described in [23], was the only proof method that could scale to more complex problems. This paper was my first attempt at assertional reasoning about nonatomic operations. It introduces the win (weakest invariant) operator that later appeared in [86], but using the notation of Pratt’s dynamic logic rather than Dijkstra’s predicate transformers.

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.