Sobre la especificación y verificación del patrón de programación paralela PCR en TLA+

Resumen

Limitaciones físicas en el diseño de microprocesadores han hecho que la industria de computadoras pase de mejorar la velocidad de un solo procesador a aumentar el número de unidades centrales de procesamiento. Pero el diseño de software para explotar la potencia de procesamiento paralelo de manera correcta y efectiva es una tarea desafiante que requiere un alto grado de experiencia. En 2017, Pérez y Yovine propusieron un patrón de programación paralela agnóstico de plataforma llamado PCR, que facilita la escritura de código paralelo. En este trabajo, formalizamos el patrón PCR en términos de TLA+ - un lenguaje de especificación formal para sistemas concurrentes que se está utilizando en lugares como Intel, Amazon y Microsoft. Buscamos proporcionar un marco formal principalmente para (1) expresar diseños PCR de alto nivel y probar su corrección funcional en el sentido de que su computación paralela calcula una función matemática dada, y (2) poder relacionar formalmente diferentes diseños PCR. De esta manera, contribuimos al estado del arte en la verificación formal de programas paralelos aprovechando las herramientas asociadas a TLA+ para probar propiedades sobre algoritmos PCR de alto nivel, como su corrección funcional y refinamiento.