An Input/Output Semantics for Distributed Program Equivalence Reasoning

A new notion of input/output equivalence of distributed imperative programs, with synchronous communications, is introduced. It preserves the input/output relation, encompassing both, initial/final state and communication channel values. For its mathematical justification, the semantic framework of Manna and Pnueli, based on finite transition systems and reduced behaviors, is extended with the notion of input/output behavior. A set of laws for the equivalence is overviewed. A deduction rule for the substitution of references to input/output equivalent procedures is defined and justified in the new semantics. The rule is applied to decompose distributed program simplification proofs, introduced in a prior work, which use the laws to establish the equivalence between a sequential and a parallel communicating program. They include communication elimination as one of their steps. An outline of one of such proofs, for a pipelined processor model, is included.