Accélération de plates-formes Java embarquées : techniques et cadre formel

Depuis quelques années, on assiste à une expansion fulgurante du marché des terminaux mobiles et sans fil. Dans ce cadre, le déploiement de la technologie Java sur ce type de terminaux connaît un grand succès à cause de ses caractéristiques attrayantes, à savoir la mobilité, la portabilité et la sécurité. En particulier, la plate-forme J2ME/CLDC (Java 2 Micro Edition for Connected Limited Device Configuration) est dédiée au développement d’applications Java qui s’exécutent sur des téléphones cellulaires, des assistants digitaux et de façon générale sur tous les systèmes embarqués dans des appareils électroniques ou industriels. Par ailleurs, la plate-forme J2ME est dotée d’une version allégée de la machine virtuelle Java, appelée KVM (Kilobyte Virtual Machine). Comme toutes machines virtuelles Java, le principal inconvénient de la KVM est sa lenteur d’exécution due au mécanisme d’interprétation. Par conséquent, il y a un besoin réel de disposer de techniques d’accélération qui permettent d’améliorer la performance de la KVM, étant données les contraintes matérielles des plates-formes Java mobiles (ressources mémoire restreintes, puissance de traitement limitée et faible batterie). C’est dans ce contexte particulier que nous abordons la problématique de l’accélération d’une machine virtuelle dédiée à une plate-forme Java mobile. Dans le cadre de cette thèse, nous proposons de concevoir et d’implanter des techniques d’accélération de la machine virtuelle Java pour la plate-forme J2ME/CLDC. Nous proposons également d’élaborer un cadre sémantique pour capturer de manière formelle le langage de bytecode de la plate-forme J2ME/CLDC. Les principaux résultats qui nous ont permis d’atteindre nos objectifs sont : 1. La conception et l’implantation d’un compilateur dynamique sélectif qui accélère la KVM d’un facteur de 400%. également, des techniques accélérant l’appel de méthodes ont été conçues et implantées. 2. élaboration d’un cadre formel dans un style dénotationnel par passage de continuations supportant les aspects intrinsèques du langage Java, à savoir : parallélisme, le non-déterminisme non borné, les structures d’échappement et les données. 3. Spécification du langage de bytecode de la plate-forme J2ME/CLDC dans le cadre sémantique élaboré.Nowdays, we are witnessing a high expansion of the mobile and wireless devices market. In this context, the Java technology is emerging as a standard execution environment due to its appealing features such as mobility, portability and security. In particular, The J2ME/CLDC platform (Java 2 Micro Edition for Connected Limited Device Configuration) is dedicated to the Java application development for mobile devices and embedded systems. The J2ME/CLDC platform is equipped with a light Java virtual machine, called KVM (Kilobyte Virtual Machine). The main issue of this virtual machine is its performance due to the interpretation mechanism. Consequently, there is a real need to design and implement acceleration techniques for the KVM. Moreover, constraints of wireless and mobile devices in terms of footprint, computation and energy consumption should be considered in the design of these techniques. The main objectives of this thesis are the design and the implementation of acceleration techniques dedicated to the Java virtual machine for the J2ME/CLDC platform. We also intent to elaborate a semantic model to formally capture the bytecode language of the J2ME/CLDC platform.The main research results that achieved these objectives are : 1. The design and implementation of a dynamic selective compiler that speeds up the KVM by a rate of 400%. Other acceleration techniques has been designed and implemented to enhance the method call mechanism. 2. The elaboration of a denotational semantic model with continuations that supports the particular features of the Java language : concurrency, unbounded nondeterminism, escaping constructs and data. 3. The specification of the bytecode language of the J2ME/CLDC platform in the elaborated semantic model