Atomic Transactions - 1st Edition - ISBN: 9781558601048, 9780080499543

Atomic Transactions

1st Edition

In Concurrent and Distributed Systems

Authors: Nancy Lynch Michael Merritt William Weihl Alan Fekete
Hardcover ISBN: 9781558601048
eBook ISBN: 9780080499543
Imprint: Morgan Kaufmann
Published Date: 1st August 1993
Page Count: 476
Tax/VAT will be calculated at check-out

Institutional Access


Table of Contents

Atomic Transactions: In Concurrent and Distributed Systems
by Nancy Lynch, Michael Merritt, William Weihl and Alan Fekete

  • Foreward
  • Preface
  • 1. Introduction
    • 1.1 Distributed Systems
    • 1.2 Atomic Transactions for Distributed Systems
      • 1.2.1 Atomic Databases
      • 1.2.2 Transactions
      • 1.2.3 Nested Transactions
    • 1.3 Transaction-Processing Algorithms
      • 1.3.1 Locking
      • 1.3.2 Timestamps
      • 1.3.3 Optimistic Algorithms
      • 1.3.4 Replication
      • 1.3.5 Recovery
    • 1.4 Formal Models
      • 1.4.1 Why a Formal Model?
      • 1.4.2 An Operational Automation Model
      • 1.4.3 Correct Systems Simulate Serial System
    • 1.5 Comparisons with the Classical Theory
      • 1.5.1 Serializability
      • 1.5.2 Classical Treatment of Recovery
      • 1.5.3 Data Types and Nesting
      • 1.5.4 Operational versus Axiomatic Model
      • 1.5.5 A Finer Granularity of Analysis
    • 1.6 Contents of This Book
      • 1.6.1 The Basic Theory
      • 1.6.2 Fundamental Transaction-Processing Algorithms
      • 1.6.3 More Advanced Transaction-Processing Algorithms
    • 1.7 Bibliographic Notes
      • 1.7.1 Transactions
      • 1.7.2 Correctness Conditions
      • 1.7.3 Algorithms for Concurrency Control and Recovery
  • 2 An Automation Model
    • 2.1 Introduction
    • 2.2 Action Signatures
    • 2.3 Automata
      • 2.3.1 Conventions: Transition Relations
      • 2.3.2 More Examples of Automata
    • 2.4 Executions and Behaviors
    • 2.5 Composition
      • 2.5.1 Compositiona of Action Signatures
      • 2.5.2 Composition of Automata
      • 2.5.3 Properties of Systems of Automata
    • 2.6 Proofs about Automata
    • 2.7 Relationships between Automata
      • 2.7.1 Implementation
      • 2.7.2 Possibilities Mappings
    • 2.8 Preserving Properties
    • 2.9 Discussion
      • 2.9.1 Process Algebras
      • 2.9.2 State-based Models
      • 2.9.3 Uses of Models
    • 2.10 Bibliographic Notes
    • 2.11 Exercises
  • 3 Serial Systems and Correctness
    • 3.1 Introduction
    • 3.2 System Types
    • 3.3 General Structure of Serial Systems
    • 3.4 Serial Actions and Well-Formedness
      • 3.4.1 Basic Definitions
      • 3.4.2 Well-Formedness
    • 3.5 Serial Systems
      • 3.5.1 Transaction Automata
      • 3.5.2 Serial Object Automata
      • 3.5.3 The Serial Scheduler
      • 3.5.4 Serial Systems, Executions, Schedules and Behaviors
      • 3.5.5 Convention: Fixing the System Type and Serial System
    • 3.6 Atomicity
      • 3.6.1 Atomicity of Action Sequences
      • 3.6.2 Atomicity of Systems
      • 3.6.3 Stronger Correctness Conditions
      • 3.6.4 Atomicity and Intuition
      • 3.6.5 Implications for Schedules and Executions
      • 3.6.6 Correctness of Infinite Behaviors
    • 3.7 An Additional Example
    • 3.8 Bibliographic Notes
    • 3.9 Exercises
  • 4 Special Classes of Serial Systems
    • 4.1 Introduction
    • 4.2 Equieffectiveness
    • 4.3 Commutativity
      • 4.3.1 Forward Commutativity
      • 4.3.2 Backward Commutativity
    • 4.4 Special Classes of Operations
      • 4.4.1 Transparent Operations
      • 4.4.2 Obliterating Operations
    • 4.5 Serial Dependency Relations
    • 4.6 Bibliographic Notes
    • 4.7 Exercises
  • 5 The Atomicity Theorem
    • 5.1 Introduction
    • 5.2 Visibility
    • 5.3 Simle Systems
      • 5.3.1 Simple Database
      • 5.3.2 Simple Systems, Executions, Schedules, and Behaviors
    • 5.4 Event and Transaction Orders
      • 5.4.1 SD-Affects Order
      • 5.4.2 Affects Order
      • 5.4.3 Sibling Orders
    • 5.5 Atomicity Theorem and Proof Sketch
    • 5.6 Proof of the Atomicity
      • 5.6.1 Pictures
      • 5.6.2 Behavior of Transactons
      • 5.6.3 Behavior of Serial Objects
      • 5.6.4 Behavior of the Serial Scheduler
      • 5.6.5 Proof of the Main Result
    • 5.7 Discussion
    • 5.8 Bibliographic Notes
    • 5.9 Exercises
  • 6 Locking Algorithms
    • 6.1 Introduction
    • 6.2 Dyamic Atomicity
      • 6.2.1 Completion Order
      • 6.2.2. Generic Systems
      • 6.2.3 Dyamic Atomicity
      • 6.2.4 Local Dyamic Atomicity
    • 6.3 General Commutativity-based Locking
      • 6.3.1 Locking Objects
      • 6.3.2 Correctness Proof
    • 6.4 Moss's Algorithm
      • 6.4.1 Moss Objects
      • 6.4.2 Correctness Proof
      • 6.4.3 Read/Write Locking Algorithm
    • 6.5 General Undo Logging Algorithm
      • 6.5.1 General Undo Logging Objects
      • 6.5.2 Correctness Proof
    • 6.6 Discussion
    • 6.7 Bibliographic Notes
    • 6.8 Exercises
  • 7 Timestamp Algorithms
    • 7.1 Introduction
    • 7.2 Simple-Pseudotime Systems
      • 7.2.1 Simple-Pseudotime Database
      • 7.2.2 Simple-Pseudotime Systems, Executions, Schedules, and Behaviors
    • 7.3 Static Atomicity
      • 7.3.1 Pseudotime Order
      • 7.3.2 Pseudotime Systems
      • 7.3.3 Static Atomicity
      • 7.3.4 Local Static Atomicity
    • 7.4 Reed's Algorithm
      • 7.4.1 Reed Objects
      • 7.4.2 Correctness Proof
      • 7.4.3 A Concrete Implementation
      • 7.4.4 Correctness Proof
    • 7.5 Type-specific Concurrency Control
      • 7.5.1 Herlihy Objects
      • 7.5.2 Correctness Proof
    • 7.6 Discussion
    • 7.7 Bibliographic Notes
    • 7.8 Exercises
  • 8 Hybrid Algorithms
    • 8.1 Introduction
    • 8.2 Hybrid Atomicity
      • 8.2.1 Hybrid Systems
      • 8.2.2 Hybrid Atomicity
      • 8.2.3 Local Hybrid Atomicity
    • 8.3 Dependecy-Based Hybrid Locking
      • 8.3.1 Dependency Objects
      • 8.3.2 Correctness Proof
    • 8.4 Discussion
    • 8.5 Bibliographic Notes
    • 8.6 Exercises
  • 9 Relationship to the Classical Theory
    • 9.1 Introduction
    • 9.2 Assumptions
      • 9.2.1 Read/Write Serial Objects
      • 9.2.2 Appropriate Return Values
      • 9.2.3 A Sufficient Condition for Appropriate Return Values
    • 9.3 The Serialization Graph Construction
    • 9.4 Moss's Algorithm
    • 9.5 Extension to General Data Types
      • 9.5.1 Serialization Graphs
      • 9.5.2 An Undo Logging Algorithm
    • 9.6 Discussion
    • 9.7 Bibliographic Notes
    • 9.8 Exercises
  • 10 Optimistic Algorithms
    • 10.1 Introduction
    • 10.2 Optimistic Hybrid Systems
      • 10.2.1 Simple-Timestamp Systems
      • 10.2.2 Optimistic Hybrid Systems
      • 10.2.3 Optimistic Hybrid Atomicity
      • 10.2.4 Local Optimistic Hybrid Atomicity
    • 10.3 An Optimistic Dependency-based Algorithm
      • 10.3.1 Optimistic Dependency Objects
      • 10.3.2 Correctness Proof
    • 10.4 Optimistic Pseudotime Systems
      • 10.4.1 Optimisitic Pseudotimes Systems
      • 10.4.2 Optimistic Static Atomicity
      • 10.4.3 Local Optimistic Static Atomicity
    • 10.5 An Optimistic Version fo Reed's Algorithm
      • 10.5.1 Correctness Proof
    • 10.6 Discussion
    • 10.7 Bibliographic Notes
    • 10.8 Exercises
  • 11 Orphan Management Algorithms
    • 11.1 Introduction
    • 11.2 The Orphan Management Problem
    • 11.3 An Affects Relation
    • 11.4 Filtered Systems
      • 11.4.1 The Filtered Database
      • 11.4.2 The Filtered System
      • 11.4.3 Simulation of the Generic System by the Filtered System
    • 11.5 Piggyback Systems
      • 11.5.1 The Piggyback Database
      • 11.5.2 The Piggyback System
      • 11.5.3 Simulation of the Generic System by the Piggyback System
    • 11.6 Strictly Filtered Systems
      • 11.6.1 The Strictly Filtered Database
      • 11.6.2 The Strictly Filtered System
      • 11.6.3 Simulation of the Generic System by the Clock System
    • 11.7 Clock Systems
      • 11.7.1 The Clock Database
      • 11.7.2 The Clock System
      • 11.7.3 Simulation of the Generic System by the Clock System
    • 11.8 Discussion
    • 11.9 Bibliographic Notes
    • 11.10 Exercises
  • 12 Replication
    • 12.1 Introduction
    • 12.2 Configurations
    • 12.3 Fixed Configuration Quorum Consensus
      • 12.3.1 System A, the Unreplicated Serial Sytem
      • 12.3.2 System B, the Fixed Configuation Quorum Consensus Algorithm
      • 12.3.3 Correctness Proof
    • 12.4 Reconfigurable Quorum Consensus
      • 12.4.1 System A, the Unreplicated Serial System with Dummy Reconfiguration
      • 12.4.2 System B, the Reconfigurable Quorum Consensus Algorithm with a Centralized Configuration
      • 12.4.3 Correctness Proof
      • 12.4.4 System C, the Reconfiturable Quorum Consensus Algorithm with Replicated Configurations
      • 12.4.5 Correctness Proof
    • 12.5 Concurrent Replicated Systems
    • 12.6 Discussion
    • 12.7 Bibliographic Notes
    • 12.8 Exercises
  • A Mathematical Concepts
    • A.1 Intorduction
    • A.2 Sets
    • A.3 Tuples
    • A.4 Relations
    • A.5 Functions and Partial Functions
    • A.6 Trees
    • A.7 Sequences
  • Bibliography
  • Index

