How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
1979/09/01 by Lamport · 2,531 citations
Computer Science · #Computer science #Embedded Systems Design Techniques #Execution time #Logic, programming, and type systems #Multiprocessing #Operating system #Order (exchange) #Out-of-order execution #Parallel Computing and Optimization Techniques #Parallel computing #Programming language
paper · doi:10.1109/tc.1979.1675439
published in IEEE Transactions on Computers C-28(9), 690-691 (Institute of Electrical and Electronics Engineers)
openalex publication_date 1979/09/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/25
Abstract
Many large sequential computers execute operations in a different order than is specified by the program. A correct execution is achieved if the results produced are the same as would be produced by executing the program steps in order. For a multiprocessor computer, such a correct execution by each processor does not guarantee the correct execution of the entire program. Additional conditions are given which do guarantee that a computer correctly executes multiprocess programs.
Cited by
- On Composition and Implementation of Sequential Consistency (Extended Version)
- Accelerating Language Model Workflows with Prompt Choreography
- Fork Sequential Consistency is Blocking
- Taming Weak Memory Models
- Actor Model of Computation: Scalable Robust Information Systems
- Decidability of Liveness on the TSO Memory Model
- Formal Modelling, Testing and Verification of HSA Memory Models using Event-B
- Thread-Modular Static Analysis for Relaxed Memory Models
- Multi-Version Coding - An Information Theoretic Perspective of Consistent Distributed Storage
- Analyzing the memory ordering models of the Apple M1
- How to make a correct multiprocess program execute correctly on a multiprocessor
- Linearizability: a correctness condition for concurrent objects
- Mastering Concurrent Computing Through Sequential Thinking: A Half-century Evolution
- Context-Bounded Model Checking for POWER
- Parallelized sequential composition, pipelines, and hardware weak memory models
- A methodology for implementing highly concurrent data objects
- A Concurrency Problem with Exponential DPLL(T) Proofs
- Creek: Low-latency, Mixed-Consistency Transactional Replication Scheme
- Wait-free synchronization
- The Impact of Memory Models on Software Reliability in Multiprocessors
- Local Linearizability
- Formalizing and Implementing Distributed Ledger Objects
- Enabling the Adoption of Processing-in-Memory: Challenges, Mechanisms, Future Research Directions
- A Unified Theory of Shared Memory Consistency
- AllConcur: Leaderless Concurrent Atomic Broadcast (Extended Version)
- Behavioural Theory of Reflective Algorithms II: Reflective Parallel Algorithms
- A Proof of Correctness for the Tardis Cache Coherence Protocol
- Consistency in Non-Transactional Distributed Storage Systems
- Weak Memory Model Formalisms: Introduction and Survey
- Verifying PRAM Consistency over Read/Write Traces of Data Replicas
- Simple Executions of Snapshot Implementations
- On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency
- Virtual-Link: A Scalable Multi-Producer, Multi-Consumer Message Queue Architecture for Cross-Core Communication
- Vive la Différence: Paxos vs. Viewstamped Replication vs. Zab
- Tardis 2.0: Optimized Time Traveling Coherence for Relaxed Consistency Models
- Shared memory consistency models: a tutorial
- Accelerating Federated Learning in Heterogeneous Data and Computational Environments
- Quantifiability: Concurrent Correctness from First Principles
- Global Clock, Physical Time Order and Pending Period Analysis in Multiprocessor Systems
- An Epistemic Perspective on Consistency of Concurrent Computations
- Performance of memory reclamation for lockless synchronization
- Safety Verification of Parameterized Systems under Release-Acquire
- No more, no less - A formal model for serverless computing
- PrideMM: A Solver for Relaxed Memory Models
- Consistency models with global operation sequencing and their composition (extended version)
- Scaling Replicated State Machines with Compartmentalization [Technical Report]
- Practical Concurrent Priority Queues
- Compiling a Calculus for Relaxed Memory: Practical constraint-based low-level concurrency
- Technical Report: Benefits of Stabilization versus Rollback in Self-Stabilizing Graph-Based Applications on Eventually Consistent Key-Value Stores
- Cheap Recovery: A Key to Self-Managing State
- Checking Robustness against TSO
- Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models
- Armed Cats
- TARDIS: Timestamp based Coherence Algorithm for Distributed Shared Memory
- Oh-RAM! One and a Half Round Atomic Memory
- New Lace and Arsenic: adventures in weak memory with a program logic
- GraphLab: A Distributed Framework for Machine Learning in the Cloud
- Evaluating Cache Coherent Shared Virtual Memory for Heterogeneous Multicore Chips
- Locality and Singularity for Store-Atomic Memory Models
- Algorithms for Timed Consistency Models
- An Operational Framework for Specifying Memory Models using Instantaneous Instruction Execution
- CoVer-ability: Consistent Versioning for Concurrent Objects
- Coherent Causal Memory
- Regional Consistency: Programmability and Performance for Non-Cache-Coherent Systems
- Between Linearizability and Quiescent Consistency: Quantitative Quiescent Consistency
- Robustness against Power is PSPACE-complete
- Efficient System-Enforced Deterministic Parallelism
- Application-Aware Consistency: An Application to Social Network
- X10
- Deterministic Consistency: A Programming Model for Shared Memory Parallelism
- On the Design of Distributed Programming Models
- Thriving in a crowded and changing world: C++ 2006–2020
- An ACL2 Mechanization of an Axiomatic Framework for Weak Memory
- Inconsistency Robustness in Foundations: Mathematics self proves its own Consistency and Other Matters
- A Scalable Transaction Management Framework for Consistent Document-Oriented NoSQL Databases
- RealityCheck: Bringing Modularity, Hierarchy, and Abstraction to Automated Microarchitectural Memory Consistency Verification
- The PowerPC 603 microprocessor
- Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations
- Single-Producer/Single-Consumer Queues on Shared Cache Multi-Core Systems
- Overhauling SC atomics in C11 and OpenCL
- Weak Memory Models with Matching Axiomatic and Operational Definitions
- A true positives theorem for a static race detector
- Concurrent computing [wikipedia]
- On Grid Quorums for Erasure Coded Data. [europepmc]
Related