The geometry of conservative programs
Géométrie des programmes conservatifs
Résumé
The programs we consider are written in a restricted form of the language introduced by Dijkstra (1968). A program is said to be conservative when each of its loops restores all the resources it consumes. We define the geometric model of such a program and prove that the collection of directed paths on it is a reasonable overapproximation of its set of execution traces. In particular, two directed paths that are close enough with respect to the uniform distance result in the same action on the memory states of the system. The same holds for weakly dihomotopic directed paths. As a by-product, we obtain a notion of independence which is favourably compared to more common ones. The geometric models actually belong to a handy class of local pospaces whose elements are called isothetic regions. The local pospaces we use differ from the original ones, we carefully explain why the alternative notion should be preferred. The title intentionally echoes the article by Carson and Reynolds Jr. (1987).
Les programmes auxquels on s'intéresse font partie d'un fragment du langage introduit par Dijkstra dans «Cooperating Sequential Processes» (1968). Un programme est dit conservatif lorsque chacune de ses boucles restaure les ressources qu'elle a utilisées. On construit le modèle géométrique d'un tel programme et on montre que la collection de ses chemins dirigés est une sur-approximation raisonnable de l'ensemble des traces d'exécution du programme. En particulier, deux chemins dirigés proches au regard de la norme uniforme produisent le même effet sur l'état mémoire du système. Le résultat est en valable pour deux chemins dirigés faiblement dihomotopes. Au passage, on introduit une notion d'indépendance qui se compare favorablement à deux autres, plus communes. Les modèles géométriques appartiennent a une classe d'espaces localement ordonnés particulièrement pratique, dont les éléments sont appelés régions isothétiques. Les espaces localement ordonnés auxquels nous avons recours diffèrent des originaux, nous expliquons avec soin pourquoi nous préférons la version alternative. Le titre fait intentionnellement écho à l'article «The Geometry of Semaphore Programs» de Carson et Raynolds (1987).
Origine : Fichiers produits par l'(les) auteur(s)