Soundness of the Quasi-Synchronous Abstraction

Guillaume Baudart 1 Timothy Bourke 1 Marc Pouzet 1
1 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Résumé : L’abstraction quasi-synchrone proposée par P. Caspi permet de faciliter l’analyse de systèmes dits quasi-périodiques où des unités de calcul s’exécutent de manière presque périodique. La simplicité de cette abstraction est prometteuse: les seuls événements considérés sont les activations des nœuds; les pas de temps logique représentent les délais de transmission; un nœud ne peut pas être activé plus de deux fois entre deux activations d’un autre nœud. Cette abstraction permet de vérifier des propriétés d’un système distribué temps-réel en utilisant un modèle discret plus simple. Dans cet article nous formalisons la relation entre les architectures quasi-périodiques et l’abstraction quasi-synchrone en utilisant la relation happened before introduite par L. Lam- port. Nous montrons que l’abstraction est valide pour des systèmes composés de deux nœuds, mais que ce n’est en général pas le cas pour des systèmes de trois nœuds ou plus. Nous donnons ensuite les restrictions nécessaires et suffisantes sur les topologies de communication pour assurer la validité de cette abstraction.
Type de document :
Rapport
[Research Report] RR-8755, INRIA Paris-Rocquencourt; INRIA. 2015, pp.19
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01175571
Contributeur : Guillaume Baudart <>
Soumis le : lundi 17 août 2015 - 14:51:28
Dernière modification le : mercredi 28 septembre 2016 - 16:16:39
Document(s) archivé(s) le : mercredi 26 avril 2017 - 10:20:19

Fichier

RR-8755-2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01175571, version 2

Collections

Citation

Guillaume Baudart, Timothy Bourke, Marc Pouzet. Soundness of the Quasi-Synchronous Abstraction. [Research Report] RR-8755, INRIA Paris-Rocquencourt; INRIA. 2015, pp.19. 〈hal-01175571v2〉

Partager

Métriques

Consultations de la notice

247

Téléchargements de fichiers

76