IRL - Vérification de la traduction binaire dynamique

De Ensiwiki
Aller à : navigation, rechercher


Vérification de la traduction binaire dynamique

Labo TIMA
Equipe System Level Synthesis
Encadrants frederic.petrot@univ-grenoble-alpes.fr,laurence.pierre@univ-grenoble-alpes.fr

Contexte

Il existe différentes techniques de simulation d'un jeu d'instructions d'un processeur (dit cible) sur un autre processeur (dit hôte). La plus simple est l'interprétation instruction par instruction (ISS pour instruction set simulator), mais elle est très lente, car il faut entre 300 et 500 instructions hôtes pour exécuter une instruction cible. Pour palier cette lenteur, des génies (le mot n'est pas trop fort) ont remarqué que si l'on exécute une certaine instruction, toutes celles qui suivent sont également exécutées, sauf si c'est un branchement : c'est, simplifiée, la notion de *basic block*. On va alors produire du code hôte *basic block* par *basic block*, et l'exécuter. Résultat des courses, on gagne un facteur 10+ par rapport à l'interprétation classique. L'archétype du traducteur binaire dynamique est QEMU [www.qemu.org]

Objectif

L’objectif de ce projet est de définir une méthode, préférentiellement formelle ou semi-formelle, qui permette de s'assurer que le code généré par le traducteur binaire dynamique réalise bien le même comportement que le code produit par le compilateur sur la cible.

Le travail attendu consiste dans un premier temps à faire un état de l'art ciblé sur la vérification des simulateurs de jeux d'instructions au sens large, et, sur cette base, de proposer une stratégie de vérification pour la traduction binaire dynamique (DBT pour dynamic binary translation), pour un sous-ensemble à définir des instructions cibles. Par ex. les accès mémoire et les sauts nécessitent l'appel à un *run-time* pour gérer la traduction d'adresses et les valeurs du pointeur d'instructions dans l'hôte. La méthode pourra être testée opérationnellement (à la main ou automatisée en fonction de l'avancement) sur QEMU traduisant du code RISC-V sur x86-64.

Prérequis

Intérêt pour la vérification formelle et les aspects bas niveau de l'informatique (assembleur, compilation)