THE PARTITIONED SYNCHRONIZATION RULE FOR PLANAR EXTENDIBLE PARTIAL ORDERS

The partitioned synchronization rule is a technique for proving the co rrectness of concurrency control algorithms. Prior work has shown the applicability of the partitioned synchronization rule to hierarchicall y decomposed databases whose structure is restricted to semitrees. The principal contribution of this paper is a demonstration that the part itioned synchronization rule also applies to more general structures t han 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 applic ation shows correctness of a component-based timestamp generation algo rithm suitable for implementing a timestamp ordering concurrency contr ol algorithm. The second application shows correctness of a snapshot a lgorithm for concurrency control in a replicated multilevel secure dat abase; we choose this application to highlight that hierarchically dec omposed databases and multilevel secure databases are structurally Sim ilar. In both cases, the correctness proofs via the partitioned synchr onization rule are substantially simpler than corresponding direct pro ofs.