Concurrency : The Works of Leslie Lamport / Dahlia Malkhi

Format:

Book

Author/Creator:

Malkhi, Dahlia, editor.

Series:

ACM books - Collection 2 ; #29.

ACM books, 2374-6777 ; #29

Language:

English

Subjects (All):

Hardware & Software (Computer Science).

Genre:

Electronic books.

Physical Description:

1 online resource (xx, 345 pages) LuaTEX

Edition:

First Edition

Place of Publication:

[New York, NY, USA] : Association for Computing Machinery; [2019].

System Details:

Mode of access: World Wide Web

System requirements: Adobe Acrobat Reader

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.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

The Partial Ordering

Logical Clocks

Ordering the Events Totally

Anomalous Behavior

Physical Clocks

Appendix

How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs

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

The Mutual Exclusion Problem: Part I-A Theory of Interprocess Communication

Abstract

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

Acknowledgments

The Mutual Exclusion Problem: Part II-Statement and Solutions

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

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.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

References

Index

Biographies

Other Format:

Print version:

ISBN:

3335772

9781450372732

9781450372725

Access Restriction:

Restricted for use by site license.