Le but de cette thèse est de présenter une analyse statique générique pour des programmes multitâche écrits en Java.<br />Les programmes multitâche exécutent plusieurs tâches en parallèle. Ces tâches communiquent implicitement par le biais de la mémoire partagée et elles se synchonisent sur des moniteurs (les primitives wait-notify, etc..). Il y a quelques années, les architectures avec double processeurs ont commencé à être disponibles sur le marché à petit prix. Aujourd'hui, presque tous les ordinateurs ont au moins deux noyaux, la tendance actuelle du marché étant de mettre de plus en plus de processeurs par puce. Cette révolution amène également de nouveaux défis en matière de programmation, car elle demande aux développeurs d'implanter des programmes multitâche. Le multitâche est supporté en natif par la plupart des langages de programmation courants, comme Java et C#.<br />Le but de l'analyse statique est de calculer des informations sur le comportement d'un programme, de manière conservative et automatique. Une application de l'analyse statique est le développement d'outils qui aident au débogage des programmes. Plusieurs méthodes d'analyse statique ont été proposées. Nous suivrons le cadre de l'interprétation abstraite, une théorie mathématique permettant de définir des approximations correctes de sémantiques de programmes. Cette méthode a déjà été utilisée pour un large spectre de langages de programmation.<br />L'idée fondamentale des analyseurs statiques génériques est de développer un outils qui puissent être interfacé avec différents domaines numériques et différentes propriétés. Pendant ces dernières années, beaucoup de travaux se sont attaqués à cet enjeu, et ils ont été appliqué avec succès pour déboguer des logiciels industriels. La force de ces analyseurs réside dans le fait qu'une grande partie de l'analyse peut être réutilisée pour vérifier plusieurs propriétés. L'utilisation de différents domaines numériques permet le développement d'analyses plus rapides mais moins précises, ou plus lentes mais plus précises.<br /><br />Dans cette thèse, nous présentons la conception d'un analyseur générique pour des programmes multitâche. Avant tout, nous définissons le modèle mémoire, appelé happens-before memory model. Puis, nous approximons ce modéle mémoire en une semantique calculable. Les modéles mémoire définissent les comportements autorisés pendant l'exé-cution d'un programme multitâche. Commençant par la définition (informelle) de ce modèle mémoire particulier, nous définissons une sémantique qui construit toutes les exécutions finies selon ce modèle mémoire. Une exécution d'un programme multitâche est décrite par une function qui associe les tâches à des séquences (ou traces) d'états. Nous montrons comment concevoir une sémantique abstraite calculable, et nous montrons formellement la correction des résultat de cette analyse.<br />Ensuite, nous définissons et approximons une nouvelle propriété qui porte sur les comportements non-déterministes causés par le multitâche, c'est à dire aux entrelacements arbitraires pendant l'exécution de differentes instructions de lecture. Avant tout, le non déterminisme d'un programme multitâche se définit par une différence entre plusieurs exécutions. Si deux exécutions engendrent des comportements différents dus au valeurs qui sont lues ou écrites en mémoire partagée, alors le programme est non déterministe. Nous approximons cette propriété en deux étapes: dans un premier temps, nous regroupons, pour chaque tâche, la valeur (abstraite) qui peut être écrite dans la mémoire partagée à un point de programme donné. Dans un deuxième temps, nous résumons toutes les valeurs pouvant être écrites en parallèle, tout en nous rapellant l'ensemble des tâches qui pourraient les avoir écrites. à un premier niveau d'approximation, nous introduisons un nouveau concept de déterminisme faible. Nous proposons par ailleurs d'autres manière affaiblir la propriété de déterminisme, par exemple par projection des traces et des états, puis nous définissons une hierarchie globale de ces affaiblissements. Nous étudions aussi comment la présence de conflit sur les accès des données peut affecter le déterminisme du programme.<br />Nous appliquons ce cadre de travail théorique à Java. En particulier, nous définissons une sémantique du language objet de Java, selon sa spécification. Ensuite, nous approximons cette sémantique afin de garder uniquement l'information qui est nécessaire pour l'analyse des programmes multitâche. Le cœur de cette abstraction est une analyse d'alias qui approxime les références afin d'identifier les tâches, de vérifier les accès en mémoire partagée, et de détecter quand deux tâches ont un moniteur commun afin d'en déduire quelles parties du code ne peuvent pas être éxécutées en parallèle.<br />L'analyseur générique qui est décrit ci-dessus a été entierement implanté, dans un outils appelé Checkmate. Checkmate est ainsi le premier analyseur générique pour des programmes multitâche écrits en Java. Des résultats expérimentaux sont donnés et analysés en détails. En particulier, nous étudions la précision de l'analyse lorsqu'elle est appliquée à des schémas courants de la programmation concurrente, ainsi qu'à d'autres exemples. Nous observons également les performances de l'analyse lorsqu'elle est appliquée à une application incrémentale, ainsi qu'à des exemples de références bien connus.<br />Une autre contribution de cette thèse est l'extension d'un analyseur générique existant qui s'appelle Clousot et qui permet de vérifier le non débordement des mémoires tampons. Il s'avère que cette analyse passe à l'échelle des programmes industriels et qu'elle est précise. En résumé, nous présentons une application d'un analyseur statique générique industriel existant pour détecter et prouver une propriété présentant un intérêt pratique, ce qui montre la puissance de cette approche dans le développement d'outils qui soient utiles pour les développeurs.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00417502 |
| Date | 22 September 2009 |
| Creators | Ferrara, Pietro |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0022 seconds