Multi-granularity locking for nested transactions: A proof using a possibilities mapping (Q1901697)

The choice of granularity for locking times in a database involves performance trade-offs. In order to provide a choice between different locking granularities within a single system, the two-phase locking algorithm needs to be modified to include intention locks. This paper extends the well-known multi-granularity locking algorithm of \textit{J. Gray} et al. to deal with nested transactions, and verifies the correctedness of the extended algorithm, using a possibility mapping to abstract commutativity-based locking.