Precise deadlock detection for polychronous data-flow specifications

Van Chan Ngo 1 Jean-Pierre Talpin 1 Thierry Gautier 2
1 ESPRESSO - Synchronous programming for the trusted component-based engineering of embedded systems and mission-critical systems
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
2 TEA - Tim, Events and Architectures
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Dependency graphs are a commonly used data structure to encode the streams of values in data-flow programs and play a central role in scheduling instructions during auto-mated code generation from such specifications. In this work, we propose a precise and effective method that combines a structure of dependency graph and first order logic formulas to check whether multi-clocked data-flow specifications are deadlock free before generating code from them. We represent the flow of values in the source programs by means of a dependency graph and attach first-order logic formulas to condition these dependencies. We use an SMT solver to effectively reason about the implied formulas and check deadlock freedom.
Type de document :
Communication dans un congrès
ESLsyn - DAC 2014, May 2014, San Francisco, United States. 2014, 〈10.1109/ESLsyn.2014.6850379〉
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-01086843
Contributeur : Van Chan Ngo <>
Soumis le : mardi 25 novembre 2014 - 10:07:19
Dernière modification le : mardi 16 janvier 2018 - 15:54:23
Document(s) archivé(s) le : jeudi 26 février 2015 - 10:50:50

Fichier

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

Identifiants

Citation

Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier. Precise deadlock detection for polychronous data-flow specifications. ESLsyn - DAC 2014, May 2014, San Francisco, United States. 2014, 〈10.1109/ESLsyn.2014.6850379〉. 〈hal-01086843〉

Partager

Métriques

Consultations de la notice

302

Téléchargements de fichiers

97