[thèse 2022] Logiques de ressources non agrégatives: modèles et calculs.

Mots clés:
sémantique, théorie de la preuve, logiques de ressources, composition non agrégative.

Contact

Didier GALMICHE
(galmiche@loria.fr)

Daniel MERY
(dmery@loria.fr)

Résumé

Dans cette thèse, nous nous concentrons sur des extensions non agrégatives des logiques de séparation (comme SL et BI) et leurs modèles de ressources associés.

Nous nous intéresserons :

  • à l’étude de nouveaux monoïdes de ressources dont la composition ne se résume pas à l’union disjointe de fonctions partielles, en commençant par des extensions et variantes du modèle standard de tas mémoires de SL ;
  • à la proposition de nouvelles logiques en adéquation avec les modèles non agrégatifs étudiés ;
  • à des extensions non agrégatives de la variante intuitionniste de SL dans lesquelles le préordre sur les ressources n’est pas dérivable de la composition ;
  • à la définition de combinaisons non orthogonales entre logiques modales (avec modalités temporelles par exemple) et logiques de ressources.

Contexte scientifique

Aujourd’hui les systèmes informatiques sont hautement complexes. La plupart d’entre eux sont intrinsèquement distribués et dynamiquement reconfigurables (Big Data, Internet des objets, Cloud Computing) et concurrents tant au niveau physique (CPU multi-coeurs) que logique (threads).
Ce niveau de complexité soulève d’importants problèmes techniques. Par exemple, comment assurer qu’un système consistant en une vaste multitude de composants hétérogènes, conçus par des développeurs divers et variés, fournit les services attendus ? Comment assurer que les composants ne s’interbloquent pas ou qu’un composant ne se voit pas refuser indéfiniment l’accès à service ? Comment vérifier qu’une mise à jour logicielle d’un composant ne laisse pas fuiter de l’information confidentielle à des tiers ?

Appréhender les systèmes complexes est possible uniquement grâce à leur modularité et les composants d’un système modulaire peuvent être vus, à un plus haut niveau d’abstraction, comme des ressources pouvant être statiques ou dynamiques (un bloc de données ou un processus), physiques ou logiques (CPUs ou threads), atomiques (une cellule de mémoire) ou structurellement plus élaborées (une liste chaînée ou un tube). L’opération principale sur un ensemble de ressources est la composition, formellement comprise comme un produit dans un monoïde.

Les monoïdes de ressources qui ont reçus le plus d’attention jusqu’ici sont les monoïdes de ressources agrégatifs, c’est à dire, ceux dont les opérateurs de composition se comportent comme des unions d’ensembles disjoints. C’est le cas notamment dans les logiques de séparation ou avec bunch [5,8].
Un exemple typique de composition agrégative est la composition de tas mémoires d’un programme. Un tas mémoire peut être modélisé comme une fonction partielle (des adresses mémoires vers les valeurs). La composition de deux tas mémoires est l’union des fonctions partielles dont les domaines sont disjoints. Par ailleurs, il y a de nombreux exemples d’opérateurs de composition non agrégatifs,comme la composition de processus concurrents modélisés comme des machines à états finis ou la composition de services partageant la même interface dans les applications distribuées en nuage.

Sujet et objectifs

Certaines propriétés algébriques (équationnelles) des compositions agrégatives, c’est à dire les compositions qui obéissent au principe que le tout est plus que la somme de ses parties, ont été identifiées dans des travaux existants [3,7]. Cependant, parce que la nature agrégative d’un opérateur de composition ne peut pas pleinement être appréhendée uniquement en termes de propriétés équationnelles, il est nécessaire d’introduire des aspects plus structurels comme des préordres sur les ressources ou des mesures de leur taille. Par exemple, une propriété attendue d’un opérateur de composition agrégatif est que les opérandes d’une composition (les composants) restent des parties discernables du résultat de la composition (le composite). Un tel opérateur fait également en sorte que le composite soit plus grand que chacun de ses composants (pour une notion de mesure donnée). Beaucoup de compostions naturelles ne satisfont pas ces principes.
Pour une illustration intuitive, considérons un opérateur de fusion qui annihile des ressources considérées comme duales (comme la collision de particules et anti-particules en physique). Composer une ressource (particule) a avec une ressource duale (anti-particule) b aboutit à la ressource vide (une quantité d’énergie matériellement intangible) e. Clairement, la taille de la composition a ∗ b n’est pas plus grande que a et que b, et en observant uniquement la ressource e, il n’est pas possible de dire si elle résulte de la composition de a et b, ou de deux autres ressources duales c et d.

Un premier objectif de cette thèse est d’étudier des modèles de ressources non-agrégatifs et de proposer des logiques non-agrégatives en adéquation avec ces modèles.

