Abstract FR:

Nous étudions une propriété de correction de programmes écrit dans un sous-ensemble de fortran étendu avec des constructions parallèles empruntées à un projet de norme ANSI. Le modèle de parallélisme est asynchrone et a mémoire partagée. La propriété est une équivalence entre le programme parallèle étudie et sa version séquentielle. Sous certaines hypothèses, nous prouvons que cette propriété résulte de la préservation des dépendances, définies sur la version séquentielle, par le flot de contrôle et les synchronisations. La condition essentielle de préservation est une relation d'implication entre la formule de dépendance et une formule de précédence. Celle-ci est définie à partir d'un graphe d'instances d'instructions qui représente la réunion de la relation de précédence due au contrôle et d'une relation de précédence induite par le mécanisme d'attente résultant de l'exécution des instructions de synchronisation. Nous passons, par projection, du graphe d'instances, infini, a un graphe d'instructions, fini, équivalent dont les arcs sont étiquetés par des formules d'arithmétique du premier ordre. Pour faciliter le calcul des précédences, nous introduisons un graphe de blocs d'un nouveau type. À l'intérieur d'un bloc la précédence est seulement due au contrôle. En considérant des chemins de longueur fini, dans ce graphe, entre la source et la cible de la dépendance, nous parvenons à exprimer des approximations de la formule de précédence. Dans le cas où les expressions du programme sont linéaires, un algorithme tente de prouver que la formule de correction, qui est alors une formule de pressurer, est une tautologie. Il est fait appel pour la réduction des systèmes au test oméga conçu à l'université du maryland. L’algorithme manipule des systèmes d'équations et d'inéquations sous forme symbolique. Il ne fournit pas seulement un résultat binaire (oui/non), mais un ensemble réduit de contraintes qui peut être interprète comme une condition de validité à respecter.