Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations

Jingshu Chen 1 Marie Duflot 1 Stephan Merz 1
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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.
Type de document :
Article dans une revue
Electronic Communications of the EASST, 2014, Automated Verification of Critical Systems 2014, 70, pp.14. 〈http://journal.ub.tu-berlin.de/eceasst/article/view/978〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01087871
Contributeur : Stephan Merz <>
Soumis le : jeudi 27 novembre 2014 - 02:41:07
Dernière modification le : jeudi 9 novembre 2017 - 01:13:21
Document(s) archivé(s) le : lundi 2 mars 2015 - 09:16:36

Fichiers

postproceedings.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas d'utilisation commerciale 4.0 International License

Identifiants

  • HAL Id : hal-01087871, version 1
  • ARXIV : 1412.0961

Collections

Citation

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. 〈http://journal.ub.tu-berlin.de/eceasst/article/view/978〉. 〈hal-01087871〉

Partager

Métriques

Consultations de la notice

238

Téléchargements de fichiers

113