Formal communication elimination and sequentialization equivalence proofs for distributed system models

Equivalence reasoning with distributed system models, expressed directly as imperative programs with explicit parallelism, communication operations, storage variables and boolean conditions, remains virtually unexplored. Only reasoning with models expressed as process algebras has been amply dealt with in literature. However, these formalisms do not contemplate either storage variables or Boolean conditions as fundamental items, although these items become essential in most situations. This article develops the foundation of the until now non existent theory of equivalence reasoning with the aforementioned imperative notation and two novel equivalence proof techniques: communication elimination and sequentialization. The development is grounded on state systems and transition interleavings, as treated by Manna and Pnueli. Equivalence proofs safely transform a model via the application of a sequence of equivalence laws; aiming to obtain an equivalent model which is purely sequential, free from internal communication operations and parallelism, as a simplification of the initial model. After this, verification of the original model can be carried out, indirectly, in the simplified model, thus reducing complexity. Some of the presented novel notions are: (1) modular procedure for decomposition of both models and proofs, (2) interface behavior for statement semantics, (3) interface equivalence between behaviors, between statements and between procedures, (4) a set of communication elimination laws and (5) substitution rules of procedure references by their bodies or by references to equivalent procedures. An elimination proof construction algorithm is also presented; when it terminates, deadlock freedom of the original model can be decided. The main design lines of a computer aided equivalence reasoning tool are outlined as well. This is the foundation for a more widely applicable tool. As an illustration, the sequentialization proof of a simplified pipelined processor is overviewed. It is modeled as a distributed system with procedures and two levels of parallelism. The model obtained at the end of the equivalence proof is the sequential loop of a Von Neumann processor. This result establishes that the original model is deadlock-free, behaves as a processor and, as a consequence, the partition of processor functions among parallel processes is correct. The ratio of the upper bounds on the number of states of the final over the initial models, final/initials, is 1/2⁶⁷².