The choice of granularity for locking items in a database involves per
formance trade-offs. In order to provide a choice between different lo
cking granularities within a single system, the two-phase locking algo
rithm needs to be modified to include intention locks. This paper exte
nds the well-known multi-granularity locking algorithm of Gray et al.
to deal with nested transactions, and verifies the correctness of the
extended algorithm, using a possibilities mapping to abstract commutat
ivity-based locking.