Description

Atomic Transactions: In Concurrent and Distributed Systems
by Nancy Lynch, Michael Merritt, William Weihl and Alan Fekete

  • Foreward
  • Preface
  • 1. Introduction
    • 1.1 Distributed Systems
    • 1.2 Atomic Transactions for Distributed Systems
      • 1.2.1 Atomic Databases
      • 1.2.2 Transactions
      • 1.2.3 Nested Transactions
    • 1.3 Transaction-Processing Algorithms
      • 1.3.1 Locking
      • 1.3.2 Timestamps
      • 1.3.3 Optimistic Algorithms
      • 1.3.4 Replication
      • 1.3.5 Recovery
    • 1.4 Formal Models
      • 1.4.1 Why a Formal Model?
      • 1.4.2 An Operational Automation Model
      • 1.4.3 Correct Systems Simulate Serial System
    • 1.5 Comparisons with the Classical Theory
      • 1.5.1 Serializability
      • 1.5.2 Classical Treatment of Recovery
      • 1.5.3 Data Types and Nesting
      • 1.5.4 Operational versus Axiomatic Model
      • 1.5.5 A Finer Granularity of Analysis
    • 1.6 Contents of This Book
      • 1.6.1 The Basic Theory
      • 1.6.2 Fundamental Transaction-Processing Algorithms
      • 1.6.3 More Advanced Transaction-Processing Algorithms
    • 1.7 Bibliographic Notes
      • 1.7.1 Transactions
      • 1.7.2 Correctness Conditions
      • 1.7.3 Algorithms for Concurrency Control and Recovery
  • 2 An Automation Model
    • 2.1 Introduction
    • 2.2 Action Signatures
    • 2.3 Automata
      • 2.3.1 Conventions: Transition Relations
      • 2.3.2 More Examples of Automata
    • 2.4 Executions and Behaviors
    • 2.5 Composition
      • 2.5.1 Compositiona of Action Signatures
      • 2.5.2 Composition of Automata
      • 2.5.3 Properties of Systems of Automata
    • 2.6 Proofs about Automata
    • 2.7 Relationships between Automata
      • 2.7.1 Implementation
      • 2.7.2 Possibilities Mappings
    • 2.8 Preserving Properties
    • 2.9 Discussion
      • 2.9.1 Process Algebras
      • 2.9.2 State-based Models
      • 2.9.3 Uses of Models
    • 2.10 Bibliographic Notes
    • 2.11 Exercises
  • 3 Serial Systems and Correctness
    • 3.1 Introduction
    • 3.2 System Types
    • 3.3 General Structure of Serial Systems
    • 3.4 Serial Actions and Well-Formedness
      • 3.4.1 Basic Definitions
      • 3.4.2 Well-Formedness
    • 3.5 Serial Systems
      • 3.5.1 Transaction Automata
      • 3.5.2 Serial Object Automata
      • 3.5.3 The Serial Scheduler
      • 3.5.4 Serial Systems, Executions, Schedules and Behaviors
      • 3.5.5 Convention: Fixing the System Type and Serial System
    • 3.6 Atomicity
      • 3.6.1 Atomicity of Action Sequences
      • 3.6.2 Atomicity of Systems
      • 3.6.3 Stronger Correctness Conditions
      • 3.6.4 Atomicity and Intuition
      • 3.6.5 Implications for Schedules and Executions
      • 3.6.6 Correctness of Infinite Behaviors
    • 3.7 An Additional Example
    • 3.8 Bibliographic Notes
    • 3.9 Exercises
  • 4 Special Classes of Serial Systems
    • 4.1 Introduction
    • 4.2 Equieffectiveness
    • 4.3 Commutativity
      • 4.3.1 Forward Commutativity
      • 4.3.2 Backward Commutativity
    • 4.4 Special Classes of Operations
      • 4.4.1 Transparent Operations
      • 4.4.2 Obliterating Operations
    • 4.5 Serial Dependency Relations
    • 4.6 Bibliographic Notes
    • 4.7 Exercises
  • 5 The Atomicity Theorem
    • 5.1 Introduction
    • 5.2 Visibility
    • 5.3 Simle Systems
      • 5.3.1 Simple Database
      • 5.3.2 Simple Systems, Executions, Schedules, and Behaviors
    • 5.4 Event and Transaction Orders
      • 5.4.1 SD-Affects Order
      • 5.4.2 Affects Order
      • 5.4.3 Sibling Orders
    • 5.5 Atomicity Theorem and Proof Sketch
    • 5.6 Proof of the Atomicity
      • 5.6.1 Pictures
      • 5.6.2 Behavior of Transactons
      • 5.6.3 Behavior of Serial Objects
      • 5.6.4 Behavior of the Serial Scheduler
      • 5.6.5 Proof of the Main Result
    • 5.7 Discussion
    • 5.8 Bibliographic Notes
    • 5.9 Exercises
  • 6 Locking Algorithms
    • 6.1 Introduction
    • 6.2 Dyamic Atomicity
      • 6.2.1 Completion Order
      • 6.2.2. Generic Systems
      • 6.2.3 Dyamic Atomicity
      • 6.2.4 Local Dyamic Atomicity
    • 6.3 General Commutativity-based Locking
      • 6.3.1 Locking Objects
      • 6.3.2 Correctness Proof
    • 6.4 Moss's Algorithm
      • 6.4.1 Moss Objects
      • 6.4.2 Correctness Proof
      • 6.4.3 Read/Write Locking Algorithm
    • 6.5 General Undo Logging Algorithm
      • 6.5.1 General Undo Logging Objects
      • 6.5.2 Correctness Proof
    • 6.6 Discussion
    • 6.7 Bibliographic Notes
    • 6.8 Exercises
  • 7 Timestamp Algorithms
    • 7.1 Introduction
    • 7.2 Simple-Pseudotime Systems
      • 7.2.1 Simple-Pseudotime Database
      • 7.2.2 Simple-Pseudotime Systems, Executions, Schedules, and Behaviors
    • 7.3 Static Atomicity
      • 7.3.1 Pseudotime Order
      • 7.3.2 Pseudotime Systems
      • 7.3.3 Static Atomicity
      • 7.3.4 Local Static Atomicity
    • 7.4 Reed's Algorithm
      • 7.4.1 Reed Objects
      • 7.4.2 Correctness Proof
      • 7.4.3 A Concrete Implementation
      • 7.4.4 Correctness Proof
    • 7.5 Type-specific Concurrency Control
      • 7.5.1 Herlihy Objects
      • 7.5.2 Correctness Proof
    • 7.6 Discussion
    • 7.7 Bibliographic Notes
    • 7.8 Exercises
  • 8 Hybrid Algorithms
    • 8.1 Introduction
    • 8.2 Hybrid Atomicity
      • 8.2.1 Hybrid Systems
      • 8.2.2 Hybrid Atomicity
      • 8.2.3 Local Hybrid Atomicity
    • 8.3 Dependecy-Based Hybrid Locking
      • 8.3.1 Dependency Objects
      • 8.3.2 Correctness Proof
    • 8.4 Discussion
    • 8.5 Bibliographic Notes
    • 8.6 Exercises
  • 9 Relationship to the Classical Theory
    • 9.1 Introduction
    • 9.2 Assumptions
      • 9.2.1 Read/Write Serial Objects
      • 9.2.2 Appropriate Return Values
      • 9.2.3 A Sufficient Condition for Appropriate Return Values
    • 9.3 The Serialization Graph Construction
    • 9.4 Moss's Algorithm
    • 9.5 Extension to General Data Types
      • 9.5.1 Serialization Graphs
      • 9.5.2 An Undo Logging Algorithm
    • 9.6 Discussion
    • 9.7 Bibliographic Notes
    • 9.8 Exercises
  • 10 Optimistic Algorithms
    • 10.1 Introduction
    • 10.2 Optimistic Hybrid Systems
      • 10.2.1 Simple-Timestamp Systems
      • 10.2.2 Optimistic Hybrid Systems
      • 10.2.3 Optimistic Hybrid Atomicity
      • 10.2.4 Local Optimistic Hybrid Atomicity
    • 10.3 An Optimistic Dependency-based Algorithm
      • 10.3.1 Optimistic Dependency Objects
      • 10.3.2 Correctness Proof
    • 10.4 Optimistic Pseudotime Systems
      • 10.4.1 Optimisitic Pseudotimes Systems
      • 10.4.2 Optimistic Static Atomicity
      • 10.4.3 Local Optimistic Static Atomicity
    • 10.5 An Optimistic Version fo Reed's Algorithm
      • 10.5.1 Correctness Proof
    • 10.6 Discussion
    • 10.7 Bibliographic Notes
    • 10.8 Exercises
  • 11 Orphan Management Algorithms
    • 11.1 Introduction
    • 11.2 The Orphan Management Problem
    • 11.3 An Affects Relation
    • 11.4 Filtered Systems
      • 11.4.1 The Filtered Database
      • 11.4.2 The Filtered System
      • 11.4.3 Simulation of the Generic System by the Filtered System
    • 11.5 Piggyback Systems
      • 11.5.1 The Piggyback Database
      • 11.5.2 The Piggyback System
      • 11.5.3 Simulation of the Generic System by the Piggyback System
    • 11.6 Strictly Filtered Systems
      • 11.6.1 The Strictly Filtered Database
      • 11.6.2 The Strictly Filtered System
      • 11.6.3 Simulation of the Generic System by the Clock System
    • 11.7 Clock Systems
      • 11.7.1 The Clock Database
      • 11.7.2 The Clock System
      • 11.7.3 Simulation of the Generic System by the Clock System
    • 11.8 Discussion
    • 11.9 Bibliographic Notes
    • 11.10 Exercises
  • 12 Replication
    • 12.1 Introduction
    • 12.2 Configurations
    • 12.3 Fixed Configuration Quorum Consensus
      • 12.3.1 System A, the Unreplicated Serial Sytem
      • 12.3.2 System B, the Fixed Configuation Quorum Consensus Algorithm
      • 12.3.3 Correctness Proof
    • 12.4 Reconfigurable Quorum Consensus
      • 12.4.1 System A, the Unreplicated Serial System with Dummy Reconfiguration
      • 12.4.2 System B, the Reconfigurable Quorum Consensus Algorithm with a Centralized Configuration
      • 12.4.3 Correctness Proof
      • 12.4.4 System C, the Reconfiturable Quorum Consensus Algorithm with Replicated Configurations
      • 12.4.5 Correctness Proof
    • 12.5 Concurrent Replicated Systems
    • 12.6 Discussion
    • 12.7 Bibliographic Notes
    • 12.8 Exercises
  • A Mathematical Concepts
    • A.1 Intorduction
    • A.2 Sets
    • A.3 Tuples
    • A.4 Relations
    • A.5 Functions and Partial Functions
    • A.6 Trees
    • A.7 Sequences
  • Bibliography
  • Index

Details

No. of pages:
476
Language:
English
Copyright:
© Morgan Kaufmann 1993
Published:
Imprint:
Morgan Kaufmann
eBook ISBN:
9780080499543
Hardcover ISBN:
9781558601048

About the Authors

Nancy Lynch Author

About the author:
Nancy A. Lynch is a professor of electrical engineering and computer science at MIT and heads MIT's Theory of Distributed Systems research group. She is the author of numerous research articles about distributed algorithms and impossibility results, and about formal modeling and verification of distributed systems.

Michael Merritt Author

Michael Merritt, AT&T

William Weihl Author

William E. Weihl, Massachusetts Institute of Technololgy

Alan Fekete Author

Alan Fekete, University of Sydney