Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Article Dans Une Revue Electronic Communications of the EASST Année : 2014

Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations

Résumé

Avoiding access conflicts is a major challenge in the design of multi-threaded programs. In the context of real-time systems, the absence of conflicts can be guaranteed by ensuring that no two potentially conflicting accesses are ever scheduled concurrently.In this paper, we analyze programs that carry time annotations specifying the time for executing each statement. We propose a technique for verifying that a multi-threaded program with time annotations is free of access conflicts. In particular, we generate constraints that reflect the possible schedules for executing the program and the required properties. We then invoke an SMT solver in order to verify that no execution gives rise to concurrent conflicting accesses. Otherwise, we obtain a trace that exhibits the access conflict.
Fichier principal
Vignette du fichier
postproceedings.pdf (171.72 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01087871 , version 1 (27-11-2014)

Licence

Paternité - Pas d'utilisation commerciale

Identifiants

Citer

Jingshu Chen, Marie Duflot, Stephan Merz. Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations. Electronic Communications of the EASST, 2014, Automated Verification of Critical Systems 2014, 70, pp.14. ⟨hal-01087871⟩
246 Consultations
84 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More