FAMe-TM: Formal Analysis Methodology for Task Migration Algorithms in Many-Core Systems

Syed Ali Asadullah Bukhari and Faiq Khalid Lodhi,

ali.asadullah@seecs.edu.pkfaiq.khalid@seecs.edu.pk 

Abstract

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 and identifies a generic set of properties for the formal verification of task migration based dDTM schemes. In particular, we propose an analysis flow using the scalable bounded model checker, nuXmv, to formally verify the suggested task migration properties, like tasks migrations, stalls, completion, creation of hot spots and time to achieve stability. For illustration purposes, we apply our proposed analysis methodology to a recently proposed task migration based dDTM scheme.

Proposed Analysis Methodology for dDTM Schemes using nuXmv

Modeling of a Core Module

Syed Ali Asadullah Bukhari and Faiq Khalid are Post Graduate students of Electrical Engineering at NUST School of Electrical Engineering & Computer Science. They are working on this project in the System Analysis & Verification (SAVE) Lab of NUST-SEECS, under the supervision of Dr. Osman Hasan.