TY - GEN
T1 - Formal Verification of Distributed Task Migration for Thermal Management in On-Chip Multi-Core Systems Using nuXmv
AU - Bukhari, Syed Ali Asadullah
AU - Lodhi, Faiq Khalid
AU - Hasan, Osman
AU - Shafique, Muhammad
AU - Henkel, Jörg
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
Copyright:
Copyright 2017 Elsevier B.V., All rights reserved.
PY - 2015
Y1 - 2015
N2 - 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.
AB - 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.
KW - Model checking
KW - Multi-core architectures
KW - Task migration
KW - Thermal management
UR - http://www.scopus.com/inward/record.url?scp=84929648631&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84929648631&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-17581-2_3
DO - 10.1007/978-3-319-17581-2_3
M3 - Conference contribution
AN - SCOPUS:84929648631
T3 - Communications in Computer and Information Science
SP - 32
EP - 46
BT - Formal Techniques for Safety-Critical Systems - 3rd International Workshop, FTSCS 2014, Revised Selected Papers
A2 - Artho, Cyrille
A2 - Ölveczky, Peter Csaba
PB - Springer Verlag
T2 - 3rd International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2014
Y2 - 6 November 2014 through 7 November 2014
ER -