A Serialization Graph Construction for Nested Transactions

Abstract

This paper makes three contributions. First, we present a proof technique that offers system designers the same ease of reasoning about nested transaction systems as is given by the classical theory for systems without nesting, and yet can be used to verify that a system satisfies the robust user view definition of correctness of another work. Second, as applications of the technique, we verify the correctness of Moss' read/write locking algorithm for nested transactions, and of an undo logging algorithm that has not previously been presented or proved for nested transaction systems. Third, we make explicit the assumptions used for this proof technique, assumptions that are usually made implicitly in the classical theory, and therefore we clarify the type of system for which the classical theory itself can reliably be used. Keywords: Concurrency control; Recovery; Fault-tolerance; Nested transactions; Serializability; Verification.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 1990
Accession Number
ADA222697

Entities

People

  • Alan Fekete
  • Nancy Lynch
  • William E. Weihl

Organizations

  • Massachusetts Institute of Technology

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Automata
  • Buildings And Structures
  • Classification
  • Computer Science
  • Computers
  • Consistency
  • Construction
  • Contracts
  • Control Systems
  • Database Management Systems
  • Databases
  • Environment
  • Military Research
  • Security
  • Transitions

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Parallel and Distributed Computing.
  • Theoretical Analysis.