The partitioned synchronization rule for planar extendible partial orders

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 the 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