Tesis:
Un marco unificado para análisis de recursos y tiempo de ejecución, validación dinámica y pruebas unitarias.
- Autor: MERA MENENDEZ, Edison Fernando
- Título: Un marco unificado para análisis de recursos y tiempo de ejecución, validación dinámica y pruebas unitarias.
- Fecha: 2010
- Materia: Sin materia definida
- Escuela: FACULTAD DE INFORMATICA
- Departamentos: INTELIGENCIA ARTIFICIAL
- Acceso electrónico: http://oa.upm.es/9886/
- Director/a 1º: LOPEZ GARCIA, Pedro
- Resumen: Hemos desarrollado un marco general para inferir automáticamente cotas superiores e inferiores del uso que un programa lógico hace de los recursos en general, dadas como funciones de los tamaños de los datos de entrada. Este permite el tratamiento de recursos independientes de la plataforma (o definidos por el usuario/dependientes de la aplicación), tales como los bits enviados o recibidos por una aplicación a través de un socket, el número de llamadas a un predicado, archivos que se dejan abiertos, accesos a una base de datos, así como otros dependientes de la plataforma, como tiempo de ejecución o consumo de energía. El trabajo incluye un análisis global paramétrico respecto a los recursos y el tipo de aproximación (cotas superiores e inferiores). El usuario puede definir los parámetros del análisis para un recurso mediante aserciones, así como asociar costes a las operaciones básicas del programa que afectan el uso de dicho recurso. El análisis estático global infiere el uso del recurso para todas las partes del programa. Las aserciones pueden definirse a diferentes niveles de abstracción. Por ejemplo, pueden asociar funciones del uso de recursos para diferentes tipos de programas a nivel del código fuente y pueden describir también cómo se actualiza el valor de dichos recursos en las cabezas de los predicados o en la preparación de un literal en el cuerpo de dichos predicados. En este caso, el analizador usa una función de coste definida en la aserción para actualizar el uso del recurso mientras se analizan las cabezas de las cláusulas o los literales del cuerpo. Para los recursos dependientes de la plataforma, como el tiempo de ejecución, realizamos una única vez por plataforma un perfilado que calcula los parámetros asociados a operaciones básicas, a nivel de código fuente o bytecode. Hemos aplicado el marco general a tiempo de ejecución de dos maneras y experimentado con la información suministrada a nivel de fuente y de byte-code. En el primer enfoque, el análisis estático devuelve un vector de recursos independiente de la plataforma relacionado con las operaciones de bajo nivel de la ejecución del programa. Dichas operaciones deben verse reflejadas en el lenguaje de alto nivel. El perfilador calcula las constantes que aparecen en las funciones de recursos de la plataforma dada. A continuación usamos aserciones para definir el tiempo de ejecución como un recurso compuesto de los recursos independientes de la plataforma y los resultados del perfilado. En el segundo enfoque, en la etapa de perfilado se calculan las constantes y funciones que acotan el tiempo de ejecución de cada instrucción de la máquina abstracta. A continuación, en la etapa de estimación de recursos se emplea la información de dichos tiempos para inferir cotas del tiempo de ejecución, dependientes de la plataforma. También el resultado puede mejorarse introduciendo aserciones a nivel de byte-code. Además, dado que no podemos verificar todas las propiedades estática- mente, presentarnos un marco unificado para verificación estática, validación dinámica (o en tiempo de ejecución) y pruebas unitarias. Hemos diseñado métodos para compilar validaciones dinámicas de (parte de) las aserciones que no pueden ser verificadas estáticamente. Las pruebas unitarias permiten poner a prueba las validaciones dinámicas y (parte de) las pruebas verificadas estáticamente se eliminan. Además de las propiedades relacionadas con recursos, podemos tratar otras como el no fallo, el determinismo y las de estado (o funcionales) corno los tipos de los argumentos de entrada/salida. Una contribución importante es que para todas las tareas hemos usado un lenguaje de aserciones unificado, el cual permite definir recursos y propiedades relacionadas y verificables con ayuda de los resultados del análisis que es lo suficientemente poderoso, general y extensible como para expresar una gran variedad de propiedades interesantes de los programas. Entre las aplicaciones del presente trabajo tenemos la verificación del consumo de recursos, depuración del rendimiento, certificación de propiedades para código móvil, control de granularidad en computación paralela/distribuida y especialización de programas orientada por los recursos. El marco para pruebas unitarias y en tiempo de ejecución se ha aplicado con éxito en la validación de la adecuación al estándar ISO-Prolog y en la detección de varios bugs en el código fuente del sistema Ciao. El marco completo ha sido integrado con éxito en el sistema Ciao/CiaoPP.