Verifying sequential consistency on shared-memory multiprocessor systems

DOI10.1007/3-540-48683-6_27MaRDI QIDQ4818798zbMATH OpenFDO

Authors Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani

Publication date 24 September 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48683-6_27

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Automatable verification of sequential consistency
• Computer Aided Verification
• Testing Shared Memories
• A unified theory of shared memory consistency
• Characterization of a sequentially consistent memory and verification of a cache memory by abstraction

Cited in

(29)

• Automatable verification of sequential consistency
• Structured development of a virtual shared memory system
• Verifying correctness of persistent concurrent data structures: a sound and complete method
• On the correctness problem for serializability
• Model checking transactional memories
• From causal consistency to sequential consistency in shared memory systems
• A unified theory of shared memory consistency
• An operational model for multiprocessors with caches
• Parameterized Verification of Asynchronous Shared-Memory Systems
• scientific article; zbMATH DE number 7295368 (Why is no real title available?)
• Efficiently and completely verifying synchronized consistency models
• Implied Set Closure and Its Application to Memory Consistency Verification
• Capturing Register and Control Dependence in Memory Consistency Models with Applications to the Itanium Architecture
• scientific article; zbMATH DE number 53304 (Why is no real title available?)
• Testing Shared Memories
• Shared Memory Consistency Conditions for Nonsequential Execution: Definitions and Programming Strategies
• Sequential consistency as lazy linearizability
• A specification and verification framework for developing weak shared memory consistency protocols
• Using timestamping and history variables to verify sequential consistency
• Extending memory consistency of finite prefixes to infinite computations
• Shared memory consistency protocol verification against weak memory models: Refinement via model-checking
• Cache consistency by design
• Characterization of a sequentially consistent memory and verification of a cache memory by abstraction
• Computer Aided Verification
• Computer Aided Verification
• Ogre and Pythia: an invariance proof method for weak consistency models
• Verifying Parameterized taDOM+ Lock Managers
• Gradual consistency checking
• Model checking a cache coherence protocol of a Java DSM implementation

Describes a project that uses

Uses Software

• PVS
• SNOOPY
• MOCHA

This page was built for publication: Verifying sequential consistency on shared-memory multiprocessor systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4818798)