Assas Recherche | CoqDRAM - Une Fondation pour la Conception de Contrôleurs de Mémoire Formellement Prouvés

CoqDRAM - Une Fondation pour la Conception de Contrôleurs de Mémoire Formellement Prouvés (Document en Anglais, Français)

Accès au(x) document(s)

Accéder au(x) document(s) :

Ce document est protégé en vertu du Code de la Propriété Intellectuelle.

Modalités de diffusion de la thèse :

Thèse consultable sur internet, en texte intégral.

Informations sur les contributeurs

Auteur : Lisboa malaquias Felipe

Lisboa malaquias, Felipe

Nom

Lisboa malaquias

Prénom

Felipe

Nationalité

Français

Date de soutenance : 21-06-2024

Directeur(s) de thèse : Alves de Barros Naviner Lirida

Alves de Barros Naviner, Lirida

Nom

Alves de Barros Naviner

Prénom

Lirida

- Brandner Florian

Brandner, Florian

Nom

Brandner

Prénom

Florian

Etablissement de soutenance : Institut polytechnique de Paris

Institut polytechnique de Paris

Nom

Institut polytechnique de Paris

Laboratoire : Laboratoire Traitement et communication de l'information (Paris ; 2003-....)

Laboratoire Traitement et communication de l'information (Paris ; 2003-....)

Nom

Laboratoire Traitement et communication de l'information (Paris ; 2003-....)

- Laboratoire de Traitement et Communication de l'Information

Laboratoire de Traitement et Communication de l'Information

Nom

Laboratoire de Traitement et Communication de l'Information

Ecole doctorale : École doctorale de l'Institut polytechnique de Paris

École doctorale de l'Institut polytechnique de Paris

Nom

École doctorale de l'Institut polytechnique de Paris

Informations générales

Discipline : Information, communications, électronique
Classification : Informatique

Mots-clés libres : Méthodes Formelles, Contrôleurs Mémoire, DRAM, Systèmes Temps-Réel, Ordonnancement
Mots-clés :

Ordinateurs -- Mémoires à accès sélectif - Construction
Ordonnancement dynamique
Commande en temps réel
Gestion mémoire (informatique)

Résumé : Les contrôleurs mémoire temps-réel récemment proposés abordent le compromis entreperformance et prédictibilité en cherchant à offrir le meilleur des deux mondes. Cependant,en conséquence, les conceptions deviennent complexes et présentent souvent des développementsmathématiques qui sont longs, difficiles à lire et à examiner, incomplets, et reposent sur des hypothèses peu claires. Etant donné que de tels composants sont souvent conçus comme faisant partie de microarchitectures utilisées dans des systèmes temps réel critiques, un degré élevé de confiance dans le comportement correct du système est nécessairepour atteindre les objectifs de certification. Pour résoudre ce problème, nous proposons un nouveauframework, intitulé CoqDRAM, écrit dans l’assistant de preuves formelles Coq, dans lequel nousmodélisons les dispositifs DRAM et les contrôleurs et leur comportement attendu en tant que spécification formelle. Le framework est destiné à aider à la conception d’algorithmes d’ordonnancement DRAM corrects par construction et dignes de confiance. La spécification CoqDRAM capture les critères de correction selon les normes JEDEC et énonce d’autrespropriétés de haut niveau, telles que l’équité (fairness) et la cohérence séquentielle (sequential consistency).Suivant cette approche, les développements mathématiques sur papier-et-crayon sont remplacéspar des preuves vérifiées par machine, ce qui accroit la confiance que la conception est effectivement correcte. Nous présentons l’utilisabilité de Coq-DRAM en modélisant et en prouvant deux algorithmes d’ordonnancement de principe : l’un basé sur la politique d’arbitrage First-In First-Out (FIFO) et l’autre sur la multiplexage par répartition dans le temps (TDM). De plus, en utilisant CoqDRAM, nous proposons un nouvel algorithme d’ordonnancement DRAM appelé TDMShelf, qui étend et améliore les travaux précédents sur l’arbitrage work-conserving dynamique TDM. Plus précisément, TDMShelf exploite des informations sur l’état interne de la mémoire auniveau de l‘ordonnancement des requêtes mémoire, fournissant ainsi un bon équilibre entre prédictibilité et latence moyenne pour les systèmes temps réel à criticité mixte.

Informations techniques

Type de contenu : Text
Format : PDF

Informations complémentaires

Entrepôt d'origine :

STAR : dépôt national des thèses électroniques françaises

Identifiant : 2024IPPAT020
Type de ressource : Thèse