Algoritmos para verificação de consistência e coerênciade memória compartilhada em multicore chips

Abstract

Este trabalho aborda o problema de verificação de modelos de memória compartilhada em chips multicore (CMP - Chip Multiprocressor) durante o tempo de projeto (pre-silicon checking). Devido a complexidade dos relaxamentos e das otimizações dos modelos de memória, faz-se necessário o desenvolvimento de técnicas de verificação inovadoras. Neste trabalho foram utilizados geradores de testes aleatórios do estado da arte em conjunto com checkers runtime a serem verificados em um simulador de microprocessadores (gem5). O objetivo foi validar e comparar um checker desenvolvido no laboratório do orientador com outros checkers do estado da arte. Este checker inovador (Spec&Check) promete ser mais eficaz que os outros checkers runtime e independente de arquitetura, podendo ser utilizado em uma maior variedade de protocolos. O trabalho do bolsista foi implementar um novo checker estado da arte para servir de baseline, ajudar na realização da verificação e análise, tratamento e formatação dos resultados. Este projeto já rendeu ao bolsista co-autoria de um trabalho aceito em evento internacional qualificado (ICCAD). Agora, com mais resultados devido a inclusão do novo checker implementado pelo bolsista, os dados estão promissores e serão utilizados em uma futura publicação.