QUATRIX

QUATRIX

Quantitative Analysis Tools for Resource-Intensive Constrained Systems

Funded by MINCyT-INRIA-CNRS grant

Philippe Clauss, Université de Strasbourg

Sergio Yovine, Universidad de Buenos Aires

Objetivos

El interés de este proyecto está en la generación de nuevo conocimiento y herramientas para la inferencia automática de propiedades cuantitativas sobre programas desarrollados en lenguajes imperativos, con orientación a objetos y concurrencia. Conocer este tipo de propiedades permite calcular de antemano los recursos (e.g., memoria dinámica, tamaño de buffers de comunicación) necesarios para desplegar una aplicación sobre una plataforma de ejecución para que pueda ejecutarse sin errores (e.g., out-of-memory, buffer overflow). También permite comparar diferentes implementaciones de la misma especificación funcional de acuerdo a criterios de calidad cuantitativos tales como performance, consumo de memoria, costo de comunicaciones, etc.

Particularmente nos interesa obtener información sobre el consumo de memoria dinámica de programas concurrentes. Este interés se debe a diversas razones.

  • Es notorio que los sistemas embebidos tienen limitaciones de memoria. Por ende, es de fundamental importancia poder cuantificar a priori los requerimientos mínimos y máximos de memoria que el programa va a necesitar para ejecutarse, para poder dimensionar el hardware (en el caso de un co-desarrollo software/hardware) o determinar si la capacidad de memoria de la arquitectura objetivo es suficiente.
  • El tiempo de ejecución de un programa debido al manejo de memoria dinámica es impredictible. Esto es impensable en el contexto de aplicaciones de tiempo real. Sin embargo, es sabido que disponer de una especificación del consumo de memoria de un programa permite recurrir a estrategias de gestión basadas en regiones que brindan garantías de tiempo de ejecución predictibles y acotados.
  • La introducción de procesadores multinúcleo en el ámbito de los sistemas embebidos trae aparejado la programación de aplicaciones concurrentes. La gestión de la memoria dinámica tiene un impacto muy importante en la planificación de las tareas dado que introduce pausas cuya duración, cantidad y lugar de ocurrencia no son predictibles. En este sentido, cuantificar el consumo de memoria y determinar el tiempo de vida de los objetos permite automatizar la generación de planificadores con garantías de tiempo real para programas concurrentes.

    El desafío de cuantificar el uso de memoria dinámica en programas orientados a objeto concurrentes (como Java, C++ y C#) es doble. Primero, a diferencia de otro tipo de propiedades cuantitativas (por ejemplo: tiempo de ejecución), el consumo de memoria evoluciona de forma no monótona con respecto al tiempo (dado que cierta porción de la memoria puede ser liberada durante la ejecución por el gargabe collector) por lo que su análisis es más complejo. Segundo, la combinación de memoria dinámica con concurrencia es explosiva en cuanto a la complejidad de las técnicas de análisis. Por eso, si bien ya hubo algunos resultados teóricos y prácticos para producir estimaciones de consumo de memoria dinámica, los mismos no son escalables ni usables por una persona inexperta. Es decir, su aplicación está limitada a programas relativamente simples y/o su uso en software complejo es penoso. Por otro lado, no conocemos ninguna técnica de análisis cuantitativo de programas concurrentes.

    El objetivo de este plan de trabajo es concebir un conjunto de técnicas de análisis estático (del código fuente) y dinámico (de las ejecuciones) de software concurrente orientado a objetos, que sean escalables y usables, y que permitan la obtención de requisitos cuantitatvos precisos de consumo de memoria. Estas técnicas deben poder soportar aplicaciones de un tamaño mediano a grande. En particular, para la validación experimental de los resultados, pensamos utilizar las mismas para analizar el software de código abierto y libre de derechos Ginga, usado como plataforma middleware de los decodificadores para la Televisión Digital Interactiva de la norma adoptada por el Sistema Argentino de Televisión Digital Terrestre (SATVD-T). Las técnicas que desarrollaremos deben poder ser integrables a las herramientas de desarrollo. Esta integración debe permitir a los programadores la interacción con las técnicas analizando su resultado e incorporando información que permita mejorarlos de manera incremental.

    Resultados esperados

    Una de las principales debilidades de las técnicas actuales radica en su incapacidad de operar de forma composicional. Este problema obliga a que las técnicas resultantes deban operar con un estado global (por ejemplo requiriendo conocer todas las variables que aparecen en el stack) imposibilitando la escalabilidad. Por otro lado los análisis globales no permiten razonar de forma local ni explotar conocimiento del dominio para proveer anotaciones con información relevante (invariantes locales, consumo de métodos, tiempo de vida de los objetos). El otro problema reside en la falta de precisión de las técnicas basadas en un análisis estático del código fuente.

    Para lograr el objetivo propuesto de escalabilidad y usabilidad es necesario desarrollar técnicas modulares de inferencia, que sean capaces de soportar código más complejo en términos de estructuras de datos, tamaño y estructuras de control. Esto implica atacar varios problemas no triviales: diseño de un lengua je de especificación, mecanismos de chequeo e inferencia por análisis estático (de código) y dinámico (de las ejecuciones) de anotaciones de consumo y tiempo de vida de los objetos, y desarrollo de un prototipo de un toolsuite que permita la integración de estas técnicas a un ambiente de programación.

    Los resultados esperados son los siguientes.

  • Lenguaje de especificación de consumo: Se desarrollará un lenguaje para la especificación del consumo de un método en función de sus parámetros contemplando que éstos pueden hacer referencia a estructuras de datos complejas. Se contemplarán mecanismos de ocultamiento de la información para garantizar la modularidad. A su vez se proveerán mecanismos para especificar no sólo consumo de memoria sino también información sobre el tiempo de vida de los objetos. El lenguaje proveerá un nivel de granularidad tal que un cliente del método (es decir, alguien que lo llame) sea capaz de razonar sobre su consumo a partir de su propio comportamiento local y de la información suministrada en la especificación del método que él llama.
  • Técnicas composicionales de inferencia de anotaciones de consumo y tiempo de vida para inferir automáticamente las anotaciones que formaran parte de las especificaciones de consumo. Se desarrollarán técnicas capaces de analizar en forma detallada la parte local del método. Para las llamadas a otros métodos las técnicas deben ser capaces de utilizar las anotaciones de los métodos llamados, vinculando y convirtiendo la información abstracta del método llamado en información concreta del método llamador. Es deseable que estas técnicas sean agnósticas al lenguaje de programación de orígen, maximizando su aplicabilidad en distintos códigos fuentes.
  • Técnicas de verificación de las anotaciones de consumo y tiempo de vida provistas por el usuario. Recordemos que los problemas de consumo y de tiempo de vida son indecidibles. Esto quiere decir que es teóricamente imposible predecir con exactitud cuánta memoria dinámica necesitará un programa para ejecutarse y en qué momento durante su ejecución un objeto dejará de ser referenciado. Por esto, las técnicas de inferencia pueden resultar en aproximaciones demasiado groseras (por ejemplo, cotas infinitas). Por esta razón, la idea es combinarlas con anotaciones provistas por el usuario, cuya validez deberá ser verificada, lo que se justifica porque en general verificar es más fácil que inferir. Para esto se desarrollarán técnicas de verificación de dichas anotaciones basadas en análisis estático (seguro, porque predica sobre todas las eventuales ejecuciones, pero sobreaproximado) y dinámico (exacto, porque está basado en ejecuciones reales, pero inseguro). Las anotaciones validadas permitirán refinar (es decir, hacer más preciso) el resultado de la inferencia. Cabe notar que desarrollar una técnica de verificación de anotaciones es un desafío en si mismo ya que las anotaciones, en general, contienen información que las técnicas de inferencia no lograron obtener (por la indecibilidad del análisis estático).

    Investigadores

    Argentina
    Sergio Yovine, Coordinador
    Diego Garbervetsky, Profesor
    Gervasio Pérez, Doctorando
    Luis Mastrangelo, Tesista de licenciatura

    Francia
    Philippe Clauss, Coordinador
    Alain Ketterlin, Profesor
    Vincent Loechner, Profesor
    Alexandra Jamborean, Doctorando
    Benoit Pradelle, Doctorando

    • Undefined