Sergio Yovine - Generación semi-automática de software paralelo usando transformaciones formales de programas

Resumen:
Desde que la industria del hardware se volcó al desarrollo de arquitecturas con múltiples procesadores de múltiples núcleos, la explotación de la performance no pasa más por una compilación inteligente del software secuencial, sino por el diseño y la programación de software explícitamente paralelo. Este cambio de paradigma, aunque en principio tecnológico, trajo consigo un conjunto de problemas teóricos y prácticos que necesitan ser estudiados en profundidad y resueltos. Estos problemas están ligados, en particular, a la complejidad intrínseca que reviste la producción eficaz de software concurrente correcto y eficiente, lo que impacta fuertemente a todas las etapas del proceso de desarrollo: modelado, diseño, programación, análisis de performance, verificación de corrección, testing y debugging. En efecto, los programas paralelos son muy propensos a tener errores difíciles de reproducir y costosos de corregir, como consecuencia del indeterminismo de las ejecuciones concurrentes. Además, las aplicaciones a gran escala utilizan arquitecturas paralelas heterogéneas, lo que requiere combinar diferentes paradigmas de computación concurrente. La proliferación de modelos de cómputo paralelo y de lenguajes de programación paralela complica aún más el panorama. En este contexto, hay consenso sobre la necesidad de diseñar nuevos lenguajes de programación que ataquen conjuntamente los problemas de corrección, eficiencia y productividad, a partir de principios fundamentales y no extendiendo lenguajes existentes. De todas maneras, estos lenguajes no liberan completamente al programador de cometer errores, cuya detección tardía y corrección son responsables en gran medida de los costos de producción de software, reduciendo así la productividad.

Entendemos que una manera de contribuir a paliar estos problemas es desarrollar herramientas automáticas o semi-automáticas basadas en formalismos de especificación que permitan 1) capturar los conceptos fundamentales del paralelismo de manera abstracta y 2) generar código mediante el uso de transformaciones formales. En esta charla presentaremos FXML, un formalismo que provee una plataforma inicial que puede ser extendida mediante el agregado de construcciones paralelas más concretas. Esto permite estudiar diferentes implementaciones de una especificación mediante transformaciones que garantizan la corrección y dan predicciones de performance. Además de los resultados obtenidos, abordaremos temas de investigación en curso y la agenda a corto y mediano plazo.