Concurrency

Description

This book is a celebration of Leslie Lamport's work on concurrency, interwoven in four-and-a-half decades of an evolving industry: from the introduction of the first personal computer to an era when parallel and distributed multiprocessors are abundant.

His works lay formal foundations for concurrent computations executed by interconnected computers. Some of the algorithms have become standard engineering practice for fault tolerant distributed computing – distributed systems that continue to function correctly despite failures of individual components. He also developed a substantial body of work on the formal specification and verification of concurrent systems, and has contributed to the development of automated tools applying these methods.

Part I consists of technical chapters of the book and a biography. The technical chapters of this book present a retrospective on Lamport's original ideas from experts in the field. Through this lens, it portrays their long-lasting impact. The chapters cover timeless notions Lamport introduced: the Bakery algorithm, atomic shared registers and sequential consistency; causality and logical time; Byzantine Agreement; state machine replication and Paxos; temporal logic of actions (TLA). The professional biography tells of Lamport's career, providing the context in which his work arose and broke new grounds, and discusses LaTeX – perhaps Lamport’s most influential contribution outside the field of concurrency. This chapter gives a voice to the people behind the achievements, notably Lamport himself, and additionally the colleagues around him, who inspired, collaborated, and helped him drive worldwide impact. Part II consists of a selection of Leslie Lamport's most influential papers.

This book touches on a lifetime of contributions by Leslie Lamport to the field of concurrency and on the extensive influence he had on people working in the field. It will be of value to historians of science, and to researchers and students who work in the area of concurrency and who are interested to read about the work of one of the most influential researchers in this field.

• Preface


• Photo and Text Credits


• Introduction


• The Computer Science of Concurrency: The Early Years


• PART I TECHNICAL PERSPECTIVES ON LAMPORT'S WORK
  • Shared Memory and the Bakery Algorithm
  • The Notions of Time and Global State in a Distributed System
  • Byzantine Faults
  • State Machine Replication with Benign Failures
  • Formal Specification and Verification
  • Biography


• PART II SELECTED PAPERS
  • A New Solution of Dijkstra's Concurrent Programming Problem
  • Time, Clocks, and the Ordering of Events in a Distributed System
  • How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
  • The Byzantine Generals Problem
  • The Mutual Exclusion Problem: Part I—A Theory of Interprocess Communication
  • The Mutual Exclusion Problem: Part II—Statement and Solutions
  • The Part-Time Parliament


• References


• Index


• Biographies

Sujets

• Distributed Systems
• Computers
• Informatique
• Distributed computing

Informations

• Publié par: Association for Computing Machinery and Morgan & Claypool Publishers
• Date de parution: 16 septembre 2019
• Nombre de lectures: 0
• EAN13: 9781450372725
• Langue: English
• Poids de l'ouvrage: 5 Mo

Extrait

