Verificación formal del algoritmos de distribución de carga para procesamiento de datos independientes

Los algoritmos de distribución de datos (carga) de procesamiento independiente proveen un conjunto de beneficios a las aplicaciones paralelas tales como: la minimización de su tiempo de ejecución, la maximi-zación de uso de los recursos, etc. Pero por su naturaleza paralela, la implementación de un algoritmo de distribución de datos es compleja lo que puede originar que no cumpla con las especificaciones para las que fue diseñado presentando problemas como: violación a la exclusión mutua, no terminación de la ejecución paralela, abrazos mortales, etc. En esta tesis de maestría, como primer etapa, se propone, modela y verifica formalmente una estructura básica que integra un algoritmo de distribución cíclico en una aplicación SPMD (Simple Program Multiple Data) de procesamiento de datos independientes. Para este proceso de verificación, auxiliándonos de la lógica temporal, se propone un conjunto de propiedades que reflejan un buen funcionamiento del sistema independientemente del algoritmo de distribución usado. La herramienta de verificación utilizada fue Spin, la cual aplica la técnica de verificación de model checking (un método que permite verificar algoritmos paralelos con un espacio de estados finito) y nos permite obtener un diagnóstico del cumplimiento de las propiedades. El sistema se modeló mediante el lenguaje promela utilizado por Spin, realizando la verificación de todas las propiedades especificadas. En la segunda etapa de este proyecto se propone un modelo promela para la verificación de la herramienta DLML (Data List Management Library) basándonos en la estructura propuesta en la primera etapa. DLML es una librería creada en el Laboratorio de Sistemas Distribuidos y Paralelos de la UAM-1 para distribuir la carga (datos) generada por las aplicaciones, de manera transparente para el programador. Para verificar DLML se valida el cumplimiento de las propiedades propuestas y de dos nuevas propie-dades relacionadas a la implementación. Después de verificar el modelo de la versión original de DLML se proponen nuevas implementaciones de este distribuidor, donde se contemplan aspectos como la capacidad de los canales, la no dependencia en la granularidad de los datos y la disminución de la cantidad de mensajes (y con ello mejorar su rendimiento). La versión que muestra mejor rendimiento, nombrada DLML-híbrido, es verificada utilizando las mis-mas propiedades que se verificaron sobre la versión original de DLML. Además se realiza su implementación en lenguaje C-MPI en la que se incorpora el uso de memoria compartida e hilos de ejecución, aprovechan-do el surgimiento de las nuevas arquitectura multicore/multiprocesador ( donde se tiene más de un núcleo (procesador) por nodo). El trabajo de la presente tesis concluye mostrando una comparación de rendimiento de la versión DLML-híbrido con la versión original de DLML, para la cual se utilizaron aplicaciones que manejan datos de gra-nularidad diferente (fina y gruesa). En la comparación se efectúa al utilizar un cluster de 32 nodos de tipo multiprocesador (4 procesadores por nodo, teniendo un total de 128 procesadores). Para la aplicación de gra-nularidad fina DLML-híbrido presenta mejores tiempos de ejecución mientras más procesadores se utilizan. La versión DLML original para este caso obtiene mejores tiempos de ejecución con un número menor de procesadores y pierde eficiencia cuando el número de nodos aumenta. Para la aplicación de granularidad gruesa la versión DLML-híbrido siempre obtiene mejores tiempos de ejecución que la versión original.