Sound and complete monitoring of sequential consistency for relaxed memory models

DOI10.1007/978-3-642-19835-9_3zbMATH Open1315.68084OpenAlexW1594825470MaRDI QIDQ3000633FDOQ3000633

Authors: Jabob Burnim, Koushik Sen, Christos Stergiou 

Publication date: 19 May 2011

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-19835-9_3

Recommendations

• Effective Program Verification for Relaxed Memory Models
• Stateless model checking for TSO and PSO
• Stateless model checking for TSO and PSO
• Effective abstractions for verification under relaxed memory models
• Effective Abstractions for Verification under Relaxed Memory Models

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Dynamic partial-order reduction for model checking software
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Computer Aided Verification
• Effective Program Verification for Relaxed Memory Models
• On the verification problem for weak memory models
• Memory model sensitive bytecode verification
• Sound and complete monitoring of sequential consistency for relaxed memory models

Cited In (15)

• Effective Program Verification for Relaxed Memory Models
• Automatically comparing memory consistency models
• Gradual consistency checking
• Stateless model checking for TSO and PSO
• Deciding Robustness against Total Store Ordering
• Efficiently and completely verifying synchronized consistency models
• From causal consistency to sequential consistency in shared memory systems
• Combining model checking and testing
• CCA-secure keyed-fully homomorphic encryption
• Stateless model checking for TSO and PSO
• On atomicity in presence of non-atomic writes
• Sound and complete monitoring of sequential consistency for relaxed memory models
• Model checking race-freedom when ``sequential consistency for data-race-free programs is guaranteed
• Verification of Concurrent Programs on Weak Memory Models
• Context-bounded analysis of TSO systems

Uses Software

• Checkfence

This page was built for publication: Sound and complete monitoring of sequential consistency for relaxed memory models

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