Espace de tas, Glaneur de cellules, Concurrence, Vérification formelle, Logique de séparation

Cette thèse aborde le problème du raisonnement formel sur l'utilisation de l'espace de tas (heap space) des programmes concurrents en présence d'un glaneur de cellules (garbage collector). Alors qu'il est facile d'identifier où l'espace est consommé, c'est-à-dire les points d'allocations, la présence d'un glaneur de cellules rend délicat de déterminer où l'espace est libéré, les points de désallocations étant implicites. En effet, le glaneur de cellules peut s'exécuter à n'importe quel moment pour désallouer des blocs mémoires inaccessibles, c'est-à-dire les blocs qui ne sont pas transitivement accessibles depuis les adresses racines (roots) du code restant à exécuter. Une question centrale à cette thèse est donc: comment raisonner sur l'inaccessibilité ? Pour répondre à cette question, nous proposons IrisFit, une nouvelle logique de séparation construite au-dessus du cadre logique Iris. IrisFit garde trace de l'accessibilité des blocs mémoire en équipant chaque adresse d'une assertion pointed-by-heap et d'une assertion pointed-by-thread, enregistrant respectivement quel bloc mémoire accessible pointe vers cette adresse et quel fil (thread) considère cette adresse comme une racine. De plus, IrisFit exploite la notion de crédits-espace, un outil purement logique qui garde trace de la quantité d'espace libre disponible. Des crédits-espace sont consommés par les allocations et peuvent être récupérés en prouvant qu'un bloc mémoire est inaccessible. Au cours de cette thèse, nous avons identifié une difficulté fondamentale dans l'analyse de la complexité en espace de tas au pire cas des programmes concurrents en présence d'un glaneur de cellules. En effet, si l'exécution du glaneur de cellules et la réduction des fils peuvent s'entrelacer de manière arbitraire, alors il existe des scénarios indésirables dans lesquels une racine retenue par un fil endormi empêche la désallocation d'une quantité de mémoire possiblement grande. Pour remédier à ce problème, nous proposons deux nouvelles constructions: les sections protégées, dans lesquelles le glaneur de cellules n'a pas le droit de s'exécuter, et les points de polling, des instructions qui bloquent le fil courant si un autre fil requiert l'exécution du glaneur de cellules. Les sections protégées peuvent être exploitées par le programmeur pour éliminer les scénarios indésirables décrits ci-dessus, permettant ainsi d'obtenir une meilleure complexité en espace de tas au pire cas. Les points de polling, quant à eux, peuvent être insérés par le compilateur pour garantir qu'aucun fil n'attend indéfiniment que le glaneur de cellules s'exécute. Nous étendons IrisFit pour permettre de raisonner sur les sections protégées. Nous prouvons qu'IrisFit offre une garantie de sûreté (les programmes vérifiés ne peuvent pas produire une erreur et n'excèdent pas une borne donnée en espace de tas) et une garantie de vivacité (il existe une stratégie d'insertion des points de polling dans les programmes vérifiés garantissant que chaque requête d'allocation sera satisfaite après un nombre de pas borné). Nous illustrons l'utilisation d'IrisFit avec plusieurs études de cas. En particulier, nous vérifions des structures de données concurrentes et non-bloquantes standards comme la pile de Treiber et la file de Michael et Scott. Nous montrons qu'en augmentant le code de ces structures avec des sections protégées, nous obtenons des implémentations qui garantissent la complexité en espace de tas intuitivement attendue. De plus, nous prouvons correcte une implémentation des fermetures, des structures de données concrètes allouées sur le tas implémentant le concept abstrait de fonction de première classe. Les techniques de raisonnement que nous développons dans cette thèse sont destinées à s'appliquer à des langages répandus comme OCaml et Java. IrisFit ainsi que tous les résultats présentés sont formalisés dans l'assistant de preuve Coq.