Email Gateway (Feb 11 2025 at 12:22): Email Gateway (Feb 11 2025 at 12:22):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I’m happy to announce a new AFP entry.
Formalization of (Conflict-)Serializability and Strict Two-Phase Locking
by Dmitriy Traytel
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.
https://www.isa-afp.org/entries/Serializable.html
Enjoy,
René
Last updated: Mar 09 2025 at 12:28 UTC