Concurrency
ACM Books
Editor in Chief
M. Tamer Özsu, University of Waterloo
ACM Books is a series of high-quality books for the computer science community, published by ACM and many in collaboration with Morgan & Claypool Publishers. ACM Books publications are widely distributed in both print and digital formats through booksellers and to libraries (and library consortia) and individual ACM members via the ACM Digital Library platform.
Concurrency: The Works of Leslie Lamport
Dahlia Malkhi, VMware Research and Calibra
2019
Providing Sound Foundations for Cryptography: On the work of Shafi Goldwasser and Silvio Micali
Oded Goldreich, Weizmann Institute of Science
2019
The Essentials of Modern Software Engineering: Free the Practices from the Method Prisons!
Ivar Jacobson, Ivar Jacobson International
Harold “Bud” Lawson, Lawson Konsult AB (deceased)
Pan-Wei Ng, DBS Singapore
Paul E. McMahon, PEM Systems
Michael Goedicke, Universität Duisburg–Essen
2019
Data Cleaning
Ihab F. Ilyas, University of Waterloo
Xu Chu, Georgia Institute of Technology
2019
Conversational UX Design: A Practitioner’s Guide to the Natural Conversation Framework
Robert J. Moore, IBM Research–Almaden
Raphael Arar, IBM Research–Almaden
2019
Heterogeneous Computing: Hardware and Software Perspectives
Mohamed Zahran, New York University
2019
Hardness of Approximation Between P and NP
Aviad Rubinstein, Stanford University
2019
The Handbook of Multimodal-Multisensor Interfaces, Volume 3: Language Processing, Software, Commercialization, and Emerging Directions
Editors: Sharon Oviatt, Monash University
Björn Schuller, Imperial College London and University of Augsburg
Philip R. Cohen, Monash University
Daniel Sonntag, German Research Center for Artificial Intelligence (DFKI)
Gerasimos Potamianos, University of Thessaly
Antonio Krüger, Saarland University and German Research Center for Artificial Intelligence (DFKI)
2019
Making Databases Work: The Pragmatic Wisdom of Michael Stonebraker
Editor: Michael L. Brodie, Massachusetts Institute of Technology
2018
The Handbook of Multimodal-Multisensor Interfaces, Volume 2: Signal Processing, Architectures, and Detection of Emotion and Cognition
Editors: Sharon Oviatt, Monash University
Björn Schuller, University of Augsburg and Imperial College London
Philip R. Cohen, Monash University
Daniel Sonntag, German Research Center for Artificial Intelligence (DFKI)
Gerasimos Potamianos, University of Thessaly
Antonio Krüger, Saarland University and German Research Center for Artificial Intelligence (DFKI)
2018
Declarative Logic Programming: Theory, Systems, and Applications
Editors: Michael Kifer, Stony Brook University
Yanhong Annie Liu, Stony Brook University
2018
The Sparse Fourier Transform: Theory and Practice
Haitham Hassanieh, University of Illinois at Urbana-Champaign
2018
The Continuing Arms Race: Code-Reuse Attacks and Defenses
Editors: Per Larsen, Immunant, Inc.
Ahmad-Reza Sadeghi, Technische Universität Darmstadt
2018
Frontiers of Multimedia Research
Editor: Shih-Fu Chang, Columbia University
2018
Shared-Memory Parallelism Can Be Simple, Fast, and Scalable
Julian Shun, University of California, Berkeley
2017
Computational Prediction of Protein Complexes from Protein Interaction Networks
Sriganesh Srihari, The University of Queensland Institute for Molecular Bioscience
Chern Han Yong, Duke-National University of Singapore Medical School
Limsoon Wong, National University of Singapore
2017
The Handbook of Multimodal-Multisensor Interfaces, Volume 1: Foundations, User Modeling, and Common Modality Combinations
Editors: Sharon Oviatt, Incaa Designs
Björn Schuller, University of Passau and Imperial College London
Philip R. Cohen, Voicebox Technologies
Daniel Sonntag, German Research Center for Artificial Intelligence (DFKI)
Gerasimos Potamianos, University of Thessaly
Antonio Krüger, Saarland University and German Research Center for Artificial Intelligence (DFKI)
2017
Communities of Computing: Computer Science and Society in the ACM
Thomas J. Misa, Editor, University of Minnesota
2017
Text Data Management and Analysis: A Practical Introduction to Information Retrieval and Text Mining
ChengXiang Zhai, University of Illinois at Urbana–Champaign
Sean Massung, University of Illinois at Urbana–Champaign
2016
An Architecture for Fast and General Data Processing on Large Clusters
Matei Zaharia, Stanford University
2016
Reactive Internet Programming: State Chart XML in Action
Franck Barbier, University of Pau, France
2016
Verified Functional Programming in Agda
Aaron Stump, The University of Iowa
2016
The VR Book: Human-Centered Design for Virtual Reality
Jason Jerald, NextGen Interactions
2016
Ada’s Legacy: Cultures of Computing from the Victorian to the Digital Age
Robin Hammerman, Stevens Institute of Technology
Andrew L. Russell, Stevens Institute of Technology
2016
Edmund Berkeley and the Social Responsibility of Computer Professionals
Bernadette Longo, New Jersey Institute of Technology
2015
Candidate Multilinear Maps
Sanjam Garg, University of California, Berkeley
2015
Smarter Than Their Machines: Oral Histories of Pioneers in Interactive Computing
John Cullinane, Northeastern University; Mossavar-Rahmani Center for Business and Government, John F. Kennedy School of Government, Harvard University
2015
A Framework for Scientific Discovery through Video Games
Seth Cooper, University of Washington
2014
Trust Extension as a Mechanism for Secure Code Execution on Commodity Computers
Bryan Jeffrey Parno, Microsoft Research
2014
Embracing Interference in Wireless Systems
Shyamnath Gollakota, University of Washington
2014

