A Synchronous Approach to Threaded Program Verification
Résumé
Modern systems involve a complex organization of computational processes sharing access to both processors and resources. The use of threads in programming provides a method in which lightweight processes may be given specific tasks that can be carried out either independently or in cooperation with other threads. The correct and efficient use of shared resources between threads relies on synchronisation methods, such as semaphores, mutexes, or events. Our work demonstrates a semi-automated method of translating threaded software to the synchronous programming language Signal in order to verify the correctness of thread synchronisations in the source code.
Les systèmes actuels s'appuient sur une organisation complexe de processus de calcul partageant l'accès aux processeurs et aux ressources. La programmation au moyen de "threads" fournit une méthode dans laquelle des processus légers se voient attribuer des tâches spécifiques qui peuvent être menées soit indépendamment, soit en coopération avec d'autres threads. L'utilisation correcte et efficace de ressources partagées entre les threads repose sur des mécanismes de synchronisation tels que les sémaphores, les sections critiques ou les événements. Notre travail décrit une méthode semi-automatique de traduction de logiciels organisés en threads vers le langage synchrone Signal dans le but de vérifier la correction des synchronisations des programmes sources.
Domaines
Systèmes embarqués
Origine : Fichiers produits par l'(les) auteur(s)