Modular and Field-Sensitive Termination Analysis of Java Bytecode = Análisis de Terminación Modular y Sensible a los Campos de Código de Byte Java

Ramirez Deantes, Diana (2011). Modular and Field-Sensitive Termination Analysis of Java Bytecode = Análisis de Terminación Modular y Sensible a los Campos de Código de Byte Java. Tesis (Doctoral), Facultad de Informática (UPM) [antigua denominación].

Descripción

Título: Modular and Field-Sensitive Termination Analysis of Java Bytecode = Análisis de Terminación Modular y Sensible a los Campos de Código de Byte Java
Autor/es:
  • Ramirez Deantes, Diana
Director/es:
  • Puebla Sánchez, Alvaro Germán
Tipo de Documento: Tesis (Doctoral)
Fecha: Febrero 2011
Materias:
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (1MB) | Vista Previa

Resumen

En las últimas dos décadas, una variedad de sofisticadas herramientas de análisis de terminación se han desarrollado. Estos incluyen los analizadores para sistemas de reescritura de terminos [GSKT06], lógicos y los de lenguajes funcionales [LS97]. El análisis de terminación [CT99, LJBA01] puede considerarse como otro tipo de análisis de uso de recursos, y también se ha estudiado en el contexto de varios lenguajes de programación. Tradicionalmente, en el contexto de la programación declarativa y, recientemente, para lenguajes imperativos y orientados a objetos (OO). De hecho, existen analizadores de terminación para OO que son capaces de probar terminación de aplicaciones de tamaño medio a través de un análisis global, en el sentido de que se debe demostrar terminación para todo el código usado por esas aplicaciones. Sin embargo, el análisis global tiene desventajas importantes, tales como, su alto consumo de memoria y su falta de eficiencia. Ya que a menudo algunas partes del código tienen que ser analizadas una y otra vez, las librerias son un ejemplo primordial de ello. El análisis modular se ha estudiado en diferentes paradigmas desde la programación lógica [ea04, CPHB06, CDG93] a la programación orientada a objetos [Pro02, BJ03, Log04]. La mayoría de los trabajos existentes que se centran en el análisis modular se aplican a los análisis específicos con propiedades particulares o dominios abstractos. Las herramientas de análisis de terminación se esfuerzan por encontrar pruebas de terminación para la mas amplia clase de programas (que terminen) como sea posible. Aunque existen varias herramientas que son capaces de probar terminación de programas no triviales, cuando se trata de aplicarlos a programas realistas, todavía hay una serie de problemas abiertos. En [AAGP08b] se identifican una serie de dificultades para resolverse con el fin de tratar los campos numéricos en la terminación y se proponer algunas ideas para un análisis ligero que es capaz de probar terminación de programas Java-like secuenciales en presencia de campos numéricos. Técnicas automatizadas para demostrar terminación se basan normalmente en los análisis que mantienen un registro del tamaño de la información, tales como el valor de los datos numéricos o el tamaño de las estructuras de datos. En particular, los análisis deben hacer un seguimiento de cómo (el tamaño de) los datos involucrados en el bucle cambian a través de sus iteraciones. Esta informaci ón se utiliza para especificar una ranking function para el bucle [PR04a], que es una función que disminuye estrictamente en cada iteración del bucle, lo que garantiza que el bucle se ejecutará un número finito de veces. Algunos análisis sensible a los campos se han desarrollado en los últimos años ([Min06, AAGP09]). Para asignar estructuras de datos en el heap, el pathlength [SHP06b] es un dominio abstracto que proporciona una aproximación segura de la longitud de la referencia más larga alcanzable desde las variables de interés. Esto permite probar terminación de los bucles que recorren las estructuras de datos acíclicos tales como listas enlazadas, árboles, etc. Sin embargo, las técnicas propuestas en [AAGP09] para los campos numéricos no son efectivos para los campos de referencia. Porque para el seguimiento de los campos de referencia, replicar los accesos de campo por las variables locales, presenta problemas de aliasing no deseado entre los campos y variables locales. Por otro lado, el enfoque sensible al contexto que se presenta en [AAG+10] es capaz de manejar los campos mediante una transformación polivariante. Static program analysis of object-oriented languages poses some challenges for termination analyzers. One of these challenges is that termination analysis traditionally requires the use of global analysis techniques to prove that the execution of an entry method terminates for any input value. In order to solve this problem, it is necessary to prove termination for all methods invoked from the entry method during its execution. Scalability is an important disadvantage of global analysis, especially in memory consumption, because it needs to analyze over and over again the whole code even if there is a small part modified. It also requires to have the code available, of all methods reachable from the method being analyzed. Some techniques developed to provide a modular termination analysis of a Java program, are presented in an approach that allows a high level of scalability, granularity and reusability to perform termination analysis of incomplete code. This approach is able to decompose large programs into small parts and can reuse previous analysis results. Also it allows reusability and scalability through the use of assertions, to store the analysis results obtained by analyzing a method at a time. Then the assertions generated are applied to the analysis of subsequent methods. Most static analyzers do not keep track of object fields, because they are field-insensitive. This type of analysis produces too imprecise results whereas applying only field-sensitive analysis is computationally intractable. There has been significant interest in developing techniques that result in a good balance between the accuracy of analysis and its associated computational cost. To solve this challenge, an implementation of field-sensitive analysis performed on object fields is presented. This transformation is based on a context-sensitive analysis that splits a program into fragments, to provide a safe way to replace an object field by a local variable in each fragment. Also using a polyvariant transformation achieves, a very good balance between accuracy and efficiency. The modular and field-sensitive termination analyses were developed, implemented and tested in a COSt and Termination Analyzer of java bytecode (costa). An analyzer that receives as entry a method signature and infers termination for all possible input values of its code and related methods. In order to test the applicability of the modular termination framework it has been applied to phoneME core libraries. Based on the implementation of Java Micro Edition (Java ME), that corresponds to the libraries used for developing mobile applications or MIDlets. Also these libraries have been used for estimating execution time of a mobile application, before running it in a specific mobile device. Finally, another contribution of this thesis is the availability of the costa system through a web interface, to allow users try out the system on a set of representative examples, and also to upload their own bytecode programs.

Más información

ID de Registro: 6094
Identificador DC: http://oa.upm.es/6094/
Identificador OAI: oai:oa.upm.es:6094
Depositado por: Archivo Digital UPM
Depositado el: 18 Feb 2011 12:47
Ultima Modificación: 20 Abr 2016 14:43
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM