DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
Accession Number:
ADA191215
Title:
An Assertional Characterization of Serializability and Locking.
Corporate Author:
CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE
Report Date:
1988-02-09
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.
Descriptive Note:
Doctoral thesis,
Pages:
0134
Contract Number:
N00014-86-K-0092
File Size:
4.66MB
