How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs

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.

• Publication year

  2016

• Venue

  IEEE transactions on computers

• Publication date

  2016-12-19

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/3335772.3335935
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Algebraic coding theory

  1984cited by this paper
• Comments on "An Approach to Highly Integrated Computer-Maintained Cellular Arrays"

  1979cited by this paper
• Algebraic Coding and Combinatorics a Tutorial Survey

  1978cited by this paper
• Erasure and Error Decoding for Semiconductor Memories

  1978cited by this paper
• Proving the Correctness of Multiprocess Programs

  1977cited by this paper
• Verifying properties of parallel programs: an axiomatic approach

  1976cited by this paper
• Minimum-distance bounds for binary linear codes

  1973cited by this paper
• A class of optimal minimum odd-weight-column SEC-DED codes

  1970cited by this paper
• Principles of data communication

  1968cited by this paper

• Towards Proving Liveness on Weak Memory (Extended Version)

  2026cites this paper
• A Scalable Transaction Management Framework for Consistent Document-Oriented NoSQL Databases

  2026cites this paper
• Event Horizon: Asymmetric Dependencies for Fast Geo-Distributed Operations

  2026cites this paper
• Consensus In Asynchrony

  2026cites this paper
• Parametrised Verification of Intel-x86 Programs

  2026cites this paper
• Trace Validation of Unmodified Concurrent Systems with OmniLink

  2026cites this paper
• Sequential Specifications for Precise Hardware Exceptions

  2025cites this paper
• Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic

  2025cites this paper
• RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency

  2025cites this paper
• CTXNL: A Software-Hardware Co-designed Solution for Efficient CXL-Based Transaction Processing

  2025cites this paper
• Formal Verification of a Custom Compiler for a Fully Homomorphic Encryption Accelerator

  2025cites this paper
• Fast Durably Linearizable Data Structures for Free

  2025cites this paper
• Elastic Relaxation of Concurrent Data Structures

  2025cites this paper
• A Pedagogical Framework for Developing Abstraction Skills

  2025cites this paper
• Behavioural Theory of Reflective Algorithms II: Reflective Parallel Algorithms

  2025cites this paper
• Pushing the boulder

  2025cites this paper
• TEMpesT: Testing Empirically for Memory Transistency

  2025cites this paper
• Data Race Detection by Digest-Driven Abstract Interpretation (Extended Version)

  2025cites this paper
• Sequentially Consistent Concurrent Encrypted Multimaps

  2025cites this paper
• Weak Memory Model Formalisms: Introduction and Survey

  2025cites this paper
• Optimal Concolic Dynamic Partial Order Reduction

  2025cites this paper
• Efficient Fault Tolerance for Stateful Serverless Computing with Asymmetric Logging

  2025cites this paper
• Coral: Fast Succinct Non-Interactive Zero-Knowledge CFG Proofs

  2025cites this paper
• Recipe: Hardware-Accelerated Replication Protocols: Rethinking Crash Fault Tolerance Protocols for Untrusted Cloud Environments

  2025cites this paper
• GPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency

  2025cites this paper
• Sufficient Conditions for Robustness of RDMA Programs

  2025influential citation
• LitmusKt: Concurrency Stress Testing for Kotlin

  2025cites this paper
• Relaxed Memory Concurrency Re-executed

  2025cites this paper
• A Generic Specification Framework for Weakly Consistent Replicated Data Types

  2025influential citation
• Enabling Efficient Transaction Processing on CXL-Based Memory Sharing

  2025cites this paper
• When You Have a Fuzzer, Everything Looks Like a Reachability Problem

  2025cites this paper
• Crossword: Adaptive Consensus for Dynamic Data-Heavy Workloads

  2025cites this paper
• Asynchronous Fault-Tolerant Language Decidability for Runtime Verification of Distributed Systems

  2025cites this paper
• FPS: Flexible Payment System

  2025cites this paper
• Accelerating Language Model Workflows with Prompt Choreography

  2025cites this paper
• Time, Fences and the Ordering of Events in TSO

  2025cites this paper
• Bodega: Serving Linearizable Reads Locally from Anywhere at Anytime via Roster Leases

  2025cites this paper
• A Novel Approach to Efficiently Verify Sequential Consistency in Concurrent Programs

  2025influential citation
• Cache Coherence Over Disaggregated Memory

  2024cites this paper
• SPORE: Combining Symmetry and Partial Order Reduction

  2024cites this paper
• KLNK: Expanding Page Boundaries in a Distributed Shared Memory System

  2024cites this paper
• PredRacer: Predictively Detecting Data Races in Android Applications

  2024cites this paper
• Opca: Enabling Optimistic Concurrent Access for Multiple Users in Oblivious Data Storage

  2024cites this paper
• What Cannot Be Implemented on Weak Memory?

  2024cites this paper
• Compositional Semantics for Shared-Variable Concurrency

  2024cites this paper
