How to make a correct multiprocess program execute correctly on a multiprocessor
Leslie Lamport · IEEE Transactions on Computers · 1997
A multiprocess program executing on a modern multiprocessor must issue explicit commands to synchronize memory accesses. A method is proposed for deriving the necessary commands from a correctness proof of the underlying algorithm in a formalism based on temporal relations among operation executions.