Modeling and Verifying the Ballooning in Xen with CSP

As a dynamic memory virtualization technique, ballooning is widely applied in many virtualization platforms, i.e. Xen and VMware ESX Server. Since ballooning technology enables the guest OS to surrender unused memory back to the host during runtime, and it can increase utilization and flexibility of memory. Despite the rapid development and extensive use of memory virtualization technologies, it is still a challenge to analyze and verify its validity and some major properties through formal methods. In this paper, we model the ballooning under Xen architecture including Xen hyper visor, a set of virtual machines and balloon drivers using the process algebra Communication Sequential Process (CSP) in order to verify some resource control properties of ballooning. The model is implemented with Process Analysis Toolkit (PAT). As a result, the ballooning used in Xen architecture satisfies these major resource control properties in VM requirement document.