This paper was inspired by Kourosh Gharachorloo’s thesis. The problem he addressed was how to execute a multiprocess program on a computer whose memory did not provide sequential consistency (see ), but instead required explicit synchronization operations (such as Alpha’s memory barrier instruction). He presented a method for deducing what synchronization operations had to be added to a program. I realized that, if one proved the correctness of an algorithm using the two-arrow formalism of , the proof would tell you what synchronization operations were necessary. This paper explains how.