Issue No.05 - October (1995 vol.7)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/69.469819
<p><it>Abstract</it>—The partitioned synchronization rule is a technique for proving the correctness of concurrency control algorithms. Prior work has shown the applicability of the partitioned synchronization rule to hierarchically decomposed databases whose structure is restricted to semitrees. The principal contribution of this paper is a demonstration that the partitioned synchronization rule also applies to more general structures than semitrees, specifically, to any planar extendible partial order, a partial order which when extended with a least and a greatest element still remains planar. To demonstrate utility, the paper presents two applications of the partitioned synchronization rule. The first application shows correctness of a component-based timestamp generation algorithm suitable for implementing a timestamp ordering concurrency control algorithm. The second application shows correctness of a snapshot algorithm for concurrency control in a replicated multilevel secure database; we choose this application to highlight that hierarchically decomposed databases and multilevel secure databases are structurally similar. In both cases, the correctness proofs via the partitioned synchronization rule are substantially simpler than corresponding direct proofs.</p>
Concurrency control, database management, hierarchically decomposed databases, multilevel secure databases, transaction processing.
Paul Ammann, Vijayalakshmi Atluri, Sushil Jajodia, "The Partitioned Synchronization Rule for Planar Extendible Partial Orders", IEEE Transactions on Knowledge & Data Engineering, vol.7, no. 5, pp. 797-808, October 1995, doi:10.1109/69.469819