Modélisation formelle de systèmes insensibles à la latence et ordonnancement
Institution:
NiceDisciplines:
Directors:
Abstract EN:
This PhD thesis links together the theory of Latency Insensitive Design (LID) on System on Chips with Marked Event Graphs (MEG) and its extension Synchronous Data Flow (SDF). This work allows using a general regular scheduling called central repetitive problem (workshop scheduling). We discuss existing links between the models MEG, SDF and LID. We present after a formally verified implementation of LID using synchronous reactive components. Then, we use a classical result on the ultimately repetitive behaviour and static scheduling of MEG to define “Equalization” techniques attempting to adjust the topology of communications of the system in order to slow-down too fast paths adding some latencies, while preserving the global throughput of the original system. Finally, we introduce some limited control in LID, with routing nodes called Select and Merge where routing conditions are known and independent of data flows. Those routing conditions are directed by ultimately periodic binary words (just like in previous static scheduling). Through an abstraction over SDF model we show the decidability of safety and liveness properties on the extended model. We produce finally a complete axiomatic for transitivity/commutativity of Select/Merge operators.
Abstract FR:
Cette thèse relie la conception dite insensible à la latence (LID) de systèmes sur puce à une modélisation par Marked Event Graphs (MEG) et extensions Synchronous Data Flow (SDF). Ces travaux permettent l’utilisation d’un ordonnancement général régulier dénommé problème central répétitif. Nous discutons des liens existants entre les modèles MEG, SDF et LID. Nous présentons ensuite une implantation vérifiée formellement de LID en utilisant des composants réactifs synchrones. Ensuite, nous utilisons un résultat classique sur le comportement ultimement répétitif et l’ordonnancement statique des MEGs pour définir des techniques d’Égalisation visant à ajuster la topologie des communications du système afin de ralentir des chemins trop rapides en rajoutant des latences, tout en conservant le débit du système originel. Enfin, nous introduisons une notion de contrôle limité au modèle LID, avec des nœuds de routage Select et Merge dont les conditions sont connues et indépendantes des flots de données. Ces conditions d’aiguillage sont dirigées elles aussi par des mots binaires ultimement périodiques (comme dans l’ordonnancement statique précédent). Par abstraction sur le modèle SDF nous montrons la décidabilité des propriétés de safety et liveness sur le modèle étendu. Nous produisons enfin une axiomatique complète pour la transitivité/commutativité des opérateurs Select/Merge.