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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Mulchandani, D.: Java for embedded systems. Internet Computing, IEEE 2(3), 30–39 (1998)
Lagosanto, L.: Next-generation embedded java operating system for smart cards. In: 4th Gemplus Developer Conference (2002)
Grimaud, G., Vandewalle, J.-J.: Introducing research issues for next generation Java-based smart card platforms. In: Proc. Smart Objects Conference (sOc 2003), Grenoble, France (2003)
Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: A developeroriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422–439. Springer, Heidelberg (2003)
Lindholm, T., Yellin, F.: Java Virtual Machine Specification. Addison-Wesley Longman Publishing Co., Inc., Amsterdam (1999)
Ishizaki, K., Kawahito, M., Yasue, T., Takeuchi, M., Ogasawara, T., Suganuma, T., Onodera, T., Komatsu, H., Nakatani, T.: Design, implementation, and evaluation of optimizations in a just-in-time compiler. In: JAVA 1999: Proceedings of the ACM 1999 conference on Java Grande, pp. 119–128. ACM Press, New York (1999)
Proebsting, T.A., Townsend, G., Bridges, P., Hartman, J.H., Newsham, T., Watterson, S.A.: Toba: Java for applications: A way ahead of time (wat) compiler. In: Third USENIX Conference on Object-Oriented Technologies (COOTS), Portland, Oregon, University of Arizona (June 1997)
Muller, G., Moura, B., Bellard, F., Consel, C.: Harissa: a flexible and efficient java environment mixing bytecode and compiled code. In: Third USENIX Conference on Object-Oriented Technologies (COOTS), USENIX, Portland (June 1997)
JC Virtual Machine, http://jcvm.sourceforge.net/
Vall´ee-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot - a java optimization framework. In: Proceedings of CASCON 1999, pp. 125–135 (1999)
Hummel, J., Azevedo, A., Kolson, D., Nicolau, A.: Annotating the Java bytecodes in support of optimization. Concurrency: Practice and Experience 9(11), 1003–1016 (1997)
Azevedo, A., Nicolau, A., Hummel, J.: Java annotation-aware just-in-time (ajit) complilation system. In: JAVA 1999: Proceedings of the ACM 1999 conference on Java Grande, pp. 142–151. ACM Press, New York (1999)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Mller, P., Kiniry, J.: JML Reference Manual (July 2005)
Pavlova, M.: Java bytecode logic and specification. tech. rep., INRIA, Sophia- Antipolis, Draft version (2005)
Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)
Java In The Small, http://www.lifl.fr/RD2P/JITS/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Courbot, A., Pavlova, M., Grimaud, G., Vandewalle, JJ. (2006). A Low-Footprint Java-to-Native Compilation Scheme Using Formal Methods. In: Domingo-Ferrer, J., Posegga, J., Schreckling, D. (eds) Smart Card Research and Advanced Applications. CARDIS 2006. Lecture Notes in Computer Science, vol 3928. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11733447_24
Download citation
DOI: https://doi.org/10.1007/11733447_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33311-1
Online ISBN: 978-3-540-33312-8
eBook Packages: Computer ScienceComputer Science (R0)