La vérification de la consistance mémoire (VCM) consiste à vérifier que l'exécution d'un programme par une plate-forme matérielle s'est déroulée conformément à un modèle de consistance mémoire (MCM).Un MCM défini certaines propriétés concernant les accès à la mémoire, en particulier concernant l'ordre d'accès provenant de différents processeurs. C'est un problème complexe qui nécessite de connaître beaucoup d'informations sur l'exécution du programme afin d'obtenir une complexité linéaire: en particulier l'ordre des écriture à chaque case mémoire.Néanmoins les techniques classiques de VCM sont trop gourmandes en occupation mémoire pour pouvoir passer à l'échelle. Dans cette thèse nous proposons une méthode de VCM destinée au prototypage virtuel ayant une complexité linéaire. Cette méthode est dynamique, c'est à dire qu'elle est effectuée en même temps que l'exécution du programme. Cette propriété est nécessaire pour pouvoir limiter l'occupation mémoire. Son occupation mémoire est par ailleurs très limitée puisque principalement dépendante de la taille des caches de la plate-forme matérielle. Pour permettre ce passage à l'échelle, la méthode proposée utilise une information supplémentaire par rapport aux méthodes classiques.Nous avons implanté la méthode proposée au dessus d'un environnement générique de traitement de trace issu de la simulation d'un prototype virtuel qui a été devéloppé durant cette thèse. Cet environnement permet la mise en relation, efficacement, d'événements effectués par différents composants (processeurs, caches, mémoires) d'un la plate-forme matérielle. La pertinence de la solution proposée a été évalué expérimentalement en analysant le comportement de différents programmes exécutés par des plateformes matérielles simulées contenant différents nombres de processeurs. / Verifying memory consistency (VMC) allow to check if the an execution of a program by a hardware platform was executed in compliance with a given memoryc consistency model (MCM). A MCM defines properties about memory acceses, particularly about the interleaving of accesses generated by several processors. In order to solve this complex problem with lineary complexity, lots of information about the program execution are needed: the order of write acceses to every memory cell is indeed needed. Existing solutions do not scale due to memory usage requirement. In this thesis, we propose a VMC method which can be used in the context of virtual prototyping. This method is dynamic, meaning it is done during program execution. This is a requirement in order to limit the memory usage. the achieved memory usage is very reasonable since it mostly depends on the size of caches included in the platform. In order to scale with the length of the program execution, the proposed method use additional informations which can be retreived by using virtual prototyping. We have implemented the proposed method with a genric framework for trace processing which was developped during this thesis. This framework allows to keep links between related events traced by differents components of the hardware platform. The proposed method has been evaluated by analysing the behaviour of several programs executed on several virtual platforms which include differents processor count.
| Identifer | oai:union.ndltd.org:theses.fr/2013GRENM079 |
| Date | 12 June 2013 |
| Creators | Hedde, Damien |
| Contributors | Grenoble, Pétrot, Frédéric |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | French |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.0017 seconds