Synchronization of Concurrent Processes without Globality Assumptions

The mathematically precise definition of a simple notation for designing and Implementing programs involving synchronization of parallel processes introduced by C.A.R. Hoare in (2) and (3) Is expressed in the COSY formalism. The latter formalism not only generalizes the semantic trace model used by Hoare but also reduces the complexity of the formalism for representing concurrency and simplifies the proofs of correctness carried out in the model. A number of versions of Hoare’s examples are developed and absence of partial or total system deadlock is demonstrated.