Un marco unificado para análisis de recursos y tiempo de ejecución, validación dinámica y pruebas unitarias = a Unified Framework for Resource and Execution Time Analysis, Run-Time Checking and Unit-Testing

摘要

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 byte- code. 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 bytecode. Además, dado que no podemos verificar todas las propiedades estáticamente, presentamos 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 la ausencia de fallo, el determinismo y las de estado (o funcionales) como 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 errores en el código fuente del sistema Ciao. El marco completo ha sido integrado con éxito en el sistema Ciao/CiaoPP. Abstract We have developed a general framework for automatically inferring both upper- and lower-bounds on the usage that a logic program makes of resources in general. Such bounds are given as functions of input data sizes. Our approach gives support for platform-independent (or user-de_ned/application- dependent) resources, such as bits sent or received by an application over a socket, number of calls to a predicate, number of _les left open, number of accesses to a database, as well as platform-dependent resources, such as execution time or energy. The framework includes a global analysis that is parametric with respect to resources and the type of approximation (lowerand upper-bounds). The user can de_ne the parameters of the analysis for a particular resource using assertions. It is also possible to associate basic cost functions with elementary program operations that a_ect the usage of such resource. Then, the global static analysis can infer the cost of all the procedures in the program. The assertions can be de_ned at di_erent abstraction levels. For example, they can associate resource usage functions to di_erent program constructs at source code level, can also describe how predicates update the value for those resources in the clause heads or in the preparation of the execution of its body literals. In such a case, a cost function de_ned in the assertion is used by the analyzer to update the resource usage when the clause heads or the body literals are analyzed. For platform-dependent resources (e.g., execution time) we perform a one-time pro_ling phase that computes parameters associated to basic operations, at source or bytecode-level. We have applied the general framework to execution time estimation in two ways and experimented with information supplied at source and bytecode-levels. In the _rst approach, the compiletime cost bounds analysis gives a vector of platform-independent resources that corresponds to particular low-level operations related to program execution. Such operations must be reected in the high-level language. The pro_ling phase determines the values of the constants appearing in the resource usage functions, for a given platform. Then, we use assertions to de_ne the platform-dependent resource (execution time) as a composition of the basic platform-independent resources and the values of the constants resulting from the pro_ling phase. In the second approach, the one-time pro- _ling stage calculates constants and functions bounding the execution time of each abstract machine instruction. Then, the compile-time resource usage estimation phase uses the instruction timing information (which is platformdependent) to infer bounds on execution time. To improve precision, resource usage assertions can also be given at bytecode level. Furthermore, since not all properties can be veri_ed statically, we have developed a framework that uni_es static veri_cation, run-time checking and unit testing. In that sense, we have designed methods for compiling run-time checks for (parts of) assertions which cannot be veri_ed at compile-time. Unit tests also provide test cases for the run-time checks, and (parts of) unit tests that can be veri_ed at compile-time are eliminated. In addition to those resource-related properties, we support other properties like non-failure, determinism and state (or functional) properties like types of input/output arguments on calls or successes. A key contribution of this work is that we preserve the use of a uni_ed assertion language for all tasks. Such language is used to de_ne resources and resource-related properties that can be veri_ed based on the results of the analysis and is powerful, general and extensible enough to express a large class of interesting properties. Applications of this work include resource usage veri_cation, performance debugging, certi_cation of resource usage properties in mobile code, resource and granularity control in parallel/distributed computing and resourceoriented specialization. The unit-testing and run-time checking framework has been e_ectively applied to the validation of ISO Prolog compliance and to the detection of di_erent types of bugs in the Ciao source. The overall uni_ed framework has been successfully integrated in the Ciao/CiaoPP system.