Liens transverses ENS de Lyon

Agenda de l'ENS de Lyon

Unique solution techniques for processes and functions

Date
jeu 11 juin 2020
Horaires

14H00

Lieu(x)
Intervenant(s)

Soutenance de thèse de M. Adrien DURIER du LIP, sous la direction de M. Daniel HIRSCHKOFF et, sous la cotutelle de M. Davide SANGIORGI de L'Université de Bologne

Langue(s) des interventions

Description générale

Cette thèse se place dans la tradition de l’étude de la théorie mathématique des langages de programmation, et plus précisément  du développement  de l’outillage sémantique pour leur étude. Afin  de définir la sémantique d’un langage formel, une méthode éprouvée est la construction d’une équivalence comportementale  : une telle équivalence permet d’identi- fier des programmes  ayant le même comportement (c’est-à-dire qu’ils produisent les mêmes résultats, qu’ils accomplissent les mêmes communications, etc), et ce même  si ce sont des programmes qui parviennent à ce résultat (ou à ces communications, dans le cas d’un langage concurrent) d’une manière tout à fait distincte.
Étudier de telles équivalences comportementales  permet d’abstraire la syntaxe des lan- gages, pour en extirper le contenu significatif, sémantique. Cependant, la concrétisation de cette opération par la preuve de l’équivalence de deux programmes peut être, dans certain cas, d’une extrême difficulté. Ainsi, si la définition de telles équivalences est aujourd’hui une question largement explorée et résolue, leur utilisation en pratique pose problème.
C’est pourquoi il  est courant  de faire appel à un outillage de techniques de preuves, permettant de faciliter la preuve que deux programmes ont bien le même comportement. De ce point de vue, la bisimilarité [Mil89] est une équivalence comportementale  notable, car elle est définie par une telle technique de preuve : la méthode de la bisimulation, à qui elle doit dans une large mesure son succès – d’autant que cette méthode constitue aussi une technique de preuve pour d’autres équivalences. En effet, la bisimilarité est une équivalence plus fine que la plupart  des autres équivalences  considérées en pratique : pour montrer que deux programmes sont  équivalents, il suffit souvent  de montrer qu’ils sont  bisimilaires (lorsque c’est possible). Les méthodes inspirées de la bisimilarité sont aujourd’hui utilisées dans de nombreux domaines de l’informatique, dans la théorie des automates par exemple [BP13, BP15], ou encore, en pratique, dans la certification du compilateur CompCert [Ler].
Cette méthode est d’autant plus robuste qu’elle a été au fur et à mesure enrichie de di- verses améliorations,  dont entre autres les techniques dites « modulo » [Mil89, San98, PS11] (« up to » en anglais). Si la théorie de ces améliorations constitue un sujet d’étude à part entière, elle a également  été comparée par Sangiorgi [San15] à la technique d’unicité  des solutions des équations. Plus précisément,  Sangiorgi établit  une correspondance entre les techniques « modulo contextes » et la technique d’unicité des solutions.  Cette technique propose d’utiliser une équation récursive entre programmes, dotée de la propriété d’unicité des solutions, caractérisant les équations dont tous les programmes qui sont solutions sont aussi équivalents  entre eux (pour une équivalence comportementale  donnée – ici, la bisimi- larité). Pour prouver que deux programmes sont équivalents, il suffit alors de prouver qu’ils sont chacun solution de ladite équation ; la preuve d’équivalence  nécessaire pour le justifier étant souvent plus simple qu’une preuve d’équivalence directe entre les deux programmes.

Toute équation n’admet pas l’unicité des solutions : ainsi, l’équation X = X  admet tout programme comme solution. Pour utiliser une telle technique, il est donc vital de caractériser les équations admettant  l’unicité  des solutions, en proposant  un ensemble de conditions suffisantes pour le garantir. Milner, dans son ouvrage pionnier sur la concurrence [Mil89], dans lequel il définit la bisimilarité, les techniques modulo, et les techniques d’unicité des solutions, donne un tel critère, qui s’appuie sur la notion syntaxique de « garde » : une équation est gardée si une opération doit nécessairement se produire avant toute récursion, c’est-à-dire avant  que la variable d’équation n’apparaisse. Ainsi, l’équation X  = X  n’est pas gardée, mais pour une opération op, garantissant une forme de précédence, l’équation X  = op(X ) le serait. Cependant le critère proposé par Milner est contraignant, en ce qu’il interdit également toute forme de concurrence dans l’équation considérée. Cela est dû au fait que l’on considère des équivalences comportementales  faibles : c’est-à-dire que l’on abstrait le programme du nombre de ses étapes  de calcul internes (ou un protocole concurrent du nombre de synchronisations internes). considérant  uniquement  les opérations « visibles ». Or, dans ce cadre, le critère syntaxique habituel de garde ne garantit pas que des opérations visibles doivent  se produire avant  qu’apparaisse la variable récursive. Il est  intéressant  de constater que les techniques modulo également souffrent de limitations dans le cadre d’une équivalence faible, pour des raisons similaires.
Le langage CSP, proposé par Hoare [Hoa85], et dont  on considère généralement  une sémantique dénotationnel le, c’est-à-dire une sémantique mathématique abstraite, possède également une théorie de la récursion et d’unicité des solutions. En particulier, si les critères de Hoare sont  soumis aux mêmes limitations  que les critères de Milner,  Roscoe  [Ros92, Ros97] propose une garantie bien plus flexible pour garantir l’unicité des solutions  pour une équivalence faible, reposant sur le concept de divergence : un programme diverge s’il a la possibilité de procéder à un nombre infini d’opérations internes, impossibles à constater pour un observateur extérieur.

Gratuit
Mots clés
Disciplines