We demonstrate in this paper that mixing functional data-structures together with reference cell comparison, which is a limited form of pointer comparison, is: (i) safe; and (ii) efficient. This demonstration is based, first, on an axiomatization of operations on the tree-like structure we used to represent the Xenstored database. From this axiomatization, we then derive an efficient algorithm for coalescing transactions which try to concurrently modify that structure. Finally, we experimentally compare the performance of our implementation, that we called OXenstored, and the C implementation of the Xenstored service distributed with the Xen hypervisor sources.
As a direct result of this work, OXenstored will be included in the future releases of Xenserver, the virtualization product distributed by Citrix Systems, where it will replace the current implementation of the Xenstored service.
START Conference Manager (V2.56.8 - Rev. 748M)