A Low-Footprint Java-to-Native Compilation Scheme Using Formal Methods

Abstract : Ahead-of-Time and Just-in-Time compilation are common ways to improve runtime performances of restrained systems like Java Card by turning critical Java methods into native code. However, native code is much bigger than Java bytecode, which severely limits or even forbids these practices for devices with memory constraints. In this paper, we describe and evaluate a method for reducing natively-compiled code by suppressing runtime exception check sites, which are emitted when compiling bytecodes that may potentially throw runtime exceptions. This is made possible by completing the Java program with JML annotations, and using a theorem prover in order to formally prove that the compiled methods never throw runtime exceptions. Runtime exception check sites can then safely be removed from the generated native code, as it is proved they will never be entered. We have experimented our approach on several card-range and embedded Java applications, and were able to remove almost all the exception check sites. Results show memory footprints for native code that are up to 70% smaller than the non-optimized version, and sometimes as low than 115% the size of the Java bytecode when compiled for ARM thumb.
Type de document :
Communication dans un congrès
Springer-Verlag. In Seventh Smart Card Research and Advanced Application IFIP Conference (CARDIS'06), Apr 2006, Tarragona, Spain, 2006, LNCS
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00113758
Contributeur : Alexandre Courbot <>
Soumis le : mardi 14 novembre 2006 - 13:33:22
Dernière modification le : samedi 27 janvier 2018 - 01:30:44
Document(s) archivé(s) le : mardi 6 avril 2010 - 22:34:45

Identifiants

  • HAL Id : inria-00113758, version 1

Collections

Citation

Alexandre Courbot, Mariela Pavlova, Gilles Grimaud, Jean-Jacques Vandewalle. A Low-Footprint Java-to-Native Compilation Scheme Using Formal Methods. Springer-Verlag. In Seventh Smart Card Research and Advanced Application IFIP Conference (CARDIS'06), Apr 2006, Tarragona, Spain, 2006, LNCS. 〈inria-00113758〉

Partager

Métriques

Consultations de la notice

321

Téléchargements de fichiers

156