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)

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

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)