Modeling and Analysis of the Thermal Properties Exhibited by Cyberphysical Data Centers

被引:32
作者
Malik, Saif U. R. [1 ]
Bilal, Kashif [1 ]
Khan, Samee U. [2 ]
Veeravalli, Bharadwaj [3 ]
Li, Keqin [4 ]
Zomaya, Albert Y. [5 ]
机构
[1] COMSATS Inst Informat Technol, Dept Comp Sci, Islamabad 44000, Pakistan
[2] North Dakota State Univ, Coll Engn, Dept Elect & Comp Engn, Fargo, ND 58105 USA
[3] Natl Univ Singapore, Fac Engn, Dept Elect & Comp Engn, Singapore 117576, Singapore
[4] SUNY Coll New Paltz, Sch Sci & Engn, Dept Comp Sci, New Paltz, NY 12561 USA
[5] Univ Sydney, Sch Informat Technol, Sydney, NSW 2006, Australia
来源
IEEE SYSTEMS JOURNAL | 2017年 / 11卷 / 01期
关键词
Cloud computing; cyberphysical systems (CPSs); data center (DC); formal methods; modeling; verification;
D O I
10.1109/JSYST.2015.2493565
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Data centers (DCs) contribute toward the prevalent application and adoption of the cloud by providing architectural and operational foundation. To perform sustainable computation and storage, a DC is equipped with tens of thousands of servers, if not more. It is worth noting that the operational cost of a DC is being dominated by the cost spent on energy consumption. In this paper, we model a DC as a cyberphysical system (CPS) to capture the thermal properties exhibited by the DC. All software aspects, such as scheduling, load balancing, and all the computations performed by the devices, are considered the "cyber" component. The supported infrastructure, such as servers and switches, are modeled as the "physical" component of the CPS. We perform detailed modeling of the thermal characteristics displayed by the major components of the CPS. Moreover, we propose a thermal-aware control strategy that uses a high-level centralized controller and a low-level centralized controller to manage and control the thermal status of the cyber components at different levels. Our proposed strategy is testified and demonstrated by executing on a real DC workload and comparing it with three existing strategies, i. e., one classical and two thermal-aware strategies. Furthermore, we also perform formal modeling, analysis, and verification of the strategies using high-level Petri nets, the Z language, the Satisfiability Modulo Theories Library (SMT-Lib), and the Z3 solver.
引用
收藏
页码:163 / 172
页数:10
相关论文
共 25 条
[1]  
[Anonymous], P 12 INT C SCALCOM C
[2]  
Bash CE, 2006, 2006 PROCEEDINGS 10TH INTERSOCIETY CONFERENCE ON THERMAL AND THERMOMECHANICAL PHENOMENA IN ELECTRONICS SYSTEMS, VOLS 1 AND 2, P445
[3]  
Biere A., 2003, ADV COMPUT, V58, P1
[4]   On the Characterization of the Structural Robustness of Data Center Networks [J].
Bilal, Kashif ;
Manzano, Marc ;
Khan, Samee U. ;
Calle, Eusebi ;
Li, Keqin ;
Zomaya, Albert Y. .
IEEE TRANSACTIONS ON CLOUD COMPUTING, 2013, 1 (01) :64-77
[5]   Market-Oriented Cloud Computing: Vision, Hype, and Reality for Delivering IT Services as Computing Utilities [J].
Buyya, Rajkumar ;
Yeo, Chee Shin ;
Venugopal, Srikumar .
HPCC 2008: 10TH IEEE INTERNATIONAL CONFERENCE ON HIGH PERFORMANCE COMPUTING AND COMMUNICATIONS, PROCEEDINGS, 2008, :5-13
[6]   SMT-Based Bounded Model Checking for Embedded ANSI-C Software [J].
Cordeiro, Lucas ;
Fischer, Bernd ;
Marques-Silva, Joao .
2009 IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2009, :137-148
[7]  
Ganai MalayK., 2006, P 2006 IEEEACM INT C, P794
[8]   Cyber-Physical Systems: A Perspective at the Centennial [J].
Kim, Kyoung-Dae ;
Kumar, P. R. .
PROCEEDINGS OF THE IEEE, 2012, 100 :1287-1308
[9]  
Koomey J., GROWTH DATA CTR ELEC
[10]  
Kumari N, 2012, INTSOC CONF THERMAL, P799, DOI 10.1109/ITHERM.2012.6231508