Trabajo de Grado - Gastón Ingaramo y Matías Tealdi

El martes 17 de diciembre de 2013 a las 10:00 hs. en el auditorio de la FaMAF, Matías Tealdi y Gastón Ingaramo defenderán sus respectivos trabajos de grado.

Ambos trabajos implementan versiones paralelizadas masivamente sobre GPGPU de los algoritmos numéricos Jacobi y Gauss-Seidel que se ejecutan en el back-end de la herramienta de verificación PRISM.

Debajo pueden encontrar los resúmenes de los respectivos trabajos.

Título: Paralelización de algoritmos para verificación simbólica de modelos probabilísticos.
Alumno: Matías D. Tealdi
Directores: Carlos Bederián y Pedro R. D’Argenio

Resumen: La verificación de modelos es una técnica útil para el análisis de modelos complejos. En particular, la verificación de modelos probabilísticos se basa en una especificación formal de un sistema que presenta comportamientos probabilísticos o estocásticos y una propiedad lógica. Esta propiedad es evaluada automáticamente para detectar posibles fallas, posibilitando el análisis cuantitativo del sistema.
La principales variables que afectan el alcance de esta técnica son los tamaños de los modelos y la complejidad computación de los cálculos numéricos involucrados. La verificación simbólica ataca el tamaño de los modelos con estructuras de datos compactas. Aún así, los cálculos numéricos demandan una gan cantidad de recursos computacionales.
La motivación de este trabajo es mejorar los tiempos de ejecución de los algoritmos numéricos, específicamente el método de Jacobi, a través de la arquitectura de GPU computing sin perder los beneficios, antes nombrados, de las estructuras simbólicas.

Título: Implementación del algoritmo Gauss-Seidel en CUDA para la verificación simbólica de modelos probabilísticos.
Alumno: Gastón Ingaramo
Directores: Carlos Bederián y Pedro R. D’Argenio

Resumen: La necesidad de verificar protocolos o sistemas críticos antes de que puedan causar algún daño o accidente es lo que dio nacimiento a las herramientas verificadoras de modelos. Primero se especifica formal- mente el modelo a verificar y luego se selecciona una de las tantas lógicas para la verificación de sus propiedades. Centraremos nuestra atención en los modelos probabilísticos y en su verificación utilizando estructuras de datos simbólicas construyendo nuestro trabajo sobre el model checker PRISM.
El alto requerimiento de calculo aritmético para la implementación de operadores de las distintas lógicas fue lo que nos llevó a explorar soluciones utilizando GPUs que ya han demostrado ser muy útiles para tales fines.
Presentaremos los distintos lenguajes para el modelado de sistemas, para sistemas de tiempo discreto y tiempo continuo, DTMC y CTMC respectivamente. Luego estudiaremos las lógicas correspondientes para su verificación prestando especial atención a los operadores que requieren de multiplicaciones matriz-vector. Explicaremos como es que PRISM, el model checker simbólico utilizado, implementa estos operadores y que estructuras de datos utiliza.
Finalmente presentaremos nuestra implementación de un algoritmo pseudo Gauss-Seidel en arquitecturas GPGPU, principalmente en CUDA. Haremos dos distinciones, cuando la memoria de la tarjeta es suficiente para contener todos los vectores y cuando se requiere particionar el problema.