• General-Purpose Multicore Architectures

  2024cites this paper
• AMECOS: A Modular Event-based Framework for Concurrent Object Specification

  2024cites this paper
• Efficient Auditing of Event-driven Web Applications

  2024cites this paper
• Reachability and Safety Games under TSO Semantics (Extended Version)

  2024cites this paper
• Automating Memory Model Metatheory with Intersections

  2024cites this paper
• Concurrent Encrypted Multimaps

  2024cites this paper
• HiRace: Accurate and Fast Data Race Checking for GPU Programs

  2024cites this paper
• RaceHunter Dynamic Data Race Detector

  2024cites this paper
• Atomic Cache: Enabling Efficient Fine-Grained Synchronization with Relaxed Memory Consistency on GPGPUs Through In-Cache Atomic Operations

  2024cites this paper
• Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models

  2024cites this paper
• CHC-Based Verification of Programs Through Graph Decompositions

  2024cites this paper
• Formal Definitions and Performance Comparison of Consistency Models for Parallel File Systems

  2024cites this paper
• HiRace: Accurate and Fast Source-Level Race Checking of GPU Programs

  2024cites this paper
• Enhancing GenMC's Usability and Performance

  2024cites this paper
• Formalisation of a New Weak Semantics for AuDaLa

  2024cites this paper
• Trace Semantics for C++11 Memory Model

  2024cites this paper
• Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware

  2024cites this paper
• A Fully Verified Persistency Library

  2024cites this paper
• A Runtime System for Interruptible Query Processing: When Incremental Computing Meets Fine-Grained Parallelism

  2024influential citation
• A Unified, Practical, and Understandable Model of Non-transactional Consistency Levels in Distributed Replication

  2024influential citation
• Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations

  2024influential citation
• A Denotational Approach to Release/Acquire Concurrency

  2024cites this paper
• Robustness against the C/C++11 Memory Model

  2024cites this paper
• Trace and Algebraic Semantics for Partial Store Order Memory Model

  2024cites this paper
• QED: Scalable Verification of Hardware Memory Consistency

  2024cites this paper
• Sound Concurrent Traces for Online Monitoring

  2024cites this paper
• Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures

  2024cites this paper
• Decidable Verification under Localized Release-Acquire Concurrency

  2024cites this paper
• Nebula: Efficient read-write memory and switchboard circuits for folding schemes

  2024cites this paper
• Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability

  2023influential citation
• Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models

  2023cites this paper
• View-Based Axiomatic Reasoning for PSO (Extended Version)

  2023cites this paper
• An Operational Approach to Library Abstraction under Relaxed Memory Concurrency

  2023cites this paper
• Kater: Automating Weak Memory Model Metatheory and Consistency Checking

  2023cites this paper
• Probabilistic Concurrency Testing for Weak Memory Programs

  2023cites this paper
• Differentiated Consistency for Worldwide Gossips

  2023cites this paper
• MC Mutants: Evaluating and Improving Testing for Memory Consistency Specifications

  2023cites this paper
• Test Data Generation based on Multiprocess Enhanced Multi-Population Genetic Algorithm

  2023cites this paper
• EveCheck: An Event-Driven, Scalable Algorithm for Coherent Shared Memory Verification

  2023cites this paper
• Meow: Memory Evaluation through Optimized Workloads - Synthesizing Litmus Tests for Memory Consistency Verification

  2023cites this paper
• AirMesh: A RIPng and Raft Based Resilient Networking Approach for Unmanned Systems

  2023cites this paper
• A formal framework to design and prove trustworthy memory controllers

  2023cites this paper
• Optimal Bounded Partial Order Reduction

  2023cites this paper
• Simulating Operational Memory Models Using Off-the-Shelf Program Analysis Tools

  2023cites this paper
• Static Analysis of Memory Models for SMT Encodings

  2023cites this paper
• Halfmoon: Log-Optimal Fault-Tolerant Stateful Serverless Computing

  2023influential citation
• Compiler Testing with Relaxed Memory Models

  2023cites this paper
• Exploring the collaboration between FEniCSx and StarPU

  2023cites this paper
• CELLO: Compiler-Assisted Efficient Load-Load Ordering in Data-Race-Free Regions

  2023cites this paper
• TSO Games - On the decidability of safety games under the total store order semantics (extended version with appendix)

  2023cites this paper
• Seismic Full Waveform Inversion Accelerated by Overlapping Data Input and Computation

  2023cites this paper
• Unblocking Dynamic Partial Order Reduction

  2023influential citation
• TOSTING: Investigating Total Store Ordering on ARM

  2023cites this paper
• A Unified and Understandable Summary of Non-transactional Consistency Levels and Protocols for Distributed Replication

  2023influential citation
• Lifting the Reasoning Level in Generic Weak Memory Verification (Extended Version)

  2023cites this paper