Distributing automata for asynchronous networks of processors

Abstract

Our objective is to prove that a given parallelization algorithm is correct, that is, that the behavior of the initial centralized program is equivalent to the behavior of the final parallel program.

Our parallelization algorithm is intended for distributed memory machines, where parallel programs communicate through a networks of FIFO channels. This algorithm has been applied to sequential imperative programs as well as synchronous programs. In both cases, the source program is given as a finite deterministic automaton labeled with actions. The behavior of the centralized program is the language of this automaton, i.e., the set of finite and infinite traces of actions it generates. Finally, the parallelization specifications are given as a partition of the set of actions into as many subsets as there are processors in the distributed memory machine.

We define a commutation relation between actions according to the data dependencies. This commutation relation induces a rewriting relation over traces of actions. The set of all possible rewritings is the set of all admissible behaviors of the centralized program according to the commutation relation. The problem is that this set cannot, in general, be recognized by a finite automaton. The intuition behind our proof is that this set is identical to the set of linear extensions of some partial order. For this reason we introduce a new model based on partial orders, that we call order automaton.

First, we build a centralized order automaton by turning each action labeling the initial automaton into a partial order capturing the data dependencies between this action and the remaining ones. The language of our order automaton is the set of finite and infinite traces of partial orders it generates. By defining a concatenation relation between partial orders, each trace is then itself a partial order! Thus the language of our order automaton is a set of finite and infinite partial orders. We show that the set of linear extensions of all these partial orders is identical to the set of all admissible behaviors of the centralized program according to the commutation relation.

Second, we show that our order automaton can be transformed into a set of parallel automata by turning the data dependencies between actions belonging to distinct processors into communication actions, and by projecting the resulting automaton onto each processor. These transformations are shown to preserve the behavior of our order automaton.

BibTeX entry

@Article{CCGJ97,
  author = 	 {B. Caillaud and P. Caspi and A. Girault and C. Jard},
  title = 	 {Distributing Automata for Asynchronous Networks of
                  Processors},
  journal = 	 {European Journal of Automation (RAIRO-APII-JESA)},
  year = 	 {1997},
  volume =       {31},
  number =       {3},
  pages =        {503--524}
}