Synchronous Message Passing and Semaphores: An Equivalence Proof