Defesa de Tese de Doutorado – Gabriel Arthur Gerber Andrade – 24/5/2021

11/05/2021 16:12
Defesa de Tese de Doutorado
Aluno Gabriel Arthur Gerber Andrade
Orientador Prof. Luiz Cláudio Villar dos Santos, Dr. – PPGEAS/UFSC
Data

 

24/5/2021  9h  (segunda-feira)

Videoconferência (https://meet.google.com/vbe-nqgq-chn)

 

 

Banca

Prof. Luiz Cláudio Villar dos Santos, Dr. – PPGEAS/UFSC (presidente);

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

Prof. Rômulo Silva de Oliveira, Dr. – DAS/UFSC;

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

Título Test Generation for Shared-Memory Verification of Multicore Chips
Abstract: This thesis contributes to the functional verification of shared-memory behavior during the design of multicore chips. Since non-deterministic behavior is key to exposing shared-memory errors, non-synchronized parallel programs are often used for design verification and prototype test. However, in the verification phase, the slow execution in a simulator requires non-conventional techniques for enabling error exposure and high coverage with shorter programs. In this context, this thesis makes three contributions. The first contribution consists of two 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, their combination reduced the average verification effort by one order of magnitude in many cases. The second contribution is 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. Such a model-based generator was faster to reach similar coverage as obtained by a data-driven generator (based on Genetic Programming), reported in a related work. For instance, when executing tests with 1K operations for verifying 32-core designs, our test generator reached 60% coverage ten times faster. The third contribution consists of an hybrid approach that is not a simple combination of data-driven and model-based techniques. It reformulates directed test generation as a double-objective optimization problem, and it explores neighborhoods to avoid explicit enumeration of the coherence state space without excluding optimal solutions from the search space. As compared to purely data-driven and model-based generators, the hybrid approach led to superior coverage evolution with time, when targeting 32-core designs relying on different protocols. For instance, for a MOESI 2-level protocol, the approach was up to 2.7 faster than the model-based generator and around 5 to 19 times faster than the data-driven generator. Finally, the hybrid approach was also compared to a data-driven generator based on Reinforcement Learning. The experimental results showed that the proposed hybrid approach was 2 to 3 times faster to obtain the maximal coverage reached by that generator. The contributions of this thesis were reported in two journal articles (ANDRADE; GRAF; SANTOS, 2020; ANDRADE et al., 2020) and two conference papers (ANDRADE et al., 2018; PFEIFER et al., 2020).