Synchronisation de fils d'exécution en interprétation abstraite

National audienceAfter a short presentation of static analysis by Abstract Interpretation, we summarize and extend previous work by A. Miné on checking for run-time errors in parallel and multi-threaded programs, focusing on real-time systems used in critical embedded software, where threads communicate through shared memory and mutual exclusion locks, using a thread-modular iteration. As an extension, we define system events and present some of their natural uses in parallel programs, proposing some theoretical ways to integrate them into previous work on Abstract Interpretation, using the idea of interference partitioning, previously introduced to take mutexes into account. We finally present a demonstrator implementing one of these techniques.Après avoir brièvement présenté l'analyse statique de programmes par interprétation abstraite, nous résumerons le travail effectué précédemment par A. Miné sur la détection d'erreurs à l'exécution dans les programmes multi-threadés, en étudiant spécifiquement le cas de systèmes temps-téels utilisés pour les logiciels critiques embarqués, dont les threads communiquent via la mémoire partagée et des verrous d'exclusion mutuelle, en utilisant une technique thread-modulaire et une itération sur les threads. Nous définirons ensuite la notion d'événement, et nous présenterons quelques-uns des ses usages courants dans les programmes parallèles, pour proposer des moyens de les intégrer à l'état de l'art dans l'interpretation abstraite, grâce à l'idée de partitionnement des interférences, introduite initialement pour le support des mutex. Nous présenterons enfin un démonstrateur implémentant l'une de ces techniques