Low-Impact Operating System Tracing

Les systèmes informatiques, tant au niveau matériel que logiciel, deviennent de plus en plus complexes. En ce qui concerne Linux, système d'exploitation utilisé dans une vaste catégorie d'applications, des petits systèmes embarqués aux serveurs de haut-niveau, la taille des noyaux de systèmes d'exploitations augmente, des librairies sont ajoutées et une réingénierie logicielle est requise pour bénéficier des architectures multi-coeurs, lesquelles sont omniprésentes. Par conséquent, l'industrie du développement logiciel et les développeurs individuels font face à des problèmes dont la résolution nécessite de comprendre l'interaction entre les applications et tous les composants d'un système d'exploitation. Dans cette thèse, nous proposons le traceur LTTng (Linux Trace Toolkit next generation) comme réponse aux besoins de traçage de l'industrie et de la communauté du logiciel libre. La faible intrusivité du traceur est un aspect clé menant à son utilisabilité, puisqu'il est nécessaire de reproduire, sous traçage, des problèmes observés sous des conditions d'exécution normales. Dans certains cas, les usagers souhaitent laisser des traceurs actifs en tout temps sur des systèmes en production, ce qui rend l'impact en performance définitivement critique. Notre approche implique l'élaboration de primitives de synchronisation qui rencontrent les requis de faible impact. Le mécanisme de synchronisation permettant la mise à l'échelle et sans attente RCU (Read-Copy Update) utilisé par le traceur LTTng remplit ces requis en ce qui concerne la lecture de données. Nous proposons un mécanisme de synchronisation pour extraire les données de traçage en préservant les caractéristiques de mise à l'échelle linéaire et de non-attente. En mesurant l'impact du traceur LTTng, nous démontrons qu'il est possible de créer un traceur qui satisfait toutes les caractéristiques suivantes : faible latence, comportement temps-réel déterministe (sans attente), faible impact sur le débit du système d'exploitation et une mise à l'échelle linéaire par rapport au nombre de processeurs. Une expérimentation sur plusieurs architectures permet d'observer la portabilité du traceur. Nous proposons un modèle général pour les systèmes superscalaires multi-coeurs avec accès mémoire faiblement ordonnés pour permettre la vérification formelle des garanties quant à l'exactitude de l'exécution et l'exécution sans attente à l'aide de la vérification de modèle. Le mécanisme de tampon de LTTng est également vérifié formellement quant à son exactitude et son exécution sans attente. La vérification formelle permet également de démontrer que ces algorithmes permettent la réentrance de plusieurs contextes d'exécution, du fil d'exécution standard aux gestionnaires d'interruptions non-masquables, permettant une large couverture d'instrumentation du système d'exploitation.