Aceleradores e multiprocessadores em chip: o impacto da execução fora de ordem na verificação de funcionalidade e de consistência

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Ciência da Computação, Florianópolis, 2012Este trabalho aborda duas classes de problemas enfrentados na verificação de projetos que exibem comportamentos fora de ordem, especificamente a verificação funcional de aceleradores em hardware e a verificação de consistência em sistemas de memória compartilhada. Comportamentos fora de ordem surgem quando relaxam-se restrições de precedência para aumentar a taxa de uso de componentes de hardware concorrentes e, portanto, aumentar o desempenho. Entretanto, o projeto de um sistema que apresenta comportamentos fora de ordem é suscetível a erros pelo fato de o relaxamento de ordem requerer controle sofisticado. Este trabalho compara as garantias de verificação de três classes de checkers dinâmicos para módulos com suporte a eventos fora de ordem. Comprovadamente, scoreboards relaxados podem ser construídos com plenas garantias de verificação contanto que utilizem regras de atualização baseadas na remoção de dominadores. Resultados experimentais mostram que um scoreboard relaxado assim projetado requer aproximadamente 1/2 do esforço exigido por um scoreboard convencional. Verificar a conformidade do hardware com um modelo de consistência é um problema relevante cuja complexidade depende da observabilidade dos eventos de memória. Este trabalho também descreve uma nova técnica de verificação de consistência de memória on-the-fly a partir de uma representação executável de um sistema multi-core. Para aumentar a eficiência sem afetar as garantias de verificação, são monitorados três pontos por núcleo, ao invés de um ou dois, como proposto em trabalhos correlatos anteriores. Os três pontos foram selecionados para serem altamente independentes da microarquitetura do core. A técnica usa scoreboards relaxados concorrentes para detectar violações em cada core. Para detectar violações globais, utiliza-se a ordem linear de eventos induzida por um caso de teste. Comprovadamente, a técnica não induz falsos positivos nem falsos negativos quando o caso de teste expõe um erro que afeta as sequências monitoradas, tornando-se o primeiro checker on-the-fly com plenas garantias de verificação. Resultados experimentais mostram que ele requer aproximadamente 1/4 a 3/4 do esforço global exigido por um checker post-mortem que monitora duas sequências por processador. A técnica é pelo menos 100 vezes mais rápida do que um checker que monitora uma única sequência por processador.Abstract : This work addresses two classes of problems faced when verifying designs exhibiting out-of-order behaviors, namely the functional verification of hardware accelerators and the verification of consistency in shared-memory systems. Out-of-order behaviors result from relaxing precedence constraints to increase the usage rate of concurrent hardware components and, therefore, lead to a performance improvement. However, the design of a system handling out-of-order behaviors is error prone, since order relaxation asks for sophisticated control. This work compares the verification guarantees of three classes of dynamic checkers for modules handling out-of-order behaviors. Provenly, relaxed scoreboards can be built with full verification guarantees, as far as they employ an update rule based on the removal of dominators. Experimental results show that such a relaxed scoreboard needs approximately 1/2 of the effort required by a conventional one. Verifying the hardware compliance with a consistency model is a relevant problem, whose complexity depends on the observability of memory events. This work also describes a novel on-the-fly technique for verifying memory consistency from an executable representation of a multi-core system. To increase efficiency without hampering verification guarantees, three points are monitored per core, instead of one or two, as proposed in previous related works. The points were selected to be largely independent from the core#s microarchitecture. The technique relies on concurrent relaxed scoreboards to check for consistency violations in each core. To check for global violations, it employs a linear order of events induced by a given test case. Provenly, the technique neither indicates false negatives nor false positives when the test case exposes an error that affects the sampled sequences, making it the first on-the-fly checker with full guarantees. Experimental results show that it needs approximately 1/4 to 3/4 of the overall verification effort required by a post-mortem checker sampling two sequences per processor. The technique is at least 100 times faster than a checker sampling a single sequence per processor