Communication and parallelism introduction and elimination in imperative concurrent programs

Transformation rules of imperative concurrent programs, based on congruence and refinement relations between statements, are presented. They introduce and/or eliminate synchronous communication statements and parallelism in these programs. The development is made within a subset of SPL, a good representative of imperative notations for concurrent and reactive programs introduced by Manna and Pnueli. The paper shows that no finite set of transformation rules suffices to eliminate synchronous communication statements from programs involving the concatenation and parallelism operators only. An infinite set is given to suit this purpose, which can be applied recursively. As an important complement for the applications, a collection of tactics, for the acceleration of broader transformations, is described. Tactics apply a sequence of rules to a program witha specific transformation objective. The transformation rules and the tactics could be used in formal design to derive new programs from verified ones, preserving their properties, and avoiding the repetition of verifications for the transformed programs. As an example, the formal parallelization of a non-trivial distributed fast Fourier transform algorithm is outlined.