A formalism for specifying and reasoning about concurrent systems is described. Unlike
more conventional formalisms, it is not based upon atomic actions. A definition of what it
means for one system to implement a higher-level system is given and justified. In Part II, the
formalism is used to specify several classes of interprocess communication mechanisms
and to prove the correctness of algorithms for implementing them.