Soutenance de thèse de Nicolas Coste

Nicolas Coste soutiendra le 24 juin 2010 à 14h00
au Grand Amphithéâtre de l'INRIA Grenoble Rhône-Alpes
655, avenue de l'Europe 38330 Montbonnot Saint Martin
(informations d'accès)

une thèse de doctorat de l'Université de Grenoble,
spécialité : informatique, intitulée :

"Vers la prédiction de performance de modèles compositionnels dans les architectures GALS"

Thèse CIFRE STMicroelectronics-INRIA préparée dans le Centre de Recherche INRIA Grenoble Rhône-Alpes, au laboratoire LIG (équipe-projet VASY) et au laboratoire AST de STMicroelectronics
sous la direction de M. Hubert GARAVEL, de M. Etienne LANTREIBECQ, et de M. Wendelin SERWE.

COMPOSITION DU JURY :

• Mme. Brigitte PLATEAU, professeur à Grenoble INP (président du jury)
  
• M. Joost-Pieter KATOEN, professeur à la Rheinisch-Westfälische Technische Hochschule Aachen (rapporteur)
  
• M. Robert DE SIMONE, directeur de recherche à l'INRIA Sophia-Antipolis - Méditerranée (rapporteur)
  
• M. Hubert GARAVEL, directeur de recherche à l'INRIA Grenoble - Rhône-Alpes (directeur de thèse)
  
• M. Holger HERMANNS, professeur à l'Universität des Saarlandes (examinateur)
  
• M. Etienne LANTREIBECQ, ingénieur à STMicroelectronics (codirecteur de thèse)
  
• M. Wendelin SERWE, chargé de recherche à l'INRIA Grenoble - Rhône-Alpes (codirecteur de thèse)
  

La soutenance sera naturellement suivie d'un pot, dans la cafétéria de l'INRIA, auquel vous êtes tous cordialement invités.

RESUME :

La validation, incluant vérification fonctionnelle et évaluation de performance, est un processus critique pour la conception de designs matériels complexes : un design fonctionnellement correct peut s'avérer incapable d'atteindre la performance ciblée. Plus un problème dans un design est identifié tard, plus son coût de correction est élevé. La validation de designs devrait donc être entreprise le plus tôt possible dans le flot de conception.

Cette thèse présente un formalisme de modélisation par composition, couvrant les aspects fonctionnels et temporisés des systèmes matériels, et définit une approche d'évaluation de performance afin d'analyser les modèles construits.

Le formalisme de modélisation défini, appelé Interactive Probabilistic Chain (IPC), est une algèbre de processus a temps discret. Nous avons défini une bisimulation de branchement et prouvé sa congruence par rapport à l'opérateur de composition parallèle, nous permettant une approche compositionnelle. les IPCs peuvent être vues comme une transposition des Interactive Markov Chains dans un espace de temps discret.

Pour l'évaluation de performance, une IPC complètement spécifiée est transformée en une chaîne de Markov à temps discret, qui peut être analysée. De plus, nous avons défini une mesure de perfor- mance, appelée latence, et un algorithme permettant de calculer sa distribution moyenne sur le long terme.

A l'aide d'outils permettant de traiter les IPCs, développés sur la base de la boîte à outils CADP, nous avons étudié les aspects de communication d'un design industriel, l'architecture xSTream, développée chez STMicroelectronics.

MOTS-CLES : évaluation de performance, Interactive Probabilistic Chain (IPC), algèbre de processus, chaîne de Markov, latence, architecture matérielle.

TITLE:

Towards Performance Prediction of Compositional Models in GALS Designs

ABSTRACT:

Validation, comprising functional verification and performance evaluation, is critical for complex hardware designs. Indeed, due to the high level of parallelism in modern designs, a functionally verified design may not meet its performance specifications. In addition, the later a design error is identified, the greater its cost. Thus, validation of designs should start as early as possible.

This thesis proposes a compositional modeling framework, taking into account functional and time aspects of hardware systems, and defines a performance evaluation approach to analyze constructed models.

The modeling framework, called Interactive Probabilistic Chain (IPC), is a discrete-time process algebra, representing delays as probabilistic phase type distributions. We defined a branching bisimulation and proved that it is a congruence with respect to parallel composition, a crucial property for compositional modeling. IPCs can be considered as a transposition of Interactive Markov Chains in a discrete-time setting, allowing a precise and compact modeling of fixed hardware delays.

For performance evaluation, a fully specified IPC is transformed, assuming urgency of actions, into a discrete-time Markov chain, which can then be analyzed. Additionally, we defined a performance measure, called latency, and provided an algorithm to compute its long-run average distribution.

The modeling approach and the computation of latency distributions have been implemented in a tool-chain relying on the CADP toolbox. Using this tool-chain, we studied communication aspects of an industrial hardware design, the xSTtream architecture, developed at STMicroelectronics.

KEYWORDS:

performance evaluation, Interactive Probabilistic Chain (IPC), process algebra, Markov chain, latency, hardware architectures.

Back to the VASY Home Page