Cover Image

Concurrency : The Works of Leslie Lamport /

Bibliographic Details
Other Authors: Malkhi, Dahlia (Editor)
Format: eBook
Language:English
Published: [New York, NY, USA] : Association for Computing Machinery, [2019]
Edition:First Edition.
Series:ACM books - Collection 2 ; #29.
Subjects:
Hardware & Software (Computer Science)
Electronic books.
Online Access:Connect to the full text of this electronic book
Table of Contents:
  • PART I TECHNICAL PERSPECTIVES ON LAMPORT'S WORK
  • 1 Shared Memory and the Bakery Algorithm
  • 1.1 Introduction
  • 1.2 Flavors of the Bakery Algorithm
  • 1.2.1 The Mutual Exclusion Problem
  • 1.2.2 The Bakery Algorithm
  • 1.2.3 Weakening the Shared Variables
  • 1.3 A Plethora of Registers
  • 1.3.1 Increasing the Number of Readers
  • 1.3.2 Increasing the Number of Values
  • 1.3.3 Strengthening the Consistency Condition
  • 1.3.4 Increasing the Number of Writers
  • 1.4 A New Model for Describing Concurrency
  • 1.5 Sequential Consistency
  • 2 The Notions of Time and Global State in a Distributed System
  • 2.1 Introduction
  • 2.2 The Notion of Logical Time
  • 2.2.1 Causality and Logical Time
  • 2.2.2 An Algorithm to Capture Causality
  • 2.2.3 Impact of Logical Time
  • 2.3 The Distributed State Machine Abstraction
  • 2.3.1 SMR Algorithm
  • 2.3.2 Impact of the Distributed State Machine Abstraction
  • 2.4 The Notion of Distributed Global State
  • 2.4.1 The Distributed Snapshot Algorithm
  • 2.4.2 Impact of Distributed Global State
  • 2.5 Conclusion
  • 3 Byzantine Faults
  • 3.1 Introduction
  • 3.2 Byzantine Agreement
  • 3.2.1 Definitions
  • 3.2.2 Implementations
  • 3.3 Byzantine Clock Synchronization
  • 3.4 Digital Signatures
  • 4 State Machine Replication with Benign Failures
  • 4.1 Active versus Passive Replication
  • 4.2 A Brief Review of State Machine Replication
  • 4.3 Benign System Models
  • 4.4 SMR Protocol Basics
  • 4.5 Early Asynchronous Consensus Protocols
  • 4.5.1 Ben-Or
  • 4.5.2 Dwork, Lynch, and Stockmeyer
  • 4.6 Paxos
  • 4.6.1 Read-Only Commands
  • 4.6.2 Discussion
  • 4.7 Dynamic Reconfiguration
  • 5 Formal Specification and Verification
  • 5.1 Introduction
  • 5.2 The Temporal Logic of Actions
  • 5.2.1 The Genesis of TLA
  • 5.2.2 The Logic TLA
  • 5.2.3 Refinement, Hiding, and Composition
  • 5.3 The Specification Language TLA+
  • 5.3.1 Overall Design of TLA+
  • 5.3.2 A Glimpse of TLA+
  • 5.3.3 Composing Modules
  • 5.4 PlusCal : An Algorithm Language
  • 5.5 Tool Support
  • 5.5 Tool Support
  • 5.5.1 The Model Checker TLC
  • 5.5.2 The tla + Proof System
  • 5.5.3 The TLA+ Toolbox
  • 5.6 Impact
  • 6 Biography
  • 6.1 Early Years
  • 6.2 Education and Early Employment
  • 6.3 The COMPASS Years (1970-1977)
  • 6.4 The SRI Years (1977-1985)
  • 6.5 The DEC/Compaq Years (1985-2001)
  • 6.6 The Microsoft Years (2001-)
  • 6.7 Honors
  • 6.8 Collegial Influences
  • PART II SELECTED PAPERS
  • A New Solution of Dijkstra's Concurrent Programming Problem
  • Introduction
  • The Algorithm
  • Proof of Correctness
  • Further Remarks
  • Conclusion
  • References
  • Time, Clocks, and the Ordering of Events in a Distributed System
  • Introduction
  • The Partial Ordering
  • Logical Clocks
  • Ordering the Events Totally
  • Anomalous Behavior
  • Physical Clocks
  • Conclusion
  • Appendix
  • References
  • How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
  • References
  • The Byzantine Generals Problem
  • 1 Introduction
  • 2 Impossibility Results
  • 3 A Solution with Oral Messages
  • 4 A Solution with Signed Messages
  • 5 Missing Communication Paths
  • 6 Reliable Systems
  • 7 Conclusion
  • References
  • The Mutual Exclusion Problem: Part I-A Theory of Interprocess Communication
  • Abstract
  • 1 Introduction
  • 2 The Model
  • 2.1 Physical Considerations
  • 2.2 System Executions
  • 2.3 Higher-Level Views
  • 3 Interprocess Communication
  • 4 Processes
  • 5 Multiple-Reader Variables
  • 6 Discussion of the Assumptions
  • 7 Conclusion
  • Acknowledgments
  • References
  • The Mutual Exclusion Problem: Part II-Statement and Solutions
  • Abstract
  • 1 Introduction
  • 2 The Problem
  • 2.1 Basic Requirements
  • 2.2 Fairness Requirements
  • 2.3 Premature Termination
  • 2.4 Failure
  • 3 The Solutions
  • 3.1 The Mutual Exclusion Protocol
  • 3.2 The One-Bit Solution
  • 3.3 A Digression
  • 3.4 The Three-Bit Algorithm
  • 3.5 FCFS Solutions
  • 4 Conclusion
  • References
  • The Part-Time Parliament
  • 1 The Problem
  • 1.1 The Island of Paxos
  • 1.2 Requirements
  • 1.3 Assumptions
  • 2 The Single-Decree Synod
  • 2.1 Mathematical Results
  • 2.2 The Preliminary Protocol
  • 2.3 The Basic Protocol
  • 2.4 The Complete Synod Protocol
  • 3 The Multidecree Parliament
  • 3.1 The Protocol
  • 3.2 Properties of the Protocol
  • 3.2.1 Definitions
  • 3.2.2 Behind Closed Doors
  • 3.3 Further Developments
  • 3.3.1 Picking a President
  • 3.3.2 Long Ledgers
  • 3.3.3 Bureaucrats
  • 3.3.4 Learning the Law
  • 3.3.5 Dishonest Legislators and Honest Mistakes
  • 3.3.6 Choosing New Legislators
  • 4 Relevance to Computer Science
  • 4.1 The State Machine Approach
  • 4.2 Commit Protocols
  • A.1 The Basic Protocol
  • A.2 Proof of Consistency
  • Acknowledgments
  • References
  • References
  • Index
  • Biographies