You are here

Typage par raffinement des systèmes en traitement du signal

Team and supervisors
Department / Team: 
Team Web Site: 
https://www.inria.fr/teams/tea
PhD Director
Jean-Pierre Talpin
Co-director(s), co-supervisor(s)
Maxime Pelcat
Contact(s)
PhD subject
Abstract

CONTEXTE
Typage par raffinement.
Le typage par raffinement permet d'associer une fonction, une procédure ou une variable, à un type décrivant son domaine de définition, et à une proposition logique (modulo théorie), raffinant ce domaine de définition au moyen de contraintes. En ce sens, par exemple, Frama-C [CKK12] implémente une notion de typage par raffinement (à minima) par la possibilité d’expliciter des assertions sur les pré- et post-conditions qui peuvent ensuite être, pour certaines, validées par analyse statique.
Le typage par raffinement est principalement mis en œuvre dans deux langages de programmation fonctionnelle : Liquid Haskell [V16] et F* [SHK16].  Liquid Haskell supporte la résolution automatique de contraintes (en logique conjonctive de 1er ordre). F* délègue la preuve de propriétés en logique propositionnelle à un solveur SAT et un démonstrateur de théorèmes (Coq).
Performance des systèmes de traitement du signal. Avec la mise en place de l'Internet des Objets et l'intérêt croissant pour les systèmes cyber-physiques, les systèmes de traitement du signal sont soumis à des contraintes de plus en plus fortes et variées (consommation d'énergie, latence, cadence, encombrement, etc). Ces contraintes poussent à l'utilisation d'implémentations matérielles dédiées, coûteuses en termes de conception, telles que le processeur Movidius dans le domaine de l'intelligence artificielle [IG15].
Dans ce contexte et afin de maintenir une productivité de conception de ces systèmes compatible avec leur mise sur le marché, de nouvelles méthodes de conception de haut niveau (HLS pour *High-Level Synthesis*) sont adoptées [CM08]. Contrairement à une description classique en VHDL ou Verilog d'un système matériel, la HLS permet une verification fonctionnelle du système indépendante de sa verification temporelle. De plus, la verification fonctionnelle ne nécessite pas de synthèse matérielle.
CAPH [SBA13] est un langage de HLS dédié à la description de systèmes de traitement du signal. Il décrit des réseaux de processus flux de données et s'appuie sur la programmation fonctionnelle. Ce langage est compilable en un code VHDL fonctionnel permettant la génération automatique d'un système matériel (FPGA ou ASIC). Il est également compilable en un code SystemC permettant une simulation efficace des fonctionnalités matérielles.


OBJECTIFS
Dans cette thèse, nous nous intéressons à assister l'analyse de modèles en traitement du signal au moyen de types par raffinement. Usuellement, l'analyse d'architecture en traitement du signal (performance, latence, énergie) est réalisée au moyen d'outils d'analyse statique (calcul d'un WCET, d'un ordonnancement, etc) en raisonnant sur l'ensemble du système.
Le typage, augmenté de propriétés logiques portant sur ces quantités, ouvre à la possibilité d'un raisonnement modulaire: d'analyser un modèle étant donné le type de son contexte d'utilisation, d'abstraire le résultat d'une analyse par un type décrivant ses contraintes non-fonctionnelles, de vérifier la compatibilité de modèles par composition.

Cette thèse consistera à exploiter les notions d'inférence de type et de problème de décision pour inférer des informations de performance sur un système de calcul sur flux représenté par un réseau de processus flux de données. La consommation d'énergie et la latence seront les deux premiers indicateurs de performance étudiés et seront inférés à partir de performances matérielles mesurées.

Bibliography

[VP09] Vuagnoux, Martin, & Pasini, Sylvain (2009) "Compromising Electromagnetic Emanations of Wired and Wireless Keyboards.” In Proceedings of the USENIX security symposium.
[CKK12] Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., & Yakobowski, B. (2012). “Frama-c.” In International Conference on Software Engineering and Formal Methods (pp. 233-247). Springer, Berlin, Heidelberg.
[V16] Vazou, N. (2016). “Liquid Haskell: Haskell as a theorem prover. “, Ph.D. Thesis, University of California, San Diego.
[SHK16] Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, et al.. (2016) Dependent Types and Multi-Monadic Effects in F*. 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), St. Petersburg, Florida, United States. ACM
[IG15] Ionica, M. H., & Gregg, D. (2015). The movidius myriad architecture's potential for scientific computing. _IEEE Micro_, _35_(1), 6-14.
[CM08] Coussy, P., & Morawiec, A. (Eds.). (2008).” High-level synthesis: from algorithm to digital circuit.” Springer Science & Business Media.
[SBA13] Sérot, J., Berry, F., & Ahmed, S. (2013). “CAPH: a language for implementing stream-processing applications on FPGAs.” In Embedded Systems Design with FPGAs (pp. 201-224). Springer, New York, NY.

Work start date: 
Automne 2018
Keywords: 
Inférence de type, Typage par raffinement, Conception des systèmes de traitement du signal.
Place: 
IRISA - Campus universitaire de Beaulieu, Rennes