Save up to 30% on Elsevier print and eBooks with free shipping. No promo code needed.
Save up to 30% on print and eBooks.
Atomic Transactions
In Concurrent and Distributed Systems
1st Edition - August 1, 1993
Authors: Nancy A. Lynch, Michael Merritt, William E. Weihl, Alan Fekete
Language: English
Hardback ISBN:9781558601048
9 7 8 - 1 - 5 5 8 6 0 - 1 0 4 - 8
This book develops a theory for transactions that provides practical solutions for system developers, focusing on the interface between the user and the database that executes tr…Read more
Purchase options
LIMITED OFFER
Save 50% on book bundles
Immediately download your ebook while waiting for your print delivery. No promo code is needed.
This book develops a theory for transactions that provides practical solutions for system developers, focusing on the interface between the user and the database that executes transactions. Atomic transactions are a useful abstraction for programming concurrent and distributed data processing systems. Presents many important algorithms which provide maximum concurrency for transaction processing without sacrificing data integrity. The authors include a well-developed data processing case study to help readers understand transaction processing algorithms more clearly. The book offers conceptual tools for the design of new algorithms, and for devising variations on the familiar algorithms presented in the discussions. Whether your background is in the development of practical systems or formal methods, this book will offer you a new way to view distributed systems.
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
No. of pages: 476
Language: English
Edition: 1
Published: August 1, 1993
Imprint: Morgan Kaufmann
Hardback ISBN: 9781558601048
NL
Nancy A. Lynch
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.
MM
Michael Merritt
Michael Merritt, AT&T
WW
William E. Weihl
William E. Weihl, Massachusetts Institute of Technololgy