Abstract
Concurrency control is an essential component of any transactional database management system, which is responsible for providing isolation (the "I" in ACID) to
transactions. Formally, concurrency control aims to achieve serializability: a way to rearrange the actions of concurrently executing transactions that eliminates concurrency while leaves the
database modifications unchanged. In this small entry, we define serializability, a syntactic over-approximation called conflict-serializability, and characterize schedules generated by the
frequently used concurrency control mechanism of strict two-phase locking (S2PL). We also prove two inclusions: S2PL implies conflict-serializability, which in turn implies serializability.
The formalization is based on standard material from an advanced database systems course.