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

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

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

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 tech-niques. 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.