查看文章

Distributed Dynamic Thermal Management (dDTM) through task migrations across cores provides a very promising solution to cater for the heating issues in Many-Core architectures. However, the growing number of cores, the distributed nature of dDTM and the inherent sampling-based nature of traditional analysis techniques, like simulation and emulation, makes a complete and rigorous analysis of these task migration algorithms almost impossible. These limitations compromise the analysis integrity and in worst cases may lead to the deployment of an inefficient and inaccurate dDTM scheme on chip, which in turn can cause permanent defects in the chip due to excessive heating. Leveraging upon the exhaustive nature of model checking based verification, we propose to use a model checker to formally verify task migration algorithms. This work proposes an analysis methodology, i.e., Formal Analysis …