Dynamic Thermal Management (DTM) through task migrations across cores provides a very promising solution to cater for the heating issues in Many-Core architectures. These techniques can be classified as central (c-) or (d-) distributed on the basis of a central DTM controller for the whole system or individual DTM controllers for each core or set of cores in the system, respectively. However, the growing number of cores, the diverse nature of DTM schemes avialable, and the inherent sampling based nature of traditional analysis techniques, like simulation and emulation, make 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 DTM 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 model checking to formally verify task migration based DTM techniques. We identify a set of generic functional and performance properties to provide a generic methodology and common ground for cDTM and dDTM comparison. We demonstrate the usability and benefits of our methodology by comparing state-of-the-art cDTM and dDTM techniques, and illustrate which technique is good w.r.t. thermal stability and other DTM parameters like tasks migrations, stalls, completion, creation of hot spots and time to achieve stability.
- CAnDy-TM: Comparative Analysis of Central & Distributed DTM in Many-Cores using Model Checking
- FAMe-TM: Formal Analysis Methodology for Task Migration Algorithms in Many-Core Systems
- Formal Verification of DTM for Thermal Management in On-chip Multi-core Systems using nuXmv
- Probabilistic Formal Verification Methodology for Decentralized Thermal Management in SOCs
- Formal Analysis of TAPE: A Thermal Management Algorithm for ICs
S. A. A. Bukhari, F. K. Lodhi, O. Hasan, M. Shafique and J. Henkel, “CAnDy-TM: Comparative Analysis of Dynamic Thermal Management in Many-Cores using Model Checking”, Design, Automation and Test in Europe (DATE-2017), Swisstech, Laussane, Switzerland, To Appear.
S. A. A. Bukhari, F. K. Lodhi, O. Hasan, M. Shafique and J. Henkel, “FAMe-TM: Formal Analysis Methodology for Task Migration Algorithms in Many-Core Systems”, Science of Computer Programming, Elsevier, Vol. 133, Part 2, 2017, pp. 154-174.
S. Iqtedar, O. Hasan, M. Shafique, J. Henkel, “Probabilistic Formal Verification Methodology for Decentralized Thermal Management in On-Chip Systems”, IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises (WETICE-2015), IEEE Computer Society, Larnaca, Cyprus. pp. 210-215.
S. A. A. Bukhari, F. K. Lodhi, O. Hasan, M.Shafique and J.Henkel, “Formal Verification of Distributed Task Migration for Thermal Management in On-chip Multi-core Systems using nuXmv”, Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014), Luxembourg City, Luxembourg, 2014, To Appear.
S. Iqtedar, O. Hasan, M. Shafique, J. Henkel, “Formal Probabilistic Analysis of Distributed Dynamic Thermal Management”, Design, Automation and Test in Europe (DATE-2015), March 9-13, Grenoble, France. pp. 1221-1224.
M. Ismail, O. Hasan, T. Ebi, M. Shafique and J. Henkel, ” Formal Verification of Distributed Dynamic Thermal Management” International Conference on Computer-Aided Design (ICCAD-2013) ,IEEE/ACM, Austin, Texas.
M. Ismail, “Formal Analysis of TAPE: A Thermal Management Algorithm for ICs “, Masters Thesis, National University of Sciences and Technology (NUST), Islamabad, Pakistan. 2013.