An Assertional Characterization of Serializability and Locking.
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 09, 1988
- Accession Number
- ADA191215
Entities
People
- Ernest R. Mccurley
Organizations
- Cornell University