In Concurrent and Distributed Systems To order this title, and for more information, click here
By Nancy Lynch Michael Merritt William Weihl Alan Fekete
Description
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.
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
Books and book related electronic products are priced in US dollars (USD), euro (EUR), and Great Britain Pounds (GBP). USD prices apply to the Americas and Asia Pacific. EUR prices apply in Europe and the Middle East. GBP prices apply to the UK and all other countries.
Home | Elsevier Sites | Privacy Policy | Terms and Conditions | Feedback | Site Map | A Reed Elsevier Company