McCurley, E. Robert2007-04-232007-04-231988-01http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR88-894https://hdl.handle.net/1813/6734The problem of synchronizing transactions in a database system so that concurrent execution transforms the system from one consistent state to another is called the Concurrency Control Problem. Over the past 20 years, a property of concurrent execution called serializability has evolved as a universal paradign for colving the Concurrency Control Problem. Up until now, most work on serializability has been characterized by an emphasis on sequences of operations. Researchers studying programming logics and methodologies have developed a different approach to characterizing the semantics of concurrent programs. This approach is called assertional reasoning, and emphasizes the system state instead of sequences of operations. This dissertation describes the extension of the formalisms and tools of assertional reasoning to the Concurrency Control Problem. Proposed is a definition of serializability that generalizes previous definitions in many respects. Two methods are described by which this definition of serializability can be specified in an assertional programming logic using formulas called proof outlines. As a consequence of specifying serializability with proof outlines, it becomes possible to formally verify serializability. The use of an assertional programming logic eliminates the need to explicitly consider transaction interleavings, simplifying verfication. Another consequence of specifying serializability with proof outlines is the ability to derive synchronization protocols for serializability. This possibility is realized in the form of a method for deriving locking protocols from assertional specifications. The method is based on a novel view of locking, in which locks held by transactions reflect properties of the system state. Using this method, semantic information available during the derivation process can be used to obtain locking protocols permiting greater concurrency among transactions than locking protocols obtained by more traditional methods. Examples are given throughout the dissertation to illustrate the methods described.6355967 bytes1308884 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report