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 many-core systems. The functional and timing verification is done on a larger grid size of \(9\times 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Brooks, D., Martonosi, M.: Dynamic thermal management for high-performance microprocessors. In: High-Performance Computer Architecture, pp. 171–182. IEEE (2001)
Bukhari, S.A.A., Lodhi, F.K.: Formal verification of distributed task migration for thermal management in on-chip multi-core systems using nuXmv, National University of Sciences and Technology (2014). http://save.seecs.nust.edu.pk/projects/fdDTM/fdDTM.html
Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv Symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Heidelberg (2014)
Chen, F., Cao, Y., Ren, W.: Distributed computation of the average of multiple time-varying reference signals. In: American Control Conference, pp. 1650–1655 (2011)
Chen, F., Cao, Y., Ren, W.: Distributed average tracking of multiple time-varying reference signals with bounded derivatives. IEEE Trans. Autom. Control 57(12), 3169–3174 (2012)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Donald, J., Martonosi, M.: Techniques for multicore thermal management: classification and new exploration. In: Computer Architecture, pp. 78–88 (2006)
Donald, J., Martonosi, M.: Techniques for multicore thermal management: Classification and new exploration. In: ACM SIGARCH Computer Architecture News. vol. 34, pp. 78–88. IEEE Computer Society (2006)
Drechsler, R.: Advanced Formal Verification. Falk Symposium Series. Springer, Boston (2004)
Dunn, D.: Intel delays Montecito in roadmap shakeup. EE Times, Manufacturing/Packaging, October 2005
Ebi, T., Faruque, M., Henkel, J.: Tape: thermal-aware agent-based power econom multi/many-core architectures. In: Computer-Aided Design. pp. 302–309 (2009)
Ebi, T., Kramer, D., Karl, W., Henkel, J.: Economic learning for thermal-aware power budgeting in many-core architectures. In: Hardware/Software Codesign and System Synthesis.pp. 189–196, ACM (2011)
Ge, Y., Malani, P., Qiu, Q.: Distributed task migration for thermal management in many-core systems. In: Design Automation Conference, pp. 579–584. ACM (2010)
Glocker, E., Schmitt-Landsiedel, D.: Modeling of temperature scenarios in a multicore processor system. Adv. Radio Sci. 11, 219–225 (2013)
Henkel, J., Ebi, T., Amrouch, H., Khdr, H.: Thermal management for dependable on-chip systems. In: Asia and South Pacific Design Automation Conference, pp. 113–118 (2013)
Holzmann, G.J.: The model checker SPIN. IEEE Trans. softw. eng. 23(5), 279–295 (1997)
Ismail, M., Hasan, O., Ebi, T., Shafique, M., Henkel, J.: Formal verification of distributed dynamic thermal management. In: Computer-Aided Design, pp. 248–255. IEEE (2013)
ITRS: (2014). http://www.itrs.net/Links/2013ITRS/2013Chapters/2013Overview.pdf
Kadin, M., Reda, S., Uht, A.: Central vs. distributed dynamic thermal management for multi-core processors: which one is better? In: Great Lakes Symposium on VLSI, pp. 137–140. ACM (2009)
Khdr, H., Ebi, T., Shafique, M., Amrouch, H., Henkel, J.: mDTM: multi-objective dynamic thermal management for on-chip systems. In: Design, Automation Test in Europe, p. 330 (2014)
Kong, J., Chung, S.W., Skadron, K.: Recent thermal management techniques for microprocessors. ACM Comput. Surv. 44(3), 13:1–13:42 (2012)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)
Liu, Z., Huang, X., Tan, S.D., Wang, H., Tang, H.: Distributed task migration for thermal hot spot reduction in many-core microprocessors. In: ASIC, pp. 1–4 (2013)
Liu, Z., Xu, T., Tan, S.D., Wang, H.: Dynamic thermal management for multi-core microprocessors considering transient thermal effects. In: Design Automation Conference, pp. 473–478 (2013)
Lungu, A., Bose, P., Sorin, D.J., German, S., Janssen, G.: Multicore power management: Ensuring robustness via early-stage formal verification. In: Formal Methods and Models for Codesign, pp. 78–87. IEEE (2009)
MathSAT 5: (2014). http://mathsat.fbk.eu/
Mukherjee, R., Memik, S.O.: Physical aware frequency selection for dynamic thermal management in multi-core systems. In: Computer-aided Design, pp. 547–552. ACM (2006)
Nath, R., Carmean, D., Rosing, T.S.: Power modeling and thermal management techniques for manycores. In: Computers and Communications. pp. 740–746. IEEE (2013)
Norman, G., Parker, D., Kwiatkowska, M., Shukla, E., Gupta, R.: Using probabilistic model checking for dynamic power management. Formal Aspects Comput. 17, 202–215 (2003)
nuSMV: (2014). http://nusmv.fbk.eu/
nuXmv: (2014). https://nuxmv.fbk.eu/
Salami, B., Baharani, M., Noori, H.: An adaptive temperature threshold schema for dynamic thermal management of multi-core processors. In: Computer Architecture and Digital Systems, pp. 119–120 (2013)
Schauer, B.: Multicore processors-a necessity. In: ProQuest discovery guides, pp. 1–14 (2008)
Shafique, M., Henkel, J.: Agent-based distributed power management for kilo-core processors. In: Computer-Aided Design, pp. 153–160. IEEE (2013)
Shukla, S., Gupta, R.: A model checking approach to evaluating system level dynamic power management policies for embedded systems. In: High-Level Design Validation and Test Workshop, pp. 53–57. IEEE (2001)
Singh, A., Shafique, M., Kumar, A., Henkel, J.: Mapping on multi/many-core systems: Survey of current and emerging trends. In: Design Automation Conference (DAC), ACM/EDAC/IEEE.pp. 1–10 (2013)
Weiss, G.: Multiagent Systems: A Modern Approach to Distributed Artificial Intelligence. MIT Press, Cambridge (1999)
Wolfram: (2014). http://functions.wolfram.com/ComplexComponents/Sign/21/01/01/
Wyngaard, J., Inggs, M., Collins, J., Farrimond, B.: Towards a many-core architecture for HPC. In: Field Programmable Logic and Applications, pp. 1–4 (2013)
Yang, J., Zhou, X., Chrobak, M., Zhang, Y., Jin, L.: Dynamic thermal management through task scheduling. In: Performance Analysis of Systems and software, pp. 191–201 (2008)
Yun, B., Shin, K.G., Wang, S.: Predicting thermal behavior for temperature management in time-critical multicore systems. In: IEEE Real-Time and Embedded Technology and Applications Symposium, pp. 185–194 (2013)
Acknowledgement
This work is supported in parts by the DAAD “Deutsch-Pakistanische Forschungskooperationen” project.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Bukhari, S.A.A., Lodhi, F.K., Hasan, O., Shafique, M., Henkel, J. (2015). Formal Verification of Distributed Task Migration for Thermal Management in On-Chip Multi-core Systems Using nuXmv. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2014. Communications in Computer and Information Science, vol 476. Springer, Cham. https://doi.org/10.1007/978-3-319-17581-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-17581-2_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-17580-5
Online ISBN: 978-3-319-17581-2
eBook Packages: Computer ScienceComputer Science (R0)