Formal derivation of an algorithm for distributed phase synchronization

The main purpose of this paper is to create more evidence for the observation that parallel programs, distributed or not, can be formally — and economically — derived by means of just the predicate calculus and the theory of Owicki and Gries. The example selected here is the problem of phase synchronization, in which a number of programs each pass through an unlimited number of phases in a more or less synchronous fashion. A solution is developed for the special case of programs located in the nodes of a tree with communication facilities restricted to communication with neighbouring nodes.