Implementation of a synchronous communication primitive in a loosely coupled system: a correctness proof