On the verification problem for weak memory models
From MaRDI portal
Recommendations
Cited in
(45)- The weakest memory-access order
- Data-race and concurrent-write freedom are undecidable.
- TSO-to-TSO linearizability is undecidable
- Static analysis of embedded real-time concurrent software with dynamic priorities
- Stateless model checking for TSO and PSO
- Cubicle-\(\mathcal{W}\): parameterized model checking on weak memory
- A wide-spectrum language for verification of programs on weak memory models
- Parameterized model checking on the TSO weak memory model
- The decidability of verification under PS 2.0
- Checking robustness between weak transactional consistency models
- Trading fences with RMRs and separating memory models
- Complexity hierarchies beyond elementary
- Studying Operational Models of Relaxed Concurrency
- What's decidable about weak memory models?
- Reasoning algebraically about refinement on TSO architectures
- Can we efficiently check concurrent programs under relaxed memory models in Maude?
- Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
- Static analysis of run-time errors in embedded critical parallel C programs
- Sound and complete monitoring of sequential consistency for relaxed memory models
- Deciding Robustness against Total Store Ordering
- A load-buffer semantics for total store ordering
- Verification of Concurrent Programs on Weak Memory Models
- Efficiently and completely verifying synchronized consistency models
- Fences in weak memory models
- Regular separability of well-structured transition systems
- An Observational Approach to Defining Linearizability on Weak Memory Models
- Robustness against Power is PSpace-complete
- Context-bounded analysis of TSO systems
- Stateless model checking for TSO and PSO
- A framework for correctness criteria on weak memory models
- View abstraction -- a tutorial (invited paper)
- A verification-based approach to memory fence insertion in PSO memory systems
- scientific article; zbMATH DE number 7327945 (Why is no real title available?)
- Parallelized sequential composition and hardware weak memory models
- Probabilistic total store ordering
- Decidability of liveness for concurrent objects on the TSO memory model
- Reasoning about promises in weak memory models with event structures
- A fine-grained semantics for arrays and pointers under weak memory models
- Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models
- Value-dependent information-flow security on weak memory models
- Effective abstractions for verification under relaxed memory models
- TSO games -- on the decidability of safety games under the total store order semantics
- Reachability and safety games under TSO semantics
- TSO games -- on the decidability of safety games under the total store order semantics
- The complexity of weak consistency
This page was built for publication: On the verification problem for weak memory models
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5255057)
