À la Une

Soutenance de thèse Dimitri Racordon

DR_400.jpg  

M. Dimitri Racordon soutiendra en anglais, en vue de l'obtention du grade de docteur ès sciences mention informatique de la Faculté des sciences de l'Université de Genève, sa thèse intitulée:

Revisiting Memory Assignment Semantics in Imperative Programming Languages

Date: Mardi 3 septembre 2019 à 10h00

Lieu: CUI / Battelle bâtiment A, salle de cours 316-318 (2ème étage)

 

Jury:

  • Prof. Didier Buchs (Directeur, Université de Genève)
  • Prof. James Noble (Victoria University of Wellington)
  • Dr Elias Castegren (KTH Royal Institute of Technology)
  • Dr Steve Hostettler (Université de Genève, Wolters Kluwer)
 

Résumé:

Les langages de programmation sont devenus un outil indispensable, non seulement pour les professionnels de l’informatique, mais aussi pour les scientifiques et ingénieurs d’autres disciplines. Ainsi, dans le but de faciliter leur utilisation, les langages de programmation offrent désormais de nombreuses abstractions visant à masquer les subtilités liées à la représentation des données et à la gestion de la mémoire. La continuelle croissance de la puissance de calcul a rendu cette évolution possible, permettant aux compilateurs et interprètes de supporter des fonctionnalités autrefois jugées irréalistes, telles que la récupération automatique de mémoire ou encore l’inférence de type. Si ces améliorations ont indubitablement contribué à rendre le code plus facile à écrire et plus clair à lire, des reliques du modèle sous-jacent transparaissent toujours dans la sémantique de la plupart des languages, lesquelles peuvent conduire à des comportements mal compris. En particulier, la relation entre valeurs et variables se révèle être une prolifique source de confusion. Alors que ces deux notions sont fréquemment perçues comme interchangeables, une valeur est en fait un object sémantique vivant dans la mémoire tandis qu’une variable est un outil syntaxique pour interagir avec. De plus, ces concepts ne sont pas nécessairement liés par une relation bijective. Par conséquent, prédire la portée d’une opération de modification requiert une compréhension claire de l’abstraction faite sur la mémoire.

Cette thèse propose un modèle pour mieux raisonner à propos de la gestion de mémoire. Notre premier objectif est de fournir une description plus précise des sémantiques d’assignation, de manière universelle et sans ambiguïté. Le modèle qui en résulte marque une distinction nette entre variables et valeurs, et met en avant les situations dans lesquelles sont créés des alias, ainsi que les situations dans lesquelles une modification peut avoir des effets de bords. Ce modèle est présenté formellement par le biais d’une sémantique complète, et informellement par le biais d’exemples de son application sur des exemples non triviaux. Il est ensuite utilisé pour décrire les erreurs mémoires liées à l’assignation. Deux méthodes sont proposées. La première consiste en une instrumentation de la sémantique dynamique pour détecter les accès à de la mémoire non initialisée ou libérée. La deuxième se repose sur un système de type basé sur des capacités pour garantir des propriétés de sureté statiquement. Finalement, nous présentons Anzen, un langage de programmation général basé sur le modèle formel susmentionné, dont le but est de valider de manière empirique son utilisabilité.

DR_illustration.jpg