Performance Modeling of Concurrent Live Migration Operations in Cloud Computing Systems Using PRISM Probabilistic Model Checker

Server virtualization technologies and their live migration function contribute to the utilization of the computing resources in cloud datacenters. However, many management operations for virtual machines (VMs) including live migrations can be evoked by many cloud users at anytime. The outburst of executions of live migration operations can deteriorate migration performance and make it difficult to provide required resources to users in a timely manner. Therefore, understanding the behaviors and the performance of simultaneous live migrations is very important to provide efficient and reliable cloud computing services. In this paper, we construct a performance model of concurrent live migrations in virtualized datacenters. We first collect performance data from an experimental virtualized system in which we execute simultaneous live migrations. Based on the data, we next construct a performance model representing the performance characteristics of live migration using PRISM, a probabilistic model checker. We then demonstrate that we can easily verify the properties described in PRISM language regarding live migration performance using this model.