Formal Verification of Distributed Task Migration for Thermal Management in On-Chip Multi-Core Systems Using nuXmv

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

With the growing interest in using distributed task migration algorithms for dynamic thermal management (DTM) in multi-core chips comes the challenge of their rigorous verification. Traditional analysis techniques, like simulation and emulation, cannot cope with the design complexity and distributed nature of such algorithms and thus compromise on the rigor and accuracy of the analysis results. Formal methods, especially model checking, can play a vital role in alleviating these issues. Due to the presence of continuous elements, such as temperatures, and the large number of cores running the distributed algorithms in this analysis, we propose to use the nuXmv model checker to analyze distributed task migration algorithms for DTM. The main motivations behind this choice include the ability to handle the real numbers and the scalable SMT-based bounded model checking capabilities in nuXmv that perfectly fit the stability and deadlock analysis requirements of the distributed DTM algorithms. The paper presents the detailed analysis of a state-of-the-art task migration algorithm of distributed DTM for manycore systems. The functional and timing verification is done on a larger grid size of 9×9 cores, which is thermally managed by the selected DTM approach. The results indicate the usefulness of the proposed approach, as we have been able to catch a couple of discrepancies in the original model and gain many new insights about the behavior of the algorithm.

Original languageEnglish (US)
Title of host publicationFormal Techniques for Safety-Critical Systems - 3rd International Workshop, FTSCS 2014, Revised Selected Papers
EditorsCyrille Artho, Peter Csaba Ölveczky
PublisherSpringer Verlag
Pages32-46
Number of pages15
ISBN (Electronic)9783319175805
DOIs
StatePublished - 2015
Event3rd International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2014 - Luxembourg, Luxembourg
Duration: Nov 6 2014Nov 7 2014

Publication series

NameCommunications in Computer and Information Science
Volume476
ISSN (Print)1865-0929

Conference

Conference3rd International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2014
Country/TerritoryLuxembourg
CityLuxembourg
Period11/6/1411/7/14

Keywords

  • Model checking
  • Multi-core architectures
  • Task migration
  • Thermal management

ASJC Scopus subject areas

  • Computer Science(all)
  • Mathematics(all)

Fingerprint

Dive into the research topics of 'Formal Verification of Distributed Task Migration for Thermal Management in On-Chip Multi-Core Systems Using nuXmv'. Together they form a unique fingerprint.

Cite this