多核系统动态温度管理TAPE策略的形式化验证

doi:10.11896/j.issn.1002-137X.2017.11A.115

摘要/Abstract

摘要： 多核系统中,分布式DTM策略因其良好的可扩展性得到了广泛应用。在部署分布式DTM策略前,必须验证其可靠性。为了克服传统分析方法的局限,模型检测技术被应用于分布式DTM策略的分析中。提出使用统计模型检测技术来验证多核系统中分布式DTM策略(以TAPE策略为例)的方案。使用UPPAAL SMC对TAPE策略的验证证明了TAPE策略的安全性、有效性、活性以及稳定性,从而验证DTM策略方案的可靠性。

关键词: 动态温度管理策略,统计模型检测,多核系统

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

屈媛媛,洪玫,孙琳. 多核系统动态温度管理TAPE策略的形式化验证[J]. 计算机科学, 2017, 44(Z11): 542-546. https://doi.org/10.11896/j.issn.1002-137X.2017.11A.115

QU Yuan-yuan, HONG Mei and SUN Ning. Formal Verification of TAPE Strategy for Dynamic Temperature Management in Multi-core System[J]. Computer Science, 2017, 44(Z11): 542-546. https://doi.org/10.11896/j.issn.1002-137X.2017.11A.115

参考文献

[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.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed