Shared memory verification for multicore chip designs

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, 2020.Multiprocessadores em um único chip, conhecidos como multicores, normalmente proveem uma abstração de memória compartilhada coerente, a qual pode ser obtida por meio da implementação de protocolos de coerência de cache no hardware. Já foi mostrado que a coerência implementada em hardware pode ser escalável em relação ao aumento do número de núcleos. Além disso, arquiteturas multicore podem adotar grande relaxação das restrições de consistência sobre a atomicidade de escrita e sobre o ordenamento entre leituras e escritas. Como resultado, a validação de memória compartilhada em multicore chips enfrenta dois desafios principais: o maior número de comportamentos válidos de execução, resultante da relaxação da consistência, e o maior espaço de estados do protocolo de coerência, induzido pelo crescente número de núcleos. No nível microarquitetural, o esforço de validação baseia-se em verificação funcional contando com a simulação da representação de projeto. A geração de testes litmus é uma abordagem efetiva para expor erros de consistência, sem a necessidade de verificadores especializados, mas tem cobertura limitada quando usada para verificação funcional. A geração aleatória de testes é uma abordagem alternativa capaz de obter maior cobertura, mas requer um verificador independente para validar se os comportamentos de memória observados obedecem a um dado modelo de consistência de memória. Esta dissertação apresenta um framework de verificação de memória compartilhada e propõe uma nova abordagem como contribuição para um de seus módulos. O framework é resultado de um esforço de pesquisa coletivo, e utiliza geração aleatória de testes dirigida por cobertura. A abordagem proposta permite a personalização de verificadores eficientes de acordo com a arquitetura e microarquitetura alvos. Ela utiliza uma especificação abstrata do comportamento da memória compartilhada e um template de observabilidade para guiar a inserção de monitores em pontos apropriados da representação de projeto. Para garantir escalabilidade sem comprometer garantias de verificação, são definidos múltiplos monitores por domínio de núcleo. Ao contrário de verificadores convencionais, os quais são incapazes de lidar com o comportamento resultante da relaxação da atomicidade de escrita, a abordagem proposta permite a construção de verificadores compatíveis com ambos os tipos de atomicidade (relaxada ou estrita). Um verificador construído sob a nova abordagem foi comparado com um convencional, ambos dentro do mesmo framework de verificação. Eles foram avaliados através da execução dos mesmos conjuntos de testes, cada um composto por vários programas de tamanho fixo. Para programas de 4Ki instruções, o verificador convencional acusou falsos positivos para um terço dos conjuntos de testes, ao verificar projetos sem erros com 32 núcleos sob atomicidade relaxada de escrita, enquanto o novo verificador não acusou erro algum. Para projetos contendo erros, o novo verificador mostrou esforço adicional desprezível em alguns casos e frequentemente reduziu o esforço. Portanto, as evidências experimentais indicam que, sob a nova abordagem, o verificador é efetivo, frequentemente reduz o esforço para detectar erros e é adequado para verificar projetos com diferentes graus de relaxação da atomicidade de escrita.Abstract: Single-chip multiprocessors, known as multicore chips, usually provide a coherent shared memory abstraction, which can be achieved by implementing a cache coherence protocol on hardware. It has been shown that on-chip hardware coherence can scale gracefully as the number of cores grows. Since scaling estimates show that the number of active cores is limited by thermal power, cache coherence can be expected to keep playing a major role for multicore chips targeting general purpose applications. Besides, multicore architectures are likely to largely relax sequential consistency constraints on store atomicity and on the ordering between loads and stores. As a result, the validation of shared memory in multicore chips faces two main challenges: the higher number of valid execution witnesses resulting from consistency relaxation and the larger coherence protocol?s state space induced by growing core counts. At the microarchitectural level, the validation effort relies on simulation-based functional verification of the design representation. Litmus test generation is an effective approach to exposing consistency errors without the need for specialized checkers, but has limited coverage when used for functional verification. Constrained random test generation is an alternative approach that leads to higher coverage, but requires an independent checker to validate the observed memory behaviors against a given memory consistency model. This dissertation reports a shared memory verification framework and proposes a novel approach to contribute to one of its modules. The framework is the result of a collective research effort, and it relies on coverage-directed random test generation. The proposed approach allows the customization of efficient runtime checkers according to architecture and microarchitecture targets. It relies on an abstract specification for shared memory behavior and on an observability template for guiding the insertion of monitors in appropriate points of the design representation. To ensure scalability without compromising verification guarantees, multiple monitors per core domain are defined. As opposed to conventional checkers, which are unable to properly handle behavior arising from relaxed store atomicity, the proposed approach allows the building of checkers compliant with either relaxed or strict atomicity. We compared a checker built under the novel approach with a conventional one, both within the reported verification framework. They were evaluated when running the same test suites, each built with many programs of fixed size. For programs with 4Ki instructions, the conventional checker raised false positives for 1/3 of the test suites when targeting correct 32-core designs with relaxed atomic behavior, whereas the new checker raised none. For faulty designs with strict store atomicity, the new checker displayed negligible effort overhead when compared to the conventional one, and often led to effort reduction. Therefore, the experimental evidence indicates that a checker produced with the novel approach is effective, it often reduces the effort to detect an error, and it is suitable to checking designs with different degrees of store atomicity relaxation