Critique of the Lake Arrowhead Three

For a number of years, I was a member of a committee that planned an annual workshop at Lake Arrowhead, in southern California. I was finally pressured into organizing a workshop myself. I got Brent Hailpern to be chairman of a workshop on specification and verification of concurrent systems. A large part of the conference was devoted to a challenge problem of specifying sequential consistency. This was a problem that, at the time, I found difficult. (I later learned how to write the simple, elegant specification that appears in [126].)

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.