An exercise in proving parallel programs correct
David Gries · Communications of the ACM · 1977
A parallel program, Dijkstra's on-the-fly garbage collector, is proved correct using a proof method developed by Owicki.The fine degree of interleaving in this program makes it especially difficult to understand, and complicates the proof greatly.Difficulties with proving such parallel programs correct are discussed.