Communication and parallelism introduction and elimination in imperative concurrent programs

Miquel Bertran, Francesc Babot, August Climent, Miquel Nicolau

Producció científica: Article en revista indexadaArticleAvaluat per experts

4 Cites (Scopus)


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.

Idioma originalAnglès
Pàgines (de-a)20-39
Nombre de pàgines20
RevistaLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Estat de la publicacióPublicada - 2001


Navegar pels temes de recerca de 'Communication and parallelism introduction and elimination in imperative concurrent programs'. Junts formen un fingerprint únic.

Com citar-ho