Concurrent Library Correctness on the TSO Memory Model
From MaRDI portal
Recommendations
- Decidability of liveness for concurrent objects on the TSO memory model
- Verification of Concurrent Programs on Weak Memory Models
- Observation-based concurrent program logic for relaxed memory consistency models
- Semantics, specification, and bounded verification of concurrent libraries in replicated systems
- CompCertTSO
- Correctness properties in a shared-memory parallel language
Cited in
(18)- Unifying Operational Weak Memory Verification: An Axiomatic Approach
- Higher-order linearisability
- Semantics, specification, and bounded verification of concurrent libraries in replicated systems
- Balancing expressiveness in formal approaches to concurrency
- TSO-to-TSO linearizability is undecidable
- Linearizability with ownership transfer
- TSO-to-TSO linearizability is undecidable
- Bounded TSO-to-SC linearizability is decidable
- Model checking simulation rules for linearizability
- Linearizability with ownership transfer
- Library abstraction for C/C++ concurrency
- Decidability of liveness for concurrent objects on the TSO memory model
- Linearizability on hardware weak memory models
- A framework for correctness criteria on weak memory models
- Parameterised linearisability
- Making Linearizability Compositional for Partially Ordered Executions
- Higher-order linearisability
- Show no weakness: sequentially consistent specifications of TSO libraries
This page was built for publication: Concurrent Library Correctness on the TSO Memory Model
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2892722)
