Autor/es

Solsona, José E.

En

Editor

Universidad de Montevideo

Notas

Physical limitations in processor design have made the computer industry shift from improving the speed of a single processor to increasing the number of processing core units. But the design of software to exploit parallel processing power in a correct and cost-effective way is a challenging task requiring a high degree of expertise. In 2017, Pérez and Yovine proposed a platform-agnostic parallel programming pattern called PCR, that eases writing parallel code. In this work, we formalize the PCR pattern in terms of TLA+ - a formal specification language for concurrent systems that is being used at places such as Intel, Amazon and Microsoft. We seek to provide a formal framework mainly for (1) expressing high level PCR designs and prove their functional correctness in the sense that their parallel computation computes a given mathematical function, and (2) being able to formally relate different PCR designs. In this way, we contribute to the state of the art in formal verification of parallel programs by leveraging TLA+-related tools to proving properties about high-level PCR-based algorithms such as their functional correctness and refinement.

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.

As limitações físicas no design do processador fizeram com que a indústria de computadores mudasse de melhorar a velocidade de um único processador para aumentar o número de unidades centrais de processamento. Mas o design de software para explorar o poder de processamento paralelo de maneira correta e econômica é uma tarefa desafiadora que requer um alto grau de especialização. Em 2017, Pérez e Yovine propuseram um padrão de programação paralela independente de plataforma chamado PCR, que facilita a escrita de código paralelo. Neste trabalho, formalizamos o padrão PCR em termos de TLA+ - uma linguagem de especificação formal para sistemas concorrentes que está sendo utilizada em locais como Intel, Amazon e Microsoft. Procuramos fornecer uma estrutura formal principalmente para (1) expressar designs de PCR de alto nível e provar sua correção funcional no sentido de que sua computação paralela calcula uma determinada função matemática e (2) ser capaz de relacionar formalmente diferentes designs de PCR. Dessa forma, contribuímos para o estado da arte na verificação formal de programas paralelos, aproveitando as ferramentas relacionadas ao TLA+ para provar propriedades sobre algoritmos baseados em PCR de alto nível, como correção e refinamento funcional.

Palabras claves

Algoritmos paralelos Patrones de diseño Métodos formales TLA

Colecciones

• Memoria Investigaciones en Ingeniería [227]