Defesa de Exame de Qualificação – Gabriel Arthur Gerber Andrade – 25/2/2019

17/05/2019 14:54
Defesa de Exame de Qualificação
Aluno Gabriel Arthur Gerber Andrade
Orientador Prof. Luiz Cláudio Villar dos Santos, Dr. – INE/UFSC
Data

 

25/2/2019  14h00  (segunda-feira)

Sala PPGEAS I (piso superior)

Banca Prof. Rômulo Silva de Oliveira, Dr. – DAS/UFSC (presidente);

Prof. Rodolfo Jardim de Azevedo,  Dr. – IC/UNICAMP;

Prof. Márcio Bastos Castro, Dr. – INE/UFSC.

Título

 

Test Generation for Shared-Memory Verification of Multicore Chips
Abstract: Since non-deterministic behavior is key to exposing shared-memory errors, non-synchronized parallel programs are often used for verification and test of multicore chips. In the verification phase, the slow execution in a simulator requires non-conventional techniques for enabling error exposure with shorter programs. In this context, this work makes three contributions. First, the work proposes two novel techniques that build upon conventional random test generation for efficient shared-memory verification. One technique exploits canonical dependence chains for constraining the random generation of instruction sequences (to raise the coverage of state transitions due to memory events conflicting at a same shared location), another exploits address space constraints for biasing random address assignment (to raise the coverage of state transitions due to eviction events). As compared to a conventional generator, the combination of these techniques reduced the average verification effort by one order of magnitude in many cases. Second, the work proposes a new mechanism for directed generation that improves the quality of non-deterministic racy tests. The mechanism exploits general properties of coherence protocols and cache memories for better control on transition coverage (which serves as a proxy for increasing the actual coverage metric adopted in a given verification environment). Being independent of coverage metric, coherence protocol, and cache parameters, the mechanism is reusable across quite different designs and verification environments. With such mechanism, our test generation was faster to reach similar coverage as compared to the most recently reported generator of racy tests (based on Genetic Programming). For instance, when executing tests with 1K operations for verifying 32-core designs, our test generator reached 60% coverage ten times faster. Third, the work envisages a novel technique for directed test generation that relies on a feedback loop for further reducing the effort towards higher coverage. It exploits local-search heuristics for detecting coverage saturation and pruning heuristics for progressively reducing the exploration of the generation space without jeopardizing coverage. The first contribution was already reported in an submitted article and the second one in a published paper. The third contribution was conceptually designed, but its elaboration and implementation are part of the planned activities towards the future thesis.