Mostrar el registro sencillo del ítem

On the specification and verification of the PCR parallel programming pattern in TLA+

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

Sobre a especificação e verificação do padrão de programação paralela PCR em TLA+

dc.creatorSolsona, José E.
dc.date2023-06-30
dc.identifierhttp://revistas.um.edu.uy/index.php/ingenieria/article/view/1146
dc.identifier10.36561/ING.24.8
dc.descriptionPhysical 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.en-US
dc.descriptionLimitaciones 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.es-ES
dc.descriptionAs 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.pt-BR
dc.formatapplication/pdf
dc.formatapplication/epub+zip
dc.languagespa
dc.publisherUniversidad de Montevideoes-ES
dc.relationhttp://revistas.um.edu.uy/index.php/ingenieria/article/view/1146/1462
dc.relationhttp://revistas.um.edu.uy/index.php/ingenieria/article/view/1146/1463
dc.rightsDerechos de autor 2023 José E. Solsonaes-ES
dc.sourceMemoria Investigaciones en Ingeniería; No. 24 (2023); 105-116en-US
dc.sourceMemoria Investigaciones en Ingeniería; Núm. 24 (2023); 105-116es-ES
dc.sourceMemoria Investigaciones en Ingenieria; n. 24 (2023); 105-116pt-BR
dc.source2301-1106
dc.source2301-1092
dc.source10.36561/ING.24
dc.subjectAlgoritmos paraleloses-ES
dc.subjectPatrones de diseñoes-ES
dc.subjectMétodos formaleses-ES
dc.subjectTLAes-ES
dc.subjectParallel algorithmsen-US
dc.subjectDesign patternsen-US
dc.subjectFormal Methodsen-US
dc.subjectTLAen-US
dc.subjectAlgoritmos paralelospt-BR
dc.subjectPadrões de designpt-BR
dc.subjectMétodos Formaispt-BR
dc.subjectTLApt-BR
dc.titleOn the specification and verification of the PCR parallel programming pattern in TLA+en-US
dc.titleSobre la especificación y verificación del patrón de programación paralela PCR en TLA+es-ES
dc.titleSobre a especificação e verificação do padrão de programação paralela PCR em TLA+pt-BR
dc.typeinfo:eu-repo/semantics/article
dc.typeinfo:eu-repo/semantics/publishedVersion
dc.typePeer reviewed articlesen-US
dc.typeArtículos evaluados por pareses-ES
dc.typeArtigos revistos por parespt-BR

Ver ítem
FicherosTamañoFormatoVer

No hay ficheros asociados a este ítem.

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem