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
      Computer Systems

Distribution Statement : APPROVED FOR PUBLIC RELEASE