Accession Number : ADA191215
Title : An Assertional Characterization of Serializability and Locking.
Descriptive Note : Doctoral thesis,
Corporate Author : CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE
Personal Author(s) : McCurley, Ernest R
PDF Url : ADA191215
Report Date : 09 Feb 1988
Pagination or Media Count : 134
Abstract : Proposed is a definition of serializability that generalizes previous definition 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 verification. 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 permitting greater concurrency among transactions than locking protocols obtained by more traditional methods. Examples are given throughout the dissertation to illustrate the methods described.
Descriptors : *SYNCHRONIZATION(ELECTRONICS), *MATHEMATICAL PROGRAMMING, COMPUTER PROGRAMMING, SEMANTICS, REASONING, DATA BASES, COMPUTER LOGIC, NAVAL RESEARCH, THESES
Subject Categories : Operations Research
Distribution Statement : APPROVED FOR PUBLIC RELEASE