How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
From MaRDI portal
Publication:3853114
DOI10.1109/TC.1979.1675439zbMath0419.68045OpenAlexW2054739713WikidataQ55871189 ScholiaQ55871189MaRDI QIDQ3853114
Publication date: 1979
Published in: IEEE Transactions on Computers (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1109/tc.1979.1675439
Related Items
Distributed Adaptive Systems ⋮ Local Data Race Freedom with Non-multi-copy Atomicity ⋮ On grainless footprint semantics for shared-memory programs ⋮ A denotational semantics for SPARC TSO ⋮ Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ TSO-to-TSO linearizability is undecidable ⋮ Owicki-Gries Reasoning for Weak Memory Models ⋮ Concurrent abstract state machines ⋮ Optimal propagation-based protocols implementing causal memories ⋮ Implementing dataflow with threads ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Verification of Concurrent Programs on Weak Memory Models ⋮ Of Concurrent Data Structures and Iterations ⋮ Relationships between memory models ⋮ Model checking a cache coherence protocol of a Java DSM implementation ⋮ Mechanising a type-safe model of multithreaded Java with a verified compiler ⋮ Tractable low-delay atomic memory ⋮ Mechanized proofs of opacity: a comparison of two techniques ⋮ The queue-read queue-write asynchronous PRAM model ⋮ Eliminating partially dead code in explicitly parallel programs ⋮ Unnamed Item ⋮ Decidability and complexity for quiescent consistency and its variations ⋮ On projective and separable properties ⋮ Abstraction for concurrent objects ⋮ Checking causal consistency of distributed databases ⋮ Parallelized sequential composition and hardware weak memory models ⋮ Sound concurrent traces for online monitoring ⋮ Data-race and concurrent-write freedom are undecidable. ⋮ Making Linearizability Compositional for Partially Ordered Executions ⋮ Quantifiability: a concurrent correctness condition modeled in vector space ⋮ An algorithmic approach for checking closure properties of Ω-regular languages ⋮ Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions ⋮ Probabilistic total store ordering ⋮ Decidability of liveness for concurrent objects on the TSO memory model ⋮ Contextuality in distributed systems ⋮ Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability ⋮ Implementing sequentially consistent programs on processor consistent platforms ⋮ Parameterized model checking on the TSO weak memory model ⋮ Randomized registers and iterative algorithms ⋮ An operational happens-before memory model ⋮ Verification of STM on relaxed memory models ⋮ Tackling Real-Life Relaxed Concurrency with FSL++ ⋮ The Synchronization Power of Coalesced Memory Accesses ⋮ Causal memory: definitions, implementation, and programming ⋮ Implementing hybrid consistency with high-level synchronization operations ⋮ Linearizable counting networks ⋮ Lock-free reference counting ⋮ Hundreds of impossibility results for distributed computing ⋮ Robustness Against Transactional Causal Consistency. ⋮ Semantics of Concurrent Revisions ⋮ Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs ⋮ Transactional memory ⋮ Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models ⋮ Set-constrained delivery broadcast: a communication abstraction for Read/write implementable distributed objects ⋮ Memory model sensitive bytecode verification ⋮ Concurrent correctness in vector space ⋮ Deciding Robustness against Total Store Ordering ⋮ MODELS AND TRENDS IN PARALLEL PROGRAMMING ⋮ Effective abstractions for verification under relaxed memory models ⋮ Extended parallelism in the Gröbner basis algorithm ⋮ The computability of relaxed data structures: queues and stacks as examples ⋮ Composing ordered sequential consistency ⋮ Contention-sensitive data structures and algorithms ⋮ Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Fork sequential consistency is blocking ⋮ Unnamed Item ⋮ A unifying logic for non-deterministic, parallel and concurrent abstract state machines ⋮ Operational semantics of a weak memory model with channel synchronization ⋮ Schedulers and finishers: on generating and filtering the behaviours of an event structure ⋮ Operational semantics of a weak memory model with channel synchronization ⋮ CCA-Secure Keyed-Fully Homomorphic Encryption ⋮ Unnamed Item ⋮ A Framework for Correctness Criteria on Weak Memory Models ⋮ Operational semantics with semicommutations ⋮ On the composability of consistency conditions ⋮ Unnamed Item ⋮ Sequentially consistent versus linearizable counting networks ⋮ An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages ⋮ Studying Operational Models of Relaxed Concurrency ⋮ A Behavioural Theory of Recursive Algorithms ⋮ Timing conditions for linearizability in uniform counting networks ⋮ Eventually-serializable data services ⋮ Linearizable read/write objects ⋮ On the definition of sequential consistency ⋮ Strict Linearizability and Abstract Atomicity ⋮ Model-checking of correctness conditions for concurrent objects