Les travaux courants qui vont au delà du modèle standard de tas mémoires de la logique de séparation (SL), comme [6] et [9] explorent principalement des extensions non annulables de la version classique de SL. Une des raisons de la prédominance du biais classique est que la variante intuitionniste du prédicat ‘points-to’ peut aisément être caractérisée dans la version classique de SL, rendant de fait la version intuitionniste peu intéressante.
Cette situation découle du choix de l’inclusion comme préordre naturel sur les tas mémoire. Comme l’inclusion des tas peut se dériver à partir de la composition des tas ( h ⊆ h’ ⇔ ∃h”.h∗h”=h’ ), la nature agrégative de la composition
des tas mène à une version intuitionniste de SL plus faible que sa version classique (par exemple, l’implication A ∗ B → A ∧ B est valide).

Un deuxième objectif de cette thèse est d’étudier des extensions intuitionniste non-agrégatives de SL dont les préordres ne sont pas dérivables de la composition des ressources.

Tous les aspects intéressants des modèles non agrégatifs ne peuvent être réduits à des opérateurs de composition de ressources. La distribution des ressources dans le temps et l’espace sont en fait mieux traités en termes de modalités [1,2,4].
Les travaux actuels combinant les logiques modales avec les logiques de ressources reposent sur des modèles dans lesquels les modalités sont interprétées de manière indépendante de la relation de préordre sur laquelle les ressources sont interprétées. Cette orthogonalité aide grandement à la réutilisation des techniques développées dans les deux champs d’étude (logiques modales et logiques de ressources), mais elle rend plus difficile pour les logiques combinées résultantes d’exprimer et de traiter des propriétés impliquant une réelle intéraction entre l’aspect modal et l’aspect ressources.
Par exemple, dans une extension temporelle de BI, les ressources sont distribuées sur des instants (points dans le temps) auxquels elles sont considérées comme disponibles. La formule A ∗ (A −∗ B) signifie donc que si (la formule) A est satisfaite à l’instant t avec les ressources r1 et que A −∗ B est satisfaite à l’instant t avec les resources r2, alors B devrait être satisfaite à l’instant t avec les ressources r1 ∗ r2. Il est assez clair que cette interprétation des connecteurs liés aux ressources ne dépend pas du temps.
Par contre, changer la conclusion à “alors B devrait être satisfaite à l’instant t + |r1|” autoriserait une plus grande interaction dans laquelle la satisfiabilité (disponibilité dans le temps) de B dépendrait de la taille de r1 (en exprimant que plus A est gros, plus cela prend de temps de produire B).

Un troisième objectif de la thèse est de proposer des combinaisons non orthogonales de logiques modales et de logiques de ressources non agrégatives.

Références

[1] Gabrielle Anderson and David Pym. A calculus and logic of bunched resources and processes. TCS, 614(C):63–96, February 2016.

[2] Stephen Brookes and Peter W. O’Hearn. Concurrent separation logic. ACM SIGLOG News, 3(3):47–65, August 2016.

[3] James Brotherston and Jules Villard. Parametric Completeness for Separation Theories. In POPL, pages 453–464. ACM, 2014.

[4] Jean-René Courtault, Didier Galmiche, and David Pym. A logic of separating modalities. Theor. Comput. Sci., 637(C):30–58, July 2016.

[5] Didier Galmiche, Daniel Méry, and David J. Pym. The semantics of BI and Resource Tableaux. MSCS, 15(6):1033–1088, 2005.

[6] Jonas Braband Jensen and Lars Birkedal. Fictional separation logic. In Helmut Seidl, editor, Programming Languages and Systems, pages 377–396, Berlin, Heidelberg, 2012. Springer Berlin, Heidelberg.

[7] Dominique Larchey-Wendling and Didier Galmiche. Looking at separation algebras with boolean bi-eyes. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, TCS 2014, volume 8705 of LNCS, pages 326–340. Springer, 2014.

[8] Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Proceedings of the 15th International Workshop on Computer Science Logic, CSL ’01, pages 1–19, 2001.

[9] Viktor Vafeiadis and Chinmay Narayan. Relaxed separation logic : A program logic for c11 concurrency. In OOPSLA 2013, OOPSLA ’13, page 867–884, New York, NY, USA, 2013. Association for Computing Machinery.

Équipe d’accueil

La thèse est proposée par l’équipe TYPES du laboratoire de recherche LORIA.

Compétences et profil

  • Qualifications requises: un Master en Informatique (ou équivalent)
  • Des connaissances dans les domaines suivants seront appréciées: logique, théorie de la preuve, sémantique, programmation (C, CAML, Java, Python)

Informations complémentaires

Durée: 3 ans

Date de début: entre le 1er octobre 2022 et le 1er décembre 2022

Comment candidater

Envoyer les documents suivants à
galmiche@loria.fr
et
dmery@loria.fr

  • un CV
  • une lettre de motivation
  • les certificats et relevés de notes de la Licence et du Master (ou équivalents)

Logo d'Inria