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. DOI: https://doi.org/10.1145/1562764.1562783
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. DOI: https://doi.org/10.1007/s10009-017-0465-2
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. DOI: https://doi.org/10.1007/3-540-48153-2_6
Cousineau, D. et al.; TLA+ Proofs, FM 2012: Formal Methods, 2012. 7436 : p. 147–154. DOI: https://doi.org/10.1007/978-3-642-32759-9_14
Kuppe, M. et al; The TLA+ Toolbox, ArXiv, 2019. p. 50–62. DOI: https://doi.org/10.4204/EPTCS.310.6
Lamport, L.; The pluscal algorithm language, Theoretical Aspects of Computing-ICTAC, 2009. 5684 : p. 36–60. DOI: https://doi.org/10.1007/978-3-642-03466-4_2
Publicado
Como Citar
Edição
Seção
Licença
Copyright (c) 2023 José E. Solsona
Este trabalho está licenciado sob uma licença Creative Commons Attribution 4.0 International License.