Concurrency
The Works of Leslie Lamport
Dahlia Malkhi, editor
VMware Research and Calibra
ACM Books #29
Copyright © 2019 by Association for Computing Machinery
All rights reserved. No part of this publication may be reproduced, stored in a retrieval system, or transmitted in any form or by any means—electronic, mechanical, photocopy, recording, or any other except for brief quotations in printed reviews—without the prior permission of the publisher.
Designations used by companies to distinguish their products are often claimed as trademarks or registered trademarks. In all instances in which the Association for Computing Machinery is aware of a claim, the product names appear in initial capital or all capital letters. Readers, however, should contact the appropriate companies for more complete information regarding trademarks and registration.
Concurrency: The Works of Leslie Lamport
Dahlia Malkhi, editor
books.acm.org
http://books.acm.org
ISBN: 978-1-4503-7270-1 hardcover
ISBN: 978-1-4503-7271-8 paperback
ISBN: 978-1-4503-7273-2 eBook
ISBN: 978-1-4503-7272-5 EPUB
Series ISSN: 2374-6769 print 2374-6777 electronic
DOIs:
10.1145/3335772 Book
10.1145/3335772.3335781 Chapter 6
10.1145/3335772.3335773 Preface
10.1145/3335772.3335782 Paper 1
10.1145/3335772.3335774 Introduction
10.1145/3335772.3335934 Paper 2
10.1145/3335772.3335775 Paper 0
10.1145/3335772.3335935 Paper 3
10.1145/3335772.3335776 Chapter 1
10.1145/3335772.3335936 Paper 4
10.1145/3335772.3335777 Chapter 2
10.1145/3335772.3335937 Paper 5
10.1145/3335772.3335778 Chapter 3
10.1145/3335772.3335938 Paper 6
10.1145/3335772.3335779 Chapter 4
10.1145/3335772.3335939 Paper 7
10.1145/3335772.3335780 Chapter 5
10.1145/3335772.3335940 References/Index/Bios
A publication in the ACM Books series, #29
Editor in Chief: M. Tamer Özsu, University of Waterloo
This book was typeset in Arnhem Pro 10/14 and Flama using ZzT E X.
First Edition
10 9 8 7 6 5 4 3 2 1
Contents
Preface
Photo and Text Credits
Introduction
Dahlia Malkhi, Idit Keidar
Chapter 1: Shared Memory and the Bakery Algorithm
Chapter 2: The Notions of Time and Global State in a Distributed System
Chapter 3: Byzantine Faults
Chapter 4: State Machine Replication with Benign Failures
Chapter 5: Formal Specification and Verification
Chapter 6: Biography
Closing Remarks
The Computer Science of Concurrency: The Early Years
Leslie Lamport
1 Foreword
2 The Beginning: Mutual Exclusion
3 Producer-Consumer Synchronization
4 Distributed Algorithms
5 Afterwards
References
PART I TECHNICAL PERSPECTIVES ON LAMPORT’S WORK
Chapter 1 Shared Memory and the Bakery Algorithm
Hagit Attiya, Jennifer L. Welch
1.1 Introduction
1.2 Flavors of the Bakery Algorithm
1.3 A Plethora of Registers
1.4 A New Model for Describing Concurrency
1.5 Sequential Consistency
Chapter 2 The Notions of Time and Global State in a Distributed System
Karolos Antoniadis, Rachid Guerraoui
2.1 Introduction
2.2 The Notion of Logical Time
2.3 The Distributed State Machine Abstraction
2.4 The Notion of Distributed Global State
2.5 Conclusion
Chapter 3 Byzantine Faults
Christian Cachin
3.1 Introduction
3.2 Byzantine Agreement
3.3 Byzantine Clock Synchronization
3.4 Digital Signatures
Chapter 4 State Machine Replication with Benign Failures
Robbert van Renesse
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.6 Paxos
4.7 Dynamic Reconfiguration
Chapter 5 Formal Specification and Verification
Stephan Merz
5.1 Introduction
5.2 The Temporal Logic of Actions
5.3 The Specification Language tla +
5.4 PlusCal: An Algorithm Language
5.5 Tool Support
5.6 Impact
Chapter 6 Biography
Roy Levin
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
Leslie Lamport
Introduction
The Algor