Principe des Méthodes de Preuve de Propriétés d'Invariance et de Fatalité des Programmes Parallèles.
(Principle of invariance and inevitability proof methods of concurrent programs.)
In « Parallélisme, communication et synchronisation », J.-P. Verjus et G. Roucairol (Eds.), Éditions du CNRS, Paris, pp. 129—149, 1985, ISBN 2-222-03672-0.
:
Les programmes, en particulier parallèles, doivent faire l'objet
d'analyses avant d'être considérés comme valides. Nous
nous intéressons à des analyses qualitatives qui consistent
à comparer les comportements possibles d'un programme
parallèle à une spécification des comportements
souhaitables. Dans ce rapport, nous ne traitons que des méthodes de
preuve. Dans un but simplificateur, nous supposons résolus les
problèmes de description d'un programme parallèle, de ses
comportements possibles et de sa spécification. Nous utiliserons
donc des modèles simples mais très généraux des
programmes (représentés par une relation de transition sur
des états), de leurs comportements (définis par des ensembles
de traces complètes) et de leur spécification (à
l'aide de propriétés d'invariance et de fatalité).
Reste notre problème d'intérêt, à savoir
l'étude des méthodes de preuve permettant de démontrer
qu'un programme parallèle se comporte conformément à
une spécification. Dans ce rapport, nous nous limiterons au cas des
méthodes de Floyd (dite des assertions invariantes) et de Burstall
(dites des assertions intermittentes) et à quelques-unes de leurs
généralisations.
Nous essayons tout d'abord d'exprimer l'essence d'une méthode de preuve à l'aide de principes d'induction. Quand c'est fait, nous en déduisons la correction et la complétude sémantique. Nous cherchons ensuite l'équivalence forte c'est-à-dire qu'une preuve par une méthode peut se réécrire en une preuve par une autre méthode. Nous nous efforçons également de généraliser ces principes d'induction, en particulier au cas de comportement à des ensembles de traces non clos. C'est le cas des hypothèses d'exécution faiblement équitables pour les programmes parallèles que nous prenons en exemple dans ce rapport. Finalement, nous étudions comment adapter une méthode de preuve à un langage particulier en partant d'une sémantique opérationnelle de ce langage et d'un principe d'induction formalisant la méthode de preuve.
:
Programs, in particular parallel ones, must be carefully analyzed before being
considered as valid. We are interested in qualitative analyzes, which
consist in comparing the possible behaviors of parallel programs to a
specification of their desired behaviors. For short we assume that the
problems of describing a parallel program, of describing its possible
behaviors and of describing its specification are solved. We will therefore use very
simple but general models of programs (represented as a relation on
states), of their behaviors (defined as sets of complete/maximal traces)
and of their specification (using safety/invariance and inevitability/liveness properties). Our
remaining problem of interest, is to study proff methods for proving that a
concurrent program behaves according to a specification. In this paper, we
will limit ourselves to the case of Floyd's method (so called
“Invariant assertions”) and of Burstall's method (so called
“Intermittent assertions”) and to a few of their
generalizations.
We first try to express the essence of a proof method by an induction principle. Once done, we derive the soundness and relative completeness of the proof method. We then look for strong equivalence results in order to show that a proof by one method can be rewritten into a proof by another method. We also try to generalize these induction principles, in particular to the case of non closed sets of traces. This is the case of the weak fairness hypotheses on parallel program execution that we consider as the basic example in this paper. Finally, we study how to adapt a proof method to a particular language starting from an operational semantics of this language and from an induction principle formalizing the proof method.
\bibitem{CousotCousot85-ATP-CNRS-PCS}
P{.} Cousot and R{.} Cousot.
\newblock Principe des M{\'e}thodes de Preuve de Propri{\'e}t{\'e}s
d'Invariance et de Fatalit{\'e} des programmes Parall{\`e}les.
\newblock In \emph{Parall{\'e}lisme, communication et synchronisation},
J.-P{.} Verjus et G{.} Roucairol (Eds.), {\'E}ditions du CNRS,
Paris, pp{.} 129--149, 1985, ISBN 2-222-03672-0.
@inproceedings{CousotCousot85-ATP-CNRS-PCS,
author = {Cousot, P{.} and Cousot, R{.}},
title = {Principe des M{\'e}thodes de Preuve de Propri{\'e}t{\'e}s
d'Invariance et de Fatalit{\'e} des programmes Parall{\`e}les},
booktitle = {Parall{\'e}lisme, communication et synchronisation},
editor = {J.-P{.} Verjus and G{.} Roucairol },
publisher = {{\'E}ditions du CNRS, Paris},
pages = {129--149},
year = {1985, ISBN 2-222-03672-0},
}
)
\bibitem{CousotR-TheseEtat-1985}
R. Cousot.
\newblock Fon\-de\-ments des m{\'e}\-tho\-des de preu\-ve d'in\-va\-rian\-ce et de
fa\-ta\-li\-t{\'e} de pro\-gramm\-es pa\-ral\-l{\`e}\-les (in {F}rench).
\newblock Th{\`e}\-se d'{{\'E}}tat {\`e}s sci\-en\-ces ma\-th{\'e}\-ma\-ti\-ques,
Ins\-ti\-tut Na\-tio\-nal Po\-ly\-tech\-ni\-que de Lor\-rai\-ne, Nan\-cy,
Fran\-ce, 15 November 1985.