Sobre a especificação e verificação do padrão de programação paralela PCR em TLA+
DOI:
https://doi.org/10.36561/ING.24.8Palavras-chave:
Algoritmos paralelos, Padrões de design, Métodos Formais, TLAResumo
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.
Downloads
Referências
Asanovic, K. et al; A view of the parallel computing landscape, Commun. ACM, 2009. 52(10) : p. 56–67.
Pérez, G. y Yovine, S.; Formal specification and implementation of an automated pattern-based parallel-code generation framework, STTT, 2017. 21(2) : p. 183–202.
Lamport, L.; Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, 2002, Addison-Wesley Longman Publishing.
Yu, Y. et al; Model Checking TLA+ Specifications, Correct Hardware Design and Verification Methods, 1999. 1703 : p. 54–66.
Cousineau, D. et al.; TLA+ Proofs, FM 2012: Formal Methods, 2012. 7436 : p. 147–154.
Kuppe, M. et al; The TLA+ Toolbox, ArXiv, 2019. p. 50–62.
Lamport, L.; The pluscal algorithm language, Theoretical Aspects of Computing-ICTAC, 2009. 5684 : p. 36–60.
