Análise Comparativa entre dois verificadores de consistência e coerência de memória

Abstract

Para que um sistema de hardware multi-core funcione corretamente é vital que o mesmo tenha a habilidade de preservar a coerência e consistência da sua memória. Logo, durante o seu desenvolvimento, ocorre a verificação de que o resultado da sua execução segue o Modelo de Consistência de Memória (MCM) adotado. A maioria dos verificadores do estado da arte foram criados para serem executados na fase de desenvolvimento em que a partir da qual, definitivamente, não acontecerá a inserção de erros. Isto é, na fase pós-silício onde a classe de complexidade da verificação é NP-difícil. Estes mesmos verificadores também são adaptados para serem utilizados na fase pré-silício, com a perspectiva de redução dos custos do projeto. Entretanto há também verificadores feitos exclusivamente para a fase pré-silício. Eles procuram aproveitar que nesta fase ocorre a queda da complexidade de verificação para a classe Polinomial, devido ao fato de haver mais observabilidade. O presente trabalho tem como objetivo comparar dois verificadores do estado da arte: um feito para a fase pós-silício Hu2012, e outro exclusivo para a fase pré-silício Freitas2013. Referências [Hu2012] Weiwu Hu, Yunji Chen, Tianshi Chen, Cheng Qian, and Lei Li. Linear Time Memory Consistency Verification. IEEE Transactions on Computers, 61(4):502–516, April 2012. [Freitas 2013] LS Freitas, EA Rambo, and LCV dos Santos. On-the-fly verification of Memory consistency with concurrent relaxed scoreboards. DATE ’13 Proceedings of the Conference on Design, Automation and Test in Europe, pages 631–636, 2013.