I first wrote about rely/guarantee reasoning in the early 80s! Since then, a lot of developments have been made but the basic ideas (that "interference" is the essence of concurrency; if one wants a compositional approach to design, one must record assumptions about interference; and that granularity is a delicate issue) have become widely accepted. More recently, I have been developing ideas about "atomicity refinement"; see "R/G thinking" as wider than any specific set of rules; realised that expressive weakness is a key to success; and appreciated the role of data reification in achieving complex R/G specifications. I'd like to review in this talk my reservations about "ghost variables" and to try to pin down where they are really required.
