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

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

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)

• Context-bounded analysis of TSO systems
• Effective Program Verification for Relaxed Memory Models
• Automatically comparing memory consistency models
• Stateless model checking for TSO and PSO
• Gradual consistency checking
• 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

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)