Distributing automata for asynchronous networks of processors

Résumé

Notre but est de prouver qu'un algorithme de parallélisation donné est correct, c'est-à-dire que le comportement du programme centralisé initial est équivalent au comportement du programme réparti final.

Notre algorithme de parallélisation est destiné aux machines à mémoire distribuée, où les programmes parallèles communiquent à travers des réseaux des cannaux FIFO. Cet algorithme a été appliqué à des programmes séquentiel impératifs ainsi qu'à des programmes synchrones. Dans les deux cas, le programme source est fourni sous la forme d'un automate fini déterministe étiqueté avec des actions. Le comportement du programme centralisé est le langage généré par l'automate, c'est-à-dire l'ensemble des traces finies ou infinies d'actions qu'il engendre. Enfin, les directives de répartition sont données sous la forme d'une partition de l'ensemble des actions en autant de sous-ensembles qu'il y a de processeurs dans la machine à mémoire distribuée cible.

Nous définissons une relation de commutation entre les actions, correspondant aux dépendances de données. Cette relation de commutation induit une relation de réécriture sur les traces d'actions. L'ensemble de toutes les réécritures possibles est l'ensemble des comportements admissibles du programme centralisé correspondant à la relation de commutation. Le problème est que cet ensemble ne peut pas, en général, être reconnu par un automate fini. L'intuition de notre preuve est que cet ensemble est identique à l'ensemble des extensions linéaires d'un certain ordre partiel. C'est pourquoi nous introduisons un nouveau model basé sur les ordres partiels, que nous appelons automate d'ordres.

Premièrement nous construisons un automate d'ordres centralisé en transformant chaque action étiquetant l'automate initial en un ordre partiel représentant les dépendances de données entre l'action de cette étiquette et les autres actions. Le langage généré par notre automate d'ordres est l'ensemble des traces d'ordres partiels finies ou infinies qu'il engendre. En définissant une relation de concaténation sur les ordres partiels, chaque trace est à son tour un ordre partiel ! Ainsi le langage généré par notre automate d'ordre est un ensemble d'ordres partiels finis ou infinis. Nous montrons que l'ensemble des extensions linéaires de tous ces ordres partiels est identique à l'ensemble des comportements admissibles du programme centralisé initial.

Deuxièmement nous montrons que notre automate d'ordres peut être transformé en un ensemble d'automates parallèles en transformant les dépendances de données entre actions appartenant à des processeurs disctincts en actions de communication, et en projettant l'automate résultant sur chaque processeur. Nous prouvons que ces transformations préservent le comportement de notre automate d'ordres.

Entrée BibTeX

@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}
}