Computer Science ›› 2017, Vol. 44 ›› Issue (Z11): 542-546, 551.doi: 10.11896/j.issn.1002-137X.2017.11A.115

Previous Articles     Next Articles

Formal Verification of TAPE Strategy for Dynamic Temperature Management in Multi-core System

QU Yuan-yuan, HONG Mei and SUN Ning   

  • Online:2018-12-01 Published:2018-12-01

Abstract: Distributed DTM strategy in multi-core system is widely used because of its scalability.Before a distributed DTM policy is deployed,its reliability must be verified.In order to overcome the limitations of the traditional analytical methods,the model checking technique is applied to the analysis of distributed DTM strategies.This paper analyzed a TAPE policy which is a distributed DTM policy instance in a multicore system using statistical model checking techniques.The verification of TAPE strategy by UPPAAL SMC proves the security,validity,activity and stability of TAPE strategy,and proves the reliability of DTM scheme.

Key words: Dynamic temperature management strategy,Statistical model checking,Multi-core system

[1] EBI T,FARUQUE M,HENKEL J.Tape:Thermal-awareagent-based power econom multi/many-core architectures[C]∥IEEE/ACM International Conference on Computer-Aided Design-Digest of Technical Papers(ICCAD 2009).IEEE,2009:302-309.
[2] ISMAIL M,HASAN O,EBI T,et al.Formal verification of distributed dynamic thermal management[C]∥Proceedings of the International Conference on Computer-Aided Design.IEEE Press,2013:248-255.
[3] DAVID A,LARSEN K G,LEGAY A,et al.Time for statistical model checking of real-time systems[C]∥Computer Aided Verification.Springer Berlin Heidelberg,2011:349-355.
[4] RAO R,VRUDHULA S.Fast and accurate prediction of thesteady-state throughput of multicore processors under thermal constraints[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2009,28(10):1559-1572.
[5] UKHOV I,BAO M,ELES P,et al.Steady-state dynamic temperature analysis and reliability optimization for embedded multiprocessor systems[C]∥Proceedings of the 49th Annual Design Automation Conference.ACM,2012:197-204.
[6] MOHAQEQI M,KARGAHI M,MOVAGHAR A.Analyticalleakage-aware thermal modeling of a real-time system[J].IEEE Transactions on Computers,2014,63(6):1378-1392.
[7] SHUKLA S K,GUPTA R K.A model checking approach to evaluating system level dynamic power management policies for embedded systems[C]∥Sixth IEEE International High-Level Design Validation and Test Workshop .IEEE,2001:53-57.
[8] NORMAN G,PARKER D,KWIATKOWSKA M,et al.Using probabilistic model checking for dynamic power management[J].Formal Aspects of Computing,2005,17(2):160-176.
[9] LUNGU A,BOSE P,SORIN D J,et al.Multicore power mana-gement:Ensuring robustness via early-stage formal verification[C]∥Proceedings of the 7th IEEE/ACM International Confe-rence on Formal Methods and Models for Codesign.IEEE Press,2009:78-87.
[10] BUKHARI S A A,LODHI F K,HASAN O,et al.Formal Verification of Distributed Task Migration for Thermal Management in On-Chip Multi-core Systems Using nuXmv[M].Formal Techniques for Safety-Critical Systems.Springer International Publishing,2014:32-46.(下转第551页)(上接第546页)
[11] IQTEDAR S,HASAN O,SHAFIQUE M,et al.Formal probabilistic analysis of distributed dynamic thermal management[C]∥Design,Automation & Test in Europe Conference & Exhibition (DATE),2015.IEEE,2015:1221-1224.
[12] DAVIS R I,BURNS A.Priority assignment for global fixed priority pre-emptive scheduling in multiprocessor real-time systems[C]∥Real-Time Systems Symposium(RTSS 2009).IEEE,2009:398-409.
[13] LIAO W,HE L,LEPAK K M.Temperature and supply voltage aware performance and power modeling at microarchitecture level[J].IEEE Transactions on Computer-Aided Design of Integra-ted Circuits and Systems,2005,24(7):1042-1053.
[14] ZHURAVLEV S,SAEZ J C,BLAGODUROV S,et al.Survey of energy-cognizant scheduling techniques[J].IEEE Transactions on Parallel and Distributed Systems,2013,24(7):1447-1464.
[15] MOHAQEQI M,KARGAHI M,MOVAGHAR A.Analyticalleakage-aware thermal modeling of a real-time system[J].IEEE Transactions on Computers,2014,63(6):1378-1392.
[16] ISMAIL M,HASAN O,EBI T,et al.Formal verification of distributed dynamic thermal management[C]∥Proceedings of the International Conference on Computer-Aided Design.IEEE Press,2013:248-255.
[17] IQTEDAR S,HASAN O,SHAFIQUE M,et al.Formal probabilistic analysis of distributed dynamic thermal management[C]∥Design,Automation & Test in Europe Conference & Exhibition (DATE).IEEE,2015:1221-1224.

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75, 88 .
[2] XIA Qing-xun and ZHUANG Yi. Remote Attestation Mechanism Based on Locality Principle[J]. Computer Science, 2018, 45(4): 148 -151, 162 .
[3] LI Bai-shen, LI Ling-zhi, SUN Yong and ZHU Yan-qin. Intranet Defense Algorithm Based on Pseudo Boosting Decision Tree[J]. Computer Science, 2018, 45(4): 157 -162 .
[4] WANG Huan, ZHANG Yun-feng and ZHANG Yan. Rapid Decision Method for Repairing Sequence Based on CFDs[J]. Computer Science, 2018, 45(3): 311 -316 .
[5] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[6] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[7] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[8] LIU Qin. Study on Data Quality Based on Constraint in Computer Forensics[J]. Computer Science, 2018, 45(4): 169 -172 .
[9] ZHONG Fei and YANG Bin. License Plate Detection Based on Principal Component Analysis Network[J]. Computer Science, 2018, 45(3): 268 -273 .
[10] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99, 116 .