FAMe-TM: Formal analysis methodology for task migration algorithms in Many-Core systems

Syed Ali Asadullah Bukhari, Faiq Khalid Lodhi, Osman Hasan, Muhammad Shafique, Jörg Henkel

Research output: Contribution to journalArticlepeer-review

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, i.e., Formal Analysis Methodology for Task Migrations (FAMe-TM), 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, time spent in migration and time to achieve stability. For illustration purposes, we apply FAMe-TM to two recently proposed task-migration-based dDTM schemes, i.e., Thermal Coupling Aware (TCA-TM) dDTM and Hot Spot Reduction (HR-TM) dDTM.

Original languageEnglish (US)
Pages (from-to)154-174
Number of pages21
JournalScience of Computer Programming
Volume133
DOIs
StatePublished - Jan 1 2017

Keywords

  • Dynamic Thermal Management
  • Formal verification
  • Many-Core systems
  • Model checking
  • nuXmv

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'FAMe-TM: Formal analysis methodology for task migration algorithms in Many-Core systems'. Together they form a unique fingerprint.

Cite this