Sound and complete monitoring of sequential consistency for relaxed memory models

DOI10.1007/978-3-642-19835-9_3MaRDI QIDQ3000633zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(15)

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

Describes a project that uses

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)